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 |
|
neuper@38022
|
6 |
"--------------------------------------------------------";
|
neuper@38022
|
7 |
"table of contents --------------------------------------";
|
neuper@38022
|
8 |
"--------------------------------------------------------";
|
neuper@38022
|
9 |
"----------- assemble rewrite ---------------------------";
|
wneuper@59382
|
10 |
"----------- test rewriting without Isac session --------";
|
wneuper@59382
|
11 |
"----------- conditional rewriting without Isac session -";
|
neuper@38022
|
12 |
"----------- step through 'and rew_sub': ----------------";
|
neuper@38025
|
13 |
"----------- step through 'fun rewrite_terms_' ---------";
|
neuper@38022
|
14 |
"----------- rewrite_inst_ bdvs -------------------------";
|
neuper@38022
|
15 |
"----------- check diff 2002--2009-3 --------------------";
|
neuper@38039
|
16 |
"----------- compare all prepat's existing 2010 ---------";
|
neuper@38039
|
17 |
"----------- fun app_rev, Rrls, -------------------------";
|
neuper@42223
|
18 |
"----------- 2011 thms with axclasses -------------------";
|
walther@59841
|
19 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
wneuper@59110
|
20 |
"----------- fun assoc_thm' -----------------------------";
|
wneuper@59252
|
21 |
"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
|
wneuper@59381
|
22 |
"----------- fun mk_thm ------------------------------------------------------------------------";
|
wneuper@59411
|
23 |
"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
|
walther@59841
|
24 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
neuper@38022
|
25 |
"--------------------------------------------------------";
|
neuper@38022
|
26 |
"--------------------------------------------------------";
|
neuper@38022
|
27 |
"--------------------------------------------------------";
|
neuper@37906
|
28 |
|
neuper@38036
|
29 |
|
neuper@38022
|
30 |
"----------- assemble rewrite ---------------------------";
|
neuper@38022
|
31 |
"----------- assemble rewrite ---------------------------";
|
neuper@38022
|
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};
|
wneuper@59188
|
39 |
val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s");
|
neuper@37906
|
40 |
"----- from old: fun rewrite__";
|
neuper@37906
|
41 |
val bdv = [];
|
wneuper@59188
|
42 |
val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) 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 |
|
neuper@38022
|
81 |
"----------- test rewriting without Isac's thys ---------";
|
neuper@38022
|
82 |
"----------- test rewriting without Isac's thys ---------";
|
neuper@38022
|
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 |
|
neuper@37906
|
91 |
val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
|
neuper@38022
|
92 |
handle _ => error "rewrite.sml diff.behav. in rewriting";
|
neuper@37906
|
93 |
(*is displayed on _TOP_ of <response> buffer...*)
|
neuper@48761
|
94 |
Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
|
neuper@38022
|
95 |
if r = @{term "y*z + x::real"}
|
neuper@38022
|
96 |
then () else error "rewrite.sml diff.result in rewriting";
|
neuper@37906
|
97 |
|
neuper@37906
|
98 |
"----- rewriting a subterm";
|
neuper@37906
|
99 |
val tm = @{term "w*(x + y*z)::real"};
|
neuper@37906
|
100 |
|
neuper@37906
|
101 |
val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
|
neuper@38022
|
102 |
handle _ => error "rewrite.sml diff.behav. in rew_sub";
|
neuper@37906
|
103 |
|
neuper@37906
|
104 |
"----- ordered rewriting";
|
wneuper@59462
|
105 |
fun tord (_:subst) pp = LibraryC.termless pp;
|
neuper@37906
|
106 |
if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
|
neuper@38022
|
107 |
else error "rewrite.sml diff.behav. in ord.rewr.";
|
neuper@37906
|
108 |
|
neuper@37906
|
109 |
val NONE = (rewrite_ thy tord e_rls false thm tm)
|
neuper@38022
|
110 |
handle _ => error "rewrite.sml diff.behav. in rewriting";
|
neuper@37906
|
111 |
(*is displayed on _TOP_ of <response> buffer...*)
|
neuper@48761
|
112 |
Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
|
neuper@37906
|
113 |
|
neuper@37906
|
114 |
val tm = @{term "x*y + z::real"};
|
neuper@37906
|
115 |
val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
|
neuper@38022
|
116 |
handle _ => error "rewrite.sml diff.behav. in rewriting";
|
neuper@37906
|
117 |
|
neuper@37906
|
118 |
|
neuper@38022
|
119 |
"----------- conditional rewriting without Isac's thys --";
|
neuper@38022
|
120 |
"----------- conditional rewriting without Isac's thys --";
|
neuper@38022
|
121 |
"----------- conditional rewriting without Isac's thys --";
|
akargl@42224
|
122 |
|
neuper@37906
|
123 |
"===== prepr cond.rew. with Pattern.match";
|
neuper@37906
|
124 |
val thy = @{theory Complex_Main};
|
neuper@37906
|
125 |
val ctxt = @{context};
|
wneuper@59358
|
126 |
val thm = @{thm nonzero_divide_mult_cancel_right};
|
neuper@37906
|
127 |
val rule = Thm.prop_of thm;
|
wneuper@59358
|
128 |
val tm = @{term "x / (2 * x)::real"};
|
neuper@37906
|
129 |
|
neuper@37906
|
130 |
val prem = Logic.strip_imp_prems rule;
|
neuper@37906
|
131 |
val nps = Logic.count_prems rule;
|
neuper@37906
|
132 |
val prems = Logic.strip_prems (nps, [], rule);
|
neuper@37906
|
133 |
|
neuper@37906
|
134 |
val eq = Logic.strip_imp_concl rule;
|
neuper@41942
|
135 |
val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
|
neuper@37906
|
136 |
|
neuper@41942
|
137 |
val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
|
neuper@37906
|
138 |
val rule' = Envir.subst_term mtcs rule;
|
neuper@37906
|
139 |
|
neuper@37906
|
140 |
val prems' = (fst o Logic.strip_prems)
|
neuper@37906
|
141 |
(Logic.count_prems rule', [], rule');
|
neuper@41942
|
142 |
val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
|
neuper@37906
|
143 |
o Logic.strip_imp_concl) rule';
|
neuper@37906
|
144 |
|
neuper@37906
|
145 |
"----- conditional rewriting creating an assumption";
|
neuper@37906
|
146 |
"----- conditional rewriting creating an assumption";
|
wneuper@59358
|
147 |
val thm = @{thm nonzero_divide_mult_cancel_right};
|
wneuper@59358
|
148 |
val tm = @{term "x / (2 * x)::real"};
|
neuper@38022
|
149 |
val SOME (rew, asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
|
neuper@38022
|
150 |
handle _ => error "rewrite.sml diff.behav. in cond.rew.";
|
neuper@37906
|
151 |
|
wneuper@59358
|
152 |
if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
|
neuper@38022
|
153 |
else error "rewrite.sml diff.result in cond.rew.";
|
neuper@37906
|
154 |
|
wneuper@59358
|
155 |
if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
|
neuper@38022
|
156 |
then () else error "rewrite.sml diff.asm in cond.rew.";
|
neuper@38022
|
157 |
"----- conditional rewriting immediately: can only be done with ";
|
neuper@38022
|
158 |
"------Isabelle numerals, because erls cannot handle them yet.";
|
neuper@37906
|
159 |
|
neuper@37906
|
160 |
|
neuper@38022
|
161 |
"----------- step through 'and rew_sub': ----------------";
|
neuper@38022
|
162 |
"----------- step through 'and rew_sub': ----------------";
|
neuper@38022
|
163 |
"----------- step through 'and rew_sub': ----------------";
|
neuper@38022
|
164 |
(*and make asms without Trueprop, beginning with the result:*)
|
wneuper@59358
|
165 |
val tm = @{term "x / (2 * x)::real"};
|
wneuper@59188
|
166 |
val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (Thm.prop_of thm) tm;
|
neuper@41924
|
167 |
(*show_types := false;*)
|
neuper@38022
|
168 |
"----- evaluate arguments";
|
neuper@38022
|
169 |
val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
|
wneuper@59188
|
170 |
(thy, 0, [], dummy_ord, e_rls, true, [], (Thm.prop_of thm), tm);
|
neuper@41942
|
171 |
"----- step 1: LHS, RHS of rule";
|
neuper@41942
|
172 |
val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
|
neuper@38022
|
173 |
o Logic.strip_imp_concl) r;
|
wneuper@59358
|
174 |
term2str r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
|
wneuper@59358
|
175 |
term2str LHS = "?b / (?a * ?b)"; term2str RHS = "(1::?'a) / ?a";
|
neuper@38022
|
176 |
"----- step 2: the rule instantiated";
|
neuper@38025
|
177 |
val r' = Envir.subst_term
|
neuper@41942
|
178 |
(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
|
wneuper@59358
|
179 |
term2str r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
|
neuper@38022
|
180 |
"----- step 3: get the (instantiated) assumption(s)";
|
neuper@38022
|
181 |
val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
|
wneuper@59358
|
182 |
term2str (hd p') = "x \<noteq> 0";
|
neuper@38022
|
183 |
"=====vvv make asms without Trueprop ---vvv";
|
neuper@38022
|
184 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
|
neuper@38022
|
185 |
(Logic.count_prems r', [], r'));
|
neuper@38022
|
186 |
case p' of
|
wneuper@59358
|
187 |
[Const ("HOL.Not", _) $ (Const ("HOL.eq", _)
|
wneuper@59358
|
188 |
$ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
|
neuper@38022
|
189 |
| _ => error "rewrite.sml assumption changed";
|
neuper@38022
|
190 |
"=====^^^ make asms without Trueprop ---^^^";
|
neuper@41942
|
191 |
"----- step 4: get the (instantiated) RHS";
|
neuper@38022
|
192 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
|
neuper@38022
|
193 |
o Logic.strip_imp_concl) r';
|
wneuper@59358
|
194 |
term2str t' = "1 / 2";
|
neuper@37906
|
195 |
|
neuper@38025
|
196 |
"----------- step through 'fun rewrite_terms_' ---------";
|
neuper@38025
|
197 |
"----------- step through 'fun rewrite_terms_' ---------";
|
neuper@38025
|
198 |
"----------- step through 'fun rewrite_terms_' ---------";
|
neuper@38025
|
199 |
"----- step 0: args for rewrite_terms_, local fun";
|
neuper@38025
|
200 |
val (thy, ord, erls, equs, t) =
|
walther@59851
|
201 |
(@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [str2term "x = 0"],
|
neuper@38025
|
202 |
str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
|
neuper@38025
|
203 |
"----- step 1: args for rew_";
|
neuper@38025
|
204 |
val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
|
neuper@38025
|
205 |
"----- step 2: rew_sub";
|
wneuper@59395
|
206 |
rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
|
neuper@38025
|
207 |
"----- step 3: step through rew_sub -- inefficient: goes into subterms";
|
neuper@38025
|
208 |
|
neuper@38025
|
209 |
|
walther@59851
|
210 |
val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
|
neuper@38025
|
211 |
writeln "----------- rewrite_terms_ 1---------------------------";
|
neuper@37906
|
212 |
if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
|
neuper@38031
|
213 |
else error "rewrite.sml rewrite_terms_ [x = 0]";
|
neuper@37906
|
214 |
|
neuper@38025
|
215 |
val equs = [str2term "M_b 0 = 0"];
|
neuper@38025
|
216 |
val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
|
walther@59851
|
217 |
val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
|
neuper@38025
|
218 |
writeln "----------- rewrite_terms_ 2---------------------------";
|
neuper@37906
|
219 |
if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
|
neuper@38031
|
220 |
else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
|
neuper@37906
|
221 |
|
neuper@38025
|
222 |
val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
|
neuper@38025
|
223 |
val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
|
walther@59851
|
224 |
val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
|
neuper@38025
|
225 |
writeln "----------- rewrite_terms_ 3---------------------------";
|
neuper@37906
|
226 |
if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
|
neuper@38031
|
227 |
else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
|
neuper@37906
|
228 |
|
neuper@37906
|
229 |
|
neuper@38022
|
230 |
"----------- rewrite_inst_ bdvs -------------------------";
|
neuper@38022
|
231 |
"----------- rewrite_inst_ bdvs -------------------------";
|
neuper@38022
|
232 |
"----------- rewrite_inst_ bdvs -------------------------";
|
neuper@37906
|
233 |
(*see smltest/Scripts/term_G.sml: inst_bdv 2*)
|
neuper@37906
|
234 |
val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
|
neuper@37906
|
235 |
val bdvs = [(str2term"bdv_1",str2term"c"),
|
neuper@37906
|
236 |
(str2term"bdv_2",str2term"c_2"),
|
neuper@37906
|
237 |
(str2term"bdv_3",str2term"c_3"),
|
neuper@37906
|
238 |
(str2term"bdv_4",str2term"c_4")];
|
neuper@37906
|
239 |
(*------------ outcommented WN071210, after inclusion into ROOT.ML
|
neuper@37926
|
240 |
val SOME (t,_) =
|
neuper@37906
|
241 |
rewrite_inst_ thy e_rew_ord
|
neuper@37906
|
242 |
(append_rls "erls_isolate_bdvs" e_rls
|
walther@59773
|
243 |
[(Num_Calc ("EqSystem.occur'_exactly'_in",
|
neuper@37906
|
244 |
eval_occur_exactly_in
|
neuper@37906
|
245 |
"#eval_occur_exactly_in_"))
|
neuper@37906
|
246 |
])
|
neuper@37967
|
247 |
false bdvs (num_str @{separate_bdvs_add) t;
|
neuper@37906
|
248 |
(writeln o term2str) t;
|
neuper@37906
|
249 |
if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
|
neuper@38031
|
250 |
then () else error "rewrite.sml rewrite_inst_ bdvs";
|
walther@59627
|
251 |
> trace_rewrite:=true;
|
neuper@37906
|
252 |
trace_rewrite:=false;--------------------------------------------*)
|
neuper@37906
|
253 |
|
neuper@38025
|
254 |
|
neuper@38022
|
255 |
"----------- check diff 2002--2009-3 --------------------";
|
neuper@38022
|
256 |
"----------- check diff 2002--2009-3 --------------------";
|
neuper@38022
|
257 |
"----------- check diff 2002--2009-3 --------------------";
|
neuper@38022
|
258 |
(*----- 2002 -------------------------------------------------------------------
|
neuper@38022
|
259 |
# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
|
neuper@38022
|
260 |
q_0 * x ^^^ 2 / 2)
|
neuper@38022
|
261 |
## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
|
neuper@38022
|
262 |
/ 2)
|
neuper@38022
|
263 |
### try thm: real_diff_minus
|
neuper@38022
|
264 |
### try thm: sym_real_mult_minus1
|
neuper@38022
|
265 |
## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
|
neuper@38022
|
266 |
/ 2)
|
neuper@38022
|
267 |
### try thm: rat_mult_poly_l
|
neuper@38022
|
268 |
### try thm: rat_mult_poly_r
|
neuper@38022
|
269 |
#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
|
neuper@38022
|
270 |
==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
|
neuper@38022
|
271 |
1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
|
neuper@38022
|
272 |
##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
|
neuper@38022
|
273 |
is_polyexp
|
neuper@38022
|
274 |
###### try calc: Poly.is'_polyexp'
|
neuper@38022
|
275 |
====== calc. to: False
|
neuper@38022
|
276 |
###### try calc: Poly.is'_polyexp'
|
neuper@38022
|
277 |
###### try calc: Poly.is'_polyexp'
|
neuper@38022
|
278 |
#### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
|
neuper@38022
|
279 |
----- 2002 NONE rewrite --------------------------------------------------------
|
neuper@38022
|
280 |
----- 2009 should maintain this behaviour, but: --------------------------------
|
neuper@38022
|
281 |
# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
|
neuper@38022
|
282 |
## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
|
neuper@38022
|
283 |
### try thm: real_diff_minus
|
neuper@38022
|
284 |
### try thm: sym_real_mult_minus1
|
neuper@38022
|
285 |
## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
|
neuper@38022
|
286 |
### try thm: rat_mult_poly_l
|
neuper@38022
|
287 |
### try thm: rat_mult_poly_r
|
neuper@38022
|
288 |
#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
|
neuper@38022
|
289 |
==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
|
neuper@38022
|
290 |
1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
|
neuper@38022
|
291 |
##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
|
neuper@38022
|
292 |
###### try calc: Poly.is'_polyexp'
|
neuper@38022
|
293 |
====== calc. to: False
|
neuper@38022
|
294 |
###### try calc: Poly.is'_polyexp'
|
neuper@38022
|
295 |
###### try calc: Poly.is'_polyexp'
|
neuper@38022
|
296 |
#### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
|
neuper@38022
|
297 |
=== rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
|
neuper@38022
|
298 |
----- 2009 -------------------------------------------------------------------*)
|
neuper@38022
|
299 |
|
neuper@38022
|
300 |
(*the situation as was before repair (asm without Trueprop) is outcommented*)
|
wneuper@59592
|
301 |
val thy = @{theory "Isac_Knowledge"};
|
neuper@38022
|
302 |
"===== example which raised the problem =================";
|
neuper@38022
|
303 |
val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
|
neuper@38022
|
304 |
"----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
|
wneuper@59382
|
305 |
val subs = [(@{term "bdv"}, @{term "x"})];
|
neuper@38022
|
306 |
val rls = norm_Rational_noadd_fractions;
|
wneuper@59112
|
307 |
val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
|
wneuper@59529
|
308 |
if term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x ^^^ 2 / 2)" andalso
|
wneuper@59112
|
309 |
terms2str asms = "[]" then {}
|
wneuper@59112
|
310 |
else error "this was NONE with Isabelle2013-2 ?!?"
|
neuper@38022
|
311 |
"----- rewrite_ rat_mult_poly_r--------------------------";
|
neuper@38022
|
312 |
val thm = @{thm rat_mult_poly_r};
|
neuper@38022
|
313 |
"?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
|
neuper@38022
|
314 |
val erls = append_rls "e_rls-is_polyexp" e_rls
|
walther@59773
|
315 |
[Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
|
neuper@38022
|
316 |
val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
|
neuper@38022
|
317 |
(*t' = t''; (*false because of further rewrites in t'*)*)
|
neuper@38022
|
318 |
"----- rew_sub --------------------------------";
|
wneuper@59188
|
319 |
val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
|
neuper@38022
|
320 |
(*t'' = t'''; (*true*)*)
|
neuper@38022
|
321 |
"----- rewrite_set_ erls --------------------------------";
|
neuper@38022
|
322 |
val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
|
neuper@38022
|
323 |
val NONE = rewrite_set_ thy true erls cond;
|
neuper@38022
|
324 |
(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
|
neuper@38022
|
325 |
|
neuper@38022
|
326 |
writeln "===== maximally simplified example =====================";
|
neuper@38022
|
327 |
val t = @{term "a / b * (x / x ^^^ 2)"};
|
neuper@38022
|
328 |
"?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
|
neuper@38022
|
329 |
writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
|
neuper@38022
|
330 |
val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
|
neuper@38022
|
331 |
term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
|
neuper@38022
|
332 |
(*checked visually: trace_rewrite looks like above for 2009*)
|
neuper@38022
|
333 |
|
neuper@38022
|
334 |
writeln "----- rewrite_ rat_mult_poly_r--------------------------";
|
neuper@38022
|
335 |
val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
|
neuper@38022
|
336 |
(*t' = t''; (*false because of further rewrites in t'*)*)
|
neuper@38022
|
337 |
writeln "----- rew_sub --------------------------------";
|
wneuper@59188
|
338 |
val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
|
neuper@38022
|
339 |
(*t'' = t'''; (*true*)*)
|
neuper@38022
|
340 |
writeln "----- rewrite_set_ erls --------------------------------";
|
neuper@38022
|
341 |
val cond = @{term "(x / x ^^^ 2)"};
|
neuper@38022
|
342 |
val NONE = rewrite_set_ thy true erls cond;
|
neuper@38022
|
343 |
(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
|
neuper@42201
|
344 |
|
neuper@38025
|
345 |
|
neuper@38039
|
346 |
"----------- compare all prepat's existing 2010 ---------";
|
neuper@38039
|
347 |
"----------- compare all prepat's existing 2010 ---------";
|
neuper@38039
|
348 |
"----------- compare all prepat's existing 2010 ---------";
|
wneuper@59592
|
349 |
val thy = @{theory "Isac_Knowledge"};
|
neuper@38036
|
350 |
val t = @{term "a + b * x = (0 ::real)"};
|
neuper@38036
|
351 |
val pat = parse_patt thy "?l = (?r ::real)";
|
neuper@38036
|
352 |
val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
|
neuper@38039
|
353 |
val precond = parse_patt thy "(?l::real) is_expanded";
|
neuper@38036
|
354 |
|
neuper@38036
|
355 |
val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
|
neuper@38036
|
356 |
val preinst = Envir.subst_term inst precond;
|
neuper@38036
|
357 |
term2str preinst;
|
neuper@38036
|
358 |
|
neuper@38036
|
359 |
"===== Rational.thy: cancel ===";
|
neuper@38036
|
360 |
(* pat matched with the current term gives an environment
|
neuper@38036
|
361 |
(or not: hen the Rrls not applied);
|
neuper@48760
|
362 |
if pre1 and pre2 evaluate to @{term True} in this environment,
|
neuper@38036
|
363 |
then the Rrls is applied. *)
|
neuper@38036
|
364 |
val t = str2term "(a + b) / c ::real";
|
neuper@38036
|
365 |
val pat = parse_patt thy "?r / ?s ::real";
|
neuper@38036
|
366 |
val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
|
neuper@38036
|
367 |
val prepat = [(pres, pat)];
|
neuper@38036
|
368 |
val erls = rational_erls;
|
neuper@38036
|
369 |
(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
|
neuper@38036
|
370 |
|
neuper@38036
|
371 |
val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
|
neuper@38036
|
372 |
val asms = map (Envir.subst_term subst) pres;
|
neuper@38036
|
373 |
if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
|
neuper@38036
|
374 |
then () else error "rewrite.sml: prepat cancel subst";
|
neuper@38036
|
375 |
if ([], true) = eval__true thy 0 asms [] erls
|
neuper@38036
|
376 |
then () else error "rewrite.sml: prepat cancel eval__true";
|
neuper@38036
|
377 |
|
neuper@52105
|
378 |
"===== Rational.thy: add_fractions_p ===";
|
neuper@38036
|
379 |
(* if each pat* matches with the current term, the Rrls is applied
|
neuper@48760
|
380 |
(there are no preconditions to be checked, they are @{term True}) *)
|
neuper@38036
|
381 |
val t = str2term "a / b + 1 / 2";
|
neuper@38036
|
382 |
val pat = parse_patt thy "?r / ?s + ?u / ?v";
|
neuper@48760
|
383 |
val pres = [@{term True}];
|
neuper@38036
|
384 |
val prepat = [(pres, pat)];
|
neuper@38036
|
385 |
val erls = rational_erls;
|
neuper@38036
|
386 |
(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
|
neuper@38036
|
387 |
|
neuper@38036
|
388 |
val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
|
neuper@38036
|
389 |
if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
|
neuper@52105
|
390 |
then () else error "rewrite.sml: prepat add_fractions_p";
|
neuper@38036
|
391 |
|
neuper@38036
|
392 |
"===== Poly.thy: order_mult_ ===";
|
neuper@38036
|
393 |
(* ?p matched with the current term gives an environment,
|
neuper@38036
|
394 |
which evaluates (the instantiated) "p is_multUnordered" to true*)
|
neuper@38036
|
395 |
val t = str2term "x^^^2 * x";
|
neuper@38036
|
396 |
val pat = parse_patt thy "?p :: real"
|
neuper@38036
|
397 |
val pres = [parse_patt thy "?p is_multUnordered"];
|
neuper@38036
|
398 |
val prepat = [(pres, pat)];
|
neuper@38036
|
399 |
val erls = append_rls "e_rls-is_multUnordered" e_rls
|
walther@59773
|
400 |
[Num_Calc ("Poly.is'_multUnordered",
|
neuper@38036
|
401 |
eval_is_multUnordered "")];
|
neuper@38036
|
402 |
|
neuper@38036
|
403 |
val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
|
neuper@38036
|
404 |
val asms = map (Envir.subst_term subst) pres;
|
neuper@38036
|
405 |
if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
|
neuper@38036
|
406 |
then () else error "rewrite.sml: prepat order_mult_ subst";
|
neuper@38036
|
407 |
if ([], true) = eval__true thy 0 asms [] erls
|
neuper@38036
|
408 |
then () else error "rewrite.sml: prepat order_mult_ eval__true";
|
neuper@38036
|
409 |
|
neuper@38036
|
410 |
|
neuper@38039
|
411 |
"----------- fun app_rev, Rrls, -------------------------";
|
neuper@38039
|
412 |
"----------- fun app_rev, Rrls, -------------------------";
|
neuper@38039
|
413 |
"----------- fun app_rev, Rrls, -------------------------";
|
neuper@38039
|
414 |
val t = str2term "x^^^2 * x";
|
neuper@41928
|
415 |
|
neuper@38039
|
416 |
if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
|
neuper@38039
|
417 |
val tm = str2term "(x^^^2 * x) is_multUnordered";
|
neuper@41928
|
418 |
eval_is_multUnordered "testid" "" tm thy;
|
neuper@41928
|
419 |
|
neuper@38039
|
420 |
case eval_is_multUnordered "testid" "" tm thy of
|
neuper@41924
|
421 |
SOME (_, Const ("HOL.Trueprop", _) $
|
neuper@41922
|
422 |
(Const ("HOL.eq", _) $
|
neuper@38039
|
423 |
(Const ("Poly.is'_multUnordered", _) $ _) $
|
neuper@41928
|
424 |
Const ("HOL.True", _))) => ()
|
neuper@41928
|
425 |
| _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
|
neuper@38039
|
426 |
|
walther@59627
|
427 |
tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := false;
|
neuper@38039
|
428 |
val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
|
neuper@38039
|
429 |
tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
|
neuper@38039
|
430 |
if term2str t' = "x * x ^^^ 2" then ()
|
neuper@38039
|
431 |
else error "rewrite.sml Poly.is'_multUnordered doesn't work";
|
neuper@38039
|
432 |
|
neuper@38039
|
433 |
(* for achieving the previous result, the following code was taken apart *)
|
neuper@38039
|
434 |
"----- rewrite__set_ ---";
|
neuper@38039
|
435 |
val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
|
neuper@38039
|
436 |
val (t', asm, rew) = app_rev thy (i+1) rrls t;
|
neuper@38039
|
437 |
"----- app_rev ---";
|
neuper@38039
|
438 |
val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
|
neuper@38039
|
439 |
fun chk_prepat thy erls [] t = true
|
neuper@38039
|
440 |
| chk_prepat thy erls prepat t =
|
neuper@38039
|
441 |
let fun chk (pres, pat) =
|
neuper@38039
|
442 |
(let val subst: Type.tyenv * Envir.tenv =
|
neuper@38039
|
443 |
Pattern.match thy (pat, t)
|
neuper@38039
|
444 |
(Vartab.empty, Vartab.empty)
|
neuper@38039
|
445 |
in snd (eval__true thy (i+1)
|
neuper@38039
|
446 |
(map (Envir.subst_term subst) pres)
|
neuper@38039
|
447 |
[] erls)
|
neuper@38039
|
448 |
end)
|
neuper@38039
|
449 |
handle _ => false
|
neuper@38039
|
450 |
fun scan_ f [] = false (*scan_ NEVER called by []*)
|
neuper@38039
|
451 |
| scan_ f (pp::pps) = if f pp then true
|
neuper@38039
|
452 |
else scan_ f pps;
|
neuper@38039
|
453 |
in scan_ chk prepat end;
|
neuper@38039
|
454 |
|
neuper@38039
|
455 |
(*.apply the normal_form of a rev-set.*)
|
neuper@38039
|
456 |
fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
|
neuper@38039
|
457 |
if chk_prepat thy erls prepat t
|
neuper@38039
|
458 |
then ((*tracing("### app_rev': t = "^(term2str t));*)
|
neuper@38039
|
459 |
normal_form t)
|
neuper@38039
|
460 |
else NONE;
|
neuper@38039
|
461 |
(*fixme val NONE = app_rev' thy rrls t;*)
|
neuper@38039
|
462 |
"----- app_rev' ---";
|
neuper@38039
|
463 |
val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
|
neuper@38039
|
464 |
(*fixme false*) chk_prepat thy erls prepat t;
|
neuper@38039
|
465 |
"----- chk_prepat ---";
|
neuper@38039
|
466 |
val (thy, erls, prepat, t) = (thy, erls, prepat, t);
|
neuper@38039
|
467 |
fun chk (pres, pat) =
|
neuper@38039
|
468 |
(let val subst: Type.tyenv * Envir.tenv =
|
neuper@38039
|
469 |
Pattern.match thy (pat, t)
|
neuper@38039
|
470 |
(Vartab.empty, Vartab.empty)
|
neuper@38039
|
471 |
in snd (eval__true thy (i+1)
|
neuper@38039
|
472 |
(map (Envir.subst_term subst) pres)
|
neuper@38039
|
473 |
[] erls)
|
neuper@38039
|
474 |
end)
|
neuper@38039
|
475 |
handle _ => false;
|
neuper@38039
|
476 |
fun scan_ f [] = false (*scan_ NEVER called by []*)
|
neuper@38039
|
477 |
| scan_ f (pp::pps) = if f pp then true
|
neuper@38039
|
478 |
else scan_ f pps;
|
neuper@38039
|
479 |
tracing "=== poly.sml: scan_ chk prepat begin";
|
neuper@38039
|
480 |
scan_ chk prepat;
|
neuper@38039
|
481 |
tracing "=== poly.sml: scan_ chk prepat end";
|
neuper@38039
|
482 |
|
neuper@38039
|
483 |
"----- chk ---";
|
neuper@38039
|
484 |
(*reestablish...*) val t = str2term "x ^^^ 2 * x";
|
neuper@38039
|
485 |
val [(pres, pat)] = prepat;
|
neuper@38039
|
486 |
val subst: Type.tyenv * Envir.tenv =
|
neuper@38039
|
487 |
Pattern.match thy (pat, t)
|
neuper@38039
|
488 |
(Vartab.empty, Vartab.empty);
|
neuper@38039
|
489 |
|
neuper@38039
|
490 |
(*fixme: asms = ["p is_multUnordered"]...instantiate*)
|
neuper@38039
|
491 |
"----- eval__true ---";
|
neuper@38039
|
492 |
val asms = (map (Envir.subst_term subst) pres);
|
neuper@38039
|
493 |
if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
|
neuper@38039
|
494 |
else error "rewrite.sml: diff. is_multUnordered, asms";
|
neuper@38039
|
495 |
val (thy, i, asms, bdv, rls) =
|
neuper@38039
|
496 |
(thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
|
neuper@38039
|
497 |
[] : (term * term) list, erls);
|
neuper@38039
|
498 |
case eval__true thy i asms bdv rls of
|
neuper@38039
|
499 |
([], true) => ()
|
neuper@38039
|
500 |
| _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
|
neuper@42223
|
501 |
|
neuper@42223
|
502 |
"----------- 2011 thms with axclasses -------------------";
|
neuper@42223
|
503 |
"----------- 2011 thms with axclasses -------------------";
|
neuper@42223
|
504 |
"----------- 2011 thms with axclasses -------------------";
|
wneuper@59348
|
505 |
val thm = num_str @{thm div_by_1};
|
wneuper@59188
|
506 |
val prop = Thm.prop_of thm;
|
neuper@42223
|
507 |
atomty prop; (*Type 'a*)
|
neuper@42223
|
508 |
val t = str2term "(2*x)/1"; (*Type real*)
|
neuper@42223
|
509 |
|
neuper@42223
|
510 |
val (thy, ro, er, inst) =
|
wneuper@59592
|
511 |
(@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
|
neuper@42223
|
512 |
val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
|
neuper@42223
|
513 |
|
walther@59841
|
514 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
walther@59841
|
515 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
walther@59841
|
516 |
"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
|
walther@59841
|
517 |
val thy = @{theory RatEq};
|
walther@59841
|
518 |
val ctxt = Proof_Context.init_global thy;
|
walther@59841
|
519 |
val SOME t = parseNEW ctxt "(3 + -1 * x + x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + x ^^^ 3) = 1 / x";
|
walther@59841
|
520 |
val rls = assoc_rls "RatEq_eliminate"
|
neuper@42394
|
521 |
|
walther@59841
|
522 |
val SOME (t''''', asm''''') =
|
walther@59841
|
523 |
rewrite_set_ thy true rls t;
|
walther@59841
|
524 |
"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
|
walther@59841
|
525 |
rewrite__set_ thy 1 bool [] rls term;
|
walther@59841
|
526 |
"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
|
walther@59841
|
527 |
= (thy, 1, bool, []:(term * term) list, rls, term);
|
walther@59841
|
528 |
|
walther@59841
|
529 |
(*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
|
walther@59841
|
530 |
datatype switch = Appl | Noap;
|
walther@59841
|
531 |
fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
|
walther@59841
|
532 |
| rew_once ruls asm ct Appl [] =
|
walther@59851
|
533 |
(case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
|
walther@59851
|
534 |
| Rule_Set.Seqence _ => (ct, asm)
|
walther@59841
|
535 |
| rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\""))
|
walther@59841
|
536 |
| rew_once ruls asm ct apno (rul :: thms) =
|
walther@59841
|
537 |
case rul of
|
walther@59841
|
538 |
Rule.Thm (thmid, thm) =>
|
walther@59841
|
539 |
(trace1 i (" try thm: " ^ thmid);
|
walther@59841
|
540 |
case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
|
walther@59841
|
541 |
((#erls o Rule.rep_rls) rls) put_asm thm ct of
|
walther@59841
|
542 |
NONE => rew_once ruls asm ct apno thms
|
walther@59841
|
543 |
| SOME (ct', asm') =>
|
walther@59841
|
544 |
(trace1 i (" rewrites to: " ^ Rule.t2str thy ct');
|
walther@59841
|
545 |
rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
|
walther@59841
|
546 |
(* once again try the same rule, e.g. associativity against "()"*)
|
walther@59841
|
547 |
| Rule.Num_Calc (cc as (op_, _)) =>
|
walther@59841
|
548 |
let val _= trace1 i (" try calc: " ^ op_ ^ "'")
|
walther@59841
|
549 |
val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
|
walther@59841
|
550 |
in case Num_Calc.adhoc_thm thy cc ct of
|
walther@59841
|
551 |
NONE => rew_once ruls asm ct apno thms
|
walther@59841
|
552 |
| SOME (_, thm') =>
|
walther@59841
|
553 |
let
|
walther@59841
|
554 |
val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
|
walther@59841
|
555 |
((#erls o Rule.rep_rls) rls) put_asm thm' ct;
|
walther@59841
|
556 |
val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
|
walther@59841
|
557 |
Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
|
walther@59841
|
558 |
val _ = trace1 i (" calc. to: " ^ Rule.t2str thy ((fst o the) pairopt))
|
walther@59841
|
559 |
in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
|
walther@59841
|
560 |
end
|
walther@59841
|
561 |
| Rule.Cal1 (cc as (op_, _)) =>
|
walther@59841
|
562 |
let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
|
walther@59841
|
563 |
val ct = TermC.uminus_to_string ct
|
walther@59841
|
564 |
in case Num_Calc.adhoc_thm1_ thy cc ct of
|
walther@59841
|
565 |
NONE => (ct, asm)
|
walther@59841
|
566 |
| SOME (_, thm') =>
|
walther@59841
|
567 |
let
|
walther@59841
|
568 |
val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
|
walther@59841
|
569 |
((#erls o Rule.rep_rls) rls) put_asm thm' ct;
|
walther@59841
|
570 |
val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
|
walther@59841
|
571 |
Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
|
walther@59841
|
572 |
val _ = trace1 i (" cal1. to: " ^ Rule.t2str thy ((fst o the) pairopt))
|
walther@59841
|
573 |
in the pairopt end
|
walther@59841
|
574 |
end
|
walther@59841
|
575 |
| Rule.Rls_ rls' =>
|
walther@59841
|
576 |
(case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
|
walther@59841
|
577 |
SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
|
walther@59841
|
578 |
| NONE => rew_once ruls asm ct apno thms)
|
walther@59841
|
579 |
| r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
|
walther@59841
|
580 |
val ruls = (#rules o Rule.rep_rls) rls;
|
walther@59850
|
581 |
(* val _ = trace i (" rls: " ^ Rule_Set.id_rls rls ^ " on: " ^ Rule.t2str thy ct)*)
|
walther@59841
|
582 |
val (ct', asm') = rew_once ruls [] ct Noap ruls;
|
walther@59841
|
583 |
"~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
|
walther@59841
|
584 |
= (ruls, []:term list, ct, Noap, ruls);
|
walther@59841
|
585 |
val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
|
walther@59841
|
586 |
|
walther@59841
|
587 |
val SOME (ct', asm') = (*case*)
|
walther@59841
|
588 |
rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
|
walther@59841
|
589 |
((#erls o Rule.rep_rls) rls) put_asm thm ct (*of*);
|
walther@59841
|
590 |
"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
|
walther@59841
|
591 |
= (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.rep_rls) rls),
|
walther@59841
|
592 |
((#erls o Rule.rep_rls) rls), put_asm, thm, ct);
|
walther@59841
|
593 |
|
walther@59841
|
594 |
val (t', asms, _ (*lrd*), rew) =
|
walther@59841
|
595 |
rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
|
walther@59841
|
596 |
(((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct;
|
walther@59841
|
597 |
"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
|
walther@59841
|
598 |
= (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
|
walther@59841
|
599 |
(((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm), ct);
|
walther@59841
|
600 |
val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
|
walther@59841
|
601 |
val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
|
walther@59841
|
602 |
;
|
walther@59841
|
603 |
(*+*)if term2str r' =
|
walther@59841
|
604 |
(*+*) "\<lbrakk>9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
|
walther@59841
|
605 |
(*+*) "\<Longrightarrow> ((3 + -1 * x + x ^^^ 2) /\n" ^
|
walther@59841
|
606 |
(*+*) " (9 * x + -6 * x ^^^ 2 + x ^^^ 3) =\n" ^
|
walther@59841
|
607 |
(*+*) " 1 / x) =\n" ^
|
walther@59841
|
608 |
(*+*) " ((3 + -1 * x + x ^^^ 2) * x =\n" ^
|
walther@59841
|
609 |
(*+*) " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3))"
|
walther@59841
|
610 |
(*+*)then () else error "instantiated rule CHANGED";
|
walther@59841
|
611 |
|
walther@59841
|
612 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
|
walther@59841
|
613 |
;
|
walther@59841
|
614 |
(*+*)if map term2str p' = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
|
walther@59841
|
615 |
(*+*)then () else error "stored assumptions CHANGED";
|
walther@59841
|
616 |
|
walther@59841
|
617 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
|
walther@59841
|
618 |
;
|
walther@59841
|
619 |
(*+*)if term2str t' = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
|
walther@59841
|
620 |
(*+*)then () else error "rewritten term (an equality) CHANGED";
|
walther@59841
|
621 |
|
walther@59841
|
622 |
val (simpl_p', nofalse) =
|
walther@59841
|
623 |
eval__true thy (i + 1) p' bdv rls;
|
walther@59841
|
624 |
"~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
|
walther@59841
|
625 |
(*if*) asms = [@{term True}] orelse asms = [] (*else*);
|
walther@59841
|
626 |
|
walther@59841
|
627 |
(*+*)if map term2str asms = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
|
walther@59841
|
628 |
(*+*)then () else error "asms before chk CHANGED";
|
walther@59841
|
629 |
|
walther@59841
|
630 |
fun chk indets [] = (indets, true) (*return asms<>True until false*)
|
walther@59841
|
631 |
| chk indets (a :: asms) =
|
walther@59841
|
632 |
(case rewrite__set_ thy (i + 1) false bdv rls a of
|
walther@59841
|
633 |
NONE => (chk (indets @ [a]) asms)
|
walther@59841
|
634 |
| SOME (t, a') =>
|
walther@59841
|
635 |
if t = @{term True} then (chk (indets @ a') asms)
|
walther@59841
|
636 |
else if t = @{term False} then ([], false)
|
walther@59841
|
637 |
(*asm false .. thm not applied ^^^; continue until False vvv*)
|
walther@59841
|
638 |
else chk (indets @ [t] @ a') asms);
|
walther@59841
|
639 |
|
walther@59841
|
640 |
val (xxx, true) =
|
walther@59841
|
641 |
chk [] asms; (*return from eval__true*);
|
walther@59841
|
642 |
"~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
|
walther@59841
|
643 |
|
walther@59851
|
644 |
(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
|
walther@59841
|
645 |
(*+*)(*val rules =
|
walther@59841
|
646 |
(*+*) [Num_Calc ("Rings.divide_class.divide", fn),
|
walther@59841
|
647 |
(*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
|
walther@59841
|
648 |
(*+*) :
|
walther@59841
|
649 |
(*+*) Num_Calc ("HOL.eq", fn),
|
walther@59841
|
650 |
(*+*) Thm ("not_true", "(\<not> True) = False"),
|
walther@59841
|
651 |
(*+*) Thm ("not_false", "(\<not> False) = True"),
|
walther@59841
|
652 |
(*+*) :
|
walther@59841
|
653 |
(*+*) Num_Calc ("Prog_Expr.pow", fn),
|
walther@59841
|
654 |
(*+*) Num_Calc ("RatEq.is'_ratequation'_in", fn)]:
|
walther@59841
|
655 |
(*+*) rule list*)
|
walther@59841
|
656 |
(*+*)chk: term list -> term list -> term list * bool
|
walther@59841
|
657 |
|
walther@59841
|
658 |
rewrite__set_ thy (i + 1) false bdv rls a (*of*);
|
walther@59841
|
659 |
|
walther@59841
|
660 |
(*+*)trace_rewrite := true;
|
walther@59841
|
661 |
|
walther@59841
|
662 |
(*this was False; vvvv--- means: indeterminate*)
|
walther@59841
|
663 |
val (* SOME (t, a') *)NONE = (*case*)
|
walther@59841
|
664 |
rewrite__set_ thy (i + 1) false bdv rls a (*of*);
|
walther@59841
|
665 |
|
walther@59841
|
666 |
(*+*)term2str a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
|
neuper@42394
|
667 |
(*
|
neuper@42394
|
668 |
:
|
walther@59841
|
669 |
#### rls: rateq_erls on: x \<noteq> 0
|
neuper@42394
|
670 |
:
|
neuper@42394
|
671 |
##### try calc: HOL.eq' <<<------------------------------- here the error comes from
|
walther@59841
|
672 |
===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
|
neuper@42394
|
673 |
##### try calc: HOL.eq'
|
neuper@42394
|
674 |
##### try thm: not_true
|
neuper@42394
|
675 |
##### try thm: not_false
|
walther@59841
|
676 |
===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
|
walther@59841
|
677 |
and True, False are NOT stored ...
|
walther@59841
|
678 |
:
|
walther@59841
|
679 |
### asms accepted: [x \<noteq> 0] stored: []
|
walther@59841
|
680 |
: *)
|
neuper@42394
|
681 |
trace_rewrite := false;
|
walther@59841
|
682 |
( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
|
walther@59841
|
683 |
|
neuper@42394
|
684 |
|
wneuper@59110
|
685 |
"----------- fun assoc_thm' -----------------------------";
|
wneuper@59110
|
686 |
"----------- fun assoc_thm' -----------------------------";
|
wneuper@59110
|
687 |
"----------- fun assoc_thm' -----------------------------";
|
wneuper@59110
|
688 |
val thy = @{theory ProgLang}
|
wneuper@59110
|
689 |
|
wneuper@59110
|
690 |
val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
|
wneuper@59110
|
691 |
if string_of_thm' thy tth = "6 = 2 * 3" then ()
|
wneuper@59110
|
692 |
else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
|
wneuper@59110
|
693 |
|
wneuper@59110
|
694 |
val tth = assoc_thm' thy ("add_0_left","");
|
wneuper@59110
|
695 |
if string_of_thm' thy tth = "0 + ?a = ?a" then ()
|
wneuper@59110
|
696 |
else error "assoc_thm' (add_0_left,\"\") changed";
|
wneuper@59110
|
697 |
|
wneuper@59110
|
698 |
val tth = assoc_thm' thy ("sym_add_0_left","");
|
wneuper@59110
|
699 |
if string_of_thm' thy tth = "?t = 0 + ?t" then ()
|
wneuper@59110
|
700 |
else error "assoc_thm' (sym_add_0_left,\"\") changed";
|
wneuper@59110
|
701 |
|
wneuper@59110
|
702 |
val tth = assoc_thm' thy ("add_commute","");
|
wneuper@59110
|
703 |
if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
|
wneuper@59110
|
704 |
else error "assoc_thm' (add_commute,\"\") changed"
|
wneuper@59110
|
705 |
|
wneuper@59252
|
706 |
"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
|
wneuper@59252
|
707 |
"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
|
wneuper@59252
|
708 |
"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
|
wneuper@59252
|
709 |
"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
|
wneuper@59252
|
710 |
(@{theory}, dummy_ord, e_rls, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
|
wneuper@59252
|
711 |
"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
|
wneuper@59252
|
712 |
(thy, 1, [], rew_ord, erls, bool, thm, term);
|
wneuper@59252
|
713 |
"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
|
wneuper@59252
|
714 |
(thy, i, bdv, tless, rls, put_asm, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct)
|
wneuper@59252
|
715 |
val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
|
wneuper@59252
|
716 |
val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
|
wneuper@59252
|
717 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
|
wneuper@59252
|
718 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
|
wneuper@59252
|
719 |
;
|
wneuper@59252
|
720 |
if term2str lhss = "?a * (?b + ?c)" andalso term2str t = "x * (y + z)" then ()
|
wneuper@59252
|
721 |
else error "ARGS FOR Pattern.match CHANGED";
|
wneuper@59252
|
722 |
val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
|
wneuper@59252
|
723 |
if (Envir.subst_term match r |> term2str) = "x * (y + z) = x * y + x * z" then ()
|
wneuper@59252
|
724 |
else error "Pattern.match CHANGED";
|
wneuper@59381
|
725 |
|
wneuper@59381
|
726 |
"----------- fun mk_thm ------------------------------------------------------------------------";
|
wneuper@59381
|
727 |
"----------- fun mk_thm ------------------------------------------------------------------------";
|
wneuper@59381
|
728 |
"----------- fun mk_thm ------------------------------------------------------------------------";
|
wneuper@59592
|
729 |
val thy = @{theory Isac_Knowledge}
|
wneuper@59381
|
730 |
|
wneuper@59385
|
731 |
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
|
wneuper@59385
|
732 |
val thm = @{thm realpow_twoI};
|
wneuper@59385
|
733 |
val patt_str = "?r ^^^ 2 = ?r * ?r";
|
wneuper@59385
|
734 |
val term_str = "r ^^^ 2 = r * r";
|
wneuper@59385
|
735 |
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
|
wneuper@59385
|
736 |
case parse_patt thy patt_str of
|
walther@59603
|
737 |
Const ("HOL.eq", _) $ (Const ("Prog_Expr.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
|
wneuper@59385
|
738 |
(Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
|
wneuper@59385
|
739 |
| _ => error "parse_patt ?r ^^^ 2 = ?r * ?r changed";
|
wneuper@59395
|
740 |
case parse thy term_str of
|
wneuper@59385
|
741 |
NONE => ()
|
wneuper@59385
|
742 |
| _ => writeln "parse does NOT take patterns with '?'";
|
wneuper@59381
|
743 |
|
wneuper@59385
|
744 |
val t1 = (#prop o Thm.rep_thm) (num_str thm);
|
wneuper@59385
|
745 |
if term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
|
wneuper@59381
|
746 |
|
wneuper@59395
|
747 |
val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
|
wneuper@59385
|
748 |
if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
|
wneuper@59385
|
749 |
|
wneuper@59385
|
750 |
(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
|
wneuper@59385
|
751 |
(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
|
wneuper@59385
|
752 |
gives a strange thm*);
|
wneuper@59395
|
753 |
(*while this..*)
|
wneuper@59385
|
754 |
val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
|
wneuper@59395
|
755 |
..gives another strange thm; but it is used and works with rewriting: *);
|
wneuper@59385
|
756 |
|
wneuper@59385
|
757 |
val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
|
wneuper@59385
|
758 |
if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
|
wneuper@59385
|
759 |
|
wneuper@59385
|
760 |
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
|
wneuper@59385
|
761 |
val thm = @{thm real_mult_div_cancel2};
|
wneuper@59385
|
762 |
val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
|
wneuper@59385
|
763 |
val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";
|
wneuper@59385
|
764 |
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
|
wneuper@59385
|
765 |
case parse_patt thy patt_str of
|
wneuper@59385
|
766 |
Const ("Pure.imp", _) $
|
wneuper@59385
|
767 |
(Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $
|
wneuper@59385
|
768 |
(Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $
|
wneuper@59385
|
769 |
(Const ("HOL.Trueprop", _) $
|
wneuper@59385
|
770 |
(Const ("HOL.eq", _) $ _ $ _ )) => ()
|
wneuper@59385
|
771 |
| _ => error "parse_patt ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n changed";
|
wneuper@59395
|
772 |
case parse thy term_str of
|
wneuper@59385
|
773 |
NONE => ()
|
wneuper@59385
|
774 |
| _ => writeln "parse does NOT take patterns with '?'";
|
wneuper@59385
|
775 |
|
wneuper@59385
|
776 |
val t1 = (#prop o Thm.rep_thm) (num_str thm);
|
wneuper@59385
|
777 |
if term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
|
wneuper@59385
|
778 |
|
wneuper@59385
|
779 |
val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
|
wneuper@59385
|
780 |
if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
|
wneuper@59385
|
781 |
|
wneuper@59385
|
782 |
(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
|
wneuper@59385
|
783 |
(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
|
wneuper@59385
|
784 |
gives a strange thm*);
|
wneuper@59385
|
785 |
(*while this*)
|
wneuper@59385
|
786 |
val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
|
wneuper@59385
|
787 |
gives another strange thm; but it is used and words with rewriting: *);
|
wneuper@59385
|
788 |
|
wneuper@59385
|
789 |
val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
|
wneuper@59385
|
790 |
if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
|
wneuper@59411
|
791 |
|
wneuper@59411
|
792 |
"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
|
wneuper@59411
|
793 |
"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
|
wneuper@59411
|
794 |
"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
|
wneuper@59411
|
795 |
(* norm_equation is defined in Test.thy, other rls see Knowledg/**)
|
wneuper@59411
|
796 |
val thy = @{theory};
|
wneuper@59411
|
797 |
val rls = norm_equation;
|
wneuper@59411
|
798 |
val term = str2term "x + 1 = 2";
|
wneuper@59411
|
799 |
|
wneuper@59411
|
800 |
val SOME (t, asm) = rewrite_set_ thy false rls term;
|
wneuper@59411
|
801 |
if term2str t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
|
wneuper@59411
|
802 |
|
wneuper@59411
|
803 |
"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
|
wneuper@59411
|
804 |
"~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
|
walther@59841
|
805 |
|