1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Thu Jul 28 11:43:27 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Sat Jul 30 16:47:45 2022 +0200
1.3 @@ -3,7 +3,6 @@
1.4 (c) due to copyright terms
1.5 *)
1.6
1.7 -Rewrite.trace_on := false; (*true false*)
1.8 "-----------------------------------------------------------------";
1.9 "table of contents -----------------------------------------------";
1.10 "-----------------------------------------------------------------";
1.11 @@ -90,7 +89,7 @@
1.12 Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_"),
1.13 Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")
1.14 ];
1.15 -val SOME (t',_) = rewrite_set_ thy false testrls t;
1.16 +val SOME (t',_) = rewrite_set_ ctxt false testrls t;
1.17 if UnparseC.term t' = "True" then ()
1.18 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
1.19
1.20 @@ -108,7 +107,7 @@
1.21 assume flawed test setup hidden by "handle _ => ..."
1.22 ERROR rewrite__set_ called with 'Erls' for '1 < 1'
1.23 val SOME (t,_) =
1.24 - rewrite_set_ thy true
1.25 + rewrite_set_ ctxt true
1.26 (Rule_Set.append_rules "prls_" Rule_Set.empty
1.27 [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.28 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.29 @@ -159,20 +158,20 @@
1.30 \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
1.31 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
1.32 (TermC.str2term"bdv_2",TermC.str2term"c_2")];
1.33 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
1.34 +val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.35 if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
1.36 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
1.37
1.38 -val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
1.39 +val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
1.40 if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
1.41 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
1.42
1.43 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
1.44 +val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
1.45 if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
1.46 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
1.47
1.48 "--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
1.49 -val SOME (t,_) = rewrite_set_ thy true order_system t;
1.50 +val SOME (t,_) = rewrite_set_ ctxt true order_system t;
1.51 if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
1.52 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
1.53
1.54 @@ -180,36 +179,37 @@
1.55 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
1.56 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
1.57 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
1.58 +val ctxt = Proof_Context.init_global thy;
1.59 val t =
1.60 TermC.str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
1.61 \ - 1 * q_0 / 24 * 0 \<up> 4),\
1.62 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
1.63 \ - 1 * q_0 / 24 * L \<up> 4)]";
1.64 -val SOME (t, _) = rewrite_set_ thy true norm_Rational t;
1.65 +val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;
1.66 if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
1.67 "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
1.68 "[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"
1.69 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
1.70
1.71 -val SOME(t, _)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
1.72 +val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.73 if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
1.74 "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
1.75 "[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"
1.76 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
1.77
1.78 -val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
1.79 +val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
1.80 if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
1.81 "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
1.82 "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"
1.83 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
1.84
1.85 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
1.86 +val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
1.87 if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
1.88 "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
1.89 "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
1.90 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
1.91
1.92 -val xxx = rewrite_set_ thy true order_system t;
1.93 +val xxx = rewrite_set_ ctxt true order_system t;
1.94 if is_none xxx
1.95 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
1.96
1.97 @@ -221,21 +221,21 @@
1.98 val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
1.99 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
1.100 (TermC.str2term"bdv_2",TermC.str2term"c_2")];
1.101 -val SOME (e2__,_) = rewrite_terms_ thy dummy_ord Rule_Set.Empty [e1__] e2__;
1.102 +val SOME (e2__,_) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty [e1__] e2__;
1.103 if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
1.104 else error "eqsystem.sml top_down_substitution,2x2] subst";
1.105
1.106 val SOME (e2__,_) =
1.107 - rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;
1.108 + rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized e2__;
1.109 if UnparseC.term e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
1.110 else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
1.111
1.112 -val SOME (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;
1.113 +val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;
1.114 if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
1.115 else error "eqsystem.sml top_down_substitution,2x2] isolate";
1.116
1.117 val t = TermC.str2term "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
1.118 -val SOME (t,_) = rewrite_set_ thy true order_system t;
1.119 +val SOME (t,_) = rewrite_set_ ctxt true order_system t;
1.120 if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
1.121 else error "eqsystem.sml top_down_substitution,2x2] order_system";
1.122
1.123 @@ -260,24 +260,24 @@
1.124 (TermC.str2term"bdv_3::real",TermC.str2term"c_3::real"),
1.125 (TermC.str2term"bdv_4::real",TermC.str2term"c_4::real")];
1.126 val SOME (t, _) =
1.127 - rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
1.128 + rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.129 if UnparseC.term t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
1.130 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
1.131
1.132 -val SOME (t, _) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
1.133 +val SOME (t, _) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
1.134 if UnparseC.term t = "[c_4 = 0, \
1.135 \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
1.136 \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
1.137 then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
1.138
1.139 -val SOME(t, _)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
1.140 +val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.141 if UnparseC.term t = "[c_4 = 0,\
1.142 \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
1.143 \ c + (c_2 + (c_3 + c_4)) = 0,\n\
1.144 \ c_2 + (c_3 + c_4) = 0]"
1.145 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
1.146
1.147 -val SOME (t, _) = rewrite_set_ thy true order_system t;
1.148 +val SOME (t, _) = rewrite_set_ ctxt true order_system t;
1.149 if UnparseC.term t = "[c_4 = 0,\
1.150 \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
1.151 \ c_2 + (c_3 + c_4) = 0,\n\
1.152 @@ -371,8 +371,8 @@
1.153 [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
1.154 val t = TermC.str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
1.155 "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
1.156 -Rewrite.trace_on := false; (*true false*)
1.157 -val SOME (t', _) = rewrite_set_ thy false prls_triangular t;
1.158 +
1.159 +val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;
1.160 (*found:...
1.161 ## try thm: NTH_CONS
1.162 ### eval asms: 1 < 2 + - 1
1.163 @@ -433,9 +433,7 @@
1.164 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
1.165 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
1.166 "solveForVars [c, c_2]", "solution LL"];
1.167 -Rewrite.trace_on := false; (*true false*)
1.168 val matches = Refine.refine fmz ["2x2", "LINEAR", "system"];
1.169 -Rewrite.trace_on := false; (*true false*)
1.170 (*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
1.171 (*brought: 'False "length_ es_ = 2"'*)
1.172