wneuper/isa: src/Tools/isac/Knowledge/RatEq.thy@73dc85c025ab

     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 Equation begin

    12 text {* univariate equations over multivariate rational terms:

    13   In 2003 this type has been integrated into ISAC's equation solver

    14   by Richard Lang; the root for the solver is Equation.thy.

    15   The migration Isabelle2002 --> 2011 found that application of theorems like

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

    17   in rule-sets does not transfer "d ~= 0" to the assumptions; see

    18   test --- repair NO asms from rls RatEq_eliminate ---.

    19   Thus the migration dropped update of Check_elementwise, which would require

    20   these assumptions; see

    21   test --- pbl: rational, univariate, equation ---, --- x / (x ^ 2 - 6 * x + 9) - 1 /...

    22 *}

    24 consts

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

    28   (*----------------------scripts-----------------------*)

    29   Solve'_rat'_equation

    30              :: "[bool,real,

    31 		   bool list] => bool list"

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

    33                   (_))" 9)

    35 axiomatization where

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

    37    (*real_diff_minus

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

    39    real_rat_mult_1:   "a*(b/c) = (a*b)/c" and

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

    41    real_rat_mult_3:   "(a/b)*c = (a*c)/b" and

    42    real_rat_pow:      "(a/b)^^^2 = a^^^2/b^^^2" and

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

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

    46                                            ((a/b) / (c/d) = (a*d) / (b*c))" and

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

    49   (* equation to same denominator *)

    50   rat_mult_denominator_both:

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

    52   rat_mult_denominator_left:

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

    54   rat_mult_denominator_right:

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

    57 ML {*

    58 val thy = @{theory};

    60 (*-------------------------functions-----------------------*)

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

    62 fun is_rateqation_in t v =

    63     let

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

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

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

    67 	  | finddivide (t as (Const ("Fields.inverse_class.divide",_) $ _ $ b)) v = coeff_in b v

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

    69                                          orelse (finddivide t2 v)

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

    71 	  | finddivide _ _ = false;

    72      in

    73 	finddivide t v

    74     end;

    76 fun eval_is_ratequation_in _ _

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

    78     if is_rateqation_in t v then

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

    80 	      Trueprop $ (mk_equality (p, @{term True})))

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

    82 	       Trueprop $ (mk_equality (p, @{term False})))

    83   | eval_is_ratequation_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);

    85 (*-------------------------rulse-----------------------*)

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

    87   append_rls "RatEq_prls" e_rls

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

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

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

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

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

    93 	      Calc ("HOL.eq",eval_equal "#equal_"),

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

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

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

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

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

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

   100 	      ];

   103 (*rls = merge_rls erls Poly_erls *)

   104 val rateq_erls =

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

   106 	(merge_rls "is_ratequation_in" calculate_Rational

   107 		   (append_rls "is_ratequation_in"

   108 			Poly_erls

   109 			[(*Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),*)

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

   111 			       eval_is_ratequation_in "")

   113 			 ]))

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

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

   116 	 ];

   117 *}

   118 setup {* KEStore_Elems.add_rlss [("rateq_erls", (Context.theory_name @{theory}, rateq_erls))] *}

   119 ML {*

   121 val RatEq_crls =

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

   123 	(merge_rls "is_ratequation_in" calculate_Rational

   124 		   (append_rls "is_ratequation_in"

   125 			Poly_erls

   126 			[(*Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),*)

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

   128 			       eval_is_ratequation_in "")

   129 			 ]))

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

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

   132 	 ];

   134 val RatEq_eliminate = prep_rls(

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

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

   137        calc = [], errpatts = [],

   138        rules = [

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

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

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

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

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

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

   145 	    ],

   146     scr = Prog ((term_of o the o (parse thy)) "empty_script")

   147     }:rls);

   148 *}

   149 setup {* KEStore_Elems.add_rlss [("RatEq_eliminate",

   150   (Context.theory_name @{theory}, RatEq_eliminate))] *}

   151 ML {*

   153 val RatEq_simplify = prep_rls(

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

   155       erls = rateq_erls, srls = Erls, calc = [], errpatts = [],

   156     rules = [

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   173 	     ],

   174     scr = Prog ((term_of o the o (parse thy)) "empty_script")

   175     }:rls);

   176 *}

   177 setup {* KEStore_Elems.add_rlss [("RatEq_simplify",

   178   (Context.theory_name @{theory}, RatEq_simplify))] *}

   179 ML {*

   181 (*-------------------------Problem-----------------------*)

   182 (*

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

   184 show_ptyps();

   185 *)

   186 store_pbt

   187  (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID

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

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

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

   191    ("#Find"  ,["solutions v_v'i'"])

   192   ],

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

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

   196 *}

   197 setup {* KEStore_Elems.add_pbts

   198   [(prep_pbt thy "pbl_equ_univ_rat" [] e_pblID

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

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

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

   202         ("#Find", ["solutions v_v'i'"])],

   203       RatEq_prls, SOME "solve (e_e::bool, v_v)", [["RatEq","solve_rat_equation"]]))] *}

   205 ML {*

   206 (*-------------------------methods-----------------------*)

   207 store_met

   208  (prep_met thy "met_rateq" [] e_metID

   209  (["RatEq"],

   210    [],

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

   212     crls=RatEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"));

   213 *}

   215 ML {*

   216 store_met

   217  (prep_met thy "met_rat_eq" [] e_metID

   218  (["RatEq", "solve_rat_equation"],

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

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

   221    ("#Find"  ,["solutions v_v'i'"])

   222   ],

   223    {rew_ord'="termlessI",

   224     rls'=rateq_erls,

   225     srls=e_rls,

   226     prls=RatEq_prls,

   227     calc=[],

   228     crls=RatEq_crls, errpats = [], nrls = norm_Rational},

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

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

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

   232     "           (Repeat(Try (Rewrite_Set add_fractions_p False))) @@  " ^

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

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

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

   236     " in Check_elementwise L_L {(v_v::real). Assumptions})"

   237    ));

   238 *}

   240 setup {* KEStore_Elems.add_calcs

   241   [("is_ratequation_in", ("RatEq.is_ratequation_in", eval_is_ratequation_in ""))] *}

   243 end

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Mon, 27 Jan 2014 21:49:27 +0100
changeset 55359	73dc85c025ab
parent 55339	cccd24e959ba
child 55363	d78bc1342183
permissions	-rw-r--r--