Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/RatEq.ML
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 25 Aug 2010 16:20:07 +0200
branchisac-update-Isa09-2
changeset 37947 22235e4dbe5f
parent 37935 src/Tools/isac/IsacKnowledge/RatEq.ML@27d365c3dd31
child 37952 9ddd1000b900
permissions -rw-r--r--
renamed isac's directories and Build_Isac.thy

Scripts --> ProgLang
ME --> Interpret
IsacKnowledge --> Knowledge 
     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"Knowledge/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 = 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;

    37     

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

    39     if is_rateqation_in t v then 

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

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

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

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

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

    45 

    46 (*-------------------------rulse-----------------------*)

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

    48   append_rls "RatEq_prls" e_rls 

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

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

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

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

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

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

    55 	      Thm ("not_true",num_str not_true),

    56 	      Thm ("not_false",num_str not_false),

    57 	      Thm ("and_true",num_str and_true),

    58 	      Thm ("and_false",num_str and_false),

    59 	      Thm ("or_true",num_str or_true),

    60 	      Thm ("or_false",num_str or_false)

    61 	      ];

    62 

    63 

    64 (*rls = merge_rls erls Poly_erls *)

    65 val rateq_erls = 

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

    67 	(merge_rls "is_ratequation_in" calculate_Rational

    68 		   (append_rls "is_ratequation_in"

    69 			Poly_erls

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

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

    72 			       eval_is_ratequation_in "")

    73 

    74 			 ]))

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

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

    77 	 ];

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

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

    80 			 ]);

    81 

    82 

    83 val RatEq_crls = 

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

    85 	(merge_rls "is_ratequation_in" calculate_Rational

    86 		   (append_rls "is_ratequation_in"

    87 			Poly_erls

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

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

    90 			       eval_is_ratequation_in "")

    91 			 ]))

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

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

    94 	 ];

    95 

    96 val RatEq_eliminate = prep_rls(

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

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

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

   100                   ("rat_mult_denominator_right","")],*)

   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 			 ]);

   114 

   115 

   116 

   117 

   118 val RatEq_simplify = prep_rls(

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

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

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

   122                   ("rat_double_rat_3","")],*)

   123     rules = [

   124 	     Thm("real_rat_mult_1",num_str real_rat_mult_1),

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

   126 	     Thm("real_rat_mult_2",num_str real_rat_mult_2),

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

   128              Thm("real_rat_mult_3",num_str real_rat_mult_3),

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

   130 	     Thm("real_rat_pow",num_str real_rat_pow),

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

   132 	     Thm("real_diff_minus",num_str real_diff_minus),

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

   134              Thm("rat_double_rat_1",num_str rat_double_rat_1),

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

   136              Thm("rat_double_rat_2",num_str rat_double_rat_2), 

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

   138              Thm("rat_double_rat_3",num_str rat_double_rat_3) 

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

   140 	     ],

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

   142     }:rls);

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

   144 			[("RatEq_simplify",RatEq_simplify)

   145 			 ]);

   146 

   147 (*-------------------------Problem-----------------------*)

   148 (*

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

   150 show_ptyps(); 

   151 *)

   152 store_pbt

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

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

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

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

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

   158   ],

   159 

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

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

   162 

   163 

   164 (*-------------------------methods-----------------------*)

   165 store_met

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

   167  (["RatEq"],

   168    [],

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

   170     crls=RatEq_crls, nrls=norm_Rational

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

   172 store_met

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

   174  (["RatEq","solve_rat_equation"],

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

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

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

   178   ],

   179    {rew_ord'="termlessI",

   180     rls'=rateq_erls,

   181     srls=e_rls,

   182     prls=RatEq_prls,

   183     calc=[],

   184     crls=RatEq_crls, nrls=norm_Rational(*,

   185     asm_rls=[],

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

   187              ("rat_mult_denominator_both",""),("rat_mult_denominator_left",""),

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

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

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

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

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

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

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

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

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

   197    ));

   198 

   199 calclist':= overwritel (!calclist', 

   200    [("is_ratequation_in", ("RatEq.is_ratequation_in", 

   201 			   eval_is_ratequation_in ""))

   202     ]);

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