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.thy
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 08 Sep 2010 16:47:22 +0200
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37988 03e6d5db883e
child 38009 b49723351533
permissions -rw-r--r--
tuned src + test

find . -type f -exec sed -i s/nadd_divide_distrib/add_divide_distrib/g {} \;
find . -type f -exec sed -i s/"\.thy\""/"\""/g {} \;
find . -type f -exec sed -i s/" indexname_ord"/" Term_Ord.indexname_ord"/g {} \;
find . -type f -exec sed -i s/"(string_of_cterm o cterm_of(sign_of thy))"/"(Syntax.string_of_term (thy2ctxt thy))"/g {} \;
find . -type f -exec sed -i s/" L_"/" L_L"/g {} \;
find . -type f -exec sed -i s/" L_:"/" L_L:"/g {} \;
find . -type f -exec sed -i s/"e_;"/"e_e;"/g {} \;
find . -type f -exec sed -i s/"v_)"/"v_v)"/g {} \;
find . -type f -exec sed -i s/"v_:"/"v_v:"/g {} \; 
     1 (*.(c) by Richard Lang, 2003 .*)

     2 (* theory collecting all knowledge for RationalEquations

     3    created by: rlang 

     4          date: 02.08.12

     5    changed by: rlang

     6    last change by: rlang

     7              date: 02.11.28

     8 *)

     9 

    10 theory RatEq imports Rational begin

    11 

    12 consts

    13 

    14   is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")

    15 

    16   (*----------------------scripts-----------------------*)

    17   Solve'_rat'_equation

    18              :: "[bool,real, 

    19 		   bool list] => bool list"

    20                ("((Script Solve'_rat'_equation (_ _ =))// 

    21                   (_))" 9)

    22 

    23 axioms 

    24    (* FIXME also in Poly.thy def. --> FIXED*)

    25    (*real_diff_minus            

    26    "a - b = a + (-1) * b"*)

    27    real_rat_mult_1:   "a*(b/c) = (a*b)/c"

    28    real_rat_mult_2:   "(a/b)*(c/d) = (a*c)/(b*d)"

    29    real_rat_mult_3:   "(a/b)*c = (a*c)/b"

    30    real_rat_pow:      "(a/b)^^^2 = a^^^2/b^^^2"

    31 

    32    rat_double_rat_1:   "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)"

    33    rat_double_rat_2:   "[|Not(b=0);Not(c=0); Not(d=0)|] ==> 

    34                                            ((a/b) / (c/d) = (a*d) / (b*c))"

    35    rat_double_rat_3:   "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))"

    36 

    37   (* equation to same denominator *)

    38   rat_mult_denominator_both:

    39    "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)"

    40   rat_mult_denominator_left:

    41    "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"

    42   rat_mult_denominator_right:

    43    "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"

    44 

    45 ML {*

    46 val thy = @{theory};

    47 

    48 (*-------------------------functions-----------------------*)

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

    50 fun is_rateqation_in t v = 

    51     let 

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

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

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

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

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

    57                                          orelse (finddivide t2 v)

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

    59 	  | finddivide _ _ = false;

    60      in

    61 	finddivide t v

    62     end;

    63     

    64 fun eval_is_ratequation_in _ _ 

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

    66     if is_rateqation_in t v then 

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

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

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

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

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

    72 

    73 (*-------------------------rulse-----------------------*)

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

    75   append_rls "RatEq_prls" e_rls 

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

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

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

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

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

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

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

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

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

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

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

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

    88 	      ];

    89 

    90 

    91 (*rls = merge_rls erls Poly_erls *)

    92 val rateq_erls = 

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

    94 	(merge_rls "is_ratequation_in" calculate_Rational

    95 		   (append_rls "is_ratequation_in"

    96 			Poly_erls

    97 			[(*Calc ("HOL.divide", eval_cancel "#divide_e"),*)

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

    99 			       eval_is_ratequation_in "")

   100 

   101 			 ]))

   102 	[Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*)

   103 	 Thm ("or_commute",num_str @{thm or_commute})    (*WN: ein Hack*)

   104 	 ];

   105 ruleset' := overwritelthy @{theory} (!ruleset',

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

   107 			 ]);

   108 

   109 

   110 val RatEq_crls = 

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

   112 	(merge_rls "is_ratequation_in" calculate_Rational

   113 		   (append_rls "is_ratequation_in"

   114 			Poly_erls

   115 			[(*Calc ("HOL.divide", eval_cancel "#divide_e"),*)

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

   117 			       eval_is_ratequation_in "")

   118 			 ]))

   119 	[Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*)

   120 	 Thm ("or_commute",num_str @{thm or_commute})    (*WN: ein Hack*)

   121 	 ];

   122 

   123 val RatEq_eliminate = prep_rls(

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

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

   126        calc = [], 

   127        rules = [

   128 	    Thm("rat_mult_denominator_both",num_str @{thm rat_mult_denominator_both}), 

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

   130 	    Thm("rat_mult_denominator_left",num_str @{thm rat_mult_denominator_left}), 

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

   132 	    Thm("rat_mult_denominator_right",num_str @{thm rat_mult_denominator_right})

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

   134 	    ],

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

   136     }:rls);

   137 ruleset' := overwritelthy @{theory} (!ruleset',

   138 			[("RatEq_eliminate",RatEq_eliminate)

   139 			 ]);

   140 

   141 val RatEq_simplify = prep_rls(

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

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

   144     rules = [

   145 	     Thm("real_rat_mult_1",num_str @{thm real_rat_mult_1}),

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

   147 	     Thm("real_rat_mult_2",num_str @{thm real_rat_mult_2}),

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

   149              Thm("real_rat_mult_3",num_str @{thm real_rat_mult_3}),

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

   151 	     Thm("real_rat_pow",num_str @{thm real_rat_pow}),

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

   153 	     Thm("real_diff_minus",num_str @{thm real_diff_minus}),

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

   155              Thm("rat_double_rat_1",num_str @{thm rat_double_rat_1}),

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

   157              Thm("rat_double_rat_2",num_str @{thm rat_double_rat_2}), 

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

   159              Thm("rat_double_rat_3",num_str @{thm rat_double_rat_3}) 

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

   161 	     ],

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

   163     }:rls);

   164 ruleset' := overwritelthy @{theory} (!ruleset',

   165 			[("RatEq_simplify",RatEq_simplify)

   166 			 ]);

   167 

   168 (*-------------------------Problem-----------------------*)

   169 (*

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

   171 show_ptyps(); 

   172 *)

   173 store_pbt

   174  (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID

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

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

   177    ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),

   178    ("#Find"  ,["solutions v_i"]) 

   179   ],

   180 

   181   RatEq_prls, SOME "solve (e_e::bool, v_v)",

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

   183 *}

   184 

   185 ML {*

   186 (*-------------------------methods-----------------------*)

   187 store_met

   188  (prep_met thy "met_rateq" [] e_metID

   189  (["RatEq"],

   190    [],

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

   192     crls=RatEq_crls, nrls=norm_Rational

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

   194 *}

   195 

   196 ML {*

   197 store_met

   198  (prep_met thy "met_rat_eq" [] e_metID

   199  (["RatEq","solve_rat_equation"],

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

   201    ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),

   202    ("#Find"  ,["solutions v_i"])

   203   ],

   204    {rew_ord'="termlessI",

   205     rls'=rateq_erls,

   206     srls=e_rls,

   207     prls=RatEq_prls,

   208     calc=[],

   209     crls=RatEq_crls, nrls=norm_Rational},

   210    "Script Solve_rat_equation  (e_e::bool) (v_v::real) =                   " ^

   211     "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify      True))) @@  " ^

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

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

   214     "           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_e;" ^

   215     " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^

   216     "                    [BOOL e_e, REAL v_v])                     " ^

   217     " in Check_elementwise L_LL {(v_v::real). Assumptions})"

   218    ));

   219 *}

   220 

   221 ML {*

   222 calclist':= overwritel (!calclist', 

   223    [("is_ratequation_in", ("RatEq.is_ratequation_in", 

   224 			   eval_is_ratequation_in ""))

   225     ]);

   226 *}

   227 

   228 end
wneuper/isa