Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Pure/isac/IsacKnowledge/RatEq.ML
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 21 Jul 2010 13:53:39 +0200
branchisac-from-Isabelle2009-2
changeset 37871 875b6efa7ced
permissions -rw-r--r--
added isac-hook in Pure/thm and isac-code 
     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 *)

     9 

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

    11    use"RatEq.ML";

    12    remove_thy"RatEq";

    13    use_thy"Isac";

    14 

    15    use"ROOT.ML";

    16    cd"IsacKnowledge";

    17    *)

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

    19 

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

    21 

    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 = v mem (vars c);

    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) orelse (finddivide t2 v)

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

    32 	  | finddivide _ _ = false;

    33      in

    34 	finddivide t v

    35     end;

    36     

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

    38     if is_rateqation_in t v then 

    39 	Some ((term2str p) ^ " = True",

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

    41     else Some ((term2str p) ^ " = True",

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

    43   | eval_is_ratequation_in _ _ _ _ = ((*writeln"### nichts matcht";*) None);

    44 

    45 (*-------------------------rulse-----------------------*)

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

    47   append_rls "RatEq_prls" e_rls 

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

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

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

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

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

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

    54 	      Thm ("not_true",num_str not_true),

    55 	      Thm ("not_false",num_str not_false),

    56 	      Thm ("and_true",num_str and_true),

    57 	      Thm ("and_false",num_str and_false),

    58 	      Thm ("or_true",num_str or_true),

    59 	      Thm ("or_false",num_str or_false)

    60 	      ];

    61 

    62 

    63 (*rls = merge_rls erls Poly_erls *)

    64 val rateq_erls = 

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

    66 	(merge_rls "is_ratequation_in" calculate_Rational

    67 		   (append_rls "is_ratequation_in"

    68 			Poly_erls

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

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

    71 			       eval_is_ratequation_in "")

    72 

    73 			 ]))

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

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

    76 	 ];

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

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

    79 			 ]);

    80 

    81 

    82 val RatEq_crls = 

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

    84 	(merge_rls "is_ratequation_in" calculate_Rational

    85 		   (append_rls "is_ratequation_in"

    86 			Poly_erls

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

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

    89 			       eval_is_ratequation_in "")

    90 			 ]))

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

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

    93 	 ];

    94 

    95 val RatEq_eliminate = prep_rls(

    96   Rls {id = "RatEq_eliminate", preconds = [], rew_ord = ("termlessI",termlessI), 

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

    98        (*asm_thm = [("rat_mult_denominator_both",""),("rat_mult_denominator_left",""),

    99                   ("rat_mult_denominator_right","")],*)

   100     rules = [

   101 	     Thm("rat_mult_denominator_both",num_str rat_mult_denominator_both), 

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

   103 	     Thm("rat_mult_denominator_left",num_str rat_mult_denominator_left), 

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

   105 	     Thm("rat_mult_denominator_right",num_str rat_mult_denominator_right)

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

   107 	     ],

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

   109     }:rls);

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

   111 			[("RatEq_eliminate",RatEq_eliminate)

   112 			 ]);

   113 

   114 

   115 

   116 

   117 val RatEq_simplify = prep_rls(

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

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

   120        (*asm_thm = [("rat_double_rat_1",""),("rat_double_rat_2",""),

   121                   ("rat_double_rat_3","")],*)

   122     rules = [

   123 	     Thm("real_rat_mult_1",num_str real_rat_mult_1),

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

   125 	     Thm("real_rat_mult_2",num_str real_rat_mult_2),

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

   127              Thm("real_rat_mult_3",num_str real_rat_mult_3),

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

   129 	     Thm("real_rat_pow",num_str real_rat_pow),

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

   131 	     Thm("real_diff_minus",num_str real_diff_minus),

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

   133              Thm("rat_double_rat_1",num_str rat_double_rat_1),

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

   135              Thm("rat_double_rat_2",num_str rat_double_rat_2), 

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

   137              Thm("rat_double_rat_3",num_str rat_double_rat_3) 

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

   139 	     ],

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

   141     }:rls);

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

   143 			[("RatEq_simplify",RatEq_simplify)

   144 			 ]);

   145 

   146 (*-------------------------Problem-----------------------*)

   147 (*

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

   149 show_ptyps(); 

   150 *)

   151 store_pbt

   152  (prep_pbt RatEq.thy "pbl_equ_univ_rat" [] e_pblID

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

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

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

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

   157   ],

   158 

   159   RatEq_prls, Some "solve (e_::bool, v_)",

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

   161 

   162 

   163 (*-------------------------methods-----------------------*)

   164 store_met

   165  (prep_met RatEq.thy "met_rateq" [] e_metID

   166  (["RatEq"],

   167    [],

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

   169     crls=RatEq_crls, nrls=norm_Rational

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

   171 store_met

   172  (prep_met RatEq.thy "met_rat_eq" [] e_metID

   173  (["RatEq","solve_rat_equation"],

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

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

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

   177   ],

   178    {rew_ord'="termlessI",

   179     rls'=rateq_erls,

   180     srls=e_rls,

   181     prls=RatEq_prls,

   182     calc=[],

   183     crls=RatEq_crls, nrls=norm_Rational(*,

   184     asm_rls=[],

   185     asm_thm=[("rat_double_rat_1",""),("rat_double_rat_2",""),("rat_double_rat_3",""),

   186              ("rat_mult_denominator_both",""),("rat_mult_denominator_left",""),

   187              ("rat_mult_denominator_right","")]*)},

   188    "Script Solve_rat_equation  (e_::bool) (v_::real) =                   \

   189     \(let e_ = ((Repeat(Try (Rewrite_Set RatEq_simplify      True))) @@  \

   190     \           (Repeat(Try (Rewrite_Set norm_Rational      False))) @@  \

   191     \           (Repeat(Try (Rewrite_Set common_nominator_p False))) @@  \

   192     \           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_;\

   193     \ (L_::bool list) =  (SubProblem (RatEq_,[univariate,equation],      \

   194     \                [no_met]) [bool_ e_, real_ v_])                     \

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

   196    ));

   197 

   198 calclist':= overwritel (!calclist', 

   199    [("is_ratequation_in", ("RatEq.is_ratequation_in", 

   200 			   eval_is_ratequation_in ""))

   201     ]);

   202 "******* RatEq.ML end *******";
wneuper/isa