1.1 --- a/doc-isac/mat-eng-en.tex Mon Oct 31 18:28:36 2022 +0100
1.2 +++ b/doc-isac/mat-eng-en.tex Mon Nov 07 17:37:20 2022 +0100
1.3 @@ -332,8 +332,8 @@
1.4 ML>
1.5 ML> sqrt_right;
1.6 val it = fn : rew_ord (* term * term -> bool *)
1.7 - ML> "sqrt_right" : rew_ord';
1.8 - val it = "sqrt_right" : rew_ord'
1.9 + ML> "sqrt_right" : rew_ord;
1.10 + val it = "sqrt_right" : rew_ord
1.11 ML>
1.12 ML> eval_rls;
1.13 val it =
1.14 @@ -341,7 +341,7 @@
1.15 {preconds=[],rew_ord=("sqrt_right",fn),
1.16 rules=[Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,
1.17 Thm #,Thm #,Thm #,Thm #,Thm #,Calc #,Calc #,...],
1.18 - scr=Script (Free #)} : rls
1.19 + program=Script (Free #)} : rls
1.20 ML> "eval_rls" : rls';
1.21 val it = "eval_rls" : rls'
1.22 ML>
1.23 @@ -364,7 +364,7 @@
1.24 ML> rewrite;
1.25 val it = fn
1.26 : theory'
1.27 - -> rew_ord'
1.28 + -> rew_ord
1.29 -> rls' -> bool -> thm' -> cterm' -> (cterm' * cterm' list) option
1.30 \end{verbatim}}%size
1.31 The arguments are the following:\\
1.32 @@ -514,7 +514,7 @@
1.33 ML> rewrite_inst;
1.34 val it = fn
1.35 : theory'
1.36 - -> rew_ord'
1.37 + -> rew_ord
1.38 -> rls'
1.39 -> bool
1.40 -> (cterm' * cterm') list
1.41 @@ -566,7 +566,7 @@
1.42 rules =
1.43 [Thm ("radd_assoc_RS_sym",num_str (radd_assoc RS sym)),
1.44 Thm ("rmult_assoc_RS_sym",num_str (rmult_assoc RS sym))],
1.45 - scr = Script ((term_of o the o (parse thy))
1.46 + program = Script ((term_of o the o (parse thy))
1.47 "empty_script")
1.48 }:rls;
1.49 \end{verbatim}}%size
1.50 @@ -575,7 +575,7 @@
1.51 \item [\tt preconds] are conditions which must be true in order to make the rule set applicable (the empty list evaluates to {\tt true})
1.52 \item [\tt rew\_ord] concerns term orders introduced below in \ref{term-order}
1.53 \item [\tt rules] are the theorems to be applied -- in priciple applied in arbitrary order, because all these rule sets should be 'complete' \cite{nipk:rew-all-that} (and actually the theorems are applied in the sequence they appear in this list). The function {\tt num\_str} must be applied to theorems containing numeral constants (and thus is obsolete in this example). {\tt RS} is an infix function applying the theorem {\tt sym} to {\tt radd\_assoc} before storage (the effect see below)
1.54 -\item [\tt scr] is the script applying the ruleset; it will disappear in later versions of \isac.
1.55 +\item [\tt program] is the script applying the ruleset; it will disappear in later versions of \isac.
1.56 \end{description}
1.57 These variables evaluate to
1.58 {\footnotesize\begin{verbatim}
1.59 @@ -587,7 +587,7 @@
1.60 {preconds=[],rew_ord=("tless_true",fn),
1.61 rules=[Thm ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"),
1.62 Thm ("rmult_assoc_RS_sym","?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")],
1.63 - scr=Script (Free ("empty_script","RealDef.real"))} : rls
1.64 + program=Script (Free ("empty_script","RealDef.real"))} : rls
1.65 \end{verbatim}}%size
1.66
1.67 \paragraph{Give it a try !} The above rule set makes an arbitrary number of parentheses disappear which are not necessary due to associativity of {\tt +} and
1.68 @@ -750,7 +750,7 @@
1.69 Thm ("rmult_commute",rmult_commute),
1.70 Thm ("rmult_left_commute",rmult_left_commute),
1.71 Thm ("rmult_assoc",rmult_assoc)],
1.72 - scr = Script ((term_of o the o (parse thy))
1.73 + program = Script ((term_of o the o (parse thy))
1.74 "empty_script")
1.75 }:rls;
1.76 val ac_plus_times =
1.77 @@ -762,7 +762,7 @@
1.78 Thm ("rmult_commute","?m * ?n = ?n * ?m"),
1.79 Thm ("rmult_left_commute","?x * (?y * ?z) = ?y * (?x * ?z)"),
1.80 Thm ("rmult_assoc","?m * ?n * ?k = ?m * (?n * ?k)")],
1.81 - scr=Script (Free ("empty_script","RealDef.real"))} : rls
1.82 + program=Script (Free ("empty_script","RealDef.real"))} : rls
1.83 \end{verbatim}}%size
1.84 Note that the theorems {\tt radd\_left\_commute} and {\tt rmult\_left\_commute} are really necessary in order to make the rule set 'confluent'~!
1.85
1.86 @@ -931,7 +931,7 @@
1.87 ML> get_pbt ["squareroot", "univariate", "equation"];
1.88 val it =
1.89 {met=[("SqRoot.thy","square_equation")],
1.90 - ppc=[("#Given",(Const (#,#),Free (#,#))),
1.91 + model=[("#Given",(Const (#,#),Free (#,#))),
1.92 ("#Given",(Const (#,#),Free (#,#))),
1.93 ("#Given",(Const (#,#),Free (#,#))),
1.94 ("#Find",(Const (#,#),Free (#,#)))],
1.95 @@ -949,7 +949,7 @@
1.96 where the records fields hold the following data:
1.97 \begin{description}
1.98 \item [\tt thy]: the theory necessary for parsing the formulas
1.99 -\item [\tt ppc]: the items of the problem type, divided into those {\tt Given}, the precondition {\tt Where} and the output item(s) {\tt Find}. The items of {\tt Given} and {\tt Find} are all headed by so-called descriptions, which determine the type. These descriptions are defined in {\tt [isac-src]/Isa99/Descript.thy}.
1.100 +\item [\tt model]: the items of the problem type, divided into those {\tt Given}, the precondition {\tt Where} and the output item(s) {\tt Find}. The items of {\tt Given} and {\tt Find} are all headed by so-called descriptions, which determine the type. These descriptions are defined in {\tt [isac-src]/Isa99/Descript.thy}.
1.101 \item [\tt met]: the list of methods solving this problem type.\\
1.102 \end{description}
1.103
1.104 @@ -978,7 +978,7 @@
1.105 {thy : theory, (* the nearest to the root,
1.106 which allows to compile that pbt *)
1.107 where_: term list, (* where - predicates *)
1.108 - ppc : ((string * (* fields "#Given","#Find" *)
1.109 + model : ((string * (* fields "#Given","#Find" *)
1.110 (term * (* description *)
1.111 term)) (* id *)
1.112 list),
1.113 @@ -1526,7 +1526,7 @@
1.114 {\it fmz}
1.115 & formalization, i.e. a minimal formula representation of an example \\
1.116 {\it met}
1.117 -& a method, i.e. a datastructure holding all informations for the solving phase ({\it rew\_ord}, {\it scr}, etc.)\\
1.118 +& a method, i.e. a datastructure holding all informations for the solving phase ({\it rew\_ord}, {\it program}, etc.)\\
1.119 {\it metID}
1.120 & reference to a {\it met}\\
1.121 {\it op}
1.122 @@ -1541,7 +1541,7 @@
1.123 & ruleset, i.e. a datastructure holding theorems {\it thm} and operators {\it op} for simplification (with a {\it rew\_ord})\\
1.124 {\it Rrls}
1.125 & ruleset for 'reverse rewriting' (an \isac-technique generating stepwise rewriting, e.g. for cancelling fractions)\\
1.126 -{\it scr}
1.127 +{\it program}
1.128 & script describing algorithms by tactics, part of a {\it met} \\
1.129 {\it norm\_rls}
1.130 & special ruleset calculating a normalform, associated with a {\it thy}\\
1.131 @@ -1567,7 +1567,7 @@
1.132 \begin{center}
1.133 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline
1.134 tactic &input & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
1.135 - & &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
1.136 + & &thy &program &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
1.137 \hline\hline
1.138 Init\_Proof
1.139 &fmz & x & & & x & & & & & & & x \\