walther@60278
|
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@60322
|
10 |
"-------- fun eval_is_atom ---------------------------------------------------------------------";
|
walther@60318
|
11 |
"-------- fun eval_is_even ---------------------------------------------------------------------";
|
walther@60387
|
12 |
"-------- fun eval_is_num ----------------------------------------------------------------------";
|
walther@60317
|
13 |
"-------- fun eval_cancel ----------------------------------------------------------------------";
|
walther@60317
|
14 |
"-------- fun eval_equ -------------------------------------------------------------------------";
|
walther@59841
|
15 |
"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
|
walther@59847
|
16 |
"-------- occurs_in ----------------------------------------------------------------------------";
|
walther@59847
|
17 |
"-------- fun eval_occurs_in -------------------------------------------------------------------";
|
walther@59847
|
18 |
"-------- fun eval_argument_of -----------------------------------------------------------------";
|
walther@59847
|
19 |
"-------- fun eval_sameFunId -------------------------------------------------------------------";
|
walther@59847
|
20 |
"-------- fun eval_filter_sameFunId ------------------------------------------------------------";
|
walther@59847
|
21 |
"-------- fun eval_boollist2sum ----------------------------------------------------------------";
|
Walther@60516
|
22 |
"-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
|
walther@59847
|
23 |
"-------- fun matchsub -------------------------------------------------------------------------";
|
walther@59847
|
24 |
"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
|
walther@59633
|
25 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
26 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
27 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
28 |
|
walther@59633
|
29 |
|
walther@60322
|
30 |
"-------- fun eval_is_atom ---------------------------------------------------------------------";
|
walther@60322
|
31 |
"-------- fun eval_is_atom ---------------------------------------------------------------------";
|
walther@60322
|
32 |
"-------- fun eval_is_atom ---------------------------------------------------------------------";
|
walther@60322
|
33 |
if is_atom @{term 0} then () else error "is_atom 0 CHANGED";
|
walther@60322
|
34 |
val eval_t = @{term "0 is_atom"};
|
walther@60322
|
35 |
case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
|
walther@60322
|
36 |
SOME ("#is_atom_0_", _) => ()
|
walther@60322
|
37 |
| _ => error "eval_is_atom 0 CHANGED";
|
walther@60322
|
38 |
|
walther@60322
|
39 |
if is_atom @{term 1} then () else error "is_atom 1 CHANGED";
|
walther@60322
|
40 |
val eval_t = @{term "1 is_atom"};
|
walther@60322
|
41 |
case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
|
walther@60322
|
42 |
SOME ("#is_atom_1_", _) => ()
|
walther@60322
|
43 |
| _ => error "eval_is_atom 1 CHANGED";
|
walther@60322
|
44 |
|
walther@60322
|
45 |
if is_atom @{term 123} then () else error "is_atom 123 CHANGED";
|
walther@60322
|
46 |
val eval_t = @{term "123 is_atom"};
|
walther@60322
|
47 |
case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
|
walther@60322
|
48 |
SOME ("#is_atom_123_", _) => ()
|
walther@60322
|
49 |
| _ => error "eval_is_atom 123 CHANGED";
|
walther@60322
|
50 |
|
walther@60322
|
51 |
if is_atom @{term abc} then () else error "is_atom abc CHANGED";
|
walther@60322
|
52 |
val eval_t = @{term "abc is_atom"};
|
walther@60322
|
53 |
case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
|
walther@60322
|
54 |
SOME ("#is_atom_abc_", _) => ()
|
walther@60322
|
55 |
| _ => error "eval_is_atom abc CHANGED";
|
walther@60322
|
56 |
|
walther@60322
|
57 |
|
walther@60318
|
58 |
"-------- fun eval_is_even ---------------------------------------------------------------------";
|
walther@60318
|
59 |
"-------- fun eval_is_even ---------------------------------------------------------------------";
|
walther@60318
|
60 |
"-------- fun eval_is_even ---------------------------------------------------------------------";
|
Walther@60565
|
61 |
val t = TermC.parse_test @{context} "2 is_even";
|
walther@60318
|
62 |
eval_is_even "aaa" "Prog_Expr.is_even" t "ccc";
|
walther@60318
|
63 |
"~~~~~ fun eval_is_even , args:"; val ((thmid:string), "Prog_Expr.is_even", (t as (Const _ $ arg)), _) =
|
walther@60318
|
64 |
("aaa", "Prog_Expr.is_even", t, "ccc");
|
walther@60318
|
65 |
(*if*) TermC.is_num arg (*then*);
|
walther@60318
|
66 |
val i = arg |> HOLogic.dest_number |> snd;
|
walther@60318
|
67 |
(*if*) even i (*then*);
|
walther@60318
|
68 |
val SOME ("aaa1_", t') =
|
walther@60318
|
69 |
SOME (TermC.mk_thmid thmid (string_of_int n) "",
|
walther@60318
|
70 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})));
|
walther@60318
|
71 |
if UnparseC.term t' = "(2 is_even) = True" then () else error "(2 is_even) = True CHANGED";
|
walther@60318
|
72 |
|
walther@60318
|
73 |
|
Walther@60565
|
74 |
val t = TermC.parse_test @{context} "3 is_even";
|
walther@60318
|
75 |
case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of
|
walther@60318
|
76 |
SOME (str, t') =>
|
walther@60318
|
77 |
if str = "aaa_" andalso UnparseC.term t' = "(3 is_even) = False" then ()
|
walther@60318
|
78 |
else error "eval_is_even (3 is_even) CHANGED 1"
|
walther@60318
|
79 |
| NONE => error "eval_is_even (3 is_even) CHANGED 2";
|
walther@60318
|
80 |
|
Walther@60565
|
81 |
val t = TermC.parse_test @{context} "a ::real";
|
walther@60318
|
82 |
val NONE =
|
walther@60318
|
83 |
eval_is_even "aaa" "Prog_Expr.is_even" t "ccc";
|
walther@60318
|
84 |
case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of
|
walther@60318
|
85 |
SOME _ => error "eval_is_even (a is_even) CHANGED"
|
walther@60318
|
86 |
| NONE => ();
|
walther@60318
|
87 |
|
walther@60318
|
88 |
|
walther@60387
|
89 |
"-------- fun eval_is_num ----------------------------------------------------------------------";
|
walther@60387
|
90 |
"-------- fun eval_is_num ----------------------------------------------------------------------";
|
walther@60387
|
91 |
"-------- fun eval_is_num ----------------------------------------------------------------------";
|
Walther@60500
|
92 |
val ctxt = Proof_Context.init_global @{theory Test}
|
Walther@60424
|
93 |
val t = TermC.parseNEW' ctxt "2 is_num";
|
Walther@60500
|
94 |
case rewrite_set_ ctxt false tval_rls t of
|
walther@60336
|
95 |
SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
|
walther@60387
|
96 |
| _ => error "2 is_num CHANGED";
|
walther@60318
|
97 |
|
Walther@60565
|
98 |
val t = TermC.parse_test @{context} "2 * x is_num";
|
walther@60387
|
99 |
val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
|
walther@60387
|
100 |
if UnparseC.term t' = "(2 * x is_num) = False" then ()
|
walther@60387
|
101 |
else error "(2 * x is_num) = False CHANGED";
|
walther@60318
|
102 |
|
Walther@60565
|
103 |
val t = TermC.parse_test @{context} "- 2 is_num";
|
walther@60387
|
104 |
val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
|
walther@60387
|
105 |
if UnparseC.term t' = "(- 2 is_num) = True" then ()
|
walther@60387
|
106 |
else error "(- 2 is_num) = False CHANGED";
|
walther@60318
|
107 |
|
Walther@60565
|
108 |
val t = TermC.parse_test @{context} "- 1 is_num";
|
walther@60387
|
109 |
val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
|
walther@60387
|
110 |
if UnparseC.term t' = "(- 1 is_num) = True" then ()
|
walther@60387
|
111 |
else error "(- 1 is_num) = False CHANGED";
|
walther@60318
|
112 |
|
Walther@60565
|
113 |
val t = TermC.parse_test @{context} "0 is_num";
|
walther@60387
|
114 |
val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
|
walther@60387
|
115 |
if UnparseC.term t' = "(0 is_num) = True" then ()
|
walther@60387
|
116 |
else error "(0 is_num) = False CHANGED";
|
walther@60318
|
117 |
|
Walther@60565
|
118 |
val t = TermC.parse_test @{context} "AA is_num";
|
walther@60387
|
119 |
val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
|
walther@60387
|
120 |
if UnparseC.term t' = "(AA is_num) = False" then ()
|
walther@60387
|
121 |
else error "(0 is_num) = False CHANGED";
|
walther@60318
|
122 |
|
walther@60318
|
123 |
|
walther@60317
|
124 |
"-------- fun eval_cancel ----------------------------------------------------------------------";
|
walther@60317
|
125 |
"-------- fun eval_cancel ----------------------------------------------------------------------";
|
walther@60317
|
126 |
"-------- fun eval_cancel ----------------------------------------------------------------------";
|
walther@60392
|
127 |
val t = @{term "- 1 / 2 :: real"};
|
walther@60392
|
128 |
val NONE = eval_cancel "cancel_" "Rings.divide_class.divide" t "";
|
walther@60392
|
129 |
"~~~~~ fun eval_cancel , args:"; val (thmid, "Rings.divide_class.divide", (t as (Const _ $ t1 $ t2))) =
|
walther@60392
|
130 |
("xxx", "Rings.divide_class.divide", t);
|
walther@60392
|
131 |
(*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*);
|
walther@60392
|
132 |
val (T, _) = HOLogic.dest_number t1;
|
walther@60392
|
133 |
val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);
|
walther@60392
|
134 |
val res_int as (d, (i1', i2')) = Eval.cancel_int (i1, i2);
|
walther@60392
|
135 |
|
walther@60392
|
136 |
(*+*)val (~1, (1, 2)) = res_int;
|
walther@60392
|
137 |
|
walther@60392
|
138 |
(*if*) abs d = 1 andalso (abs i1, abs i2) = (abs i1', abs i2') (*then*);
|
walther@60392
|
139 |
NONE (*return value*);
|
walther@60392
|
140 |
|
walther@60392
|
141 |
"-------- further examples ";
|
walther@60317
|
142 |
val t = @{term "3 / 2 :: real"};
|
walther@60317
|
143 |
val NONE = eval_cancel "cancel_" "Rings.divide_class.divide" t ""
|
walther@60317
|
144 |
|
walther@60317
|
145 |
val t = @{term "6 / 4 :: real"};
|
walther@60317
|
146 |
case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
|
walther@60317
|
147 |
SOME ("cancel_6_4", t') =>
|
walther@60317
|
148 |
if UnparseC.term t' = "6 / 4 = 3 / 2" then ()
|
walther@60317
|
149 |
else error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 1"
|
walther@60317
|
150 |
| _ => error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 2";
|
walther@60317
|
151 |
|
walther@60317
|
152 |
val t = @{term "- 6 / 4 :: real"};
|
walther@60317
|
153 |
case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
|
walther@60317
|
154 |
SOME ("cancel_~6_4", t') =>
|
walther@60317
|
155 |
if UnparseC.term t' = "- 6 / 4 = - 3 / 2" then ()
|
walther@60317
|
156 |
else error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 1"
|
walther@60317
|
157 |
| _ => error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 2";
|
walther@60317
|
158 |
|
walther@60317
|
159 |
val t = @{term "6 / - 4 :: real"};
|
walther@60317
|
160 |
case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
|
walther@60317
|
161 |
SOME ("cancel_6_~4", t') =>
|
walther@60317
|
162 |
if UnparseC.term t' = "6 / - 4 = - 3 / 2" then ()
|
walther@60317
|
163 |
else error "eval_cancel 6 / - 4 = - 3 / 2 CHANGED 1"
|
walther@60317
|
164 |
| _ => error "eval_cancel 6 / - 4 = - 3 / 2 CHANGED 2";
|
walther@60317
|
165 |
|
walther@60317
|
166 |
val t = @{term "- 6 /- 4 :: real"};
|
walther@60317
|
167 |
case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
|
walther@60317
|
168 |
SOME ("cancel_~6_~4", t') =>
|
walther@60317
|
169 |
if UnparseC.term t' = "- 6 / - 4 = 3 / 2" then ()
|
walther@60317
|
170 |
else error "eval_cancel - 6 / - 4 = 3 / 2 CHANGED 1"
|
walther@60317
|
171 |
| _ => error "eval_cancel - 6 / - 4 = 3 / 2 CHANGED 2";
|
walther@60317
|
172 |
|
walther@60317
|
173 |
val t = @{term "- (6 / 4) :: real"};
|
walther@60317
|
174 |
val NONE = eval_cancel "adhoc_thm_cancel" "Rings.divide_class.divide" t "";
|
walther@60317
|
175 |
|
walther@60317
|
176 |
|
walther@60317
|
177 |
"-------- fun eval_equ -------------------------------------------------------------------------";
|
walther@60317
|
178 |
"-------- fun eval_equ -------------------------------------------------------------------------";
|
walther@60317
|
179 |
"-------- fun eval_equ -------------------------------------------------------------------------";
|
walther@60317
|
180 |
eval_equ: string -> string -> term -> 'a -> (string * term) option;
|
walther@60317
|
181 |
|
walther@60317
|
182 |
case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (2::real)"} "" of
|
walther@60317
|
183 |
SOME
|
walther@60317
|
184 |
("#less_1_2",
|
walther@60336
|
185 |
Const (\<^const_name>\<open>Trueprop\<close>, _) $
|
walther@60336
|
186 |
(Const (\<^const_name>\<open>HOL.eq\<close>, _) $
|
walther@60336
|
187 |
(Const (\<^const_name>\<open>ord_class.less\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) $
|
walther@60336
|
188 |
(Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) $
|
walther@60336
|
189 |
Const (\<^const_name>\<open>True\<close>, _))) => ()
|
walther@60317
|
190 |
| _ => error "eval_equ 1 < 2 CHANGED";
|
walther@60317
|
191 |
|
walther@60317
|
192 |
case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (1::real)"} "" of
|
walther@60317
|
193 |
SOME
|
walther@60317
|
194 |
("#less_1_1",
|
walther@60336
|
195 |
Const (\<^const_name>\<open>Trueprop\<close>, _) $
|
walther@60336
|
196 |
(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>ord_class.less\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _)) $
|
walther@60336
|
197 |
Const (\<^const_name>\<open>False\<close>, _))) => ()
|
walther@60317
|
198 |
| _ => error "eval_equ 1 < 1 CHANGED";
|
walther@60317
|
199 |
|
walther@60317
|
200 |
|
walther@59841
|
201 |
"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
|
walther@59841
|
202 |
"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
|
walther@59841
|
203 |
"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
|
walther@59841
|
204 |
val thy = @{theory}
|
Walther@60424
|
205 |
val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge")
|
walther@59841
|
206 |
|
Walther@60565
|
207 |
val t = TermC.parse_test @{context} "x = 0";
|
Walther@60504
|
208 |
val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
|
walther@59841
|
209 |
|
Walther@60565
|
210 |
val t = TermC.parse_test @{context} "(x + 1) = (x + 1)";
|
walther@59841
|
211 |
val (Const _(*op0,t0*) $ t1 $ t2 ) = t
|
Walther@60504
|
212 |
val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
|
walther@59868
|
213 |
if UnparseC.term t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED";
|
walther@59841
|
214 |
|
Walther@60565
|
215 |
val t as Const _ $ v $ c = TermC.parse_test @{context} "1 = 0";
|
walther@59841
|
216 |
val false = variable_constant_pair (v, c);
|
Walther@60504
|
217 |
val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
|
walther@59868
|
218 |
if UnparseC.term t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED";
|
walther@59841
|
219 |
|
Walther@60565
|
220 |
val t = TermC.parse_test @{context} "0 = 0";
|
Walther@60504
|
221 |
val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
|
walther@59868
|
222 |
if UnparseC.term t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";
|
walther@59847
|
223 |
|
walther@59847
|
224 |
|
walther@59847
|
225 |
"-------- occurs_in ----------------------------------------------------------------------------";
|
walther@59847
|
226 |
"-------- occurs_in ----------------------------------------------------------------------------";
|
walther@59847
|
227 |
"-------- occurs_in ----------------------------------------------------------------------------";
|
walther@60317
|
228 |
val t = @{term "x::real"};
|
walther@59847
|
229 |
if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";
|
walther@59847
|
230 |
|
Walther@60565
|
231 |
val t = TermC.parse_test @{context} "x occurs_in x";
|
walther@60278
|
232 |
val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs_in" t 0;
|
walther@59868
|
233 |
if UnparseC.term t' = "x occurs_in x = True" then ()
|
walther@59847
|
234 |
else error "x occurs_in x = True ..changed";
|
walther@59847
|
235 |
|
walther@59847
|
236 |
"------- some_occur_in";
|
walther@60317
|
237 |
if some_occur_in [@{term "c::real"}, @{term "c_2::real"}] @{term "a + b + c::real"} then ()
|
walther@60317
|
238 |
else error "";
|
walther@60317
|
239 |
|
walther@60317
|
240 |
val t = @{term "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2"};
|
walther@60317
|
241 |
val SOME (str, t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0;
|
walther@60317
|
242 |
if UnparseC.term t' =
|
walther@60317
|
243 |
"some_of [c, c_2, c_3,\n c_4] occur_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 =\nTrue" then ()
|
walther@60317
|
244 |
else error "atools.sml: some_occur_in true";
|
walther@60317
|
245 |
|
walther@60317
|
246 |
val t = @{term "some_of [c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2"};
|
walther@60278
|
247 |
val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0;
|
walther@59868
|
248 |
if UnparseC.term t' =
|
walther@60317
|
249 |
"some_of [c_3, c_4] occur_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False" then ()
|
walther@59847
|
250 |
else error "atools.sml: some_occur_in false";
|
walther@59847
|
251 |
|
walther@59847
|
252 |
|
walther@59847
|
253 |
"-------- fun eval_occurs_in -------------------------------------------------------------------";
|
walther@59847
|
254 |
"-------- fun eval_occurs_in -------------------------------------------------------------------";
|
walther@59847
|
255 |
"-------- fun eval_occurs_in -------------------------------------------------------------------";
|
Walther@60424
|
256 |
val v = TermC.parseNEW' ctxt "x";
|
Walther@60424
|
257 |
val t = TermC.parseNEW' ctxt "1";
|
walther@59847
|
258 |
if occurs_in v t then error "factor_right_deg (1) x ..changed" else ();
|
walther@59847
|
259 |
|
Walther@60424
|
260 |
val v = TermC.parseNEW' ctxt "AA";
|
Walther@60424
|
261 |
val t = TermC.parseNEW' ctxt "1";
|
walther@59847
|
262 |
if occurs_in v t then error "factor_right_deg (1) AA ..changed" else ();
|
walther@59847
|
263 |
|
walther@59847
|
264 |
(*----------*)
|
Walther@60424
|
265 |
val v = TermC.parseNEW' ctxt "x";
|
Walther@60424
|
266 |
val t = TermC.parseNEW' ctxt "a*b+c";
|
walther@59847
|
267 |
if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else ();
|
walther@59847
|
268 |
|
Walther@60424
|
269 |
val v = TermC.parseNEW' ctxt "AA";
|
Walther@60424
|
270 |
val t = TermC.parseNEW' ctxt "a*b+c";
|
walther@59847
|
271 |
if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else ();
|
walther@59847
|
272 |
|
walther@59847
|
273 |
(*----------*)
|
Walther@60424
|
274 |
val v = TermC.parseNEW' ctxt "x";
|
Walther@60424
|
275 |
val t = TermC.parseNEW' ctxt "a*x+c";
|
walther@59847
|
276 |
if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed";
|
walther@59847
|
277 |
|
Walther@60424
|
278 |
val v = TermC.parseNEW' ctxt "AA";
|
Walther@60424
|
279 |
val t = TermC.parseNEW' ctxt "a*AA+c";
|
walther@59847
|
280 |
if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed";
|
walther@59847
|
281 |
|
walther@59847
|
282 |
(*----------*)
|
Walther@60424
|
283 |
val v = TermC.parseNEW' ctxt "x";
|
Walther@60424
|
284 |
val t = TermC.parseNEW' ctxt "(a*b+c)*x \<up> 7";
|
walther@60242
|
285 |
if occurs_in v t then () else error "factor_right_deg (a*b+c)*x \<up> 7) x ..changed";
|
walther@59847
|
286 |
|
Walther@60424
|
287 |
val v = TermC.parseNEW' ctxt "AA";
|
Walther@60424
|
288 |
val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
|
walther@60242
|
289 |
if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA \<up> 7) AA ..changed";
|
walther@59847
|
290 |
|
walther@59847
|
291 |
(*----------*)
|
Walther@60424
|
292 |
val v = TermC.parseNEW' ctxt "x";
|
Walther@60424
|
293 |
val t = TermC.parseNEW' ctxt "x \<up> 7";
|
walther@60242
|
294 |
if occurs_in v t then () else error "factor_right_deg (x \<up> 7) x ..changed";
|
walther@59847
|
295 |
|
Walther@60424
|
296 |
val v = TermC.parseNEW' ctxt "AA";
|
Walther@60424
|
297 |
val t = TermC.parseNEW' ctxt "AA \<up> 7";
|
walther@60242
|
298 |
if occurs_in v t then () else error "factor_right_deg (AA \<up> 7) AA ..changed";
|
walther@59847
|
299 |
|
walther@59847
|
300 |
(*----------*)
|
Walther@60424
|
301 |
val v = TermC.parseNEW' ctxt "x";
|
Walther@60424
|
302 |
val t = TermC.parseNEW' ctxt "(a*b+c)*x";
|
walther@59847
|
303 |
if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed";
|
walther@59847
|
304 |
|
Walther@60424
|
305 |
val v = TermC.parseNEW' ctxt "AA";
|
Walther@60424
|
306 |
val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
|
walther@59847
|
307 |
if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed";
|
walther@59847
|
308 |
|
walther@59847
|
309 |
(*----------*)
|
Walther@60424
|
310 |
val v = TermC.parseNEW' ctxt "x";
|
Walther@60424
|
311 |
val t = TermC.parseNEW' ctxt "(a*b+x)*x";
|
walther@59847
|
312 |
if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed";
|
walther@59847
|
313 |
|
Walther@60424
|
314 |
val v = TermC.parseNEW' ctxt "AA";
|
Walther@60424
|
315 |
val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
|
walther@59847
|
316 |
if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed";
|
walther@59847
|
317 |
|
walther@59847
|
318 |
(*----------*)
|
Walther@60424
|
319 |
val v = TermC.parseNEW' ctxt "x";
|
Walther@60424
|
320 |
val t = TermC.parseNEW' ctxt "x";
|
walther@59847
|
321 |
if occurs_in v t then () else error "factor_right_deg (x) x ..changed";
|
walther@59847
|
322 |
|
Walther@60424
|
323 |
val v = TermC.parseNEW' ctxt "AA";
|
Walther@60424
|
324 |
val t = TermC.parseNEW' ctxt "AA";
|
walther@59847
|
325 |
if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed";
|
walther@59847
|
326 |
|
walther@59847
|
327 |
(*----------*)
|
Walther@60424
|
328 |
val v = TermC.parseNEW' ctxt "x";
|
Walther@60424
|
329 |
val t = TermC.parseNEW' ctxt "ab - (a*b)*x";
|
walther@59847
|
330 |
if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed";
|
walther@59847
|
331 |
|
Walther@60424
|
332 |
val v = TermC.parseNEW' ctxt "AA";
|
Walther@60424
|
333 |
val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
|
walther@59847
|
334 |
if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed";
|
walther@59847
|
335 |
|
walther@59847
|
336 |
|
walther@59847
|
337 |
"---------fun eval_argument_of -----------------------------------------------------------------";
|
walther@59847
|
338 |
"---------fun eval_argument_of -----------------------------------------------------------------";
|
walther@59847
|
339 |
"---------fun eval_argument_of -----------------------------------------------------------------";
|
Walther@60565
|
340 |
val t = TermC.parse_test @{context} "argument_in (M_b x)";
|
walther@60278
|
341 |
val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument_in" t 0;
|
walther@59868
|
342 |
if UnparseC.term t' = "(argument_in M_b x) = x" then ()
|
walther@59847
|
343 |
else error "atools.sml:(argument_in M_b x) = x ???";
|
walther@59847
|
344 |
|
walther@59847
|
345 |
|
walther@59847
|
346 |
"---------fun eval_sameFunId -------------------------------------------------------------------";
|
walther@59847
|
347 |
"---------fun eval_sameFunId -------------------------------------------------------------------";
|
walther@59847
|
348 |
"---------fun eval_sameFunId -------------------------------------------------------------------";
|
walther@60317
|
349 |
val t = @{term "M_b L"}; TermC.atomty t;
|
walther@60317
|
350 |
val t as f1 $ _ = @{term "M_b L"};
|
walther@60336
|
351 |
val t as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _ = @{term "M_b x = c + L*x"};
|
walther@59847
|
352 |
f1 = f2 (*true*);
|
walther@60336
|
353 |
val (p as Const (\<^const_name>\<open>sameFunId\<close>, _) $
|
walther@59847
|
354 |
(f1 $ _) $
|
wenzelm@60309
|
355 |
(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _)) =
|
walther@60317
|
356 |
@{term "sameFunId (M_b L) (M_b x = c + L*x)"};
|
walther@59847
|
357 |
f1 = f2 (*true*);
|
walther@59847
|
358 |
eval_sameFunId "" "Prog_Expr.sameFunId"
|
walther@60317
|
359 |
(@{term "sameFunId (M_b L) (M_b x = c + L*x)"})""(*true*);
|
walther@59847
|
360 |
eval_sameFunId "" "Prog_Expr.sameFunId"
|
walther@60317
|
361 |
(@{term "sameFunId (M_b L) ( y' x = c + L*x)"})""(*false*);
|
walther@59847
|
362 |
eval_sameFunId "" "Prog_Expr.sameFunId"
|
walther@60317
|
363 |
(@{term "sameFunId (M_b L) ( y x = c + L*x)"})""(*false*);
|
walther@59847
|
364 |
eval_sameFunId "" "Prog_Expr.sameFunId"
|
walther@60317
|
365 |
(@{term "sameFunId ( y L) (M_b x = c + L*x)"})""(*false*);
|
walther@59847
|
366 |
eval_sameFunId "" "Prog_Expr.sameFunId"
|
walther@60317
|
367 |
(@{term "sameFunId ( y L) ( y x = c + L*x)"})""(*true*);
|
walther@59847
|
368 |
|
walther@59847
|
369 |
|
walther@59847
|
370 |
"---------fun eval_filter_sameFunId ------------------------------------------------------------";
|
walther@59847
|
371 |
"---------fun eval_filter_sameFunId ------------------------------------------------------------";
|
walther@59847
|
372 |
"---------fun eval_filter_sameFunId ------------------------------------------------------------";
|
walther@60317
|
373 |
val flhs as (fid $ _) = @{term "y' L"};
|
walther@60317
|
374 |
val fs = @{term "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};
|
walther@60336
|
375 |
val (p as Const (\<^const_name>\<open>filter_sameFunId\<close>,_) $ (fid $ _) $ fs) =
|
walther@60317
|
376 |
@{term "filter_sameFunId (y' L) [M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};
|
walther@60278
|
377 |
val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter_sameFunId" p "";
|
walther@59868
|
378 |
if UnparseC.term 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
|
379 |
else error "atools.slm diff.behav. in filter_sameFunId";
|
walther@59847
|
380 |
|
walther@59847
|
381 |
|
walther@59847
|
382 |
"---------fun eval_boollist2sum ----------------------------------------------------------------";
|
walther@59847
|
383 |
"---------fun eval_boollist2sum ----------------------------------------------------------------";
|
walther@59847
|
384 |
"---------fun eval_boollist2sum ----------------------------------------------------------------";
|
walther@60336
|
385 |
fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
|
walther@59868
|
386 |
| lhs t = error("lhs called with (" ^ UnparseC.term t ^ ")");
|
walther@60242
|
387 |
"----------- \<up> redefined due to overwritten identifier -----------";
|
walther@60317
|
388 |
val u_ = @{term "[]"};
|
walther@60317
|
389 |
val u_ = @{term "[b1 = k - 2*q]"};
|
walther@60317
|
390 |
val u_ = @{term "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
|
walther@59847
|
391 |
val ut_ = isalist2list u_;
|
walther@59847
|
392 |
val sum_ = map lhs ut_;
|
walther@59847
|
393 |
val t = list2sum sum_;
|
walther@59868
|
394 |
UnparseC.term t;
|
walther@59847
|
395 |
|
walther@60317
|
396 |
val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
|
walther@60317
|
397 |
case t of
|
walther@60336
|
398 |
Const (\<^const_name>\<open>boollist2sum\<close>, _) $
|
walther@60336
|
399 |
(Const (\<^const_name>\<open>Cons\<close>, _) $
|
walther@60336
|
400 |
(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b1", _) $ _ ) $
|
walther@60336
|
401 |
(Const (\<^const_name>\<open>Cons\<close>, _) $
|
walther@60336
|
402 |
(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b2", _) $ _ ) $
|
walther@60336
|
403 |
(Const (\<^const_name>\<open>Cons\<close>, _) $
|
walther@60336
|
404 |
(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b3", _) $ _ ) $
|
walther@60336
|
405 |
(Const (\<^const_name>\<open>Cons\<close>, _) $
|
walther@60336
|
406 |
(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b4", _) $ _ ) $
|
walther@60336
|
407 |
Const (\<^const_name>\<open>Nil\<close>, _))))) => ()
|
walther@60317
|
408 |
| _ => error "boollist2sum CHANGED";
|
walther@59847
|
409 |
val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t "";
|
walther@59868
|
410 |
if UnparseC.term 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
|
411 |
else error "atools.sml diff.behav. in eval_boollist2sum";
|
walther@59847
|
412 |
|
walther@59852
|
413 |
val srls_ = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty
|
walther@59878
|
414 |
[Eval ("Prog_Expr.boollist2sum", eval_boollist2sum "")];
|
walther@60317
|
415 |
val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
|
Walther@60500
|
416 |
case rewrite_set_ ctxt false srls_ t of SOME _ => ()
|
walther@59847
|
417 |
| _ => error "atools.sml diff.rewrite boollist2sum";
|
walther@59847
|
418 |
|
walther@59847
|
419 |
|
Walther@60516
|
420 |
"-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
|
Walther@60516
|
421 |
"-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
|
Walther@60516
|
422 |
"-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
|
walther@59847
|
423 |
val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
|
Walther@60424
|
424 |
val t = TermC.parseNEW' ctxt "2 * (3::real)";
|
Walther@60504
|
425 |
(*val SOME (thmid,t') = *)get_pair ctxt op_ ef t;
|
walther@59847
|
426 |
;
|
walther@60401
|
427 |
"~~~~~ fun get_pair, args:"; val(*3*)(thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
|
walther@59847
|
428 |
(thy, op_, ef, t);
|
walther@60401
|
429 |
(*if*) op_ = op0; (*then*)
|
walther@60401
|
430 |
val popt =
|
Walther@60504
|
431 |
ef op_ t ctxt;
|
Walther@60516
|
432 |
"~~~~~ fun Calc_Binop.numeric , args:"; val ((_ : string), (_: string),
|
walther@60401
|
433 |
(t as (Const (op0, _) $ t1 $ t2)), thy) =
|
walther@60401
|
434 |
("#mult_", op_, t, thy);
|
walther@60401
|
435 |
val Const (c, _) $ t1 $ t2 = (* binary \<circ> n1 \<circ> n2 *)
|
walther@60401
|
436 |
(*case*) t (*of*);
|
Walther@60516
|
437 |
(*if*) Calc_Binop.is c andalso is_num t1 andalso is_num t2 (*then*);
|
Walther@60516
|
438 |
val res = Calc_Binop.simplify ctxt t;
|
walther@60401
|
439 |
val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
|
walther@60401
|
440 |
SOME ("#: " ^ UnparseC.term prop, prop) (*return value*);
|
walther@59847
|
441 |
;
|
walther@60401
|
442 |
if "#: " ^ UnparseC.term prop = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
|
walther@59847
|
443 |
else error "eval_binop changed"
|
walther@59847
|
444 |
;
|
Walther@60516
|
445 |
val SOME (thmid, tm) = Calc_Binop.numeric "#mult_" op_ t ctxt;
|
walther@59868
|
446 |
if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
|
walther@59847
|
447 |
else error "eval_binop changed 2"
|
walther@59847
|
448 |
|
walther@59847
|
449 |
|
walther@59847
|
450 |
"-------- fun matchsub -------------------------------------------------------------------------";
|
walther@59847
|
451 |
"-------- fun matchsub -------------------------------------------------------------------------";
|
walther@59847
|
452 |
"-------- fun matchsub -------------------------------------------------------------------------";
|
Walther@60565
|
453 |
if matchsub thy (TermC.parse_test @{context} "(a + (b + c))") (TermC.parse_patt_test @{theory} "?x + (?y + ?z)")
|
walther@59847
|
454 |
then () else error "tools.sml matchsub a + (b + c)";
|
walther@59847
|
455 |
|
Walther@60565
|
456 |
if matchsub thy (TermC.parse_test @{context} "(a + (b + c)) + d") (TermC.parse_patt_test @{theory} "?x + (?y + ?z)")
|
walther@59847
|
457 |
then () else error "tools.sml matchsub (a + (b + c)) + d";
|
walther@59847
|
458 |
|
walther@59847
|
459 |
|
walther@59847
|
460 |
"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
|
walther@59847
|
461 |
"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
|
walther@59847
|
462 |
"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
|
walther@59847
|
463 |
"see: --------- search for Or_to_List ---";
|
walther@60336
|
464 |
case or2list @{term True} of Const (\<^const_name>\<open>UniversalList\<close>, _) => ()
|
walther@59847
|
465 |
| _ => error "TermC.UniversalList changed 1";
|
wenzelm@60309
|
466 |
case or2list @{term False} of Const (\<^const_name>\<open>Nil\<close>, _) => ()
|
walther@59847
|
467 |
| _ => error "TermC.UniversalList changed 2";
|
Walther@60565
|
468 |
val t = (TermC.parse_test @{context} "x=3");
|
walther@59868
|
469 |
if UnparseC.term (or2list t) = "[x = 3]" then ()
|
walther@59847
|
470 |
else error "or2list changed";
|
Walther@60565
|
471 |
val t = (TermC.parse_test @{context} "x=3 | x=-3 | x=0");
|
walther@60317
|
472 |
if UnparseC.term (or2list t) = "[x = 3, x = - 3, x = 0]" then ()
|
walther@59847
|
473 |
else error "HOL.eq ? HOL.disj ? changed";
|