wneuper/isa: doc-isac/mat-eng.sml@26037efefd61

     1 (* cut and paste for math.tex

     2 *)

     4 (*2.2. *)

     5 "a + b * 3";

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

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

     8 atomt term;

     9 TermC.atom_trace_detail @{context} term;

    11 (*2.3. Theories and parsing*)

    13  > Isac.thy;

    14 val it =

    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

    29 Group.thy

    30 suche nach '*' Link: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html

    31 locale semigroup =

    32   fixes f :: "'a => 'a => 'a" (infixl "*" 70)

    33   assumes assoc [ac_simps]: "a * b * c = a * (b * c)"

    35 > parse;

    36 val it = fn : Theory.theory -> string -> Thm.cterm Library.option

    40 > (*-1-*);

    41 > parse HOL.thy "2^^^3";

    42 *** Inner lexical error at: "^^^3"

    43 val it = None : Thm.cterm Library.option

    44 > (*-2-*);

    45 > parse HOL.thy "d_d x (a + x)";

    46 val it = None : Thm.cterm Library.option

    47 > (*-3-*);

    48 > parse Rational.thy "2^^^3";

    49 val it = Some "2 ^^^ 3" : Thm.cterm Library.option

    50 > (*-4-*);

    51 val Some t4 = parse Rational.thy "d_d x (a + x)";

    52 val t4 = "d_d x (a + x)" : Thm.cterm

    53 > (*-5-*);

    54 val Some t5 = parse Diff.thy  "d_d x (a + x)";

    55 val t5 = "d_d x (a + x)" : Thm.cterm

    58 > term_of;

    59 val it = fn : Thm.cterm -> Term.term

    60 > term_of t4;

    61 val it =

    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"))

    66 : Term.term

    67 > term_of t5;

    68 val it =

    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"))

    73 : Term.term

    75 > print_depth;

    76 val it = fn : int -> unit

    82 > (*-4-*) val thy = Rational.thy;

    83 val 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}

    94 : Theory.theory

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

    97 ***

    98 *** Free (d_d, [real, real] => real)

    99 *** . Free (x, real)

   100 *** . Const (op +, [real, real] => real)

   101 *** . . Free (a, real)

   102 *** . . Free (x, real)

   103 ***

   105 val it = () : unit

   106 > (*-5-*) val thy = Diff.thy;

   107 val 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 > ((TermC.atom_trace_detail @{context}) o term_of o the o (parse thy)) "d_d x (a + x)";

   123 ***

   124 *** Const (Diff.d_d, [real, real] => real)

   125 *** . Free (x, real)

   126 *** . Const (op +, [real, real] => real)

   127 *** . . Free (a, real)

   128 *** . . Free (x, real)

   129 ***

   131 val it = () : unit

   135 > print_depth 1;

   136 val it = () : unit

   137 > term_of t4;

   138 val it =

   139    Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ ...

   140 : Term.term

   143 > print_depth 1;

   144 val it = () : unit

   145 > term_of t5;

   146 val it =

   147    Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $

   148       ... : Term.term

   152 -------------------------------------------ALT...

   153 explode it;

   154 	  \footnote{

   155 	  print_depth 9;

   156 	  explode "a + b * 3";

   157 	  }

   159 (*unschoen*)

   161 -------------------------------------------ALT...

   162  HOL.thy;

   163  parse;

   164  parse thy "a + b * 3";

   165  val t = (term_of o the) it;

   166  term_of;

   168 (*2.3. Displaying terms*)

   169  print_depth;

   170  ////Compiler.Control.Print.printDepth;

   171 ? Compiler.Control.Print.printDepth:= 2;

   172  t;

   173  ?Compiler.Control.Print.printDepth:= 6;

   174  t;

   175  ?Compiler.Control.Print.printLength;

   176  ?Compiler.Control.Print.stringDepth;

   177  atomt;

   178  atomt t;

   179  TermC.atom_trace_detail @{context};

   180  TermC.atom_trace_detail @{context} t;

   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  ((TermC.atom_trace_detail @{context} thy) o term_of o the o (parse thy)) "d_d x (a + x)";

   191  ?val thy = Differentiate.thy;

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

   194 (*2.4. Converting terms*)

   195  term_of;

   196  the;

   197  val t = (term_of o the o (parse thy)) "a + b * 3";

   199  sign_of;

   200  cterm_of;

   201  val ct = cterm_of (sign_of thy) t;

   203  Sign.string_of_term;

   204  Sign.string_of_term (sign_of thy) t;

   206  string_of_cterm;

   207  string_of_cterm ct;

   209 (*2.5. Theorems *)

   210  ?theorem' := overwritel (!theorem',

   211   [("diff_const",num_str diff_const)

   212    ]);

   214 (** 3. Rewriting **)

   215 (*3.1. The arguments for rewriting*)

   216  HOL.thy;

   217  "HOL.thy" : theory';

   218  sqrt_right;

   219  "sqrt_right" : rew_ord;

   220  eval_rls;

   221  "eval_rls" : rls';

   222  diff_sum;

   223  ("diff_sum", "") : thm';

   225 (*3.2. The functions for rewriting*)

   226  rewrite_;

   227  rewrite;

   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*)

   310  rewrite_inst_;

   311  rewrite_inst;

   313  rewrite_set_;

   314  rewrite_set;

   316  rewrite_set_inst_;

   317  rewrite_set_inst;

   319  toggle;

   320  toggle trace_rewrite;

   322 (*3.4. Rule sets*)

   323  sym;

   324  rearrange_assoc;

   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*)

   335  calculate;

   336  calculate_;

   338  ?calc_list;

   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*)

   347  sqrt_right;

   348  tless_true;

   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*)

   360  ac_plus_times;

   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'*)

   382  matches;

   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";

   386  atomt p;

   387  mk_Var;

   388  val pat = mk_Var p;

   389  matches thy t pat;

   391  val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";

   392  matches thy t2 pat;

   394  val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v";

   395  matches thy t2 pat2;

   397 (*5.2. Accessing the hierarchy*)

   398  show_ptyps;

   399  show_ptyps();

   400  get_pbt;

   401  ?get_pbt ["squareroot", "univariate", "equation"];

   403  store_pbt;

   404  ?store_pbt

   405     (prep_pbt SqRoot.thy

   406     (["newtype","univariate","equation"],

   407      [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),

   408       ("#Where" ,["contains_root (e_::bool)"]),

   409       ("#Find"  ,["solutions v_i_"])

   410      ],

   411      [("SqRoot.thy","square_equation")]));

   412  show_ptyps();

   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)",

   417  	    "solveFor x",

   418  	    "solutions L"] : fmz;

   419  by_formalise;

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

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

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

   424 (*5.5. Refine a problem specification *)

   425  refine;

   426  ?val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",

   427  	    "solveFor x","errorBound (eps=#0)",

   428  	    "solutions L"];

   429  ?refine fmz ["univariate","equation"];

   431  ?val fmz = ["equality (x+#1=#2)",

   432  	    "solveFor x","errorBound (eps=#0)",

   433  	    "solutions L"];

   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;

   449  ?f;

   450  ?Compiler.Control.Print.printDepth:=4;

   452  ?nxt;

   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*)

   457  ?nxt;

   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;

   463  ?f;

   464  ?Compiler.Control.Print.printDepth:=4;

   466 (*6.3. The phase of specification*)

   467  ?nxt;

   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*)

   493  nxt;

   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;

author	wneuper <Walther.Neuper@jku.at>
	Sun, 31 Dec 2023 09:42:27 +0100
changeset 60787	26037efefd61
parent 60769	0df0759fed26
permissions	-rw-r--r--