author | lcp |

Tue Nov 09 16:47:38 1993 +0100 (1993-11-09) | |

changeset 103 | 30bd42401ab2 |

parent 102 | e04cb6295a3f |

child 104 | d8205bb279a7 |

Initial revision

1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/doc-src/CHANGES-93.txt Tue Nov 09 16:47:38 1993 +0100 1.3 @@ -0,0 +1,90 @@ 1.4 +**** Isabelle-93 : a faster version of Isabelle-92 **** 1.5 + 1.6 +Isabelle now runs faster through a combination of improvements: pattern 1.7 +unification, discrimination nets and removal of assumptions during 1.8 +simplification. A new simplifier, although less flexible than the old one, 1.9 +runs many times faster for large subgoals. Classical reasoning 1.10 +(e.g. fast_tac) runs up to 30% faster when large numbers of rules are 1.11 +involved. Incompatibilities are few, and mostly concern the simplifier. 1.12 + 1.13 +THE SPEEDUPS 1.14 + 1.15 +The new simplifier is described in the Reference Manual, Chapter 8. See 1.16 +below for advice on converting. 1.17 + 1.18 +Pattern unification is completely invisible to users. It efficiently 1.19 +handles a common case of higher-order unification. 1.20 + 1.21 +Discrimination nets replace the old stringtrees. They provide fast lookup 1.22 +in a large set of rules for matching or unification. New "net" tactics 1.23 +replace the "compat_..." tactics based on stringtrees. Tactics 1.24 +biresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac and 1.25 +match_from_net_tac take a net, rather than a list of rules, and perform 1.26 +resolution or matching. Tactics net_biresolve_tac, net_bimatch_tac 1.27 +net_resolve_tac and net_match_tac take a list of rules, build a net 1.28 +(internally) and perform resolution or matching. 1.29 + 1.30 +The tactical METAHYPS, which allows a subgoal's hypotheses to be taken as a 1.31 +list of theorems, has been extended to handle unknowns (although not type 1.32 +unknowns). The simplification tactics now use METAHYPS to economise on 1.33 +storage consumption, and to avoid problems involving "parameters" bound in 1.34 +a subgoal. The modified simplifier now requires the auto_tac to take an 1.35 +extra argument: a list of theorems, which represents the assumptions of the 1.36 +current subgoal. 1.37 + 1.38 +OTHER CHANGES 1.39 + 1.40 +Apart from minor improvements in Pure Isabelle, the main other changes are 1.41 +extensions to object-logics. HOL now contains a treatment of co-induction 1.42 +and co-recursion, while ZF contains a formalization of equivalence classes, 1.43 +the integers and binary arithmetic. None of this material is documented. 1.44 + 1.45 + 1.46 +CONVERTING FROM THE OLD TO THE NEW SIMPLIFIER (for FOL/ZF/LCF/HOL) 1.47 + 1.48 +1. Run a crude shell script to convert your ML-files: 1.49 + 1.50 + change_simp *ML 1.51 + 1.52 +2. Most congruence rules are no longer needed. Hence you should remove all 1.53 +calls to mk_congs and mk_typed_congs (they no longer exist) and most 1.54 +occurrences of addcongs. The only exception are congruence rules for special 1.55 +constants like (in FOL) 1.56 + 1.57 +[| ?P <-> ?P'; ?P' ==> ?Q <-> ?Q' |] ==> ?P --> ?Q = ?P' --> ?Q' 1.58 +and 1.59 +[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> 1.60 +(ALL x:A. P(x)) <-> (ALL x:A'. P'(x)) 1.61 + 1.62 +where some of the arguments are simplified under additional premises. Most 1.63 +likely you don't have any constructs like that, or they are already included 1.64 +in the basic simpset. 1.65 + 1.66 +3. In case you have used the addsplits facilities of the old simplifier: 1.67 +The case-splitting and simplification tactics have been separated. If you 1.68 +want to interleave case-splitting with simplification, you have do so 1.69 +explicitly by the following command: 1.70 + 1.71 +ss setloop (split_tac split_thms) 1.72 + 1.73 +where ss is a simpset and split_thms the list of case-splitting theorems. 1.74 +The shell script in step 1 tries to convert to from addsplits to setloop 1.75 +automatically. 1.76 + 1.77 +4. If you have used setauto, you have to change it to setsolver by hand. 1.78 +The solver is more delicate than the auto tactic used to be. For details see 1.79 +the full description of the new simplifier. One very slight incompatibility 1.80 +is the fact that the old auto tactic could sometimes see premises as part of 1.81 +the proof state, whereas now they are always passed explicit as arguments. 1.82 + 1.83 +5. It is quite likely that a few proofs require further hand massaging. 1.84 + 1.85 +Known incompatibilities: 1.86 +- Applying a rewrite rule cannot instantiate a subgoal. This rules out 1.87 +solving a premise of a conditional rewrite rule with extra unknowns by 1.88 +rewriting. Only the solver can instantiate. 1.89 + 1.90 +Known bugs: 1.91 +- The names of bound variables can be changed by the simplifier. 1.92 + 1.93 +

2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 2.2 +++ b/doc-src/Errata.txt Tue Nov 09 16:47:38 1993 +0100 2.3 @@ -0,0 +1,27 @@ 2.4 +ERRATA FOR ISABELLE MANUAL 2.5 + 2.6 +** THM : BASIC INFERENCE ** 2.7 + 2.8 +Pure/tactic/lift_inst_rule: now checks for distinct parameters (could also 2.9 +compare with free variable names, though). Variables in the insts are now 2.10 +lifted over all parameters; their index is also increased. Type vars in 2.11 +the lhs variables are also increased by maxidx+1; this is essential for HOL 2.12 +examples to work. 2.13 + 2.14 + 2.15 +** THEORY MATTERS (GENERAL) ** 2.16 + 2.17 +Definitions: users must ensure that the left-hand side is nothing 2.18 +more complex than a function application -- never using fancy syntax. E.g. 2.19 +never 2.20 +> ("the_def", "THE y. P(y) == Union({y . x:{0}, P(y)})" ), 2.21 +but 2.22 +< ("the_def", "The(P) == Union({y . x:{0}, P(y)})" ), 2.23 + 2.24 +Provers/classical, simp (new simplifier), tsimp (old simplifier), ind 2.25 + 2.26 +** SYSTEMS MATTERS ** 2.27 + 2.28 +explain make system? maketest 2.29 + 2.30 +expandshort

3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 3.2 +++ b/doc-src/MacroHints Tue Nov 09 16:47:38 1993 +0100 3.3 @@ -0,0 +1,142 @@ 3.4 + 3.5 +Hints 3.6 +===== 3.7 + 3.8 +This is an incomprehensive list of facts about the new version of the syntax 3.9 +module (the macro system). 3.10 + 3.11 + 3.12 +- Syntax of "translations" section is list of <xrule> where: (metachars: [ | ]) 3.13 + 3.14 + <xrule> ::= [(<id>)] <string> [ => | <= | == ] [(<id>)] <string> 3.15 + 3.16 + One such line specifies a parse rule (=>) or a print rule (<=) or both (==). 3.17 + The optional <id> before each <string> specifies the name of the syntactic 3.18 + category to be used for parsing the string; the default is logic. Note that 3.19 + this has no influence on the applicability of rules. 3.20 + 3.21 + Example: 3.22 + 3.23 + translations 3.24 + (prop) "x:X" == (prop) "|- x:X" 3.25 + "Lam x:A.B" == "Abs(A, %x.B)" 3.26 + "Pi x:A.B" => "Prod(A, %x.B)" 3.27 + 3.28 + All rules of a theory will be shown in their internal (ast * ast) form by 3.29 + Syntax.print_trans. 3.30 + 3.31 +- Caveat: rewrite rules know no "context" nor "semantics", e.g. something 3.32 + like "('a, Nil)Cons", "% Nil Cons. Cons(a, Nil)" or "Cons(a, [])" will be 3.33 + rewritten by the rules "[x]" <= "Cons(x, [])", "[]" <= "Nil"; (this is a 3.34 + general problem with macro systems); 3.35 + 3.36 +- syn_of: theory -> Syntax.syntax 3.37 + 3.38 +- Syntax.print_gram shows grammer of syntax 3.39 + 3.40 +- Syntax.print_trans shows translations of syntax 3.41 + 3.42 +- Syntax.print_syntax shows grammer and translations of syntax 3.43 + 3.44 +- Ast.stat_normalize := true enables output of statistics after normalizing; 3.45 + 3.46 +- Ast.trace_normalize := true enables verbose output while normalizing and 3.47 + statistics; 3.48 + 3.49 +- eta_contract := false disables eta contraction when printing terms; 3.50 + 3.51 +- asts: (see also Pure/Syntax/ast.ML *) 3.52 + 3.53 + (*Asts come in two flavours: 3.54 + - proper asts representing terms and types: Variables are treated like 3.55 + Constants; 3.56 + - patterns used as lhs and rhs in rules: Variables are placeholders for 3.57 + proper asts.*) 3.58 + 3.59 + datatype ast = 3.60 + Constant of string | (* "not", "_%", "fun" *) 3.61 + Variable of string | (* x, ?x, 'a, ?'a *) 3.62 + Appl of ast list; (* (f x y z), ("fun" 'a 'b) *) 3.63 + 3.64 + (*the list of subasts of an Appl node has to contain at least 2 elements, i.e. 3.65 + there are no empty asts or nullary applications; use mk_appl for convenience*) 3.66 + 3.67 +- ast output style: 3.68 + Constant a -> "a" 3.69 + Variable a -> a 3.70 + Appl [ast1, ..., astn] -> (ast1 ... astn) 3.71 + 3.72 +- sext: (see also Pure/Syntax/sextension.ML) 3.73 + 3.74 + (** datatype sext **) 3.75 + 3.76 + datatype xrule = 3.77 + op |-> of (string * string) * (string * string) | 3.78 + op <-| of (string * string) * (string * string) | 3.79 + op <-> of (string * string) * (string * string); 3.80 + 3.81 + datatype sext = 3.82 + Sext of { 3.83 + mixfix: mixfix list, 3.84 + parse_translation: (string * (term list -> term)) list, 3.85 + print_translation: (string * (term list -> term)) list} | 3.86 + NewSext of { 3.87 + mixfix: mixfix list, 3.88 + xrules: xrule list, 3.89 + parse_ast_translation: (string * (ast list -> ast)) list, 3.90 + parse_preproc: (ast -> ast) option, 3.91 + parse_postproc: (ast -> ast) option, 3.92 + parse_translation: (string * (term list -> term)) list, 3.93 + print_translation: (string * (term list -> term)) list, 3.94 + print_preproc: (ast -> ast) option, 3.95 + print_postproc: (ast -> ast) option, 3.96 + print_ast_translation: (string * (ast list -> ast)) list}; 3.97 + 3.98 +- local (thy, ext) order of rules is preserved, global (merge) order is 3.99 + unspecified; 3.100 + 3.101 +- read asts contain a mixture of Constant and Variable atoms (some 3.102 + Variables become Const later); 3.103 + 3.104 +- *.thy-file/ML-section: all declarations will be exported, therefore 3.105 + one should use local-in-end constructs where appropriate; especially 3.106 + the examples in Logics/Defining could be better behaved; 3.107 + 3.108 +- [document the asts generated by the standard syntactic categories 3.109 + (idt, idts, args, ...)]; 3.110 + 3.111 +- print(_ast)_translation: the constant has to disappear or execption 3.112 + Match raised, otherwise the printer will not terminate; 3.113 + 3.114 +- binders are implemented traditionally, i.e. as parse/print_translations 3.115 + (compatibility, alpha, eta, HOL hack easy); 3.116 + 3.117 +- changes to the term/ast "parsetree" structure: renamed most constants 3.118 + (_args, _idts, ...), unified typ applications, _tapp/_tappl, type atoms 3.119 + no Const rather than Free; 3.120 + 3.121 +- misfeature: eta-contraction before rewriting therefore bounded quantifiers, 3.122 + Collect etc. may fall back to internal form; 3.123 + 3.124 +- changes and fixes to printing of types: 3.125 + 3.126 + "'a => 'b => 'c" now printed as "['a,'b] => 'c"; 3.127 + 3.128 + constraints now printed iff not dummyT and show_types enabled, changed 3.129 + internal print_translations accordingly; old translations that intruduce 3.130 + frees may cause printing of constraints at all occurences; 3.131 + 3.132 + constraints of bound vars now printed where bound (i.e. "%x::'a. x" rather 3.133 + than "%x. x::'a") and put in braces if necessary ("%(x::'a) y::'b. f(x,y)"); 3.134 + 3.135 + constraints of bound var printed even if a free var in another scope happens 3.136 + to have the same name and type; 3.137 + 3.138 +- [man: toplevel pretty printers for NJ]; 3.139 + 3.140 +- (syntactic constants "_..." (e.g. "_idts") are reserved, you may use "@..." 3.141 + or "*..." instead); 3.142 + 3.143 +- Printer: clash of fun/type constants with concrete syntax type/fun 3.144 + constants causes incorrect printing of of applications; 3.145 +

4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 4.2 +++ b/doc-src/ind-defs.tex Tue Nov 09 16:47:38 1993 +0100 4.3 @@ -0,0 +1,1585 @@ 4.4 +\documentstyle[11pt,a4,proof,lcp,alltt,amssymbols,draft]{article} 4.5 +\newif\ifCADE 4.6 +\CADEfalse 4.7 + 4.8 +\title{A Fixedpoint Approach to Implementing (Co-)Inductive Definitions\\ 4.9 + DRAFT\thanks{Research funded by the SERC (grants GR/G53279, 4.10 + GR/H40570) and by the ESPRIT Basic Research Action 6453 `Types'.}} 4.11 + 4.12 +\author{{\em Lawrence C. Paulson}\\ 4.13 + Computer Laboratory, University of Cambridge} 4.14 +\date{\today} 4.15 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} 4.16 + 4.17 +\def\picture #1 by #2 (#3){% pictures: width by height (name) 4.18 + \message{Picture #3} 4.19 + \vbox to #2{\hrule width #1 height 0pt depth 0pt 4.20 + \vfill \special{picture #3}}} 4.21 + 4.22 + 4.23 +\newcommand\sbs{\subseteq} 4.24 +\newcommand\List[1]{\lbrakk#1\rbrakk} 4.25 +\let\To=\Rightarrow 4.26 +\newcommand\Var[1]{{?\!#1}} 4.27 + 4.28 + 4.29 +%%%\newcommand\Pow{{\tt Pow}} 4.30 +\let\pow=\wp 4.31 +\newcommand\RepFun{{\tt RepFun}} 4.32 +\newcommand\pair[1]{\langle#1\rangle} 4.33 +\newcommand\cons{{\tt cons}} 4.34 +\def\succ{{\tt succ}} 4.35 +\newcommand\split{{\tt split}} 4.36 +\newcommand\fst{{\tt fst}} 4.37 +\newcommand\snd{{\tt snd}} 4.38 +\newcommand\converse{{\tt converse}} 4.39 +\newcommand\domain{{\tt domain}} 4.40 +\newcommand\range{{\tt range}} 4.41 +\newcommand\field{{\tt field}} 4.42 +\newcommand\bndmono{\hbox{\tt bnd\_mono}} 4.43 +\newcommand\lfp{{\tt lfp}} 4.44 +\newcommand\gfp{{\tt gfp}} 4.45 +\newcommand\id{{\tt id}} 4.46 +\newcommand\trans{{\tt trans}} 4.47 +\newcommand\wf{{\tt wf}} 4.48 +\newcommand\wfrec{\hbox{\tt wfrec}} 4.49 +\newcommand\nat{{\tt nat}} 4.50 +\newcommand\natcase{\hbox{\tt nat\_case}} 4.51 +\newcommand\transrec{{\tt transrec}} 4.52 +\newcommand\rank{{\tt rank}} 4.53 +\newcommand\univ{{\tt univ}} 4.54 +\newcommand\Vrec{{\tt Vrec}} 4.55 +\newcommand\Inl{{\tt Inl}} 4.56 +\newcommand\Inr{{\tt Inr}} 4.57 +\newcommand\case{{\tt case}} 4.58 +\newcommand\lst{{\tt list}} 4.59 +\newcommand\Nil{{\tt Nil}} 4.60 +\newcommand\Cons{{\tt Cons}} 4.61 +\newcommand\lstcase{\hbox{\tt list\_case}} 4.62 +\newcommand\lstrec{\hbox{\tt list\_rec}} 4.63 +\newcommand\length{{\tt length}} 4.64 +\newcommand\listn{{\tt listn}} 4.65 +\newcommand\acc{{\tt acc}} 4.66 +\newcommand\primrec{{\tt primrec}} 4.67 +\newcommand\SC{{\tt SC}} 4.68 +\newcommand\CONST{{\tt CONST}} 4.69 +\newcommand\PROJ{{\tt PROJ}} 4.70 +\newcommand\COMP{{\tt COMP}} 4.71 +\newcommand\PREC{{\tt PREC}} 4.72 + 4.73 +\newcommand\quniv{{\tt quniv}} 4.74 +\newcommand\llist{{\tt llist}} 4.75 +\newcommand\LNil{{\tt LNil}} 4.76 +\newcommand\LCons{{\tt LCons}} 4.77 +\newcommand\lconst{{\tt lconst}} 4.78 +\newcommand\lleq{{\tt lleq}} 4.79 +\newcommand\map{{\tt map}} 4.80 +\newcommand\term{{\tt term}} 4.81 +\newcommand\Apply{{\tt Apply}} 4.82 +\newcommand\termcase{{\tt term\_case}} 4.83 +\newcommand\rev{{\tt rev}} 4.84 +\newcommand\reflect{{\tt reflect}} 4.85 +\newcommand\tree{{\tt tree}} 4.86 +\newcommand\forest{{\tt forest}} 4.87 +\newcommand\Part{{\tt Part}} 4.88 +\newcommand\TF{{\tt tree\_forest}} 4.89 +\newcommand\Tcons{{\tt Tcons}} 4.90 +\newcommand\Fcons{{\tt Fcons}} 4.91 +\newcommand\Fnil{{\tt Fnil}} 4.92 +\newcommand\TFcase{\hbox{\tt TF\_case}} 4.93 +\newcommand\Fin{{\tt Fin}} 4.94 +\newcommand\QInl{{\tt QInl}} 4.95 +\newcommand\QInr{{\tt QInr}} 4.96 +\newcommand\qsplit{{\tt qsplit}} 4.97 +\newcommand\qcase{{\tt qcase}} 4.98 +\newcommand\Con{{\tt Con}} 4.99 +\newcommand\data{{\tt data}} 4.100 + 4.101 +\sloppy 4.102 +\binperiod %%%treat . like a binary operator 4.103 + 4.104 +\begin{document} 4.105 +\pagestyle{empty} 4.106 +\begin{titlepage} 4.107 +\maketitle 4.108 +\begin{abstract} 4.109 + Several theorem provers provide commands for formalizing recursive 4.110 + datatypes and/or inductively defined sets. This paper presents a new 4.111 + approach, based on fixedpoint definitions. It is unusually general: 4.112 + it admits all monotone inductive definitions. It is conceptually simple, 4.113 + which has allowed the easy implementation of mutual recursion and other 4.114 + conveniences. It also handles co-inductive definitions: simply replace 4.115 + the least fixedpoint by a greatest fixedpoint. This represents the first 4.116 + automated support for co-inductive definitions. 4.117 + 4.118 + Examples include lists of $n$ elements, the accessible part of a relation 4.119 + and the set of primitive recursive functions. One example of a 4.120 + co-inductive definition is bisimulations for lazy lists. \ifCADE\else 4.121 + Recursive datatypes are examined in detail, as well as one example of a 4.122 + ``co-datatype'': lazy lists. The appendices are simple user's manuals 4.123 + for this Isabelle/ZF package.\fi 4.124 + 4.125 + The method has been implemented in Isabelle's ZF set theory. It should 4.126 + be applicable to any logic in which the Knaster-Tarski Theorem can be 4.127 + proved. The paper briefly describes a method of formalizing 4.128 + non-well-founded data structures in standard ZF set theory. 4.129 +\end{abstract} 4.130 +% 4.131 +\begin{center} Copyright \copyright{} \number\year{} by Lawrence C. Paulson 4.132 +\end{center} 4.133 +\thispagestyle{empty} 4.134 +\end{titlepage} 4.135 + 4.136 +\tableofcontents 4.137 +\cleardoublepage 4.138 +\pagenumbering{arabic}\pagestyle{headings}\DRAFT 4.139 + 4.140 +\section{Introduction} 4.141 +Several theorem provers provide commands for formalizing recursive data 4.142 +structures, like lists and trees. Examples include Boyer and Moore's shell 4.143 +principle~\cite{bm79} and Melham's recursive type package for the HOL 4.144 +system~\cite{melham89}. Such data structures are called {\bf datatypes} 4.145 +below, by analogy with {\tt datatype} definitions in Standard~ML\@. 4.146 + 4.147 +A datatype is but one example of a {\bf inductive definition}. This 4.148 +specifies the least set closed under given rules~\cite{aczel77}. The 4.149 +collection of theorems in a logic is inductively defined. A structural 4.150 +operational semantics~\cite{hennessy90} is an inductive definition of a 4.151 +reduction or evaluation relation on programs. A few theorem provers 4.152 +provide commands for formalizing inductive definitions; these include 4.153 +Coq~\cite{paulin92} and again the HOL system~\cite{camilleri92}. 4.154 + 4.155 +The dual notion is that of a {\bf co-inductive definition}. This specifies 4.156 +the greatest set closed under given rules. Important examples include 4.157 +using bisimulation relations to formalize equivalence of 4.158 +processes~\cite{milner89} or lazy functional programs~\cite{abramsky90}. 4.159 +Other examples include lazy lists and other infinite data structures; these 4.160 +are called {\bf co-datatypes} below. 4.161 + 4.162 +Most existing implementations of datatype and inductive definitions accept 4.163 +an artifically narrow class of inputs, and are not easily extended. The 4.164 +shell principle and Coq's inductive definition rules are built into the 4.165 +underlying logic. Melham's packages derive datatypes and inductive 4.166 +definitions from specialized constructions in higher-order logic. 4.167 + 4.168 +This paper describes a package based on a fixedpoint approach. Least 4.169 +fixedpoints yield inductive definitions; greatest fixedpoints yield 4.170 +co-inductive definitions. The package is uniquely powerful: 4.171 +\begin{itemize} 4.172 +\item It accepts the largest natural class of inductive definitions, namely 4.173 + all monotone inductive definitions. 4.174 +\item It accepts a wide class of datatype definitions. 4.175 +\item It handles co-inductive and co-datatype definitions. Most of 4.176 + the discussion below applies equally to inductive and co-inductive 4.177 + definitions, and most of the code is shared. To my knowledge, this is 4.178 + the only package supporting co-inductive definitions. 4.179 +\item Definitions may be mutually recursive. 4.180 +\end{itemize} 4.181 +The package is implemented in Isabelle~\cite{isabelle-intro}, using ZF set 4.182 +theory \cite{paulson-set-I,paulson-set-II}. However, the fixedpoint 4.183 +approach is independent of Isabelle. The recursion equations are specified 4.184 +as introduction rules for the mutually recursive sets. The package 4.185 +transforms these rules into a mapping over sets, and attempts to prove that 4.186 +the mapping is monotonic and well-typed. If successful, the package 4.187 +makes fixedpoint definitions and proves the introduction, elimination and 4.188 +(co-)induction rules. The package consists of several Standard ML 4.189 +functors~\cite{paulson91}; it accepts its argument and returns its result 4.190 +as ML structures. 4.191 + 4.192 +Most datatype packages equip the new datatype with some means of expressing 4.193 +recursive functions. This is the main thing lacking from my package. Its 4.194 +fixedpoint operators define recursive sets, not recursive functions. But 4.195 +the Isabelle/ZF theory provides well-founded recursion and other logical 4.196 +tools to simplify this task~\cite{paulson-set-II}. 4.197 + 4.198 +\S2 briefly introduces the least and greatest fixedpoint operators. \S3 4.199 +discusses the form of introduction rules, mutual recursion and other points 4.200 +common to inductive and co-inductive definitions. \S4 discusses induction 4.201 +and co-induction rules separately. \S5 presents several examples, 4.202 +including a co-inductive definition. \S6 describes datatype definitions, 4.203 +while \S7 draws brief conclusions. \ifCADE\else The appendices are simple 4.204 +user's manuals for this Isabelle/ZF package.\fi 4.205 + 4.206 +Most of the definitions and theorems shown below have been generated by the 4.207 +package. I have renamed some variables to improve readability. 4.208 + 4.209 +\section{Fixedpoint operators} 4.210 +In set theory, the least and greatest fixedpoint operators are defined as 4.211 +follows: 4.212 +\begin{eqnarray*} 4.213 + \lfp(D,h) & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\ 4.214 + \gfp(D,h) & \equiv & \union\{X\sbs D. X\sbs h(X)\} 4.215 +\end{eqnarray*} 4.216 +Say that $h$ is {\bf bounded by}~$D$ if $h(D)\sbs D$, and {\bf monotone} if 4.217 +$h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$. If $h$ is 4.218 +bounded by~$D$ and monotone then both operators yield fixedpoints: 4.219 +\begin{eqnarray*} 4.220 + \lfp(D,h) & = & h(\lfp(D,h)) \\ 4.221 + \gfp(D,h) & = & h(\gfp(D,h)) 4.222 +\end{eqnarray*} 4.223 +These equations are instances of the Knaster-Tarski theorem, which states 4.224 +that every monotonic function over a complete lattice has a 4.225 +fixedpoint~\cite{davey&priestley}. It is obvious from their definitions 4.226 +that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest. 4.227 + 4.228 +This fixedpoint theory is simple. The Knaster-Tarski theorem is easy to 4.229 +prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must 4.230 +also exhibit a bounding set~$D$ for~$h$. Sometimes this is trivial, as 4.231 +when a set of ``theorems'' is (co-)inductively defined over some previously 4.232 +existing set of ``formulae.'' But defining the bounding set for 4.233 +(co-)datatype definitions requires some effort; see~\S\ref{data-sec} below. 4.234 + 4.235 + 4.236 +\section{Elements of an inductive or co-inductive definition}\label{basic-sec} 4.237 +Consider a (co-)inductive definition of the sets $R_1$, \ldots,~$R_n$, in 4.238 +mutual recursion. They will be constructed from previously existing sets 4.239 +$D_1$, \ldots,~$D_n$, respectively, which are called their {\bf domains}. 4.240 +The construction yields not $R_i\sbs D_i$ but $R_i\sbs D_1+\cdots+D_n$, where 4.241 +$R_i$ is the image of~$D_i$ under an injection~\cite[\S4.5]{paulson-set-II}. 4.242 + 4.243 +The definition may involve arbitrary parameters $\vec{p}=p_1$, 4.244 +\ldots,~$p_k$. Each recursive set then has the form $R_i(\vec{p})$. The 4.245 +parameters must be identical every time they occur within a definition. This 4.246 +would appear to be a serious restriction compared with other systems such as 4.247 +Coq~\cite{paulin92}. For instance, we cannot define the lists of 4.248 +$n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$ 4.249 +varies. \S\ref{listn-sec} describes how to express this definition using the 4.250 +package. 4.251 + 4.252 +To avoid clutter below, the recursive sets are shown as simply $R_i$ 4.253 +instead of $R_i(\vec{p})$. 4.254 + 4.255 +\subsection{The form of the introduction rules}\label{intro-sec} 4.256 +The body of the definition consists of the desired introduction rules, 4.257 +specified as strings. The conclusion of each rule must have the form $t\in 4.258 +R_i$, where $t$ is any term. Premises typically have the same form, but 4.259 +they can have the more general form $t\in M(R_i)$ or express arbitrary 4.260 +side-conditions. 4.261 + 4.262 +The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on 4.263 +sets, satisfying the rule 4.264 +\[ \infer{M(A)\sbs M(B)}{A\sbs B} \] 4.265 +The inductive definition package must be supplied monotonicity rules for 4.266 +all such premises. 4.267 + 4.268 +Because any monotonic $M$ may appear in premises, the criteria for an 4.269 +acceptable definition is semantic rather than syntactic. A suitable choice 4.270 +of~$M$ and~$t$ can express a lot. The powerset operator $\pow$ is 4.271 +monotone, and the premise $t\in\pow(R)$ expresses $t\sbs R$; see 4.272 +\S\ref{acc-sec} for an example. The `list of' operator is monotone, and 4.273 +the premise $t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ 4.274 +using mutual recursion; see \S\ref{primrec-sec} and also my earlier 4.275 +paper~\cite[\S4.4]{paulson-set-II}. 4.276 + 4.277 +Introduction rules may also contain {\bf side-conditions}. These are 4.278 +premises consisting of arbitrary formulae not mentioning the recursive 4.279 +sets. Side-conditions typically involve type-checking. One example is the 4.280 +premise $a\in A$ in the following rule from the definition of lists: 4.281 +\[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \] 4.282 + 4.283 +\subsection{The fixedpoint definitions} 4.284 +The package translates the list of desired introduction rules into a fixedpoint 4.285 +definition. Consider, as a running example, the finite set operator 4.286 +$\Fin(A)$: the set of all finite subsets of~$A$. It can be 4.287 +defined as the least set closed under the rules 4.288 +\[ \emptyset\in\Fin(A) \qquad 4.289 + \infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)} 4.290 +\] 4.291 + 4.292 +The domain for a (co-)inductive definition must be some existing set closed 4.293 +under the rules. A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all 4.294 +subsets of~$A$. The package generates the definition 4.295 +\begin{eqnarray*} 4.296 + \Fin(A) & \equiv & \lfp(\pow(A), \; 4.297 + \begin{array}[t]{r@{\,}l} 4.298 + \lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\ 4.299 + &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in X)\}) 4.300 + \end{array} 4.301 +\end{eqnarray*} 4.302 +The contribution of each rule to the definition of $\Fin(A)$ should be 4.303 +obvious. A co-inductive definition is similar but uses $\gfp$ instead 4.304 +of~$\lfp$. 4.305 + 4.306 +The package must prove that the fixedpoint operator is applied to a 4.307 +monotonic function. If the introduction rules have the form described 4.308 +above, and if the package is supplied a monotonicity theorem for every 4.309 +$t\in M(R_i)$ premise, then this proof is trivial.\footnote{Due to the 4.310 + presence of logical connectives in the fixedpoint's body, the 4.311 + monotonicity proof requires some unusual rules. These state that the 4.312 + connectives $\conj$, $\disj$ and $\exists$ are monotonic with respect to 4.313 + the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and 4.314 + only if $\forall x.P(x)\imp Q(x)$.} 4.315 + 4.316 +The result structure returns the definitions of the recursive sets as a theorem 4.317 +list called {\tt defs}. It also returns, as the theorem {\tt unfold}, a 4.318 +fixedpoint equation such as 4.319 +\begin{eqnarray*} 4.320 + \Fin(A) & = & 4.321 + \begin{array}[t]{r@{\,}l} 4.322 + \{z\in\pow(A). & z=\emptyset \disj{} \\ 4.323 + &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\} 4.324 + \end{array} 4.325 +\end{eqnarray*} 4.326 +It also returns, as the theorem {\tt dom\_subset}, an inclusion such as 4.327 +$\Fin(A)\sbs\pow(A)$. 4.328 + 4.329 + 4.330 +\subsection{Mutual recursion} \label{mutual-sec} 4.331 +In a mutually recursive definition, the domain for the fixedoint construction 4.332 +is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$, 4.333 +\ldots,~$n$. The package uses the injections of the 4.334 +binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections 4.335 +$h_{1,n}$, \ldots, $h_{n,n}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$. 4.336 + 4.337 +As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/ZF defines the 4.338 +operator $\Part$ to support mutual recursion. The set $\Part(A,h)$ 4.339 +contains those elements of~$A$ having the form~$h(z)$: 4.340 +\begin{eqnarray*} 4.341 + \Part(A,h) & \equiv & \{x\in A. \exists z. x=h(z)\}. 4.342 +\end{eqnarray*} 4.343 +For mutually recursive sets $R_1$, \ldots,~$R_n$ with 4.344 +$n>1$, the package makes $n+1$ definitions. The first defines a set $R$ using 4.345 +a fixedpoint operator. The remaining $n$ definitions have the form 4.346 +\begin{eqnarray*} 4.347 + R_i & \equiv & \Part(R,h_{i,n}), \qquad i=1,\ldots, n. 4.348 +\end{eqnarray*} 4.349 +It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint. 4.350 + 4.351 + 4.352 +\subsection{Proving the introduction rules} 4.353 +The uesr supplies the package with the desired form of the introduction 4.354 +rules. Once it has derived the theorem {\tt unfold}, it attempts 4.355 +to prove the introduction rules. From the user's point of view, this is the 4.356 +trickiest stage; the proofs often fail. The task is to show that the domain 4.357 +$D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is 4.358 +closed under all the introduction rules. This essentially involves replacing 4.359 +each~$R_i$ by $D_1+\cdots+D_n$ in each of the introduction rules and 4.360 +attempting to prove the result. 4.361 + 4.362 +Consider the $\Fin(A)$ example. After substituting $\pow(A)$ for $\Fin(A)$ 4.363 +in the rules, the package must prove 4.364 +\[ \emptyset\in\pow(A) \qquad 4.365 + \infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)} 4.366 +\] 4.367 +Such proofs can be regarded as type-checking the definition. The user 4.368 +supplies the package with type-checking rules to apply. Usually these are 4.369 +general purpose rules from the ZF theory. They could however be rules 4.370 +specifically proved for a particular inductive definition; sometimes this is 4.371 +the easiest way to get the definition through! 4.372 + 4.373 +The package returns the introduction rules as the theorem list {\tt intrs}. 4.374 + 4.375 +\subsection{The elimination rule} 4.376 +The elimination rule, called {\tt elim}, is derived in a straightforward 4.377 +manner. Applying the rule performs a case analysis, with one case for each 4.378 +introduction rule. Continuing our example, the elimination rule for $\Fin(A)$ 4.379 +is 4.380 +\[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]} 4.381 + & \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} } 4.382 +\] 4.383 +The package also returns a function {\tt mk\_cases}, for generating simplified 4.384 +instances of the elimination rule. However, {\tt mk\_cases} only works for 4.385 +datatypes and for inductive definitions involving datatypes, such as an 4.386 +inductively defined relation between lists. It instantiates {\tt elim} 4.387 +with a user-supplied term, then simplifies the cases using the freeness of 4.388 +the underlying datatype. 4.389 + 4.390 + 4.391 +\section{Induction and co-induction rules} 4.392 +Here we must consider inductive and co-inductive definitions separately. 4.393 +For an inductive definition, the package returns an induction rule derived 4.394 +directly from the properties of least fixedpoints, as well as a modified 4.395 +rule for mutual recursion and inductively defined relations. For a 4.396 +co-inductive definition, the package returns a basic co-induction rule. 4.397 + 4.398 +\subsection{The basic induction rule}\label{basic-ind-sec} 4.399 +The basic rule, called simply {\tt induct}, is appropriate in most situations. 4.400 +For inductive definitions, it is strong rule induction~\cite{camilleri92}; for 4.401 +datatype definitions (see below), it is just structural induction. 4.402 + 4.403 +The induction rule for an inductively defined set~$R$ has the following form. 4.404 +The major premise is $x\in R$. There is a minor premise for each 4.405 +introduction rule: 4.406 +\begin{itemize} 4.407 +\item If the introduction rule concludes $t\in R_i$, then the minor premise 4.408 +is~$P(t)$. 4.409 + 4.410 +\item The minor premise's eigenvariables are precisely the introduction 4.411 +rule's free variables that are not parameters of~$R$ --- for instance, $A$ 4.412 +is not an eigenvariable in the $\Fin(A)$ rule below. 4.413 + 4.414 +\item If the introduction rule has a premise $t\in R_i$, then the minor 4.415 +premise discharges the assumption $t\in R_i$ and the induction 4.416 +hypothesis~$P(t)$. If the introduction rule has a premise $t\in M(R_i)$ 4.417 +then the minor premise discharges the single assumption 4.418 +\[ t\in M(\{z\in R_i. P(z)\}). \] 4.419 +Because $M$ is monotonic, this assumption implies $t\in M(R_i)$. The 4.420 +occurrence of $P$ gives the effect of an induction hypothesis, which may be 4.421 +exploited by appealing to properties of~$M$. 4.422 +\end{itemize} 4.423 +The rule for $\Fin(A)$ is 4.424 +\[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset) 4.425 + & \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} } 4.426 +\] 4.427 +Stronger induction rules often suggest themselves. In the case of 4.428 +$\Fin(A)$, the Isabelle/ZF theory proceeds to derive a rule whose third 4.429 +premise discharges the extra assumption $a\not\in b$. Most special induction 4.430 +rules must be proved manually, but the package proves a rule for mutual 4.431 +induction and inductive relations. 4.432 + 4.433 +\subsection{Mutual induction} 4.434 +The mutual induction rule is called {\tt 4.435 +mutual\_induct}. It differs from the basic rule in several respects: 4.436 +\begin{itemize} 4.437 +\item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$, 4.438 +\ldots,~$P_n$: one for each recursive set. 4.439 + 4.440 +\item There is no major premise such as $x\in R_i$. Instead, the conclusion 4.441 +refers to all the recursive sets: 4.442 +\[ (\forall z.z\in R_1\imp P_1(z))\conj\cdots\conj 4.443 + (\forall z.z\in R_n\imp P_n(z)) 4.444 +\] 4.445 +Proving the premises simultaneously establishes $P_i(z)$ for $z\in 4.446 +R_i$ and $i=1$, \ldots,~$n$. 4.447 + 4.448 +\item If the domain of some $R_i$ is the Cartesian product 4.449 +$A_1\times\cdots\times A_m$, then the corresponding predicate $P_i$ takes $m$ 4.450 +arguments and the corresponding conjunct of the conclusion is 4.451 +\[ (\forall z_1\ldots z_m.\pair{z_1,\ldots,z_m}\in R_i\imp P_i(z_1,\ldots,z_m)) 4.452 +\] 4.453 +\end{itemize} 4.454 +The last point above simplifies reasoning about inductively defined 4.455 +relations. It eliminates the need to express properties of $z_1$, 4.456 +\ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$. 4.457 + 4.458 +\subsection{Co-induction}\label{co-ind-sec} 4.459 +A co-inductive definition yields a primitive co-induction rule, with no 4.460 +refinements such as those for the induction rules. (Experience may suggest 4.461 +refinements later.) Consider the co-datatype of lazy lists as an example. For 4.462 +suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the 4.463 +greatest fixedpoint satisfying the rules 4.464 +\[ \LNil\in\llist(A) \qquad 4.465 + \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)} 4.466 +\] 4.467 +The $(-)$ tag stresses that this is a co-inductive definition. A suitable 4.468 +domain for $\llist(A)$ is $\quniv(A)$, a set closed under variant forms of 4.469 +sum and product for representing infinite data structures 4.470 +(\S\ref{data-sec}). Co-inductive definitions use these variant sums and 4.471 +products. 4.472 + 4.473 +The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$. 4.474 +Then it proves the theorem {\tt co\_induct}, which expresses that $\llist(A)$ 4.475 +is the greatest solution to this equation contained in $\quniv(A)$: 4.476 +\[ \infer{a\in\llist(A)}{a\in X & X\sbs \quniv(A) & 4.477 + \infer*{z=\LNil\disj \bigl(\exists a\,l.\, 4.478 + \begin{array}[t]{@{}l} 4.479 + z=\LCons(a,l) \conj a\in A \conj{}\\ 4.480 + l\in X\un\llist(A) \bigr) 4.481 + \end{array} }{[z\in X]_z}} 4.482 +\] 4.483 +Having $X\un\llist(A)$ instead of simply $X$ in the third premise above 4.484 +represents a slight strengthening of the greatest fixedpoint property. I 4.485 +discuss several forms of co-induction rules elsewhere~\cite{paulson-coind}. 4.486 + 4.487 + 4.488 +\section{Examples of inductive and co-inductive definitions}\label{ind-eg-sec} 4.489 +This section presents several examples: the finite set operator, 4.490 +lists of $n$ elements, bisimulations on lazy lists, the well-founded part 4.491 +of a relation, and the primitive recursive functions. 4.492 + 4.493 +\subsection{The finite set operator} 4.494 +The definition of finite sets has been discussed extensively above. Here 4.495 +is the corresponding ML invocation (note that $\cons(a,b)$ abbreviates 4.496 +$\{a\}\un b$ in Isabelle/ZF): 4.497 +\begin{ttbox} 4.498 +structure Fin = Inductive_Fun 4.499 + (val thy = Arith.thy addconsts [(["Fin"],"i=>i")]; 4.500 + val rec_doms = [("Fin","Pow(A)")]; 4.501 + val sintrs = 4.502 + ["0 : Fin(A)", 4.503 + "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"]; 4.504 + val monos = []; 4.505 + val con_defs = []; 4.506 + val type_intrs = [empty_subsetI, cons_subsetI, PowI] 4.507 + val type_elims = [make_elim PowD]); 4.508 +\end{ttbox} 4.509 +The parent theory is obtained from {\tt Arith.thy} by adding the unary 4.510 +function symbol~$\Fin$. Its domain is specified as $\pow(A)$, where $A$ is 4.511 +the parameter appearing in the introduction rules. For type-checking, the 4.512 +package supplies the introduction rules: 4.513 +\[ \emptyset\sbs A \qquad 4.514 + \infer{\{a\}\un B\sbs C}{a\in C & B\sbs C} 4.515 +\] 4.516 +A further introduction rule and an elimination rule express the two 4.517 +directions of the equivalence $A\in\pow(B)\bimp A\sbs B$. Type-checking 4.518 +involves mostly introduction rules. When the package returns, we can refer 4.519 +to the $\Fin(A)$ introduction rules as {\tt Fin.intrs}, the induction rule 4.520 +as {\tt Fin.induct}, and so forth. 4.521 + 4.522 +\subsection{Lists of $n$ elements}\label{listn-sec} 4.523 +This has become a standard example in the 4.524 +literature. Following Paulin-Mohring~\cite{paulin92}, we could attempt to 4.525 +define a new datatype $\listn(A,n)$, for lists of length~$n$, as an $n$-indexed 4.526 +family of sets. But her introduction rules 4.527 +\[ {\tt Niln}\in\listn(A,0) \qquad 4.528 + \infer{{\tt Consn}(n,a,l)\in\listn(A,\succ(n))} 4.529 + {n\in\nat & a\in A & l\in\listn(A,n)} 4.530 +\] 4.531 +are not acceptable to the inductive definition package: 4.532 +$\listn$ occurs with three different parameter lists in the definition. 4.533 + 4.534 +\begin{figure} 4.535 +\begin{small} 4.536 +\begin{verbatim} 4.537 +structure ListN = Inductive_Fun 4.538 + (val thy = ListFn.thy addconsts [(["listn"],"i=>i")]; 4.539 + val rec_doms = [("listn", "nat*list(A)")]; 4.540 + val sintrs = 4.541 + ["<0,Nil> : listn(A)", 4.542 + "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]; 4.543 + val monos = []; 4.544 + val con_defs = []; 4.545 + val type_intrs = nat_typechecks@List.intrs@[SigmaI] 4.546 + val type_elims = [SigmaE2]); 4.547 +\end{verbatim} 4.548 +\end{small} 4.549 +\hrule 4.550 +\caption{Defining lists of $n$ elements} \label{listn-fig} 4.551 +\end{figure} 4.552 + 4.553 +There is an obvious way of handling this particular example, which may suggest 4.554 +a general approach to varying parameters. Here, we can take advantage of an 4.555 +existing datatype definition of $\lst(A)$, with constructors $\Nil$ 4.556 +and~$\Cons$. Then incorporate the number~$n$ into the inductive set itself, 4.557 +defining $\listn(A)$ as a relation. It consists of pairs $\pair{n,l}$ such 4.558 +that $n\in\nat$ and~$l\in\lst(A)$ and $l$ has length~$n$. In fact, 4.559 +$\listn(A)$ turns out to be the converse of the length function on~$\lst(A)$. 4.560 +The Isabelle/ZF introduction rules are 4.561 +\[ \pair{0,\Nil}\in\listn(A) \qquad 4.562 + \infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)} 4.563 + {a\in A & \pair{n,l}\in\listn(A)} 4.564 +\] 4.565 +Figure~\ref{listn-fig} presents the ML invocation. A theory of lists, 4.566 +extended with a declaration of $\listn$, is the parent theory. The domain 4.567 +is specified as $\nat\times\lst(A)$. The type-checking rules include those 4.568 +for 0, $\succ$, $\Nil$ and $\Cons$. Because $\listn(A)$ is a set of pairs, 4.569 +type-checking also requires introduction and elimination rules to express 4.570 +both directions of the equivalence $\pair{a,b}\in A\times B \bimp a\in A 4.571 +\conj b\in B$. 4.572 + 4.573 +The package returns introduction, elimination and induction rules for 4.574 +$\listn$. The basic induction rule, {\tt ListN.induct}, is 4.575 +\[ \infer{P(x)}{x\in\listn(A) & P(\pair{0,\Nil}) & 4.576 + \infer*{P(\pair{\succ(n),\Cons(a,l)})} 4.577 + {[a\in A & \pair{n,l}\in\listn(A) & P(\pair{n,l})]_{a,l,n}}} 4.578 +\] 4.579 +This rule requires the induction formula to be a 4.580 +unary property of pairs,~$P(\pair{n,l})$. The alternative rule, {\tt 4.581 +ListN.mutual\_induct}, uses a binary property instead: 4.582 +\[ \infer{\forall n\,l. \pair{n,l}\in\listn(A) \imp P(\pair{n,l})} 4.583 + {P(0,\Nil) & 4.584 + \infer*{P(\succ(n),\Cons(a,l))} 4.585 + {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}} 4.586 +\] 4.587 +It is now a simple matter to prove theorems about $\listn(A)$, such as 4.588 +\[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \] 4.589 +\[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \] 4.590 +This latter result --- here $r``A$ denotes the image of $A$ under $r$ 4.591 +--- asserts that the inductive definition agrees with the obvious notion of 4.592 +$n$-element list. 4.593 + 4.594 +Unlike in Coq, the definition does not declare a new datatype. A `list of 4.595 +$n$ elements' really is a list, and is subject to list operators such 4.596 +as append. For example, a trivial induction yields 4.597 +\[ \infer{\pair{m\mathbin{+} m,\, l@l'}\in\listn(A)} 4.598 + {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} 4.599 +\] 4.600 +where $+$ here denotes addition on the natural numbers and @ denotes append. 4.601 + 4.602 +\ifCADE\typeout{****Omitting mk_cases from CADE version!} 4.603 +\else 4.604 +\subsection{A demonstration of {\tt mk\_cases}} 4.605 +The elimination rule, {\tt ListN.elim}, is cumbersome: 4.606 +\[ \infer{Q}{x\in\listn(A) & 4.607 + \infer*{Q}{[x = \pair{0,\Nil}]} & 4.608 + \infer*{Q} 4.609 + {\left[\begin{array}{l} 4.610 + x = \pair{\succ(n),\Cons(a,l)} \\ 4.611 + a\in A \\ 4.612 + \pair{n,l}\in\listn(A) 4.613 + \end{array} \right]_{a,l,n}}} 4.614 +\] 4.615 +The function {\tt ListN.mk\_cases} generates simplified instances of this 4.616 +rule. It works by freeness reasoning on the list constructors. 4.617 +If $x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt ListN.mk\_cases} 4.618 +deduces the corresponding form of~$i$. For example, 4.619 +\begin{ttbox} 4.620 +ListN.mk_cases List.con_defs "<i,Cons(a,l)> : listn(A)" 4.621 +\end{ttbox} 4.622 +yields the rule 4.623 +\[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & 4.624 + \infer*{Q} 4.625 + {\left[\begin{array}{l} 4.626 + i = \succ(n) \\ a\in A \\ \pair{n,l}\in\listn(A) 4.627 + \end{array} \right]_{n}}} 4.628 +\] 4.629 +The package also has built-in rules for freeness reasoning about $0$ 4.630 +and~$\succ$. So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt 4.631 +ListN.mk\_cases} can similarly deduce the corresponding form of~$l$. 4.632 + 4.633 +The function {\tt mk\_cases} is also useful with datatype definitions 4.634 +themselves. The version from the definition of lists, namely {\tt 4.635 +List.mk\_cases}, can prove the rule 4.636 +\[ \infer{Q}{\Cons(a,l)\in\lst(A) & 4.637 + & \infer*{Q}{[a\in A &l\in\lst(A)]} } 4.638 +\] 4.639 +The most important uses of {\tt mk\_cases} concern inductive definitions of 4.640 +evaluation relations. Then {\tt mk\_cases} supports the kind of backward 4.641 +inference typical of hand proofs, for example to prove that the evaluation 4.642 +relation is functional. 4.643 +\fi %CADE 4.644 + 4.645 +\subsection{A co-inductive definition: bisimulations on lazy lists} 4.646 +This example anticipates the definition of the co-datatype $\llist(A)$, which 4.647 +consists of lazy lists over~$A$. Its constructors are $\LNil$ and $\LCons$, 4.648 +satisfying the introduction rules shown in~\S\ref{co-ind-sec}. 4.649 +Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant 4.650 +pairing and injection operators, it contains non-well-founded elements such as 4.651 +solutions to $\LCons(a,l)=l$. 4.652 + 4.653 +The next step in the development of lazy lists is to define a co-induction 4.654 +principle for proving equalities. This is done by showing that the equality 4.655 +relation on lazy lists is the greatest fixedpoint of some monotonic 4.656 +operation. The usual approach~\cite{pitts94} is to define some notion of 4.657 +bisimulation for lazy lists, define equivalence to be the greatest 4.658 +bisimulation, and finally to prove that two lazy lists are equivalent if and 4.659 +only if they are equal. The co-induction rule for equivalence then yields a 4.660 +co-induction principle for equalities. 4.661 + 4.662 +A binary relation $R$ on lazy lists is a {\bf bisimulation} provided $R\sbs 4.663 +R^+$, where $R^+$ is the relation 4.664 +\[ \{\pair{\LNil;\LNil}\} \un 4.665 + \{\pair{\LCons(a,l);\LCons(a,l')} . a\in A \conj \pair{l;l'}\in R\}. 4.666 +\] 4.667 +Variant pairs are used, $\pair{l;l'}$ instead of $\pair{l,l'}$, because this 4.668 +is a co-inductive definition. 4.669 + 4.670 +A pair of lazy lists are {\bf equivalent} if they belong to some bisimulation. 4.671 +Equivalence can be co-inductively defined as the greatest fixedpoint for the 4.672 +introduction rules 4.673 +\[ \pair{\LNil;\LNil} \in\lleq(A) \qquad 4.674 + \infer[(-)]{\pair{\LCons(a,l);\LCons(a,l')} \in\lleq(A)} 4.675 + {a\in A & \pair{l;l'}\in \lleq(A)} 4.676 +\] 4.677 +To make this co-inductive definition, we invoke \verb|Co_Inductive_Fun|: 4.678 +\begin{ttbox} 4.679 +structure LList_Eq = Co_Inductive_Fun 4.680 +(val thy = LList.thy addconsts [(["lleq"],"i=>i")]; 4.681 + val rec_doms = [("lleq", "llist(A) <*> llist(A)")]; 4.682 + val sintrs = 4.683 + ["<LNil; LNil> : lleq(A)", 4.684 + "[| a:A; <l;l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')>: lleq(A)"]; 4.685 + val monos = []; 4.686 + val con_defs = []; 4.687 + val type_intrs = LList.intrs@[QSigmaI]; 4.688 + val type_elims = [QSigmaE2]); 4.689 +\end{ttbox} 4.690 +Again, {\tt addconsts} declares a constant for $\lleq$ in the parent theory. 4.691 +The domain of $\lleq(A)$ is $\llist(A)\otimes\llist(A)$, where $\otimes$ 4.692 +denotes the variant Cartesian product. The type-checking rules include the 4.693 +introduction rules for lazy lists as well as rules expressinve both 4.694 +definitions of the equivalence 4.695 +\[ \pair{a;b}\in A\otimes B \bimp a\in A \conj b\in B. \] 4.696 + 4.697 +The package returns the introduction rules and the elimination rule, as 4.698 +usual. But instead of induction rules, it returns a co-induction rule. 4.699 +The rule is too big to display in the usual notation; its conclusion is 4.700 +$a\in\lleq(A)$ and its premises are $a\in X$, $X\sbs \llist(A)\otimes\llist(A)$ 4.701 +and 4.702 +\[ \infer*{z=\pair{\LNil;\LNil}\disj \bigl(\exists a\,l\,l'.\, 4.703 + \begin{array}[t]{@{}l} 4.704 + z=\pair{\LCons(a,l);\LCons(a,l')} \conj a\in A \conj{}\\ 4.705 + \pair{l;l'}\in X\un\lleq(A) \bigr) 4.706 + \end{array} }{[z\in X]_z} 4.707 +\] 4.708 +Thus if $a\in X$, where $X$ is a bisimulation contained in the 4.709 +domain of $\lleq(A)$, then $a\in\lleq(A)$. It is easy to show that 4.710 +$\lleq(A)$ is reflexive: the equality relation is a bisimulation. And 4.711 +$\lleq(A)$ is symmetric: its converse is a bisimulation. But showing that 4.712 +$\lleq(A)$ coincides with the equality relation takes considerable work. 4.713 + 4.714 +\subsection{The accessible part of a relation}\label{acc-sec} 4.715 +Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$. 4.716 +The {\bf accessible} or {\bf well-founded} part of~$\prec$, written 4.717 +$\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits 4.718 +no infinite decreasing chains~\cite{aczel77}. Formally, $\acc(\prec)$ is 4.719 +inductively defined to be the least set that contains $a$ if it contains 4.720 +all $\prec$-predecessors of~$a$, for $a\in D$. Thus we need an 4.721 +introduction rule of the form 4.722 +%%%%\[ \infer{a\in\acc(\prec)}{\infer*{y\in\acc(\prec)}{[y\prec a]_y}} \] 4.723 +\[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \] 4.724 +Paulin-Mohring treats this example in Coq~\cite{paulin92}, but it causes 4.725 +difficulties for other systems. Its premise does not conform to 4.726 +the structure of introduction rules for HOL's inductive definition 4.727 +package~\cite{camilleri92}. It is also unacceptable to Isabelle package 4.728 +(\S\ref{intro-sec}), but fortunately can be transformed into one of the 4.729 +form $t\in M(R)$. 4.730 + 4.731 +The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to 4.732 +$t\sbs R$. This in turn is equivalent to $\forall y\in t. y\in R$. To 4.733 +express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a 4.734 +term~$t$ such that $y\in t$ if and only if $y\prec a$. A suitable $t$ is 4.735 +the inverse image of~$\{a\}$ under~$\prec$. 4.736 + 4.737 +The ML invocation below follows this approach. Here $r$ is~$\prec$ and 4.738 +$\field(r)$ refers to~$D$, the domain of $\acc(r)$. Finally $r^{-}``\{a\}$ 4.739 +denotes the inverse image of~$\{a\}$ under~$r$. The package is supplied 4.740 +the theorem {\tt Pow\_mono}, which asserts that $\pow$ is monotonic. 4.741 +\begin{ttbox} 4.742 +structure Acc = Inductive_Fun 4.743 + (val thy = WF.thy addconsts [(["acc"],"i=>i")]; 4.744 + val rec_doms = [("acc", "field(r)")]; 4.745 + val sintrs = 4.746 + ["[| r-``\{a\} : Pow(acc(r)); a : field(r) |] ==> a : acc(r)"]; 4.747 + val monos = [Pow_mono]; 4.748 + val con_defs = []; 4.749 + val type_intrs = []; 4.750 + val type_elims = []); 4.751 +\end{ttbox} 4.752 +The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For 4.753 +instance, $\prec$ is well-founded if and only if its field is contained in 4.754 +$\acc(\prec)$. 4.755 + 4.756 +As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$ 4.757 +gives rise to an unusual induction hypothesis. Let us examine the 4.758 +induction rule, {\tt Acc.induct}: 4.759 +\[ \infer{P(x)}{x\in\acc(r) & 4.760 + \infer*{P(a)}{[r^{-}``\{a\}\in\pow(\{z\in\acc(r).P(z)\}) & 4.761 + a\in\field(r)]_a}} 4.762 +\] 4.763 +The strange induction hypothesis is equivalent to 4.764 +$\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$. 4.765 +Therefore the rule expresses well-founded induction on the accessible part 4.766 +of~$\prec$. 4.767 + 4.768 +The use of inverse image is not essential. The Isabelle package can accept 4.769 +introduction rules with arbitrary premises of the form $\forall 4.770 +\vec{y}.P(\vec{y})\imp f(\vec{y})\in R$. The premise can be expressed 4.771 +equivalently as 4.772 +\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \] 4.773 +provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$. The 4.774 +following section demonstrates another use of the premise $t\in M(R)$, 4.775 +where $M=\lst$. 4.776 + 4.777 +\subsection{The primitive recursive functions}\label{primrec-sec} 4.778 +The primitive recursive functions are traditionally defined inductively, as 4.779 +a subset of the functions over the natural numbers. One difficulty is that 4.780 +functions of all arities are taken together, but this is easily 4.781 +circumvented by regarding them as functions on lists. Another difficulty, 4.782 +the notion of composition, is less easily circumvented. 4.783 + 4.784 +Here is a more precise definition. Letting $\vec{x}$ abbreviate 4.785 +$x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$, 4.786 +$[y+1,\vec{x}]$, etc. A function is {\bf primitive recursive} if it 4.787 +belongs to the least set of functions in $\lst(\nat)\to\nat$ containing 4.788 +\begin{itemize} 4.789 +\item The {\bf successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$. 4.790 +\item All {\bf constant} functions $\CONST(k)$, such that 4.791 + $\CONST(k)[\vec{x}]=k$. 4.792 +\item All {\bf projection} functions $\PROJ(i)$, such that 4.793 + $\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$. 4.794 +\item All {\bf compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$, 4.795 +where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive, 4.796 +such that 4.797 +\begin{eqnarray*} 4.798 + \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] & = & 4.799 + g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]]. 4.800 +\end{eqnarray*} 4.801 + 4.802 +\item All {\bf recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive 4.803 + recursive, such that 4.804 +\begin{eqnarray*} 4.805 + \PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\ 4.806 + \PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}]. 4.807 +\end{eqnarray*} 4.808 +\end{itemize} 4.809 +Composition is awkward because it combines not two functions, as is usual, 4.810 +but $m+1$ functions. In her proof that Ackermann's function is not 4.811 +primitive recursive, Nora Szasz was unable to formalize this definition 4.812 +directly~\cite{szasz93}. So she generalized primitive recursion to 4.813 +tuple-valued functions. This modified the inductive definition such that 4.814 +each operation on primitive recursive functions combined just two functions. 4.815 + 4.816 +\begin{figure} 4.817 +\begin{ttbox} 4.818 +structure Primrec = Inductive_Fun 4.819 + (val thy = Primrec0.thy; 4.820 + val rec_doms = [("primrec", "list(nat)->nat")]; 4.821 + val ext = None 4.822 + val sintrs = 4.823 + ["SC : primrec", 4.824 + "k: nat ==> CONST(k) : primrec", 4.825 + "i: nat ==> PROJ(i) : primrec", 4.826 + "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec", 4.827 + "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"]; 4.828 + val monos = [list_mono]; 4.829 + val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]; 4.830 + val type_intrs = pr0_typechecks 4.831 + val type_elims = []); 4.832 +\end{ttbox} 4.833 +\hrule 4.834 +\caption{Inductive definition of the primitive recursive functions} 4.835 +\label{primrec-fig} 4.836 +\end{figure} 4.837 +\def\fs{{\it fs}} 4.838 +Szasz was using ALF, but Coq and HOL would also have problems accepting 4.839 +this definition. Isabelle's package accepts it easily since 4.840 +$[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and 4.841 +$\lst$ is monotonic. There are five introduction rules, one for each of 4.842 +the five forms of primitive recursive function. Note the one for $\COMP$: 4.843 +\[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \] 4.844 +The induction rule for $\primrec$ has one case for each introduction rule. 4.845 +Due to the use of $\lst$ as a monotone operator, the composition case has 4.846 +an unusual induction hypothesis: 4.847 + \[ \infer*{P(\COMP(g,\fs))} 4.848 + {[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(x)\})]_{\fs,g}} \] 4.849 +The hypothesis states that $\fs$ is a list of primitive recursive functions 4.850 +satisfying the induction formula. Proving the $\COMP$ case typically requires 4.851 +structural induction on lists, yielding two subcases: either $\fs=\Nil$ or 4.852 +else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and $\fs'$ is 4.853 +another list of primitive recursive functions satisfying~$P$. 4.854 + 4.855 +Figure~\ref{primrec-fig} presents the ML invocation. Theory {\tt 4.856 + Primrec0.thy} defines the constants $\SC$, etc.; their definitions 4.857 +consist of routine list programming and are omitted. The Isabelle theory 4.858 +goes on to formalize Ackermann's function and prove that it is not 4.859 +primitive recursive, using the induction rule {\tt Primrec.induct}. The 4.860 +proof follows Szasz's excellent account. 4.861 + 4.862 +ALF and Coq treat inductive definitions as datatypes, with a new 4.863 +constructor for each introduction rule. This forced Szasz to define a 4.864 +small programming language for the primitive recursive functions, and then 4.865 +define their semantics. But the Isabelle/ZF formulation defines the 4.866 +primitive recursive functions directly as a subset of the function set 4.867 +$\lst(\nat)\to\nat$. This saves a step and conforms better to mathematical 4.868 +tradition. 4.869 + 4.870 + 4.871 +\section{Datatypes and co-datatypes}\label{data-sec} 4.872 +A (co-)datatype definition is a (co-)inductive definition with automatically 4.873 +defined constructors and case analysis operator. The package proves that the 4.874 +case operator inverts the constructors, and can also prove freeness theorems 4.875 +involving any pair of constructors. 4.876 + 4.877 + 4.878 +\subsection{Constructors and their domain} 4.879 +Conceptually, our two forms of definition are distinct: a (co-)inductive 4.880 +definition selects a subset of an existing set, but a (co-)datatype 4.881 +definition creates a new set. But the package reduces the latter to the 4.882 +former. A set having strong closure properties must serve as the domain 4.883 +of the (co-)inductive definition. Constructing this set requires some 4.884 +theoretical effort. Consider first datatypes and then co-datatypes. 4.885 + 4.886 +Isabelle/ZF defines the standard notion of Cartesian product $A\times B$, 4.887 +containing ordered pairs $\pair{a,b}$. Now the $m$-tuple 4.888 +$\pair{x_1,\ldots\,x_m}$ is the empty set~$\emptyset$ if $m=0$, simply 4.889 +$x_1$ if $m=1$, and $\pair{x_1,\pair{x_2,\ldots\,x_m}}$ if $m\geq2$. 4.890 +Isabelle/ZF also defines the disjoint sum $A+B$, containing injections 4.891 +$\Inl(a)\equiv\pair{0,a}$ and $\Inr(b)\equiv\pair{1,b}$. 4.892 + 4.893 +A datatype constructor $\Con(x_1,\ldots\,x_m)$ is defined to be 4.894 +$h(\pair{x_1,\ldots\,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$. 4.895 +In a mutually recursive definition, all constructors for the set~$R_i$ have 4.896 +the outer form~$h_{i,n}$, where $h_{i,n}$ is the injection described 4.897 +in~\S\ref{mutual-sec}. Further nested injections ensure that the 4.898 +constructors for~$R_i$ are pairwise distinct. 4.899 + 4.900 +Isabelle/ZF defines the set $\univ(A)$, which contains~$A$ and 4.901 +furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$, 4.902 +$b\in\univ(A)$. In a typical datatype definition with set parameters 4.903 +$A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is 4.904 +$\univ(A_1\un\cdots\un A_k)$. This solves the problem for 4.905 +datatypes~\cite[\S4.2]{paulson-set-II}. 4.906 + 4.907 +The standard pairs and injections can only yield well-founded 4.908 +constructions. This eases the (manual!) definition of recursive functions 4.909 +over datatypes. But they are unsuitable for co-datatypes, which typically 4.910 +contain non-well-founded objects. 4.911 + 4.912 +To support co-datatypes, Isabelle/ZF defines a variant notion of ordered 4.913 +pair, written~$\pair{a;b}$. It also defines the corresponding variant 4.914 +notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$ 4.915 +and~$\QInr(b)$, and variant disjoint sum $A\oplus B$. Finally it defines 4.916 +the set $\quniv(A)$, which contains~$A$ and furthermore contains 4.917 +$\pair{a;b}$, $\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a 4.918 +typical co-datatype definition with set parameters $A_1$, \ldots, $A_k$, a 4.919 +suitable domain is $\quniv(A_1\un\cdots\un A_k)$. This approach is an 4.920 +alternative to adopting an Anti-Foundation 4.921 +Axiom~\cite{aczel88}.\footnote{No reference is available. Variant pairs 4.922 + are defined by $\pair{a;b}\equiv a+b \equiv (\{0\}\times a) \un (\{1\}\times 4.923 + b)$, where $\times$ is the Cartesian product for standard ordered pairs. Now 4.924 + $\pair{a;b}$ is injective and monotonic in its two arguments. 4.925 + Non-well-founded constructions, such as infinite lists, are constructed 4.926 + as least fixedpoints; the bounding set typically has the form 4.927 + $\univ(a_1\un\cdots\un a_k)$, where $a_1$, \ldots, $a_k$ are specified 4.928 + elements of the construction.} 4.929 + 4.930 + 4.931 +\subsection{The case analysis operator} 4.932 +The (co-)datatype package automatically defines a case analysis operator, 4.933 +called {\tt$R$\_case}. A mutually recursive definition still has only 4.934 +one operator, called {\tt$R_1$\_\ldots\_$R_n$\_case}. The case operator is 4.935 +analogous to those for products and sums. 4.936 + 4.937 +Datatype definitions employ standard products and sums, whose operators are 4.938 +$\split$ and $\case$ and satisfy the equations 4.939 +\begin{eqnarray*} 4.940 + \split(f,\pair{x,y}) & = & f(x,y) \\ 4.941 + \case(f,g,\Inl(x)) & = & f(x) \\ 4.942 + \case(f,g,\Inr(y)) & = & g(y) 4.943 +\end{eqnarray*} 4.944 +Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$. Then 4.945 +its case operator takes $k+1$ arguments and satisfies an equation for each 4.946 +constructor: 4.947 +\begin{eqnarray*} 4.948 + R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) & = & f_i(\vec{x}), 4.949 + \qquad i = 1, \ldots, k 4.950 +\end{eqnarray*} 4.951 +Note that if $f$ and $g$ have meta-type $i\To i$ then so do $\split(f)$ and 4.952 +$\case(f,g)$. This works because $\split$ and $\case$ operate on their 4.953 +last argument. They are easily combined to make complex case analysis 4.954 +operators. Here are two examples: 4.955 +\begin{itemize} 4.956 +\item $\split(\lambda x.\split(f(x)))$ performs case analysis for 4.957 +$A\times (B\times C)$, as is easily verified: 4.958 +\begin{eqnarray*} 4.959 + \split(\lambda x.\split(f(x)), \pair{a,b,c}) 4.960 + & = & (\lambda x.\split(f(x))(a,\pair{b,c}) \\ 4.961 + & = & \split(f(a), \pair{b,c}) \\ 4.962 + & = & f(a,b,c) 4.963 +\end{eqnarray*} 4.964 + 4.965 +\item $\case(f,\case(g,h))$ performs case analysis for $A+(B+C)$; let us 4.966 +verify one of the three equations: 4.967 +\begin{eqnarray*} 4.968 + \case(f,\case(g,h), \Inr(\Inl(b))) 4.969 + & = & \case(g,h,\Inl(b)) \\ 4.970 + & = & g(b) 4.971 +\end{eqnarray*} 4.972 +\end{itemize} 4.973 +Co-datatype definitions are treated in precisely the same way. They express 4.974 +case operators using those for the variant products and sums, namely 4.975 +$\qsplit$ and~$\qcase$. 4.976 + 4.977 + 4.978 +\ifCADE The package has processed all the datatypes discussed in my earlier 4.979 +paper~\cite{paulson-set-II} and the co-datatype of lazy lists. Space 4.980 +limitations preclude discussing these examples here, but they are 4.981 +distributed with Isabelle. 4.982 +\typeout{****Omitting datatype examples from CADE version!} \else 4.983 + 4.984 +To see how constructors and the case analysis operator are defined, let us 4.985 +examine some examples. These include lists and trees/forests, which I have 4.986 +discussed extensively in another paper~\cite{paulson-set-II}. 4.987 + 4.988 +\begin{figure} 4.989 +\begin{ttbox} 4.990 +structure List = Datatype_Fun 4.991 + (val thy = Univ.thy; 4.992 + val rec_specs = 4.993 + [("list", "univ(A)", 4.994 + [(["Nil"], "i"), 4.995 + (["Cons"], "[i,i]=>i")])]; 4.996 + val rec_styp = "i=>i"; 4.997 + val ext = None 4.998 + val sintrs = 4.999 + ["Nil : list(A)", 4.1000 + "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"]; 4.1001 + val monos = []; 4.1002 + val type_intrs = datatype_intrs 4.1003 + val type_elims = datatype_elims); 4.1004 +\end{ttbox} 4.1005 +\hrule 4.1006 +\caption{Defining the datatype of lists} \label{list-fig} 4.1007 + 4.1008 +\medskip 4.1009 +\begin{ttbox} 4.1010 +structure LList = Co_Datatype_Fun 4.1011 + (val thy = QUniv.thy; 4.1012 + val rec_specs = 4.1013 + [("llist", "quniv(A)", 4.1014 + [(["LNil"], "i"), 4.1015 + (["LCons"], "[i,i]=>i")])]; 4.1016 + val rec_styp = "i=>i"; 4.1017 + val ext = None 4.1018 + val sintrs = 4.1019 + ["LNil : llist(A)", 4.1020 + "[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"]; 4.1021 + val monos = []; 4.1022 + val type_intrs = co_datatype_intrs 4.1023 + val type_elims = co_datatype_elims); 4.1024 +\end{ttbox} 4.1025 +\hrule 4.1026 +\caption{Defining the co-datatype of lazy lists} \label{llist-fig} 4.1027 +\end{figure} 4.1028 + 4.1029 +\subsection{Example: lists and lazy lists} 4.1030 +Figures \ref{list-fig} and~\ref{llist-fig} present the ML definitions of 4.1031 +lists and lazy lists, respectively. They highlight the (many) similarities 4.1032 +and (few) differences between datatype and co-datatype definitions. 4.1033 + 4.1034 +Each form of list has two constructors, one for the empty list and one for 4.1035 +adding an element to a list. Each takes a parameter, defining the set of 4.1036 +lists over a given set~$A$. Each uses the appropriate domain from a 4.1037 +Isabelle/ZF theory: 4.1038 +\begin{itemize} 4.1039 +\item $\lst(A)$ specifies domain $\univ(A)$ and parent theory {\tt Univ.thy}. 4.1040 + 4.1041 +\item $\llist(A)$ specifies domain $\quniv(A)$ and parent theory {\tt 4.1042 +QUniv.thy}. 4.1043 +\end{itemize} 4.1044 + 4.1045 +Since $\lst(A)$ is a datatype, it enjoys a structural rule, {\tt List.induct}: 4.1046 +\[ \infer{P(x)}{x\in\lst(A) & P(\Nil) 4.1047 + & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} } 4.1048 +\] 4.1049 +Induction and freeness yield the law $l\not=\Cons(a,l)$. To strengthen this, 4.1050 +Isabelle/ZF defines the rank of a set and proves that the standard pairs and 4.1051 +injections have greater rank than their components. An immediate consequence, 4.1052 +which justifies structural recursion on lists \cite[\S4.3]{paulson-set-II}, 4.1053 +is 4.1054 +\[ \rank(l) < \rank(\Cons(a,l)). \] 4.1055 + 4.1056 +Since $\llist(A)$ is a co-datatype, it has no induction rule. Instead it has 4.1057 +the co-induction rule shown in \S\ref{co-ind-sec}. Since variant pairs and 4.1058 +injections are monotonic and need not have greater rank than their 4.1059 +components, fixedpoint operators can create cyclic constructions. For 4.1060 +example, the definition 4.1061 +\begin{eqnarray*} 4.1062 + \lconst(a) & \equiv & \lfp(\univ(a), \lambda l. \LCons(a,l)) 4.1063 +\end{eqnarray*} 4.1064 +yields $\lconst(a) = \LCons(a,\lconst(a))$. 4.1065 + 4.1066 +\medskip 4.1067 +It may be instructive to examine the definitions of the constructors and 4.1068 +case operator for $\lst(A)$. The definitions for $\llist(A)$ are similar. 4.1069 +The list constructors are defined as follows: 4.1070 +\begin{eqnarray*} 4.1071 + \Nil & = & \Inl(\emptyset) \\ 4.1072 + \Cons(a,l) & = & \Inr(\pair{a,l}) 4.1073 +\end{eqnarray*} 4.1074 +The operator $\lstcase$ performs case analysis on these two alternatives: 4.1075 +\begin{eqnarray*} 4.1076 + \lstcase(c,h) & \equiv & \case(\lambda u.c, \split(h)) 4.1077 +\end{eqnarray*} 4.1078 +Let us verify the two equations: 4.1079 +\begin{eqnarray*} 4.1080 + \lstcase(c, h, \Nil) & = & 4.1081 + \case(\lambda u.c, \split(h), \Inl(\emptyset)) \\ 4.1082 + & = & (\lambda u.c)(\emptyset) \\ 4.1083 + & = & c.\\[1ex] 4.1084 + \lstcase(c, h, \Cons(x,y)) & = & 4.1085 + \case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\ 4.1086 + & = & \split(h, \pair{x,y}) \\ 4.1087 + & = & h(x,y). 4.1088 +\end{eqnarray*} 4.1089 + 4.1090 +\begin{figure} 4.1091 +\begin{small} 4.1092 +\begin{verbatim} 4.1093 +structure TF = Datatype_Fun 4.1094 + (val thy = Univ.thy; 4.1095 + val rec_specs = 4.1096 + [("tree", "univ(A)", 4.1097 + [(["Tcons"], "[i,i]=>i")]), 4.1098 + ("forest", "univ(A)", 4.1099 + [(["Fnil"], "i"), 4.1100 + (["Fcons"], "[i,i]=>i")])]; 4.1101 + val rec_styp = "i=>i"; 4.1102 + val ext = None 4.1103 + val sintrs = 4.1104 + ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)", 4.1105 + "Fnil : forest(A)", 4.1106 + "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"]; 4.1107 + val monos = []; 4.1108 + val type_intrs = datatype_intrs 4.1109 + val type_elims = datatype_elims); 4.1110 +\end{verbatim} 4.1111 +\end{small} 4.1112 +\hrule 4.1113 +\caption{Defining the datatype of trees and forests} \label{tf-fig} 4.1114 +\end{figure} 4.1115 + 4.1116 + 4.1117 +\subsection{Example: mutual recursion} 4.1118 +In the mutually recursive trees/forests~\cite[\S4.5]{paulson-set-II}, trees 4.1119 +have the one constructor $\Tcons$, while forests have the two constructors 4.1120 +$\Fnil$ and~$\Fcons$. Figure~\ref{tf-fig} presents the ML 4.1121 +definition. It has much in common with that of $\lst(A)$, including its 4.1122 +use of $\univ(A)$ for the domain and {\tt Univ.thy} for the parent theory. 4.1123 +The three introduction rules define the mutual recursion. The 4.1124 +distinguishing feature of this example is its two induction rules. 4.1125 + 4.1126 +The basic induction rule is called {\tt TF.induct}: 4.1127 +\[ \infer{P(x)}{x\in\TF(A) & 4.1128 + \infer*{P(\Tcons(a,f))} 4.1129 + {\left[\begin{array}{l} a\in A \\ 4.1130 + f\in\forest(A) \\ P(f) 4.1131 + \end{array} 4.1132 + \right]_{a,f}} 4.1133 + & P(\Fnil) 4.1134 + & \infer*{P(\Fcons(a,l))} 4.1135 + {\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\ 4.1136 + f\in\forest(A) \\ P(f) 4.1137 + \end{array} 4.1138 + \right]_{t,f}} } 4.1139 +\] 4.1140 +This rule establishes a single predicate for $\TF(A)$, the union of the 4.1141 +recursive sets. 4.1142 + 4.1143 +Although such reasoning is sometimes useful 4.1144 +\cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish 4.1145 +separate predicates for $\tree(A)$ and $\forest(A)$. The package calls this 4.1146 +rule {\tt TF.mutual\_induct}. Observe the usage of $P$ and $Q$ in the 4.1147 +induction hypotheses: 4.1148 +\[ \infer{(\forall z. z\in\tree(A)\imp P(z)) \conj 4.1149 + (\forall z. z\in\forest(A)\imp Q(z))} 4.1150 + {\infer*{P(\Tcons(a,f))} 4.1151 + {\left[\begin{array}{l} a\in A \\ 4.1152 + f\in\forest(A) \\ Q(f) 4.1153 + \end{array} 4.1154 + \right]_{a,f}} 4.1155 + & Q(\Fnil) 4.1156 + & \infer*{Q(\Fcons(a,l))} 4.1157 + {\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\ 4.1158 + f\in\forest(A) \\ Q(f) 4.1159 + \end{array} 4.1160 + \right]_{t,f}} } 4.1161 +\] 4.1162 +As mentioned above, the package does not define a structural recursion 4.1163 +operator. I have described elsewhere how this is done 4.1164 +\cite[\S4.5]{paulson-set-II}. 4.1165 + 4.1166 +Both forest constructors have the form $\Inr(\cdots)$, 4.1167 +while the tree constructor has the form $\Inl(\cdots)$. This pattern would 4.1168 +hold regardless of how many tree or forest constructors there were. 4.1169 +\begin{eqnarray*} 4.1170 + \Tcons(a,l) & = & \Inl(\pair{a,l}) \\ 4.1171 + \Fnil & = & \Inr(\Inl(\emptyset)) \\ 4.1172 + \Fcons(a,l) & = & \Inr(\Inr(\pair{a,l})) 4.1173 +\end{eqnarray*} 4.1174 +There is only one case operator; it works on the union of the trees and 4.1175 +forests: 4.1176 +\begin{eqnarray*} 4.1177 + {\tt tree\_forest\_case}(f,c,g) & \equiv & 4.1178 + \case(\split(f),\, \case(\lambda u.c, \split(g))) 4.1179 +\end{eqnarray*} 4.1180 + 4.1181 +\begin{figure} 4.1182 +\begin{small} 4.1183 +\begin{verbatim} 4.1184 +structure Data = Datatype_Fun 4.1185 + (val thy = Univ.thy; 4.1186 + val rec_specs = 4.1187 + [("data", "univ(A Un B)", 4.1188 + [(["Con0"], "i"), 4.1189 + (["Con1"], "i=>i"), 4.1190 + (["Con2"], "[i,i]=>i"), 4.1191 + (["Con3"], "[i,i,i]=>i")])]; 4.1192 + val rec_styp = "[i,i]=>i"; 4.1193 + val ext = None 4.1194 + val sintrs = 4.1195 + ["Con0 : data(A,B)", 4.1196 + "[| a: A |] ==> Con1(a) : data(A,B)", 4.1197 + "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)", 4.1198 + "[| a: A; b: B; d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"]; 4.1199 + val monos = []; 4.1200 + val type_intrs = datatype_intrs 4.1201 + val type_elims = datatype_elims); 4.1202 +\end{verbatim} 4.1203 +\end{small} 4.1204 +\hrule 4.1205 +\caption{Defining the four-constructor sample datatype} \label{data-fig} 4.1206 +\end{figure} 4.1207 + 4.1208 +\subsection{A four-constructor datatype} 4.1209 +Finally let us consider a fairly general datatype. It has four 4.1210 +constructors $\Con_0$, $\Con_1$\ $\Con_2$ and $\Con_3$, with the 4.1211 +corresponding arities. Figure~\ref{data-fig} presents the ML definition. 4.1212 +Because this datatype has two set parameters, $A$ and~$B$, it specifies 4.1213 +$\univ(A\un B)$ as its domain. The structural induction rule has four 4.1214 +minor premises, one per constructor: 4.1215 +\[ \infer{P(x)}{x\in\data(A,B) & 4.1216 + P(\Con_0) & 4.1217 + \infer*{P(\Con_1(a))}{[a\in A]_a} & 4.1218 + \infer*{P(\Con_2(a,b))} 4.1219 + {\left[\begin{array}{l} a\in A \\ b\in B \end{array} 4.1220 + \right]_{a,b}} & 4.1221 + \infer*{P(\Con_3(a,b,d))} 4.1222 + {\left[\begin{array}{l} a\in A \\ b\in B \\ 4.1223 + d\in\data(A,B) \\ P(d) 4.1224 + \end{array} 4.1225 + \right]_{a,b,d}} } 4.1226 +\] 4.1227 + 4.1228 +The constructor definitions are 4.1229 +\begin{eqnarray*} 4.1230 + \Con_0 & = & \Inl(\Inl(\emptyset)) \\ 4.1231 + \Con_1(a) & = & \Inl(\Inr(a)) \\ 4.1232 + \Con_2(a,b) & = & \Inr(\Inl(\pair{a,b})) \\ 4.1233 + \Con_3(a,b,c) & = & \Inr(\Inr(\pair{a,b,c})). 4.1234 +\end{eqnarray*} 4.1235 +The case operator is 4.1236 +\begin{eqnarray*} 4.1237 + {\tt data\_case}(f_0,f_1,f_2,f_3) & \equiv & 4.1238 + \case(\begin{array}[t]{@{}l} 4.1239 + \case(\lambda u.f_0,\; f_1),\, \\ 4.1240 + \case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) ) 4.1241 + \end{array} 4.1242 +\end{eqnarray*} 4.1243 +This may look cryptic, but the case equations are trivial to verify. 4.1244 + 4.1245 +In the constructor definitions, the injections are balanced. A more naive 4.1246 +approach is to define $\Con_3(a,b,c)$ as 4.1247 +$\Inr(\Inr(\Inr(\pair{a,b,c})))$; instead, each constructor has two 4.1248 +injections. The difference here is small. But the ZF examples include a 4.1249 +60-element enumeration type, where each constructor has 5 or~6 injections. 4.1250 +The naive approach would require 1 to~59 injections; the definitions would be 4.1251 +quadratic in size. It is like the difference between the binary and unary 4.1252 +numeral systems. 4.1253 + 4.1254 +The package returns the constructor and case operator definitions as the 4.1255 +theorem list \verb|con_defs|. The head of this list defines the case 4.1256 +operator and the tail defines the constructors. 4.1257 + 4.1258 +The package returns the case equations, such as 4.1259 +\begin{eqnarray*} 4.1260 + {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) & = & f_3(a,b,c), 4.1261 +\end{eqnarray*} 4.1262 +as the theorem list \verb|case_eqns|. There is one equation per constructor. 4.1263 + 4.1264 +\subsection{Proving freeness theorems} 4.1265 +There are two kinds of freeness theorems: 4.1266 +\begin{itemize} 4.1267 +\item {\bf injectiveness} theorems, such as 4.1268 +\[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \] 4.1269 + 4.1270 +\item {\bf distinctness} theorems, such as 4.1271 +\[ \Con_1(a) \not= \Con_2(a',b') \] 4.1272 +\end{itemize} 4.1273 +Since the number of such theorems is quadratic in the number of constructors, 4.1274 +the package does not attempt to prove them all. Instead it returns tools for 4.1275 +proving desired theorems --- either explicitly or `on the fly' during 4.1276 +simplification or classical reasoning. 4.1277 + 4.1278 +The theorem list \verb|free_iffs| enables the simplifier to perform freeness 4.1279 +reasoning. This works by incremental unfolding of constructors that appear in 4.1280 +equations. The theorem list contains logical equivalences such as 4.1281 +\begin{eqnarray*} 4.1282 + \Con_0=c & \bimp & c=\Inl(\Inl(\emptyset)) \\ 4.1283 + \Con_1(a)=c & \bimp & c=\Inl(\Inr(a)) \\ 4.1284 + & \vdots & \\ 4.1285 + \Inl(a)=\Inl(b) & \bimp & a=b \\ 4.1286 + \Inl(a)=\Inr(b) & \bimp & \bot \\ 4.1287 + \pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b' 4.1288 +\end{eqnarray*} 4.1289 +For example, these rewrite $\Con_1(a)=\Con_1(b)$ to $a=b$ in four steps. 4.1290 + 4.1291 +The theorem list \verb|free_SEs| enables the classical 4.1292 +reasoner to perform similar replacements. It consists of elimination rules 4.1293 +to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$, and so forth, in the 4.1294 +assumptions. 4.1295 + 4.1296 +Such incremental unfolding combines freeness reasoning with other proof 4.1297 +steps. It has the unfortunate side-effect of unfolding definitions of 4.1298 +constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should 4.1299 +be left alone. Calling the Isabelle tactic {\tt fold\_tac con\_defs} 4.1300 +restores the defined constants. 4.1301 +\fi %CADE 4.1302 + 4.1303 +\section{Conclusions and future work} 4.1304 +The fixedpoint approach makes it easy to implement a uniquely powerful 4.1305 +package for inductive and co-inductive definitions. It is efficient: it 4.1306 +processes most definitions in seconds and even a 60-constructor datatype 4.1307 +requires only two minutes. It is also simple: the package consists of 4.1308 +under 1100 lines (35K bytes) of Standard ML code. The first working 4.1309 +version took under a week to code. 4.1310 + 4.1311 +The approach is not restricted to set theory. It should be suitable for 4.1312 +any logic that has some notion of set and the Knaster-Tarski Theorem. 4.1313 +Indeed, Melham's inductive definition package for the HOL 4.1314 +system~\cite{camilleri92} implicitly proves this theorem. 4.1315 + 4.1316 +Datatype and co-datatype definitions furthermore require a particular set 4.1317 +closed under a suitable notion of ordered pair. I intend to use the 4.1318 +Isabelle/ZF package as the basis for a higher-order logic one, using 4.1319 +Isabelle/HOL\@. The necessary theory is already 4.1320 +mechanizeds~\cite{paulson-coind}. HOL represents sets by unary predicates; 4.1321 +defining the corresponding types may cause complication. 4.1322 + 4.1323 + 4.1324 +\bibliographystyle{plain} 4.1325 +\bibliography{atp,theory,funprog,isabelle} 4.1326 +%%%%%\doendnotes 4.1327 + 4.1328 +\ifCADE\typeout{****Omitting appendices from CADE version!} 4.1329 +\else 4.1330 +\newpage 4.1331 +\appendix 4.1332 +\section{Inductive and co-inductive definitions: users guide} 4.1333 +The ML functors \verb|Inductive_Fun| and \verb|Co_Inductive_Fun| build 4.1334 +inductive and co-inductive definitions, respectively. This section describes 4.1335 +how to invoke them. 4.1336 + 4.1337 +\subsection{The result structure} 4.1338 +Many of the result structure's components have been discussed 4.1339 +in~\S\ref{basic-sec}; others are self-explanatory. 4.1340 +\begin{description} 4.1341 +\item[\tt thy] is the new theory containing the recursive sets. 4.1342 + 4.1343 +\item[\tt defs] is the list of definitions of the recursive sets. 4.1344 + 4.1345 +\item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator. 4.1346 + 4.1347 +\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of 4.1348 +the recursive sets, in the case of mutual recursion). 4.1349 + 4.1350 +\item[\tt dom\_subset] is a theorem stating inclusion in the domain. 4.1351 + 4.1352 +\item[\tt intrs] is the list of introduction rules, now proved as theorems, for 4.1353 +the recursive sets. 4.1354 + 4.1355 +\item[\tt elim] is the elimination rule. 4.1356 + 4.1357 +\item[\tt mk\_cases] is a function to create simplified instances of {\tt 4.1358 +elim}, using freeness reasoning on some underlying datatype. 4.1359 +\end{description} 4.1360 + 4.1361 +For an inductive definition, the result structure contains two induction rules, 4.1362 +{\tt induct} and \verb|mutual_induct|. For a co-inductive definition, it 4.1363 +contains the rule \verb|co_induct|. 4.1364 + 4.1365 +\begin{figure} 4.1366 +\begin{ttbox} 4.1367 +sig 4.1368 +val thy : theory 4.1369 +val defs : thm list 4.1370 +val bnd_mono : thm 4.1371 +val unfold : thm 4.1372 +val dom_subset : thm 4.1373 +val intrs : thm list 4.1374 +val elim : thm 4.1375 +val mk_cases : thm list -> string -> thm 4.1376 +{\it(Inductive definitions only)} 4.1377 +val induct : thm 4.1378 +val mutual_induct: thm 4.1379 +{\it(Co-inductive definitions only)} 4.1380 +val co_induct : thm 4.1381 +end 4.1382 +\end{ttbox} 4.1383 +\hrule 4.1384 +\caption{The result of a (co-)inductive definition} \label{def-result-fig} 4.1385 +\end{figure} 4.1386 + 4.1387 +Figure~\ref{def-result-fig} summarizes the two result signatures, 4.1388 +specifying the types of all these components. 4.1389 + 4.1390 +\begin{figure} 4.1391 +\begin{ttbox} 4.1392 +sig 4.1393 +val thy : theory 4.1394 +val rec_doms : (string*string) list 4.1395 +val sintrs : string list 4.1396 +val monos : thm list 4.1397 +val con_defs : thm list 4.1398 +val type_intrs : thm list 4.1399 +val type_elims : thm list 4.1400 +end 4.1401 +\end{ttbox} 4.1402 +\hrule 4.1403 +\caption{The argument of a (co-)inductive definition} \label{def-arg-fig} 4.1404 +\end{figure} 4.1405 + 4.1406 +\subsection{The argument structure} 4.1407 +Both \verb|Inductive_Fun| and \verb|Co_Inductive_Fun| take the same argument 4.1408 +structure (Figure~\ref{def-arg-fig}). Its components are as follows: 4.1409 +\begin{description} 4.1410 +\item[\tt thy] is the definition's parent theory, which {\it must\/} 4.1411 +declare constants for the recursive sets. 4.1412 + 4.1413 +\item[\tt rec\_doms] is a list of pairs, associating the name of each recursive 4.1414 +set with its domain. 4.1415 + 4.1416 +\item[\tt sintrs] specifies the desired introduction rules as strings. 4.1417 + 4.1418 +\item[\tt monos] consists of monotonicity theorems for each operator applied 4.1419 +to a recursive set in the introduction rules. 4.1420 + 4.1421 +\item[\tt con\_defs] contains definitions of constants appearing in the 4.1422 +introduction rules. The (co-)datatype package supplies the constructors' 4.1423 +definitions here. Most direct calls of \verb|Inductive_Fun| or 4.1424 +\verb|Co_Inductive_Fun| pass the empty list; one exception is the primitive 4.1425 +recursive functions example (\S\ref{primrec-sec}). 4.1426 + 4.1427 +\item[\tt type\_intrs] consists of introduction rules for type-checking the 4.1428 + definition, as discussed in~\S\ref{basic-sec}. They are applied using 4.1429 + depth-first search; you can trace the proof by setting 4.1430 + \verb|trace_DEPTH_FIRST := true|. 4.1431 + 4.1432 +\item[\tt type\_elims] consists of elimination rules for type-checking the 4.1433 +definition. They are presumed to be `safe' and are applied as much as 4.1434 +possible, prior to the {\tt type\_intrs} search. 4.1435 +\end{description} 4.1436 +The package has a few notable restrictions: 4.1437 +\begin{itemize} 4.1438 +\item The parent theory, {\tt thy}, must declare the recursive sets as 4.1439 + constants. You can extend a theory with new constants using {\tt 4.1440 + addconsts}, as illustrated in~\S\ref{ind-eg-sec}. If the inductive 4.1441 + definition also requires new concrete syntax, then it is simpler to 4.1442 + express the parent theory using a theory file. It is often convenient to 4.1443 + define an infix syntax for relations, say $a\prec b$ for $\pair{a,b}\in 4.1444 + R$. 4.1445 + 4.1446 +\item The names of the recursive sets must be identifiers, not infix 4.1447 +operators. 4.1448 + 4.1449 +\item Side-conditions must not be conjunctions. However, an introduction rule 4.1450 +may contain any number of side-conditions. 4.1451 +\end{itemize} 4.1452 + 4.1453 + 4.1454 +\section{Datatype and co-datatype definitions: users guide} 4.1455 +The ML functors \verb|Datatype_Fun| and \verb|Co_Datatype_Fun| define datatypes 4.1456 +and co-datatypes, invoking \verb|Datatype_Fun| and 4.1457 +\verb|Co_Datatype_Fun| to make the underlying (co-)inductive definitions. 4.1458 + 4.1459 + 4.1460 +\subsection{The result structure} 4.1461 +The result structure extends that of (co-)inductive definitions 4.1462 +(Figure~\ref{def-result-fig}) with several additional items: 4.1463 +\begin{ttbox} 4.1464 +val con_thy : theory 4.1465 +val con_defs : thm list 4.1466 +val case_eqns : thm list 4.1467 +val free_iffs : thm list 4.1468 +val free_SEs : thm list 4.1469 +val mk_free : string -> thm 4.1470 +\end{ttbox} 4.1471 +Most of these have been discussed in~\S\ref{data-sec}. Here is a summary: 4.1472 +\begin{description} 4.1473 +\item[\tt con\_thy] is a new theory containing definitions of the 4.1474 +(co-)datatype's constructors and case operator. It also declares the 4.1475 +recursive sets as constants, so that it may serve as the parent 4.1476 +theory for the (co-)inductive definition. 4.1477 + 4.1478 +\item[\tt con\_defs] is a list of definitions: the case operator followed by 4.1479 +the constructors. This theorem list can be supplied to \verb|mk_cases|, for 4.1480 +example. 4.1481 + 4.1482 +\item[\tt case\_eqns] is a list of equations, stating that the case operator 4.1483 +inverts each constructor. 4.1484 + 4.1485 +\item[\tt free\_iffs] is a list of logical equivalences to perform freeness 4.1486 +reasoning by rewriting. A typical application has the form 4.1487 +\begin{ttbox} 4.1488 +by (asm_simp_tac (ZF_ss addsimps free_iffs) 1); 4.1489 +\end{ttbox} 4.1490 + 4.1491 +\item[\tt free\_SEs] is a list of `safe' elimination rules to perform freeness 4.1492 +reasoning. It can be supplied to \verb|eresolve_tac| or to the classical 4.1493 +reasoner: 4.1494 +\begin{ttbox} 4.1495 +by (fast_tac (ZF_cs addSEs free_SEs) 1); 4.1496 +\end{ttbox} 4.1497 + 4.1498 +\item[\tt mk\_free] is a function to prove freeness properties, specified as 4.1499 +strings. The theorems can be expressed in various forms, such as logical 4.1500 +equivalences or elimination rules. 4.1501 +\end{description} 4.1502 + 4.1503 +The result structure also inherits everything from the underlying 4.1504 +(co-)inductive definition, such as the introduction rules, elimination rule, 4.1505 +and induction/co-induction rule. 4.1506 + 4.1507 + 4.1508 +\begin{figure} 4.1509 +\begin{ttbox} 4.1510 +sig 4.1511 +val thy : theory 4.1512 +val rec_specs : (string * string * (string list*string)list) list 4.1513 +val rec_styp : string 4.1514 +val ext : Syntax.sext option 4.1515 +val sintrs : string list 4.1516 +val monos : thm list 4.1517 +val type_intrs: thm list 4.1518 +val type_elims: thm list 4.1519 +end 4.1520 +\end{ttbox} 4.1521 +\hrule 4.1522 +\caption{The argument of a (co-)datatype definition} \label{data-arg-fig} 4.1523 +\end{figure} 4.1524 + 4.1525 +\subsection{The argument structure} 4.1526 +Both (co-)datatype functors take the same argument structure 4.1527 +(Figure~\ref{data-arg-fig}). It does not extend that for (co-)inductive 4.1528 +definitions, but shares several components and passes them uninterpreted to 4.1529 +\verb|Datatype_Fun| or 4.1530 +\verb|Co_Datatype_Fun|. The new components are as follows: 4.1531 +\begin{description} 4.1532 +\item[\tt thy] is the (co-)datatype's parent theory. It {\it must not\/} 4.1533 +declare constants for the recursive sets. Recall that (co-)inductive 4.1534 +definitions have the opposite restriction. 4.1535 + 4.1536 +\item[\tt rec\_specs] is a list of triples of the form ({\it recursive set\/}, 4.1537 +{\it domain\/}, {\it constructors\/}) for each mutually recursive set. {\it 4.1538 +Constructors\/} is a list of the form (names, type). See the discussion and 4.1539 +examples in~\S\ref{data-sec}. 4.1540 + 4.1541 +\item[\tt rec\_styp] is the common meta-type of the mutually recursive sets, 4.1542 +specified as a string. They must all have the same type because all must 4.1543 +take the same parameters. 4.1544 + 4.1545 +\item[\tt ext] is an optional syntax extension, usually omitted by writing 4.1546 +{\tt None}. You can supply mixfix syntax for the constructors by supplying 4.1547 +\begin{ttbox} 4.1548 +Some (Syntax.simple_sext [{\it mixfix declarations\/}]) 4.1549 +\end{ttbox} 4.1550 +\end{description} 4.1551 +The choice of domain is usually simple. Isabelle/ZF defines the set 4.1552 +$\univ(A)$, which contains~$A$ and is closed under the standard Cartesian 4.1553 +products and disjoint sums \cite[\S4.2]{paulson-set-II}. In a typical 4.1554 +datatype definition with set parameters $A_1$, \ldots, $A_k$, a suitable 4.1555 +domain for all the recursive sets is $\univ(A_1\un\cdots\un A_k)$. For a 4.1556 +co-datatype definition, the set 4.1557 +$\quniv(A)$ contains~$A$ and is closed under the variant Cartesian products 4.1558 +and disjoint sums; the appropropriate domain is 4.1559 +$\quniv(A_1\un\cdots\un A_k)$. 4.1560 + 4.1561 +The {\tt sintrs} specify the introduction rules, which govern the recursive 4.1562 +structure of the datatype. Introduction rules may involve monotone operators 4.1563 +and side-conditions to express things that go beyond the usual notion of 4.1564 +datatype. The theorem lists {\tt monos}, {\tt type\_intrs} and {\tt 4.1565 +type\_elims} should contain precisely what is needed for the underlying 4.1566 +(co-)inductive definition. Isabelle/ZF defines theorem lists that can be 4.1567 +defined for the latter two components: 4.1568 +\begin{itemize} 4.1569 +\item {\tt datatype\_intrs} and {\tt datatype\_elims} are type-checking rules 4.1570 +for $\univ(A)$. 4.1571 +\item {\tt co\_datatype\_intrs} and {\tt co\_datatype\_elims} are type-checking 4.1572 +rules for $\quniv(A)$. 4.1573 +\end{itemize} 4.1574 +In typical definitions, these theorem lists need not be supplemented with 4.1575 +other theorems. 4.1576 + 4.1577 +The constructor definitions' right-hand sides can overlap. A 4.1578 +simple example is the datatype for the combinators, whose constructors are 4.1579 +\begin{eqnarray*} 4.1580 + {\tt K} & \equiv & \Inl(\emptyset) \\ 4.1581 + {\tt S} & \equiv & \Inr(\Inl(\emptyset)) \\ 4.1582 + p{\tt\#}q & \equiv & \Inr(\Inl(\pair{p,q})) 4.1583 +\end{eqnarray*} 4.1584 +Unlike in previous versions of Isabelle, \verb|fold_tac| now ensures that the 4.1585 +longest right-hand sides are folded first. 4.1586 + 4.1587 +\fi 4.1588 +\end{document}

5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 5.2 +++ b/doc-src/sedindex Tue Nov 09 16:47:38 1993 +0100 5.3 @@ -0,0 +1,19 @@ 5.4 +#! /bin/sh 5.5 +# 5.6 +#sedindex - shell script to create indexes, preprocessing LaTeX's .idx file 5.7 +# 5.8 +# puts strings prefixed by * into \tt font 5.9 +# terminator characters for strings are |!@{} 5.10 +# 5.11 +# change *"X"Y"Z"W to "X"Y"Z"W@{\tt "X"Y"Z"W} 5.12 +# change *"X"Y"Z to "X"Y"Z@{\tt "X"Y"Z} 5.13 +# change *"X"Y to "X"Y@{\tt "X"Y} 5.14 +# change *"X to "X@{\tt "X} 5.15 +# change *IDENT to IDENT@{\tt IDENT} 5.16 +# where IDENT is any string not containing | ! or @ 5.17 +# FOUR backslashes: to escape the shell AND sed 5.18 +sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\tt \1}~g 5.19 +s~\*\(\".\".\".\)~\1@{\\\\tt \1}~g 5.20 +s~\*\(\".\".\)~\1@{\\\\tt \1}~g 5.21 +s~\*\(\".\)~\1@{\\\\tt \1}~g 5.22 +s~\*\([^|!@{}][^|!@{}]*\)~\1@{\\\\tt \1}~g" $1.idx | makeindex -q -o $1.ind