1 (* cut and paste for math.tex
7 val term = str2term "a + b * 3";
11 (*2.3. Theories and parsing*)
15 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
16 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
17 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
18 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
19 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
20 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
21 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
22 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
23 Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
24 Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
25 Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
26 Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
27 AlgEin, Test, Isac} : Theory.theory
30 suche nach '*' Link: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html
32 fixes f :: "'a => 'a => 'a" (infixl "*" 70)
33 assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
36 val it = fn : Theory.theory -> string -> Thm.cterm Library.option
41 > parse HOL.thy "2^^^3";
42 *** Inner lexical error at: "^^^3"
43 val it = None : Thm.cterm Library.option
45 > parse HOL.thy "d_d x (a + x)";
46 val it = None : Thm.cterm Library.option
48 > parse Rational.thy "2^^^3";
49 val it = Some "2 ^^^ 3" : Thm.cterm Library.option
51 val Some t4 = parse Rational.thy "d_d x (a + x)";
52 val t4 = "d_d x (a + x)" : Thm.cterm
54 val Some t5 = parse Diff.thy "d_d x (a + x)";
55 val t5 = "d_d x (a + x)" : Thm.cterm
59 val it = fn : Thm.cterm -> Term.term
62 Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
63 Free ("x", "RealDef.real") $
64 (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
65 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
69 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
70 Free ("x", "RealDef.real") $
71 (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
72 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
76 val it = fn : int -> unit
82 > (*-4-*) val thy = Rational.thy;
84 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
85 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
86 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
87 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
88 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
89 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
90 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
91 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
92 Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
93 Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
95 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
98 *** Free (d_d, [real, real] => real)
100 *** . Const (op +, [real, real] => real)
101 *** . . Free (a, real)
102 *** . . Free (x, real)
106 > (*-5-*) val thy = Diff.thy;
108 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
109 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
110 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
111 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
112 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
113 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
114 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
115 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
116 Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,
117 Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,
118 Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
119 PolyEq, LogExp, Diff} : Theory.theory
121 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
124 *** Const (Diff.d_d, [real, real] => real)
126 *** . Const (op +, [real, real] => real)
127 *** . . Free (a, real)
128 *** . . Free (x, real)
139 Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ ...
147 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
152 -------------------------------------------ALT...
161 -------------------------------------------ALT...
164 parse thy "a + b * 3";
165 val t = (term_of o the) it;
168 (*2.3. Displaying terms*)
170 ////Compiler.Control.Print.printDepth;
171 ? Compiler.Control.Print.printDepth:= 2;
173 ?Compiler.Control.Print.printDepth:= 6;
175 ?Compiler.Control.Print.printLength;
176 ?Compiler.Control.Print.stringDepth;
181 (*Give it a try: the mathematics knowledge grows*)
182 parse HOL.thy "2^^^3";
183 parse HOL.thy "d_d x (a + x)";
184 ?parse RatArith.thy "#2^^^#3";
185 ?parse RatArith.thy "d_d x (a + x)";
186 parse Differentiate.thy "d_d x (a + x)";
187 ?parse Differentiate.thy "#2^^^#3";
188 (*don't trust the string representation*)
189 ?val thy = RatArith.thy;
190 ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
191 ?val thy = Differentiate.thy;
192 ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
194 (*2.4. Converting terms*)
197 val t = (term_of o the o (parse thy)) "a + b * 3";
201 val ct = cterm_of (sign_of thy) t;
204 Sign.string_of_term (sign_of thy) t;
210 ?theorem' := overwritel (!theorem',
211 [("diff_const",num_str diff_const)
215 (*3.1. The arguments for rewriting*)
219 "sqrt_right" : rew_ord';
223 ("diff_sum", "") : thm';
225 (*3.2. The functions for rewriting*)
229 > val thy' = "Diff.thy";
230 val thy' = "Diff.thy" : string
231 > val ct = "d_d x (a * 3 + b)";
232 val ct = "d_d x (a * 3 + b)" : string
233 > val thm = ("diff_sum","");
234 val thm = ("diff_sum", "") : string * string
235 > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
236 [("bdv","x::real")] thm ct;
237 val ct = "d_d x (a * 3) + d_d x b" : cterm'
238 > val thm = ("diff_prod_const","");
239 val thm = ("diff_prod_const", "") : string * string
240 > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
241 [("bdv","x::real")] thm ct;
242 val ct = "a * d_d x 3 + d_d x b" : cterm'
246 > val thy' = "Diff.thy";
247 val thy' = "Diff.thy" : string
248 > val ct = "d_d x (a + a * (2 + b))";
249 val ct = "d_d x (a + a * (2 + b))" : string
250 > val thm = ("diff_sum","");
251 val thm = ("diff_sum", "") : string * string
252 > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
253 [("bdv","x::real")] thm ct;
254 val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'
256 > val thm = ("diff_prod_const","");
257 val thm = ("diff_prod_const", "") : string * string
258 > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
259 [("bdv","x::real")] thm ct;
260 val ct = "d_d x a + a * d_d x (2 + b)" : cterm'
264 (*Give it a try: rewriting*)
265 val thy' = "Diff.thy";
266 val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
267 val thm = ("diff_sum","");
268 val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct;
269 val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct;
270 val thm = ("diff_prod_const","");
271 val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct;
272 (*Give it a try: conditional rewriting*)
273 val thy' = "Isac.thy";
274 val ct' = "3 * a + 2 * (a + 1)";
275 val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n");
276 (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
277 val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1");
278 ?(*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
279 ?val thm' = ("rcollect_right",
280 "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n");
281 ?(*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
282 ?(*4*) val Some (ct',_) = calculate thy' "plus" ct';
283 ?(*5*) val Some (ct',_) = calculate thy' "times" ct';
285 (*Give it a try: functional programming*)
286 val thy' = "InsSort.thy";
287 val ct = "sort [#1,#3,#2]" : cterm';
289 val thm = ("sort_def","");
290 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
292 val thm = ("foldr_rec","");
293 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
295 val thm = ("ins_base","");
296 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
298 val thm = ("foldr_rec","");
299 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
301 val thm = ("ins_rec","");
302 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
304 ?val (ct,_) = the (calculate thy' "le" ct);
306 val thm = ("if_True","(if True then ?x else ?y) = ?x");
307 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
309 (*3.3. Variants of rewriting*)
320 toggle trace_rewrite;
326 (*Give it a try: remove parentheses*)
327 ?val ct = (string_of_cterm o the o (parse RatArith.thy))
328 "a + (b * (c * d) + e)";
329 ?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
331 toggle trace_rewrite;
332 ?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
334 (*3.5. Calculate numeric constants*)
339 ?calculate "Isac.thy" "plus" "#1 + #2";
340 ?calculate "Isac.thy" "times" "#2 * #3";
341 ?calculate "Isac.thy" "power" "#2 ^^^ #3";
342 ?calculate "Isac.thy" "cancel_" "#9 // #12";
345 (** 4. Term orders **)
346 (*4.1. Exmpales for term orders*)
350 val t1 = (term_of o the o (parse thy)) "(sqrt a) + b";
351 val t2 = (term_of o the o (parse thy)) "b + (sqrt a)";
352 ?sqrt_right false SqRoot.thy (t1, t2);
353 ?sqrt_right false SqRoot.thy (t2, t1);
355 val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d";
356 val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d";
357 ?sqrt_right true SqRoot.thy (t1, t2);
359 (*4.2. Ordered rewriting*)
362 (*Give it a try: polynomial (normal) form*)
363 val ct' = "#3 * a + b + #2 * a";
364 val thm' = ("radd_commute","") : thm';
365 ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
366 val thm' = ("rdistr_right_assoc_p","") : thm';
367 ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
368 ?val Some (ct',_) = calculate thy' "plus" ct';
370 val ct' = "3 * a + b + 2 * a" : cterm';
371 val thm' = ("radd_commute","") : thm';
372 ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
373 ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
374 ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
376 toggle trace_rewrite;
377 ?rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct;
380 (** 5. The hierarchy of problem types **)
381 (*5.1. The standard-function for 'matching'*)
384 val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
385 val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
388 val pat = free2var p;
391 val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";
394 val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v";
397 (*5.2. Accessing the hierarchy*)
401 ?get_pbt ["squareroot", "univariate", "equation"];
406 (["newtype","univariate","equation"],
407 [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
408 ("#Where" ,["contains_root (e_::bool)"]),
409 ("#Find" ,["solutions v_i_"])
411 [("SqRoot.thy","square_equation")]));
414 (*5.3. Internals of the datastructure*)
415 (*5.4. Match a problem with a problem type*)
416 ?val fmz = ["equality (#1 + #2 * x = #0)",
418 "solutions L"] : fmz;
420 ?match_pbl fmz (get_pbt ["univariate","equation"]);
421 ?match_pbl fmz (get_pbt ["linear","univariate","equation"]);
422 ?match_pbl fmz (get_pbt ["squareroot","univariate","equation"]);
424 (*5.5. Refine a problem specification *)
426 ?val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
427 "solveFor x","errorBound (eps=#0)",
429 ?refine fmz ["univariate","equation"];
431 ?val fmz = ["equality (x+#1=#2)",
432 "solveFor x","errorBound (eps=#0)",
434 ?refine fmz ["univariate","equation"];
437 (* 6. Do a calculational proof *)
438 ?val fmz = ["equality ((x+#1) * (x+#2) = x^^^#2+#8)","solveFor x",
439 "errorBound (eps=#0)","solutions L"];
440 val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
441 ("SqRoot.thy","no_met"));
443 (*6.1. Initialize the calculation*)
444 val p = e_pos'; val c = [];
445 ?val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
446 ?val (p,_,f,nxt,_,pt) = me (mID,m) p c EmptyPtree;
448 ?Compiler.Control.Print.printDepth:=8;
450 ?Compiler.Control.Print.printDepth:=4;
453 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
454 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
456 (*6.2. The phase of modeling*)
458 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
459 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
460 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
462 ?Compiler.Control.Print.printDepth:=8;
464 ?Compiler.Control.Print.printDepth:=4;
466 (*6.3. The phase of specification*)
468 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
471 val nxt = ("Specify_Problem",
472 Specify_Problem ["polynomial","univariate","equation"]);
473 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
475 val nxt = ("Specify_Problem",
476 Specify_Problem ["linear","univariate","equation"]);
477 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
478 ?Compiler.Control.Print.printDepth:=8;f;Compiler.Control.Print.printDepth:=4;
480 val nxt = ("Refine_Problem",
481 Refine_Problem ["linear","univariate","equation"]);
482 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
483 ?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
485 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
486 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
487 ?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
489 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
490 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
492 (*6.4. The phase of solving*)
494 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
495 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
496 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
498 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
499 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
500 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
501 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
502 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
503 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
504 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
505 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
506 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
507 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
508 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
509 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
511 (*6.5. The final phase: check the postcondition*)
512 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
513 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;