walther@59841
|
1 |
(* Title: "ProgLang/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@60230
|
39 |
val t = (Thm.term_of o the) (TermC.parse thy "((r + u) + t) + s");
|
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');
|
akargl@42188
|
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@60262
|
91 |
val SOME (r,_) = (rewrite_ thy dummy_ord 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@60262
|
100 |
val SOME (r, _) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
|
neuper@37906
|
101 |
|
neuper@37906
|
102 |
"----- ordered rewriting";
|
wneuper@59462
|
103 |
fun tord (_:subst) pp = LibraryC.termless pp;
|
neuper@37906
|
104 |
if tord [] (@{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@60262
|
107 |
val NONE = (rewrite_ thy 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@60262
|
112 |
val SOME (r,_) = (rewrite_ thy 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@60262
|
153 |
val SOME (rew, asm) = (rewrite_ thy dummy_ord 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 ";
|
neuper@38022
|
161 |
"------Isabelle numerals, because erls 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@60262
|
169 |
val erls = eval_rls;
|
walther@60262
|
170 |
|
walther@60262
|
171 |
(**)val SOME (rew, asm) = (rewrite_ thy dummy_ord 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@60262
|
175 |
"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
|
walther@60262
|
176 |
(thy, dummy_ord, erls, false, thm, tm);
|
walther@60262
|
177 |
"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
|
walther@60262
|
178 |
(thy, 1, []: (term * term) list, rew_ord, erls, bool, thm, term);
|
walther@60262
|
179 |
|
walther@60262
|
180 |
(**) val (t', asms, _(*lrd*), rew) = rew_sub thy 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@60262
|
198 |
val _ = trace_in2 i "eval asms" thy r';
|
walther@60262
|
199 |
val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls;
|
walther@60262
|
200 |
(*if*) nofalse (*then*);
|
walther@60262
|
201 |
val (t'', p'') = (trace_in4 i "asms accepted" thy 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@59852
|
213 |
val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord 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@59852
|
217 |
(thy, 0, [], dummy_ord, 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
|
wneuper@59358
|
234 |
[Const ("HOL.Not", _) $ (Const ("HOL.eq", _)
|
wneuper@59358
|
235 |
$ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
|
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";
|
neuper@38025
|
247 |
val (thy, ord, erls, equs, t) =
|
walther@60230
|
248 |
(@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [TermC.str2term "x = 0"],
|
walther@60242
|
249 |
TermC.str2term "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";
|
wneuper@59395
|
253 |
rew_sub thy 1 [] ord erls 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@59851
|
257 |
val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
|
walther@60262
|
258 |
writeln "---------- rewrite_terms_ 1---------------------------";
|
walther@60242
|
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@60230
|
262 |
val equs = [TermC.str2term "M_b 0 = 0"];
|
walther@60242
|
263 |
val t = TermC.str2term "M_b 0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
|
walther@59851
|
264 |
val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
|
walther@60262
|
265 |
writeln "---------- rewrite_terms_ 2---------------------------";
|
walther@60242
|
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@60230
|
269 |
val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
|
walther@60242
|
270 |
val t = TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
|
walther@59851
|
271 |
val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
|
walther@60262
|
272 |
writeln "---------- rewrite_terms_ 3---------------------------";
|
walther@60242
|
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@60242
|
281 |
val t = TermC.str2term"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";
|
walther@60230
|
282 |
val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
|
walther@60230
|
283 |
(TermC.str2term"bdv_2",TermC.str2term"c_2"),
|
walther@60230
|
284 |
(TermC.str2term"bdv_3",TermC.str2term"c_3"),
|
walther@60230
|
285 |
(TermC.str2term"bdv_4",TermC.str2term"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@59878
|
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@59901
|
298 |
> Rewrite.trace_on:=true;
|
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@60230
|
320 |
val t = TermC.str2term "(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)];
|
neuper@38036
|
324 |
val erls = rational_erls;
|
neuper@38036
|
325 |
(* erls got from Rrls {erls, prepat, scr = 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";
|
neuper@38036
|
331 |
if ([], true) = eval__true thy 0 asms [] erls
|
neuper@38036
|
332 |
then () else error "rewrite.sml: prepat cancel eval__true";
|
neuper@38036
|
333 |
|
neuper@52105
|
334 |
"===== Rational.thy: add_fractions_p ===";
|
walther@60230
|
335 |
(* if each pat* TermC.matches with the current term, the Rrls is applied
|
neuper@48760
|
336 |
(there are no preconditions to be checked, they are @{term True}) *)
|
walther@60230
|
337 |
val t = TermC.str2term "a / b + 1 / 2";
|
walther@60230
|
338 |
val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";
|
neuper@48760
|
339 |
val pres = [@{term True}];
|
neuper@38036
|
340 |
val prepat = [(pres, pat)];
|
neuper@38036
|
341 |
val erls = rational_erls;
|
neuper@38036
|
342 |
(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
|
neuper@38036
|
343 |
|
neuper@38036
|
344 |
val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
|
neuper@38036
|
345 |
if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
|
neuper@52105
|
346 |
then () else error "rewrite.sml: prepat add_fractions_p";
|
neuper@38036
|
347 |
|
neuper@38036
|
348 |
"===== Poly.thy: order_mult_ ===";
|
neuper@38036
|
349 |
(* ?p matched with the current term gives an environment,
|
neuper@38036
|
350 |
which evaluates (the instantiated) "p is_multUnordered" to true*)
|
walther@60242
|
351 |
val t = TermC.str2term "x \<up> 2 * x";
|
walther@60230
|
352 |
val pat = TermC.parse_patt thy "?p :: real"
|
walther@60230
|
353 |
val pres = [TermC.parse_patt thy "?p is_multUnordered"];
|
neuper@38036
|
354 |
val prepat = [(pres, pat)];
|
walther@59852
|
355 |
val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
|
walther@59878
|
356 |
[Eval ("Poly.is'_multUnordered",
|
neuper@38036
|
357 |
eval_is_multUnordered "")];
|
neuper@38036
|
358 |
|
neuper@38036
|
359 |
val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
|
neuper@38036
|
360 |
val asms = map (Envir.subst_term subst) pres;
|
walther@60242
|
361 |
if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
|
neuper@38036
|
362 |
then () else error "rewrite.sml: prepat order_mult_ subst";
|
neuper@38036
|
363 |
if ([], true) = eval__true thy 0 asms [] erls
|
neuper@38036
|
364 |
then () else error "rewrite.sml: prepat order_mult_ eval__true";
|
neuper@38036
|
365 |
|
neuper@38036
|
366 |
|
walther@60262
|
367 |
"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
|
walther@60262
|
368 |
"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
|
walther@60262
|
369 |
"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
|
walther@60242
|
370 |
val t = TermC.str2term "x \<up> 2 * x";
|
neuper@41928
|
371 |
|
neuper@38039
|
372 |
if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
|
walther@60242
|
373 |
val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
|
neuper@41928
|
374 |
eval_is_multUnordered "testid" "" tm thy;
|
neuper@41928
|
375 |
|
neuper@38039
|
376 |
case eval_is_multUnordered "testid" "" tm thy of
|
neuper@41924
|
377 |
SOME (_, Const ("HOL.Trueprop", _) $
|
neuper@41922
|
378 |
(Const ("HOL.eq", _) $
|
neuper@38039
|
379 |
(Const ("Poly.is'_multUnordered", _) $ _) $
|
neuper@41928
|
380 |
Const ("HOL.True", _))) => ()
|
neuper@41928
|
381 |
| _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
|
neuper@38039
|
382 |
|
walther@60242
|
383 |
tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
|
neuper@38039
|
384 |
val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
|
walther@60242
|
385 |
tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
|
walther@60242
|
386 |
if UnparseC.term t' = "x * x \<up> 2" then ()
|
neuper@38039
|
387 |
else error "rewrite.sml Poly.is'_multUnordered doesn't work";
|
neuper@38039
|
388 |
|
neuper@38039
|
389 |
(* for achieving the previous result, the following code was taken apart *)
|
neuper@38039
|
390 |
"----- rewrite__set_ ---";
|
neuper@38039
|
391 |
val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
|
neuper@38039
|
392 |
val (t', asm, rew) = app_rev thy (i+1) rrls t;
|
neuper@38039
|
393 |
"----- app_rev ---";
|
neuper@38039
|
394 |
val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
|
neuper@38039
|
395 |
fun chk_prepat thy erls [] t = true
|
neuper@38039
|
396 |
| chk_prepat thy erls prepat t =
|
neuper@38039
|
397 |
let fun chk (pres, pat) =
|
neuper@38039
|
398 |
(let val subst: Type.tyenv * Envir.tenv =
|
neuper@38039
|
399 |
Pattern.match thy (pat, t)
|
neuper@38039
|
400 |
(Vartab.empty, Vartab.empty)
|
neuper@38039
|
401 |
in snd (eval__true thy (i+1)
|
neuper@38039
|
402 |
(map (Envir.subst_term subst) pres)
|
neuper@38039
|
403 |
[] erls)
|
neuper@38039
|
404 |
end)
|
neuper@38039
|
405 |
handle _ => false
|
neuper@38039
|
406 |
fun scan_ f [] = false (*scan_ NEVER called by []*)
|
neuper@38039
|
407 |
| scan_ f (pp::pps) = if f pp then true
|
neuper@38039
|
408 |
else scan_ f pps;
|
neuper@38039
|
409 |
in scan_ chk prepat end;
|
neuper@38039
|
410 |
|
neuper@38039
|
411 |
(*.apply the normal_form of a rev-set.*)
|
neuper@38039
|
412 |
fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
|
neuper@38039
|
413 |
if chk_prepat thy erls prepat t
|
walther@59868
|
414 |
then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)
|
neuper@38039
|
415 |
normal_form t)
|
neuper@38039
|
416 |
else NONE;
|
neuper@38039
|
417 |
(*fixme val NONE = app_rev' thy rrls t;*)
|
neuper@38039
|
418 |
"----- app_rev' ---";
|
neuper@38039
|
419 |
val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
|
neuper@38039
|
420 |
(*fixme false*) chk_prepat thy erls prepat t;
|
neuper@38039
|
421 |
"----- chk_prepat ---";
|
neuper@38039
|
422 |
val (thy, erls, prepat, t) = (thy, erls, prepat, t);
|
neuper@38039
|
423 |
fun chk (pres, pat) =
|
neuper@38039
|
424 |
(let val subst: Type.tyenv * Envir.tenv =
|
neuper@38039
|
425 |
Pattern.match thy (pat, t)
|
neuper@38039
|
426 |
(Vartab.empty, Vartab.empty)
|
neuper@38039
|
427 |
in snd (eval__true thy (i+1)
|
neuper@38039
|
428 |
(map (Envir.subst_term subst) pres)
|
neuper@38039
|
429 |
[] erls)
|
neuper@38039
|
430 |
end)
|
neuper@38039
|
431 |
handle _ => false;
|
neuper@38039
|
432 |
fun scan_ f [] = false (*scan_ NEVER called by []*)
|
neuper@38039
|
433 |
| scan_ f (pp::pps) = if f pp then true
|
neuper@38039
|
434 |
else scan_ f pps;
|
neuper@38039
|
435 |
tracing "=== poly.sml: scan_ chk prepat begin";
|
neuper@38039
|
436 |
scan_ chk prepat;
|
neuper@38039
|
437 |
tracing "=== poly.sml: scan_ chk prepat end";
|
neuper@38039
|
438 |
|
neuper@38039
|
439 |
"----- chk ---";
|
walther@60242
|
440 |
(*reestablish...*) val t = TermC.str2term "x \<up> 2 * x";
|
neuper@38039
|
441 |
val [(pres, pat)] = prepat;
|
neuper@38039
|
442 |
val subst: Type.tyenv * Envir.tenv =
|
neuper@38039
|
443 |
Pattern.match thy (pat, t)
|
neuper@38039
|
444 |
(Vartab.empty, Vartab.empty);
|
neuper@38039
|
445 |
|
neuper@38039
|
446 |
(*fixme: asms = ["p is_multUnordered"]...instantiate*)
|
neuper@38039
|
447 |
"----- eval__true ---";
|
neuper@38039
|
448 |
val asms = (map (Envir.subst_term subst) pres);
|
walther@60242
|
449 |
if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then ()
|
neuper@38039
|
450 |
else error "rewrite.sml: diff. is_multUnordered, asms";
|
neuper@38039
|
451 |
val (thy, i, asms, bdv, rls) =
|
walther@60242
|
452 |
(thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"],
|
neuper@38039
|
453 |
[] : (term * term) list, erls);
|
neuper@38039
|
454 |
case eval__true thy i asms bdv rls of
|
neuper@38039
|
455 |
([], true) => ()
|
neuper@38039
|
456 |
| _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
|
neuper@42223
|
457 |
|
walther@60262
|
458 |
"----------- 2011 thms with axclasses ----------------------------------------------------------";
|
walther@60262
|
459 |
"----------- 2011 thms with axclasses ----------------------------------------------------------";
|
walther@60262
|
460 |
"----------- 2011 thms with axclasses ----------------------------------------------------------";
|
walther@59871
|
461 |
val thm = ThmC.numerals_to_Free @{thm div_by_1};
|
wneuper@59188
|
462 |
val prop = Thm.prop_of thm;
|
walther@60230
|
463 |
TermC.atomty prop; (*Type 'a*)
|
walther@60230
|
464 |
val t = TermC.str2term "(2*x)/1"; (*Type real*)
|
neuper@42223
|
465 |
|
neuper@42223
|
466 |
val (thy, ro, er, inst) =
|
wneuper@59592
|
467 |
(@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
|
walther@60230
|
468 |
val SOME (t, _) = rewrite_ thy ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)
|
neuper@42223
|
469 |
|
walther@59841
|
470 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
walther@59841
|
471 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
walther@59841
|
472 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
walther@59841
|
473 |
val thy = @{theory RatEq};
|
walther@59841
|
474 |
val ctxt = Proof_Context.init_global thy;
|
walther@60242
|
475 |
val SOME t = parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
|
walther@59841
|
476 |
val rls = assoc_rls "RatEq_eliminate"
|
neuper@42394
|
477 |
|
walther@59841
|
478 |
val SOME (t''''', asm''''') =
|
walther@59841
|
479 |
rewrite_set_ thy true rls t;
|
walther@59841
|
480 |
"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
|
walther@59841
|
481 |
rewrite__set_ thy 1 bool [] rls term;
|
walther@59841
|
482 |
"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
|
walther@59841
|
483 |
= (thy, 1, bool, []:(term * term) list, rls, term);
|
walther@59841
|
484 |
|
walther@59841
|
485 |
(*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
|
walther@59920
|
486 |
datatype switch = Applicable.Yes | Noap;
|
walther@59841
|
487 |
fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
|
walther@59920
|
488 |
| rew_once ruls asm ct Applicable.Yes [] =
|
walther@59851
|
489 |
(case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
|
walther@59878
|
490 |
| Rule_Set.Sequence _ => (ct, asm)
|
walther@59867
|
491 |
| rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
|
walther@59841
|
492 |
| rew_once ruls asm ct apno (rul :: thms) =
|
walther@59841
|
493 |
case rul of
|
walther@59841
|
494 |
Rule.Thm (thmid, thm) =>
|
walther@59841
|
495 |
(trace1 i (" try thm: " ^ thmid);
|
walther@59852
|
496 |
case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
|
walther@59852
|
497 |
((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
|
walther@59841
|
498 |
NONE => rew_once ruls asm ct apno thms
|
walther@59841
|
499 |
| SOME (ct', asm') =>
|
walther@59870
|
500 |
(trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
|
walther@59920
|
501 |
rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms)))
|
walther@59841
|
502 |
(* once again try the same rule, e.g. associativity against "()"*)
|
walther@59878
|
503 |
| Rule.Eval (cc as (op_, _)) =>
|
walther@59841
|
504 |
let val _= trace1 i (" try calc: " ^ op_ ^ "'")
|
walther@59841
|
505 |
val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
|
walther@59878
|
506 |
in case Eval.adhoc_thm thy cc ct of
|
walther@59841
|
507 |
NONE => rew_once ruls asm ct apno thms
|
walther@59841
|
508 |
| SOME (_, thm') =>
|
walther@59841
|
509 |
let
|
walther@59852
|
510 |
val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
|
walther@59852
|
511 |
((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
|
walther@59841
|
512 |
val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
|
walther@59875
|
513 |
ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
|
walther@59870
|
514 |
val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
|
walther@59920
|
515 |
in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end
|
walther@59841
|
516 |
end
|
walther@59841
|
517 |
| Rule.Cal1 (cc as (op_, _)) =>
|
walther@59841
|
518 |
let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
|
walther@59841
|
519 |
val ct = TermC.uminus_to_string ct
|
walther@59878
|
520 |
in case Eval.adhoc_thm1_ thy cc ct of
|
walther@59841
|
521 |
NONE => (ct, asm)
|
walther@59841
|
522 |
| SOME (_, thm') =>
|
walther@59841
|
523 |
let
|
walther@59852
|
524 |
val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
|
walther@59852
|
525 |
((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
|
walther@59841
|
526 |
val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
|
walther@59875
|
527 |
ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
|
walther@59870
|
528 |
val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
|
walther@59841
|
529 |
in the pairopt end
|
walther@59841
|
530 |
end
|
walther@59841
|
531 |
| Rule.Rls_ rls' =>
|
walther@59841
|
532 |
(case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
|
walther@59920
|
533 |
SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms
|
walther@59841
|
534 |
| NONE => rew_once ruls asm ct apno thms)
|
walther@59867
|
535 |
| r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
|
walther@59852
|
536 |
val ruls = (#rules o Rule.Rule_Set.rep) rls;
|
walther@59870
|
537 |
(* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)*)
|
walther@59841
|
538 |
val (ct', asm') = rew_once ruls [] ct Noap ruls;
|
walther@59841
|
539 |
"~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
|
walther@59841
|
540 |
= (ruls, []:term list, ct, Noap, ruls);
|
walther@59841
|
541 |
val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
|
walther@59841
|
542 |
|
walther@59841
|
543 |
val SOME (ct', asm') = (*case*)
|
walther@59852
|
544 |
rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
|
walther@59852
|
545 |
((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
|
walther@59841
|
546 |
"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
|
walther@59852
|
547 |
= (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
|
walther@59852
|
548 |
((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
|
walther@59841
|
549 |
|
walther@59841
|
550 |
val (t', asms, _ (*lrd*), rew) =
|
walther@59841
|
551 |
rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
|
wenzelm@60203
|
552 |
(((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm) ct;
|
walther@59841
|
553 |
"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
|
walther@59841
|
554 |
= (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
|
wenzelm@60203
|
555 |
(((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct);
|
walther@59841
|
556 |
val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
|
walther@59841
|
557 |
val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
|
walther@59841
|
558 |
;
|
walther@59868
|
559 |
(*+*)if UnparseC.term r' =
|
walther@60242
|
560 |
(*+*) "\<lbrakk>9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
|
walther@60242
|
561 |
(*+*) "\<Longrightarrow> ((3 + -1 * x + x \<up> 2) /\n" ^
|
walther@60242
|
562 |
(*+*) " (9 * x + -6 * x \<up> 2 + x \<up> 3) =\n" ^
|
walther@59841
|
563 |
(*+*) " 1 / x) =\n" ^
|
walther@60242
|
564 |
(*+*) " ((3 + -1 * x + x \<up> 2) * x =\n" ^
|
walther@60242
|
565 |
(*+*) " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3))"
|
walther@59841
|
566 |
(*+*)then () else error "instantiated rule CHANGED";
|
walther@59841
|
567 |
|
walther@59841
|
568 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
|
walther@59841
|
569 |
;
|
walther@60242
|
570 |
(*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
|
walther@59841
|
571 |
(*+*)then () else error "stored assumptions CHANGED";
|
walther@59841
|
572 |
|
walther@59841
|
573 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
|
walther@59841
|
574 |
;
|
walther@60242
|
575 |
(*+*)if UnparseC.term t' = "(3 + -1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)"
|
walther@59841
|
576 |
(*+*)then () else error "rewritten term (an equality) CHANGED";
|
walther@59841
|
577 |
|
walther@59841
|
578 |
val (simpl_p', nofalse) =
|
walther@59841
|
579 |
eval__true thy (i + 1) p' bdv rls;
|
walther@59841
|
580 |
"~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
|
walther@59841
|
581 |
(*if*) asms = [@{term True}] orelse asms = [] (*else*);
|
walther@59841
|
582 |
|
walther@60242
|
583 |
(*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
|
walther@59841
|
584 |
(*+*)then () else error "asms before chk CHANGED";
|
walther@59841
|
585 |
|
walther@59841
|
586 |
fun chk indets [] = (indets, true) (*return asms<>True until false*)
|
walther@59841
|
587 |
| chk indets (a :: asms) =
|
walther@59841
|
588 |
(case rewrite__set_ thy (i + 1) false bdv rls a of
|
walther@59841
|
589 |
NONE => (chk (indets @ [a]) asms)
|
walther@59841
|
590 |
| SOME (t, a') =>
|
walther@59841
|
591 |
if t = @{term True} then (chk (indets @ a') asms)
|
walther@59841
|
592 |
else if t = @{term False} then ([], false)
|
walther@60242
|
593 |
(*asm false .. thm not applied \<up> ; continue until False vvv*)
|
walther@59841
|
594 |
else chk (indets @ [t] @ a') asms);
|
walther@59841
|
595 |
|
walther@59841
|
596 |
val (xxx, true) =
|
walther@59841
|
597 |
chk [] asms; (*return from eval__true*);
|
walther@59841
|
598 |
"~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
|
walther@59841
|
599 |
|
walther@59851
|
600 |
(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
|
walther@59841
|
601 |
(*+*)(*val rules =
|
walther@59878
|
602 |
(*+*) [Eval ("Rings.divide_class.divide", fn),
|
walther@59841
|
603 |
(*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
|
walther@59841
|
604 |
(*+*) :
|
walther@59878
|
605 |
(*+*) Eval ("HOL.eq", fn),
|
walther@59841
|
606 |
(*+*) Thm ("not_true", "(\<not> True) = False"),
|
walther@59841
|
607 |
(*+*) Thm ("not_false", "(\<not> False) = True"),
|
walther@59841
|
608 |
(*+*) :
|
walther@59878
|
609 |
(*+*) Eval ("Prog_Expr.pow", fn),
|
walther@59878
|
610 |
(*+*) Eval ("RatEq.is'_ratequation'_in", fn)]:
|
walther@59841
|
611 |
(*+*) rule list*)
|
walther@59841
|
612 |
(*+*)chk: term list -> term list -> term list * bool
|
walther@59841
|
613 |
|
walther@59841
|
614 |
rewrite__set_ thy (i + 1) false bdv rls a (*of*);
|
walther@59841
|
615 |
|
walther@59901
|
616 |
(*+*)Rewrite.trace_on := true;
|
walther@59841
|
617 |
|
walther@59841
|
618 |
(*this was False; vvvv--- means: indeterminate*)
|
walther@59841
|
619 |
val (* SOME (t, a') *)NONE = (*case*)
|
walther@59841
|
620 |
rewrite__set_ thy (i + 1) false bdv rls a (*of*);
|
walther@59841
|
621 |
|
walther@59868
|
622 |
(*+*)UnparseC.term a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
|
neuper@42394
|
623 |
(*
|
neuper@42394
|
624 |
:
|
walther@59841
|
625 |
#### rls: rateq_erls on: x \<noteq> 0
|
neuper@42394
|
626 |
:
|
neuper@42394
|
627 |
##### try calc: HOL.eq' <<<------------------------------- here the error comes from
|
walther@59841
|
628 |
===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
|
neuper@42394
|
629 |
##### try calc: HOL.eq'
|
neuper@42394
|
630 |
##### try thm: not_true
|
neuper@42394
|
631 |
##### try thm: not_false
|
walther@59841
|
632 |
===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
|
walther@59841
|
633 |
and True, False are NOT stored ...
|
walther@59841
|
634 |
:
|
walther@59841
|
635 |
### asms accepted: [x \<noteq> 0] stored: []
|
walther@59841
|
636 |
: *)
|
walther@59901
|
637 |
Rewrite.trace_on := false;
|
walther@59841
|
638 |
( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
|
walther@59841
|
639 |
|
neuper@42394
|
640 |
|
wneuper@59252
|
641 |
"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
|
wneuper@59252
|
642 |
"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
|
wneuper@59252
|
643 |
"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
|
wneuper@59252
|
644 |
"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
|
walther@59852
|
645 |
(@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
|
wneuper@59252
|
646 |
"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
|
wneuper@59252
|
647 |
(thy, 1, [], rew_ord, erls, bool, thm, term);
|
wneuper@59252
|
648 |
"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
|
walther@60230
|
649 |
(thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)
|
walther@60262
|
650 |
val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r
|
wneuper@59252
|
651 |
val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
|
wneuper@59252
|
652 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
|
walther@60262
|
653 |
val t' = (snd o HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r'
|
wneuper@59252
|
654 |
;
|
walther@59868
|
655 |
if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()
|
wneuper@59252
|
656 |
else error "ARGS FOR Pattern.match CHANGED";
|
wneuper@59252
|
657 |
val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
|
walther@59868
|
658 |
if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
|
wneuper@59252
|
659 |
else error "Pattern.match CHANGED";
|
wneuper@59381
|
660 |
|
walther@60262
|
661 |
"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
|
walther@60262
|
662 |
"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
|
walther@60262
|
663 |
"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
|
wneuper@59411
|
664 |
(* norm_equation is defined in Test.thy, other rls see Knowledg/**)
|
wneuper@59411
|
665 |
val thy = @{theory};
|
wneuper@59411
|
666 |
val rls = norm_equation;
|
walther@60230
|
667 |
val term = TermC.str2term "x + 1 = 2";
|
wneuper@59411
|
668 |
|
walther@60262
|
669 |
(**)val SOME (t, asm) = rewrite_set_ thy false rls term;
|
walther@60262
|
670 |
(** )##### try thm: "root_ge0"
|
walther@60262
|
671 |
exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):
|
walther@60262
|
672 |
dest_eq
|
walther@60262
|
673 |
0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True( **)
|
walther@59868
|
674 |
if UnparseC.term t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
|
wneuper@59411
|
675 |
|
walther@60262
|
676 |
"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
|
walther@60262
|
677 |
"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
|
walther@60262
|
678 |
(thy, 1, bool, []: (term * term) list, rls, term);
|
walther@60262
|
679 |
(*deleted after error detection*)
|
walther@59841
|
680 |
|