1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sun Feb 25 16:31:17 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri Mar 02 14:19:59 2018 +0100
1.3 @@ -76,11 +76,11 @@
1.4 fun eval_occur_exactly_in _ "EqSystem.occur'_exactly'_in"
1.5 (p as (Const ("EqSystem.occur'_exactly'_in",_)
1.6 $ vs $ all $ t)) _ =
1.7 - if occur_exactly_in (isalist2list vs) (isalist2list all) t
1.8 + if occur_exactly_in (TermC.isalist2list vs) (TermC.isalist2list all) t
1.9 then SOME ((term2str p) ^ " = True",
1.10 - Trueprop $ (mk_equality (p, @{term True})))
1.11 + TermC.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.12 else SOME ((term2str p) ^ " = False",
1.13 - Trueprop $ (mk_equality (p, @{term False})))
1.14 + TermC.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.15 | eval_occur_exactly_in _ _ _ _ = NONE;
1.16 *}
1.17 setup {* KEStore_Elems.add_calcs
1.18 @@ -118,7 +118,7 @@
1.19 fun size_of_term' (Free (ccc, _)) =
1.20 (case Symbol.explode ccc of (*WN0510 hack for the bound variables*)
1.21 "c"::[] => 1000
1.22 - | "c"::"_"::is => 1000 * ((str2int o implode) is)
1.23 + | "c"::"_"::is => 1000 * ((TermC.str2int o implode) is)
1.24 | _ => 1)
1.25 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1.26 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1.27 @@ -179,17 +179,17 @@
1.28 rew_ord = ("ord_simplify_System",
1.29 ord_simplify_System false @{theory "Integrate"}),
1.30 erls = e_rls,srls = Erls, calc = [], errpatts = [],
1.31 - rules = [Thm ("mult_commute",num_str @{thm mult.commute}),
1.32 + rules = [Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1.33 (* z * w = w * z *)
1.34 - Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
1.35 + Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.36 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.37 - Thm ("mult_assoc",num_str @{thm mult.assoc}),
1.38 + Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1.39 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.40 - Thm ("add_commute",num_str @{thm add.commute}),
1.41 + Thm ("add_commute",TermC.num_str @{thm add.commute}),
1.42 (*z + w = w + z*)
1.43 - Thm ("add_left_commute",num_str @{thm add.left_commute}),
1.44 + Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1.45 (*x + (y + z) = y + (x + z)*)
1.46 - Thm ("add_assoc",num_str @{thm add.assoc})
1.47 + Thm ("add_assoc",TermC.num_str @{thm add.assoc})
1.48 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.49 ],
1.50 scr = EmptyScr}:rls;
1.51 @@ -213,7 +213,7 @@
1.52 (*Rls_ add_fractions_p, #2*)
1.53 Rls_ cancel_p
1.54 ],
1.55 - scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
1.56 + scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.57 }:rls;
1.58 *}
1.59 ML {*
1.60 @@ -234,7 +234,7 @@
1.61 Rls_ add_fractions_p,
1.62 Rls_ cancel_p
1.63 ],
1.64 - scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
1.65 + scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.66 }:rls;
1.67 *}
1.68 ML {*
1.69 @@ -251,15 +251,15 @@
1.70 Seq {id = "simplify_System_parenthesized", preconds = []:term list,
1.71 rew_ord = ("dummy_ord", dummy_ord),
1.72 erls = Atools_erls, srls = Erls, calc = [], errpatts = [],
1.73 - rules = [Thm ("distrib_right",num_str @{thm distrib_right}),
1.74 + rules = [Thm ("distrib_right",TermC.num_str @{thm distrib_right}),
1.75 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.76 - Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}),
1.77 + Thm ("add_divide_distrib",TermC.num_str @{thm add_divide_distrib}),
1.78 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.79 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.80 Rls_ norm_Rational_noadd_fractions(**2**),
1.81 Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
1.82 Thm ("sym_mult_assoc",
1.83 - num_str (@{thm mult.assoc} RS @{thm sym}))
1.84 + TermC.num_str (@{thm mult.assoc} RS @{thm sym}))
1.85 (*Rls_ discard_parentheses *3**),
1.86 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.87 Rls_ separate_bdv2,
1.88 @@ -288,7 +288,7 @@
1.89 val simplify_System =
1.90 append_rls "simplify_System" simplify_System_parenthesized
1.91 [Thm ("sym_add_assoc",
1.92 - num_str (@{thm add.assoc} RS @{thm sym}))];
1.93 + TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
1.94 *)
1.95 *}
1.96 ML {*
1.97 @@ -302,9 +302,9 @@
1.98 ],
1.99 srls = Erls, calc = [], errpatts = [],
1.100 rules =
1.101 - [Thm ("commute_0_equality", num_str @{thm commute_0_equality}),
1.102 - Thm ("separate_bdvs_add", num_str @{thm separate_bdvs_add}),
1.103 - Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})],
1.104 + [Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.105 + Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}),
1.106 + Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult})],
1.107 scr = EmptyScr};
1.108 *}
1.109 ML {*
1.110 @@ -318,15 +318,15 @@
1.111 Calc ("Atools.ident",eval_ident "#ident_"),
1.112 Calc ("Atools.some'_occur'_in",
1.113 eval_some_occur_in "#some_occur_in_"),
1.114 - Thm ("not_true",num_str @{thm not_true}),
1.115 - Thm ("not_false",num_str @{thm not_false})
1.116 + Thm ("not_true",TermC.num_str @{thm not_true}),
1.117 + Thm ("not_false",TermC.num_str @{thm not_false})
1.118 ],
1.119 srls = Erls, calc = [], errpatts = [],
1.120 - rules = [Thm ("commute_0_equality", num_str @{thm commute_0_equality}),
1.121 - Thm ("separate_bdvs0", num_str @{thm separate_bdvs0}),
1.122 - Thm ("separate_bdvs_add1", num_str @{thm separate_bdvs_add1}),
1.123 - Thm ("separate_bdvs_add1", num_str @{thm separate_bdvs_add2}),
1.124 - Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})
1.125 + rules = [Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.126 + Thm ("separate_bdvs0", TermC.num_str @{thm separate_bdvs0}),
1.127 + Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add1}),
1.128 + Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add2}),
1.129 + Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult})
1.130 ], scr = EmptyScr};
1.131
1.132 *}
1.133 @@ -339,7 +339,7 @@
1.134 rew_ord = ("ord_simplify_System",
1.135 ord_simplify_System false thy),
1.136 erls = Erls, srls = Erls, calc = [], errpatts = [],
1.137 - rules = [Thm ("order_system_NxN", num_str @{thm order_system_NxN})
1.138 + rules = [Thm ("order_system_NxN", TermC.num_str @{thm order_system_NxN})
1.139 ],
1.140 scr = EmptyScr};
1.141
1.142 @@ -357,11 +357,11 @@
1.143 ],
1.144 scr = EmptyScr},
1.145 srls = Erls, calc = [], errpatts = [],
1.146 - rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.147 + rules = [Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.148 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.149 - Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.150 - Thm ("tl_Cons",num_str @{thm tl_Cons}),
1.151 - Thm ("tl_Nil",num_str @{thm tl_Nil}),
1.152 + Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.153 + Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.154 + Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.155 Calc ("EqSystem.occur'_exactly'_in",
1.156 eval_occur_exactly_in
1.157 "#eval_occur_exactly_in_")
1.158 @@ -386,11 +386,11 @@
1.159 ],
1.160 scr = EmptyScr},
1.161 srls = Erls, calc = [], errpatts = [],
1.162 - rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.163 + rules = [Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.164 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.165 - Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.166 - Thm ("tl_Cons",num_str @{thm tl_Cons}),
1.167 - Thm ("tl_Nil",num_str @{thm tl_Nil}),
1.168 + Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.169 + Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.170 + Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.171 Calc ("EqSystem.occur'_exactly'_in",
1.172 eval_occur_exactly_in
1.173 "#eval_occur_exactly_in_")
1.174 @@ -430,8 +430,8 @@
1.175 ("#Where" ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
1.176 ("#Find" ,["solution ss'''"])],
1.177 append_rls "prls_2x2_linear_system" e_rls
1.178 - [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
1.179 - Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
1.180 + [Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.181 + Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.182 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.183 Calc ("HOL.eq",eval_equal "#equal_")],
1.184 SOME "solveSystem e_s v_s", [])),
1.185 @@ -457,8 +457,8 @@
1.186 ("#Where" ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
1.187 ("#Find" ,["solution ss'''"])],
1.188 append_rls "prls_3x3_linear_system" e_rls
1.189 - [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
1.190 - Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
1.191 + [Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.192 + Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.193 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.194 Calc ("HOL.eq",eval_equal "#equal_")],
1.195 SOME "solveSystem e_s v_s", [])),
1.196 @@ -469,8 +469,8 @@
1.197 ("#Where" ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
1.198 ("#Find" ,["solution ss'''"])],
1.199 append_rls "prls_4x4_linear_system" e_rls
1.200 - [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
1.201 - Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
1.202 + [Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.203 + Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.204 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.205 Calc ("HOL.eq",eval_equal "#equal_")],
1.206 SOME "solveSystem e_s v_s", [])),
1.207 @@ -508,9 +508,9 @@
1.208 Calc("Groups.plus_class.plus", eval_binop "#add_")
1.209 ],
1.210 srls = Erls, calc = [], errpatts = [],
1.211 - rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.212 + rules = [Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.213 Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.214 - Thm ("NTH_NIL",num_str @{thm NTH_NIL})],
1.215 + Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})],
1.216 scr = EmptyScr};
1.217 *}
1.218
1.219 @@ -535,9 +535,9 @@
1.220 ("#Find" ,["solution ss'''"])],
1.221 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
1.222 srls = append_rls "srls_top_down_2x2" e_rls
1.223 - [Thm ("hd_thm",num_str @{thm hd_thm}),
1.224 - Thm ("tl_Cons",num_str @{thm tl_Cons}),
1.225 - Thm ("tl_Nil",num_str @{thm tl_Nil})],
1.226 + [Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.227 + Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.228 + Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.229 prls = prls_triangular, crls = Erls, errpats = [], nrls = Erls},
1.230 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.231 " (let e_1 = Take (hd e_s); " ^
1.232 @@ -583,9 +583,9 @@
1.233 ("#Find" ,["solution ss'''"])],
1.234 {rew_ord'="tless_true", rls' = Erls, calc = [],
1.235 srls = append_rls "srls_normalise_2x2" e_rls
1.236 - [Thm ("hd_thm",num_str @{thm hd_thm}),
1.237 - Thm ("tl_Cons",num_str @{thm tl_Cons}),
1.238 - Thm ("tl_Nil",num_str @{thm tl_Nil})],
1.239 + [Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.240 + Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.241 + Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.242 prls = Erls, crls = Erls, errpats = [], nrls = Erls},
1.243 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.244 " (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@ " ^
1.245 @@ -604,9 +604,9 @@
1.246 ("#Find" ,["solution ss'''"])],
1.247 {rew_ord'="tless_true", rls' = Erls, calc = [],
1.248 srls = append_rls "srls_normalise_4x4" srls
1.249 - [Thm ("hd_thm",num_str @{thm hd_thm}),
1.250 - Thm ("tl_Cons",num_str @{thm tl_Cons}),
1.251 - Thm ("tl_Nil",num_str @{thm tl_Nil})],
1.252 + [Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.253 + Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.254 + Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.255 prls = Erls, crls = Erls, errpats = [], nrls = Erls},
1.256 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.257 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^