1.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Mar 15 10:17:44 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Mar 15 12:42:04 2018 +0100
1.3 @@ -172,21 +172,21 @@
1.4 fun eval_contains_root (thmid:string) _
1.5 (t as (Const("Test.contains'_root",t0) $ arg)) thy =
1.6 if member op = (ids_of arg) "sqrt"
1.7 - then SOME (TermC.mk_thmid thmid (term_to_string''' thy arg)"",
1.8 + then SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg)"",
1.9 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.10 - else SOME (TermC.mk_thmid thmid (term_to_string''' thy arg)"",
1.11 + else SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg)"",
1.12 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.13 | eval_contains_root _ _ _ _ = NONE;
1.14
1.15 (*dummy precondition for root-met of x+1=2*)
1.16 fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy =
1.17 - SOME (TermC.mk_thmid thmid (term_to_string''' thy arg)"",
1.18 + SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg)"",
1.19 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.20 | eval_precond_rootmet _ _ _ _ = NONE;
1.21
1.22 (*dummy precondition for root-pbl of x+1=2*)
1.23 fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy =
1.24 - SOME (TermC.mk_thmid thmid (term_to_string''' thy arg) "",
1.25 + SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg) "",
1.26 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.27 | eval_precond_rootpbl _ _ _ _ = NONE;
1.28 *}
1.29 @@ -197,120 +197,120 @@
1.30 eval_precond_rootpbl"#Test.precond_rootpbl_"))] *}
1.31 ML {*
1.32 (** term order **)
1.33 -fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
1.34 +fun term_order (_: Celem.subst) tu = (term_ordI [] tu = LESS);
1.35
1.36 (** rule sets **)
1.37
1.38 val testerls =
1.39 - Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
1.40 - erls = e_rls, srls = Erls,
1.41 + Celem.Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
1.42 + erls = Celem.e_rls, srls = Celem.Erls,
1.43 calc = [], errpatts = [],
1.44 - rules = [Thm ("refl",TermC.num_str @{thm refl}),
1.45 - Thm ("order_refl",TermC.num_str @{thm order_refl}),
1.46 - Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
1.47 - Thm ("not_true",TermC.num_str @{thm not_true}),
1.48 - Thm ("not_false",TermC.num_str @{thm not_false}),
1.49 - Thm ("and_true",TermC.num_str @{thm and_true}),
1.50 - Thm ("and_false",TermC.num_str @{thm and_false}),
1.51 - Thm ("or_true",TermC.num_str @{thm or_true}),
1.52 - Thm ("or_false",TermC.num_str @{thm or_false}),
1.53 - Thm ("and_commute",TermC.num_str @{thm and_commute}),
1.54 - Thm ("or_commute",TermC.num_str @{thm or_commute}),
1.55 + rules = [Celem.Thm ("refl",TermC.num_str @{thm refl}),
1.56 + Celem.Thm ("order_refl",TermC.num_str @{thm order_refl}),
1.57 + Celem.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
1.58 + Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
1.59 + Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
1.60 + Celem.Thm ("and_true",TermC.num_str @{thm and_true}),
1.61 + Celem.Thm ("and_false",TermC.num_str @{thm and_false}),
1.62 + Celem.Thm ("or_true",TermC.num_str @{thm or_true}),
1.63 + Celem.Thm ("or_false",TermC.num_str @{thm or_false}),
1.64 + Celem.Thm ("and_commute",TermC.num_str @{thm and_commute}),
1.65 + Celem.Thm ("or_commute",TermC.num_str @{thm or_commute}),
1.66
1.67 - Calc ("Atools.is'_const",eval_const "#is_const_"),
1.68 - Calc ("Tools.matches",eval_matches ""),
1.69 + Celem.Calc ("Atools.is'_const",eval_const "#is_const_"),
1.70 + Celem.Calc ("Tools.matches",eval_matches ""),
1.71
1.72 - Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.73 - Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.74 - Calc ("Atools.pow" ,eval_binop "#power_"),
1.75 + Celem.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.76 + Celem.Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.77 + Celem.Calc ("Atools.pow" ,eval_binop "#power_"),
1.78
1.79 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.80 - Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
1.81 + Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.82 + Celem.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
1.83
1.84 - Calc ("Atools.ident",eval_ident "#ident_")],
1.85 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.86 - }:rls;
1.87 + Celem.Calc ("Atools.ident",eval_ident "#ident_")],
1.88 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.89 + };
1.90 *}
1.91 ML {*
1.92 (*.for evaluation of conditions in rewrite rules.*)
1.93 (*FIXXXXXXME 10.8.02: handle like _simplify*)
1.94 val tval_rls =
1.95 - Rls{id = "tval_rls", preconds = [],
1.96 + Celem.Rls{id = "tval_rls", preconds = [],
1.97 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
1.98 - erls=testerls,srls = e_rls,
1.99 + erls=testerls,srls = Celem.e_rls,
1.100 calc=[], errpatts = [],
1.101 - rules = [Thm ("refl",TermC.num_str @{thm refl}),
1.102 - Thm ("order_refl",TermC.num_str @{thm order_refl}),
1.103 - Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
1.104 - Thm ("not_true",TermC.num_str @{thm not_true}),
1.105 - Thm ("not_false",TermC.num_str @{thm not_false}),
1.106 - Thm ("and_true",TermC.num_str @{thm and_true}),
1.107 - Thm ("and_false",TermC.num_str @{thm and_false}),
1.108 - Thm ("or_true",TermC.num_str @{thm or_true}),
1.109 - Thm ("or_false",TermC.num_str @{thm or_false}),
1.110 - Thm ("and_commute",TermC.num_str @{thm and_commute}),
1.111 - Thm ("or_commute",TermC.num_str @{thm or_commute}),
1.112 + rules = [Celem.Thm ("refl",TermC.num_str @{thm refl}),
1.113 + Celem.Thm ("order_refl",TermC.num_str @{thm order_refl}),
1.114 + Celem.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
1.115 + Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
1.116 + Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
1.117 + Celem.Thm ("and_true",TermC.num_str @{thm and_true}),
1.118 + Celem.Thm ("and_false",TermC.num_str @{thm and_false}),
1.119 + Celem.Thm ("or_true",TermC.num_str @{thm or_true}),
1.120 + Celem.Thm ("or_false",TermC.num_str @{thm or_false}),
1.121 + Celem.Thm ("and_commute",TermC.num_str @{thm and_commute}),
1.122 + Celem.Thm ("or_commute",TermC.num_str @{thm or_commute}),
1.123
1.124 - Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
1.125 + Celem.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
1.126
1.127 - Thm ("root_ge0",TermC.num_str @{thm root_ge0}),
1.128 - Thm ("root_add_ge0",TermC.num_str @{thm root_add_ge0}),
1.129 - Thm ("root_ge0_1",TermC.num_str @{thm root_ge0_1}),
1.130 - Thm ("root_ge0_2",TermC.num_str @{thm root_ge0_2}),
1.131 + Celem.Thm ("root_ge0",TermC.num_str @{thm root_ge0}),
1.132 + Celem.Thm ("root_add_ge0",TermC.num_str @{thm root_add_ge0}),
1.133 + Celem.Thm ("root_ge0_1",TermC.num_str @{thm root_ge0_1}),
1.134 + Celem.Thm ("root_ge0_2",TermC.num_str @{thm root_ge0_2}),
1.135
1.136 - Calc ("Atools.is'_const",eval_const "#is_const_"),
1.137 - Calc ("Test.contains'_root",eval_contains_root "#eval_contains_root"),
1.138 - Calc ("Tools.matches",eval_matches ""),
1.139 - Calc ("Test.contains'_root",
1.140 + Celem.Calc ("Atools.is'_const",eval_const "#is_const_"),
1.141 + Celem.Calc ("Test.contains'_root",eval_contains_root "#eval_contains_root"),
1.142 + Celem.Calc ("Tools.matches",eval_matches ""),
1.143 + Celem.Calc ("Test.contains'_root",
1.144 eval_contains_root"#contains_root_"),
1.145
1.146 - Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.147 - Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.148 - Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
1.149 - Calc ("Atools.pow" ,eval_binop "#power_"),
1.150 + Celem.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.151 + Celem.Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.152 + Celem.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
1.153 + Celem.Calc ("Atools.pow" ,eval_binop "#power_"),
1.154
1.155 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.156 - Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
1.157 + Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.158 + Celem.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
1.159
1.160 - Calc ("Atools.ident",eval_ident "#ident_")],
1.161 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.162 - }:rls;
1.163 + Celem.Calc ("Atools.ident",eval_ident "#ident_")],
1.164 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.165 + };
1.166 *}
1.167 setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))] *}
1.168
1.169 ML {*
1.170 (*make () dissappear*)
1.171 val rearrange_assoc =
1.172 - Rls{id = "rearrange_assoc", preconds = [],
1.173 - rew_ord = ("e_rew_ord",e_rew_ord),
1.174 - erls = e_rls, srls = e_rls, calc = [], errpatts = [],
1.175 + Celem.Rls{id = "rearrange_assoc", preconds = [],
1.176 + rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
1.177 + erls = Celem.e_rls, srls = Celem.e_rls, calc = [], errpatts = [],
1.178 rules =
1.179 - [Thm ("sym_add_assoc",TermC.num_str (@{thm add.assoc} RS @{thm sym})),
1.180 - Thm ("sym_rmult_assoc",TermC.num_str (@{thm rmult_assoc} RS @{thm sym}))],
1.181 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.182 - }:rls;
1.183 + [Celem.Thm ("sym_add_assoc",TermC.num_str (@{thm add.assoc} RS @{thm sym})),
1.184 + Celem.Thm ("sym_rmult_assoc",TermC.num_str (@{thm rmult_assoc} RS @{thm sym}))],
1.185 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.186 + };
1.187
1.188 val ac_plus_times =
1.189 - Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
1.190 - erls = e_rls, srls = e_rls, calc = [], errpatts = [],
1.191 + Celem.Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
1.192 + erls = Celem.e_rls, srls = Celem.e_rls, calc = [], errpatts = [],
1.193 rules =
1.194 - [Thm ("radd_commute",TermC.num_str @{thm radd_commute}),
1.195 - Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}),
1.196 - Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
1.197 - Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),
1.198 - Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}),
1.199 - Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc})],
1.200 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.201 - }:rls;
1.202 + [Celem.Thm ("radd_commute",TermC.num_str @{thm radd_commute}),
1.203 + Celem.Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}),
1.204 + Celem.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
1.205 + Celem.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),
1.206 + Celem.Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}),
1.207 + Celem.Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc})],
1.208 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.209 + };
1.210
1.211 (*todo: replace by Rewrite("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add)*)
1.212 val norm_equation =
1.213 - Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.214 - erls = tval_rls, srls = e_rls, calc = [], errpatts = [],
1.215 - rules = [Thm ("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add})
1.216 + Celem.Rls{id = "norm_equation", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
1.217 + erls = tval_rls, srls = Celem.e_rls, calc = [], errpatts = [],
1.218 + rules = [Celem.Thm ("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add})
1.219 ],
1.220 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.221 - }:rls;
1.222 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.223 + };
1.224 *}
1.225 ML {*
1.226 (** rule sets **)
1.227 @@ -366,59 +366,59 @@
1.228 ML {*
1.229 (* expects * distributed over + *)
1.230 val Test_simplify =
1.231 - Rls{id = "Test_simplify", preconds = [],
1.232 + Celem.Rls{id = "Test_simplify", preconds = [],
1.233 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
1.234 - erls = tval_rls, srls = e_rls,
1.235 + erls = tval_rls, srls = Celem.e_rls,
1.236 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
1.237 rules = [
1.238 - Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
1.239 - Thm ("radd_mult_distrib2",TermC.num_str @{thm radd_mult_distrib2}),
1.240 - Thm ("rdistr_right_assoc",TermC.num_str @{thm rdistr_right_assoc}),
1.241 - Thm ("rdistr_right_assoc_p",TermC.num_str @{thm rdistr_right_assoc_p}),
1.242 - Thm ("rdistr_div_right",TermC.num_str @{thm rdistr_div_right}),
1.243 - Thm ("rbinom_power_2",TermC.num_str @{thm rbinom_power_2}),
1.244 + Celem.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
1.245 + Celem.Thm ("radd_mult_distrib2",TermC.num_str @{thm radd_mult_distrib2}),
1.246 + Celem.Thm ("rdistr_right_assoc",TermC.num_str @{thm rdistr_right_assoc}),
1.247 + Celem.Thm ("rdistr_right_assoc_p",TermC.num_str @{thm rdistr_right_assoc_p}),
1.248 + Celem.Thm ("rdistr_div_right",TermC.num_str @{thm rdistr_div_right}),
1.249 + Celem.Thm ("rbinom_power_2",TermC.num_str @{thm rbinom_power_2}),
1.250
1.251 - Thm ("radd_commute",TermC.num_str @{thm radd_commute}),
1.252 - Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}),
1.253 - Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
1.254 - Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),
1.255 - Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}),
1.256 - Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc}),
1.257 + Celem.Thm ("radd_commute",TermC.num_str @{thm radd_commute}),
1.258 + Celem.Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}),
1.259 + Celem.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
1.260 + Celem.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),
1.261 + Celem.Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}),
1.262 + Celem.Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc}),
1.263
1.264 - Thm ("radd_real_const_eq",TermC.num_str @{thm radd_real_const_eq}),
1.265 - Thm ("radd_real_const",TermC.num_str @{thm radd_real_const}),
1.266 + Celem.Thm ("radd_real_const_eq",TermC.num_str @{thm radd_real_const_eq}),
1.267 + Celem.Thm ("radd_real_const",TermC.num_str @{thm radd_real_const}),
1.268 (* these 2 rules are invers to distr_div_right wrt. termination.
1.269 thus they MUST be done IMMEDIATELY before calc *)
1.270 - Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.271 - Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.272 - Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.273 - Calc ("Atools.pow", eval_binop "#power_"),
1.274 + Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.275 + Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.276 + Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.277 + Celem.Calc ("Atools.pow", eval_binop "#power_"),
1.278
1.279 - Thm ("rcollect_right",TermC.num_str @{thm rcollect_right}),
1.280 - Thm ("rcollect_one_left",TermC.num_str @{thm rcollect_one_left}),
1.281 - Thm ("rcollect_one_left_assoc",TermC.num_str @{thm rcollect_one_left_assoc}),
1.282 - Thm ("rcollect_one_left_assoc_p",TermC.num_str @{thm rcollect_one_left_assoc_p}),
1.283 + Celem.Thm ("rcollect_right",TermC.num_str @{thm rcollect_right}),
1.284 + Celem.Thm ("rcollect_one_left",TermC.num_str @{thm rcollect_one_left}),
1.285 + Celem.Thm ("rcollect_one_left_assoc",TermC.num_str @{thm rcollect_one_left_assoc}),
1.286 + Celem.Thm ("rcollect_one_left_assoc_p",TermC.num_str @{thm rcollect_one_left_assoc_p}),
1.287
1.288 - Thm ("rshift_nominator",TermC.num_str @{thm rshift_nominator}),
1.289 - Thm ("rcancel_den",TermC.num_str @{thm rcancel_den}),
1.290 - Thm ("rroot_square_inv",TermC.num_str @{thm rroot_square_inv}),
1.291 - Thm ("rroot_times_root",TermC.num_str @{thm rroot_times_root}),
1.292 - Thm ("rroot_times_root_assoc_p",TermC.num_str @{thm rroot_times_root_assoc_p}),
1.293 - Thm ("rsqare",TermC.num_str @{thm rsqare}),
1.294 - Thm ("power_1",TermC.num_str @{thm power_1}),
1.295 - Thm ("rtwo_of_the_same",TermC.num_str @{thm rtwo_of_the_same}),
1.296 - Thm ("rtwo_of_the_same_assoc_p",TermC.num_str @{thm rtwo_of_the_same_assoc_p}),
1.297 + Celem.Thm ("rshift_nominator",TermC.num_str @{thm rshift_nominator}),
1.298 + Celem.Thm ("rcancel_den",TermC.num_str @{thm rcancel_den}),
1.299 + Celem.Thm ("rroot_square_inv",TermC.num_str @{thm rroot_square_inv}),
1.300 + Celem.Thm ("rroot_times_root",TermC.num_str @{thm rroot_times_root}),
1.301 + Celem.Thm ("rroot_times_root_assoc_p",TermC.num_str @{thm rroot_times_root_assoc_p}),
1.302 + Celem.Thm ("rsqare",TermC.num_str @{thm rsqare}),
1.303 + Celem.Thm ("power_1",TermC.num_str @{thm power_1}),
1.304 + Celem.Thm ("rtwo_of_the_same",TermC.num_str @{thm rtwo_of_the_same}),
1.305 + Celem.Thm ("rtwo_of_the_same_assoc_p",TermC.num_str @{thm rtwo_of_the_same_assoc_p}),
1.306
1.307 - Thm ("rmult_1",TermC.num_str @{thm rmult_1}),
1.308 - Thm ("rmult_1_right",TermC.num_str @{thm rmult_1_right}),
1.309 - Thm ("rmult_0",TermC.num_str @{thm rmult_0}),
1.310 - Thm ("rmult_0_right",TermC.num_str @{thm rmult_0_right}),
1.311 - Thm ("radd_0",TermC.num_str @{thm radd_0}),
1.312 - Thm ("radd_0_right",TermC.num_str @{thm radd_0_right})
1.313 + Celem.Thm ("rmult_1",TermC.num_str @{thm rmult_1}),
1.314 + Celem.Thm ("rmult_1_right",TermC.num_str @{thm rmult_1_right}),
1.315 + Celem.Thm ("rmult_0",TermC.num_str @{thm rmult_0}),
1.316 + Celem.Thm ("rmult_0_right",TermC.num_str @{thm rmult_0_right}),
1.317 + Celem.Thm ("radd_0",TermC.num_str @{thm radd_0}),
1.318 + Celem.Thm ("radd_0_right",TermC.num_str @{thm radd_0_right})
1.319 ],
1.320 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.321 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.322 (*since 040209 filled by prep_rls': STest_simplify*)
1.323 - }:rls;
1.324 + };
1.325 *}
1.326 ML {*
1.327
1.328 @@ -428,33 +428,33 @@
1.329
1.330 (*isolate the root in a root-equation*)
1.331 val isolate_root =
1.332 - Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.333 - erls=tval_rls,srls = e_rls, calc=[], errpatts = [],
1.334 - rules = [Thm ("rroot_to_lhs",TermC.num_str @{thm rroot_to_lhs}),
1.335 - Thm ("rroot_to_lhs_mult",TermC.num_str @{thm rroot_to_lhs_mult}),
1.336 - Thm ("rroot_to_lhs_add_mult",TermC.num_str @{thm rroot_to_lhs_add_mult}),
1.337 - Thm ("risolate_root_add",TermC.num_str @{thm risolate_root_add}),
1.338 - Thm ("risolate_root_mult",TermC.num_str @{thm risolate_root_mult}),
1.339 - Thm ("risolate_root_div",TermC.num_str @{thm risolate_root_div}) ],
1.340 - scr = Prog ((Thm.term_of o the o (TermC.parse thy))
1.341 + Celem.Rls{id = "isolate_root", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
1.342 + erls=tval_rls,srls = Celem.e_rls, calc=[], errpatts = [],
1.343 + rules = [Celem.Thm ("rroot_to_lhs",TermC.num_str @{thm rroot_to_lhs}),
1.344 + Celem.Thm ("rroot_to_lhs_mult",TermC.num_str @{thm rroot_to_lhs_mult}),
1.345 + Celem.Thm ("rroot_to_lhs_add_mult",TermC.num_str @{thm rroot_to_lhs_add_mult}),
1.346 + Celem.Thm ("risolate_root_add",TermC.num_str @{thm risolate_root_add}),
1.347 + Celem.Thm ("risolate_root_mult",TermC.num_str @{thm risolate_root_mult}),
1.348 + Celem.Thm ("risolate_root_div",TermC.num_str @{thm risolate_root_div}) ],
1.349 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy))
1.350 "empty_script")
1.351 - }:rls;
1.352 + };
1.353
1.354 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
1.355 val isolate_bdv =
1.356 - Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.357 - erls=tval_rls,srls = e_rls, calc= [], errpatts = [],
1.358 + Celem.Rls{id = "isolate_bdv", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
1.359 + erls=tval_rls,srls = Celem.e_rls, calc= [], errpatts = [],
1.360 rules =
1.361 - [Thm ("risolate_bdv_add",TermC.num_str @{thm risolate_bdv_add}),
1.362 - Thm ("risolate_bdv_mult_add",TermC.num_str @{thm risolate_bdv_mult_add}),
1.363 - Thm ("risolate_bdv_mult",TermC.num_str @{thm risolate_bdv_mult}),
1.364 - Thm ("mult_square",TermC.num_str @{thm mult_square}),
1.365 - Thm ("constant_square",TermC.num_str @{thm constant_square}),
1.366 - Thm ("constant_mult_square",TermC.num_str @{thm constant_mult_square})
1.367 + [Celem.Thm ("risolate_bdv_add",TermC.num_str @{thm risolate_bdv_add}),
1.368 + Celem.Thm ("risolate_bdv_mult_add",TermC.num_str @{thm risolate_bdv_mult_add}),
1.369 + Celem.Thm ("risolate_bdv_mult",TermC.num_str @{thm risolate_bdv_mult}),
1.370 + Celem.Thm ("mult_square",TermC.num_str @{thm mult_square}),
1.371 + Celem.Thm ("constant_square",TermC.num_str @{thm constant_square}),
1.372 + Celem.Thm ("constant_mult_square",TermC.num_str @{thm constant_mult_square})
1.373 ],
1.374 - scr = Prog ((Thm.term_of o the o (TermC.parse thy))
1.375 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy))
1.376 "empty_script")
1.377 - }:rls;
1.378 + };
1.379 *}
1.380 ML {*
1.381
1.382 @@ -489,24 +489,24 @@
1.383 ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)),
1.384 ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)),
1.385 ("matches", (Context.theory_name @{theory}, prep_rls'
1.386 - (append_rls "matches" testerls [Calc ("Tools.matches",eval_matches "#matches_")])))] *}
1.387 + (Celem.append_rls "matches" testerls [Celem.Calc ("Tools.matches",eval_matches "#matches_")])))] *}
1.388
1.389 (** problem types **)
1.390 setup {* KEStore_Elems.add_pbts
1.391 - [(Specify.prep_pbt thy "pbl_test" [] e_pblID (["test"], [], e_rls, NONE, [])),
1.392 - (Specify.prep_pbt thy "pbl_test_equ" [] e_pblID
1.393 + [(Specify.prep_pbt thy "pbl_test" [] Celem.e_pblID (["test"], [], Celem.e_rls, NONE, [])),
1.394 + (Specify.prep_pbt thy "pbl_test_equ" [] Celem.e_pblID
1.395 (["equation","test"],
1.396 [("#Given" ,["equality e_e","solveFor v_v"]),
1.397 ("#Where" ,["matches (?a = ?b) e_e"]),
1.398 ("#Find" ,["solutions v_v'i'"])],
1.399 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
1.400 - (Specify.prep_pbt thy "pbl_test_uni" [] e_pblID
1.401 + (Specify.prep_pbt thy "pbl_test_uni" [] Celem.e_pblID
1.402 (["univariate","equation","test"],
1.403 [("#Given" ,["equality e_e","solveFor v_v"]),
1.404 ("#Where" ,["matches (?a = ?b) e_e"]),
1.405 ("#Find" ,["solutions v_v'i'"])],
1.406 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
1.407 - (Specify.prep_pbt thy "pbl_test_uni_lin" [] e_pblID
1.408 + (Specify.prep_pbt thy "pbl_test_uni_lin" [] Celem.e_pblID
1.409 (["LINEAR","univariate","equation","test"],
1.410 [("#Given" ,["equality e_e","solveFor v_v"]),
1.411 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
1.412 @@ -530,16 +530,16 @@
1.413
1.414 (** methods **)
1.415 setup {* KEStore_Elems.add_mets
1.416 - [Specify.prep_met @{theory "Diff"} "met_test" [] e_metID
1.417 + [Specify.prep_met @{theory "Diff"} "met_test" [] Celem.e_metID
1.418 (["Test"], [],
1.419 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.420 - crls=Atools_erls, errpats = [], nrls = e_rls}, "empty_script"),
1.421 - Specify.prep_met thy "met_test_solvelin" [] e_metID
1.422 - (["Test","solve_linear"]:metID,
1.423 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
1.424 + crls=Atools_erls, errpats = [], nrls = Celem.e_rls}, "empty_script"),
1.425 + Specify.prep_met thy "met_test_solvelin" [] Celem.e_metID
1.426 + (["Test","solve_linear"],
1.427 [("#Given" ,["equality e_e","solveFor v_v"]),
1.428 ("#Where" ,["matches (?a = ?b) e_e"]),
1.429 ("#Find" ,["solutions v_v'i'"])],
1.430 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
1.431 + {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls,
1.432 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
1.433 nrls = Test_simplify},
1.434 "Script Solve_linear (e_e::bool) (v_v::real)= " ^
1.435 @@ -549,10 +549,10 @@
1.436 " (Rewrite_Set Test_simplify False))) e_e" ^
1.437 " in [e_e::bool])")(*,
1.438 Specify.prep_met thy (*test for equations*)
1.439 - (["Test","testeq"]:metID,
1.440 + (["Test","testeq"],
1.441 [("#Given" ,["boolTestGiven g_g"]),
1.442 ("#Find" ,["boolTestFind f_f"])],
1.443 - {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[], asm_thm=[("square_equation_left","")]},
1.444 + {rew_ord'="xxxe_rew_ordxxx",rls'="tval_rls",asm_rls=[], asm_thm=[("square_equation_left","")]},
1.445 "Script Testeq (e_q::bool) = " ^
1.446 "Repeat " ^
1.447 " (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q)); " ^
1.448 @@ -707,7 +707,7 @@
1.449 *}
1.450 (** problem types **)
1.451 setup {* KEStore_Elems.add_pbts
1.452 - [(Specify.prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
1.453 + [(Specify.prep_pbt thy "pbl_test_uni_plain2" [] Celem.e_pblID
1.454 (["plain_square","univariate","equation","test"],
1.455 [("#Given" ,["equality e_e","solveFor v_v"]),
1.456 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
1.457 @@ -740,71 +740,71 @@
1.458
1.459 *)
1.460 setup {* KEStore_Elems.add_pbts
1.461 - [(Specify.prep_pbt thy "pbl_test_uni_poly" [] e_pblID
1.462 + [(Specify.prep_pbt thy "pbl_test_uni_poly" [] Celem.e_pblID
1.463 (["polynomial","univariate","equation","test"],
1.464 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
1.465 ("#Where" ,["HOL.False"]),
1.466 ("#Find" ,["solutions v_v'i'"])],
1.467 - e_rls, SOME "solve (e_e::bool, v_v)", [])),
1.468 - (Specify.prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
1.469 + Celem.e_rls, SOME "solve (e_e::bool, v_v)", [])),
1.470 + (Specify.prep_pbt thy "pbl_test_uni_poly_deg2" [] Celem.e_pblID
1.471 (["degree_two","polynomial","univariate","equation","test"],
1.472 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
1.473 ("#Find" ,["solutions v_v'i'"])],
1.474 - e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
1.475 - (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
1.476 + Celem.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
1.477 + (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] Celem.e_pblID
1.478 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
1.479 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
1.480 ("#Find" ,["solutions v_v'i'"])],
1.481 - e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
1.482 - (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
1.483 + Celem.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
1.484 + (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] Celem.e_pblID
1.485 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
1.486 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
1.487 ("#Find" ,["solutions v_v'i'"])],
1.488 - e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])),
1.489 - (Specify.prep_pbt thy "pbl_test_uni_root" [] e_pblID
1.490 + Celem.e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])),
1.491 + (Specify.prep_pbt thy "pbl_test_uni_root" [] Celem.e_pblID
1.492 (["squareroot","univariate","equation","test"],
1.493 [("#Given" ,["equality e_e","solveFor v_v"]),
1.494 ("#Where" ,["precond_rootpbl v_v"]),
1.495 ("#Find" ,["solutions v_v'i'"])],
1.496 - append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
1.497 + Celem.append_rls "contains_root" Celem.e_rls [Celem.Calc ("Test.contains'_root",
1.498 eval_contains_root "#contains_root_")],
1.499 SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]])),
1.500 - (Specify.prep_pbt thy "pbl_test_uni_norm" [] e_pblID
1.501 + (Specify.prep_pbt thy "pbl_test_uni_norm" [] Celem.e_pblID
1.502 (["normalise","univariate","equation","test"],
1.503 [("#Given" ,["equality e_e","solveFor v_v"]),
1.504 ("#Where" ,[]),
1.505 ("#Find" ,["solutions v_v'i'"])],
1.506 - e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])),
1.507 - (Specify.prep_pbt thy "pbl_test_uni_roottest" [] e_pblID
1.508 + Celem.e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])),
1.509 + (Specify.prep_pbt thy "pbl_test_uni_roottest" [] Celem.e_pblID
1.510 (["sqroot-test","univariate","equation","test"],
1.511 [("#Given" ,["equality e_e","solveFor v_v"]),
1.512 ("#Where" ,["precond_rootpbl v_v"]),
1.513 ("#Find" ,["solutions v_v'i'"])],
1.514 - e_rls, SOME "solve (e_e::bool, v_v)", [])),
1.515 - (Specify.prep_pbt thy "pbl_test_intsimp" [] e_pblID
1.516 + Celem.e_rls, SOME "solve (e_e::bool, v_v)", [])),
1.517 + (Specify.prep_pbt thy "pbl_test_intsimp" [] Celem.e_pblID
1.518 (["inttype","test"],
1.519 [("#Given" ,["intTestGiven t_t"]),
1.520 ("#Where" ,[]),
1.521 ("#Find" ,["intTestFind s_s"])],
1.522 - e_rls, NONE, [["Test","intsimp"]]))] *}
1.523 + Celem.e_rls, NONE, [["Test","intsimp"]]))] *}
1.524 (*
1.525 show_ptyps();
1.526 get_pbt ["inttype","test"];
1.527 *)
1.528
1.529 setup {* KEStore_Elems.add_mets
1.530 - [Specify.prep_met thy "met_test_sqrt" [] e_metID
1.531 + [Specify.prep_met thy "met_test_sqrt" [] Celem.e_metID
1.532 (*root-equation, version for tests before 8.01.01*)
1.533 - (["Test","sqrt-equ-test"]:metID,
1.534 + (["Test","sqrt-equ-test"],
1.535 [("#Given" ,["equality e_e","solveFor v_v"]),
1.536 ("#Where" ,["contains_root (e_e::bool)"]),
1.537 ("#Find" ,["solutions v_v'i'"])],
1.538 - {rew_ord'="e_rew_ord",rls'=tval_rls,
1.539 - srls = append_rls "srls_contains_root" e_rls
1.540 - [Calc ("Test.contains'_root",eval_contains_root "")],
1.541 - prls = append_rls "prls_contains_root" e_rls
1.542 - [Calc ("Test.contains'_root",eval_contains_root "")],
1.543 - calc=[], crls=tval_rls, errpats = [], nrls = e_rls (*,asm_rls=[],
1.544 + {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
1.545 + srls = Celem.append_rls "srls_contains_root" Celem.e_rls
1.546 + [Celem.Calc ("Test.contains'_root",eval_contains_root "")],
1.547 + prls = Celem.append_rls "prls_contains_root" Celem.e_rls
1.548 + [Celem.Calc ("Test.contains'_root",eval_contains_root "")],
1.549 + calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls (*,asm_rls=[],
1.550 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
1.551 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.552 "(let e_e = " ^
1.553 @@ -820,15 +820,15 @@
1.554 " (Try (Rewrite_Set Test_simplify False)))" ^
1.555 " e_e" ^
1.556 " in [e_e::bool])"),
1.557 - Specify.prep_met thy "met_test_sqrt2" [] e_metID
1.558 + Specify.prep_met thy "met_test_sqrt2" [] Celem.e_metID
1.559 (*root-equation ... for test-*.sml until 8.01*)
1.560 - (["Test","squ-equ-test2"]:metID,
1.561 + (["Test","squ-equ-test2"],
1.562 [("#Given" ,["equality e_e","solveFor v_v"]),
1.563 ("#Find" ,["solutions v_v'i'"])],
1.564 - {rew_ord'="e_rew_ord",rls'=tval_rls,
1.565 - srls = append_rls "srls_contains_root" e_rls
1.566 - [Calc ("Test.contains'_root",eval_contains_root"")],
1.567 - prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
1.568 + {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
1.569 + srls = Celem.append_rls "srls_contains_root" Celem.e_rls
1.570 + [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
1.571 + prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,asm_rls=[],
1.572 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
1.573 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.574 "(let e_e = " ^
1.575 @@ -846,15 +846,15 @@
1.576 " (L_L::bool list) = Tac subproblem_equation_dummy; " ^
1.577 " L_L = Tac solve_equation_dummy " ^
1.578 " in Check_elementwise L_L {(v_v::real). Assumptions})"),
1.579 - Specify.prep_met thy "met_test_squ_sub" [] e_metID
1.580 + Specify.prep_met thy "met_test_squ_sub" [] Celem.e_metID
1.581 (*tests subproblem fixed linear*)
1.582 - (["Test","squ-equ-test-subpbl1"]:metID,
1.583 + (["Test","squ-equ-test-subpbl1"],
1.584 [("#Given" ,["equality e_e","solveFor v_v"]),
1.585 ("#Where" ,["precond_rootmet v_v"]),
1.586 ("#Find" ,["solutions v_v'i'"])],
1.587 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
1.588 - prls = append_rls "prls_met_test_squ_sub" e_rls
1.589 - [Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
1.590 + {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls,
1.591 + prls = Celem.append_rls "prls_met_test_squ_sub" Celem.e_rls
1.592 + [Celem.Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
1.593 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
1.594 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.595 " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
1.596 @@ -865,28 +865,28 @@
1.597 " [Test,solve_linear]) " ^
1.598 " [BOOL e_e, REAL v_v]) " ^
1.599 " in Check_elementwise L_L {(v_v::real). Assumptions}) "),
1.600 - Specify.prep_met thy "met_test_squ_sub2" [] e_metID
1.601 + Specify.prep_met thy "met_test_squ_sub2" [] Celem.e_metID
1.602 (*tests subproblem fixed degree 2*)
1.603 - (["Test","squ-equ-test-subpbl2"]:metID,
1.604 + (["Test","squ-equ-test-subpbl2"],
1.605 [("#Given" ,["equality e_e","solveFor v_v"]),
1.606 ("#Find" ,["solutions v_v'i'"])],
1.607 - {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], crls=tval_rls,
1.608 - errpats = [], nrls = e_rls (*, asm_rls=[],asm_thm=[("square_equation_left",""),
1.609 + {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,srls=Celem.e_rls,prls=Celem.e_rls,calc=[], crls=tval_rls,
1.610 + errpats = [], nrls = Celem.e_rls (*, asm_rls=[],asm_thm=[("square_equation_left",""),
1.611 ("square_equation_right","")]*)},
1.612 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.613 " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^
1.614 "(L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
1.615 " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_v])" ^
1.616 "in Check_elementwise L_L {(v_v::real). Assumptions})"),
1.617 - Specify.prep_met thy "met_test_squ_nonterm" [] e_metID
1.618 + Specify.prep_met thy "met_test_squ_nonterm" [] Celem.e_metID
1.619 (*root-equation: see foils..., but notTerminating*)
1.620 - (["Test","square_equation...notTerminating"]:metID,
1.621 + (["Test","square_equation...notTerminating"],
1.622 [("#Given" ,["equality e_e","solveFor v_v"]),
1.623 ("#Find" ,["solutions v_v'i'"])],
1.624 - {rew_ord'="e_rew_ord",rls'=tval_rls,
1.625 - srls = append_rls "srls_contains_root" e_rls
1.626 - [Calc ("Test.contains'_root",eval_contains_root"")],
1.627 - prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
1.628 + {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
1.629 + srls = Celem.append_rls "srls_contains_root" Celem.e_rls
1.630 + [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
1.631 + prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,asm_rls=[],
1.632 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
1.633 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.634 "(let e_e = " ^
1.635 @@ -903,15 +903,15 @@
1.636 " (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
1.637 " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
1.638 "in Check_elementwise L_L {(v_v::real). Assumptions})"),
1.639 - Specify.prep_met thy "met_test_eq1" [] e_metID
1.640 + Specify.prep_met thy "met_test_eq1" [] Celem.e_metID
1.641 (*root-equation1:*)
1.642 - (["Test","square_equation1"]:metID,
1.643 + (["Test","square_equation1"],
1.644 [("#Given" ,["equality e_e","solveFor v_v"]),
1.645 ("#Find" ,["solutions v_v'i'"])],
1.646 - {rew_ord'="e_rew_ord",rls'=tval_rls,
1.647 - srls = append_rls "srls_contains_root" e_rls
1.648 - [Calc ("Test.contains'_root",eval_contains_root"")], prls=e_rls, calc=[], crls=tval_rls,
1.649 - errpats = [], nrls = e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),
1.650 + {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
1.651 + srls = Celem.append_rls "srls_contains_root" Celem.e_rls
1.652 + [Celem.Calc ("Test.contains'_root",eval_contains_root"")], prls=Celem.e_rls, calc=[], crls=tval_rls,
1.653 + errpats = [], nrls = Celem.e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),
1.654 ("square_equation_right","")]*)},
1.655 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.656 "(let e_e = " ^
1.657 @@ -927,15 +927,15 @@
1.658 " (L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
1.659 " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
1.660 " in Check_elementwise L_L {(v_v::real). Assumptions})"),
1.661 - Specify.prep_met thy "met_test_squ2" [] e_metID
1.662 + Specify.prep_met thy "met_test_squ2" [] Celem.e_metID
1.663 (*root-equation2*)
1.664 - (["Test","square_equation2"]:metID,
1.665 + (["Test","square_equation2"],
1.666 [("#Given" ,["equality e_e","solveFor v_v"]),
1.667 ("#Find" ,["solutions v_v'i'"])],
1.668 - {rew_ord'="e_rew_ord",rls'=tval_rls,
1.669 - srls = append_rls "srls_contains_root" e_rls
1.670 - [Calc ("Test.contains'_root",eval_contains_root"")],
1.671 - prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
1.672 + {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
1.673 + srls = Celem.append_rls "srls_contains_root" Celem.e_rls
1.674 + [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
1.675 + prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,asm_rls=[],
1.676 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
1.677 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.678 "(let e_e = " ^
1.679 @@ -952,15 +952,15 @@
1.680 " (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
1.681 " [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
1.682 " in Check_elementwise L_L {(v_v::real). Assumptions})"),
1.683 - Specify.prep_met thy "met_test_squeq" [] e_metID
1.684 + Specify.prep_met thy "met_test_squeq" [] Celem.e_metID
1.685 (*root-equation*)
1.686 - (["Test","square_equation"]:metID,
1.687 + (["Test","square_equation"],
1.688 [("#Given" ,["equality e_e","solveFor v_v"]),
1.689 ("#Find" ,["solutions v_v'i'"])],
1.690 - {rew_ord'="e_rew_ord",rls'=tval_rls,
1.691 - srls = append_rls "srls_contains_root" e_rls
1.692 - [Calc ("Test.contains'_root",eval_contains_root"")],
1.693 - prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls = e_rls (*,asm_rls=[],
1.694 + {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
1.695 + srls = Celem.append_rls "srls_contains_root" Celem.e_rls
1.696 + [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
1.697 + prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls (*,asm_rls=[],
1.698 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
1.699 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.700 "(let e_e = " ^
1.701 @@ -977,17 +977,17 @@
1.702 " (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
1.703 " [no_met]) [BOOL e_e, REAL v_v])" ^
1.704 " in Check_elementwise L_L {(v_v::real). Assumptions})"),
1.705 - Specify.prep_met thy "met_test_eq_plain" [] e_metID
1.706 + Specify.prep_met thy "met_test_eq_plain" [] Celem.e_metID
1.707 (*solve_plain_square*)
1.708 - (["Test","solve_plain_square"]:metID,
1.709 + (["Test","solve_plain_square"],
1.710 [("#Given",["equality e_e","solveFor v_v"]),
1.711 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
1.712 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
1.713 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
1.714 "(matches ( v_v ^^^2 = 0) e_e)"]),
1.715 ("#Find" ,["solutions v_v'i'"])],
1.716 - {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
1.717 - prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = e_rls(*,
1.718 + {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,calc=[],srls=Celem.e_rls,
1.719 + prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,
1.720 asm_rls=[],asm_thm=[]*)},
1.721 "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
1.722 " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@ " ^
1.723 @@ -996,25 +996,25 @@
1.724 " (Rewrite square_equality True)) @@ " ^
1.725 " (Try (Rewrite_Set tval_rls False))) e_e " ^
1.726 " in ((Or_to_List e_e)::bool list))"),
1.727 - Specify.prep_met thy "met_test_norm_univ" [] e_metID
1.728 - (["Test","norm_univar_equation"]:metID,
1.729 + Specify.prep_met thy "met_test_norm_univ" [] Celem.e_metID
1.730 + (["Test","norm_univar_equation"],
1.731 [("#Given",["equality e_e","solveFor v_v"]),
1.732 ("#Where" ,[]),
1.733 ("#Find" ,["solutions v_v'i'"])],
1.734 - {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls, calc=[], crls=tval_rls,
1.735 - errpats = [], nrls = e_rls},
1.736 + {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,srls = Celem.e_rls,prls=Celem.e_rls, calc=[], crls=tval_rls,
1.737 + errpats = [], nrls = Celem.e_rls},
1.738 "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
1.739 " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
1.740 " (Try (Rewrite_Set Test_simplify False))) e_e " ^
1.741 " in (SubProblem (Test',[univariate,equation,test], " ^
1.742 " [no_met]) [BOOL e_e, REAL v_v]))"),
1.743 (*17.9.02 aus SqRoot.ML------------------------------^^^---*)
1.744 - Specify.prep_met thy "met_test_intsimp" [] e_metID
1.745 - (["Test","intsimp"]:metID,
1.746 + Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID
1.747 + (["Test","intsimp"],
1.748 [("#Given" ,["intTestGiven t_t"]),
1.749 ("#Where" ,[]),
1.750 ("#Find" ,["intTestFind s_s"])],
1.751 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls, prls = e_rls, calc = [],
1.752 + {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls, prls = Celem.e_rls, calc = [],
1.753 crls = tval_rls, errpats = [], nrls = Test_simplify},
1.754 "Script STest_simplify (t_t::int) = " ^
1.755 "(Repeat " ^
1.756 @@ -1061,10 +1061,10 @@
1.757 | term_ord' pr thy (t, u) =
1.758 (if pr then
1.759 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.760 - val _ = tracing ("t= f@ts= \"" ^ term2str f ^ "\" @ \"[" ^
1.761 - commas(map term2str ts) ^ "]\"")
1.762 - val _ = tracing ("u= g@us= \"" ^ term2str g ^"\" @ \"[" ^
1.763 - commas(map term2str us) ^"]\"")
1.764 + val _ = tracing ("t= f@ts= \"" ^ Celem.term2str f ^ "\" @ \"[" ^
1.765 + commas(map Celem.term2str ts) ^ "]\"")
1.766 + val _ = tracing ("u= g@us= \"" ^ Celem.term2str g ^"\" @ \"[" ^
1.767 + commas(map Celem.term2str us) ^"]\"")
1.768 val _ = tracing ("size_of_term(t,u)= (" ^
1.769 string_of_int (size_of_term' t) ^ ", " ^
1.770 string_of_int (size_of_term' u) ^ ")")
1.771 @@ -1084,17 +1084,17 @@
1.772 and hd_ord (f, g) = (* ~ term.ML *)
1.773 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
1.774 and terms_ord str pr (ts, us) =
1.775 - list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
1.776 + list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us);
1.777 in
1.778
1.779 -fun ord_make_polytest (pr:bool) thy (_:subst) tu =
1.780 +fun ord_make_polytest (pr:bool) thy (_: Celem.subst) tu =
1.781 (term_ord' pr thy(***) tu = LESS );
1.782
1.783 end;(*local*)
1.784 *}
1.785 ML {*
1.786
1.787 -rew_ord' := overwritel (!rew_ord',
1.788 +Celem.rew_ord' := overwritel (! Celem.rew_ord',
1.789 [("termlessI", termlessI),
1.790 ("ord_make_polytest", ord_make_polytest false thy)
1.791 ]);
1.792 @@ -1139,72 +1139,72 @@
1.793 -----------------------------------------------------*)
1.794
1.795 val make_polytest =
1.796 - Rls{id = "make_polytest", preconds = []:term list,
1.797 + Celem.Rls{id = "make_polytest", preconds = []:term list,
1.798 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
1.799 - erls = testerls, srls = Erls,
1.800 + erls = testerls, srls = Celem.Erls,
1.801 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.802 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.803 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.804 ], errpatts = [],
1.805 - rules = [Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
1.806 + rules = [Celem.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
1.807 (*"a - b = a + (-1) * b"*)
1.808 - Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
1.809 + Celem.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
1.810 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.811 - Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
1.812 + Celem.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
1.813 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.814 - Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),
1.815 + Celem.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),
1.816 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.817 - Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),
1.818 + Celem.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),
1.819 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.820 - Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1.821 + Celem.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1.822 (*"1 * z = z"*)
1.823 - Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1.824 + Celem.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1.825 (*"0 * z = 0"*)
1.826 - Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
1.827 + Celem.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
1.828 (*"0 + z = z"*)
1.829
1.830 (*AC-rewriting*)
1.831 - Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1.832 + Celem.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1.833 (* z * w = w * z *)
1.834 - Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.835 + Celem.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.836 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.837 - Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1.838 + Celem.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1.839 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.840 - Thm ("add_commute",TermC.num_str @{thm add.commute}),
1.841 + Celem.Thm ("add_commute",TermC.num_str @{thm add.commute}),
1.842 (*z + w = w + z*)
1.843 - Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1.844 + Celem.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1.845 (*x + (y + z) = y + (x + z)*)
1.846 - Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
1.847 + Celem.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
1.848 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.849
1.850 - Thm ("sym_realpow_twoI",
1.851 + Celem.Thm ("sym_realpow_twoI",
1.852 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
1.853 (*"r1 * r1 = r1 ^^^ 2"*)
1.854 - Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
1.855 + Celem.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
1.856 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.857 - Thm ("sym_real_mult_2",
1.858 + Celem.Thm ("sym_real_mult_2",
1.859 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
1.860 (*"z1 + z1 = 2 * z1"*)
1.861 - Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1.862 + Celem.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1.863 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.864
1.865 - Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1.866 + Celem.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1.867 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.868 - Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
1.869 + Celem.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
1.870 (*"[| l is_const; m is_const |] ==>
1.871 l * n + (m * n + k) = (l + m) * n + k"*)
1.872 - Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
1.873 + Celem.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
1.874 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.875 - Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
1.876 + Celem.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
1.877 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.878
1.879 - Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.880 - Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.881 - Calc ("Atools.pow", eval_binop "#power_")
1.882 + Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.883 + Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.884 + Celem.Calc ("Atools.pow", eval_binop "#power_")
1.885 ],
1.886 - scr = EmptyScr(*Prog ((Thm.term_of o the o (parse thy))
1.887 + scr = Celem.EmptyScr(*Celem.Prog ((Thm.term_of o the o (parse thy))
1.888 scr_make_polytest)*)
1.889 - }:rls;
1.890 + };
1.891 *}
1.892 ML {*
1.893 (*WN060510 this was done before 'fun prep_rls ...------------------------
1.894 @@ -1244,100 +1244,100 @@
1.895 --------------------------------------------------------------------------*)
1.896
1.897 val expand_binomtest =
1.898 - Rls{id = "expand_binomtest", preconds = [],
1.899 + Celem.Rls{id = "expand_binomtest", preconds = [],
1.900 rew_ord = ("termlessI",termlessI),
1.901 - erls = testerls, srls = Erls,
1.902 + erls = testerls, srls = Celem.Erls,
1.903 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.904 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.905 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.906 ], errpatts = [],
1.907 rules =
1.908 - [Thm ("real_plus_binom_pow2" ,TermC.num_str @{thm real_plus_binom_pow2}),
1.909 + [Celem.Thm ("real_plus_binom_pow2" ,TermC.num_str @{thm real_plus_binom_pow2}),
1.910 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1.911 - Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),
1.912 + Celem.Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),
1.913 (*"(a + b)*(a + b) = ...*)
1.914 - Thm ("real_minus_binom_pow2" ,TermC.num_str @{thm real_minus_binom_pow2}),
1.915 + Celem.Thm ("real_minus_binom_pow2" ,TermC.num_str @{thm real_minus_binom_pow2}),
1.916 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1.917 - Thm ("real_minus_binom_times",TermC.num_str @{thm real_minus_binom_times}),
1.918 + Celem.Thm ("real_minus_binom_times",TermC.num_str @{thm real_minus_binom_times}),
1.919 (*"(a - b)*(a - b) = ...*)
1.920 - Thm ("real_plus_minus_binom1",TermC.num_str @{thm real_plus_minus_binom1}),
1.921 + Celem.Thm ("real_plus_minus_binom1",TermC.num_str @{thm real_plus_minus_binom1}),
1.922 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1.923 - Thm ("real_plus_minus_binom2",TermC.num_str @{thm real_plus_minus_binom2}),
1.924 + Celem.Thm ("real_plus_minus_binom2",TermC.num_str @{thm real_plus_minus_binom2}),
1.925 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1.926 (*RL 020915*)
1.927 - Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}),
1.928 + Celem.Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}),
1.929 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1.930 - Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}),
1.931 + Celem.Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}),
1.932 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1.933 - Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}),
1.934 + Celem.Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}),
1.935 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
1.936 - Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}),
1.937 + Celem.Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}),
1.938 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
1.939 - Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}),
1.940 + Celem.Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}),
1.941 (*(a*b)^^^n = a^^^n * b^^^n*)
1.942 - Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
1.943 + Celem.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
1.944 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1.945 - Thm ("real_minus_binom_pow3",TermC.num_str @{thm real_minus_binom_pow3}),
1.946 + Celem.Thm ("real_minus_binom_pow3",TermC.num_str @{thm real_minus_binom_pow3}),
1.947 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1.948
1.949
1.950 - (* Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
1.951 + (* Celem.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
1.952 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.953 - Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
1.954 + Celem.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
1.955 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.956 - Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),
1.957 + Celem.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),
1.958 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.959 - Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),
1.960 + Celem.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),
1.961 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.962 *)
1.963
1.964 - Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1.965 + Celem.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1.966 (*"1 * z = z"*)
1.967 - Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1.968 + Celem.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1.969 (*"0 * z = 0"*)
1.970 - Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
1.971 + Celem.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
1.972 (*"0 + z = z"*)
1.973
1.974 - Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.975 - Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.976 - Calc ("Atools.pow", eval_binop "#power_"),
1.977 + Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.978 + Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.979 + Celem.Calc ("Atools.pow", eval_binop "#power_"),
1.980 (*
1.981 - Thm ("mult_commute",TermC.num_str @{thm mult_commute}),
1.982 + Celem.Thm ("mult_commute",TermC.num_str @{thm mult_commute}),
1.983 (*AC-rewriting*)
1.984 - Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.985 - Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1.986 - Thm ("add_commute",TermC.num_str @{thm add_commute}),
1.987 - Thm ("add_left_commute",TermC.num_str @{thm add_left_commute}),
1.988 - Thm ("add_assoc",TermC.num_str @{thm add_assoc}),
1.989 + Celem.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.990 + Celem.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1.991 + Celem.Thm ("add_commute",TermC.num_str @{thm add_commute}),
1.992 + Celem.Thm ("add_left_commute",TermC.num_str @{thm add_left_commute}),
1.993 + Celem.Thm ("add_assoc",TermC.num_str @{thm add_assoc}),
1.994 *)
1.995
1.996 - Thm ("sym_realpow_twoI",
1.997 + Celem.Thm ("sym_realpow_twoI",
1.998 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
1.999 (*"r1 * r1 = r1 ^^^ 2"*)
1.1000 - Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
1.1001 + Celem.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
1.1002 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.1003 - (*Thm ("sym_real_mult_2",
1.1004 + (*Celem.Thm ("sym_real_mult_2",
1.1005 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
1.1006 (*"z1 + z1 = 2 * z1"*)*)
1.1007 - Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1.1008 + Celem.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1.1009 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.1010
1.1011 - Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1.1012 + Celem.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1.1013 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1.1014 - Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
1.1015 + Celem.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
1.1016 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.1017 - Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
1.1018 + Celem.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
1.1019 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.1020 - Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
1.1021 + Celem.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
1.1022 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.1023
1.1024 - Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.1025 - Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.1026 - Calc ("Atools.pow", eval_binop "#power_")
1.1027 + Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.1028 + Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.1029 + Celem.Calc ("Atools.pow", eval_binop "#power_")
1.1030 ],
1.1031 - scr = EmptyScr
1.1032 + scr = Celem.EmptyScr
1.1033 (*Script ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
1.1034 - }:rls;
1.1035 + };
1.1036 *}
1.1037 setup {* KEStore_Elems.add_rlss
1.1038 [("make_polytest", (Context.theory_name @{theory}, prep_rls' make_polytest)),