wneuper/isa: src/Tools/isac/Knowledge/RatEq.thy@78938fc8e022

     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 *)

    10 theory RatEq imports Rational begin

    12 consts

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

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

    17   Solve'_rat'_equation

    18              :: "[bool,real,

    19 		   bool list] => bool list"

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

    21                   (_))" 9)

    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

    28    "a*(b/c) = (a*b)/c"

    29    real_rat_mult_2

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

    31    real_rat_mult_3

    32    "(a/b)*c = (a*c)/b"

    33    real_rat_pow

    34    "(a/b)^^^2 = a^^^2/b^^^2"

    36    rat_double_rat_1

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

    38    rat_double_rat_2

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

    40    rat_double_rat_3

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

    43   (* equation to same denominator *)

    44   rat_mult_denominator_both

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

    46   rat_mult_denominator_left

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

    48   rat_mult_denominator_right

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

    51 ML {*

    52 (*-------------------------functions-----------------------*)

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

    54 fun is_rateqation_in t v =

    55     let

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

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

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

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

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

    61                                          orelse (finddivide t2 v)

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

    63 	  | finddivide _ _ = false;

    64      in

    65 	finddivide t v

    66     end;

    68 fun eval_is_ratequation_in _ _

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

    70     if is_rateqation_in t v then

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

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

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

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

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

    77 (*-------------------------rulse-----------------------*)

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

    79   append_rls "RatEq_prls" e_rls

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

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

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

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

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

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

    86 	      Thm ("not_true",num_str @{not_true),

    87 	      Thm ("not_false",num_str @{not_false),

    88 	      Thm ("and_true",num_str @{and_true),

    89 	      Thm ("and_false",num_str @{and_false),

    90 	      Thm ("or_true",num_str @{or_true),

    91 	      Thm ("or_false",num_str @{or_false)

    92 	      ];

    95 (*rls = merge_rls erls Poly_erls *)

    96 val rateq_erls =

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

    98 	(merge_rls "is_ratequation_in" calculate_Rational

    99 		   (append_rls "is_ratequation_in"

   100 			Poly_erls

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

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

   103 			       eval_is_ratequation_in "")

   105 			 ]))

   106 	[Thm ("and_commute",num_str @{and_commute), (*WN: ein Hack*)

   107 	 Thm ("or_commute",num_str @{or_commute)    (*WN: ein Hack*)

   108 	 ];

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

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

   111 			 ]);

   114 val RatEq_crls =

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

   116 	(merge_rls "is_ratequation_in" calculate_Rational

   117 		   (append_rls "is_ratequation_in"

   118 			Poly_erls

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

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

   121 			       eval_is_ratequation_in "")

   122 			 ]))

   123 	[Thm ("and_commute",num_str @{and_commute), (*WN: ein Hack*)

   124 	 Thm ("or_commute",num_str @{or_commute)    (*WN: ein Hack*)

   125 	 ];

   127 val RatEq_eliminate = prep_rls(

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

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

   130        calc = [],

   131        rules = [

   132 	    Thm("rat_mult_denominator_both",num_str @{rat_mult_denominator_both),

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

   134 	    Thm("rat_mult_denominator_left",num_str @{rat_mult_denominator_left),

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

   136 	    Thm("rat_mult_denominator_right",num_str @{rat_mult_denominator_right)

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

   138 	    ],

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

   140     }:rls);

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

   142 			[("RatEq_eliminate",RatEq_eliminate)

   143 			 ]);

   145 val RatEq_simplify = prep_rls(

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

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

   148     rules = [

   149 	     Thm("real_rat_mult_1",num_str @{real_rat_mult_1),

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

   151 	     Thm("real_rat_mult_2",num_str @{real_rat_mult_2),

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

   153              Thm("real_rat_mult_3",num_str @{real_rat_mult_3),

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

   155 	     Thm("real_rat_pow",num_str @{real_rat_pow),

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

   157 	     Thm("real_diff_minus",num_str @{real_diff_minus),

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

   159              Thm("rat_double_rat_1",num_str @{rat_double_rat_1),

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

   161              Thm("rat_double_rat_2",num_str @{rat_double_rat_2),

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

   163              Thm("rat_double_rat_3",num_str @{rat_double_rat_3)

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

   165 	     ],

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

   167     }:rls);

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

   169 			[("RatEq_simplify",RatEq_simplify)

   170 			 ]);

   172 (*-------------------------Problem-----------------------*)

   173 (*

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

   175 show_ptyps();

   176 *)

   177 store_pbt

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

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

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

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

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

   183   ],

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

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

   189 (*-------------------------methods-----------------------*)

   190 store_met

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

   192  (["RatEq"],

   193    [],

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

   195     crls=RatEq_crls, nrls=norm_Rational

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

   197 store_met

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

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

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

   201    ("#Where" ,["(e_::bool) is_ratequation_in (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_::bool) (v_::real) =                   " ^

   211     "(let 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_;" ^

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

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

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

   218    ));

   220 calclist':= overwritel (!calclist',

   221    [("is_ratequation_in", ("RatEq.is_ratequation_in",

   222 			   eval_is_ratequation_in ""))

   223     ]);

   224 *}

   226 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 31 Aug 2010 16:00:13 +0200
branch	isac-update-Isa09-2
changeset 37966	78938fc8e022
parent 37954	4022d670753c
child 37967	bd4f7a35e892
permissions	-rw-r--r--