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

     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 text {* univariate equations over rational terms containing real square roots:

    13   In 2003 this type has been developed as part of ISAC's equation solver

    14   by Richard Lang in 2003.

    15   The migration Isabelle2002 --> 2011 dropped this type of equation, see RootEq.thy.

    16 *}

    18 consts

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

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

    23 (*---------scripts--------------------------*)

    24   Elim'_rootrat'_equation

    25              :: "[bool,real,

    26 		    bool list] => bool list"

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

    28                    (_))" 9)

    29  (*-------------------- rules------------------------------------------------*)

    31 axiomatization where

    32   (* eliminate ratRootTerm *)

    33   rootrat_equation_left_1:

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

    35   rootrat_equation_left_2:

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

    37   rootrat_equation_right_2:

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

    39   rootrat_equation_right_1:

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

    42 ML {*

    43 val thy = @{theory};

    45 (*-------------------------functions---------------------*)

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

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

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

    49 fun is_rootRatAddTerm_in t v =

    50     let

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

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

    53             (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)

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

    55             (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)

    56 	  | rootadd _ _ = false;

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

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

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

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

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

    62             (findrootrat t1 v) orelse (findrootrat t2 v)

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

    64 	  | findrootrat _ _ = false;

    65      in

    66 	findrootrat t v

    67     end;

    69 fun eval_is_rootRatAddTerm_in _ _

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

    71     if is_rootRatAddTerm_in t v then

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

    73 	      Trueprop $ (mk_equality (p, @{term True})))

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

    75 	       Trueprop $ (mk_equality (p, @{term False})))

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

    77 *}

    78 ML {*

    79 (*-------------------------rulse-------------------------*)

    80 val RootRatEq_prls =

    81     append_rls "RootRatEq_prls" e_rls

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

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

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

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

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

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

    88                        eval_is_rootRatAddTerm_in ""),

    89                  Calc ("HOL.eq",eval_equal "#equal_"),

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

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

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

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

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

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

    96 		 ];

    98 val RooRatEq_erls =

    99     merge_rls "RooRatEq_erls" rootrat_erls

   100     (merge_rls "" RootEq_erls

   101      (merge_rls "" rateq_erls

   102       (append_rls "" e_rls

   103 		[])));

   105 val RootRatEq_crls =

   106     merge_rls "RootRatEq_crls" rootrat_erls

   107     (merge_rls "" RootEq_erls

   108      (merge_rls "" rateq_erls

   109       (append_rls "" e_rls

   110 		[])));

   111 *}

   112 setup {* KEStore_Elems.add_rlss

   113   [("RooRatEq_erls", (Context.theory_name @{theory}, RooRatEq_erls))] *}

   114 ML {*

   115 (* Solves a rootrat Equation *)

   116  val rootrat_solve = prep_rls(

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

   118 	  rew_ord = ("termlessI",termlessI),

   119      erls = e_rls, srls = Erls, calc = [], errpatts = [],

   120      rules =

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

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

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

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

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

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

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

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

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

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

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

   132 *}

   133 setup {* KEStore_Elems.add_rlss

   134   [("rootrat_solve", (Context.theory_name @{theory}, rootrat_solve))] *}

   135 ML {*

   137 (*-----------------------probleme------------------------*)

   138 (*

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

   140 show_ptyps();

   141 *)

   143 store_pbt

   144  (prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID

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

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

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

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

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

   150    ],

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

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

   153 *}

   154 ML {*

   155 (*-------------------------Methode-----------------------*)

   156 store_met

   157  (prep_met @{theory LinEq} "met_rootrateq" [] e_metID

   158  (["RootRatEq"],

   159    [],

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

   161     crls=Atools_erls, errpats = [], nrls = norm_Rational}, "empty_script"));

   162 (*-- left 20.10.02 --*)

   163 store_met

   164  (prep_met thy "met_rootrateq_elim" [] e_metID

   165  (["RootRatEq","elim_rootrat_equation"],

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

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

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

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

   170    ],

   171    {rew_ord'="termlessI",

   172     rls'=RooRatEq_erls,

   173     srls=e_rls,

   174     prls=RootRatEq_prls,

   175     calc=[],

   176     crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},

   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 *}

   188 setup {* KEStore_Elems.add_calcs

   189   [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", eval_is_rootRatAddTerm_in""))] *}

   191 end

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Fri, 25 Oct 2013 20:58:28 +0100
changeset 52159	db46e97751eb
parent 52155	e4ddf21390fd
child 55339	cccd24e959ba
permissions	-rw-r--r--