1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Mon Apr 13 13:27:55 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Apr 13 15:31:23 2020 +0200
1.3 @@ -174,17 +174,17 @@
1.4 rew_ord = ("ord_simplify_System",
1.5 ord_simplify_System false @{theory "Integrate"}),
1.6 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
1.7 - rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1.8 + rules = [Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult.commute}),
1.9 (* z * w = w * z *)
1.10 - Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.11 + Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
1.12 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.13 - Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1.14 + Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
1.15 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.16 - Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),
1.17 + Rule.Thm ("add_commute",ThmC.numerals_to_Free @{thm add.commute}),
1.18 (*z + w = w + z*)
1.19 - Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1.20 + Rule.Thm ("add_left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
1.21 (*x + (y + z) = y + (x + z)*)
1.22 - Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc})
1.23 + Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc})
1.24 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.25 ],
1.26 scr = Rule.EmptyScr};
1.27 @@ -246,15 +246,15 @@
1.28 Rule_Set.Seqence {id = "simplify_System_parenthesized", preconds = []:term list,
1.29 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.30 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.31 - rules = [Rule.Thm ("distrib_right",TermC.num_str @{thm distrib_right}),
1.32 + rules = [Rule.Thm ("distrib_right",ThmC.numerals_to_Free @{thm distrib_right}),
1.33 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.34 - Rule.Thm ("add_divide_distrib",TermC.num_str @{thm add_divide_distrib}),
1.35 + Rule.Thm ("add_divide_distrib",ThmC.numerals_to_Free @{thm add_divide_distrib}),
1.36 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.37 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.38 Rule.Rls_ norm_Rational_noadd_fractions(**2**),
1.39 Rule.Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
1.40 Rule.Thm ("sym_mult_assoc",
1.41 - TermC.num_str (@{thm mult.assoc} RS @{thm sym}))
1.42 + ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym}))
1.43 (*Rule.Rls_ discard_parentheses *3**),
1.44 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.45 Rule.Rls_ separate_bdv2,
1.46 @@ -283,7 +283,7 @@
1.47 val simplify_System =
1.48 Rule_Set.append_rules "simplify_System" simplify_System_parenthesized
1.49 [Rule.Thm ("sym_add_assoc",
1.50 - TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
1.51 + ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))];
1.52 *)
1.53 \<close>
1.54 ML \<open>
1.55 @@ -297,9 +297,9 @@
1.56 ],
1.57 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.58 rules =
1.59 - [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.60 - Rule.Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}),
1.61 - Rule.Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult})],
1.62 + [Rule.Thm ("commute_0_equality", ThmC.numerals_to_Free @{thm commute_0_equality}),
1.63 + Rule.Thm ("separate_bdvs_add", ThmC.numerals_to_Free @{thm separate_bdvs_add}),
1.64 + Rule.Thm ("separate_bdvs_mult", ThmC.numerals_to_Free @{thm separate_bdvs_mult})],
1.65 scr = Rule.EmptyScr};
1.66 \<close>
1.67 ML \<open>
1.68 @@ -312,15 +312,15 @@
1.69 eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.70 Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.71 Rule.Num_Calc ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.72 - Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.73 - Rule.Thm ("not_false",TermC.num_str @{thm not_false})
1.74 + Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1.75 + Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
1.76 ],
1.77 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.78 - rules = [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.79 - Rule.Thm ("separate_bdvs0", TermC.num_str @{thm separate_bdvs0}),
1.80 - Rule.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add1}),
1.81 - Rule.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add2}),
1.82 - Rule.Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult})
1.83 + rules = [Rule.Thm ("commute_0_equality", ThmC.numerals_to_Free @{thm commute_0_equality}),
1.84 + Rule.Thm ("separate_bdvs0", ThmC.numerals_to_Free @{thm separate_bdvs0}),
1.85 + Rule.Thm ("separate_bdvs_add1", ThmC.numerals_to_Free @{thm separate_bdvs_add1}),
1.86 + Rule.Thm ("separate_bdvs_add1", ThmC.numerals_to_Free @{thm separate_bdvs_add2}),
1.87 + Rule.Thm ("separate_bdvs_mult", ThmC.numerals_to_Free @{thm separate_bdvs_mult})
1.88 ], scr = Rule.EmptyScr};
1.89
1.90 \<close>
1.91 @@ -333,7 +333,7 @@
1.92 rew_ord = ("ord_simplify_System",
1.93 ord_simplify_System false thy),
1.94 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.95 - rules = [Rule.Thm ("order_system_NxN", TermC.num_str @{thm order_system_NxN})
1.96 + rules = [Rule.Thm ("order_system_NxN", ThmC.numerals_to_Free @{thm order_system_NxN})
1.97 ],
1.98 scr = Rule.EmptyScr};
1.99
1.100 @@ -351,11 +351,11 @@
1.101 ],
1.102 scr = Rule.EmptyScr},
1.103 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.104 - rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.105 + rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.106 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.107 - Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.108 - Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.109 - Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.110 + Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.111 + Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.112 + Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
1.113 Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.114 eval_occur_exactly_in
1.115 "#eval_occur_exactly_in_")
1.116 @@ -380,11 +380,11 @@
1.117 ],
1.118 scr = Rule.EmptyScr},
1.119 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.120 - rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.121 + rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.122 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.123 - Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.124 - Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.125 - Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.126 + Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.127 + Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.128 + Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
1.129 Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.130 eval_occur_exactly_in
1.131 "#eval_occur_exactly_in_")
1.132 @@ -424,8 +424,8 @@
1.133 ("#Where" ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
1.134 ("#Find" ,["solution ss'''"])],
1.135 Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
1.136 - [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.137 - Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.138 + [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.139 + Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.140 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.141 Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.142 SOME "solveSystem e_s v_s", [])),
1.143 @@ -451,8 +451,8 @@
1.144 ("#Where" ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
1.145 ("#Find" ,["solution ss'''"])],
1.146 Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
1.147 - [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.148 - Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.149 + [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.150 + Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.151 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.152 Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.153 SOME "solveSystem e_s v_s", [])),
1.154 @@ -463,8 +463,8 @@
1.155 ("#Where" ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
1.156 ("#Find" ,["solution ss'''"])],
1.157 Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
1.158 - [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.159 - Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.160 + [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.161 + Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.162 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.163 Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.164 SOME "solveSystem e_s v_s", [])),
1.165 @@ -502,9 +502,9 @@
1.166 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")
1.167 ],
1.168 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.169 - rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.170 + rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.171 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.172 - Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})],
1.173 + Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL})],
1.174 scr = Rule.EmptyScr};
1.175 \<close>
1.176
1.177 @@ -551,9 +551,9 @@
1.178 ("#Find" ,["solution ss'''"])],
1.179 {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.180 srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
1.181 - [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.182 - Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.183 - Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.184 + [Rule.Thm ("hd_thm",ThmC.numerals_to_Free @{thm hd_thm}),
1.185 + Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.186 + Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil})],
1.187 prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.188 @{thm solve_system.simps})]
1.189 \<close>
1.190 @@ -586,9 +586,9 @@
1.191 ("#Find" ,["solution ss'''"])],
1.192 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.193 srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
1.194 - [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.195 - Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.196 - Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.197 + [Rule.Thm ("hd_thm",ThmC.numerals_to_Free @{thm hd_thm}),
1.198 + Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.199 + Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil})],
1.200 prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.201 @{thm solve_system2.simps})]
1.202 \<close>
1.203 @@ -618,9 +618,9 @@
1.204 ("#Find" ,["solution ss'''"])],
1.205 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.206 srls = Rule_Set.append_rules "srls_normalise_4x4" srls
1.207 - [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.208 - Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.209 - Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.210 + [Rule.Thm ("hd_thm",ThmC.numerals_to_Free @{thm hd_thm}),
1.211 + Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.212 + Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil})],
1.213 prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.214 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
1.215 @{thm solve_system3.simps})]