doc-isac/mat-eng.sml
author wneuper <Walther.Neuper@jku.at>
Sun, 31 Dec 2023 09:42:27 +0100
changeset 60787 26037efefd61
parent 60769 0df0759fed26
permissions -rw-r--r--
Doc/Specify_Phase 2: copy finished
erott@37872
     1
(* cut and paste for math.tex
erott@37872
     2
*)
erott@37872
     3
erott@37872
     4
(*2.2. *)
erott@37872
     5
"a + b * 3";
Walther@60566
     6
TermC.parse_test @{context} "a + b * 3";
Walther@60566
     7
val term = TermC.parse_test @{context} "a + b * 3";
erott@37872
     8
atomt term;
Walther@60650
     9
TermC.atom_trace_detail @{context} term;
erott@37872
    10
erott@37872
    11
(*2.3. Theories and parsing*)
erott@37872
    12
erott@37872
    13
 > Isac.thy;
erott@37872
    14
val it =
erott@37872
    15
   {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
erott@37872
    16
     Sum_Type, Relation, Record, Inductive, Transitive_Closure,
erott@37872
    17
     Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
erott@37872
    18
     SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
erott@37872
    19
     Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
erott@37872
    20
     IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
erott@37872
    21
     Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
erott@37872
    22
     RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
erott@37872
    23
     Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
erott@37872
    24
     Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
erott@37872
    25
     Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
erott@37872
    26
     Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
erott@37872
    27
     AlgEin, Test, Isac} : Theory.theory
erott@37872
    28
erott@37872
    29
Group.thy
erott@37872
    30
suche nach '*' Link: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html
erott@37872
    31
locale semigroup =
erott@37872
    32
  fixes f :: "'a => 'a => 'a" (infixl "*" 70)
erott@37872
    33
  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
erott@37872
    34
erott@37872
    35
> parse;
erott@37872
    36
val it = fn : Theory.theory -> string -> Thm.cterm Library.option
erott@37872
    37
erott@37872
    38
erott@37872
    39
erott@37872
    40
> (*-1-*);
erott@37872
    41
> parse HOL.thy "2^^^3";
erott@37872
    42
*** Inner lexical error at: "^^^3"
erott@37872
    43
val it = None : Thm.cterm Library.option
erott@37872
    44
> (*-2-*);
erott@37872
    45
> parse HOL.thy "d_d x (a + x)";
erott@37872
    46
val it = None : Thm.cterm Library.option
erott@37872
    47
> (*-3-*);
erott@37872
    48
> parse Rational.thy "2^^^3";
erott@37872
    49
val it = Some "2 ^^^ 3" : Thm.cterm Library.option
erott@37872
    50
> (*-4-*);
erott@37872
    51
val Some t4 = parse Rational.thy "d_d x (a + x)";
erott@37872
    52
val t4 = "d_d x (a + x)" : Thm.cterm
erott@37872
    53
> (*-5-*);
erott@37872
    54
val Some t5 = parse Diff.thy  "d_d x (a + x)";
erott@37872
    55
val t5 = "d_d x (a + x)" : Thm.cterm
erott@37872
    56
erott@37872
    57
erott@37872
    58
> term_of;
erott@37872
    59
val it = fn : Thm.cterm -> Term.term
erott@37872
    60
> term_of t4;
erott@37872
    61
val it =
erott@37872
    62
   Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
erott@37872
    63
         Free ("x", "RealDef.real") $
