(* cut and paste for math.tex

*)

(*2.2. *)

"a + b * 3";

TermC.parse_test @{context} "a + b * 3";

val term = TermC.parse_test @{context} "a + b * 3";

atomt term;

TermC.atom_trace_detail @{context} 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

> ((TermC.atom_trace_detail @{context}) 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

> ((TermC.atom_trace_detail @{context}) 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; 

 TermC.atom_trace_detail @{context};

 TermC.atom_trace_detail @{context} 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;

 ((TermC.atom_trace_detail @{context} thy) o term_of o the o (parse thy)) "d_d x (a + x)";

 ?val thy = Differentiate.thy;

 ((TermC.atom_trace_detail @{context} 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;

 mk_Var;

 val pat = mk_Var 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;

 by_formalise;

 ?by_formalise fmz (get_pbt ["univariate","equation"]);

 ?by_formalise fmz (get_pbt ["linear","univariate","equation"]);

 ?by_formalise 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;