1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Aug 29 13:52:47 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Sep 03 12:40:27 2019 +0200
1.3 @@ -25,7 +25,7 @@
1.4 | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
1.5 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
1.6 | is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
1.7 - | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
1.8 + | is_ratpolyexp (Const ("Prog_Expr.pow",_) $ Free _ $ Free _) = true
1.9 | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ Free _ $ Free _) = true
1.10 | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1.11 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
1.12 @@ -33,7 +33,7 @@
1.13 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
1.14 | is_ratpolyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
1.15 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
1.16 - | is_ratpolyexp (Const ("Atools.pow",_) $ t1 $ t2) =
1.17 + | is_ratpolyexp (Const ("Prog_Expr.pow",_) $ t1 $ t2) =
1.18 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
1.19 | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ t1 $ t2) =
1.20 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
1.21 @@ -52,7 +52,7 @@
1.22 (*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
1.23 fun eval_get_denominator (thmid:string) _
1.24 (t as Const ("Rational.get_denominator", _) $
1.25 - (Const ("Rings.divide_class.divide", _) $ num $
1.26 + (Const ("Rings.divide_class.divide", _) $ _(*num*) $
1.27 denom)) thy =
1.28 SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy denom) "",
1.29 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
1.30 @@ -127,7 +127,7 @@
1.31 if TermC.is_num' id
1.32 then (id |> TermC.int_of_str_opt |> the |> curry op * c, es) (*several numerals in one monom*)
1.33 else (c, list_update es (find_index (curry op = t) vs) 1)
1.34 - | monom_of_term vs (c, es) (Const ("Atools.pow", _) $ (t as Free _) $ Free (e, _)) =
1.35 + | monom_of_term vs (c, es) (Const ("Prog_Expr.pow", _) $ (t as Free _) $ Free (e, _)) =
1.36 (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_of_str_opt e)))
1.37 | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
1.38 let val (c', es') = monom_of_term vs (c, es) m1
1.39 @@ -138,7 +138,7 @@
1.40 [monom_of_term vs (1, replicate (length vs) 0) t]
1.41 | monoms_of_term vs (t as Free _) =
1.42 [monom_of_term vs (1, replicate (length vs) 0) t]
1.43 - | monoms_of_term vs (t as Const ("Atools.pow", _) $ _ $ _) =
1.44 + | monoms_of_term vs (t as Const ("Prog_Expr.pow", _) $ _ $ _) =
1.45 [monom_of_term vs (1, replicate (length vs) 0) t]
1.46 | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $ _) =
1.47 [monom_of_term vs (1, replicate (length vs) 0) t]
1.48 @@ -179,7 +179,7 @@
1.49 | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
1.50 | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
1.51 | term_of_es baseT expT (v :: vs) (e :: es) =
1.52 - Const ("Atools.pow", [baseT, expT] ---> baseT) $ v $ (Free (TermC.isastr_of_int e, expT))
1.53 + Const ("Prog_Expr.pow", [baseT, expT] ---> baseT) $ v $ (Free (TermC.isastr_of_int e, expT))
1.54 :: term_of_es baseT expT vs es
1.55 | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
1.56
1.57 @@ -394,8 +394,8 @@
1.58 (Rule.Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
1.59 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
1.60 rules =
1.61 - [Rule.Calc ("HOL.eq", eval_equal "#equal_"),
1.62 - Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
1.63 + [Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.64 + Rule.Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
1.65 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.66 Rule.Thm ("not_false", TermC.num_str @{thm not_false})],
1.67 scr = Rule.EmptyScr});
1.68 @@ -409,7 +409,7 @@
1.69 erls = calc_rat_erls, srls = Rule.Erls,
1.70 calc = [], errpatts = [],
1.71 rules =
1.72 - [Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.73 + [Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.74
1.75 Rule.Thm ("minus_divide_left", TermC.num_str (@{thm minus_divide_left} RS @{thm sym})),
1.76 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
1.77 @@ -469,7 +469,7 @@
1.78
1.79 subsection \<open>Embed cancellation into rewriting\<close>
1.80 ML \<open>
1.81 -local (* cancel_p *)
1.82 +(**)local (* cancel_p *)
1.83
1.84 val {rules = rules, rew_ord = (_, ro), ...} = Rule.rep_rls (assoc_rls' @{theory} "rev_rew_p");
1.85
1.86 @@ -513,10 +513,10 @@
1.87 rew_ord=("ord_make_polynomial", ord_make_polynomial false thy),
1.88 erls = rational_erls,
1.89 calc =
1.90 - [("PLUS", ("Groups.plus_class.plus", eval_binop "#add_")),
1.91 - ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.92 - ("DIVIDE", ("Rings.divide_class.divide", eval_cancel "#divide_e")),
1.93 - ("POWER", ("Atools.pow", eval_binop "#power_"))],
1.94 + [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1.95 + ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
1.96 + ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
1.97 + ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))],
1.98 errpatts = [],
1.99 scr =
1.100 Rule.Rfuns {init_state = init_state thy Atools_erls ro,
1.101 @@ -529,7 +529,7 @@
1.102
1.103 subsection \<open>Embed addition into rewriting\<close>
1.104 ML \<open>
1.105 -local (* add_fractions_p *)
1.106 +(** )local ( * add_fractions_p *)
1.107
1.108 (*val {rules = rules, rew_ord = (_, ro), ...} = Rule.rep_rls (assoc_rls "make_polynomial");*)
1.109 val {rules, rew_ord=(_,ro),...} = Rule.rep_rls (assoc_rls' @{theory} "rev_rew_p");
1.110 @@ -546,6 +546,7 @@
1.111 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
1.112 in (t, t'', [rs(*here only _ONE_*)], der) end;
1.113
1.114 +\<close> ML \<open>
1.115 fun locate_rule thy eval_rls ro [rs] t r =
1.116 if member op = ((map (Celem.id_of_thm)) rs) (Celem.id_of_thm r)
1.117 then
1.118 @@ -574,23 +575,23 @@
1.119 val prepat = [([@{term True}], pat0),
1.120 ([@{term True}], pat1),
1.121 ([@{term True}], pat2)];
1.122 -in
1.123 +(** )in( **)
1.124
1.125 val add_fractions_p =
1.126 Rule.Rrls {id = "add_fractions_p", prepat=prepat,
1.127 rew_ord = ("ord_make_polynomial", ord_make_polynomial false thy),
1.128 erls = rational_erls,
1.129 - calc = [("PLUS", ("Groups.plus_class.plus", eval_binop "#add_")),
1.130 - ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")),
1.131 - ("DIVIDE", ("Rings.divide_class.divide", eval_cancel "#divide_e")),
1.132 - ("POWER", ("Atools.pow", eval_binop "#power_"))],
1.133 + calc = [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1.134 + ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
1.135 + ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
1.136 + ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))],
1.137 errpatts = [],
1.138 scr = Rule.Rfuns {init_state = init_state thy Atools_erls ro,
1.139 normal_form = add_fraction_p_ thy,
1.140 locate_rule = locate_rule thy Atools_erls ro,
1.141 next_rule = next_rule thy Atools_erls ro,
1.142 attach_form = attach_form}}
1.143 -end; (*local add_fractions_p *)
1.144 +(** )end; ( *local add_fractions_p *)
1.145 \<close>
1.146
1.147 subsection \<open>Cancelling and adding all occurrences in a term /////////////////////////////\<close>
1.148 @@ -604,12 +605,12 @@
1.149 val powers_erls = prep_rls'(
1.150 Rule.Rls {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
1.151 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
1.152 - rules = [Rule.Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
1.153 - Rule.Calc ("Atools.is'_even",eval_is_even "#is_even_"),
1.154 - Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.155 + rules = [Rule.Calc ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"),
1.156 + Rule.Calc ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_"),
1.157 + Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.158 Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
1.159 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.160 - Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_")
1.161 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.162 ],
1.163 scr = Rule.EmptyScr
1.164 });
1.165 @@ -642,7 +643,7 @@
1.166 (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)
1.167 Rule.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI}),
1.168 (*"1 ^^^ n = 1"*)
1.169 - Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_")
1.170 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.171 ],
1.172 scr = Rule.EmptyScr
1.173 });
1.174 @@ -666,7 +667,7 @@
1.175 Rule.Thm ("divide_divide_eq_left",
1.176 TermC.num_str @{thm divide_divide_eq_left}),
1.177 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.178 - Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.179 + Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.180 ],
1.181 scr = Rule.EmptyScr
1.182 });
1.183 @@ -706,7 +707,7 @@
1.184 val norm_rat_erls = prep_rls'(
1.185 Rule.Rls {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
1.186 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
1.187 - rules = [Rule.Calc ("Atools.is'_const",eval_const "#is_const_")
1.188 + rules = [Rule.Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")
1.189 ], scr = Rule.EmptyScr});
1.190
1.191 (* consists of rls containing the absolute minimum of thms *)
1.192 @@ -808,7 +809,7 @@
1.193 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.194 Rule.Thm ("divide_divide_eq_left", TermC.num_str @{thm divide_divide_eq_left}),
1.195 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.196 - Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.197 + Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.198
1.199 Rule.Thm ("rat_power", TermC.num_str @{thm rat_power})
1.200 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)