erott@37872: %WN051006 dropped in code, but interesting for case study 'order a list' erott@37872: %EqSystem.thy erott@37872: %--------------------------------------------------------------------------- erott@37872: % erott@37872: % order'_system :: "bool list => bool list " ("order'_system _") erott@37872: % erott@37872: %EqSystem.ML erott@37872: %--------------------------------------------------------------------------- erott@37872: %(*("order_system", ("EqSystem.order'_system", erott@37872: % eval_order_system "#eval_order_system_"))*) erott@37872: %fun eval_order_system _ "EqSystem.order'_system" erott@37872: % (p as (Const ("EqSystem.order'_system",_) $ ts)) _ = erott@37872: % let val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") []) erott@37872: % (isalist2list ts) erott@37872: % val ts'' = list2isalist HOLogic.boolT ts' erott@37872: % in if ts <> ts'' erott@37872: % then Some (term2str p ^ " = " ^ term2str ts'', erott@37872: % Trueprop $ (mk_equality (p,ts''))) erott@37872: % else None erott@37872: % end erott@37872: % | eval_order_system _ _ _ _ = None; erott@37872: % erott@37872: % erott@37872: %"Script Norm2SystemScript (es_::bool list) (vs_::real list) = \ erott@37872: %\ (let es__ = Try (Rewrite_Set simplify_Integral_parenthesized False) es_; \ erott@37872: %\ es__ = (Try (Calculate order_system_) (order_system es__))\ erott@37872: %\in (SubProblem (Biegelinie_,[linear,system],[no_met])\ erott@37872: %\ [bool_list_ es__, real_list_ vs_]))" erott@37872: % )); erott@37872: % erott@37872: %eqsystem.sml erott@37872: %--------------------------------------------------------------------------- erott@37872: %"----------- eval_sort -------------------------------------------"; erott@37872: %"----------- eval_sort -------------------------------------------"; erott@37872: %"----------- eval_sort -------------------------------------------"; Walther@60566: %val ts = TermC.parse_test @{context} "[c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]"; erott@37872: %val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") []) erott@37872: % (isalist2list ts); erott@37872: %terms2str ts'; erott@37872: %val ts'' = list2isalist HOLogic.boolT ts'; erott@37872: %if term2str ts'' = "[-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]" erott@37872: %then () else raise error "eqsystem.sml eval_sort 1"; erott@37872: % Walther@60566: %val t = TermC.parse_test @{context} "order_system [c_2 = 0,\ erott@37872: % \-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]"; erott@37872: %val Some (str,_) = eval_order_system "" "EqSystem.order'_system" t ""; erott@37872: %if str = "order_system [c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0] = [-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]" then () erott@37872: %else raise error "eqsystem.sml eval_sort 2"; erott@37872: % erott@37872: % erott@37872: % erott@37872: % calculate_ thy ("EqSystem.order'_system", erott@37872: % eval_order_system "#eval_order_system_") t; erott@37872: % erott@37872: %--------------------------------------------------------------------------- erott@37872: %--------------------------------------------------------------------------- erott@37872: %--------------------------------------------------------------------------- erott@37872: erott@37872: erott@37872: %In the following this text is not compatible with isac-code: erott@37872: %* move termorder to knowledge: FIXXXmat0201a erott@37872: % erott@37872: % erott@37872: erott@37872: \documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report} erott@37872: \usepackage{latexsym} % recommended by Ch.Schinagl 10.98 erott@37872: \bibliographystyle{alpha} erott@37872: erott@37872: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} erott@37872: erott@37872: \title{\isac --- Interface for\\ erott@37872: Developers of Math Knowledge\\[1.0ex] erott@37872: and\\[1.0ex] erott@37872: Tools for Experiments in\\ erott@37872: Symbolic Computation\\[1.0ex]} erott@37872: \author{The \isac-Team\\ erott@37872: \tt isac-users@ist.tugraz.at\\[1.0ex]} erott@37872: \date{\today} erott@37872: erott@37872: \begin{document} erott@37872: \maketitle erott@37872: \newpage erott@37872: \tableofcontents erott@37872: \newpage erott@37872: \listoftables erott@37872: \newpage erott@37872: erott@37872: \chapter{Introduction} erott@37872: \section{The scope of this document} erott@37872: \paragraph{As a manual:} This document describes the interface to \isac's kernel (KE), the interface to the mathematics engine (ME) included in the KE, and to the various tools like rewriting, matching etc. erott@37872: erott@37872: \isac's KE is written in SML, the language developed in conjunction with predecessors of the theorem prover Isabelle. Thus, in this document we use the plain ASCII representation of SML code. The reader may note that the \isac-user is presented a completely different view on a graphical user interface. erott@37872: erott@37872: The document is selfcontained; basic knowledge about SML (as an introduction \cite{Paulson:91} is recommended), terms and rewriting is assumed. erott@37872: erott@37872: %The interfaces will be moderately exended during the first phase of development of the mathematics knowledge. The work on the subprojects defined should {\em not} create interfaces of any interest to a user or another author of knowledge except identifiers (of type string) for theorems, rulesets etc. erott@37872: erott@37872: Notation: SML code, directories, file names are {\tt written in 'tt'}; in particular {\tt ML>} is the KE prompt. erott@37872: erott@37872: \paragraph{Give it a try !} Another aim of this text is to give the reader hints for experiments with the tools introduced. erott@37872: erott@37872: \section{Related documents}\label{related-docs} erott@37872: Isabelle reference manual \cite{Isa-ref}, also contained in the Isabelle distribution under $\sim${\tt /doc/}. erott@37872: erott@37872: {\bf The actual locations of files is being recorded in \\{\tt /software/services/isac/README} erott@37872: \footnote{The KEs current version is {\tt isac.020120-math/} which is based on the version Isabelle99 at {\tt http://isabelle.in.tum.de}.\\ erott@37872: The current locations at IST are\\ erott@37872: {\tt [isabelle]\hspace{3em} /software/sol26/Isabelle99/}\\ erott@37872: {\tt [isac-src]\hspace{3em} /software/services/isac/src/ke/}\\ erott@37872: {\tt [isac-bin]\hspace{3em} /software/services/isac/bin/ke/} erott@37872: } erott@37872: and rigorously updated.} In this document we refer to the following directories erott@37872: \begin{tabbing} erott@37872: xxx\=Isabelle sources1234 \=\kill erott@37872: \>Isabelle sources \> {\tt [isabelle]/}\\ erott@37872: \>KE sources \> {\tt [isac-src]/\dots{version}\dots/}\\ erott@37872: \>KE binary \> {\tt [isac-bin]/\dots{version}\dots/} erott@37872: \end{tabbing} erott@37872: where {\tt\dots version\dots} stands for a directory-name containing information on the version. erott@37872: erott@37872: \section{Getting started} erott@37872: Change to the directory {\tt [isac-bin]} where \isac's binary is located and type to the unix-prompt '$>$' (ask your system administrator where the directory {\tt [isac-bin]} is on your system): erott@37872: \begin{verbatim} erott@37872: > [isac-bin]/sml @SMLload=isac.020120-math erott@37872: val it = false : bool erott@37872: ML> erott@37872: \end{verbatim} erott@37872: yielding the message {\tt val it = false : bool} followed by the prompt of the KE. Having been successful so far, just type in the input presented below -- all of it belongs to {\em one} session~! erott@37872: erott@37872: \part{Experimental approach} erott@37872: erott@37872: \chapter{Basics, terms and parsing} erott@37872: Isabelle implements terms of the {\it simply typed lambda calculus} \cite{typed-lambda} defined in $\sim${\tt/src/Pure.ML}. erott@37872: \section{The definition of terms} erott@37872: There are two kinds of terms in Isabelle, 'raw terms' and 'certified terms'. \isac{} works on raw terms, which are efficient but hard to comprehend. erott@37872: {\footnotesize\begin{verbatim} erott@37872: datatype term = erott@37872: Const of string * typ erott@37872: | Free of string * typ erott@37872: | Var of indexname * typ erott@37872: | Bound of int erott@37872: | Abs of string * typ * term erott@37872: | op $ of term * term; erott@37872: erott@37872: datatype typ = Type of string * typ list erott@37872: | TFree of string * sort erott@37872: | TVar of indexname * sort; erott@37872: \end{verbatim}}%size % $ erott@37872: where the definitions of sort and indexname is not relevant in this context. The {\tt typ}e is being inferred during parsing. Parsing creates the other kind of terms, {\tt cterm}. These {\tt cterm}s are encapsulated records, which cannot be composed without the respective Isabelle functions (checking for type correctness), but which then are conveniently displayed as strings (using SML compiler internals -- see below). erott@37872: erott@37872: \section{Theories and parsing} erott@37872: Parsing uses information contained in Isabelles theories $\sim${\tt /src/HOL}. The currently active theory is held in a global variable {\tt thy}; theories can be accessed individually; erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> thy; erott@37872: val it = erott@37872: {ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun, erott@37872: Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat, Arith, erott@37872: Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype, Numeral, Bin, erott@37872: IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option, Map, Record, erott@37872: RelPow, Sexp, String, Calculation, SVC_Oracle, Main, Zorn, Filter, PNat, erott@37872: PRat, PReal, RealDef, RealOrd, RealInt, RealBin, HyperDef, Descript, ListG, erott@37872: Tools, Script, Typefix, Atools, RatArith, SqRoot, Differentiate, DiffAppl, erott@37872: InsSort, Isac} : theory ML> erott@37872: ML> HOL.thy; erott@37872: val it = {ProtoPure, CPure, HOL} : theory erott@37872: ML> erott@37872: ML> parse; erott@37872: val it = fn : theory -> string -> cterm option erott@37872: ML> parse thy "a + b * #3"; erott@37872: val it = Some "a + b * #3" : cterm option erott@37872: ML> erott@37872: ML> val t = (term_of o the) it; erott@37872: val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term erott@37872: \end{verbatim}}%size erott@37872: where {\tt term\_of} and {\tt the} are explained below. The syntax of the list of characters can be read out of Isabelles theories \cite{Isa-obj} {\tt [isabelle]/src/HOL/}\footnote{Or you may use your internetbrowser to look at the files in {\tt [isabelle]/browser\_info}.} erott@37872: and from theories developed with in \isac{} at {\tt [isac-src]/knowledge/}. Note that the syntax of the terms is different from those displayed at \isac's frontend after conversion to MathML. erott@37872: erott@37872: erott@37872: \section{Displaying terms} erott@37872: The print depth on the SML top-level can be set in order to produce output in the amount of detail desired: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> Compiler.Control.Print.printDepth; erott@37872: val it = ref 4 : int ref erott@37872: ML> erott@37872: ML> Compiler.Control.Print.printDepth:= 2; erott@37872: val it = () : unit erott@37872: ML> t; erott@37872: val it = # $ # $ (# $ #) : term erott@37872: ML> erott@37872: ML> Compiler.Control.Print.printDepth:= 6; erott@37872: val it = () : unit erott@37872: ML> t; erott@37872: val it = erott@37872: Const ("op +","[RealDef.real, RealDef.real] => RealDef.real") $ erott@37872: Free ("a","RealDef.real") $ erott@37872: (Const ("op *","[RealDef.real, RealDef.real] => RealDef.real") $ erott@37872: Free ("b","RealDef.real") $ Free ("#3","RealDef.real")) : term erott@37872: \end{verbatim}}%size % $ erott@37872: A closer look to the latter output shows that {\tt typ} is output as a string like {\tt cterm}. Other useful settings for the output are: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> Compiler.Control.Print.printLength; erott@37872: val it = ref 8 : int ref erott@37872: ML> Compiler.Control.Print.stringDepth; erott@37872: val it = ref 250 : int ref erott@37872: \end{verbatim}}%size erott@37872: Anyway, the SML output of terms is not very readable; there are functions in the KE to display them: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> atomt; erott@37872: val it = fn : term -> unit erott@37872: ML> atomt t; erott@37872: *** ------------- erott@37872: *** Const ( op +) erott@37872: *** . Free ( a, ) erott@37872: *** . Const ( op *) erott@37872: *** . . Free ( b, ) erott@37872: *** . . Free ( #3, ) erott@37872: val it = () : unit erott@37872: ML> Walther@60650: ML> TermC.atom_trace_detail \@\{context\}; erott@37872: val it = fn : theory -> term -> unit Walther@60650: ML> TermC.atom_trace_detail \@\{context\} t; erott@37872: *** ------------- erott@37872: *** Const ( op +, [real, real] => real) erott@37872: *** . Free ( a, real) erott@37872: *** . Const ( op *, [real, real] => real) erott@37872: *** . . Free ( b, real) erott@37872: *** . . Free ( #3, real) erott@37872: val it = () : unit erott@37872: \end{verbatim}}%size erott@37872: where again the {\tt typ}s are rendered as strings, but more elegantly by use of the information contained in {\tt thy}.. erott@37872: erott@37872: \paragraph{Give it a try !} {\bf The mathematics knowledge grows} as it is defined in Isabelle theory by theory. Have a look by your internet browser to the hierarchy of those theories at {\tt [isabelle]/src/HOL/HOL.thy} and its children available on your system. Or you may use your internetbrowser to look at the files in {\tt [isabelle]/browser\_info}. erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> (*-1-*) parse HOL.thy "#2^^^#3"; erott@37872: *** Inner lexical error at: "^^^#3" erott@37872: val it = None : cterm option erott@37872: ML> erott@37872: ML> (*-2-*) parse HOL.thy "d_d x (a + x)"; erott@37872: val it = None : cterm option erott@37872: ML> erott@37872: ML> erott@37872: ML> (*-3-*) parse RatArith.thy "#2^^^#3"; erott@37872: val it = Some "#2 ^^^ #3" : cterm option erott@37872: ML> erott@37872: ML> (*-4-*) parse RatArith.thy "d_d x (a + x)"; erott@37872: val it = Some "d_d x (a + x)" : cterm option erott@37872: ML> erott@37872: ML> erott@37872: ML> (*-5-*) parse Differentiate.thy "d_d x (a + x)"; erott@37872: val it = Some "d_d x (a + x)" : cterm option erott@37872: ML> erott@37872: ML> (*-6-*) parse Differentiate.thy "#2^^^#3"; erott@37872: val it = Some "#2 ^^^ #3" : cterm option erott@37872: \end{verbatim}}%size erott@37872: Don't trust the string representation: if we convert {\tt(*-4-*)} and {\tt(*-6-*)} to terms \dots erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> (*-4-*) val thy = RatArith.thy; Walther@60650: ML> ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)"; erott@37872: *** ------------- erott@37872: *** Free ( d_d, [real, real] => real) erott@37872: *** . Free ( x, real) erott@37872: *** . Const ( op +, [real, real] => real) erott@37872: *** . . Free ( a, real) erott@37872: *** . . Free ( x, real) erott@37872: val it = () : unit erott@37872: ML> erott@37872: ML> (*-6-*) val thy = Differentiate.thy; Walther@60650: ML> ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)"; erott@37872: *** ------------- erott@37872: *** Const ( Differentiate.d_d, [real, real] => real) erott@37872: *** . Free ( x, real) erott@37872: *** . Const ( op +, [real, real] => real) erott@37872: *** . . Free ( a, real) erott@37872: *** . . Free ( x, real) erott@37872: val it = () : unit erott@37872: \end{verbatim}}%size erott@37872: \dots we see: in {\tt(*-4-*)} we have an arbitrary function {\tt Free ( d\_d, \_)} and in {\tt(*-6-*)} we have the special function constant {\tt Const ( Differentiate.d\_d, \_)} for differentiation, which is defined in {\tt Differentiate.thy} and presumerably is meant. erott@37872: erott@37872: erott@37872: \section{Converting terms} erott@37872: The conversion from {\tt cterm} to {\tt term} has been shown above: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> term_of; erott@37872: val it = fn : cterm -> term erott@37872: ML> erott@37872: ML> the; erott@37872: val it = fn : 'a option -> 'a erott@37872: ML> erott@37872: ML> val t = (term_of o the o (parse thy)) "a + b * #3"; erott@37872: val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term erott@37872: \end{verbatim}}%size erott@37872: where {\tt the} unwraps the {\tt term option} --- an auxiliary function from Larry Paulsons basic library at {\tt [isabelle]/src/Pure/library.ML}, which is really worthwile to study for any SML programmer. erott@37872: erott@37872: The other conversions are the following, some of which use the {\it signature} {\tt sign} of a theory: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> sign_of; erott@37872: val it = fn : theory -> Sign.sg erott@37872: ML> erott@37872: ML> cterm_of; erott@37872: val it = fn : Sign.sg -> term -> cterm erott@37872: ML> val ct = cterm_of (sign_of thy) t; erott@37872: val ct = "a + b * #3" : cterm erott@37872: ML> erott@37872: ML> Sign.string_of_term; erott@37872: val it = fn : Sign.sg -> term -> string erott@37872: ML> Sign.string_of_term (sign_of thy) t; erott@37872: val it = "a + b * #3" : ctem' erott@37872: ML> erott@37872: ML> string_of_cterm; erott@37872: val it = fn : cterm -> string erott@37872: ML> string_of_cterm ct; erott@37872: val it = "a + b * #3" : ctem' erott@37872: \end{verbatim}}%size erott@37872: erott@37872: \section{Theorems} erott@37872: Theorems are a type, {\tt thm}, even more protected than {\tt cterms}: they are defined as axioms or proven in Isabelle. These definitions and proofs are contained in theories in the directory {\tt[isac-src]/knowledge/}, e.g. the theorem {\tt diff\_sum} in the theory {\tt[isac-src]/knowledge/Differentiate.thy}. Additionally, each theorem has to be recorded for \isac{} in the respective {\tt *.ML}, e.g. {\tt diff\_sum} in {\tt[isac-src]/knowledge/Differentiate.ML} as follows: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> theorem' := overwritel (!theorem', erott@37872: [("diff_const",num_str diff_const) erott@37872: ]); erott@37872: \end{verbatim}}%size erott@37872: The additional recording of theorems and other values will disappear in later versions of \isac. erott@37872: erott@37872: \chapter{Rewriting} erott@37872: \section{The arguments for rewriting} erott@37872: The type identifiers of the arguments and values of the rewrite-functions in \ref{rewrite} differ only in an apostroph: the apostrohped types are re-named strings in order to maintain readability. erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> HOL.thy; erott@37872: val it = {ProtoPure, CPure, HOL} : theory erott@37872: ML> "HOL.thy" : theory'; erott@37872: val it = "HOL.thy" : theory' erott@37872: ML> erott@37872: ML> sqrt_right; erott@37872: val it = fn : rew_ord (* term * term -> bool *) Walther@60586: ML> "sqrt_right" : rew_ord; Walther@60586: val it = "sqrt_right" : rew_ord erott@37872: ML> erott@37872: ML> eval_rls; erott@37872: val it = erott@37872: Rls erott@37872: {preconds=[],rew_ord=("sqrt_right",fn), erott@37872: rules=[Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #, erott@37872: Thm #,Thm #,Thm #,Thm #,Thm #,Calc #,Calc #,...], Walther@60586: program=Script (Free #)} : rls erott@37872: ML> "eval_rls" : rls'; erott@37872: val it = "eval_rls" : rls' erott@37872: ML> erott@37872: ML> diff_sum; erott@37872: val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : thm erott@37872: ML> ("diff_sum", "") : thm'; erott@37872: val it = ("diff_sum","") : thm' erott@37872: \end{verbatim}}%size erott@37872: where a {\tt thm'} is a pair, eventually with the string-representation of the respective theorem. erott@37872: erott@37872: \section{The functions for rewriting}\label{rewrite} erott@37872: Rewriting comes along with two equivalent functions, where the first is being actually used within the KE, and the second one is useful for tests: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> rewrite_; erott@37872: val it = fn erott@37872: : theory erott@37872: -> rew_ord erott@37872: -> rls -> bool -> thm -> term -> (term * term list) option erott@37872: ML> erott@37872: ML> rewrite; erott@37872: val it = fn erott@37872: : theory' Walther@60586: -> rew_ord erott@37872: -> rls' -> bool -> thm' -> cterm' -> (cterm' * cterm' list) option erott@37872: \end{verbatim}}%size erott@37872: The arguments are the following:\\ erott@37872: \tabcolsep=4mm erott@37872: \def\arraystretch{1.5} erott@37872: \begin{tabular}{lp{11.0cm}} erott@37872: {\tt theory} & the Isabelle theory containing the definitions necessary for parsing the {\tt term} \\ erott@37872: {\tt rew\_ord}& the rewrite order \cite{nipk:rew-all-that} for ordered rewriting -- see the section \ref{term-order} below. For {\em no} ordered rewriting take {\tt tless\_true}, a dummy order yielding true for all arguments \\ erott@37872: {\tt rls} & the rule set for evaluating the condition within {\tt thm} in case {\tt thm} is a conditional rule \\ erott@37872: {\tt bool} & a flag which triggers the evaluation of the eventual condition in {\tt thm}: if {\tt false} then evaluate the condition and according to the result of the evaluation apply {\tt thm} or not (conditional rewriting \cite{nipk:rew-all-that}), if {\tt true} then don't evaluate the condition, but put it into the set of assumptions \\ erott@37872: {\tt thm} & the theorem used to try to rewrite {\tt term} \\ erott@37872: {\tt term} & the term eventually rewritten by {\tt thm} \\ erott@37872: \end{tabular}\\ erott@37872: erott@37872: \noindent The respective values of {\tt rewrite\_} and {\tt rewrite} are an {\tt option} of a pair, i.e. {\tt Some(\_,\_)} in case the {\tt term} can be rewritten by {\tt thm} w.r.t. {\tt rew\_ord} and/or {\tt rls}, or {\tt None} if no rewrite is found:\\ erott@37872: \begin{tabular}{lp{10.4cm}} erott@37872: {\tt term} & the term rewritten \\ erott@37872: {\tt term list}& the assumptions eventually generated if the {\tt bool} flag is set to {\tt true} and {\tt thm} is applicable. \\ erott@37872: \end{tabular}\\ erott@37872: erott@37872: \paragraph{Give it a try !} {\bf\dots rewriting is fun~!} many examples can be found in {\tt [isac-src]/tests/\dots}. In {\tt [isac-src]/tests/differentiate.sml} the following can be found: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val thy' = "Differentiate.thy"; erott@37872: val thy' = "Differentiate.thy" : string erott@37872: ML> val ct = "d_d x (x ^^^ #2 + #3 * x + #4)"; erott@37872: val ct = "d_d x (x ^^^ #2 + #3 * x + #4)" : cterm' erott@37872: ML> erott@37872: ML> val thm = ("diff_sum",""); erott@37872: val thm = ("diff_sum","") : thm' erott@37872: ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true erott@37872: [("bdv","x::real")] thm ct; erott@37872: val ct = "d_d x (x ^^^ #2 + #3 * x) + d_d x #4" : cterm' erott@37872: ML> erott@37872: ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true erott@37872: [("bdv","x::real")] thm ct; erott@37872: val ct = "d_d x (x ^^^ #2) + d_d x (#3 * x) + d_d x #4" : cterm' erott@37872: ML> erott@37872: ML> val thm = ("diff_prod_const",""); erott@37872: val thm = ("diff_prod_const","") : thm' erott@37872: ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true erott@37872: [("bdv","x::real")] thm ct; erott@37872: val ct = "d_d x (x ^^^ #2) + #3 * d_d x x + d_d x #4" : cterm' erott@37872: \end{verbatim}}%size erott@37872: You can look up the theorems in {\tt [isac-src]/knowledge/Differentiate.thy} and try to apply them until you get the result you would expect if calculating by hand. erott@37872: \footnote{Hint: At the end you will need {\tt val (ct,\_) = the (rewrite\_set thy' "eval\_rls" false "SqRoot\_simplify" ct);}} erott@37872: erott@37872: \paragraph{Give it a try !}\label{cond-rew} {\bf Conditional rewriting} is a more powerful technique then ordinary rewriting, and is closer to the power of programming languages (see the subsequent 'try it out'~!). The following example expands a term to poynomial form: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val thy' = "Isac.thy"; erott@37872: val thy' = "Isac.thy" : string erott@37872: ML> val ct' = "#3 * a + #2 * (a + #1)"; erott@37872: val ct' = "#3 * a + #2 * (a + #1)" : cterm' erott@37872: ML> erott@37872: ML> val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n"); erott@37872: val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n") erott@37872: : thm' erott@37872: ML> (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: val ct' = "#3 * a + (#2 * a + #2 * #1)" : cterm' erott@37872: ML> erott@37872: ML> val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"); erott@37872: val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1") erott@37872: : thm' erott@37872: ML> (*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: val ct' = "#3 * a + #2 * a + #2 * #1" : cterm' erott@37872: ML> erott@37872: ML> val thm' = ("rcollect_right", erott@37872: "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n"); erott@37872: val thm' = erott@37872: ("rcollect_right", erott@37872: "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n") erott@37872: : thm' erott@37872: ML> (*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: val ct' = "(#3 + #2) * a + #2 * #1" : cterm' erott@37872: ML> erott@37872: ML> (*4*) val Some (ct',_) = calculate' thy' "plus" ct'; erott@37872: val ct' = "#5 * a + #2 * #1" : cterm' erott@37872: ML> erott@37872: ML> (*5*) val Some (ct',_) = calculate' thy' "times" ct'; erott@37872: val ct' = "#5 * a + #2" : cterm' erott@37872: \end{verbatim}}%size erott@37872: Note, that the two rules, {\tt radd\_mult\_distrib2} in {\tt(*1*)} and {\tt rcollect\_right} in {\tt(*3*)} would neutralize each other (i.e. a rule set would not terminate), if there would not be the condition {\tt is\_const}. erott@37872: erott@37872: \paragraph{Give it a try !} {\bf Functional programming} can, within a certain range, modeled by rewriting. In {\tt [isac-src]/\dots/tests/InsSort.thy} the following rules can be found, which are able to sort a list ('insertion sort'): erott@37872: {\footnotesize\begin{verbatim} erott@37872: sort_def "sort ls = foldr ins ls []" erott@37872: erott@37872: ins_base "ins [] a = [a]" erott@37872: ins_rec "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))" erott@37872: erott@37872: foldr_base "foldr f [] a = a" erott@37872: foldr_rec "foldr f (x#xs) a = foldr f xs (f a x)" erott@37872: erott@37872: if_True "(if True then ?x else ?y) = ?x" erott@37872: if_False "(if False then ?x else ?y) = ?y" erott@37872: \end{verbatim}}%size erott@37872: where {\tt\#} is the list-constructor, {\tt foldr} is the well-known standard function of functional programming, and {\tt if\_True, if\_False} are auxiliary rules. Then the sort may be done by the following rewrites: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val thy' = "InsSort.thy"; erott@37872: val thy' = "InsSort.thy" : theory' erott@37872: ML> val ct = "sort [#1,#3,#2]" : cterm'; erott@37872: val ct = "sort [#1,#3,#2]" : cterm' erott@37872: ML> erott@37872: ML> val thm = ("sort_def",""); erott@37872: ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: val ct = "foldr ins [#1, #3, #2] []" : cterm' erott@37872: ML> erott@37872: ML> val thm = ("foldr_rec",""); erott@37872: ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: val ct = "foldr ins [#3, #2] (ins [] #1)" : cterm' erott@37872: ML> erott@37872: ML> val thm = ("ins_base",""); erott@37872: ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: val ct = "foldr ins [#3, #2] [#1]" : cterm' erott@37872: ML> erott@37872: ML> val thm = ("foldr_rec",""); erott@37872: ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: val ct = "foldr ins [#2] (ins [#1] #3)" : cterm' erott@37872: ML> erott@37872: ML> val thm = ("ins_rec",""); erott@37872: ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])" erott@37872: : cterm' erott@37872: ML> erott@37872: ML> val (ct,_) = the (calculate' thy' "le" ct); erott@37872: val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])" : cterm' erott@37872: ML> erott@37872: ML> val thm = ("if_True","(if True then ?x else ?y) = ?x"); erott@37872: ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); erott@37872: val ct = "foldr ins [#2] (#1 # ins [] #3)" : cterm' erott@37872: ML> erott@37872: ... erott@37872: val ct = "sort [#1,#3,#2]" : cterm' erott@37872: \end{verbatim}}%size erott@37872: erott@37872: erott@37872: \section{Variants of rewriting} erott@37872: Some of the above examples already used variants of {\tt rewrite} all of which have the same value, and very similar arguments: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> rewrite_inst_; erott@37872: val it = fn erott@37872: : theory erott@37872: -> rew_ord erott@37872: -> rls erott@37872: -> bool erott@37872: -> (cterm' * cterm') list erott@37872: -> thm -> term -> (term * term list) option erott@37872: ML> rewrite_inst; erott@37872: val it = fn erott@37872: : theory' Walther@60586: -> rew_ord erott@37872: -> rls' erott@37872: -> bool erott@37872: -> (cterm' * cterm') list erott@37872: -> thm' -> cterm' -> (cterm' * cterm' list) option erott@37872: ML> erott@37872: ML> rewrite_set_; erott@37872: val it = fn erott@37872: : theory -> rls -> bool -> rls -> term -> (term * term list) option erott@37872: ML> rewrite_set; erott@37872: val it = fn erott@37872: : theory' -> rls' -> bool -> rls' -> cterm' -> (cterm' * cterm' list) option erott@37872: ML> erott@37872: ML> rewrite_set_inst_; erott@37872: val it = fn erott@37872: : theory erott@37872: -> rls erott@37872: -> bool erott@37872: -> (cterm' * cterm') list erott@37872: -> rls -> term -> (term * term list) option erott@37872: ML> rewrite_set_inst; erott@37872: val it = fn erott@37872: : theory' erott@37872: -> rls' erott@37872: -> bool erott@37872: -> (cterm' * cterm') list erott@37872: -> rls' -> cterm' -> (cterm' * cterm' list) option erott@37872: \end{verbatim}}%size erott@37872: erott@37872: \noindent The variant {\tt rewrite\_inst} substitutes {\tt (term * term) list} in {\tt thm} before rewriting,\\ erott@37872: the variant {\tt rewrite\_set} rewrites with a whole rule set {\tt rls} (instead with a {\tt thm} only),\\ erott@37872: the variant {\tt rewrite\_set\_inst} is a combination of the latter two variants. In order to watch how a term is rewritten theorem by theorem, there is a switch {\tt trace\_rewrite}: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> toggle; erott@37872: val it = fn : bool ref -> bool erott@37872: ML> erott@37872: ML> toggle trace_rewrite; erott@37872: val it = true : bool erott@37872: ML> toggle trace_rewrite; erott@37872: val it = false : bool erott@37872: \end{verbatim}}%size erott@37872: erott@37872: \section{Rule sets} erott@37872: Some of the variants of {\tt rewrite} above do not only apply one theorem, but a whole set of theorems, called a 'rule set'. Such a rule set is applied as long one of its elements can be used for a rewrite (which can go forever, i.e. the rule set eventually does not 'terminate'). erott@37872: erott@37872: A simple example of a rule set is {\tt rearrange\_assoc} which is defined in {\tt knowledge/RatArith.ML} as: erott@37872: {\footnotesize\begin{verbatim} erott@37872: val rearrange_assoc = erott@37872: Rls{preconds = [], rew_ord = ("tless_true",tless_true), erott@37872: rules = erott@37872: [Thm ("radd_assoc_RS_sym",num_str (radd_assoc RS sym)), erott@37872: Thm ("rmult_assoc_RS_sym",num_str (rmult_assoc RS sym))], Walther@60586: program = Script ((term_of o the o (parse thy)) erott@37872: "empty_script") erott@37872: }:rls; erott@37872: \end{verbatim}}%size erott@37872: where erott@37872: \begin{description} erott@37872: \item [\tt preconds] are conditions which must be true in order to make the rule set applicable (the empty list evaluates to {\tt true}) erott@37872: \item [\tt rew\_ord] concerns term orders introduced below in \ref{term-order} erott@37872: \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) Walther@60586: \item [\tt program] is the script applying the ruleset; it will disappear in later versions of \isac. erott@37872: \end{description} erott@37872: These variables evaluate to erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> sym; erott@37872: val it = "?s = ?t ==> ?t = ?s" : thm erott@37872: ML> rearrange_assoc; erott@37872: val it = erott@37872: Rls erott@37872: {preconds=[],rew_ord=("tless_true",fn), erott@37872: rules=[Thm ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"), erott@37872: Thm ("rmult_assoc_RS_sym","?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")], Walther@60586: program=Script (Free ("empty_script","RealDef.real"))} : rls erott@37872: \end{verbatim}}%size erott@37872: erott@37872: \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 erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val ct = (string_of_cterm o the o (parse RatArith.thy)) erott@37872: "a + (b * (c * d) + e)"; erott@37872: val ct = "a + ((b * (c * d) + e) + f)" : cterm' erott@37872: ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct; erott@37872: val it = Some ("a + b * c * d + e + f",[]) : (string * string list) option erott@37872: \end{verbatim}}%size erott@37872: For acchieving this result the rule set has to be surprisingly busy: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> toggle trace_rewrite; erott@37872: val it = true : bool erott@37872: ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct; erott@37872: ### trying thm 'radd_assoc_RS_sym' erott@37872: ### rewrite_set_: a + b * (c * d) + e erott@37872: ### trying thm 'radd_assoc_RS_sym' erott@37872: ### trying thm 'rmult_assoc_RS_sym' erott@37872: ### rewrite_set_: a + b * c * d + e erott@37872: ### trying thm 'rmult_assoc_RS_sym' erott@37872: ### trying thm 'radd_assoc_RS_sym' erott@37872: ### trying thm 'rmult_assoc_RS_sym' erott@37872: val it = Some ("a + b * c * d + e",[]) : (string * string list) option erott@37872: \end{verbatim}}%size erott@37872: erott@37872: erott@37872: \section{Calculate numeric constants} erott@37872: As soon as numeric constants are in adjacent subterms (see the example on p.\pageref{cond-rew}), they can be calculated by the function erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> calculate; erott@37872: val it = fn : theory' -> string -> cterm' -> (cterm' * thm') option erott@37872: ML> calculate_; erott@37872: val it = fn : theory -> string -> term -> (term * (string * thm)) option erott@37872: \end{verbatim}}%size erott@37872: where the {\tt string} in the arguments defines the algebraic operation to be calculated. The function returns the result of the calculation, and as second element in the pair the theorem applied. The following algebraic operations are available: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> calc_list; erott@37872: val it = erott@37872: ref erott@37872: [("plus",("op +",fn)), erott@37872: ("times",("op *",fn)), erott@37872: ("cancel_",("cancel",fn)), erott@37872: ("power",("pow",fn)), erott@37872: ("sqrt",("sqrt",fn)), erott@37872: ("Var",("Var",fn)), erott@37872: ("Length",("Length",fn)), erott@37872: ("Nth",("Nth",fn)), erott@37872: ("power",("pow",fn)), erott@37872: ("le",("op <",fn)), erott@37872: ("leq",("op <=",fn)), erott@37872: ("is_const",("is'_const",fn)), erott@37872: ("is_root_free",("is'_root'_free",fn)), erott@37872: ("contains_root",("contains'_root",fn)), erott@37872: ("ident",("ident",fn))] erott@37872: : (string * (string * (string -> term -> theory -> erott@37872: (string * term) option))) list ref erott@37872: \end{verbatim}}%size erott@37872: These operations can be used in the following way. erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> calculate' "Isac.thy" "plus" "#1 + #2"; erott@37872: val it = Some ("#3",("#add_#1_#2","\"#1 + #2 = #3\"")) : (string * thm') option erott@37872: ML> erott@37872: ML> calculate' "Isac.thy" "times" "#2 * #3"; erott@37872: val it = Some ("#6",("#mult_#2_#3","\"#2 * #3 = #6\"")) erott@37872: : (string * thm') option erott@37872: ML> erott@37872: ML> calculate' "Isac.thy" "power" "#2 ^^^ #3"; erott@37872: val it = Some ("#8",("#power_#2_#3","\"#2 ^^^ #3 = #8\"")) erott@37872: : (string * thm') option erott@37872: ML> erott@37872: ML> calculate' "Isac.thy" "cancel_" "#9 // #12"; erott@37872: val it = Some ("#3 // #4",("#cancel_#9_#12","\"#9 // #12 = #3 // #4\"")) erott@37872: : (string * thm') option erott@37872: ML> erott@37872: ML> ... erott@37872: \end{verbatim}}%size erott@37872: erott@37872: erott@37872: erott@37872: \chapter{Term orders}\label{term-order} erott@37872: Orders on terms are indispensable for the purpose of rewriting to normal forms in associative - commutative domains \cite{nipk:rew-all-that}, and for rewriting to normal forms necessary for matching models to problems, see sect.\ref{pbt}. erott@37872: \section{Examples for term orders} erott@37872: It is not trivial to construct a relation $<$ on terms such that it is really an order, i.e. a transitive and antisymmetric relation. These orders are 'recursive path orders' \cite{nipk:rew-all-that}. Some orders implemented in the knowledgebase at {\tt [isac-src]/knowledge/\dots}, %FIXXXmat0201a erott@37872: e.g. erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> sqrt_right; erott@37872: val it = fn : bool -> theory -> term * term -> bool erott@37872: ML> tless_true; erott@37872: val it = fn : 'a -> bool erott@37872: \end{verbatim}}%size erott@37872: where the bool argument is a switch for tracing the checks on the respective subterms (and theory is necessary for displyinging the (sub-)terms as strings in the case of 'true'). The order {\tt tless\_true} is a dummy always yielding {\tt true}, and {\tt sqrt\_right} prefers a square root shifted to the right within a term: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val t1 = (term_of o the o (parse thy)) "(sqrt a) + b"; erott@37872: val t1 = Const # $ (# $ #) $ Free (#,#) : term erott@37872: ML> erott@37872: ML> val t2 = (term_of o the o (parse thy)) "b + (sqrt a)"; erott@37872: val t2 = Const # $ Free # $ (Const # $ Free #) : term erott@37872: ML> erott@37872: ML> sqrt_right false SqRoot.thy (t1, t2); erott@37872: val it = false : bool erott@37872: ML> sqrt_right false SqRoot.thy (t2, t1); erott@37872: val it = true : bool erott@37872: \end{verbatim}}%size erott@37872: The many checks performed recursively through all subterms can be traced throughout the algorithm in {\tt [isac-src]/knowledge/SqRoot.ML} by setting the flag to true: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d"; erott@37872: val t1 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term erott@37872: ML> erott@37872: ML> val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d"; erott@37872: val t2 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term erott@37872: ML> erott@37872: ML> sqrt_right true SqRoot.thy (t1, t2); erott@37872: t= f@ts= "op +" @ "[a + b * sqrt c,d]" erott@37872: u= g@us= "op +" @ "[a + sqrt b * c,d]" erott@37872: size_of_term(t,u)= (8, 8) erott@37872: hd_ord(f,g) = EQUAL erott@37872: terms_ord(ts,us) = LESS erott@37872: ------- erott@37872: t= f@ts= "op +" @ "[a,b * sqrt c]" erott@37872: u= g@us= "op +" @ "[a,sqrt b * c]" erott@37872: size_of_term(t,u)= (6, 6) erott@37872: hd_ord(f,g) = EQUAL erott@37872: terms_ord(ts,us) = LESS erott@37872: ------- erott@37872: t= f@ts= "a" @ "[]" erott@37872: u= g@us= "a" @ "[]" erott@37872: size_of_term(t,u)= (1, 1) erott@37872: hd_ord(f,g) = EQUAL erott@37872: terms_ord(ts,us) = EQUAL erott@37872: ------- erott@37872: t= f@ts= "op *" @ "[b,sqrt c]" erott@37872: u= g@us= "op *" @ "[sqrt b,c]" erott@37872: size_of_term(t,u)= (4, 4) erott@37872: hd_ord(f,g) = EQUAL erott@37872: terms_ord(ts,us) = LESS erott@37872: ------- erott@37872: t= f@ts= "b" @ "[]" erott@37872: u= g@us= "sqrt" @ "[b]" erott@37872: size_of_term(t,u)= (1, 2) erott@37872: hd_ord(f,g) = LESS erott@37872: terms_ord(ts,us) = LESS erott@37872: ------- erott@37872: val it = true : bool erott@37872: \end{verbatim}}%size erott@37872: erott@37872: erott@37872: erott@37872: \section{Ordered rewriting} erott@37872: Rewriting faces problems in just the most elementary domains, which are all associative and commutative w.r.t. {\tt +} and {\tt *} --- the law of commutativity applied within a rule set causes this set not to terminate~! One method to cope with this difficulty is ordered rewriting, where a rewrite is only done if the resulting term is smaller w.r.t. a term order (with some additional properties called 'rewrite orders' \cite{nipk:rew-all-that}). erott@37872: erott@37872: Such a rule set {\tt ac\_plus\_times}, called an AC-rewrite system, can be found in {\tt[isac-src]/knowledge/RathArith.ML}: erott@37872: {\footnotesize\begin{verbatim} erott@37872: val ac_plus_times = erott@37872: Rls{preconds = [], rew_ord = ("term_order",term_order), erott@37872: rules = erott@37872: [Thm ("radd_commute",radd_commute), erott@37872: Thm ("radd_left_commute",radd_left_commute), erott@37872: Thm ("radd_assoc",radd_assoc), erott@37872: Thm ("rmult_commute",rmult_commute), erott@37872: Thm ("rmult_left_commute",rmult_left_commute), erott@37872: Thm ("rmult_assoc",rmult_assoc)], Walther@60586: program = Script ((term_of o the o (parse thy)) erott@37872: "empty_script") erott@37872: }:rls; erott@37872: val ac_plus_times = erott@37872: Rls erott@37872: {preconds=[],rew_ord=("term_order",fn), erott@37872: rules=[Thm ("radd_commute","?m + ?n = ?n + ?m"), erott@37872: Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), erott@37872: Thm ("radd_assoc","?m + ?n + ?k = ?m + (?n + ?k)"), erott@37872: Thm ("rmult_commute","?m * ?n = ?n * ?m"), erott@37872: Thm ("rmult_left_commute","?x * (?y * ?z) = ?y * (?x * ?z)"), erott@37872: Thm ("rmult_assoc","?m * ?n * ?k = ?m * (?n * ?k)")], Walther@60586: program=Script (Free ("empty_script","RealDef.real"))} : rls erott@37872: \end{verbatim}}%size erott@37872: Note that the theorems {\tt radd\_left\_commute} and {\tt rmult\_left\_commute} are really necessary in order to make the rule set 'confluent'~! erott@37872: erott@37872: erott@37872: \paragraph{Give it a try !} Ordered rewriting is one technique to produce polynomial normal from from arbitrary integer terms: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val ct' = "#3 * a + b + #2 * a"; erott@37872: val ct' = "#3 * a + b + #2 * a" : cterm' erott@37872: ML> erott@37872: ML> (*-1-*) radd_commute; val thm' = ("radd_commute","") : thm'; erott@37872: val it = "?m + ?n = ?n + ?m" : thm erott@37872: val thm' = ("radd_commute","") : thm' erott@37872: ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: val ct' = "#2 * a + (#3 * a + b)" : cterm' erott@37872: ML> erott@37872: ML> (*-2-*) rdistr_right_assoc_p; val thm' = ("rdistr_right_assoc_p","") : thm'; erott@37872: val it = "?l * ?n + (?m * ?n + ?k) = (?l + ?m) * ?n + ?k" : thm erott@37872: val thm' = ("rdistr_right_assoc_p","") : thm' erott@37872: ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: val ct' = "(#2 + #3) * a + b" : cterm' erott@37872: ML> erott@37872: ML> (*-3-*) erott@37872: ML> val Some (ct',_) = calculate thy' "plus" ct'; erott@37872: val ct' = "#5 * a + b" : cterm' erott@37872: \end{verbatim}}%size %FIXXXmat0201b ... calculate ! erott@37872: This looks nice, but if {\tt radd\_commute} is applied automatically in {\tt (*-1-*)} without checking the resulting term to be 'smaller' w.r.t. a term order, then rewritin goes on forever (i.e. it does not 'terminate') \dots erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val ct' = "#3 * a + b + #2 * a" : cterm'; erott@37872: val ct' = "#3 * a + b + #2 * a" : cterm' erott@37872: ML> val thm' = ("radd_commute","") : thm'; erott@37872: val thm' = ("radd_commute","") : thm' erott@37872: ML> erott@37872: ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: val ct' = "#2 * a + (#3 * a + b)" : cterm' erott@37872: ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: val ct' = "#3 * a + b + #2 * a" : cterm' erott@37872: ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; erott@37872: val ct' = "#2 * a + (#3 * a + b)" : cterm' erott@37872: .......... erott@37872: \end{verbatim}}%size erott@37872: erott@37872: Ordered rewriting with the above AC-rewrite system {\tt ac\_plus\_times} performs a kind of bubble sort which can be traced: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> toggle trace_rewrite; erott@37872: val it = true : bool erott@37872: ML> erott@37872: ML> rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct; erott@37872: ### trying thm 'radd_commute' erott@37872: ### not: "a + (b * (c * d) + e)" > "b * (c * d) + e + a" erott@37872: ### rewrite_set_: a + (e + b * (c * d)) erott@37872: ### trying thm 'radd_commute' erott@37872: ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a" erott@37872: ### not: "e + b * (c * d)" > "b * (c * d) + e" erott@37872: ### trying thm 'radd_left_commute' erott@37872: ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))" erott@37872: ### trying thm 'radd_assoc' erott@37872: ### trying thm 'rmult_commute' erott@37872: ### not: "b * (c * d)" > "c * d * b" erott@37872: ### not: "c * d" > "d * c" erott@37872: ### trying thm 'rmult_left_commute' erott@37872: ### not: "b * (c * d)" > "c * (b * d)" erott@37872: ### trying thm 'rmult_assoc' erott@37872: ### trying thm 'radd_commute' erott@37872: ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a" erott@37872: ### not: "e + b * (c * d)" > "b * (c * d) + e" erott@37872: ### trying thm 'radd_left_commute' erott@37872: ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))" erott@37872: ### trying thm 'radd_assoc' erott@37872: ### trying thm 'rmult_commute' erott@37872: ### not: "b * (c * d)" > "c * d * b" erott@37872: ### not: "c * d" > "d * c" erott@37872: ### trying thm 'rmult_left_commute' erott@37872: ### not: "b * (c * d)" > "c * (b * d)" erott@37872: ### trying thm 'rmult_assoc' erott@37872: val it = Some ("a + (e + b * (c * d))",[]) : (string * string list) option \end{verbatim}}%size erott@37872: Notice that {\tt +} is left-associative where the parentheses are omitted for {\tt (a + b) + c = a + b + c}, but not for {\tt a + (b + c)}. Ordered rewriting necessarily terminates with parentheses which could be omitted due to associativity. erott@37872: erott@37872: erott@37872: \chapter{The hierarchy of problem types}\label{pbt} erott@37872: \section{The standard-function for 'matching'} erott@37872: Matching \cite{nipk:rew-all-that} is a technique used within rewriting, and used by \isac{} also for (a generalized) 'matching' a problem with a problem type. The function which tests for matching has the following signature: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> matches; erott@37872: val it = fn : theory -> term -> term -> bool erott@37872: \end{verbatim}}%size erott@37872: where the first of the two {\tt term} arguments is the particular term to be tested, and the second one is the pattern: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val t = (term_of o the o (parse thy)) "#3 * x^^^#2 = #1"; erott@37872: val t = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#1","RealDef.real") : term erott@37872: ML> erott@37872: ML> val p = (term_of o the o (parse thy)) "a * b^^^#2 = c"; erott@37872: val p = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("c","RealDef.real") : term erott@37872: ML> atomt p; erott@37872: *** ------------- erott@37872: *** Const ( op =) erott@37872: *** . Const ( op *) erott@37872: *** . . Free ( a, ) erott@37872: *** . . Const ( RatArith.pow) erott@37872: *** . . . Free ( b, ) erott@37872: *** . . . Free ( #2, ) erott@37872: *** . Free ( c, ) erott@37872: val it = () : unit erott@37872: ML> Walther@60650: ML> mk_Var; erott@37872: val it = fn : term -> term erott@37872: ML> Walther@60650: ML> val pat = mk_Var p; erott@37872: val pat = Const (#,#) $ (# $ # $ (# $ #)) $ Var ((#,#),"RealDef.real") : term erott@37872: ML> Sign.string_of_term (sign_of thy) pat; erott@37872: val it = "?a * ?b ^^^ #2 = ?c" : cterm' erott@37872: ML> atomt pat; erott@37872: *** ------------- erott@37872: *** Const ( op =) erott@37872: *** . Const ( op *) erott@37872: *** . . Var ((a, 0), ) erott@37872: *** . . Const ( RatArith.pow) erott@37872: *** . . . Var ((b, 0), ) erott@37872: *** . . . Free ( #2, ) erott@37872: *** . Var ((c, 0), ) erott@37872: val it = () : unit erott@37872: \end{verbatim}}%size % $ Walther@60650: Note that the pattern {\tt pat} contains so-called {\it scheme variables} decorated with a {\tt ?} (analoguous to theorems). The pattern is generated by the function {\tt mk_Var}. This format of the pattern is necessary in order to obtain results like these: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> matches thy t pat; erott@37872: val it = true : bool erott@37872: ML> erott@37872: ML> val t2 = (term_of o the o (parse thy)) "x^^^#2 = #1"; erott@37872: val t2 = Const (#,#) $ (# $ # $ Free #) $ Free ("#1","RealDef.real") : term erott@37872: ML> matches thy t2 pat; erott@37872: val it = false : bool erott@37872: ML> erott@37872: ML> val pat2 = (term_of o the o (parse thy)) "?u^^^#2 = ?v"; erott@37872: val pat2 = Const (#,#) $ (# $ # $ Free #) $ Var ((#,#),"RealDef.real") : term erott@37872: ML> matches thy t2 pat2; erott@37872: val it = true : bool erott@37872: \end{verbatim}}%size % $ erott@37872: erott@37872: \section{Accessing the hierarchy} erott@37872: The hierarchy of problem types is encapsulated; it can be accessed by the following functions. {\tt show\_ptyps} retrieves all leaves of the hierarchy (here in an early version for testing): erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> show_ptyps; erott@37872: val it = fn : unit -> unit erott@37872: ML> show_ptyps(); erott@37872: [ erott@37872: ["e_pblID"], erott@37872: ["equation", "univariate", "linear"], erott@37872: ["equation", "univariate", "plain_square"], erott@37872: ["equation", "univariate", "polynomial", "degree_two", "pq_formula"], erott@37872: ["equation", "univariate", "polynomial", "degree_two", "abc_formula"], erott@37872: ["equation", "univariate", "squareroot"], erott@37872: ["equation", "univariate", "normalize"], erott@37872: ["equation", "univariate", "sqroot-test"], erott@37872: ["function", "derivative_of"], erott@37872: ["function", "maximum_of", "on_interval"], erott@37872: ["function", "make"], erott@37872: ["tool", "find_values"], erott@37872: ["functional", "inssort"] erott@37872: ] erott@37872: val it = () : unit erott@37872: \end{verbatim}}%size erott@37872: The retrieve function for individual problem types is {\tt get\_pbt} erott@37872: \footnote{A function providing better readable output is in preparation}. Note that its argument, the 'problem identifier' {\tt pblID}, has the strings listed in reverse order w.r.t. the hierarchy, i.e. from the leave to the root. This order makes the {\tt pblID} closer to a natural description: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> get_pbt; erott@37872: val it = fn : pblID -> pbt erott@37872: ML> get_pbt ["squareroot", "univariate", "equation"]; erott@37872: val it = erott@37872: {met=[("SqRoot.thy","square_equation")], Walther@60586: model=[("#Given",(Const (#,#),Free (#,#))), erott@37872: ("#Given",(Const (#,#),Free (#,#))), erott@37872: ("#Given",(Const (#,#),Free (#,#))), erott@37872: ("#Find",(Const (#,#),Free (#,#)))], erott@37872: thy={ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun, erott@37872: Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat, erott@37872: Arith, Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype, erott@37872: Numeral, Bin, IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option, erott@37872: Map, Record, RelPow, Sexp, String, Calculation, SVC_Oracle, Main, erott@37872: Zorn, Filter, PNat, PRat, PReal, RealDef, RealOrd, RealInt, RealBin, erott@37872: HyperDef, Descript, ListG, Tools, Script, Typefix, Atools, RatArith, erott@37872: SqRoot}, erott@37872: where_=[Const ("SqRoot.contains'_root","bool => bool") $ erott@37872: Free ("e_","bool")]} : pbt erott@37872: \end{verbatim}}%size %$ erott@37872: where the records fields hold the following data: erott@37872: \begin{description} erott@37872: \item [\tt thy]: the theory necessary for parsing the formulas Walther@60586: \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}. erott@37872: \item [\tt met]: the list of methods solving this problem type.\\ erott@37872: \end{description} erott@37872: erott@37872: The following function adds or replaces a problem type (after having it prepared using {\tt prep\_pbt}) erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> store_pbt; erott@37872: val it = fn : pbt * pblID -> unit erott@37872: ML> store_pbt erott@37872: (prep_pbt SqRoot.thy erott@37872: (["newtype","univariate","equation"], erott@37872: [("#Given" ,["equality e_","solveFor v_","errorBound err_"]), erott@37872: ("#Where" ,["contains_root (e_::bool)"]), erott@37872: ("#Find" ,["solutions v_i_"]) erott@37872: ], erott@37872: [("SqRoot.thy","square_equation")])); erott@37872: val it = () : unit erott@37872: \end{verbatim}}%size erott@37872: When adding a new type with argument {\tt pblID}, an immediate parent must already exist in the hierarchy (this is the one with the tail of {\tt pblID}). erott@37872: erott@37872: \section{Internals of the datastructure} erott@37872: This subsection only serves for the implementation of the hierarchy browser and can be skipped by the authors of math knowledge. erott@37872: erott@37872: A problem type is described by the following record type (in the file {\tt [isac-src]/globals.sml}, the respective functions are in {\tt [isac-src]/ME/ptyps.sml}), and held in a global reference variable: erott@37872: {\footnotesize\begin{verbatim} erott@37872: type pbt = erott@37872: {thy : theory, (* the nearest to the root, erott@37872: which allows to compile that pbt *) erott@37872: where_: term list, (* where - predicates *) Walther@60586: model : ((string * (* fields "#Given","#Find" *) erott@37872: (term * (* description *) erott@37872: term)) (* id *) erott@37872: list), erott@37872: met : metID list}; (* methods solving the pbt *) erott@37872: datatype ptyp = erott@37872: Ptyp of string * (* key within pblID *) erott@37872: pbt list * (* several pbts with different domIDs*) erott@37872: ptyp list; erott@37872: val e_Ptyp = Ptyp ("empty",[],[]); erott@37872: erott@37872: type ptyps = ptyp list; erott@37872: val ptyps = ref ([e_Ptyp]:ptyps); erott@37872: \end{verbatim}}%size erott@37872: The predicates in {\tt where\_} (i.e. the preconditions) usually are defined in the respective theory in {\tt[isac-src]/knowledge}. Most of the predicates are not defined by rewriting, but by SML-code contained in the respective {\tt *.ML} file. erott@37872: erott@37872: Each item is headed by a so-called description which provides some guidance for interactive input. The descriptions are defined in {\tt[isac-src]/Isa99/Descript.thy}. erott@37872: erott@37872: erott@37872: erott@37872: \section{Match a formalization with a problem type}\label{pbl} erott@37872: A formalization is {\it match}ed with a problem type which yields a problem. A formal description of this kind of {\it match}ing can be found in \\{\tt ftp://ft.ist.tugraz.at/projects/isac/publ/calculemus01.ps.gz}. A formalization of an equation is e.g. erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val fmz = ["equality (#1 + #2 * x = #0)", erott@37872: "solveFor x", erott@37872: "solutions L"] : fmz; erott@37872: val fmz = ["equality (#1 + #2 * x = #0)","solveFor x","solutions L"] : fmz erott@37872: \end{verbatim}}%size erott@37872: Given a formalization (and a specification of the problem, i.e. a theory, a problemtype, and a method) \isac{} can solve the respective problem automatically. The formalization must match the problem type for this purpose: erott@37872: {\footnotesize\begin{verbatim} Walther@60769: ML> by_formalise; erott@37872: val it = fn : fmz -> pbt -> match' erott@37872: ML> Walther@60769: ML> by_formalise fmz (get_pbt ["univariate","equation"]); erott@37872: val it = erott@37872: Matches' erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"], erott@37872: Relate=[],Where=[Correct "matches (?a = ?b) (#1 + #2 * x = #0)"],With=[]} erott@37872: : match' erott@37872: ML> Walther@60769: ML> by_formalise fmz (get_pbt ["linear","univariate","equation"]); erott@37872: val it = erott@37872: Matches' erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"], erott@37872: Relate=[], erott@37872: Where=[Correct erott@37872: "matches ( x = #0) (#1 + #2 * x = #0) | erott@37872: matches ( ?b * x = #0) (#1 + #2 * x = #0) | erott@37872: matches (?a + x = #0) (#1 + #2 * x = #0) | erott@37872: matches (?a + ?b * x = #0) (#1 + #2 * x = #0)"], erott@37872: With=[]} : match' erott@37872: ML> Walther@60769: ML> by_formalise fmz (get_pbt ["squareroot","univariate","equation"]); erott@37872: val it = erott@37872: NoMatch' erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x", erott@37872: Missing "errorBound err_"],Relate=[], erott@37872: Where=[False "contains_root #1 + #2 * x = #0 "],With=[]} : match' erott@37872: \end{verbatim}}%size erott@37872: The above formalization does not match the problem type \\{\tt["squareroot","univariate","equation"]} which is explained by the tags: erott@37872: \begin{tabbing} erott@37872: 123\=\kill erott@37872: \> {\tt Missing:} the item is missing in the formalization as required by the problem type\\ erott@37872: \> {\tt Superfl:} the item is not required by the problem type\\ erott@37872: \> {\tt Correct:} the item is correct, or the precondition ({\tt Where}) is true\\ erott@37872: \> {\tt False:} the precondition ({\tt Where}) is false\\ erott@37872: \> {\tt Incompl:} the item is incomlete, or not yet input.\\ erott@37872: \end{tabbing} erott@37872: erott@37872: erott@37872: erott@37872: \section{Refine a problem specification} erott@37872: The challenge in constructing the problem hierarchy is, to design the branches in such a way, that problem refinement can be done automatically (as it is done in algebra system e.g. by a internal hierarchy of equations). erott@37872: erott@37872: For this purpose the hierarchy must be built using the following rules: Let $F$ be a formalization and $P$ and $P_i,\:i=1\cdots n$ problem types, where the $P_i$ are specialized problem types w.r.t. $P$ (i.e. $P$ is a parent node of $P_i$), then erott@37872: {\small erott@37872: \begin{enumerate} erott@37872: \item for all $F$ matching some $P_i$ must follow, that $F$ matches $P$ erott@37872: \item an $F$ matching $P$ should not have more than {\em one} $P_i,\:i=1\cdots n-1$ with $F$ matching $P_i$ (if there are more than one $P_i$, the first one will be taken) erott@37872: \item for all $F$ matching some $P$ must follow, that $F$ matches $P_n$\\ erott@37872: \end{enumerate}}%small erott@37872: \noindent Let us give an example for the point (1.) and (2.) first: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> refine; erott@37872: val it = fn : fmz -> pblID -> match list erott@37872: ML> erott@37872: ML> val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", erott@37872: "solveFor x","errorBound (eps=#0)", erott@37872: "solutions L"]; erott@37872: ML> erott@37872: ML> refine fmz ["univariate","equation"]; erott@37872: *** pass ["equation","univariate"] erott@37872: *** pass ["equation","univariate","linear"] erott@37872: *** pass ["equation","univariate","plain_square"] erott@37872: *** pass ["equation","univariate","polynomial"] erott@37872: *** pass ["equation","univariate","squareroot"] erott@37872: val it = erott@37872: [Matches erott@37872: (["univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))", erott@37872: Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[], erott@37872: Where=[Correct erott@37872: "matches (?a = ?b) (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"], erott@37872: With=[]}), erott@37872: NoMatch erott@37872: (["linear","univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))", erott@37872: Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[], erott@37872: Where=[False "(?a + ?b * x = #0) (sqrt (#9 + #4 * x#"], erott@37872: With=[]}), erott@37872: NoMatch erott@37872: (["plain_square","univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))", erott@37872: Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[], erott@37872: Where=[False erott@37872: "matches (?a + ?b * x ^^^ #2 = #0)"], erott@37872: With=[]}), erott@37872: NoMatch erott@37872: (["polynomial","univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))", erott@37872: Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[], erott@37872: Where=[False erott@37872: "is_polynomial_in sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) x"], erott@37872: With=[]}), erott@37872: Matches erott@37872: (["squareroot","univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))", erott@37872: Correct "solveFor x",Correct "errorBound (eps = #0)"],Relate=[], erott@37872: Where=[Correct erott@37872: "contains_root sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) "], erott@37872: With=[]})] : match list erott@37872: \end{verbatim}}%size}%footnotesize\label{refine} erott@37872: This example shows, that in order to refine an {\tt["univariate","equation"]}, the formalization must match respective respective problem type (rule (1.)) and one of the descendants which should match selectively (rule (2.)). erott@37872: erott@37872: If no one of the descendants of {\tt["univariate","equation"]} match, rule (3.) comes into play: The {\em last} problem type on this level ($P_n$) provides for a special 'problem type' {\tt["normalize"]}. This node calls a method transforming the equation to a (or another) normal form, which then may match. Look at this example: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val fmz = ["equality (x+#1=#2)", erott@37872: "solveFor x","errorBound (eps=#0)", erott@37872: "solutions L"]; erott@37872: [...] erott@37872: ML> erott@37872: ML> refine fmz ["univariate","equation"]; erott@37872: *** pass ["equation","univariate"] erott@37872: *** pass ["equation","univariate","linear"] erott@37872: *** pass ["equation","univariate","plain_square"] erott@37872: *** pass ["equation","univariate","polynomial"] erott@37872: *** pass ["equation","univariate","squareroot"] erott@37872: *** pass ["equation","univariate","normalize"] erott@37872: val it = erott@37872: [Matches erott@37872: (["univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x", erott@37872: Superfl "errorBound (eps = #0)"],Relate=[], erott@37872: Where=[Correct "matches (?a = ?b) (x + #1 = #2)"],With=[]}), erott@37872: NoMatch erott@37872: (["linear","univariate","equation"], erott@37872: [...] erott@37872: With=[]}), erott@37872: NoMatch erott@37872: (["squareroot","univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x", erott@37872: Correct "errorBound (eps = #0)"],Relate=[], erott@37872: Where=[False "contains_root x + #1 = #2 "],With=[]}), erott@37872: Matches erott@37872: (["normalize","univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x", erott@37872: Superfl "errorBound (eps = #0)"],Relate=[],Where=[],With=[]})] erott@37872: : match list erott@37872: \end{verbatim}}%size erott@37872: The problem type $P_n$, {\tt["normalize","univariate","equation"]}, will transform the equation {\tt x + \#1 = \#2} to the normal form {\tt \#-1 + x = \#0}, which then will match {\tt["linear","univariate","equation"]}. erott@37872: erott@37872: This recursive search on the problem hierarchy can be done within a proof state. This leads to the next section. erott@37872: erott@37872: erott@37872: \chapter{Methods} erott@37872: A problem type can have one ore more methods solving a respective problem. A method is described by means of another new program language. The language itself looks like a simple functional language, but constructs an imperative proof-state behind the scenes (thus liberating the programer from dealing with technical details and also prohibiting incorrect construction of the proof tree). The interpreter of 'scripts' written in this language evaluates the scriptexpressions, and also delivers certain parts of the script itself for discussion with the user. erott@37872: erott@37872: \section{The scripts' syntax} erott@37872: The syntax of scripts follows the definition given in Backus-normal-form: erott@37872: {\it erott@37872: \begin{tabbing} erott@37872: 123\=123\=expr ::=\=$|\;\;$\=\kill erott@37872: \>script ::= {\tt Script} id arg$\,^*$ = body\\ erott@37872: \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\ erott@37872: \>\>body ::= expr\\ erott@37872: \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\ erott@37872: \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\ erott@37872: \>\>\>$|\;$\>listexpr\\ erott@37872: \>\>\>$|\;$\>id\\ erott@37872: \>\>\>$|\;$\>seqex id\\ erott@37872: \>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\ erott@37872: \>\>\>$|\;$\>{\tt Repeat} seqex\\ erott@37872: \>\>\>$|\;$\>{\tt Try} seqex\\ erott@37872: \>\>\>$|\;$\>seqex {\tt Or} seqex\\ erott@37872: \>\>\>$|\;$\>seqex {\tt @@} seqex\\ erott@37872: \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\ erott@37872: \>\>type ::= id\\ erott@37872: \>\>tac ::= id erott@37872: \end{tabbing}} erott@37872: where {\it id} is an identifier with the usual syntax, {\it prop} is a proposition constructed by Isabelles logical operators (see \cite{Isa-obj} {\tt [isabelle]/src/HOL/HOL.thy}), {\it listexpr} (called {\bf list-expression}) is constructed by Isabelles list functions like {\tt hd, tl, nth} described in {\tt [isabelle]/src/HOL/List.thy}, and {\it type} are (virtually) all types declared in Isabelles version 99. erott@37872: erott@37872: Expressions containing some of the keywords {\tt let}, {\tt if} etc. are called {\bf script-expressions}. erott@37872: erott@37872: Tactics {\it tac} are (curried) functions. For clarity and simplicity reasons, {\it listexpr} must not contain a {\it tac}, and {\it tac}s must not be nested, erott@37872: erott@37872: erott@37872: \section{Control the flow of evaluation} erott@37872: The flow of control is managed by the following script-expressions called {\it tacticals}. erott@37872: \begin{description} erott@37872: \item{{\tt while} prop {\tt Do} expr id} erott@37872: \item{{\tt if} prop {\tt then} expr {\tt else} expr} erott@37872: \end{description} erott@37872: While the the above script-expressions trigger the flow of control by evaluating the current formula, the other expressions depend on the applicability of the tactics within their respective subexpressions (which in turn depends on the proofstate) erott@37872: \begin{description} erott@37872: \item{{\tt Repeat} expr id} erott@37872: \item{{\tt Try} expr id} erott@37872: \item{expr {\tt Or} expr id} erott@37872: \item{expr {\tt @@} expr id} erott@37872: \end{description} erott@37872: erott@37872: \begin{description} erott@37872: \item xxx erott@37872: erott@37872: \end{description} erott@37872: erott@37872: \chapter{Do a calculational proof} erott@37872: First we list all the tactics available so far (this list may be extended during further development of \isac). erott@37872: erott@37872: \section{Tactics for doing steps in calculations} erott@37872: \input{tactics} erott@37872: erott@37872: \section{The functionality of the math engine} erott@37872: A proof is being started in the math engine {\tt me} by the tactic erott@37872: \footnote{In the present version a tactic is of type {\tt mstep}.} erott@37872: {\tt Init\_Proof}, and interactively promoted by other tactics. On input of each tactic the {\tt me} returns the resulting formula and the next tactic applicable. The proof is finished, when the {\tt me} proposes {\tt End\_Proof} as the next tactic. erott@37872: erott@37872: We show a calculation (calculational proof) concerning equation solving, where the type of equation is refined automatically: The equation is given by the respective formalization ... erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x", erott@37872: "errorBound (eps=#0)","solutions L"]; erott@37872: val fmz = erott@37872: ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)", erott@37872: "solutions L"] : string list erott@37872: ML> erott@37872: ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"], erott@37872: ("SqRoot.thy","no_met")); erott@37872: val dom = "SqRoot.thy" : string erott@37872: val pbt = ["univariate","equation"] : string list erott@37872: val met = ("SqRoot.thy","no_met") : string * string erott@37872: \end{verbatim}}%size erott@37872: ... and the specification {\tt spec} of a domain {\tt dom}, a problem type {\tt pbt} and a method {\tt met}. Note that the equation is such, that it is not immediatly clear, what type it is in particular (it could be a polynomial of degree 2; but, for sure, the type is some specialized type of a univariate equation). Thus, no method ({\tt no\_met}) can be specified for solving the problem. erott@37872: erott@37872: Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types. erott@37872: erott@37872: erott@37872: \section{Initialize the calculation} wneuper@59279: The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ctree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons. erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met))); erott@37872: val mID = "Init_Proof" : string erott@37872: val m = erott@37872: Init_Proof erott@37872: (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)", erott@37872: "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree; erott@37872: val p = ([],Pbl) : pos' erott@37872: val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout erott@37872: val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"]) erott@37872: : string * mstep erott@37872: val pt = erott@37872: Nd erott@37872: (PblObj erott@37872: {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, wneuper@59279: result=#,spec=#},[]) : ctree erott@37872: \end{verbatim}}%size wneuper@59279: The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ctree}, {\tt pos'}). erott@37872: erott@37872: We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> Compiler.Control.Print.printDepth:=8; (*4 default*) erott@37872: val it = () : unit erott@37872: ML> erott@37872: ML> f; erott@37872: val it = erott@37872: Form' erott@37872: (PpcKF erott@37872: (0,EdUndef,0,Nundef, erott@37872: (Problem [], erott@37872: {Find=[Incompl "solutions []"], erott@37872: Given=[Incompl "equality",Incompl "solveFor"],Relate=[], erott@37872: Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout erott@37872: \end{verbatim}}%size erott@37872: Recall, please, the format of a problem as presented in sect.\ref{pbl} on p.\pageref{pbl}; such an 'empty' problem can be found above encapsulated by several constructors containing additional data (necessary for the dialog guide, not relevant here).\\ erott@37872: erott@37872: {\it In the sequel we will omit output of the {\tt me} if it is not important for the respective context}.\\ erott@37872: erott@37872: In general, the dialog guide will hide the following two tactics {\tt Refine\_Tacitly} and {\tt Model\_Problem} from the user. erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> nxt; erott@37872: val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"]) erott@37872: : string * mstep erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"]) erott@37872: : string * mstep erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: \end{verbatim}}%size erott@37872: erott@37872: erott@37872: \section{The phase of modeling} erott@37872: comprises the input of the items of the problem; the {\tt me} can help by use of the formalization tacitly transferred by {\tt Init\_Proof}. In particular, the {\tt me} in general 'knows' the next promising tactic; the first one has been returned by the (hidden) tactic {\tt Model\_Problem}. erott@37872: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> nxt; erott@37872: val it = erott@37872: ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)") erott@37872: : string * mstep erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout erott@37872: \end{verbatim}}%size erott@37872: \noindent Now the problem is 'modeled', all items are input. We convince ourselves by increasing {\tt Compiler.Control.Print.printDepth} once more. erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> Compiler.Control.Print.printDepth:=8; erott@37872: ML> f; erott@37872: val it = erott@37872: Form' erott@37872: (PpcKF erott@37872: (0,EdUndef,0,Nundef, erott@37872: (Problem [], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", erott@37872: Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout erott@37872: \end{verbatim}}%size erott@37872: %One of the input items is considered {\tt Superfluous} by the {\tt me} consulting the problem type {\tt ["univariate","equation"]}. The {\tt ErrorBound}, however, could become important in case the equation only could be solved by some iteration method. erott@37872: erott@37872: \section{The phase of specification} erott@37872: This phase provides for explicit determination of the domain, the problem type, and the method to be used. In particular, the search for the appropriate problem type is being supported. There are two tactics for this purpose: {\tt Specify\_Problem} generates feedback on how a candidate of a problem type matches the current problem, and {\tt Refine\_Problem} provides help by the system, if the user gets lost. erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> nxt; erott@37872: val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val nxt = erott@37872: ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"]) erott@37872: : string * mstep erott@37872: val pt = erott@37872: Nd erott@37872: (PblObj erott@37872: {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, wneuper@59279: result=#,spec=#},[]) : ctree erott@37872: \end{verbatim}}%size erott@37872: The {\tt me} is smart enough to know the appropriate problem type (transferred tacitly with {\tt Init\_Proof}). In order to challenge the student, the dialog guide may hide this information; then the {\tt me} works as follows. erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val nxt = ("Specify_Problem", erott@37872: Specify_Problem ["polynomial","univariate","equation"]); erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout erott@37872: val nxt = erott@37872: ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"]) erott@37872: : string * mstep erott@37872: ML> erott@37872: ML> val nxt = ("Specify_Problem", erott@37872: Specify_Problem ["linear","univariate","equation"]); erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val f = erott@37872: Form' erott@37872: (PpcKF erott@37872: (0,EdUndef,0,Nundef, erott@37872: (Problem ["linear","univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", erott@37872: Correct "solveFor x"],Relate=[], erott@37872: Where=[False erott@37872: "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"], erott@37872: With=[]}))) : mout erott@37872: \end{verbatim}}%size erott@37872: Again assuming that the dialog guide hide the next tactic proposed by the {\tt me}, and the student gets lost, {\tt Refine\_Problem} always 'knows' the way out, if applied to the problem type {\tt["univariate","equation"]}. erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> val nxt = ("Refine_Problem", erott@37872: Refine_Problem ["linear","univariate","equation erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val f = Problems (RefinedKF [NoMatch #]) : mout erott@37872: ML> erott@37872: ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4; erott@37872: val f = erott@37872: Problems erott@37872: (RefinedKF erott@37872: [NoMatch erott@37872: (["linear","univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", erott@37872: Correct "solveFor x"],Relate=[], erott@37872: Where=[False erott@37872: "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"], erott@37872: With=[]})]) : mout erott@37872: ML> erott@37872: ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]); erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val f = erott@37872: Problems erott@37872: (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #]) erott@37872: : mout erott@37872: ML> erott@37872: ML> erott@37872: ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4; erott@37872: val f = erott@37872: Problems erott@37872: (RefinedKF erott@37872: [Matches erott@37872: (["univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", erott@37872: Correct "solveFor x"],Relate=[], erott@37872: Where=[Correct erott@37872: With=[]}), erott@37872: NoMatch erott@37872: (["linear","univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", erott@37872: Correct "solveFor x"],Relate=[], erott@37872: Where=[False erott@37872: "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"], erott@37872: With=[]}), erott@37872: NoMatch erott@37872: ... erott@37872: ... erott@37872: Matches erott@37872: (["normalize","univariate","equation"], erott@37872: {Find=[Correct "solutions L"], erott@37872: Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", erott@37872: Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout erott@37872: \end{verbatim}}%size erott@37872: The tactic {\tt Refine\_Problem} returns all matches to problem types along the path traced in the problem hierarchy (anlogously to the authoring tool for refinement in sect.\ref{refine} on p.\pageref{refine}) --- a lot of information to be displayed appropriately in the hiearchy browser~! erott@37872: erott@37872: \section{The phase of solving} erott@37872: This phase starts by invoking a method, which acchieves the normal form within two tactics, {\tt Rewrite rnorm\_equation\_add} and {\tt Rewrite\_Set SqRoot\_simplify}: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> nxt; erott@37872: val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation")) erott@37872: : string * mstep erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val f = erott@37872: Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8")) erott@37872: val nxt = erott@37872: ("Rewrite", Rewrite erott@37872: ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)")) erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val f = erott@37872: Form' (FormKF (~1,EdUndef,1,Nundef, erott@37872: "(x + #1) * (x + #2) + #-1 * (x ^^^ #2 + #8) = #0")) : mout erott@37872: val nxt = ("Rewrite_Set",Rewrite_Set "SqRoot_simplify") : string * mstep erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout erott@37872: val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep erott@37872: \end{verbatim}}%size erott@37872: Now the normal form {\tt \#-6 + \#3 * x = \#0} is the input to a subproblem, which again allows for specification of the type of equation, and the respective method: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> nxt; erott@37872: val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"])) erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val f = erott@37872: Form' (FormKF erott@37872: (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])")) erott@37872: : mout erott@37872: val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"]) erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]) erott@37872: \end{verbatim}}%size erott@37872: As required, the tactic {\tt Refine ["univariate","equation"]} selects the appropriate type of equation from the problem hierarchy, which can be seen by the tactic {\tt Model\_Problem ["linear","univariate","equation"]} prosed by the system. erott@37872: erott@37872: Again the whole phase of modeling and specification follows; we skip it here, and \isac's dialog guide may decide to do so as well. erott@37872: erott@37872: erott@37872: \section{The final phase: check the post-condition} erott@37872: The type of problems solved by \isac{} are so-called 'example construction problems' as shown above. The most characteristic point of such a problem is the post-condition. The handling of the post-condition in the given context is an open research question. erott@37872: erott@37872: Thus the post-condition is just mentioned, in our example for both, the problem and the subproblem: erott@37872: {\footnotesize\begin{verbatim} erott@37872: ML> nxt; erott@37872: val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"]) erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout erott@37872: val nxt = erott@37872: ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"]) erott@37872: ML> erott@37872: ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; erott@37872: val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout erott@37872: val nxt = ("End_Proof'",End_Proof') : string * mstep erott@37872: \end{verbatim}}%size erott@37872: The next tactic proposed by the system, {\tt End\_Proof'} indicates that the proof has finished successfully.\\ erott@37872: erott@37872: {\it The tactics proposed by the system need {\em not} be followed by the user; the user is free to choose other tactics, and the system will report, if this is applicable at the respective proof state, or not~! The reader may try out~!} erott@37872: erott@37872: erott@37872: erott@37872: \part{Systematic description} erott@37872: erott@37872: erott@37872: \chapter{The structure of the knowledge base} erott@37872: erott@37872: \section{Tactics and data} erott@37872: First we view the ME from outside, i.e. we regard tactics and relate them to the knowledge base (KB). W.r.t. the KB we address the atomic items which have to be implemented in detail by the authors of the KB erott@37872: \footnote{Some of these items are fetched by the tactics from intermediate storage within the ME, and not directly from the KB.} erott@37872: . The items are listed in alphabetical order in Tab.\ref{kb-items} on p.\pageref{kb-items}. erott@37872: {\begin{table}[h] erott@37872: \caption{Atomic items of the KB} \label{kb-items} erott@37872: %\tabcolsep=0.3mm erott@37872: \begin{center} erott@37872: \def\arraystretch{1.0} erott@37872: \begin{tabular}{lp{9.0cm}} erott@37872: abbrevation & description \\ erott@37872: \hline erott@37872: &\\ erott@37872: {\it calc\_list} erott@37872: & associationlist of the evaluation-functions {\it eval\_fn}\\ erott@37872: {\it eval\_fn} erott@37872: & evaluation-function for numerals and for predicates coded in SML\\ erott@37872: {\it eval\_rls } erott@37872: & ruleset {\it rls} for simplifying expressions with {\it eval\_fn}s\\ erott@37872: {\it fmz} erott@37872: & formalization, i.e. a minimal formula representation of an example \\ erott@37872: {\it met} Walther@60586: & a method, i.e. a datastructure holding all informations for the solving phase ({\it rew\_ord}, {\it program}, etc.)\\ erott@37872: {\it metID} erott@37872: & reference to a {\it met}\\ erott@37872: {\it op} erott@37872: & operator as key to an {\it eval\_fn} in a {\it calc\_list}\\ erott@37872: {\it pbl} erott@37872: & problem, i.e. a node in the problem-hierarchy\\ erott@37872: {\it pblID} erott@37872: & reference to a {\it pbl}\\ erott@37872: {\it rew\_ord} erott@37872: & rewrite-order\\ erott@37872: {\it rls} erott@37872: & ruleset, i.e. a datastructure holding theorems {\it thm} and operators {\it op} for simplification (with a {\it rew\_ord})\\ erott@37872: {\it Rrls} erott@37872: & ruleset for 'reverse rewriting' (an \isac-technique generating stepwise rewriting, e.g. for cancelling fractions)\\ Walther@60586: {\it program} erott@37872: & script describing algorithms by tactics, part of a {\it met} \\ erott@37872: {\it norm\_rls} erott@37872: & special ruleset calculating a normalform, associated with a {\it thy}\\ erott@37872: {\it spec} erott@37872: & specification, i.e. a tripel ({\it thyID, pblID, metID})\\ erott@37872: {\it subs} erott@37872: & substitution, i.e. a list of variable-value-pairs\\ erott@37872: {\it term} erott@37872: & Isabelle term, i.e. a formula\\ erott@37872: {\it thm} erott@37872: & theorem\\ erott@37872: {\it thy} erott@37872: & theory\\ erott@37872: {\it thyID} erott@37872: & reference to a {\it thy} \\ erott@37872: \end{tabular}\end{center}\end{table} erott@37872: } erott@37872: The relations between tactics and data items are shown in Tab.\ref{tac-kb}on p.\pageref{tac-kb}. erott@37872: {\def\arraystretch{1.2} erott@37872: \begin{table}[h] erott@37872: \caption{Which tactic uses which KB's item~?} \label{tac-kb} erott@37872: \tabcolsep=0.3mm erott@37872: \begin{center} erott@37872: \begin{tabular}{|ll||cccc|ccc|cccc|} \hline erott@37872: tactic &input & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\ Walther@60586: & &thy &program &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\ erott@37872: \hline\hline erott@37872: Init\_Proof erott@37872: &fmz & x & & & x & & & & & & & x \\ erott@37872: &spec & & & & & & & & & & & \\ erott@37872: \hline erott@37872: \multicolumn{13}{|l|}{model phase}\\ erott@37872: \hline erott@37872: Add\_* &term & x & & & x & & & & & & & x \\ erott@37872: FormFK &model & x & & & x & & & & & & & x \\ erott@37872: \hline erott@37872: \multicolumn{13}{|l|}{specify phase}\\ erott@37872: \hline erott@37872: Specify\_Theory erott@37872: &thyID & x & & & x & & & & x & x & & x \\ erott@37872: Specify\_Problem erott@37872: &pblID & x & & & x & & & & x & x & & x \\ erott@37872: Refine\_Problem erott@37872: &pblID & x & & & x & & & & x & x & & x \\ erott@37872: Specify\_Method erott@37872: &metID & x & & & x & & & & x & x & & x \\ erott@37872: Apply\_Method erott@37872: &metID & x & x & & x & & & & x & x & & x \\ erott@37872: \hline erott@37872: \multicolumn{13}{|l|}{solve phase}\\ erott@37872: \hline erott@37872: Rewrite,\_Inst erott@37872: &thm & x & x & & & x &met & & x &met & & \\ erott@37872: Rewrite, Detail erott@37872: &thm & x & x & & & x &rls & & x &rls & & \\ erott@37872: Rewrite, Detail erott@37872: &thm & x & x & & & x &Rrls & & x &Rrls & & \\ erott@37872: Rewrite\_Set,\_Inst erott@37872: &rls & x & x & & & & & x & x & x & & \\ erott@37872: Calculate erott@37872: &op & x & x & & & & & & & & x & \\ erott@37872: Substitute erott@37872: &subs & x & & & x & & & & & & & \\ erott@37872: & & & & & & & & & & & & \\ erott@37872: SubProblem erott@37872: &spec & x & x & & x & & & & x & x & & x \\ erott@37872: &fmz & & & & & & & & & & & \\ erott@37872: \hline erott@37872: \end{tabular}\end{center}\end{table} erott@37872: } erott@37872: erott@37872: \section{\isac's theories} erott@37872: \isac's theories build upon Isabelles theories for high-order-logic (HOL) up to the respective development of real numbers ({\tt HOL/Real}). Theories have a special format defined in \cite{Isa-ref} and the suffix {\tt *.thy}; usually theories are paired with SML-files having the same filename and the suffix {\tt *.ML}. erott@37872: erott@37872: \isac's theories represent the deductive part of \isac's knowledge base, the hierarchy of theories is structured accordingly. The {\tt *.ML}-files, however, contain {\em all} data of the other two axes of the knowledge base, the problems and the methods (without presenting their respective structure, which is done by the problem browser and the method browser, see \ref{pbt}). erott@37872: erott@37872: Tab.\ref{theories} on p.\pageref{theories} lists the basic theories planned to be implemented in version \isac.1. We expext the list to be expanded in the near future, actually, have a look to the theory browser~! erott@37872: erott@37872: The first three theories in the list do {\em not} belong to \isac's knowledge base; they are concerned with \isac's script-language for methods and listed here for completeness. erott@37872: {\begin{table}[h] erott@37872: \caption{Theories in \isac-version I} \label{theories} erott@37872: %\tabcolsep=0.3mm erott@37872: \begin{center} erott@37872: \def\arraystretch{1.0} erott@37872: \begin{tabular}{lp{9.0cm}} erott@37872: theory & description \\ erott@37872: \hline erott@37872: &\\ erott@37872: ListI.thy erott@37872: & assigns identifiers to the functions defined in {\tt Isabelle2002/src/HOL/List.thy} and (intermediatly~?) defines some more list functions\\ erott@37872: ListI.ML erott@37872: & {\tt eval\_fn} for the additional list functions\\ erott@37872: Tools.thy erott@37872: & functions required for the evaluation of scripts\\ erott@37872: Tools.ML erott@37872: & the respective {\tt eval\_fn}s\\ erott@37872: Script.thy erott@37872: & prerequisites for scripts: types, tactics, tacticals,\\ erott@37872: Script.ML erott@37872: & sets of tactics and functions for internal use\\ erott@37872: & \\ erott@37872: \hline erott@37872: & \\ erott@37872: Typefix.thy erott@37872: & an intermediate hack for escaping type errors\\ erott@37872: Descript.thy erott@37872: & {\it description}s for the formulas in {\it model}s and {\it problem}s\\ erott@37872: Atools erott@37872: & (re-)definition of operators; general predicates and functions for preconditions; theorems for the {\tt eval\_rls}\\ erott@37872: Float erott@37872: & floating point numerals\\ erott@37872: Equation erott@37872: & basic notions for equations and equational systems\\ erott@37872: Poly erott@37872: & polynomials\\ erott@37872: PolyEq erott@37872: & polynomial equations and equational systems \\ erott@37872: Rational.thy erott@37872: & additional theorems for rationals\\ erott@37872: Rational.ML erott@37872: & cancel, add and simplify rationals using (a generalization of) Euclids algorithm; respective reverse rulesets\\ erott@37872: RatEq erott@37872: & equations on rationals\\ erott@37872: Root erott@37872: & radicals; calculate normalform; respective reverse rulesets\\ erott@37872: RootEq erott@37872: & equations on roots\\ erott@37872: RatRootEq erott@37872: & equations on rationals and roots (i.e. on terms containing both operations)\\ erott@37872: Vect erott@37872: & vector analysis\\ erott@37872: Trig erott@37872: & trigonometriy\\ erott@37872: LogExp erott@37872: & logarithms and exponential functions\\ erott@37872: Calculus erott@37872: & nonstandard analysis\\ erott@37872: Diff erott@37872: & differentiation\\ erott@37872: DiffApp erott@37872: & applications of differentiaten (maxima-minima-problems)\\ erott@37872: Test erott@37872: & (old) data for the test suite\\ erott@37872: Isac erott@37872: & collects all \isac-theoris.\\ erott@37872: \end{tabular}\end{center}\end{table} erott@37872: } erott@37872: erott@37872: erott@37872: \section{Data in {\tt *.thy}- and {\tt *.ML}-files} erott@37872: As already mentioned, theories come in pairs of {\tt *.thy}- and {\tt *.ML}-files with the same respective filename. How data are distributed between the two files is shown in Tab.\ref{thy-ML} on p.\pageref{thy-ML}. erott@37872: {\begin{table}[h] erott@37872: \caption{Data in {\tt *.thy}- and {\tt *.ML}-files} \label{thy-ML} erott@37872: \tabcolsep=2.0mm erott@37872: \begin{center} erott@37872: \def\arraystretch{1.0} erott@37872: \begin{tabular}{llp{7.7cm}} erott@37872: file & data & description \\ erott@37872: \hline erott@37872: & &\\ erott@37872: {\tt *.thy} erott@37872: & consts erott@37872: & operators, predicates, functions, script-names ('{\tt Script} name \dots{\tt arguments}') erott@37872: \\ erott@37872: & rules erott@37872: & theorems: \isac{} uses Isabelles theorems if possible; additional theorems analoguous to such existing in Isabelle get the Isabelle-identifier attached an {\it I} erott@37872: \\& &\\ erott@37872: {\tt *.ML} erott@37872: & {\tt theory' :=} erott@37872: & the theory defined by the actual {\tt *.thy}-file is made accessible to \isac erott@37872: \\ erott@37872: & {\tt eval\_fn} erott@37872: & evaluation function for operators and predicates, coded on the meta-level (SML); the identifier of such a function is a combination of the keyword {\tt eval\_} with the identifier of the function as defined in {\tt *.thy} erott@37872: \\ erott@37872: & {\tt *\_simplify} erott@37872: & the canonical simplifier for the actual theory, i.e. the identifier for this ruleset is a combination of the theories identifier and the keyword {\tt *\_simplify} erott@37872: \\ erott@37872: & {\tt norm\_rls :=} erott@37872: & the canonical simplifier {\tt *\_simplify} is stored such that it is accessible for \isac erott@37872: \\ erott@37872: & {\tt rew\_ord' :=} erott@37872: & the same for rewrite orders, if needed outside of one particular ruleset erott@37872: \\ erott@37872: & {\tt ruleset' :=} erott@37872: & the same for rulesets (ordinary rulesets, reverse rulesets and {\tt eval\_rls}) erott@37872: \\ erott@37872: & {\tt calc\_list :=} erott@37872: & the same for {\tt eval\_fn}s, if needed outside of one particular ruleset (e.g. for a tactic {\tt Calculate} in a script) erott@37872: \\ erott@37872: & {\tt store\_pbl} erott@37872: & problems defined within this {\tt *.ML}-file are made accessible for \isac erott@37872: \\ erott@37872: & {\tt methods :=} erott@37872: & methods defined within this {\tt *.ML}-file are made accessible for \isac erott@37872: \\ erott@37872: \end{tabular}\end{center}\end{table} erott@37872: } erott@37872: The order of the data-items within the theories should adhere to the order given in this list. erott@37872: erott@37872: \section{Formal description of the problem-hierarchy} erott@37872: %for Richard Lang erott@37872: erott@37872: \section{Script tactics} erott@37872: The tactics actually promote the calculation: they construct the prooftree behind the scenes, and they are the points during evaluation where the script-interpreter transfers control to the user. Here we only describe the sytax of the tactics; the semantics is described on p.\pageref{user-tactics} below in context with the tactics the student uses ('user-tactics'): there is a 1-to-1 correspondence between user-tactics and script-tactics. erott@37872: erott@37872: erott@37872: erott@37872: erott@37872: erott@37872: \part{Authoring on the knowledge} erott@37872: erott@37872: erott@37872: \section{Add a theorem} erott@37872: \section{Define and add a problem} erott@37872: \section{Define and add a predicate} erott@37872: \section{Define and add a method} erott@37872: \section{} erott@37872: \section{} erott@37872: \section{} erott@37872: \section{} erott@37872: erott@37872: erott@37872: erott@37872: \newpage erott@37872: \bibliography{bib/isac,bib/from-theses} erott@37872: erott@37872: \end{document}