1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 05 18:09:56 2018 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Nov 21 12:32:54 2018 +0100
1.3 @@ -53,7 +53,7 @@
1.4 (*requires rew_ord for termination, eg. ord_simplify_Integral;
1.5 works for lists of any length, interestingly !?!*)
1.6
1.7 -ML {*
1.8 +ML \<open>
1.9 val thy = @{theory};
1.10
1.11 (** eval functions **)
1.12 @@ -82,12 +82,12 @@
1.13 else SOME ((Rule.term2str p) ^ " = False",
1.14 HOLogic.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 +\<close>
1.19 +setup \<open>KEStore_Elems.add_calcs
1.20 [("occur_exactly_in",
1.21 ("EqSystem.occur'_exactly'_in",
1.22 - eval_occur_exactly_in "#eval_occur_exactly_in_"))] *}
1.23 -ML {*
1.24 + eval_occur_exactly_in "#eval_occur_exactly_in_"))]\<close>
1.25 +ML \<open>
1.26 (** rewrite order 'ord_simplify_System' **)
1.27
1.28 (* order wrt. several linear (i.e. without exponents) variables "c","c_2",..
1.29 @@ -169,8 +169,8 @@
1.30 Rule.rew_ord' := overwritel (! Rule.rew_ord',
1.31 [("ord_simplify_System", ord_simplify_System false thy)
1.32 ]);
1.33 -*}
1.34 -ML {*
1.35 +\<close>
1.36 +ML \<open>
1.37 (** rulesets **)
1.38
1.39 (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*)
1.40 @@ -193,8 +193,8 @@
1.41 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.42 ],
1.43 scr = Rule.EmptyScr};
1.44 -*}
1.45 -ML {*
1.46 +\<close>
1.47 +ML \<open>
1.48 (*.adapted from 'norm_Rational' by
1.49 #1 using 'ord_simplify_System' in 'order_add_mult_System'
1.50 #2 NOT using common_nominator_p .*)
1.51 @@ -215,8 +215,8 @@
1.52 ],
1.53 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.54 };
1.55 -*}
1.56 -ML {*
1.57 +\<close>
1.58 +ML \<open>
1.59 (*.adapted from 'norm_Rational' by
1.60 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
1.61 val norm_System =
1.62 @@ -236,8 +236,8 @@
1.63 ],
1.64 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.65 };
1.66 -*}
1.67 -ML {*
1.68 +\<close>
1.69 +ML \<open>
1.70 (*.simplify an equational system BEFORE solving it such that parentheses are
1.71 ( ((u0*v0)*w0) + ( ((u1*v1)*w1) * c + ... +((u4*v4)*w4) * c_4 ) )
1.72 ATTENTION: works ONLY for bound variables c, c_1, c_2, c_3, c_4 :ATTENTION
1.73 @@ -266,8 +266,8 @@
1.74 Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.75 ],
1.76 scr = Rule.EmptyScr};
1.77 -*}
1.78 -ML {*
1.79 +\<close>
1.80 +ML \<open>
1.81 (*.simplify an equational system AFTER solving it;
1.82 This is a copy of 'make_ratpoly_in' with the differences
1.83 *1* ord_simplify_System instead of termlessI .*)
1.84 @@ -290,8 +290,8 @@
1.85 [Rule.Thm ("sym_add_assoc",
1.86 TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
1.87 *)
1.88 -*}
1.89 -ML {*
1.90 +\<close>
1.91 +ML \<open>
1.92 val isolate_bdvs =
1.93 Rule.Rls {id="isolate_bdvs", preconds = [],
1.94 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.95 @@ -306,8 +306,8 @@
1.96 Rule.Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}),
1.97 Rule.Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult})],
1.98 scr = Rule.EmptyScr};
1.99 -*}
1.100 -ML {*
1.101 +\<close>
1.102 +ML \<open>
1.103 val isolate_bdvs_4x4 =
1.104 Rule.Rls {id="isolate_bdvs_4x4", preconds = [],
1.105 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.106 @@ -329,8 +329,8 @@
1.107 Rule.Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult})
1.108 ], scr = Rule.EmptyScr};
1.109
1.110 -*}
1.111 -ML {*
1.112 +\<close>
1.113 +ML \<open>
1.114
1.115 (*.order the equations in a system such, that a triangular system (if any)
1.116 appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
1.117 @@ -367,8 +367,8 @@
1.118 "#eval_occur_exactly_in_")
1.119 ],
1.120 scr = Rule.EmptyScr};
1.121 -*}
1.122 -ML {*
1.123 +\<close>
1.124 +ML \<open>
1.125
1.126 (*WN060914 quickly created for 4x4;
1.127 more similarity to prls_triangular desirable*)
1.128 @@ -396,9 +396,9 @@
1.129 "#eval_occur_exactly_in_")
1.130 ],
1.131 scr = Rule.EmptyScr};
1.132 -*}
1.133 +\<close>
1.134
1.135 -setup {* KEStore_Elems.add_rlss
1.136 +setup \<open>KEStore_Elems.add_rlss
1.137 [("simplify_System_parenthesized",
1.138 (Context.theory_name @{theory}, prep_rls' simplify_System_parenthesized)),
1.139 ("simplify_System", (Context.theory_name @{theory}, prep_rls' simplify_System)),
1.140 @@ -408,10 +408,10 @@
1.141 ("order_add_mult_System", (Context.theory_name @{theory}, prep_rls' order_add_mult_System)),
1.142 ("norm_System_noadd_fractions",
1.143 (Context.theory_name @{theory}, prep_rls' norm_System_noadd_fractions)),
1.144 - ("norm_System", (Context.theory_name @{theory}, prep_rls' norm_System))] *}
1.145 + ("norm_System", (Context.theory_name @{theory}, prep_rls' norm_System))]\<close>
1.146
1.147 (** problems **)
1.148 -setup {* KEStore_Elems.add_pbts
1.149 +setup \<open>KEStore_Elems.add_pbts
1.150 [(Specify.prep_pbt thy "pbl_equsys" [] Celem.e_pblID
1.151 (["system"],
1.152 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.153 @@ -494,9 +494,9 @@
1.154 ("#Find" ,["solution ss'''"])],
1.155 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)],
1.156 SOME "solveSystem e_s v_s",
1.157 - [["EqSystem","normalise","4x4"]]))] *}
1.158 + [["EqSystem","normalise","4x4"]]))]\<close>
1.159
1.160 -ML {*
1.161 +ML \<open>
1.162 (*this is for NTH only*)
1.163 val srls = Rule.Rls {id="srls_normalise_4x4",
1.164 preconds = [],
1.165 @@ -512,10 +512,10 @@
1.166 Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.167 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})],
1.168 scr = Rule.EmptyScr};
1.169 -*}
1.170 +\<close>
1.171
1.172 (**methods**)
1.173 -setup {* KEStore_Elems.add_mets
1.174 +setup \<open>KEStore_Elems.add_mets
1.175 [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
1.176 (["EqSystem"], [],
1.177 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.178 @@ -654,6 +654,6 @@
1.179 " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
1.180 " norm_Rational False))) e_2 " ^
1.181 " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])")]
1.182 -*}
1.183 +\<close>
1.184
1.185 end
1.186 \ No newline at end of file