diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/mat-eng.sml --- a/src/Doc/isac/mat-eng.sml Mon Sep 16 12:27:20 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,519 +0,0 @@ -(* cut and paste for math.tex -*) - -(*2.2. *) -"a + b * 3"; -str2term "a + b * 3"; -val term = str2term "a + b * 3"; -atomt term; -atomty term; - -(*2.3. Theories and parsing*) - - > Isac.thy; -val it = - {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, - Sum_Type, Relation, Record, Inductive, Transitive_Closure, - Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power, - SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe, - Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv, - IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map, - Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd, - RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow, - Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix, - Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus, - Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect, - Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie, - AlgEin, Test, Isac} : Theory.theory - -Group.thy -suche nach '*' Link: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html -locale semigroup = - fixes f :: "'a => 'a => 'a" (infixl "*" 70) - assumes assoc [ac_simps]: "a * b * c = a * (b * c)" - -> parse; -val it = fn : Theory.theory -> string -> Thm.cterm Library.option - - - -> (*-1-*); -> parse HOL.thy "2^^^3"; -*** Inner lexical error at: "^^^3" -val it = None : Thm.cterm Library.option -> (*-2-*); -> parse HOL.thy "d_d x (a + x)"; -val it = None : Thm.cterm Library.option -> (*-3-*); -> parse Rational.thy "2^^^3"; -val it = Some "2 ^^^ 3" : Thm.cterm Library.option -> (*-4-*); -val Some t4 = parse Rational.thy "d_d x (a + x)"; -val t4 = "d_d x (a + x)" : Thm.cterm -> (*-5-*); -val Some t5 = parse Diff.thy "d_d x (a + x)"; -val t5 = "d_d x (a + x)" : Thm.cterm - - -> term_of; -val it = fn : Thm.cterm -> Term.term -> term_of t4; -val it = - Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ - Free ("x", "RealDef.real") $ - (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $ - Free ("a", "RealDef.real") $ Free ("x", "RealDef.real")) -: Term.term -> term_of t5; -val it = - Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ - Free ("x", "RealDef.real") $ - (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $ - Free ("a", "RealDef.real") $ Free ("x", "RealDef.real")) -: Term.term - -> print_depth; -val it = fn : int -> unit - - - - - -> (*-4-*) val thy = Rational.thy; -val thy = - {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, - Sum_Type, Relation, Record, Inductive, Transitive_Closure, - Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power, - SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe, - Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv, - IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map, - Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd, - RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow, - Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix, - Float, ComplexI, Descript, Atools, Simplify, Poly, Rational} -: Theory.theory -> ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)"; - -*** -*** Free (d_d, [real, real] => real) -*** . Free (x, real) -*** . Const (op +, [real, real] => real) -*** . . Free (a, real) -*** . . Free (x, real) -*** - -val it = () : unit -> (*-5-*) val thy = Diff.thy; -val thy = - {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, - Sum_Type, Relation, Record, Inductive, Transitive_Closure, - Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power, - SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe, - Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv, - IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map, - Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd, - RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow, - Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools, - Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly, - Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq, - PolyEq, LogExp, Diff} : Theory.theory - -> ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)"; - -*** -*** Const (Diff.d_d, [real, real] => real) -*** . Free (x, real) -*** . Const (op +, [real, real] => real) -*** . . Free (a, real) -*** . . Free (x, real) -*** - -val it = () : unit - - - -> print_depth 1; -val it = () : unit -> term_of t4; -val it = - Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ ... -: Term.term - - -> print_depth 1; -val it = () : unit -> term_of t5; -val it = - Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ - ... : Term.term - - - --------------------------------------------ALT... -explode it; - \footnote{ - print_depth 9; - explode "a + b * 3"; - } - -(*unschoen*) - --------------------------------------------ALT... - HOL.thy; - parse; - parse thy "a + b * 3"; - val t = (term_of o the) it; - term_of; - -(*2.3. Displaying terms*) - print_depth; - ////Compiler.Control.Print.printDepth; -? Compiler.Control.Print.printDepth:= 2; - t; - ?Compiler.Control.Print.printDepth:= 6; - t; - ?Compiler.Control.Print.printLength; - ?Compiler.Control.Print.stringDepth; - atomt; - atomt t; - atomty; - atomty thy t; -(*Give it a try: the mathematics knowledge grows*) - parse HOL.thy "2^^^3"; - parse HOL.thy "d_d x (a + x)"; - ?parse RatArith.thy "#2^^^#3"; - ?parse RatArith.thy "d_d x (a + x)"; - parse Differentiate.thy "d_d x (a + x)"; - ?parse Differentiate.thy "#2^^^#3"; -(*don't trust the string representation*) - ?val thy = RatArith.thy; - ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)"; - ?val thy = Differentiate.thy; - ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)"; - -(*2.4. Converting terms*) - term_of; - the; - val t = (term_of o the o (parse thy)) "a + b * 3"; - - sign_of; - cterm_of; - val ct = cterm_of (sign_of thy) t; - - Sign.string_of_term; - Sign.string_of_term (sign_of thy) t; - - string_of_cterm; - string_of_cterm ct; - -(*2.5. Theorems *) - ?theorem' := overwritel (!theorem', - [("diff_const",num_str diff_const) - ]); - -(** 3. Rewriting **) -(*3.1. The arguments for rewriting*) - HOL.thy; - "HOL.thy" : theory'; - sqrt_right; - "sqrt_right" : rew_ord'; - eval_rls; - "eval_rls" : rls'; - diff_sum; - ("diff_sum", "") : thm'; - -(*3.2. The functions for rewriting*) - rewrite_; - rewrite; - -> val thy' = "Diff.thy"; -val thy' = "Diff.thy" : string -> val ct = "d_d x (a * 3 + b)"; -val ct = "d_d x (a * 3 + b)" : string -> val thm = ("diff_sum",""); -val thm = ("diff_sum", "") : string * string -> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true - [("bdv","x::real")] thm ct; -val ct = "d_d x (a * 3) + d_d x b" : cterm' -> val thm = ("diff_prod_const",""); -val thm = ("diff_prod_const", "") : string * string -> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true - [("bdv","x::real")] thm ct; -val ct = "a * d_d x 3 + d_d x b" : cterm' - - - -> val thy' = "Diff.thy"; -val thy' = "Diff.thy" : string -> val ct = "d_d x (a + a * (2 + b))"; -val ct = "d_d x (a + a * (2 + b))" : string -> val thm = ("diff_sum",""); -val thm = ("diff_sum", "") : string * string -> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true - [("bdv","x::real")] thm ct; -val ct = "d_d x a + d_d x (a * (2 + b))" : cterm' - -> val thm = ("diff_prod_const",""); -val thm = ("diff_prod_const", "") : string * string -> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true - [("bdv","x::real")] thm ct; -val ct = "d_d x a + a * d_d x (2 + b)" : cterm' - - - -(*Give it a try: rewriting*) - val thy' = "Diff.thy"; - val ct = "d_d x (x ^^^ 2 + 3 * x + 4)"; - val thm = ("diff_sum",""); - val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct; - val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct; - val thm = ("diff_prod_const",""); - val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct; -(*Give it a try: conditional rewriting*) - val thy' = "Isac.thy"; - val ct' = "3 * a + 2 * (a + 1)"; - val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n"); - (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; - val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"); - ?(*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; - ?val thm' = ("rcollect_right", - "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n"); - ?(*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; - ?(*4*) val Some (ct',_) = calculate thy' "plus" ct'; - ?(*5*) val Some (ct',_) = calculate thy' "times" ct'; - -(*Give it a try: functional programming*) - val thy' = "InsSort.thy"; - val ct = "sort [#1,#3,#2]" : cterm'; - - val thm = ("sort_def",""); - ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); - - val thm = ("foldr_rec",""); - ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); - - val thm = ("ins_base",""); - ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); - - val thm = ("foldr_rec",""); - ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); - - val thm = ("ins_rec",""); - ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); - - ?val (ct,_) = the (calculate thy' "le" ct); - - val thm = ("if_True","(if True then ?x else ?y) = ?x"); - ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); - -(*3.3. Variants of rewriting*) - rewrite_inst_; - rewrite_inst; - - rewrite_set_; - rewrite_set; - - rewrite_set_inst_; - rewrite_set_inst; - - toggle; - toggle trace_rewrite; - -(*3.4. Rule sets*) - sym; - rearrange_assoc; - -(*Give it a try: remove parentheses*) - ?val ct = (string_of_cterm o the o (parse RatArith.thy)) - "a + (b * (c * d) + e)"; - ?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct; - - toggle trace_rewrite; - ?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct; - -(*3.5. Calculate numeric constants*) - calculate; - calculate_; - - ?calc_list; - ?calculate "Isac.thy" "plus" "#1 + #2"; - ?calculate "Isac.thy" "times" "#2 * #3"; - ?calculate "Isac.thy" "power" "#2 ^^^ #3"; - ?calculate "Isac.thy" "cancel_" "#9 // #12"; - - -(** 4. Term orders **) -(*4.1. Exmpales for term orders*) - sqrt_right; - tless_true; - - val t1 = (term_of o the o (parse thy)) "(sqrt a) + b"; - val t2 = (term_of o the o (parse thy)) "b + (sqrt a)"; - ?sqrt_right false SqRoot.thy (t1, t2); - ?sqrt_right false SqRoot.thy (t2, t1); - - val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d"; - val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d"; - ?sqrt_right true SqRoot.thy (t1, t2); - -(*4.2. Ordered rewriting*) - ac_plus_times; - -(*Give it a try: polynomial (normal) form*) - val ct' = "#3 * a + b + #2 * a"; - val thm' = ("radd_commute","") : thm'; - ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; - val thm' = ("rdistr_right_assoc_p","") : thm'; - ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; - ?val Some (ct',_) = calculate thy' "plus" ct'; - - val ct' = "3 * a + b + 2 * a" : cterm'; - val thm' = ("radd_commute","") : thm'; - ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; - ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; - ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; - - toggle trace_rewrite; - ?rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct; - - -(** 5. The hierarchy of problem types **) -(*5.1. The standard-function for 'matching'*) - matches; - - val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1"; - val p = (term_of o the o (parse thy)) "a * b^^^2 = c"; - atomt p; - free2var; - val pat = free2var p; - matches thy t pat; - - val t2 = (term_of o the o (parse thy)) "x^^^2 = 1"; - matches thy t2 pat; - - val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v"; - matches thy t2 pat2; - -(*5.2. Accessing the hierarchy*) - show_ptyps; - show_ptyps(); - get_pbt; - ?get_pbt ["squareroot", "univariate", "equation"]; - - store_pbt; - ?store_pbt - (prep_pbt SqRoot.thy - (["newtype","univariate","equation"], - [("#Given" ,["equality e_","solveFor v_","errorBound err_"]), - ("#Where" ,["contains_root (e_::bool)"]), - ("#Find" ,["solutions v_i_"]) - ], - [("SqRoot.thy","square_equation")])); - show_ptyps(); - -(*5.3. Internals of the datastructure*) -(*5.4. Match a problem with a problem type*) - ?val fmz = ["equality (#1 + #2 * x = #0)", - "solveFor x", - "solutions L"] : fmz; - match_pbl; - ?match_pbl fmz (get_pbt ["univariate","equation"]); - ?match_pbl fmz (get_pbt ["linear","univariate","equation"]); - ?match_pbl fmz (get_pbt ["squareroot","univariate","equation"]); - -(*5.5. Refine a problem specification *) - refine; - ?val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", - "solveFor x","errorBound (eps=#0)", - "solutions L"]; - ?refine fmz ["univariate","equation"]; - - ?val fmz = ["equality (x+#1=#2)", - "solveFor x","errorBound (eps=#0)", - "solutions L"]; - ?refine fmz ["univariate","equation"]; - - -(* 6. Do a calculational proof *) - ?val fmz = ["equality ((x+#1) * (x+#2) = x^^^#2+#8)","solveFor x", - "errorBound (eps=#0)","solutions L"]; - val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"], - ("SqRoot.thy","no_met")); - -(*6.1. Initialize the calculation*) - val p = e_pos'; val c = []; - ?val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met))); - ?val (p,_,f,nxt,_,pt) = me (mID,m) p c EmptyPtree; - - ?Compiler.Control.Print.printDepth:=8; - ?f; - ?Compiler.Control.Print.printDepth:=4; - - ?nxt; - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - -(*6.2. The phase of modeling*) - ?nxt; - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - - ?Compiler.Control.Print.printDepth:=8; - ?f; - ?Compiler.Control.Print.printDepth:=4; - -(*6.3. The phase of specification*) - ?nxt; - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - - - val nxt = ("Specify_Problem", - Specify_Problem ["polynomial","univariate","equation"]); - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - - val nxt = ("Specify_Problem", - Specify_Problem ["linear","univariate","equation"]); - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - ?Compiler.Control.Print.printDepth:=8;f;Compiler.Control.Print.printDepth:=4; - - val nxt = ("Refine_Problem", - Refine_Problem ["linear","univariate","equation"]); - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - ?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4; - - val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]); - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - ?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4; - - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - -(*6.4. The phase of solving*) - nxt; - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - -(*6.5. The final phase: check the postcondition*) - ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - val (p,_,f,nxt,_,pt) = me nxt p [1] pt; - - - - - -