walther@60318
|
1 |
(* Title: "MathEngBasic/rewrite.sml"
|
neuper@38036
|
2 |
Author: Walther Neuper 050908
|
neuper@37906
|
3 |
(c) copyright due to lincense terms.
|
neuper@37906
|
4 |
*)
|
neuper@37906
|
5 |
|
walther@60262
|
6 |
"-----------------------------------------------------------------------------------------------";
|
walther@60262
|
7 |
"table of contents -----------------------------------------------------------------------------";
|
walther@60262
|
8 |
"-----------------------------------------------------------------------------------------------";
|
walther@60262
|
9 |
"----------- assemble rewrite ------------------------------------------------------------------";
|
walther@60262
|
10 |
"----------- test rewriting without Isac's thys ------------------------------------------------";
|
walther@60262
|
11 |
"----------- test rewriting without Isac's thys, ~~~~~ fun rewrite_ ----------------------------";
|
walther@60262
|
12 |
"----------- conditional rewriting without Isac's thys -----------------------------------------";
|
walther@60262
|
13 |
"----------- conditional rewriting without Isac's thys, ~~~~~ fun ------------------------------";
|
walther@60262
|
14 |
"----------- conditional rewriting creating an assumption---------------------------------------";
|
walther@60262
|
15 |
"----------- step through 'and rew_sub': -------------------------------------------------------";
|
walther@60262
|
16 |
"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
|
walther@60262
|
17 |
"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
|
walther@60262
|
18 |
"----------- check diff 2002--2009-3 -----------------------------------------------------------";
|
walther@60262
|
19 |
"----------- compare all prepat's existing 2010 ------------------------------------------------";
|
walther@60262
|
20 |
"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
|
walther@60262
|
21 |
"----------- 2011 thms with axclasses ----------------------------------------------------------";
|
walther@59841
|
22 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
wneuper@59252
|
23 |
"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
|
wneuper@59411
|
24 |
"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
|
walther@60262
|
25 |
"-----------------------------------------------------------------------------------------------";
|
walther@60262
|
26 |
"-----------------------------------------------------------------------------------------------";
|
walther@60262
|
27 |
"-----------------------------------------------------------------------------------------------";
|
neuper@37906
|
28 |
|
neuper@38036
|
29 |
|
walther@60262
|
30 |
"----------- assemble rewrite ------------------------------------------------------------------";
|
walther@60262
|
31 |
"----------- assemble rewrite ------------------------------------------------------------------";
|
walther@60262
|
32 |
"----------- assemble rewrite ------------------------------------------------------------------";
|
neuper@37906
|
33 |
"===== rewriting by thm with 'a";
|
neuper@41924
|
34 |
(*show_types := true;*)
|
akargl@42188
|
35 |
|
neuper@37906
|
36 |
val thy = @{theory Complex_Main};
|
neuper@37906
|
37 |
val ctxt = @{context};
|
wneuper@59112
|
38 |
val thm = @{thm add.commute};
|
Walther@60424
|
39 |
val t = TermC.parseNEW' ctxt "((r + u) + t) + (s::real)";
|
neuper@37906
|
40 |
"----- from old: fun rewrite__";
|
neuper@37906
|
41 |
val bdv = [];
|
walther@60230
|
42 |
val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm));
|
neuper@37906
|
43 |
"----- from old: and rew_sub";
|
wneuper@59395
|
44 |
val (LHS,RHS) = (dest_equals o strip_trueprop
|
neuper@37906
|
45 |
o Logic.strip_imp_concl) r;
|
neuper@37906
|
46 |
(* old
|
neuper@41942
|
47 |
val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
|
neuper@37906
|
48 |
"----- fun match_rew in Pure/pattern.ML";
|
neuper@41942
|
49 |
val rtm = the_default RHS (Term.rename_abs LHS t RHS);
|
neuper@37906
|
50 |
|
neuper@38022
|
51 |
writeln(Syntax.string_of_term ctxt rtm);
|
neuper@41942
|
52 |
writeln(Syntax.string_of_term ctxt LHS);
|
neuper@38022
|
53 |
writeln(Syntax.string_of_term ctxt t);
|
neuper@37906
|
54 |
|
neuper@41942
|
55 |
(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
|
neuper@41942
|
56 |
val (rew, RHS) = (Envir.subst_term
|
neuper@41942
|
57 |
(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
|
neuper@37906
|
58 |
(*lookup in isabelle?trace?response...*)
|
neuper@37906
|
59 |
writeln(Syntax.string_of_term ctxt rew);
|
neuper@41942
|
60 |
writeln(Syntax.string_of_term ctxt RHS);
|
neuper@37906
|
61 |
"===== rewriting: prep insertion into rew_sub";
|
neuper@37906
|
62 |
val thy = @{theory Complex_Main};
|
neuper@37906
|
63 |
val ctxt = @{context};
|
wneuper@59358
|
64 |
val thm = @{thm nonzero_divide_mult_cancel_right};
|
neuper@37906
|
65 |
val r = Thm.prop_of thm;
|
wneuper@59358
|
66 |
val tm = @{term "x / (2 * x)::real"};
|
neuper@37906
|
67 |
"----- and rew_sub";
|
neuper@41942
|
68 |
val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
|
neuper@37906
|
69 |
o Logic.strip_imp_concl) r;
|
neuper@41942
|
70 |
val r' = Envir.subst_term (Pattern.match thy (LHS, tm)
|
neuper@37906
|
71 |
(Vartab.empty, Vartab.empty)) r;
|
neuper@37906
|
72 |
val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
|
neuper@37906
|
73 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
|
neuper@37906
|
74 |
o Logic.strip_imp_concl) r';
|
neuper@37906
|
75 |
|
neuper@37906
|
76 |
(*is displayed on top of <response> buffer...*)
|
neuper@48761
|
77 |
Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
|
neuper@48761
|
78 |
Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
|
walther@60340
|
79 |
(**)
|
neuper@37906
|
80 |
|
walther@60262
|
81 |
"----------- test rewriting without Isac's thys ------------------------------------------------";
|
walther@60262
|
82 |
"----------- test rewriting without Isac's thys ------------------------------------------------";
|
walther@60262
|
83 |
"----------- test rewriting without Isac's thys ------------------------------------------------";
|
neuper@38022
|
84 |
|
neuper@37906
|
85 |
"===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
|
neuper@37906
|
86 |
val thy = @{theory Complex_Main};
|
neuper@37906
|
87 |
val ctxt = @{context};
|
wneuper@59112
|
88 |
val thm = @{thm add.commute};
|
neuper@37906
|
89 |
val tm = @{term "x + y*z::real"};
|
neuper@37906
|
90 |
|
Walther@60509
|
91 |
val SOME (r,_) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
|
neuper@37906
|
92 |
(*is displayed on _TOP_ of <response> buffer...*)
|
neuper@48761
|
93 |
Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
|
neuper@38022
|
94 |
if r = @{term "y*z + x::real"}
|
neuper@38022
|
95 |
then () else error "rewrite.sml diff.result in rewriting";
|
neuper@37906
|
96 |
|
neuper@37906
|
97 |
"----- rewriting a subterm";
|
neuper@37906
|
98 |
val tm = @{term "w*(x + y*z)::real"};
|
neuper@37906
|
99 |
|
Walther@60509
|
100 |
val SOME (r, _) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
|
neuper@37906
|
101 |
|
neuper@37906
|
102 |
"----- ordered rewriting";
|
Walther@60594
|
103 |
fun tord (_:Proof.context) (_:subst) pp = LibraryC.termless pp;
|
Walther@60594
|
104 |
if tord @{context} [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
|
neuper@38022
|
105 |
else error "rewrite.sml diff.behav. in ord.rewr.";
|
neuper@37906
|
106 |
|
Walther@60500
|
107 |
val NONE = (rewrite_ ctxt tord Rule_Set.empty false thm tm);
|
neuper@37906
|
108 |
(*is displayed on _TOP_ of <response> buffer...*)
|
neuper@48761
|
109 |
Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
|
neuper@37906
|
110 |
|
neuper@37906
|
111 |
val tm = @{term "x*y + z::real"};
|
Walther@60500
|
112 |
val SOME (r, _) = (rewrite_ ctxt tord Rule_Set.empty false thm tm);
|
neuper@37906
|
113 |
|
neuper@37906
|
114 |
|
walther@60262
|
115 |
"----------- conditional rewriting without Isac's thys -----------------------------------------";
|
walther@60262
|
116 |
"----------- conditional rewriting without Isac's thys -----------------------------------------";
|
walther@60262
|
117 |
"----------- conditional rewriting without Isac's thys -----------------------------------------";
|
neuper@37906
|
118 |
"===== prepr cond.rew. with Pattern.match";
|
neuper@37906
|
119 |
val thy = @{theory Complex_Main};
|
neuper@37906
|
120 |
val ctxt = @{context};
|
walther@60262
|
121 |
val thm = @{thm nonzero_divide_mult_cancel_right}; (* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a":*)
|
neuper@37906
|
122 |
val rule = Thm.prop_of thm;
|
wneuper@59358
|
123 |
val tm = @{term "x / (2 * x)::real"};
|
neuper@37906
|
124 |
val prem = Logic.strip_imp_prems rule;
|
neuper@37906
|
125 |
val nps = Logic.count_prems rule;
|
neuper@37906
|
126 |
val prems = Logic.strip_prems (nps, [], rule);
|
neuper@37906
|
127 |
|
neuper@37906
|
128 |
val eq = Logic.strip_imp_concl rule;
|
neuper@41942
|
129 |
val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
|
neuper@37906
|
130 |
|
neuper@41942
|
131 |
val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
|
neuper@37906
|
132 |
val rule' = Envir.subst_term mtcs rule;
|
neuper@37906
|
133 |
|
walther@60262
|
134 |
val prems' = (fst o Logic.strip_prems) (Logic.count_prems rule', [], rule');
|
walther@60262
|
135 |
val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) rule';
|
neuper@37906
|
136 |
|
walther@60262
|
137 |
(rule' |> UnparseC.term) = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
|
walther@60262
|
138 |
rule';
|
walther@60262
|
139 |
|
walther@60262
|
140 |
(rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
|
walther@60262
|
141 |
rule' |> Logic.strip_imp_concl;
|
walther@60262
|
142 |
|
walther@60262
|
143 |
(rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
|
walther@60262
|
144 |
rule' |> Logic.strip_imp_concl;
|
walther@60262
|
145 |
|
walther@60262
|
146 |
|
walther@60262
|
147 |
"----------- conditional rewriting creating an assumption---------------------------------------";
|
walther@60262
|
148 |
"----------- conditional rewriting creating an assumption---------------------------------------";
|
walther@60262
|
149 |
"----------- conditional rewriting creating an assumption---------------------------------------";
|
wneuper@59358
|
150 |
val thm = @{thm nonzero_divide_mult_cancel_right};
|
wneuper@59358
|
151 |
val tm = @{term "x / (2 * x)::real"};
|
walther@60262
|
152 |
|
Walther@60509
|
153 |
val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;
|
neuper@37906
|
154 |
|
wneuper@59358
|
155 |
if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
|
neuper@38022
|
156 |
else error "rewrite.sml diff.result in cond.rew.";
|
neuper@37906
|
157 |
|
wneuper@59358
|
158 |
if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
|
neuper@38022
|
159 |
then () else error "rewrite.sml diff.asm in cond.rew.";
|
neuper@38022
|
160 |
"----- conditional rewriting immediately: can only be done with ";
|
Walther@60586
|
161 |
"------Isabelle numerals, because asm_rls cannot handle them yet.";
|
neuper@37906
|
162 |
|
neuper@37906
|
163 |
|
walther@60262
|
164 |
"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
|
walther@60262
|
165 |
"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
|
walther@60262
|
166 |
"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
|
walther@60262
|
167 |
val thm = @{thm nonzero_divide_mult_cancel_right};(* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a"*)
|
walther@60262
|
168 |
val tm = @{term "x / (2 * x)::real"};
|
Walther@60586
|
169 |
val asm_rls = eval_rls;
|
walther@60262
|
170 |
|
Walther@60509
|
171 |
(**)val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;
|
walther@60262
|
172 |
(** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
|
walther@60262
|
173 |
dest_Trueprop
|
walther@60262
|
174 |
?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
|
Walther@60586
|
175 |
"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, asm_rls, bool, thm, term) =
|
Walther@60586
|
176 |
(thy, Rewrite_Ord.function_empty, asm_rls, false, thm, tm);
|
walther@60262
|
177 |
"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
|
Walther@60586
|
178 |
(thy, 1, []: Subst.T, rew_ord, asm_rls, bool, thm, term);
|
walther@60262
|
179 |
|
Walther@60500
|
180 |
(**) val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
|
walther@60262
|
181 |
(TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;
|
walther@60262
|
182 |
(** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
|
walther@60262
|
183 |
dest_Trueprop
|
walther@60262
|
184 |
?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
|
walther@60262
|
185 |
"~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
|
walther@60262
|
186 |
(thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
|
walther@60262
|
187 |
(TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);
|
walther@60262
|
188 |
(*+*)UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
|
walther@60262
|
189 |
|
walther@60262
|
190 |
val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r;
|
walther@60262
|
191 |
(*+*)(UnparseC.term lhs, UnparseC.term rhs) = ("?b / (?a * ?b)", "(1::?'a) / ?a");
|
walther@60262
|
192 |
val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
|
walther@60262
|
193 |
handle Pattern.MATCH => raise NO_REWRITE;
|
walther@60262
|
194 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'));
|
walther@60262
|
195 |
(*+*)UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
|
walther@60262
|
196 |
(*+*)r';
|
walther@60262
|
197 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
|
Walther@60500
|
198 |
val _ = trace_in2 ctxt i "eval asms" r';
|
Walther@60500
|
199 |
val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls;
|
walther@60262
|
200 |
(*if*) nofalse (*then*);
|
Walther@60500
|
201 |
val (t'', p'') = (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t',simpl_p'));
|
walther@60262
|
202 |
(*## asms accepted: [x \<noteq> 0] stored: [x \<noteq> 0] *)
|
walther@60262
|
203 |
|
walther@60262
|
204 |
(*+*)if (UnparseC.term t'', map UnparseC.term p'') = ("1 / 2", ["x \<noteq> 0"]) then ()
|
walther@60262
|
205 |
(*+*)else error "conditional rewriting x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2 CHANGED";
|
walther@60262
|
206 |
|
walther@60262
|
207 |
|
neuper@38022
|
208 |
"----------- step through 'and rew_sub': ----------------";
|
neuper@38022
|
209 |
"----------- step through 'and rew_sub': ----------------";
|
neuper@38022
|
210 |
"----------- step through 'and rew_sub': ----------------";
|
neuper@38022
|
211 |
(*and make asms without Trueprop, beginning with the result:*)
|
wneuper@59358
|
212 |
val tm = @{term "x / (2 * x)::real"};
|
Walther@60509
|
213 |
val (t', asm, _, _) = rew_sub ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true [] (Thm.prop_of thm) tm;
|
neuper@41924
|
214 |
(*show_types := false;*)
|
neuper@38022
|
215 |
"----- evaluate arguments";
|
neuper@38022
|
216 |
val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
|
Walther@60509
|
217 |
(thy, 0, [], Rewrite_Ord.function_empty, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
|
neuper@41942
|
218 |
"----- step 1: LHS, RHS of rule";
|
neuper@41942
|
219 |
val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
|
neuper@38022
|
220 |
o Logic.strip_imp_concl) r;
|
walther@59868
|
221 |
UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
|
walther@59868
|
222 |
UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term RHS = "(1::?'a) / ?a";
|
neuper@38022
|
223 |
"----- step 2: the rule instantiated";
|
neuper@38025
|
224 |
val r' = Envir.subst_term
|
neuper@41942
|
225 |
(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
|
walther@59868
|
226 |
UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
|
neuper@38022
|
227 |
"----- step 3: get the (instantiated) assumption(s)";
|
neuper@38022
|
228 |
val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
|
walther@59868
|
229 |
UnparseC.term (hd p') = "x \<noteq> 0";
|
neuper@38022
|
230 |
"=====vvv make asms without Trueprop ---vvv";
|
neuper@38022
|
231 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
|
neuper@38022
|
232 |
(Logic.count_prems r', [], r'));
|
neuper@38022
|
233 |
case p' of
|
wenzelm@60309
|
234 |
[Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _)
|
walther@60336
|
235 |
$ Free ("x", _) $ Const (\<^const_name>\<open>zero_class.zero\<close>, _))] => ()
|
neuper@38022
|
236 |
| _ => error "rewrite.sml assumption changed";
|
walther@60242
|
237 |
"===== \<up> make asms without Trueprop --- \<up> ";
|
neuper@41942
|
238 |
"----- step 4: get the (instantiated) RHS";
|
neuper@38022
|
239 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
|
neuper@38022
|
240 |
o Logic.strip_imp_concl) r';
|
walther@59868
|
241 |
UnparseC.term t' = "1 / 2";
|
neuper@37906
|
242 |
|
walther@60262
|
243 |
"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
|
walther@60262
|
244 |
"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
|
walther@60262
|
245 |
"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
|
neuper@38025
|
246 |
"----- step 0: args for rewrite_terms_, local fun";
|
Walther@60586
|
247 |
val (thy, ord, asm_rls, equs, t) =
|
Walther@60660
|
248 |
(@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [ParseC.parse_test @{context} "x = 0"],
|
Walther@60660
|
249 |
ParseC.parse_test @{context} "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
|
neuper@38025
|
250 |
"----- step 1: args for rew_";
|
walther@59861
|
251 |
val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
|
neuper@38025
|
252 |
"----- step 2: rew_sub";
|
Walther@60586
|
253 |
rew_sub ctxt 1 [] ord asm_rls false [] (HOLogic.Trueprop $ r) t;
|
neuper@38025
|
254 |
"----- step 3: step through rew_sub -- inefficient: goes into subterms";
|
neuper@38025
|
255 |
|
neuper@38025
|
256 |
|
Walther@60509
|
257 |
val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
|
walther@60262
|
258 |
writeln "---------- rewrite_terms_ 1---------------------------";
|
walther@60317
|
259 |
if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
|
neuper@38031
|
260 |
else error "rewrite.sml rewrite_terms_ [x = 0]";
|
neuper@37906
|
261 |
|
Walther@60660
|
262 |
val equs = [ParseC.parse_test @{context} "M_b 0 = 0"];
|
Walther@60660
|
263 |
val t = ParseC.parse_test @{context} "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
|
Walther@60509
|
264 |
val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
|
walther@60262
|
265 |
writeln "---------- rewrite_terms_ 2---------------------------";
|
walther@60317
|
266 |
if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
|
neuper@38031
|
267 |
else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
|
neuper@37906
|
268 |
|
Walther@60660
|
269 |
val equs = [ParseC.parse_test @{context} "x = 0", ParseC.parse_test @{context}"M_b 0 = 0"];
|
Walther@60660
|
270 |
val t = ParseC.parse_test @{context} "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
|
Walther@60509
|
271 |
val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
|
walther@60262
|
272 |
writeln "---------- rewrite_terms_ 3---------------------------";
|
walther@60317
|
273 |
if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
|
neuper@38031
|
274 |
else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
|
neuper@37906
|
275 |
|
neuper@37906
|
276 |
|
walther@60262
|
277 |
"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
|
walther@60262
|
278 |
"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
|
walther@60262
|
279 |
"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
|
neuper@37906
|
280 |
(*see smltest/Scripts/term_G.sml: inst_bdv 2*)
|
Walther@60660
|
281 |
val t = ParseC.parse_test @{context}"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";
|
Walther@60660
|
282 |
val bdvs = [(ParseC.parse_test @{context}"bdv_1",ParseC.parse_test @{context}"c"),
|
Walther@60660
|
283 |
(ParseC.parse_test @{context}"bdv_2",ParseC.parse_test @{context}"c_2"),
|
Walther@60660
|
284 |
(ParseC.parse_test @{context}"bdv_3",ParseC.parse_test @{context}"c_3"),
|
Walther@60660
|
285 |
(ParseC.parse_test @{context}"bdv_4",ParseC.parse_test @{context}"c_4")];
|
neuper@37906
|
286 |
(*------------ outcommented WN071210, after inclusion into ROOT.ML
|
neuper@37926
|
287 |
val SOME (t,_) =
|
neuper@37906
|
288 |
rewrite_inst_ thy e_rew_ord
|
walther@59852
|
289 |
(Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
|
walther@60278
|
290 |
[(Eval ("EqSystem.occur_exactly_in",
|
neuper@37906
|
291 |
eval_occur_exactly_in
|
neuper@37906
|
292 |
"#eval_occur_exactly_in_"))
|
neuper@37906
|
293 |
])
|
walther@59871
|
294 |
false bdvs (ThmC.numerals_to_Free @{separate_bdvs_add) t;
|
walther@59868
|
295 |
(writeln o UnparseC.term) t;
|
walther@60242
|
296 |
if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L \<up> 2) / 2)"
|
neuper@38031
|
297 |
then () else error "rewrite.sml rewrite_inst_ bdvs";
|
walther@60330
|
298 |
> Rewrite.trace_on:=true;false
|
walther@59901
|
299 |
Rewrite.trace_on:=false;--------------------------------------------*)
|
neuper@37906
|
300 |
|
neuper@38025
|
301 |
|
walther@60262
|
302 |
"----------- compare all prepat's existing 2010 ------------------------------------------------";
|
walther@60262
|
303 |
"----------- compare all prepat's existing 2010 ------------------------------------------------";
|
walther@60262
|
304 |
"----------- compare all prepat's existing 2010 ------------------------------------------------";
|
wneuper@59592
|
305 |
val thy = @{theory "Isac_Knowledge"};
|
neuper@38036
|
306 |
val t = @{term "a + b * x = (0 ::real)"};
|
walther@60230
|
307 |
val pat = TermC.parse_patt thy "?l = (?r ::real)";
|
walther@60230
|
308 |
val precond = TermC.parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
|
walther@60230
|
309 |
val precond = TermC.parse_patt thy "(?l::real) is_expanded";
|
neuper@38036
|
310 |
|
neuper@38036
|
311 |
val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
|
neuper@38036
|
312 |
val preinst = Envir.subst_term inst precond;
|
walther@59868
|
313 |
UnparseC.term preinst;
|
neuper@38036
|
314 |
|
neuper@38036
|
315 |
"===== Rational.thy: cancel ===";
|
neuper@38036
|
316 |
(* pat matched with the current term gives an environment
|
neuper@38036
|
317 |
(or not: hen the Rrls not applied);
|
neuper@48760
|
318 |
if pre1 and pre2 evaluate to @{term True} in this environment,
|
neuper@38036
|
319 |
then the Rrls is applied. *)
|
Walther@60660
|
320 |
val t = ParseC.parse_test @{context} "(a + b) / c ::real";
|
walther@60230
|
321 |
val pat = TermC.parse_patt thy "?r / ?s ::real";
|
walther@60230
|
322 |
val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"];
|
neuper@38036
|
323 |
val prepat = [(pres, pat)];
|
Walther@60586
|
324 |
val asm_rls = rational_erls;
|
Walther@60586
|
325 |
(* asm_rls got from Rrls {asm_rls, prepat, program = Rfuns {normal_form, ...}, ...} *)
|
neuper@38036
|
326 |
|
neuper@38036
|
327 |
val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
|
neuper@38036
|
328 |
val asms = map (Envir.subst_term subst) pres;
|
walther@59997
|
329 |
if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
|
neuper@38036
|
330 |
then () else error "rewrite.sml: prepat cancel subst";
|
walther@60318
|
331 |
|
Walther@60586
|
332 |
if ([], true) = eval__true ctxt 0 asms [] asm_rls
|
neuper@38036
|
333 |
then () else error "rewrite.sml: prepat cancel eval__true";
|
neuper@38036
|
334 |
|
neuper@52105
|
335 |
"===== Rational.thy: add_fractions_p ===";
|
walther@60230
|
336 |
(* if each pat* TermC.matches with the current term, the Rrls is applied
|
neuper@48760
|
337 |
(there are no preconditions to be checked, they are @{term True}) *)
|
Walther@60660
|
338 |
val t = ParseC.parse_test @{context} "a / b + 1 / 2";
|
walther@60230
|
339 |
val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";
|
neuper@48760
|
340 |
val pres = [@{term True}];
|
neuper@38036
|
341 |
val prepat = [(pres, pat)];
|
Walther@60586
|
342 |
val asm_rls = rational_erls;
|
Walther@60586
|
343 |
(* asm_rls got from Rrls {asm_rls, prepat, program = Rfuns {normal_form, ...}, ...} *)
|
neuper@38036
|
344 |
|
neuper@38036
|
345 |
val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
|
Walther@60586
|
346 |
if ([], true) = eval__true ctxt 0 (map (Envir.subst_term subst) pres) [] asm_rls
|
neuper@52105
|
347 |
then () else error "rewrite.sml: prepat add_fractions_p";
|
neuper@38036
|
348 |
|
neuper@38036
|
349 |
"===== Poly.thy: order_mult_ ===";
|
neuper@38036
|
350 |
(* ?p matched with the current term gives an environment,
|
neuper@38036
|
351 |
which evaluates (the instantiated) "p is_multUnordered" to true*)
|
Walther@60660
|
352 |
val t = ParseC.parse_test @{context} "x \<up> 2 * x";
|
walther@60230
|
353 |
val pat = TermC.parse_patt thy "?p :: real"
|
walther@60230
|
354 |
val pres = [TermC.parse_patt thy "?p is_multUnordered"];
|
neuper@38036
|
355 |
val prepat = [(pres, pat)];
|
Walther@60586
|
356 |
val asm_rls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
|
walther@60278
|
357 |
[Eval ("Poly.is_multUnordered",
|
neuper@38036
|
358 |
eval_is_multUnordered "")];
|
neuper@38036
|
359 |
|
neuper@38036
|
360 |
val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
|
neuper@38036
|
361 |
val asms = map (Envir.subst_term subst) pres;
|
walther@60242
|
362 |
if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
|
neuper@38036
|
363 |
then () else error "rewrite.sml: prepat order_mult_ subst";
|
walther@60318
|
364 |
|
Walther@60586
|
365 |
if ([], true) = eval__true ctxt 0 asms [] asm_rls
|
neuper@38036
|
366 |
then () else error "rewrite.sml: prepat order_mult_ eval__true";
|
neuper@38036
|
367 |
|
neuper@38036
|
368 |
|
walther@60262
|
369 |
"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
|
walther@60262
|
370 |
"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
|
walther@60262
|
371 |
"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
|
Walther@60660
|
372 |
val t = ParseC.parse_test @{context} "x \<up> 2 * x";
|
neuper@41928
|
373 |
|
neuper@38039
|
374 |
if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
|
Walther@60660
|
375 |
val tm = ParseC.parse_test @{context} "(x \<up> 2 * x) is_multUnordered";
|
walther@60318
|
376 |
|
Walther@60504
|
377 |
(*+*)case eval_is_multUnordered "testid" "" tm ctxt of
|
walther@60318
|
378 |
(*+*) SOME
|
walther@60318
|
379 |
(*+*) ("testidx \<up> 2 * x_",
|
walther@60336
|
380 |
(*+*) Const (\<^const_name>\<open>Trueprop\<close>, _) $
|
walther@60336
|
381 |
(*+*) (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
|
walther@60336
|
382 |
(*+*) (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $
|
walther@60336
|
383 |
(*+*) (Const (\<^const_name>\<open>times\<close>, _) $
|
wenzelm@60405
|
384 |
(*+*) (Const (\<^const_name>\<open>realpow\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
|
walther@60336
|
385 |
(*+*) Const (\<^const_name>\<open>True\<close>, _))) => ()
|
walther@60318
|
386 |
(*+*)(* ^^^^^^ compare ---vvv *)
|
walther@60318
|
387 |
(*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
|
walther@60318
|
388 |
|
walther@60318
|
389 |
|
Walther@60504
|
390 |
eval_is_multUnordered "testid" "" tm ctxt;
|
neuper@41928
|
391 |
|
Walther@60504
|
392 |
case eval_is_multUnordered "testid" "" tm ctxt of
|
wenzelm@60309
|
393 |
SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
|
wenzelm@60309
|
394 |
(Const (\<^const_name>\<open>HOL.eq\<close>, _) $
|
walther@60336
|
395 |
(Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
|
wenzelm@60309
|
396 |
Const (\<^const_name>\<open>True\<close>, _))) => ()
|
neuper@41928
|
397 |
| _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
|
neuper@38039
|
398 |
|
Walther@60500
|
399 |
tracing "----- begin rewrite x \<up> 2 * x ---";
|
Walther@60500
|
400 |
val SOME (t', _) = rewrite_set_ ctxt true order_mult_ t;
|
Walther@60500
|
401 |
tracing "----- end rewrite x \<up> 2 * x ---";
|
walther@60242
|
402 |
if UnparseC.term t' = "x * x \<up> 2" then ()
|
walther@60278
|
403 |
else error "rewrite.sml Poly.is_multUnordered doesn't work";
|
neuper@38039
|
404 |
|
neuper@38039
|
405 |
(* for achieving the previous result, the following code was taken apart *)
|
neuper@38039
|
406 |
"----- rewrite__set_ ---";
|
neuper@38039
|
407 |
val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
|
Walther@60500
|
408 |
val (t', asm, rew) = app_rev ctxt (i+1) rrls t;
|
neuper@38039
|
409 |
"----- app_rev ---";
|
neuper@38039
|
410 |
val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
|
Walther@60586
|
411 |
fun chk_prepat thy asm_rls [] t = true
|
Walther@60586
|
412 |
| chk_prepat thy asm_rls prepat t =
|
neuper@38039
|
413 |
let fun chk (pres, pat) =
|
neuper@38039
|
414 |
(let val subst: Type.tyenv * Envir.tenv =
|
neuper@38039
|
415 |
Pattern.match thy (pat, t)
|
neuper@38039
|
416 |
(Vartab.empty, Vartab.empty)
|
Walther@60500
|
417 |
in snd (eval__true ctxt (i+1)
|
neuper@38039
|
418 |
(map (Envir.subst_term subst) pres)
|
Walther@60586
|
419 |
[] asm_rls)
|
neuper@38039
|
420 |
end)
|
walther@60270
|
421 |
handle Pattern.MATCH => false
|
neuper@38039
|
422 |
fun scan_ f [] = false (*scan_ NEVER called by []*)
|
neuper@38039
|
423 |
| scan_ f (pp::pps) = if f pp then true
|
neuper@38039
|
424 |
else scan_ f pps;
|
neuper@38039
|
425 |
in scan_ chk prepat end;
|
neuper@38039
|
426 |
|
neuper@38039
|
427 |
(*.apply the normal_form of a rev-set.*)
|
Walther@60586
|
428 |
fun app_rev' thy (Rrls{asm_rls,prepat,program=Rfuns{normal_form,...},...}) t =
|
Walther@60586
|
429 |
if chk_prepat thy asm_rls prepat t
|
walther@59868
|
430 |
then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)
|
neuper@38039
|
431 |
normal_form t)
|
neuper@38039
|
432 |
else NONE;
|
neuper@38039
|
433 |
(*fixme val NONE = app_rev' thy rrls t;*)
|
neuper@38039
|
434 |
"----- app_rev' ---";
|
Walther@60586
|
435 |
val (thy, Rrls{asm_rls,prepat,program=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
|
Walther@60586
|
436 |
(*fixme false*) chk_prepat thy asm_rls prepat t;
|
neuper@38039
|
437 |
"----- chk_prepat ---";
|
Walther@60586
|
438 |
val (thy, asm_rls, prepat, t) = (thy, asm_rls, prepat, t);
|
neuper@38039
|
439 |
fun chk (pres, pat) =
|
neuper@38039
|
440 |
(let val subst: Type.tyenv * Envir.tenv =
|
neuper@38039
|
441 |
Pattern.match thy (pat, t)
|
neuper@38039
|
442 |
(Vartab.empty, Vartab.empty)
|
Walther@60500
|
443 |
in snd (eval__true ctxt (i+1)
|
neuper@38039
|
444 |
(map (Envir.subst_term subst) pres)
|
Walther@60586
|
445 |
[] asm_rls)
|
neuper@38039
|
446 |
end)
|
walther@60270
|
447 |
handle Pattern.MATCH => false;
|
walther@60270
|
448 |
fun scan_ _ [] = false (*scan_ NEVER called by []*)
|
neuper@38039
|
449 |
| scan_ f (pp::pps) = if f pp then true
|
neuper@38039
|
450 |
else scan_ f pps;
|
neuper@38039
|
451 |
tracing "=== poly.sml: scan_ chk prepat begin";
|
neuper@38039
|
452 |
scan_ chk prepat;
|
neuper@38039
|
453 |
tracing "=== poly.sml: scan_ chk prepat end";
|
neuper@38039
|
454 |
|
neuper@38039
|
455 |
"----- chk ---";
|
Walther@60660
|
456 |
(*reestablish...*) val t = ParseC.parse_test @{context} "x \<up> 2 * x";
|
neuper@38039
|
457 |
val [(pres, pat)] = prepat;
|
neuper@38039
|
458 |
val subst: Type.tyenv * Envir.tenv =
|
neuper@38039
|
459 |
Pattern.match thy (pat, t)
|
neuper@38039
|
460 |
(Vartab.empty, Vartab.empty);
|
neuper@38039
|
461 |
|
neuper@38039
|
462 |
(*fixme: asms = ["p is_multUnordered"]...instantiate*)
|
neuper@38039
|
463 |
"----- eval__true ---";
|
neuper@38039
|
464 |
val asms = (map (Envir.subst_term subst) pres);
|
walther@60242
|
465 |
if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then ()
|
neuper@38039
|
466 |
else error "rewrite.sml: diff. is_multUnordered, asms";
|
neuper@38039
|
467 |
val (thy, i, asms, bdv, rls) =
|
Walther@60660
|
468 |
(thy, (i+1), [ParseC.parse_test @{context} "(x \<up> 2 * x) is_multUnordered"],
|
Walther@60586
|
469 |
[] : Subst.T, asm_rls);
|
Walther@60500
|
470 |
case eval__true ctxt i asms bdv rls of
|
neuper@38039
|
471 |
([], true) => ()
|
neuper@38039
|
472 |
| _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
|
neuper@42223
|
473 |
|
walther@60262
|
474 |
"----------- 2011 thms with axclasses ----------------------------------------------------------";
|
walther@60262
|
475 |
"----------- 2011 thms with axclasses ----------------------------------------------------------";
|
walther@60262
|
476 |
"----------- 2011 thms with axclasses ----------------------------------------------------------";
|
walther@60337
|
477 |
val thm = @{thm div_by_1};
|
wneuper@59188
|
478 |
val prop = Thm.prop_of thm;
|
Walther@60650
|
479 |
TermC.atom_trace_detail @{context} prop; (*Type 'a*)
|
Walther@60660
|
480 |
val t = ParseC.parse_test @{context} "(2*x)/1"; (*Type real*)
|
neuper@42223
|
481 |
|
neuper@42223
|
482 |
val (thy, ro, er, inst) =
|
wneuper@59592
|
483 |
(@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
|
Walther@60500
|
484 |
val SOME (t, _) = rewrite_ ctxt ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)
|
neuper@42223
|
485 |
|
walther@59841
|
486 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
walther@59841
|
487 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
walther@59841
|
488 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
walther@59841
|
489 |
val thy = @{theory RatEq};
|
walther@59841
|
490 |
val ctxt = Proof_Context.init_global thy;
|
Walther@60424
|
491 |
val SOME t = TermC.parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
|
Walther@60543
|
492 |
val rls = get_rls ctxt "RatEq_eliminate"
|
neuper@42394
|
493 |
|
walther@59841
|
494 |
val SOME (t''''', asm''''') =
|
Walther@60500
|
495 |
rewrite_set_ ctxt true rls t;
|
walther@59841
|
496 |
"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
|
Walther@60500
|
497 |
rewrite__set_ ctxt 1 bool [] rls term;
|
walther@59841
|
498 |
"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
|
Walther@60477
|
499 |
= (thy, 1, bool, []:Subst.T, rls, term);
|
walther@59841
|
500 |
|
walther@59841
|
501 |
(*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
|
walther@59920
|
502 |
datatype switch = Applicable.Yes | Noap;
|
walther@59841
|
503 |
fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
|
walther@59920
|
504 |
| rew_once ruls asm ct Applicable.Yes [] =
|
walther@59851
|
505 |
(case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
|
walther@59878
|
506 |
| Rule_Set.Sequence _ => (ct, asm)
|
walther@59867
|
507 |
| rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
|
walther@59841
|
508 |
| rew_once ruls asm ct apno (rul :: thms) =
|
walther@59841
|
509 |
case rul of
|
walther@59841
|
510 |
Rule.Thm (thmid, thm) =>
|
walther@59841
|
511 |
(trace1 i (" try thm: " ^ thmid);
|
walther@59852
|
512 |
case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
|
Walther@60586
|
513 |
((#asm_rls o Rule.Rule_Set.rep) rls) put_asm thm ct of
|
walther@59841
|
514 |
NONE => rew_once ruls asm ct apno thms
|
walther@59841
|
515 |
| SOME (ct', asm') =>
|
walther@59870
|
516 |
(trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
|
walther@59920
|
517 |
rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms)))
|
walther@59841
|
518 |
(* once again try the same rule, e.g. associativity against "()"*)
|
walther@59878
|
519 |
| Rule.Eval (cc as (op_, _)) =>
|
walther@59841
|
520 |
let val _= trace1 i (" try calc: " ^ op_ ^ "'")
|
walther@59841
|
521 |
val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
|
Walther@60519
|
522 |
in case Eval.adhoc_thm ctxt cc ct of
|
walther@59841
|
523 |
NONE => rew_once ruls asm ct apno thms
|
walther@59841
|
524 |
| SOME (_, thm') =>
|
walther@59841
|
525 |
let
|
walther@59852
|
526 |
val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
|
Walther@60586
|
527 |
((#asm_rls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
|
walther@59841
|
528 |
val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
|
walther@59875
|
529 |
ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
|
walther@59870
|
530 |
val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
|
walther@59920
|
531 |
in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end
|
walther@59841
|
532 |
end
|
walther@59841
|
533 |
| Rule.Cal1 (cc as (op_, _)) =>
|
walther@59841
|
534 |
let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
|
walther@59841
|
535 |
val ct = TermC.uminus_to_string ct
|
Walther@60519
|
536 |
in case Eval.adhoc_thm1_ @{context} cc ct of
|
walther@59841
|
537 |
NONE => (ct, asm)
|
walther@59841
|
538 |
| SOME (_, thm') =>
|
walther@59841
|
539 |
let
|
walther@59852
|
540 |
val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
|
Walther@60586
|
541 |
((#asm_rls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
|
walther@59841
|
542 |
val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
|
walther@59875
|
543 |
ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
|
walther@59870
|
544 |
val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
|
walther@59841
|
545 |
in the pairopt end
|
walther@59841
|
546 |
end
|
walther@59841
|
547 |
| Rule.Rls_ rls' =>
|
walther@59841
|
548 |
(case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
|
walther@59920
|
549 |
SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms
|
walther@59841
|
550 |
| NONE => rew_once ruls asm ct apno thms)
|
walther@59867
|
551 |
| r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
|
walther@59852
|
552 |
val ruls = (#rules o Rule.Rule_Set.rep) rls;
|
walther@59870
|
553 |
(* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)*)
|
walther@59841
|
554 |
val (ct', asm') = rew_once ruls [] ct Noap ruls;
|
walther@59841
|
555 |
"~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
|
walther@59841
|
556 |
= (ruls, []:term list, ct, Noap, ruls);
|
walther@59841
|
557 |
val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
|
walther@59841
|
558 |
|
walther@59841
|
559 |
val SOME (ct', asm') = (*case*)
|
walther@59852
|
560 |
rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
|
Walther@60586
|
561 |
((#asm_rls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
|
walther@59841
|
562 |
"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
|
walther@59852
|
563 |
= (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
|
Walther@60586
|
564 |
((#asm_rls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
|
walther@59841
|
565 |
|
walther@59841
|
566 |
val (t', asms, _ (*lrd*), rew) =
|
walther@59841
|
567 |
rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
|
wenzelm@60203
|
568 |
(((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm) ct;
|
walther@59841
|
569 |
"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
|
walther@59841
|
570 |
= (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
|
wenzelm@60203
|
571 |
(((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct);
|
walther@59841
|
572 |
val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
|
walther@59841
|
573 |
val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
|
walther@59841
|
574 |
;
|
walther@59868
|
575 |
(*+*)if UnparseC.term r' =
|
walther@60242
|
576 |
(*+*) "\<lbrakk>9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
|
walther@60242
|
577 |
(*+*) "\<Longrightarrow> ((3 + -1 * x + x \<up> 2) /\n" ^
|
walther@60242
|
578 |
(*+*) " (9 * x + -6 * x \<up> 2 + x \<up> 3) =\n" ^
|
walther@59841
|
579 |
(*+*) " 1 / x) =\n" ^
|
walther@60242
|
580 |
(*+*) " ((3 + -1 * x + x \<up> 2) * x =\n" ^
|
walther@60242
|
581 |
(*+*) " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3))"
|
walther@59841
|
582 |
(*+*)then () else error "instantiated rule CHANGED";
|
walther@59841
|
583 |
|
walther@59841
|
584 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
|
walther@59841
|
585 |
;
|
walther@60242
|
586 |
(*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
|
walther@59841
|
587 |
(*+*)then () else error "stored assumptions CHANGED";
|
walther@59841
|
588 |
|
walther@59841
|
589 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
|
walther@59841
|
590 |
;
|
walther@60242
|
591 |
(*+*)if UnparseC.term t' = "(3 + -1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)"
|
walther@59841
|
592 |
(*+*)then () else error "rewritten term (an equality) CHANGED";
|
walther@59841
|
593 |
|
walther@59841
|
594 |
val (simpl_p', nofalse) =
|
walther@59841
|
595 |
eval__true thy (i + 1) p' bdv rls;
|
walther@59841
|
596 |
"~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
|
walther@59841
|
597 |
(*if*) asms = [@{term True}] orelse asms = [] (*else*);
|
walther@59841
|
598 |
|
walther@60242
|
599 |
(*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
|
walther@59841
|
600 |
(*+*)then () else error "asms before chk CHANGED";
|
walther@59841
|
601 |
|
walther@59841
|
602 |
fun chk indets [] = (indets, true) (*return asms<>True until false*)
|
walther@59841
|
603 |
| chk indets (a :: asms) =
|
walther@59841
|
604 |
(case rewrite__set_ thy (i + 1) false bdv rls a of
|
walther@59841
|
605 |
NONE => (chk (indets @ [a]) asms)
|
walther@59841
|
606 |
| SOME (t, a') =>
|
walther@59841
|
607 |
if t = @{term True} then (chk (indets @ a') asms)
|
walther@59841
|
608 |
else if t = @{term False} then ([], false)
|
walther@60242
|
609 |
(*asm false .. thm not applied \<up> ; continue until False vvv*)
|
walther@59841
|
610 |
else chk (indets @ [t] @ a') asms);
|
walther@59841
|
611 |
|
walther@59841
|
612 |
val (xxx, true) =
|
walther@59841
|
613 |
chk [] asms; (*return from eval__true*);
|
walther@59841
|
614 |
"~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
|
walther@59841
|
615 |
|
walther@59851
|
616 |
(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
|
walther@59841
|
617 |
(*+*)(*val rules =
|
wenzelm@60309
|
618 |
(*+*) [Eval (\<^const_name>\<open>divide\<close>, fn),
|
walther@59841
|
619 |
(*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
|
walther@59841
|
620 |
(*+*) :
|
wenzelm@60309
|
621 |
(*+*) Eval (\<^const_name>\<open>HOL.eq\<close>, fn),
|
walther@59841
|
622 |
(*+*) Thm ("not_true", "(\<not> True) = False"),
|
walther@59841
|
623 |
(*+*) Thm ("not_false", "(\<not> False) = True"),
|
walther@59841
|
624 |
(*+*) :
|
wenzelm@60405
|
625 |
(*+*) Eval (\<^const_name>\<open>realpow\<close>, fn),
|
walther@60278
|
626 |
(*+*) Eval ("RatEq.is_ratequation_in", fn)]:
|
walther@59841
|
627 |
(*+*) rule list*)
|
walther@59841
|
628 |
(*+*)chk: term list -> term list -> term list * bool
|
walther@59841
|
629 |
|
walther@59841
|
630 |
rewrite__set_ thy (i + 1) false bdv rls a (*of*);
|
walther@59841
|
631 |
|
walther@60330
|
632 |
(*+*)Rewrite.trace_on := false; (*true false*)
|
walther@59841
|
633 |
|
walther@59841
|
634 |
(*this was False; vvvv--- means: indeterminate*)
|
walther@59841
|
635 |
val (* SOME (t, a') *)NONE = (*case*)
|
walther@59841
|
636 |
rewrite__set_ thy (i + 1) false bdv rls a (*of*);
|
walther@59841
|
637 |
|
walther@59868
|
638 |
(*+*)UnparseC.term a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
|
neuper@42394
|
639 |
(*
|
neuper@42394
|
640 |
:
|
walther@59841
|
641 |
#### rls: rateq_erls on: x \<noteq> 0
|
neuper@42394
|
642 |
:
|
neuper@42394
|
643 |
##### try calc: HOL.eq' <<<------------------------------- here the error comes from
|
walther@59841
|
644 |
===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
|
neuper@42394
|
645 |
##### try calc: HOL.eq'
|
neuper@42394
|
646 |
##### try thm: not_true
|
neuper@42394
|
647 |
##### try thm: not_false
|
walther@59841
|
648 |
===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
|
walther@59841
|
649 |
and True, False are NOT stored ...
|
walther@59841
|
650 |
:
|
walther@59841
|
651 |
### asms accepted: [x \<noteq> 0] stored: []
|
walther@59841
|
652 |
: *)
|
walther@60330
|
653 |
Rewrite.trace_on := false; (*true false*)
|
walther@59841
|
654 |
( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
|
walther@59841
|
655 |
|
neuper@42394
|
656 |
|
wneuper@59252
|
657 |
"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
|
wneuper@59252
|
658 |
"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
|
wneuper@59252
|
659 |
"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
|
Walther@60586
|
660 |
"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, asm_rls, bool, thm, term) =
|
Walther@60509
|
661 |
(@{theory}, Rewrite_Ord.function_empty, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
|
wneuper@59252
|
662 |
"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
|
Walther@60586
|
663 |
(thy, 1, [], rew_ord, asm_rls, bool, thm, term);
|
wneuper@59252
|
664 |
"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
|
walther@60230
|
665 |
(thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)
|
walther@60262
|
666 |
val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r
|
wneuper@59252
|
667 |
val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
|
wneuper@59252
|
668 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
|
walther@60262
|
669 |
val t' = (snd o HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r'
|
wneuper@59252
|
670 |
;
|
walther@59868
|
671 |
if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()
|
wneuper@59252
|
672 |
else error "ARGS FOR Pattern.match CHANGED";
|
wneuper@59252
|
673 |
val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
|
walther@59868
|
674 |
if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
|
wneuper@59252
|
675 |
else error "Pattern.match CHANGED";
|
wneuper@59381
|
676 |
|
walther@60262
|
677 |
"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
|
walther@60262
|
678 |
"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
|
walther@60262
|
679 |
"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
|
wneuper@59411
|
680 |
(* norm_equation is defined in Test.thy, other rls see Knowledg/**)
|
wneuper@59411
|
681 |
val thy = @{theory};
|
wneuper@59411
|
682 |
val rls = norm_equation;
|
Walther@60660
|
683 |
val term = ParseC.parse_test @{context} "x + 1 = 2";
|
wneuper@59411
|
684 |
|
Walther@60500
|
685 |
(**)val SOME (t, asm) = rewrite_set_ ctxt false rls term;
|
walther@60262
|
686 |
(** )##### try thm: "root_ge0"
|
walther@60262
|
687 |
exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):
|
walther@60262
|
688 |
dest_eq
|
walther@60262
|
689 |
0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True( **)
|
walther@60318
|
690 |
if UnparseC.term t = "x + 1 + - 1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
|
wneuper@59411
|
691 |
|
walther@60262
|
692 |
"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
|
walther@60262
|
693 |
"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
|
Walther@60477
|
694 |
(thy, 1, bool, []: Subst.T, rls, term);
|
walther@60262
|
695 |
(*deleted after error detection*)
|
walther@59841
|
696 |
|