walther@59633
|
1 |
(* Title: ProgLang/program.sml
|
walther@59633
|
2 |
Author: Walther Neuper 190922
|
walther@59633
|
3 |
(c) due to copyright terms
|
walther@59633
|
4 |
*)
|
walther@59633
|
5 |
|
walther@59633
|
6 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
7 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
8 |
"table of contents -----------------------------------------------------------------------------";
|
walther@59633
|
9 |
"-----------------------------------------------------------------------------------------------";
|
walther@59841
|
10 |
"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
|
walther@59847
|
11 |
"-------- occurs_in ----------------------------------------------------------------------------";
|
walther@59847
|
12 |
"-------- fun eval_occurs_in -------------------------------------------------------------------";
|
walther@59847
|
13 |
"-------- fun eval_argument_of -----------------------------------------------------------------";
|
walther@59847
|
14 |
"-------- fun eval_sameFunId -------------------------------------------------------------------";
|
walther@59847
|
15 |
"-------- fun eval_filter_sameFunId ------------------------------------------------------------";
|
walther@59847
|
16 |
"-------- fun eval_boollist2sum ----------------------------------------------------------------";
|
walther@59847
|
17 |
"-------- fun eval_binop -----------------------------------------------------------------------";
|
walther@59847
|
18 |
"-------- fun matchsub -------------------------------------------------------------------------";
|
walther@59847
|
19 |
"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
|
walther@59633
|
20 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
21 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
22 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
23 |
|
walther@59633
|
24 |
|
walther@59841
|
25 |
"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
|
walther@59841
|
26 |
"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
|
walther@59841
|
27 |
"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
|
walther@59841
|
28 |
val thy = @{theory}
|
walther@59841
|
29 |
|
walther@59841
|
30 |
val t = str2term "x = 0";
|
walther@59841
|
31 |
val NONE(*= indetermined*) = eval_equal "equal_" "HOL.eq" t thy;
|
walther@59841
|
32 |
|
walther@59841
|
33 |
val t = str2term "(x + 1) = (x + 1)";
|
walther@59841
|
34 |
val (Const _(*op0,t0*) $ t1 $ t2 ) = t
|
walther@59841
|
35 |
val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" "HOL.eq" t thy;
|
walther@59841
|
36 |
if term2str t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED";
|
walther@59841
|
37 |
|
walther@59841
|
38 |
val t as Const _ $ v $ c = str2term "1 = 0";
|
walther@59841
|
39 |
val false = variable_constant_pair (v, c);
|
walther@59841
|
40 |
val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" "HOL.eq" t thy;
|
walther@59841
|
41 |
if term2str t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED";
|
walther@59841
|
42 |
|
walther@59841
|
43 |
val t = str2term "0 = 0";
|
walther@59841
|
44 |
val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" "HOL.eq" t thy;
|
walther@59841
|
45 |
if term2str t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";
|
walther@59847
|
46 |
|
walther@59847
|
47 |
|
walther@59847
|
48 |
"-------- occurs_in ----------------------------------------------------------------------------";
|
walther@59847
|
49 |
"-------- occurs_in ----------------------------------------------------------------------------";
|
walther@59847
|
50 |
"-------- occurs_in ----------------------------------------------------------------------------";
|
walther@59847
|
51 |
(*=========================================================================*)
|
walther@59847
|
52 |
fun str2t str = (Thm.term_of o the o (parse thy)) str;
|
walther@59847
|
53 |
fun term2s t = term_to_string''' thy t;
|
walther@59847
|
54 |
(*=========================================================================*)
|
walther@59847
|
55 |
|
walther@59847
|
56 |
val t = str2t "x";
|
walther@59847
|
57 |
if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";
|
walther@59847
|
58 |
|
walther@59847
|
59 |
val t = str2term "x occurs_in x";
|
walther@59847
|
60 |
val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs'_in" t 0;
|
walther@59847
|
61 |
if term2str t' = "x occurs_in x = True" then ()
|
walther@59847
|
62 |
else error "x occurs_in x = True ..changed";
|
walther@59847
|
63 |
|
walther@59847
|
64 |
"------- some_occur_in";
|
walther@59847
|
65 |
some_occur_in [str2t"c",str2t"c_2"] (str2t"a + b + c");
|
walther@59847
|
66 |
val t = str2t "some_of [c, c_2, c_3, c_4] occur_in \
|
walther@59847
|
67 |
\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
|
walther@59847
|
68 |
val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some'_occur'_in" t 0;
|
walther@59847
|
69 |
if term2str t' =
|
walther@59847
|
70 |
"some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then ()
|
walther@59847
|
71 |
else error "atools.sml: some_occur_in true";
|
walther@59847
|
72 |
|
walther@59847
|
73 |
val t = str2t "some_of [c_3, c_4] occur_in \
|
walther@59847
|
74 |
\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
|
walther@59847
|
75 |
val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some'_occur'_in" t 0;
|
walther@59847
|
76 |
if term2str t' =
|
walther@59847
|
77 |
"some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
|
walther@59847
|
78 |
else error "atools.sml: some_occur_in false";
|
walther@59847
|
79 |
|
walther@59847
|
80 |
|
walther@59847
|
81 |
"-------- fun eval_occurs_in -------------------------------------------------------------------";
|
walther@59847
|
82 |
"-------- fun eval_occurs_in -------------------------------------------------------------------";
|
walther@59847
|
83 |
"-------- fun eval_occurs_in -------------------------------------------------------------------";
|
walther@59847
|
84 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
walther@59847
|
85 |
val t = (Thm.term_of o the o (parse thy)) "1";
|
walther@59847
|
86 |
if occurs_in v t then error "factor_right_deg (1) x ..changed" else ();
|
walther@59847
|
87 |
|
walther@59847
|
88 |
val v = (Thm.term_of o the o (parse thy)) "AA";
|
walther@59847
|
89 |
val t = (Thm.term_of o the o (parse thy)) "1";
|
walther@59847
|
90 |
if occurs_in v t then error "factor_right_deg (1) AA ..changed" else ();
|
walther@59847
|
91 |
|
walther@59847
|
92 |
(*----------*)
|
walther@59847
|
93 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
walther@59847
|
94 |
val t = (Thm.term_of o the o (parse thy)) "a*b+c";
|
walther@59847
|
95 |
if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else ();
|
walther@59847
|
96 |
|
walther@59847
|
97 |
val v = (Thm.term_of o the o (parse thy)) "AA";
|
walther@59847
|
98 |
val t = (Thm.term_of o the o (parse thy)) "a*b+c";
|
walther@59847
|
99 |
if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else ();
|
walther@59847
|
100 |
|
walther@59847
|
101 |
(*----------*)
|
walther@59847
|
102 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
walther@59847
|
103 |
val t = (Thm.term_of o the o (parse thy)) "a*x+c";
|
walther@59847
|
104 |
if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed";
|
walther@59847
|
105 |
|
walther@59847
|
106 |
val v = (Thm.term_of o the o (parse thy)) "AA";
|
walther@59847
|
107 |
val t = (Thm.term_of o the o (parse thy)) "a*AA+c";
|
walther@59847
|
108 |
if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed";
|
walther@59847
|
109 |
|
walther@59847
|
110 |
(*----------*)
|
walther@59847
|
111 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
walther@59847
|
112 |
val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x^^^7";
|
walther@59847
|
113 |
if occurs_in v t then () else error "factor_right_deg (a*b+c)*x^^^7) x ..changed";
|
walther@59847
|
114 |
|
walther@59847
|
115 |
val v = (Thm.term_of o the o (parse thy)) "AA";
|
walther@59847
|
116 |
val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA^^^7";
|
walther@59847
|
117 |
if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA^^^7) AA ..changed";
|
walther@59847
|
118 |
|
walther@59847
|
119 |
(*----------*)
|
walther@59847
|
120 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
walther@59847
|
121 |
val t = (Thm.term_of o the o (parse thy)) "x^^^7";
|
walther@59847
|
122 |
if occurs_in v t then () else error "factor_right_deg (x^^^7) x ..changed";
|
walther@59847
|
123 |
|
walther@59847
|
124 |
val v = (Thm.term_of o the o (parse thy)) "AA";
|
walther@59847
|
125 |
val t = (Thm.term_of o the o (parse thy)) "AA^^^7";
|
walther@59847
|
126 |
if occurs_in v t then () else error "factor_right_deg (AA^^^7) AA ..changed";
|
walther@59847
|
127 |
|
walther@59847
|
128 |
(*----------*)
|
walther@59847
|
129 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
walther@59847
|
130 |
val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x";
|
walther@59847
|
131 |
if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed";
|
walther@59847
|
132 |
|
walther@59847
|
133 |
val v = (Thm.term_of o the o (parse thy)) "AA";
|
walther@59847
|
134 |
val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA";
|
walther@59847
|
135 |
if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed";
|
walther@59847
|
136 |
|
walther@59847
|
137 |
(*----------*)
|
walther@59847
|
138 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
walther@59847
|
139 |
val t = (Thm.term_of o the o (parse thy)) "(a*b+x)*x";
|
walther@59847
|
140 |
if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed";
|
walther@59847
|
141 |
|
walther@59847
|
142 |
val v = (Thm.term_of o the o (parse thy)) "AA";
|
walther@59847
|
143 |
val t = (Thm.term_of o the o (parse thy)) "(a*b+AA)*AA";
|
walther@59847
|
144 |
if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed";
|
walther@59847
|
145 |
|
walther@59847
|
146 |
(*----------*)
|
walther@59847
|
147 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
walther@59847
|
148 |
val t = (Thm.term_of o the o (parse thy)) "x";
|
walther@59847
|
149 |
if occurs_in v t then () else error "factor_right_deg (x) x ..changed";
|
walther@59847
|
150 |
|
walther@59847
|
151 |
val v = (Thm.term_of o the o (parse thy)) "AA";
|
walther@59847
|
152 |
val t = (Thm.term_of o the o (parse thy)) "AA";
|
walther@59847
|
153 |
if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed";
|
walther@59847
|
154 |
|
walther@59847
|
155 |
(*----------*)
|
walther@59847
|
156 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
walther@59847
|
157 |
val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*x";
|
walther@59847
|
158 |
if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed";
|
walther@59847
|
159 |
|
walther@59847
|
160 |
val v = (Thm.term_of o the o (parse thy)) "AA";
|
walther@59847
|
161 |
val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*AA";
|
walther@59847
|
162 |
if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed";
|
walther@59847
|
163 |
|
walther@59847
|
164 |
|
walther@59847
|
165 |
"---------fun eval_argument_of -----------------------------------------------------------------";
|
walther@59847
|
166 |
"---------fun eval_argument_of -----------------------------------------------------------------";
|
walther@59847
|
167 |
"---------fun eval_argument_of -----------------------------------------------------------------";
|
walther@59847
|
168 |
val t = str2term "argument_in (M_b x)";
|
walther@59847
|
169 |
val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument'_in" t 0;
|
walther@59847
|
170 |
if term2str t' = "(argument_in M_b x) = x" then ()
|
walther@59847
|
171 |
else error "atools.sml:(argument_in M_b x) = x ???";
|
walther@59847
|
172 |
|
walther@59847
|
173 |
|
walther@59847
|
174 |
"---------fun eval_sameFunId -------------------------------------------------------------------";
|
walther@59847
|
175 |
"---------fun eval_sameFunId -------------------------------------------------------------------";
|
walther@59847
|
176 |
"---------fun eval_sameFunId -------------------------------------------------------------------";
|
walther@59847
|
177 |
val t = str2t "M_b L"; atomty t;
|
walther@59847
|
178 |
val t as f1 $ _ = str2t "M_b L";
|
walther@59847
|
179 |
val t as Const ("HOL.eq", _) $ (f2 $ _) $ _ = str2t "M_b x = c + L*x";
|
walther@59847
|
180 |
f1 = f2 (*true*);
|
walther@59847
|
181 |
val (p as Const ("Prog_Expr.sameFunId",_) $
|
walther@59847
|
182 |
(f1 $ _) $
|
walther@59847
|
183 |
(Const ("HOL.eq", _) $ (f2 $ _) $ _)) =
|
walther@59847
|
184 |
str2t "sameFunId (M_b L) (M_b x = c + L*x)";
|
walther@59847
|
185 |
f1 = f2 (*true*);
|
walther@59847
|
186 |
eval_sameFunId "" "Prog_Expr.sameFunId"
|
walther@59847
|
187 |
(str2t "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*);
|
walther@59847
|
188 |
eval_sameFunId "" "Prog_Expr.sameFunId"
|
walther@59847
|
189 |
(str2t "sameFunId (M_b L) ( y' x = c + L*x)")""(*false*);
|
walther@59847
|
190 |
eval_sameFunId "" "Prog_Expr.sameFunId"
|
walther@59847
|
191 |
(str2t "sameFunId (M_b L) ( y x = c + L*x)")""(*false*);
|
walther@59847
|
192 |
eval_sameFunId "" "Prog_Expr.sameFunId"
|
walther@59847
|
193 |
(str2t "sameFunId ( y L) (M_b x = c + L*x)")""(*false*);
|
walther@59847
|
194 |
eval_sameFunId "" "Prog_Expr.sameFunId"
|
walther@59847
|
195 |
(str2t "sameFunId ( y L) ( y x = c + L*x)")""(*true*);
|
walther@59847
|
196 |
|
walther@59847
|
197 |
|
walther@59847
|
198 |
"---------fun eval_filter_sameFunId ------------------------------------------------------------";
|
walther@59847
|
199 |
"---------fun eval_filter_sameFunId ------------------------------------------------------------";
|
walther@59847
|
200 |
"---------fun eval_filter_sameFunId ------------------------------------------------------------";
|
walther@59847
|
201 |
val flhs as (fid $ _) = str2t "y' L";
|
walther@59847
|
202 |
val fs = str2t "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
|
walther@59847
|
203 |
val (p as Const ("Prog_Expr.filter'_sameFunId",_) $ (fid $ _) $ fs) =
|
walther@59847
|
204 |
str2t "filter_sameFunId (y' L) \
|
walther@59847
|
205 |
\[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
|
walther@59847
|
206 |
val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter'_sameFunId" p "";
|
walther@59847
|
207 |
if term2str es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n y x = c + L * x]) =\n[y' x = c + L * x]" then ()
|
walther@59847
|
208 |
else error "atools.slm diff.behav. in filter_sameFunId";
|
walther@59847
|
209 |
|
walther@59847
|
210 |
|
walther@59847
|
211 |
"---------fun eval_boollist2sum ----------------------------------------------------------------";
|
walther@59847
|
212 |
"---------fun eval_boollist2sum ----------------------------------------------------------------";
|
walther@59847
|
213 |
"---------fun eval_boollist2sum ----------------------------------------------------------------";
|
walther@59847
|
214 |
fun lhs (Const ("HOL.eq",_) $ l $ _) = l
|
walther@59847
|
215 |
| lhs t = error("lhs called with (" ^ term2str t ^ ")");
|
walther@59847
|
216 |
"-----------^^^redefined due to overwritten identifier -----------";
|
walther@59847
|
217 |
val u_ = str2t "[]";
|
walther@59847
|
218 |
val u_ = str2t "[b1 = k - 2*q]";
|
walther@59847
|
219 |
val u_ = str2t "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
|
walther@59847
|
220 |
val ut_ = isalist2list u_;
|
walther@59847
|
221 |
val sum_ = map lhs ut_;
|
walther@59847
|
222 |
val t = list2sum sum_;
|
walther@59847
|
223 |
term2str t;
|
walther@59847
|
224 |
|
walther@59847
|
225 |
val t = str2t "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
|
walther@59847
|
226 |
|
walther@59847
|
227 |
val p as Const ("Prog_Expr.boollist2sum", _) $ (Const ("List.list.Cons", _) $ _ $ _) = t;
|
walther@59847
|
228 |
|
walther@59847
|
229 |
val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t "";
|
walther@59847
|
230 |
if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then ()
|
walther@59847
|
231 |
else error "atools.sml diff.behav. in eval_boollist2sum";
|
walther@59847
|
232 |
|
walther@59847
|
233 |
trace_rewrite := false;
|
walther@59852
|
234 |
val srls_ = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty
|
walther@59847
|
235 |
[Num_Calc ("Prog_Expr.boollist2sum", eval_boollist2sum "")];
|
walther@59847
|
236 |
val t = str2t
|
walther@59847
|
237 |
"boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
|
walther@59847
|
238 |
case rewrite_set_ thy false srls_ t of SOME _ => ()
|
walther@59847
|
239 |
| _ => error "atools.sml diff.rewrite boollist2sum";
|
walther@59847
|
240 |
trace_rewrite := false;
|
walther@59847
|
241 |
|
walther@59847
|
242 |
|
walther@59847
|
243 |
"---------fun eval_binop -----------------------------------------------------------------------";
|
walther@59847
|
244 |
"---------fun eval_binop -----------------------------------------------------------------------";
|
walther@59847
|
245 |
"---------fun eval_binop -----------------------------------------------------------------------";
|
walther@59847
|
246 |
val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
|
walther@59847
|
247 |
val t = (Thm.term_of o the o (parse thy)) "2 * 3";
|
walther@59847
|
248 |
(*val SOME (thmid,t') = *)get_pair thy op_ ef t;
|
walther@59847
|
249 |
;
|
walther@59847
|
250 |
"~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
|
walther@59847
|
251 |
(thy, op_, ef, t);
|
walther@59847
|
252 |
op_ = op0 = true;
|
walther@59847
|
253 |
ef op_ t thy
|
walther@59847
|
254 |
;
|
walther@59847
|
255 |
"~~~~~ fun eval_binop, args:"; val ((thmid : string), (op_: string),
|
walther@59847
|
256 |
(t as (Const (op0, t0) $ t1 $ t2)), _) = ("#mult_", op_, t, thy); (* binary . n1.(n2.v) *)
|
walther@59847
|
257 |
val (SOME n1, SOME n2) = (numeral t1, numeral t2)
|
walther@59847
|
258 |
val (_, _, Trange) = dest_binop_typ t0;
|
walther@59847
|
259 |
val res = calcul op0 n1 n2;
|
walther@59847
|
260 |
val rhs = term_of_float Trange res;
|
walther@59847
|
261 |
val prop = HOLogic.Trueprop $ (mk_equality (t, rhs));
|
walther@59847
|
262 |
val SOME (thmid, tm) = SOME ("#: " ^ term2str prop, prop)
|
walther@59847
|
263 |
;
|
walther@59847
|
264 |
if thmid = "#: 2 * 3 = 6" andalso term2str prop = "2 * 3 = 6" then ()
|
walther@59847
|
265 |
else error "eval_binop changed"
|
walther@59847
|
266 |
;
|
walther@59847
|
267 |
val SOME (thmid, tm) = eval_binop "#mult_" op_ t thy;
|
walther@59847
|
268 |
if thmid = "#: 2 * 3 = 6" andalso term2str prop = "2 * 3 = 6" then ()
|
walther@59847
|
269 |
else error "eval_binop changed 2"
|
walther@59847
|
270 |
|
walther@59847
|
271 |
|
walther@59847
|
272 |
"-------- fun matchsub -------------------------------------------------------------------------";
|
walther@59847
|
273 |
"-------- fun matchsub -------------------------------------------------------------------------";
|
walther@59847
|
274 |
"-------- fun matchsub -------------------------------------------------------------------------";
|
walther@59847
|
275 |
if matchsub thy (str2term "(a + (b + c))") (str2term "?x + (?y + ?z)")
|
walther@59847
|
276 |
then () else error "tools.sml matchsub a + (b + c)";
|
walther@59847
|
277 |
|
walther@59847
|
278 |
if matchsub thy (str2term "(a + (b + c)) + d") (str2term "?x + (?y + ?z)")
|
walther@59847
|
279 |
then () else error "tools.sml matchsub (a + (b + c)) + d";
|
walther@59847
|
280 |
|
walther@59847
|
281 |
|
walther@59847
|
282 |
"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
|
walther@59847
|
283 |
"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
|
walther@59847
|
284 |
"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
|
walther@59847
|
285 |
"see: --------- search for Or_to_List ---";
|
walther@59847
|
286 |
case or2list @{term True} of Const ("ListC.UniversalList", _) => ()
|
walther@59847
|
287 |
| _ => error "TermC.UniversalList changed 1";
|
walther@59847
|
288 |
case or2list @{term False} of Const ("List.list.Nil", _) => ()
|
walther@59847
|
289 |
| _ => error "TermC.UniversalList changed 2";
|
walther@59847
|
290 |
val t = (str2term "x=3");
|
walther@59847
|
291 |
if term2str (or2list t) = "[x = 3]" then ()
|
walther@59847
|
292 |
else error "or2list changed";
|
walther@59847
|
293 |
val t = (str2term "x=3 | x=-3 | x=0");
|
walther@59847
|
294 |
if term2str (or2list t) = "[x = 3, x = -3, x = 0]" then ()
|
walther@59847
|
295 |
else error "HOL.eq ? HOL.disj ? changed";
|