wneuper/isa: src/Tools/isac/Knowledge/RootRatEq.ML@22235e4dbe5f

     1 (*.(c) by Richard Lang, 2003 .*)

     2 (* collecting all knowledge for Root and Rational Equations

     3    created by: rlang

     4          date: 02.10

     5    changed by: rlang

     6    last change by: rlang

     7              date: 02.11.04

     8 *)

    10 (* use"knowledge/RootRatEq.ML";

    11    use"RootRatEq.ML";

    13    use"ROOT.ML";

    14    cd"knowledge";

    16    remove_thy"RootRatEq";

    17    use_thy"Isac";

    18    *)

    20 "******* RootRatEq.ML begin *******";

    21 theory' := overwritel (!theory', [("RootRatEq.thy",RootRatEq.thy)]);

    23 (*-------------------------functions---------------------*)

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

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

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

    27 fun is_rootRatAddTerm_in t v =

    28     let

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

    30 	fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse

    31 	                                                    (is_rootTerm_in t3 v)

    32 	  | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse

    33                                                             (is_rootTerm_in t3 v)

    34 	  | rootadd _ _ = false;

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

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

    37 	  | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v =

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

    39 	  | findrootrat (_ $ t1 $ t2) v = (findrootrat t1 v) orelse (findrootrat t2 v)

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

    41 	  | findrootrat _ _ = false;

    42      in

    43 	findrootrat t v

    44     end;

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

    47     if is_rootRatAddTerm_in t v then

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

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

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

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

    52   | eval_is_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);

    54 (*-------------------------rulse-------------------------*)

    55 val RootRatEq_prls =

    56     append_rls "RootRatEq_prls" e_rls

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

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

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

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

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

    62                  Calc ("RootRatEq.is'_rootRatAddTerm'_in", eval_is_rootRatAddTerm_in ""),

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

    64                  Thm ("not_true",num_str not_true),

    65                  Thm ("not_false",num_str not_false),

    66                  Thm ("and_true",num_str and_true),

    67                  Thm ("and_false",num_str and_false),

    68                  Thm ("or_true",num_str or_true),

    69                  Thm ("or_false",num_str or_false)

    70 		 ];

    73 val RooRatEq_erls =

    74     merge_rls "RooRatEq_erls" rootrat_erls

    75     (merge_rls "" RootEq_erls

    76      (merge_rls "" rateq_erls

    77       (append_rls "" e_rls

    78 		[])));

    80 val RootRatEq_crls =

    81     merge_rls "RootRatEq_crls" rootrat_erls

    82     (merge_rls "" RootEq_erls

    83      (merge_rls "" rateq_erls

    84       (append_rls "" e_rls

    85 		[])));

    87 ruleset' := overwritelthy thy (!ruleset',

    88 			[("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)

    89 			 ]);

    91 (* Solves a rootrat Equation *)

    92  val rootrat_solve = prep_rls(

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

    94 	  rew_ord = ("termlessI",termlessI),

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

    96      rules = [  Thm("rootrat_equation_left_1",num_str rootrat_equation_left_1),

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

    98                 Thm("rootrat_equation_left_2",num_str rootrat_equation_left_2),

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

   100 	        Thm("rootrat_equation_right_1",num_str rootrat_equation_right_1),

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

   102 	        Thm("rootrat_equation_right_2",num_str rootrat_equation_right_2)

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

   104 	      ],

   105 	 scr = Script ((term_of o the o (parse thy)) "empty_script")

   106          }:rls);

   107 ruleset' := overwritelthy thy (!ruleset',

   108 			[("rootrat_solve",rootrat_solve)

   109 			 ]);

   111 (*-----------------------probleme------------------------*)

   112 (*

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

   114 show_ptyps();

   115 *)

   116 store_pbt

   117  (prep_pbt RootRatEq.thy "pbl_equ_univ_root_sq_rat" [] e_pblID

   118  (["rat","sq","root","univariate","equation"],

   119   [("#Given" ,["equality e_","solveFor v_"]),

   120    ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) )| \

   121 	       \( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]),

   122    ("#Find"  ,["solutions v_i_"])

   123    ],

   124   RootRatEq_prls, SOME "solve (e_::bool, v_)",

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

   127 (*-------------------------Methode-----------------------*)

   128 store_met

   129  (prep_met LinEq.thy "met_rootrateq" [] e_metID

   130  (["RootRatEq"],

   131    [],

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

   133     crls=Atools_erls, nrls=norm_Rational(*,

   134     asm_rls=[],asm_thm=[]*)}, "empty_script"));

   135 (*-- left 20.10.02 --*)

   136 store_met

   137  (prep_met RootRatEq.thy "met_rootrateq_elim" [] e_metID

   138  (["RootRatEq","elim_rootrat_equation"],

   139    [("#Given" ,["equality e_","solveFor v_"]),

   140     ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) ) | \

   141 	       \( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]),

   142     ("#Find"  ,["solutions v_i_"])

   143    ],

   144    {rew_ord'="termlessI",

   145     rls'=RooRatEq_erls,

   146     srls=e_rls,

   147     prls=RootRatEq_prls,

   148     calc=[],

   149     crls=RootRatEq_crls, nrls=norm_Rational(*,

   150     asm_rls=[],

   151     asm_thm=[]*)},

   152    "Script Elim_rootrat_equation  (e_::bool) (v_::real)  =      \

   153     \(let e_ = ((Try (Rewrite_Set expand_rootbinoms False)) @@  \

   154     \           (Try (Rewrite_Set rooteq_simplify   False)) @@  \

   155     \           (Try (Rewrite_Set make_rooteq       False)) @@  \

   156     \           (Try (Rewrite_Set rooteq_simplify   False)) @@  \

   157     \           (Try (Rewrite_Set_Inst [(bdv,v_)]               \

   158     \                                  rootrat_solve False))) e_ \

   159     \ in (SubProblem (RootEq_,[univariate,equation],            \

   160     \        [no_met]) [bool_ e_, real_ v_]))"

   161    ));

   162 calclist':= overwritel (!calclist',

   163    [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in",

   164 			      eval_is_rootRatAddTerm_in""))

   165     ]);(*("", ("", "")),*)

   166 "******* RootRatEq.ML end *******";

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 25 Aug 2010 16:20:07 +0200
branch	isac-update-Isa09-2
changeset 37947	22235e4dbe5f
parent 37935	src/Tools/isac/IsacKnowledge/RootRatEq.ML@27d365c3dd31
child 37952	9ddd1000b900
permissions	-rw-r--r--