wneuper/isa: src/Tools/isac/Knowledge/RootRatEq.thy@460c24a6a6ba

     1 (* collecting all knowledge for Root and Rational Equations

     2    created by: rlang

     3          date: 02.10

     4    changed by: rlang

     5    last change by: rlang

     6              date: 02.11.04

     7    (c) by Richard Lang, 2003

     8 *)

    10 theory RootRatEq imports LinEq RootEq RatEq RootRat begin

    12 consts

    14   is'_rootRatAddTerm'_in :: "[real, real] => bool"

    15                              ("_ is'_rootRatAddTerm'_in _") (*RL DA*)

    17 (*---------scripts--------------------------*)

    18   Elim'_rootrat'_equation

    19              :: "[bool,real,

    20 		    bool list] => bool list"

    21                ("((Script Elim'_rootrat'_equation (_ _ =))//

    22                    (_))" 9)

    23  (*-------------------- rules------------------------------------------------*)

    25 axioms

    26   (* eliminate ratRootTerm *)

    27   rootrat_equation_left_1:

    28    "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"

    29   rootrat_equation_left_2:

    30    "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"

    31   rootrat_equation_right_2:

    32    "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"

    33   rootrat_equation_right_1:

    34    "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"

    36 ML {*

    37 val thy = @{theory};

    39 (*-------------------------functions---------------------*)

    40 (* true if denominator contains (sq)root in + or - term

    41    1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true

    42    if false then (term)^2 contains no (sq)root *)

    43 fun is_rootRatAddTerm_in t v =

    44     let

    45 	fun coeff_in c v = member op = (vars c) v;

    46 	fun rootadd (t as (Const ("Groups.plus_class.plus",_) $ t2 $ t3)) v =

    47             (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)

    48 	  | rootadd (t as (Const ("Groups.minus_class.minus",_) $ t2 $ t3)) v =

    49             (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)

    50 	  | rootadd _ _ = false;

    51 	fun findrootrat (_ $ _ $ _ $ _) v = error("is_rootRatAddTerm_in:")

    52 	  (* at the moment there is no term like this, but ....*)

    53 	  | findrootrat (t as (Const ("Rings.inverse_class.divide",_) $ _ $ t3)) v =

    54 	               if (is_rootTerm_in t3 v) then rootadd t3 v else false

    55 	  | findrootrat (_ $ t1 $ t2) v =

    56             (findrootrat t1 v) orelse (findrootrat t2 v)

    57 	  | findrootrat (_ $ t1) v = (findrootrat t1 v)

    58 	  | findrootrat _ _ = false;

    59      in

    60 	findrootrat t v

    61     end;

    63 fun eval_is_rootRatAddTerm_in _ _

    64            (p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _  =

    65     if is_rootRatAddTerm_in t v then

    66 	SOME ((term2str p) ^ " = True",

    67 	      Trueprop $ (mk_equality (p, HOLogic.true_const)))

    68     else SOME ((term2str p) ^ " = True",

    69 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))

    70   | eval_is_rootRatAddTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);

    71 *}

    72 ML {*

    73 (*-------------------------rulse-------------------------*)

    74 val RootRatEq_prls =

    75     append_rls "RootRatEq_prls" e_rls

    76 		[Calc ("Atools.ident",eval_ident "#ident_"),

    77                  Calc ("Tools.matches",eval_matches ""),

    78                  Calc ("Tools.lhs"    ,eval_lhs ""),

    79                  Calc ("Tools.rhs"    ,eval_rhs ""),

    80                  Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),

    81                  Calc ("RootRatEq.is'_rootRatAddTerm'_in",

    82                        eval_is_rootRatAddTerm_in ""),

    83                  Calc ("op =",eval_equal "#equal_"),

    84                  Thm ("not_true",num_str @{thm not_true}),

    85                  Thm ("not_false",num_str @{thm not_false}),

    86                  Thm ("and_true",num_str @{thm and_true}),

    87                  Thm ("and_false",num_str @{thm and_false}),

    88                  Thm ("or_true",num_str @{thm or_true}),

    89                  Thm ("or_false",num_str @{thm or_false})

    90 		 ];

    92 val RooRatEq_erls =

    93     merge_rls "RooRatEq_erls" rootrat_erls

    94     (merge_rls "" RootEq_erls

    95      (merge_rls "" rateq_erls

    96       (append_rls "" e_rls

    97 		[])));

    99 val RootRatEq_crls =

   100     merge_rls "RootRatEq_crls" rootrat_erls

   101     (merge_rls "" RootEq_erls

   102      (merge_rls "" rateq_erls

   103       (append_rls "" e_rls

   104 		[])));

   106 ruleset' := overwritelthy @{theory} (!ruleset',

   107 	     [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]);

   109 *}

   110 ML {*

   111 (* Solves a rootrat Equation *)

   112  val rootrat_solve = prep_rls(

   113      Rls {id = "rootrat_solve", preconds = [],

   114 	  rew_ord = ("termlessI",termlessI),

   115      erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)

   116      rules =

   117      [Thm("rootrat_equation_left_1", num_str @{thm rootrat_equation_left_1}),

   118 	        (* [|c is_rootTerm_in bdv|] ==>

   119                                     ( (a + b/c = d) = ( b = (d - a) * c )) *)

   120       Thm("rootrat_equation_left_2",num_str @{thm rootrat_equation_left_2}),

   121 	        (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)

   122       Thm("rootrat_equation_right_1",num_str @{thm rootrat_equation_right_1}),

   123 		(* [|f is_rootTerm_in bdv|] ==>

   124                                     ( (a = d + e/f) = ( (a - d) * f = e )) *)

   125       Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})

   126 		(* [|f is_rootTerm_in bdv|] ==> ( (a =  e/f) = ( a  * f = e ))*)

   127       ], scr = Script ((term_of o the o (parse thy)) "empty_script")}:rls);

   129 ruleset' := overwritelthy @{theory} (!ruleset',

   130 			[("rootrat_solve",rootrat_solve)

   131 			 ]);

   132 *}

   133 ML {*

   135 (*-----------------------probleme------------------------*)

   136 (*

   137 (get_pbt ["rat","root'","univariate","equation"]);

   138 show_ptyps();

   139 *)

   141 store_pbt

   142  (prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID

   143  (["rat","sq","root'","univariate","equation"],

   144   [("#Given" ,["equality e_e","solveFor v_v"]),

   145    ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^

   146 	       "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),

   147    ("#Find"  ,["solutions v_v'i'"])

   148    ],

   149   RootRatEq_prls, SOME "solve (e_e::bool, v_v)",

   150   [["RootRatEq","elim_rootrat_equation"]]));

   151 *}

   152 ML {*

   153 (*-------------------------Methode-----------------------*)

   154 store_met

   155  (prep_met (theory "LinEq") "met_rootrateq" [] e_metID

   156  (["RootRatEq"],

   157    [],

   158    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,

   159     crls=Atools_erls, nrls=norm_Rational}, "empty_script"));

   160 (*-- left 20.10.02 --*)

   161 store_met

   162  (prep_met thy "met_rootrateq_elim" [] e_metID

   163  (["RootRatEq","elim_rootrat_equation"],

   164    [("#Given" ,["equality e_e","solveFor v_v"]),

   165     ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^

   166 	       "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),

   167     ("#Find"  ,["solutions v_v'i'"])

   168    ],

   169    {rew_ord'="termlessI",

   170     rls'=RooRatEq_erls,

   171     srls=e_rls,

   172     prls=RootRatEq_prls,

   173     calc=[],

   174     crls=RootRatEq_crls, nrls=norm_Rational(*,

   175     asm_rls=[],

   176     asm_thm=[]*)},

   177    "Script Elim_rootrat_equation  (e_e::bool) (v_v::real)  =      " ^

   178     "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@  " ^

   179     "           (Try (Rewrite_Set rooteq_simplify   False)) @@  " ^

   180     "           (Try (Rewrite_Set make_rooteq       False)) @@  " ^

   181     "           (Try (Rewrite_Set rooteq_simplify   False)) @@  " ^

   182     "           (Try (Rewrite_Set_Inst [(bdv,v_v)]               " ^

   183     "                                  rootrat_solve False))) e_e " ^

   184     " in (SubProblem (RootEq',[univariate,equation],            " ^

   185     "        [no_met]) [BOOL e_e, REAL v_v]))"

   186    ));

   187 calclist':= overwritel (!calclist',

   188    [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in",

   189 			      eval_is_rootRatAddTerm_in""))

   190     ]);

   191 *}

   193 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 09:06:56 +0200
branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38015	67ba02dffacc
child 40836	69364e021751
permissions	-rw-r--r--