neuper@37906: (* collecting all knowledge for Root and Rational Equations
neuper@37906:    created by: rlang 
neuper@37906:          date: 02.10
neuper@37906:    changed by: rlang
neuper@37906:    last change by: rlang
neuper@37906:              date: 02.11.04
neuper@37954:    (c) by Richard Lang, 2003
neuper@37906: *)
neuper@37906: 
neuper@37954: theory RootRatEq imports RootEq RatEq RootRat begin 
neuper@37906: 
neuper@37906: consts
neuper@37906: 
neuper@37954:   is'_rootRatAddTerm'_in :: "[real, real] => bool" 
neuper@37954:                              ("_ is'_rootRatAddTerm'_in _") (*RL DA*)
neuper@37906: 
neuper@37906: (*---------scripts--------------------------*)
neuper@37906:   Elim'_rootrat'_equation
neuper@37954:              :: "[bool,real,  
neuper@37954: 		    bool list] => bool list"
neuper@37954:                ("((Script Elim'_rootrat'_equation (_ _ =))//  
neuper@37954:                    (_))" 9)
neuper@37906:  (*-------------------- rules------------------------------------------------*)
neuper@37906: 
neuper@37954: axioms
neuper@37906:   (* eliminate ratRootTerm *)
neuper@37906:   rootrat_equation_left_1
neuper@37906:    "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"
neuper@37906:   rootrat_equation_left_2
neuper@37906:    "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"
neuper@37906:   rootrat_equation_right_2
neuper@37906:    "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"
neuper@37906:   rootrat_equation_right_1
neuper@37906:    "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
neuper@37906: 
neuper@37954: ML {*
neuper@37954: (*-------------------------functions---------------------*)
neuper@37954: (* true if denominator contains (sq)root in + or - term 
neuper@37954:    1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true
neuper@37954:    if false then (term)^2 contains no (sq)root *)
neuper@37954: fun is_rootRatAddTerm_in t v = 
neuper@37954:     let 
neuper@37954: 	fun coeff_in c v = member op = (vars c) v;
neuper@37954: 	fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = 
neuper@37954:             (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
neuper@37954: 	  | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = 
neuper@37954:             (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
neuper@37954: 	  | rootadd _ _ = false;
neuper@37954: 	fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:")
neuper@37954: 	  (* at the moment there is no term like this, but ....*)
neuper@37954: 	  | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v = 
neuper@37954: 	               if (is_rootTerm_in t3 v) then rootadd t3 v else false
neuper@37954: 	  | findrootrat (_ $ t1 $ t2) v = 
neuper@37954:             (findrootrat t1 v) orelse (findrootrat t2 v)
neuper@37954: 	  | findrootrat (_ $ t1) v = (findrootrat t1 v)
neuper@37954: 	  | findrootrat _ _ = false;
neuper@37954:      in
neuper@37954: 	findrootrat t v
neuper@37954:     end;
neuper@37906: 
neuper@37954: fun eval_is_rootRatAddTerm_in _ _ 
neuper@37954:            (p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _  =
neuper@37954:     if is_rootRatAddTerm_in t v then 
neuper@37954: 	SOME ((term2str p) ^ " = True",
neuper@37954: 	      Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37954:     else SOME ((term2str p) ^ " = True",
neuper@37954: 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37954:   | eval_is_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
neuper@37954: 
neuper@37954: (*-------------------------rulse-------------------------*)
neuper@37954: val RootRatEq_prls = 
neuper@37954:     append_rls "RootRatEq_prls" e_rls
neuper@37954: 		[Calc ("Atools.ident",eval_ident "#ident_"),
neuper@37954:                  Calc ("Tools.matches",eval_matches ""),
neuper@37954:                  Calc ("Tools.lhs"    ,eval_lhs ""),
neuper@37954:                  Calc ("Tools.rhs"    ,eval_rhs ""),
neuper@37954:                  Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
neuper@37954:                  Calc ("RootRatEq.is'_rootRatAddTerm'_in", 
neuper@37954:                        eval_is_rootRatAddTerm_in ""),
neuper@37954:                  Calc ("op =",eval_equal "#equal_"),
neuper@37966:                  Thm ("not_true",num_str @{not_true),
neuper@37966:                  Thm ("not_false",num_str @{not_false),
neuper@37966:                  Thm ("and_true",num_str @{and_true),
neuper@37966:                  Thm ("and_false",num_str @{and_false),
neuper@37966:                  Thm ("or_true",num_str @{or_true),
neuper@37966:                  Thm ("or_false",num_str @{or_false)
neuper@37954: 		 ];
neuper@37954: 
neuper@37954: val RooRatEq_erls = 
neuper@37954:     merge_rls "RooRatEq_erls" rootrat_erls
neuper@37954:     (merge_rls "" RootEq_erls
neuper@37954:      (merge_rls "" rateq_erls
neuper@37954:       (append_rls "" e_rls
neuper@37954: 		[])));
neuper@37954: 
neuper@37954: val RootRatEq_crls = 
neuper@37954:     merge_rls "RootRatEq_crls" rootrat_erls
neuper@37954:     (merge_rls "" RootEq_erls
neuper@37954:      (merge_rls "" rateq_erls
neuper@37954:       (append_rls "" e_rls
neuper@37954: 		[])));
neuper@37954: 
neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37954: 	     [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]);
neuper@37954: 
neuper@37954: (* Solves a rootrat Equation *)
neuper@37954:  val rootrat_solve = prep_rls(
neuper@37954:      Rls {id = "rootrat_solve", preconds = [], 
neuper@37954: 	  rew_ord = ("termlessI",termlessI), 
neuper@37954:      erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
neuper@37966:      rules = [Thm("rootrat_equation_left_1", num_str @{rootrat_equation_left_1),   
neuper@37954: 	        (* [|c is_rootTerm_in bdv|] ==> 
neuper@37954:                                     ( (a + b/c = d) = ( b = (d - a) * c )) *)
neuper@37966:               Thm("rootrat_equation_left_2",num_str @{rootrat_equation_left_2),
neuper@37954: 	        (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
neuper@37966: 	      Thm("rootrat_equation_right_1",num_str @{rootrat_equation_right_1),
neuper@37954: 		(* [|f is_rootTerm_in bdv|] ==> 
neuper@37954:                                     ( (a = d + e/f) = ( (a - d) * f = e )) *)
neuper@37966: 	      Thm("rootrat_equation_right_2",num_str @{rootrat_equation_right_2)
neuper@37954: 		(* [|f is_rootTerm_in bdv|] ==> ( (a =  e/f) = ( a  * f = e ))*)
neuper@37954: 	      ],
neuper@37954: 	 scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954:          }:rls);
neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37954: 			[("rootrat_solve",rootrat_solve)
neuper@37954: 			 ]);
neuper@37954: 
neuper@37954: (*-----------------------probleme------------------------*)
neuper@37954: (*
neuper@37954: (get_pbt ["rat","root","univariate","equation"]);
neuper@37954: show_ptyps(); 
neuper@37954: *)
neuper@37954: store_pbt
neuper@37954:  (prep_pbt (theory "RootRatEq") "pbl_equ_univ_root_sq_rat" [] e_pblID
neuper@37954:  (["rat","sq","root","univariate","equation"],
neuper@37954:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37954:    ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) )| " ^
neuper@37954: 	       "( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]),
neuper@37954:    ("#Find"  ,["solutions v_i_"])
neuper@37954:    ],
neuper@37954:   RootRatEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954:   [["RootRatEq","elim_rootrat_equation"]]));
neuper@37954: 
neuper@37954: (*-------------------------Methode-----------------------*)
neuper@37954: store_met
neuper@37954:  (prep_met (theory "LinEq") "met_rootrateq" [] e_metID
neuper@37954:  (["RootRatEq"],
neuper@37954:    [],
neuper@37954:    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
neuper@37954:     crls=Atools_erls, nrls=norm_Rational}, "empty_script"));
neuper@37954: (*-- left 20.10.02 --*)
neuper@37954: store_met
neuper@37954:  (prep_met (theory "RootRatEq") "met_rootrateq_elim" [] e_metID
neuper@37954:  (["RootRatEq","elim_rootrat_equation"],
neuper@37954:    [("#Given" ,["equality e_","solveFor v_"]),
neuper@37954:     ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) ) | " ^
neuper@37954: 	       "( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]),
neuper@37954:     ("#Find"  ,["solutions v_i_"])
neuper@37954:    ],
neuper@37954:    {rew_ord'="termlessI",
neuper@37954:     rls'=RooRatEq_erls,
neuper@37954:     srls=e_rls,
neuper@37954:     prls=RootRatEq_prls,
neuper@37954:     calc=[],
neuper@37954:     crls=RootRatEq_crls, nrls=norm_Rational(*,
neuper@37954:     asm_rls=[],
neuper@37954:     asm_thm=[]*)},
neuper@37954:    "Script Elim_rootrat_equation  (e_::bool) (v_::real)  =      " ^
neuper@37954:     "(let e_ = ((Try (Rewrite_Set expand_rootbinoms False)) @@  " ^ 
neuper@37954:     "           (Try (Rewrite_Set rooteq_simplify   False)) @@  " ^ 
neuper@37954:     "           (Try (Rewrite_Set make_rooteq       False)) @@  " ^
neuper@37954:     "           (Try (Rewrite_Set rooteq_simplify   False)) @@  " ^
neuper@37954:     "           (Try (Rewrite_Set_Inst [(bdv,v_)]               " ^
neuper@37954:     "                                  rootrat_solve False))) e_ " ^
neuper@37954:     " in (SubProblem (RootEq_,[univariate,equation],            " ^
neuper@37954:     "        [no_met]) [bool_ e_, real_ v_]))"
neuper@37954:    ));
neuper@37954: calclist':= overwritel (!calclist', 
neuper@37954:    [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", 
neuper@37954: 			      eval_is_rootRatAddTerm_in""))
neuper@37954:     ]);
neuper@37954: *}
neuper@37906: 
neuper@37906: end