1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 12 14:29:10 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 12 18:06:27 2021 +0200
1.3 @@ -173,17 +173,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",ThmC.numerals_to_Free @{thm mult.commute}),
1.8 + rules = [\<^rule_thm>\<open>mult.commute\<close>,
1.9 (* z * w = w * z *)
1.10 - Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
1.11 + \<^rule_thm>\<open>real_mult_left_commute\<close>,
1.12 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.13 - Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
1.14 + \<^rule_thm>\<open>mult.assoc\<close>,
1.15 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.16 - Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
1.17 + \<^rule_thm>\<open>add.commute\<close>,
1.18 (*z + w = w + z*)
1.19 - Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
1.20 + \<^rule_thm>\<open>add.left_commute\<close>,
1.21 (*x + (y + z) = y + (x + z)*)
1.22 - Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc})
1.23 + \<^rule_thm>\<open>add.assoc\<close>
1.24 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.25 ],
1.26 scr = Rule.Empty_Prog};
1.27 @@ -245,9 +245,9 @@
1.28 Rule_Set.Sequence {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",ThmC.numerals_to_Free @{thm distrib_right}),
1.32 + rules = [\<^rule_thm>\<open>distrib_right\<close>,
1.33 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.34 - Rule.Thm ("add_divide_distrib",ThmC.numerals_to_Free @{thm add_divide_distrib}),
1.35 + \<^rule_thm>\<open>add_divide_distrib\<close>,
1.36 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.37 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.38 Rule.Rls_ norm_Rational_noadd_fractions(**2**),
1.39 @@ -291,9 +291,9 @@
1.40 [(\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))],
1.41 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.42 rules =
1.43 - [Rule.Thm ("commute_0_equality", ThmC.numerals_to_Free @{thm commute_0_equality}),
1.44 - Rule.Thm ("separate_bdvs_add", ThmC.numerals_to_Free @{thm separate_bdvs_add}),
1.45 - Rule.Thm ("separate_bdvs_mult", ThmC.numerals_to_Free @{thm separate_bdvs_mult})],
1.46 + [\<^rule_thm>\<open>commute_0_equality\<close>,
1.47 + \<^rule_thm>\<open>separate_bdvs_add\<close>,
1.48 + \<^rule_thm>\<open>separate_bdvs_mult\<close>],
1.49 scr = Rule.Empty_Prog};
1.50 \<close>
1.51 ML \<open>
1.52 @@ -305,15 +305,15 @@
1.53 [\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.54 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.55 \<^rule_eval>\<open>Prog_Expr.some_occur_in\<close> (Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.56 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1.57 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
1.58 + \<^rule_thm>\<open>not_true\<close>,
1.59 + \<^rule_thm>\<open>not_false\<close>
1.60 ],
1.61 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.62 - rules = [Rule.Thm ("commute_0_equality", ThmC.numerals_to_Free @{thm commute_0_equality}),
1.63 - Rule.Thm ("separate_bdvs0", ThmC.numerals_to_Free @{thm separate_bdvs0}),
1.64 - Rule.Thm ("separate_bdvs_add1", ThmC.numerals_to_Free @{thm separate_bdvs_add1}),
1.65 - Rule.Thm ("separate_bdvs_add1", ThmC.numerals_to_Free @{thm separate_bdvs_add2}),
1.66 - Rule.Thm ("separate_bdvs_mult", ThmC.numerals_to_Free @{thm separate_bdvs_mult})
1.67 + rules = [\<^rule_thm>\<open>commute_0_equality\<close>,
1.68 + \<^rule_thm>\<open>separate_bdvs0\<close>,
1.69 + \<^rule_thm>\<open>separate_bdvs_add1\<close>,
1.70 + \<^rule_thm>\<open>separate_bdvs_add2\<close>,
1.71 + \<^rule_thm>\<open>separate_bdvs_mult\<close>
1.72 ], scr = Rule.Empty_Prog};
1.73
1.74 \<close>
1.75 @@ -326,7 +326,7 @@
1.76 rew_ord = ("ord_simplify_System",
1.77 ord_simplify_System false \<^theory>),
1.78 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.79 - rules = [Rule.Thm ("order_system_NxN", ThmC.numerals_to_Free @{thm order_system_NxN})
1.80 + rules = [\<^rule_thm>\<open>order_system_NxN\<close>
1.81 ],
1.82 scr = Rule.Empty_Prog};
1.83
1.84 @@ -344,11 +344,11 @@
1.85 ],
1.86 scr = Rule.Empty_Prog},
1.87 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.88 - rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.89 + rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
1.90 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.91 - Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.92 - Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.93 - Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
1.94 + \<^rule_thm>\<open>NTH_NIL\<close>,
1.95 + \<^rule_thm>\<open>tl_Cons\<close>,
1.96 + \<^rule_thm>\<open>tl_Nil\<close>,
1.97 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")
1.98 ],
1.99 scr = Rule.Empty_Prog};
1.100 @@ -371,11 +371,11 @@
1.101 ],
1.102 scr = Rule.Empty_Prog},
1.103 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.104 - rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.105 + rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
1.106 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.107 - Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.108 - Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.109 - Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
1.110 + \<^rule_thm>\<open>NTH_NIL\<close>,
1.111 + \<^rule_thm>\<open>tl_Cons\<close>,
1.112 + \<^rule_thm>\<open>tl_Nil\<close>,
1.113 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")
1.114 ],
1.115 scr = Rule.Empty_Prog};
1.116 @@ -413,8 +413,8 @@
1.117 ("#Where" ,["Length (e_s:: bool list) = 2", "Length v_s = 2"]),
1.118 ("#Find" ,["solution ss'''"])],
1.119 Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
1.120 - [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.121 - Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.122 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
1.123 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
1.124 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.125 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
1.126 SOME "solveSystem e_s v_s", [])),
1.127 @@ -440,8 +440,8 @@
1.128 ("#Where" ,["Length (e_s:: bool list) = 3", "Length v_s = 3"]),
1.129 ("#Find" ,["solution ss'''"])],
1.130 Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
1.131 - [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.132 - Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.133 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
1.134 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
1.135 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.136 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
1.137 SOME "solveSystem e_s v_s", [])),
1.138 @@ -452,8 +452,8 @@
1.139 ("#Where" ,["Length (e_s:: bool list) = 4", "Length v_s = 4"]),
1.140 ("#Find" ,["solution ss'''"])],
1.141 Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
1.142 - [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.143 - Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.144 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
1.145 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
1.146 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.147 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
1.148 SOME "solveSystem e_s v_s", [])),
1.149 @@ -491,9 +491,9 @@
1.150 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.151 ],
1.152 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.153 - rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.154 + rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
1.155 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.156 - Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL})],
1.157 + \<^rule_thm>\<open>NTH_NIL\<close>],
1.158 scr = Rule.Empty_Prog};
1.159 \<close>
1.160
1.161 @@ -541,9 +541,9 @@
1.162 ("#Find" ,["solution ss'''"])],
1.163 {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.164 srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
1.165 - [Rule.Thm ("hd_thm",ThmC.numerals_to_Free @{thm hd_thm}),
1.166 - Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.167 - Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil})],
1.168 + [\<^rule_thm>\<open>hd_thm\<close>,
1.169 + \<^rule_thm>\<open>tl_Cons\<close>,
1.170 + \<^rule_thm>\<open>tl_Nil\<close>],
1.171 prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.172 @{thm solve_system.simps})]
1.173 \<close>
1.174 @@ -576,9 +576,9 @@
1.175 ("#Find" ,["solution ss'''"])],
1.176 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.177 srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
1.178 - [Rule.Thm ("hd_thm",ThmC.numerals_to_Free @{thm hd_thm}),
1.179 - Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.180 - Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil})],
1.181 + [\<^rule_thm>\<open>hd_thm\<close>,
1.182 + \<^rule_thm>\<open>tl_Cons\<close>,
1.183 + \<^rule_thm>\<open>tl_Nil\<close>],
1.184 prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.185 @{thm solve_system2.simps})]
1.186 \<close>
1.187 @@ -608,9 +608,9 @@
1.188 ("#Find" ,["solution ss'''"])],
1.189 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.190 srls = Rule_Set.append_rules "srls_normalise_4x4" srls
1.191 - [Rule.Thm ("hd_thm",ThmC.numerals_to_Free @{thm hd_thm}),
1.192 - Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.193 - Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil})],
1.194 + [\<^rule_thm>\<open>hd_thm\<close>,
1.195 + \<^rule_thm>\<open>tl_Cons\<close>,
1.196 + \<^rule_thm>\<open>tl_Nil\<close>],
1.197 prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.198 (*STOPPED.WN06? met ["EqSystem", "normalise", "4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
1.199 @{thm solve_system3.simps})]