wneuper/isa: src/Tools/isac/Knowledge/RatEq.ML@9ddd1000b900

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

     2 (* collecting all knowledge for RationalEquations

     3    created by: rlang

     4          date: 02.09

     5    changed by: rlang

     6    last change by: rlang

     7              date: 02.11.29

     8 *)

    10 (* use"Knowledge/RatEq.ML";

    11    use"RatEq.ML";

    12    remove_thy"RatEq";

    13    use_thy"Isac";

    15    use"ROOT.ML";

    16    cd"IsacKnowledge";

    17    *)

    18 "******* RatEq.ML begin *******";

    20 theory' := overwritel (!theory', [("RatEq.thy",RatEq.thy)]);

    22 (*-------------------------functions-----------------------*)

    23 (* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)

    24 fun is_rateqation_in t v =

    25     let

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

    27    	fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:")

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

    29 	  | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = coeff_in b v

    30 	  | finddivide (_ $ t1 $ t2) v = (finddivide t1 v)

    31                                          orelse (finddivide t2 v)

    32 	  | finddivide (_ $ t1) v = (finddivide t1 v)

    33 	  | finddivide _ _ = false;

    34      in

    35 	finddivide t v

    36     end;

    38 fun eval_is_ratequation_in _ _

    39        (p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _  =

    40     if is_rateqation_in t v then

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

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

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

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

    45   | eval_is_ratequation_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);

    47 (*-------------------------rulse-----------------------*)

    48 val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)

    49   append_rls "RatEq_prls" e_rls

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

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

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

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

    54 	      Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),

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

    56 	      Thm ("not_true",num_str not_true),

    57 	      Thm ("not_false",num_str not_false),

    58 	      Thm ("and_true",num_str and_true),

    59 	      Thm ("and_false",num_str and_false),

    60 	      Thm ("or_true",num_str or_true),

    61 	      Thm ("or_false",num_str or_false)

    62 	      ];

    65 (*rls = merge_rls erls Poly_erls *)

    66 val rateq_erls =

    67     remove_rls "rateq_erls"                                   (*WN: ein Hack*)

    68 	(merge_rls "is_ratequation_in" calculate_Rational

    69 		   (append_rls "is_ratequation_in"

    70 			Poly_erls

    71 			[(*Calc ("HOL.divide", eval_cancel "#divide_"),*)

    72 			 Calc ("RatEq.is'_ratequation'_in",

    73 			       eval_is_ratequation_in "")

    75 			 ]))

    76 	[Thm ("and_commute",num_str and_commute), (*WN: ein Hack*)

    77 	 Thm ("or_commute",num_str or_commute)    (*WN: ein Hack*)

    78 	 ];

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

    80 			[("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)

    81 			 ]);

    84 val RatEq_crls =

    85     remove_rls "RatEq_crls"                                   (*WN: ein Hack*)

    86 	(merge_rls "is_ratequation_in" calculate_Rational

    87 		   (append_rls "is_ratequation_in"

    88 			Poly_erls

    89 			[(*Calc ("HOL.divide", eval_cancel "#divide_"),*)

    90 			 Calc ("RatEq.is'_ratequation'_in",

    91 			       eval_is_ratequation_in "")

    92 			 ]))

    93 	[Thm ("and_commute",num_str and_commute), (*WN: ein Hack*)

    94 	 Thm ("or_commute",num_str or_commute)    (*WN: ein Hack*)

    95 	 ];

    97 val RatEq_eliminate = prep_rls(

    98   Rls {id = "RatEq_eliminate", preconds = [],

    99        rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Erls,

   100        calc = [],

   101        rules = [

   102 	    Thm("rat_mult_denominator_both",num_str rat_mult_denominator_both),

   103 	     (* a/b=c/d -> ad=cb *)

   104 	    Thm("rat_mult_denominator_left",num_str rat_mult_denominator_left),

   105 	     (* a  =c/d -> ad=c  *)

   106 	    Thm("rat_mult_denominator_right",num_str rat_mult_denominator_right)

   107 	     (* a/b=c   ->  a=cb *)

   108 	    ],

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

   110     }:rls);

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

   112 			[("RatEq_eliminate",RatEq_eliminate)

   113 			 ]);

   115 val RatEq_simplify = prep_rls(

   116   Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI),

   117       erls = rateq_erls, srls = Erls, calc = [],

   118     rules = [

   119 	     Thm("real_rat_mult_1",num_str real_rat_mult_1),

   120 	     (*a*(b/c) = (a*b)/c*)

   121 	     Thm("real_rat_mult_2",num_str real_rat_mult_2),

   122 	     (*(a/b)*(c/d) = (a*c)/(b*d)*)

   123              Thm("real_rat_mult_3",num_str real_rat_mult_3),

   124              (* (a/b)*c = (a*c)/b*)

   125 	     Thm("real_rat_pow",num_str real_rat_pow),

   126 	     (*(a/b)^^^2 = a^^^2/b^^^2*)

   127 	     Thm("real_diff_minus",num_str real_diff_minus),

   128 	     (* a - b = a + (-1) * b *)

   129              Thm("rat_double_rat_1",num_str rat_double_rat_1),

   130              (* (a / (c/d) = (a*d) / c) *)

   131              Thm("rat_double_rat_2",num_str rat_double_rat_2),

   132              (* ((a/b) / (c/d) = (a*d) / (b*c)) *)

   133              Thm("rat_double_rat_3",num_str rat_double_rat_3)

   134              (* ((a/b) / c = a / (b*c) ) *)

   135 	     ],

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

   137     }:rls);

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

   139 			[("RatEq_simplify",RatEq_simplify)

   140 			 ]);

   142 (*-------------------------Problem-----------------------*)

   143 (*

   144 (get_pbt ["rational","univariate","equation"]);

   145 show_ptyps();

   146 *)

   147 store_pbt

   148  (prep_pbt (theory "RatEq") "pbl_equ_univ_rat" [] e_pblID

   149  (["rational","univariate","equation"],

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

   151    ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),

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

   153   ],

   155   RatEq_prls, SOME "solve (e_::bool, v_)",

   156   [["RatEq","solve_rat_equation"]]));

   159 (*-------------------------methods-----------------------*)

   160 store_met

   161  (prep_met (theory "RatEq") "met_rateq" [] e_metID

   162  (["RatEq"],

   163    [],

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

   165     crls=RatEq_crls, nrls=norm_Rational

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

   167 store_met

   168  (prep_met (theory "RatEq") "met_rat_eq" [] e_metID

   169  (["RatEq","solve_rat_equation"],

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

   171    ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),

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

   173   ],

   174    {rew_ord'="termlessI",

   175     rls'=rateq_erls,

   176     srls=e_rls,

   177     prls=RatEq_prls,

   178     calc=[],

   179     crls=RatEq_crls, nrls=norm_Rational},

   180    "Script Solve_rat_equation  (e_::bool) (v_::real) =                   " ^

   181     "(let e_ = ((Repeat(Try (Rewrite_Set RatEq_simplify      True))) @@  " ^

   182     "           (Repeat(Try (Rewrite_Set norm_Rational      False))) @@  " ^

   183     "           (Repeat(Try (Rewrite_Set common_nominator_p False))) @@  " ^

   184     "           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_;" ^

   185     " (L_::bool list) =  (SubProblem (RatEq_,[univariate,equation],      " ^

   186     "                [no_met]) [bool_ e_, real_ v_])                     " ^

   187     " in Check_elementwise L_ {(v_::real). Assumptions})"

   188    ));

   190 calclist':= overwritel (!calclist',

   191    [("is_ratequation_in", ("RatEq.is_ratequation_in",

   192 			   eval_is_ratequation_in ""))

   193     ]);

   194 "******* RatEq.ML end *******";

author	Walther Neuper <neuper@ist.tugraz.at>
	Fri, 27 Aug 2010 10:28:44 +0200
branch	isac-update-Isa09-2
changeset 37952	9ddd1000b900
parent 37947	22235e4dbe5f
permissions	-rw-r--r--