(* 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;