erott@37872
|
1 |
(* cut and paste for math.tex
|
erott@37872
|
2 |
*)
|
erott@37872
|
3 |
|
erott@37872
|
4 |
(*2.2. *)
|
erott@37872
|
5 |
"a + b * 3";
|
erott@37872
|
6 |
str2term "a + b * 3";
|
erott@37872
|
7 |
val term = str2term "a + b * 3";
|
erott@37872
|
8 |
atomt term;
|
erott@37872
|
9 |
atomty term;
|
erott@37872
|
10 |
|
erott@37872
|
11 |
(*2.3. Theories and parsing*)
|
erott@37872
|
12 |
|
erott@37872
|
13 |
> Isac.thy;
|
erott@37872
|
14 |
val it =
|
erott@37872
|
15 |
{ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
|
erott@37872
|
16 |
Sum_Type, Relation, Record, Inductive, Transitive_Closure,
|
erott@37872
|
17 |
Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
|
erott@37872
|
18 |
SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
|
erott@37872
|
19 |
Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
|
erott@37872
|
20 |
IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
|
erott@37872
|
21 |
Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
|
erott@37872
|
22 |
RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
|
erott@37872
|
23 |
Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
|
erott@37872
|
24 |
Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
|
erott@37872
|
25 |
Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
|
erott@37872
|
26 |
Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
|
erott@37872
|
27 |
AlgEin, Test, Isac} : Theory.theory
|
erott@37872
|
28 |
|
erott@37872
|
29 |
Group.thy
|
erott@37872
|
30 |
suche nach '*' Link: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html
|
erott@37872
|
31 |
locale semigroup =
|
erott@37872
|
32 |
fixes f :: "'a => 'a => 'a" (infixl "*" 70)
|
erott@37872
|
33 |
assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
|
erott@37872
|
34 |
|
erott@37872
|
35 |
> parse;
|
erott@37872
|
36 |
val it = fn : Theory.theory -> string -> Thm.cterm Library.option
|
erott@37872
|
37 |
|
erott@37872
|
38 |
|
erott@37872
|
39 |
|
erott@37872
|
40 |
> (*-1-*);
|
erott@37872
|
41 |
> parse HOL.thy "2^^^3";
|
erott@37872
|
42 |
*** Inner lexical error at: "^^^3"
|
erott@37872
|
43 |
val it = None : Thm.cterm Library.option
|
erott@37872
|
44 |
> (*-2-*);
|
erott@37872
|
45 |
> parse HOL.thy "d_d x (a + x)";
|
erott@37872
|
46 |
val it = None : Thm.cterm Library.option
|
erott@37872
|
47 |
> (*-3-*);
|
erott@37872
|
48 |
> parse Rational.thy "2^^^3";
|
erott@37872
|
49 |
val it = Some "2 ^^^ 3" : Thm.cterm Library.option
|
erott@37872
|
50 |
> (*-4-*);
|
erott@37872
|
51 |
val Some t4 = parse Rational.thy "d_d x (a + x)";
|
erott@37872
|
52 |
val t4 = "d_d x (a + x)" : Thm.cterm
|
erott@37872
|
53 |
> (*-5-*);
|
erott@37872
|
54 |
val Some t5 = parse Diff.thy "d_d x (a + x)";
|
erott@37872
|
55 |
val t5 = "d_d x (a + x)" : Thm.cterm
|
erott@37872
|
56 |
|
erott@37872
|
57 |
|
erott@37872
|
58 |
> term_of;
|
erott@37872
|
59 |
val it = fn : Thm.cterm -> Term.term
|
erott@37872
|
60 |
> term_of t4;
|
erott@37872
|
61 |
val it =
|
erott@37872
|
62 |
Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
|
erott@37872
|
63 |
Free ("x", "RealDef.real") $
|
erott@37872
|
64 |
(Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
|
erott@37872
|
65 |
Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
|
erott@37872
|
66 |
: Term.term
|
erott@37872
|
67 |
> term_of t5;
|
erott@37872
|
68 |
val it =
|
erott@37872
|
69 |
Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
|
erott@37872
|
70 |
Free ("x", "RealDef.real") $
|
erott@37872
|
71 |
(Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
|
erott@37872
|
72 |
Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
|
erott@37872
|
73 |
: Term.term
|
erott@37872
|
74 |
|
erott@37872
|
75 |
> print_depth;
|
erott@37872
|
76 |
val it = fn : int -> unit
|
erott@37872
|
77 |
|
erott@37872
|
78 |
|
erott@37872
|
79 |
|
erott@37872
|
80 |
|
erott@37872
|
81 |
|
erott@37872
|
82 |
> (*-4-*) val thy = Rational.thy;
|
erott@37872
|
83 |
val thy =
|
erott@37872
|
84 |
{ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
|
erott@37872
|
85 |
Sum_Type, Relation, Record, Inductive, Transitive_Closure,
|
erott@37872
|
86 |
Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
|
erott@37872
|
87 |
SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
|
erott@37872
|
88 |
Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
|
erott@37872
|
89 |
IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
|
erott@37872
|
90 |
Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
|
erott@37872
|
91 |
RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
|
erott@37872
|
92 |
Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
|
erott@37872
|
93 |
Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
|
erott@37872
|
94 |
: Theory.theory
|
erott@37872
|
95 |
> ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
|
erott@37872
|
96 |
|
erott@37872
|
97 |
***
|
erott@37872
|
98 |
*** Free (d_d, [real, real] => real)
|
erott@37872
|
99 |
*** . Free (x, real)
|
erott@37872
|
100 |
*** . Const (op +, [real, real] => real)
|
erott@37872
|
101 |
*** . . Free (a, real)
|
erott@37872
|
102 |
*** . . Free (x, real)
|
erott@37872
|
103 |
***
|
erott@37872
|
104 |
|
erott@37872
|
105 |
val it = () : unit
|
erott@37872
|
106 |
> (*-5-*) val thy = Diff.thy;
|
erott@37872
|
107 |
val thy =
|
erott@37872
|
108 |
{ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
|
erott@37872
|
109 |
Sum_Type, Relation, Record, Inductive, Transitive_Closure,
|
erott@37872
|
110 |
Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
|
erott@37872
|
111 |
SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
|
erott@37872
|
112 |
Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
|
erott@37872
|
113 |
IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
|
erott@37872
|
114 |
Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
|
erott@37872
|
115 |
RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
|
erott@37872
|
116 |
Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,
|
erott@37872
|
117 |
Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,
|
erott@37872
|
118 |
Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
|
erott@37872
|
119 |
PolyEq, LogExp, Diff} : Theory.theory
|
erott@37872
|
120 |
|
erott@37872
|
121 |
> ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
|
erott@37872
|
122 |
|
erott@37872
|
123 |
***
|
erott@37872
|
124 |
*** Const (Diff.d_d, [real, real] => real)
|
erott@37872
|
125 |
*** . Free (x, real)
|
erott@37872
|
126 |
*** . Const (op +, [real, real] => real)
|
erott@37872
|
127 |
*** . . Free (a, real)
|
erott@37872
|
128 |
*** . . Free (x, real)
|
erott@37872
|
129 |
***
|
erott@37872
|
130 |
|
erott@37872
|
131 |
val it = () : unit
|
erott@37872
|
132 |
|
erott@37872
|
133 |
|
erott@37872
|
134 |
|
erott@37872
|
135 |
> print_depth 1;
|
erott@37872
|
136 |
val it = () : unit
|
erott@37872
|
137 |
> term_of t4;
|
erott@37872
|
138 |
val it =
|
erott@37872
|
139 |
Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ ...
|
erott@37872
|
140 |
: Term.term
|
erott@37872
|
141 |
|
erott@37872
|
142 |
|
erott@37872
|
143 |
> print_depth 1;
|
erott@37872
|
144 |
val it = () : unit
|
erott@37872
|
145 |
> term_of t5;
|
erott@37872
|
146 |
val it =
|
erott@37872
|
147 |
Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
|
erott@37872
|
148 |
... : Term.term
|
erott@37872
|
149 |
|
erott@37872
|
150 |
|
erott@37872
|
151 |
|
erott@37872
|
152 |
-------------------------------------------ALT...
|
erott@37872
|
153 |
explode it;
|
erott@37872
|
154 |
\footnote{
|
erott@37872
|
155 |
print_depth 9;
|
erott@37872
|
156 |
explode "a + b * 3";
|
erott@37872
|
157 |
}
|
erott@37872
|
158 |
|
erott@37872
|
159 |
(*unschoen*)
|
erott@37872
|
160 |
|
erott@37872
|
161 |
-------------------------------------------ALT...
|
erott@37872
|
162 |
HOL.thy;
|
erott@37872
|
163 |
parse;
|
erott@37872
|
164 |
parse thy "a + b * 3";
|
erott@37872
|
165 |
val t = (term_of o the) it;
|
erott@37872
|
166 |
term_of;
|
erott@37872
|
167 |
|
erott@37872
|
168 |
(*2.3. Displaying terms*)
|
erott@37872
|
169 |
print_depth;
|
erott@37872
|
170 |
////Compiler.Control.Print.printDepth;
|
erott@37872
|
171 |
? Compiler.Control.Print.printDepth:= 2;
|
erott@37872
|
172 |
t;
|
erott@37872
|
173 |
?Compiler.Control.Print.printDepth:= 6;
|
erott@37872
|
174 |
t;
|
erott@37872
|
175 |
?Compiler.Control.Print.printLength;
|
erott@37872
|
176 |
?Compiler.Control.Print.stringDepth;
|
erott@37872
|
177 |
atomt;
|
erott@37872
|
178 |
atomt t;
|
erott@37872
|
179 |
atomty;
|
erott@37872
|
180 |
atomty thy t;
|
erott@37872
|
181 |
(*Give it a try: the mathematics knowledge grows*)
|
erott@37872
|
182 |
parse HOL.thy "2^^^3";
|
erott@37872
|
183 |
parse HOL.thy "d_d x (a + x)";
|
erott@37872
|
184 |
?parse RatArith.thy "#2^^^#3";
|
erott@37872
|
185 |
?parse RatArith.thy "d_d x (a + x)";
|
erott@37872
|
186 |
parse Differentiate.thy "d_d x (a + x)";
|
erott@37872
|
187 |
?parse Differentiate.thy "#2^^^#3";
|
erott@37872
|
188 |
(*don't trust the string representation*)
|
erott@37872
|
189 |
?val thy = RatArith.thy;
|
erott@37872
|
190 |
((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
|
erott@37872
|
191 |
?val thy = Differentiate.thy;
|
erott@37872
|
192 |
((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
|
erott@37872
|
193 |
|
erott@37872
|
194 |
(*2.4. Converting terms*)
|
erott@37872
|
195 |
term_of;
|
erott@37872
|
196 |
the;
|
erott@37872
|
197 |
val t = (term_of o the o (parse thy)) "a + b * 3";
|
erott@37872
|
198 |
|
erott@37872
|
199 |
sign_of;
|
erott@37872
|
200 |
cterm_of;
|
erott@37872
|
201 |
val ct = cterm_of (sign_of thy) t;
|
erott@37872
|
202 |
|
erott@37872
|
203 |
Sign.string_of_term;
|
erott@37872
|
204 |
Sign.string_of_term (sign_of thy) t;
|
erott@37872
|
205 |
|
erott@37872
|
206 |
string_of_cterm;
|
erott@37872
|
207 |
string_of_cterm ct;
|
erott@37872
|
208 |
|
erott@37872
|
209 |
(*2.5. Theorems *)
|
erott@37872
|
210 |
?theorem' := overwritel (!theorem',
|
erott@37872
|
211 |
[("diff_const",num_str diff_const)
|
erott@37872
|
212 |
]);
|
erott@37872
|
213 |
|
erott@37872
|
214 |
(** 3. Rewriting **)
|
erott@37872
|
215 |
(*3.1. The arguments for rewriting*)
|
erott@37872
|
216 |
HOL.thy;
|
erott@37872
|
217 |
"HOL.thy" : theory';
|
erott@37872
|
218 |
sqrt_right;
|
erott@37872
|
219 |
"sqrt_right" : rew_ord';
|
erott@37872
|
220 |
eval_rls;
|
erott@37872
|
221 |
"eval_rls" : rls';
|
erott@37872
|
222 |
diff_sum;
|
erott@37872
|
223 |
("diff_sum", "") : thm';
|
erott@37872
|
224 |
|
erott@37872
|
225 |
(*3.2. The functions for rewriting*)
|
erott@37872
|
226 |
rewrite_;
|
erott@37872
|
227 |
rewrite;
|
erott@37872
|
228 |
|
erott@37872
|
229 |
> val thy' = "Diff.thy";
|
erott@37872
|
230 |
val thy' = "Diff.thy" : string
|
erott@37872
|
231 |
> val ct = "d_d x (a * 3 + b)";
|
erott@37872
|
232 |
val ct = "d_d x (a * 3 + b)" : string
|
erott@37872
|
233 |
> val thm = ("diff_sum","");
|
erott@37872
|
234 |
val thm = ("diff_sum", "") : string * string
|
erott@37872
|
235 |
> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
|
erott@37872
|
236 |
[("bdv","x::real")] thm ct;
|
erott@37872
|
237 |
val ct = "d_d x (a * 3) + d_d x b" : cterm'
|
erott@37872
|
238 |
> val thm = ("diff_prod_const","");
|
erott@37872
|
239 |
val thm = ("diff_prod_const", "") : string * string
|
erott@37872
|
240 |
> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
|
erott@37872
|
241 |
[("bdv","x::real")] thm ct;
|
erott@37872
|
242 |
val ct = "a * d_d x 3 + d_d x b" : cterm'
|
erott@37872
|
243 |
|
erott@37872
|
244 |
|
erott@37872
|
245 |
|
erott@37872
|
246 |
> val thy' = "Diff.thy";
|
erott@37872
|
247 |
val thy' = "Diff.thy" : string
|
erott@37872
|
248 |
> val ct = "d_d x (a + a * (2 + b))";
|
erott@37872
|
249 |
val ct = "d_d x (a + a * (2 + b))" : string
|
erott@37872
|
250 |
> val thm = ("diff_sum","");
|
erott@37872
|
251 |
val thm = ("diff_sum", "") : string * string
|
erott@37872
|
252 |
> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
|
erott@37872
|
253 |
[("bdv","x::real")] thm ct;
|
erott@37872
|
254 |
val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'
|
erott@37872
|
255 |
|
erott@37872
|
256 |
> val thm = ("diff_prod_const","");
|
erott@37872
|
257 |
val thm = ("diff_prod_const", "") : string * string
|
erott@37872
|
258 |
> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
|
erott@37872
|
259 |
[("bdv","x::real")] thm ct;
|
erott@37872
|
260 |
val ct = "d_d x a + a * d_d x (2 + b)" : cterm'
|
erott@37872
|
261 |
|
erott@37872
|
262 |
|
erott@37872
|
263 |
|
erott@37872
|
264 |
(*Give it a try: rewriting*)
|
erott@37872
|
265 |
val thy' = "Diff.thy";
|
erott@37872
|
266 |
val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
|
erott@37872
|
267 |
val thm = ("diff_sum","");
|
erott@37872
|
268 |
val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct;
|
erott@37872
|
269 |
val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct;
|
erott@37872
|
270 |
val thm = ("diff_prod_const","");
|
erott@37872
|
271 |
val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct;
|
erott@37872
|
272 |
(*Give it a try: conditional rewriting*)
|
erott@37872
|
273 |
val thy' = "Isac.thy";
|
erott@37872
|
274 |
val ct' = "3 * a + 2 * (a + 1)";
|
erott@37872
|
275 |
val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n");
|
erott@37872
|
276 |
(*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
|
erott@37872
|
277 |
val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1");
|
erott@37872
|
278 |
?(*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
|
erott@37872
|
279 |
?val thm' = ("rcollect_right",
|
erott@37872
|
280 |
"[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n");
|
erott@37872
|
281 |
?(*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
|
erott@37872
|
282 |
?(*4*) val Some (ct',_) = calculate thy' "plus" ct';
|
erott@37872
|
283 |
?(*5*) val Some (ct',_) = calculate thy' "times" ct';
|
erott@37872
|
284 |
|
erott@37872
|
285 |
(*Give it a try: functional programming*)
|
erott@37872
|
286 |
val thy' = "InsSort.thy";
|
erott@37872
|
287 |
val ct = "sort [#1,#3,#2]" : cterm';
|
erott@37872
|
288 |
|
erott@37872
|
289 |
val thm = ("sort_def","");
|
erott@37872
|
290 |
?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
|
erott@37872
|
291 |
|
erott@37872
|
292 |
val thm = ("foldr_rec","");
|
erott@37872
|
293 |
?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
|
erott@37872
|
294 |
|
erott@37872
|
295 |
val thm = ("ins_base","");
|
erott@37872
|
296 |
?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
|
erott@37872
|
297 |
|
erott@37872
|
298 |
val thm = ("foldr_rec","");
|
erott@37872
|
299 |
?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
|
erott@37872
|
300 |
|
erott@37872
|
301 |
val thm = ("ins_rec","");
|
erott@37872
|
302 |
?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
|
erott@37872
|
303 |
|
erott@37872
|
304 |
?val (ct,_) = the (calculate thy' "le" ct);
|
erott@37872
|
305 |
|
erott@37872
|
306 |
val thm = ("if_True","(if True then ?x else ?y) = ?x");
|
erott@37872
|
307 |
?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
|
erott@37872
|
308 |
|
erott@37872
|
309 |
(*3.3. Variants of rewriting*)
|
erott@37872
|
310 |
rewrite_inst_;
|
erott@37872
|
311 |
rewrite_inst;
|
erott@37872
|
312 |
|
erott@37872
|
313 |
rewrite_set_;
|
erott@37872
|
314 |
rewrite_set;
|
erott@37872
|
315 |
|
erott@37872
|
316 |
rewrite_set_inst_;
|
erott@37872
|
317 |
rewrite_set_inst;
|
erott@37872
|
318 |
|
erott@37872
|
319 |
toggle;
|
erott@37872
|
320 |
toggle trace_rewrite;
|
erott@37872
|
321 |
|
erott@37872
|
322 |
(*3.4. Rule sets*)
|
erott@37872
|
323 |
sym;
|
erott@37872
|
324 |
rearrange_assoc;
|
erott@37872
|
325 |
|
erott@37872
|
326 |
(*Give it a try: remove parentheses*)
|
erott@37872
|
327 |
?val ct = (string_of_cterm o the o (parse RatArith.thy))
|
erott@37872
|
328 |
"a + (b * (c * d) + e)";
|
erott@37872
|
329 |
?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
|
erott@37872
|
330 |
|
erott@37872
|
331 |
toggle trace_rewrite;
|
erott@37872
|
332 |
?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
|
erott@37872
|
333 |
|
erott@37872
|
334 |
(*3.5. Calculate numeric constants*)
|
erott@37872
|
335 |
calculate;
|
erott@37872
|
336 |
calculate_;
|
erott@37872
|
337 |
|
erott@37872
|
338 |
?calc_list;
|
erott@37872
|
339 |
?calculate "Isac.thy" "plus" "#1 + #2";
|
erott@37872
|
340 |
?calculate "Isac.thy" "times" "#2 * #3";
|
erott@37872
|
341 |
?calculate "Isac.thy" "power" "#2 ^^^ #3";
|
erott@37872
|
342 |
?calculate "Isac.thy" "cancel_" "#9 // #12";
|
erott@37872
|
343 |
|
erott@37872
|
344 |
|
erott@37872
|
345 |
(** 4. Term orders **)
|
erott@37872
|
346 |
(*4.1. Exmpales for term orders*)
|
erott@37872
|
347 |
sqrt_right;
|
erott@37872
|
348 |
tless_true;
|
erott@37872
|
349 |
|
erott@37872
|
350 |
val t1 = (term_of o the o (parse thy)) "(sqrt a) + b";
|
erott@37872
|
351 |
val t2 = (term_of o the o (parse thy)) "b + (sqrt a)";
|
erott@37872
|
352 |
?sqrt_right false SqRoot.thy (t1, t2);
|
erott@37872
|
353 |
?sqrt_right false SqRoot.thy (t2, t1);
|
erott@37872
|
354 |
|
erott@37872
|
355 |
val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d";
|
erott@37872
|
356 |
val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d";
|
erott@37872
|
357 |
?sqrt_right true SqRoot.thy (t1, t2);
|
erott@37872
|
358 |
|
erott@37872
|
359 |
(*4.2. Ordered rewriting*)
|
erott@37872
|
360 |
ac_plus_times;
|
erott@37872
|
361 |
|
erott@37872
|
362 |
(*Give it a try: polynomial (normal) form*)
|
erott@37872
|
363 |
val ct' = "#3 * a + b + #2 * a";
|
erott@37872
|
364 |
val thm' = ("radd_commute","") : thm';
|
erott@37872
|
365 |
?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
|
erott@37872
|
366 |
val thm' = ("rdistr_right_assoc_p","") : thm';
|
erott@37872
|
367 |
?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
|
erott@37872
|
368 |
?val Some (ct',_) = calculate thy' "plus" ct';
|
erott@37872
|
369 |
|
erott@37872
|
370 |
val ct' = "3 * a + b + 2 * a" : cterm';
|
erott@37872
|
371 |
val thm' = ("radd_commute","") : thm';
|
erott@37872
|
372 |
?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
|
erott@37872
|
373 |
?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
|
erott@37872
|
374 |
?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
|
erott@37872
|
375 |
|
erott@37872
|
376 |
toggle trace_rewrite;
|
erott@37872
|
377 |
?rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct;
|
erott@37872
|
378 |
|
erott@37872
|
379 |
|
erott@37872
|
380 |
(** 5. The hierarchy of problem types **)
|
erott@37872
|
381 |
(*5.1. The standard-function for 'matching'*)
|
erott@37872
|
382 |
matches;
|
erott@37872
|
383 |
|
erott@37872
|
384 |
val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
|
erott@37872
|
385 |
val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
|
erott@37872
|
386 |
atomt p;
|
erott@37872
|
387 |
free2var;
|
erott@37872
|
388 |
val pat = free2var p;
|
erott@37872
|
389 |
matches thy t pat;
|
erott@37872
|
390 |
|
erott@37872
|
391 |
val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";
|
erott@37872
|
392 |
matches thy t2 pat;
|
erott@37872
|
393 |
|
erott@37872
|
394 |
val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v";
|
erott@37872
|
395 |
matches thy t2 pat2;
|
erott@37872
|
396 |
|
erott@37872
|
397 |
(*5.2. Accessing the hierarchy*)
|
erott@37872
|
398 |
show_ptyps;
|
erott@37872
|
399 |
show_ptyps();
|
erott@37872
|
400 |
get_pbt;
|
erott@37872
|
401 |
?get_pbt ["squareroot", "univariate", "equation"];
|
erott@37872
|
402 |
|
erott@37872
|
403 |
store_pbt;
|
erott@37872
|
404 |
?store_pbt
|
erott@37872
|
405 |
(prep_pbt SqRoot.thy
|
erott@37872
|
406 |
(["newtype","univariate","equation"],
|
erott@37872
|
407 |
[("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
|
erott@37872
|
408 |
("#Where" ,["contains_root (e_::bool)"]),
|
erott@37872
|
409 |
("#Find" ,["solutions v_i_"])
|
erott@37872
|
410 |
],
|
erott@37872
|
411 |
[("SqRoot.thy","square_equation")]));
|
erott@37872
|
412 |
show_ptyps();
|
erott@37872
|
413 |
|
erott@37872
|
414 |
(*5.3. Internals of the datastructure*)
|
erott@37872
|
415 |
(*5.4. Match a problem with a problem type*)
|
erott@37872
|
416 |
?val fmz = ["equality (#1 + #2 * x = #0)",
|
erott@37872
|
417 |
"solveFor x",
|
erott@37872
|
418 |
"solutions L"] : fmz;
|
erott@37872
|
419 |
match_pbl;
|
erott@37872
|
420 |
?match_pbl fmz (get_pbt ["univariate","equation"]);
|
erott@37872
|
421 |
?match_pbl fmz (get_pbt ["linear","univariate","equation"]);
|
erott@37872
|
422 |
?match_pbl fmz (get_pbt ["squareroot","univariate","equation"]);
|
erott@37872
|
423 |
|
erott@37872
|
424 |
(*5.5. Refine a problem specification *)
|
erott@37872
|
425 |
refine;
|
erott@37872
|
426 |
?val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
|
erott@37872
|
427 |
"solveFor x","errorBound (eps=#0)",
|
erott@37872
|
428 |
"solutions L"];
|
erott@37872
|
429 |
?refine fmz ["univariate","equation"];
|
erott@37872
|
430 |
|
erott@37872
|
431 |
?val fmz = ["equality (x+#1=#2)",
|
erott@37872
|
432 |
"solveFor x","errorBound (eps=#0)",
|
erott@37872
|
433 |
"solutions L"];
|
erott@37872
|
434 |
?refine fmz ["univariate","equation"];
|
erott@37872
|
435 |
|
erott@37872
|
436 |
|
erott@37872
|
437 |
(* 6. Do a calculational proof *)
|
erott@37872
|
438 |
?val fmz = ["equality ((x+#1) * (x+#2) = x^^^#2+#8)","solveFor x",
|
erott@37872
|
439 |
"errorBound (eps=#0)","solutions L"];
|
erott@37872
|
440 |
val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
|
erott@37872
|
441 |
("SqRoot.thy","no_met"));
|
erott@37872
|
442 |
|
erott@37872
|
443 |
(*6.1. Initialize the calculation*)
|
erott@37872
|
444 |
val p = e_pos'; val c = [];
|
erott@37872
|
445 |
?val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
|
erott@37872
|
446 |
?val (p,_,f,nxt,_,pt) = me (mID,m) p c EmptyPtree;
|
erott@37872
|
447 |
|
erott@37872
|
448 |
?Compiler.Control.Print.printDepth:=8;
|
erott@37872
|
449 |
?f;
|
erott@37872
|
450 |
?Compiler.Control.Print.printDepth:=4;
|
erott@37872
|
451 |
|
erott@37872
|
452 |
?nxt;
|
erott@37872
|
453 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
454 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
455 |
|
erott@37872
|
456 |
(*6.2. The phase of modeling*)
|
erott@37872
|
457 |
?nxt;
|
erott@37872
|
458 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
459 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
460 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
461 |
|
erott@37872
|
462 |
?Compiler.Control.Print.printDepth:=8;
|
erott@37872
|
463 |
?f;
|
erott@37872
|
464 |
?Compiler.Control.Print.printDepth:=4;
|
erott@37872
|
465 |
|
erott@37872
|
466 |
(*6.3. The phase of specification*)
|
erott@37872
|
467 |
?nxt;
|
erott@37872
|
468 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
469 |
|
erott@37872
|
470 |
|
erott@37872
|
471 |
val nxt = ("Specify_Problem",
|
erott@37872
|
472 |
Specify_Problem ["polynomial","univariate","equation"]);
|
erott@37872
|
473 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
474 |
|
erott@37872
|
475 |
val nxt = ("Specify_Problem",
|
erott@37872
|
476 |
Specify_Problem ["linear","univariate","equation"]);
|
erott@37872
|
477 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
478 |
?Compiler.Control.Print.printDepth:=8;f;Compiler.Control.Print.printDepth:=4;
|
erott@37872
|
479 |
|
erott@37872
|
480 |
val nxt = ("Refine_Problem",
|
erott@37872
|
481 |
Refine_Problem ["linear","univariate","equation"]);
|
erott@37872
|
482 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
483 |
?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
|
erott@37872
|
484 |
|
erott@37872
|
485 |
val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
|
erott@37872
|
486 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
487 |
?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
|
erott@37872
|
488 |
|
erott@37872
|
489 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
490 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
491 |
|
erott@37872
|
492 |
(*6.4. The phase of solving*)
|
erott@37872
|
493 |
nxt;
|
erott@37872
|
494 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
495 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
496 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
497 |
|
erott@37872
|
498 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
499 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
500 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
501 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
502 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
503 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
504 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
505 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
506 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
507 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
508 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
509 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
510 |
|
erott@37872
|
511 |
(*6.5. The final phase: check the postcondition*)
|
erott@37872
|
512 |
?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
513 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
erott@37872
|
514 |
|
erott@37872
|
515 |
|
erott@37872
|
516 |
|
erott@37872
|
517 |
|
erott@37872
|
518 |
|
erott@37872
|
519 |
|