erott@37872
    64
      (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
erott@37872
    65
            Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
erott@37872
    66
: Term.term
erott@37872
    67
> term_of t5;
erott@37872
    68
val it =
erott@37872
    69
   Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
erott@37872
    70
         Free ("x", "RealDef.real") $
erott@37872
    71
      (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
erott@37872
    72
            Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
erott@37872
    73
: Term.term
erott@37872
    74
erott@37872
    75
> print_depth;
erott@37872
    76
val it = fn : int -> unit
erott@37872
    77
erott@37872
    78
erott@37872
    79
erott@37872
    80
erott@37872
    81
erott@37872
    82
> (*-4-*) val thy = Rational.thy;
erott@37872
    83
val thy =
erott@37872
    84
   {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
erott@37872
    85
     Sum_Type, Relation, Record, Inductive, Transitive_Closure,
erott@37872
    86
     Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
erott@37872
    87
     SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
erott@37872
    88
     Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
erott@37872
    89
     IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
erott@37872
    90
     Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
erott@37872
    91
     RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
erott@37872
    92
     Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
erott@37872
    93
     Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
erott@37872
    94
: Theory.theory
Walther@60650
    95
> ((TermC.atom_trace_detail @{context}) o term_of o the o (parse thy)) "d_d x (a + x)";
erott@37872
    96
erott@37872
    97
***
erott@37872
    98
*** Free (d_d, [real, real] => real)
erott@37872
    99
*** . Free (x, real)
erott@37872
   100
*** . Const (op +, [real, real] => real)
erott@37872
   101
*** . . Free (a, real)
erott@37872
   102
*** . . Free (x, real)
erott@37872
   103
***
erott@37872
   104
erott@37872
   105
val it = () : unit
erott@37872
   106
> (*-5-*) val thy = Diff.thy;
erott@37872
   107
val thy =
erott@37872
   108
   {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
erott@37872
   109
     Sum_Type, Relation, Record, Inductive, Transitive_Closure,
erott@37872
   110
     Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
erott@37872
   111
     SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
erott@37872
   112
     Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
erott@37872
   113
     IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
erott@37872
   114
     Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
erott@37872
   115
     RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
erott@37872
   116
     Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,
erott@37872
   117
     Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,
erott@37872
   118
     Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
erott@37872
   119
     PolyEq, LogExp, Diff} : Theory.theory
erott@37872
   120
Walther@60650
   121
> ((TermC.atom_trace_detail @{context}) o term_of o the o (parse thy)) "d_d x (a + x)";
erott@37872
   122
erott@37872
   123
***
erott@37872
   124
*** Const (Diff.d_d, [real, real] => real)
erott@37872
   125
*** . Free (x, real)
erott@37872
   126
*** . Const (op +, [real, real] => real)
erott@37872
   127
*** . . Free (a, real)
erott@37872
   128
*** . . Free (x, real)
erott@37872
   129
***
erott@37872
   130
erott@37872
   131
val it = () : unit
erott@37872
   132
erott@37872
   133
erott@37872
   134
erott@37872
   135
> print_depth 1;
erott@37872
   136
val it = () : unit
erott@37872
   137
> term_of t4;
erott@37872
   138
val it =
erott@37872
   139
   Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ ...
erott@37872
   140
: Term.term
erott@37872
   141
erott@37872
   142
erott@37872
   143
> print_depth 1;
erott@37872
   144
val it = () : unit
erott@37872
   145
> term_of t5;
erott@37872
   146
val it =
erott@37872
   147
   Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
erott@37872
   148
      ... : Term.term
erott@37872
   149
erott@37872
   150
erott@37872
   151
erott@37872
   152
-------------------------------------------ALT...
erott@37872
   153
explode it;
erott@37872
   154
	  \footnote{
erott@37872
   155
	  print_depth 9;
erott@37872
   156
	  explode "a + b * 3";
erott@37872
   157
	  }
erott@37872
   158
erott@37872
   159
(*unschoen*)
erott@37872
   160
erott@37872
   161
-------------------------------------------ALT...
erott@37872
   162
 HOL.thy;
erott@37872
   163
 parse;
erott@37872
   164
 parse thy "a + b * 3";
erott@37872
   165
 val t = (term_of o the) it;
erott@37872
   166
 term_of;
erott@37872
   167
erott@37872
   168
(*2.3. Displaying terms*)
erott@37872
   169
 print_depth;
erott@37872
   170
 ////Compiler.Control.Print.printDepth;
erott@37872
   171
? Compiler.Control.Print.printDepth:= 2;
erott@37872
   172
 t;
erott@37872
   173
 ?Compiler.Control.Print.printDepth:= 6;
erott@37872
   174
 t;
erott@37872
   175
 ?Compiler.Control.Print.printLength;
erott@37872
   176
 ?Compiler.Control.Print.stringDepth;
erott@37872
   177
 atomt;
erott@37872
   178
 atomt t; 
Walther@60650
   179
 TermC.atom_trace_detail @{context};
Walther@60650
   180
 TermC.atom_trace_detail @{context} t;
erott@37872
   181
(*Give it a try: the mathematics knowledge grows*)
erott@37872
   182
 parse HOL.thy "2^^^3";
erott@37872
   183
 parse HOL.thy "d_d x (a + x)";
erott@37872
   184
 ?parse RatArith.thy "#2^^^#3";
erott@37872
   185
 ?parse RatArith.thy "d_d x (a + x)";
erott@37872
   186
 parse Differentiate.thy "d_d x (a + x)";
erott@37872
   187
 ?parse Differentiate.thy "#2^^^#3";
erott@37872
   188
(*don't trust the string representation*)
erott@37872
   189
 ?val thy = RatArith.thy;
Walther@60650
   190
 ((TermC.atom_trace_detail @{context} thy) o term_of o the o (parse thy)) "d_d x (a + x)";
erott@37872
   191
 ?val thy = Differentiate.thy;
Walther@60650
   192
 ((TermC.atom_trace_detail @{context} thy) o term_of o the o (parse thy)) "d_d x (a + x)";
erott@37872
   193
erott@37872
   194
(*2.4. Converting terms*)
erott@37872
   195
 term_of;
erott@37872
   196
 the;
erott@37872
   197
 val t = (term_of o the o (parse thy)) "a + b * 3";
erott@37872
   198
erott@37872
   199
 sign_of;
erott@37872
   200
 cterm_of;
erott@37872
   201
 val ct = cterm_of (sign_of thy) t;
erott@37872
   202
erott@37872
   203
 Sign.string_of_term;
erott@37872
   204
 Sign.string_of_term (sign_of thy) t;
erott@37872
   205
erott@37872
   206
 string_of_cterm;
erott@37872
   207
 string_of_cterm ct;
erott@37872
   208
erott@37872
   209
(*2.5. Theorems *)
erott@37872
   210
 ?theorem' := overwritel (!theorem',
erott@37872
   211
  [("diff_const",num_str diff_const)
erott@37872
   212
   ]);
erott@37872
   213
erott@37872
   214
(** 3. Rewriting **)
erott@37872
   215
(*3.1. The arguments for rewriting*)
erott@37872
   216
 HOL.thy;
erott@37872
   217
 "HOL.thy" : theory';
erott@37872
   218
 sqrt_right;
Walther@60586
   219
 "sqrt_right" : rew_ord;
erott@37872
   220
 eval_rls;
erott@37872
   221
 "eval_rls" : rls';
erott@37872
   222
 diff_sum;
erott@37872
   223
 ("diff_sum", "") : thm';
erott@37872
   224
erott@37872
   225
(*3.2. The functions for rewriting*)
erott@37872
   226
 rewrite_;
erott@37872
   227
 rewrite;
erott@37872
   228
erott@37872
   229
> val thy' = "Diff.thy";
erott@37872
   230
val thy' = "Diff.thy" : string
erott@37872
   231
> val ct = "d_d x (a * 3 + b)";
erott@37872
   232
val ct = "d_d x (a * 3 + b)" : string
erott@37872
   233
> val thm = ("diff_sum","");
erott@37872
   234
val thm = ("diff_sum", "") : string * string
erott@37872
   235
> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
erott@37872
   236
                     [("bdv","x::real")] thm ct;
erott@37872
   237
val ct = "d_d x (a * 3) + d_d x b" : cterm'
erott@37872
   238
> val thm = ("diff_prod_const","");
erott@37872
   239
val thm = ("diff_prod_const", "") : string * string
erott@37872
   240
> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
erott@37872
   241
                     [("bdv","x::real")] thm ct;
erott@37872
   242
val ct = "a * d_d x 3 + d_d x b" : cterm'
erott@37872
   243
erott@37872
   244
erott@37872
   245
erott@37872
   246
> val thy' = "Diff.thy";
erott@37872
   247
val thy' = "Diff.thy" : string
erott@37872
   248
> val ct = "d_d x (a + a * (2 + b))";
erott@37872
   249
val ct = "d_d x (a + a * (2 + b))" : string
erott@37872
   250
> val thm = ("diff_sum","");
erott@37872
   251
val thm = ("diff_sum", "") : string * string
erott@37872
   252
> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
erott@37872
   253
                     [("bdv","x::real")] thm ct;
erott@37872
   254
val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'
erott@37872
   255
erott@37872
   256
> val thm = ("diff_prod_const","");
erott@37872
   257
val thm = ("diff_prod_const", "") : string * string
erott@37872
   258
> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
erott@37872
   259
                     [("bdv","x::real")] thm ct;
erott@37872
   260
val ct = "d_d x a + a * d_d x (2 + b)" : cterm'
erott@37872
   261
erott@37872
   262
erott@37872
   263
erott@37872
   264
(*Give it a try: rewriting*)
erott@37872
   265
 val thy' = "Diff.thy";
erott@37872
   266
 val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
erott@37872
   267
 val thm = ("diff_sum","");
erott@37872
   268
 val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct;
erott@37872
   269
 val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true  [("bdv","x::real")] thm ct;
erott@37872
   270
 val thm = ("diff_prod_const","");
erott@37872
   271
 val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct;
erott@37872
   272
(*Give it a try: conditional rewriting*)
erott@37872
   273
 val thy' = "Isac.thy";
erott@37872
   274
 val ct' = "3 * a + 2 * (a + 1)";
erott@37872
   275
 val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n");
erott@37872
   276
 (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
erott@37872
   277
 val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1");
erott@37872
   278
 ?(*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
erott@37872
   279
 ?val thm' = ("rcollect_right",
erott@37872
   280
     "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n");
erott@37872
   281
 ?(*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
erott@37872
   282
 ?(*4*) val Some (ct',_) = calculate thy' "plus" ct';
erott@37872
   283
 ?(*5*) val Some (ct',_) = calculate thy' "times" ct';
erott@37872
   284
erott@37872
   285
(*Give it a try: functional programming*)
erott@37872
   286
 val thy' = "InsSort.thy";
erott@37872
   287
 val ct = "sort [#1,#3,#2]" : cterm';
erott@37872
   288
erott@37872
   289
 val thm = ("sort_def","");
erott@37872
   290
 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
erott@37872
   291
erott@37872
   292
 val thm = ("foldr_rec","");
erott@37872
   293
 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
erott@37872
   294
erott@37872
   295
 val thm = ("ins_base","");
erott@37872
   296
 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
erott@37872
   297
erott@37872
   298
 val thm = ("foldr_rec","");
erott@37872
   299
 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
erott@37872
   300
erott@37872
   301
 val thm = ("ins_rec","");
erott@37872
   302
 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
erott@37872
   303
erott@37872
   304
 ?val (ct,_) = the (calculate thy' "le" ct);
erott@37872
   305
erott@37872
   306
 val thm = ("if_True","(if True then ?x else ?y) = ?x");
erott@37872
   307
 ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
erott@37872
   308
erott@37872
   309
(*3.3. Variants of rewriting*)
erott@37872
   310
 rewrite_inst_;
erott@37872
   311
 rewrite_inst;
erott@37872
   312
erott@37872
   313
 rewrite_set_;
erott@37872
   314
 rewrite_set;
erott@37872
   315
erott@37872
   316
 rewrite_set_inst_;
erott@37872
   317
 rewrite_set_inst;
erott@37872
   318
erott@37872
   319
 toggle;
erott@37872
   320
 toggle trace_rewrite;
erott@37872
   321
erott@37872
   322
(*3.4. Rule sets*)
erott@37872
   323
 sym;
erott@37872
   324
 rearrange_assoc;
erott@37872
   325
erott@37872
   326
(*Give it a try: remove parentheses*)
erott@37872
   327
 ?val ct = (string_of_cterm o the o (parse RatArith.thy))
erott@37872
   328
           "a + (b * (c * d) + e)";
erott@37872
   329
 ?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
erott@37872
   330
erott@37872
   331
 toggle trace_rewrite;
erott@37872
   332
 ?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
erott@37872
   333
erott@37872
   334
(*3.5. Calculate numeric constants*)
erott@37872
   335
 calculate;
erott@37872
   336
 calculate_;
erott@37872
   337
erott@37872
   338
 ?calc_list;
erott@37872
   339
 ?calculate "Isac.thy" "plus" "#1 + #2";
erott@37872
   340
 ?calculate "Isac.thy" "times" "#2 * #3";
erott@37872
   341
 ?calculate "Isac.thy" "power" "#2 ^^^ #3";
erott@37872
   342
 ?calculate "Isac.thy" "cancel_" "#9 // #12";
erott@37872
   343
   
erott@37872
   344
erott@37872
   345
(** 4. Term orders **)
erott@37872
   346
(*4.1. Exmpales for term orders*)
erott@37872
   347
 sqrt_right;
erott@37872
   348
 tless_true;
erott@37872
   349
erott@37872
   350
 val t1 = (term_of o the o (parse thy)) "(sqrt a) + b";
erott@37872
   351
 val t2 = (term_of o the o (parse thy)) "b + (sqrt a)";
erott@37872
   352
 ?sqrt_right false SqRoot.thy (t1, t2);
erott@37872
   353
 ?sqrt_right false SqRoot.thy (t2, t1);
erott@37872
   354
erott@37872
   355
 val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d";
erott@37872
   356
 val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d";
erott@37872
   357
 ?sqrt_right true SqRoot.thy (t1, t2);
erott@37872
   358
erott@37872
   359
(*4.2. Ordered rewriting*)   
erott@37872
   360
 ac_plus_times;
erott@37872
   361
erott@37872
   362
(*Give it a try: polynomial (normal) form*)
erott@37872
   363
 val ct' = "#3 * a + b + #2 * a";
erott@37872
   364
 val thm' = ("radd_commute","") : thm';
erott@37872
   365
 ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
erott@37872
   366
 val thm' = ("rdistr_right_assoc_p","") : thm';
erott@37872
   367
 ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
erott@37872
   368
 ?val Some (ct',_) = calculate thy' "plus" ct';
erott@37872
   369
erott@37872
   370
 val ct' = "3 * a + b + 2 * a" : cterm';
erott@37872
   371
 val thm' = ("radd_commute","") : thm';
erott@37872
   372
 ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
erott@37872
   373
 ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
erott@37872
   374
 ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
erott@37872
   375
erott@37872
   376
 toggle trace_rewrite;
erott@37872
   377
 ?rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct;
erott@37872
   378
erott@37872
   379
erott@37872
   380
(** 5. The hierarchy of problem types **)
erott@37872
   381
(*5.1. The standard-function for 'matching'*)
erott@37872
   382
 matches;
erott@37872
   383
erott@37872
   384
 val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
erott@37872
   385
 val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
erott@37872
   386
 atomt p;
Walther@60650
   387
 mk_Var;
Walther@60650
   388
 val pat = mk_Var p;
erott@37872
   389
 matches thy t pat;
erott@37872
   390
erott@37872
   391
 val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";
erott@37872
   392
 matches thy t2 pat;
erott@37872
   393
erott@37872
   394
 val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v";
erott@37872
   395
 matches thy t2 pat2;
erott@37872
   396
erott@37872
   397
(*5.2. Accessing the hierarchy*)
erott@37872
   398
 show_ptyps;
erott@37872
   399
 show_ptyps();
erott@37872
   400
 get_pbt;
erott@37872
   401
 ?get_pbt ["squareroot", "univariate", "equation"];
erott@37872
   402
erott@37872
   403
 store_pbt;
erott@37872
   404
 ?store_pbt
erott@37872
   405
    (prep_pbt SqRoot.thy
erott@37872
   406
    (["newtype","univariate","equation"],
erott@37872
   407
     [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
erott@37872
   408
      ("#Where" ,["contains_root (e_::bool)"]),
erott@37872
   409
      ("#Find"  ,["solutions v_i_"])
erott@37872
   410
     ],
erott@37872
   411
     [("SqRoot.thy","square_equation")]));
erott@37872
   412
 show_ptyps();
erott@37872
   413
erott@37872
   414
(*5.3. Internals of the datastructure*)
erott@37872
   415
(*5.4. Match a problem with a problem type*)
erott@37872
   416
 ?val fmz = ["equality (#1 + #2 * x = #0)",
erott@37872
   417
 	    "solveFor x",
erott@37872
   418
 	    "solutions L"] : fmz;
Walther@60769
   419
 by_formalise;
Walther@60769
   420
 ?by_formalise fmz (get_pbt ["univariate","equation"]);
Walther@60769
   421
 ?by_formalise fmz (get_pbt ["linear","univariate","equation"]);
Walther@60769
   422
 ?by_formalise fmz (get_pbt ["squareroot","univariate","equation"]);
erott@37872
   423
erott@37872
   424
(*5.5. Refine a problem specification *)
erott@37872
   425
 refine;
erott@37872
   426
 ?val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
erott@37872
   427
 	    "solveFor x","errorBound (eps=#0)",
erott@37872
   428
 	    "solutions L"];
erott@37872
   429
 ?refine fmz ["univariate","equation"];
erott@37872
   430
erott@37872
   431
 ?val fmz = ["equality (x+#1=#2)",
erott@37872
   432
 	    "solveFor x","errorBound (eps=#0)",
erott@37872
   433
 	    "solutions L"];
erott@37872
   434
 ?refine fmz ["univariate","equation"];
erott@37872
   435
 
erott@37872
   436
erott@37872
   437
(* 6. Do a calculational proof *)
erott@37872
   438
 ?val fmz = ["equality ((x+#1) * (x+#2) = x^^^#2+#8)","solveFor x",
erott@37872
   439
 	    "errorBound (eps=#0)","solutions L"];
erott@37872
   440
 val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
erott@37872
   441
 				("SqRoot.thy","no_met"));
erott@37872
   442
 
erott@37872
   443
(*6.1. Initialize the calculation*)
erott@37872
   444
 val p = e_pos'; val c = [];
erott@37872
   445
 ?val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
erott@37872
   446
 ?val (p,_,f,nxt,_,pt) = me (mID,m) p c EmptyPtree;
erott@37872
   447
erott@37872
   448
 ?Compiler.Control.Print.printDepth:=8;
erott@37872
   449
 ?f;
erott@37872
   450
 ?Compiler.Control.Print.printDepth:=4;
erott@37872
   451
erott@37872
   452
 ?nxt;
erott@37872
   453
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   454
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   455
erott@37872
   456
(*6.2. The phase of modeling*)
erott@37872
   457
 ?nxt;
erott@37872
   458
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   459
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   460
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   461
erott@37872
   462
 ?Compiler.Control.Print.printDepth:=8;
erott@37872
   463
 ?f;
erott@37872
   464
 ?Compiler.Control.Print.printDepth:=4;
erott@37872
   465
erott@37872
   466
(*6.3. The phase of specification*)
erott@37872
   467
 ?nxt;
erott@37872
   468
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   469
erott@37872
   470
erott@37872
   471
 val nxt = ("Specify_Problem",
erott@37872
   472
	    Specify_Problem ["polynomial","univariate","equation"]);
erott@37872
   473
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   474
erott@37872
   475
 val nxt = ("Specify_Problem",
erott@37872
   476
	    Specify_Problem ["linear","univariate","equation"]);
erott@37872
   477
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   478
 ?Compiler.Control.Print.printDepth:=8;f;Compiler.Control.Print.printDepth:=4;
erott@37872
   479
erott@37872
   480
 val nxt = ("Refine_Problem",
erott@37872
   481
	    Refine_Problem ["linear","univariate","equation"]);
erott@37872
   482
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   483
 ?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
erott@37872
   484
erott@37872
   485
 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
erott@37872
   486
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   487
 ?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
erott@37872
   488
erott@37872
   489
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   490
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   491
erott@37872
   492
(*6.4. The phase of solving*)
erott@37872
   493
 nxt;
erott@37872
   494
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   495
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   496
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   497
erott@37872
   498
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   499
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   500
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   501
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   502
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   503
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   504
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   505
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   506
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   507
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   508
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   509
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   510
erott@37872
   511
(*6.5. The final phase: check the postcondition*)
erott@37872
   512
 ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   513
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
erott@37872
   514
erott@37872
   515
erott@37872
   516
erott@37872
   517
erott@37872
   518
erott@37872
   519