# HG changeset patch # User wenzelm # Date 1436172855 -7200 # Node ID ca1e07005b8b67ea0a42b2996b9a3ec156c3a546 # Parent 7df8e5b05f5a028035ed9f192123b581272bc751 tuned whitespace; diff -r 7df8e5b05f5a -r ca1e07005b8b src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Sun Jul 05 23:16:35 2015 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Jul 06 10:54:15 2015 +0200 @@ -1,8 +1,14 @@ theory HOL_Specific -imports Base "~~/src/HOL/Library/Old_Datatype" "~~/src/HOL/Library/Old_Recdef" - "~~/src/Tools/Adhoc_Overloading" "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/FSet" +imports + Base + "~~/src/HOL/Library/Old_Datatype" + "~~/src/HOL/Library/Old_Recdef" + "~~/src/Tools/Adhoc_Overloading" + "~~/src/HOL/Library/Dlist" + "~~/src/HOL/Library/FSet" begin + chapter \Higher-Order Logic\ text \Isabelle/HOL is based on Higher-Order Logic, a polymorphic @@ -171,12 +177,10 @@ \end{description} - When several predicates @{text "R\<^sub>1, \, R\<^sub>n"} are - defined simultaneously, the list of introduction rules is called - @{text "R\<^sub>1_\_R\<^sub>n.intros"}, the case analysis rules are - called @{text "R\<^sub>1.cases, \, R\<^sub>n.cases"}, and the list - of mutual induction rules is called @{text - "R\<^sub>1_\_R\<^sub>n.inducts"}. + When several predicates @{text "R\<^sub>1, \, R\<^sub>n"} are defined simultaneously, + the list of introduction rules is called @{text "R\<^sub>1_\_R\<^sub>n.intros"}, the + case analysis rules are called @{text "R\<^sub>1.cases, \, R\<^sub>n.cases"}, and the + list of mutual induction rules is called @{text "R\<^sub>1_\_R\<^sub>n.inducts"}. \ @@ -236,8 +240,8 @@ (*<*)end(*>*) text \Common logical connectives can be easily characterized as -non-recursive inductive definitions with parameters, but without -arguments.\ + non-recursive inductive definitions with parameters, but without + arguments.\ (*<*)experiment begin(*>*) inductive AND for A B :: bool @@ -251,12 +255,12 @@ where "B a \ EXISTS B" (*<*)end(*>*) -text \Here the @{text "cases"} or @{text "induct"} rules produced by - the @{command inductive} package coincide with the expected - elimination rules for Natural Deduction. Already in the original - article by Gerhard Gentzen @{cite "Gentzen:1935"} there is a hint that - each connective can be characterized by its introductions, and the - elimination can be constructed systematically.\ +text \Here the @{text "cases"} or @{text "induct"} rules produced by the + @{command inductive} package coincide with the expected elimination rules + for Natural Deduction. Already in the original article by Gerhard Gentzen + @{cite "Gentzen:1935"} there is a hint that each connective can be + characterized by its introductions, and the elimination can be constructed + systematically.\ section \Recursive functions \label{sec:recursion}\ @@ -288,101 +292,98 @@ \begin{description} - \item @{command (HOL) "primrec"} defines primitive recursive - functions over datatypes (see also @{command_ref (HOL) datatype}). - The given @{text equations} specify reduction rules that are produced - by instantiating the generic combinator for primitive recursion that - is available for each datatype. + \item @{command (HOL) "primrec"} defines primitive recursive functions + over datatypes (see also @{command_ref (HOL) datatype}). The given @{text + equations} specify reduction rules that are produced by instantiating the + generic combinator for primitive recursion that is available for each + datatype. Each equation needs to be of the form: @{text [display] "f x\<^sub>1 \ x\<^sub>m (C y\<^sub>1 \ y\<^sub>k) z\<^sub>1 \ z\<^sub>n = rhs"} - such that @{text C} is a datatype constructor, @{text rhs} contains - only the free variables on the left-hand side (or from the context), - and all recursive occurrences of @{text "f"} in @{text "rhs"} are of - the form @{text "f \ y\<^sub>i \"} for some @{text i}. At most one - reduction rule for each constructor can be given. The order does - not matter. For missing constructors, the function is defined to - return a default value, but this equation is made difficult to - access for users. - - The reduction rules are declared as @{attribute simp} by default, - which enables standard proof methods like @{method simp} and - @{method auto} to normalize expressions of @{text "f"} applied to - datatype constructions, by simulating symbolic computation via - rewriting. - - \item @{command (HOL) "function"} defines functions by general - wellfounded recursion. A detailed description with examples can be - found in @{cite "isabelle-function"}. The function is specified by a - set of (possibly conditional) recursive equations with arbitrary - pattern matching. The command generates proof obligations for the - completeness and the compatibility of patterns. + such that @{text C} is a datatype constructor, @{text rhs} contains only + the free variables on the left-hand side (or from the context), and all + recursive occurrences of @{text "f"} in @{text "rhs"} are of the form + @{text "f \ y\<^sub>i \"} for some @{text i}. At most one reduction rule for + each constructor can be given. The order does not matter. For missing + constructors, the function is defined to return a default value, but this + equation is made difficult to access for users. + + The reduction rules are declared as @{attribute simp} by default, which + enables standard proof methods like @{method simp} and @{method auto} to + normalize expressions of @{text "f"} applied to datatype constructions, by + simulating symbolic computation via rewriting. + + \item @{command (HOL) "function"} defines functions by general wellfounded + recursion. A detailed description with examples can be found in @{cite + "isabelle-function"}. The function is specified by a set of (possibly + conditional) recursive equations with arbitrary pattern matching. The + command generates proof obligations for the completeness and the + compatibility of patterns. The defined function is considered partial, and the resulting - simplification rules (named @{text "f.psimps"}) and induction rule - (named @{text "f.pinduct"}) are guarded by a generated domain - predicate @{text "f_dom"}. The @{command (HOL) "termination"} - command can then be used to establish that the function is total. - - \item @{command (HOL) "fun"} is a shorthand notation for ``@{command - (HOL) "function"}~@{text "(sequential)"}'', followed by automated - proof attempts regarding pattern matching and termination. See - @{cite "isabelle-function"} for further details. - - \item @{command (HOL) "termination"}~@{text f} commences a - termination proof for the previously defined function @{text f}. If - this is omitted, the command refers to the most recent function - definition. After the proof is closed, the recursive equations and - the induction principle is established. - - \item @{command (HOL) "fun_cases"} generates specialized elimination - rules for function equations. It expects one or more function equations - and produces rules that eliminate the given equalities, following the cases + simplification rules (named @{text "f.psimps"}) and induction rule (named + @{text "f.pinduct"}) are guarded by a generated domain predicate @{text + "f_dom"}. The @{command (HOL) "termination"} command can then be used to + establish that the function is total. + + \item @{command (HOL) "fun"} is a shorthand notation for ``@{command (HOL) + "function"}~@{text "(sequential)"}'', followed by automated proof attempts + regarding pattern matching and termination. See @{cite + "isabelle-function"} for further details. + + \item @{command (HOL) "termination"}~@{text f} commences a termination + proof for the previously defined function @{text f}. If this is omitted, + the command refers to the most recent function definition. After the proof + is closed, the recursive equations and the induction principle is + established. + + \item @{command (HOL) "fun_cases"} generates specialized elimination rules + for function equations. It expects one or more function equations and + produces rules that eliminate the given equalities, following the cases given in the function definition. + \end{description} Recursive definitions introduced by the @{command (HOL) "function"} - command accommodate reasoning by induction (cf.\ @{method induct}): - rule @{text "f.induct"} refers to a specific induction rule, with - parameters named according to the user-specified equations. Cases - are numbered starting from 1. For @{command (HOL) "primrec"}, the - induction principle coincides with structural recursion on the - datatype where the recursion is carried out. - - The equations provided by these packages may be referred later as - theorem list @{text "f.simps"}, where @{text f} is the (collective) - name of the functions defined. Individual equations may be named - explicitly as well. - - The @{command (HOL) "function"} command accepts the following - options. + command accommodate reasoning by induction (cf.\ @{method induct}): rule + @{text "f.induct"} refers to a specific induction rule, with parameters + named according to the user-specified equations. Cases are numbered + starting from 1. For @{command (HOL) "primrec"}, the induction principle + coincides with structural recursion on the datatype where the recursion is + carried out. + + The equations provided by these packages may be referred later as theorem + list @{text "f.simps"}, where @{text f} is the (collective) name of the + functions defined. Individual equations may be named explicitly as well. + + The @{command (HOL) "function"} command accepts the following options. \begin{description} \item @{text sequential} enables a preprocessor which disambiguates - overlapping patterns by making them mutually disjoint. Earlier - equations take precedence over later ones. This allows to give the - specification in a format very similar to functional programming. - Note that the resulting simplification and induction rules - correspond to the transformed specification, not the one given - originally. This usually means that each equation given by the user - may result in several theorems. Also note that this automatic - transformation only works for ML-style datatype patterns. - - \item @{text domintros} enables the automated generation of - introduction rules for the domain predicate. While mostly not - needed, they can be helpful in some proofs about partial functions. + overlapping patterns by making them mutually disjoint. Earlier equations + take precedence over later ones. This allows to give the specification in + a format very similar to functional programming. Note that the resulting + simplification and induction rules correspond to the transformed + specification, not the one given originally. This usually means that each + equation given by the user may result in several theorems. Also note that + this automatic transformation only works for ML-style datatype patterns. + + \item @{text domintros} enables the automated generation of introduction + rules for the domain predicate. While mostly not needed, they can be + helpful in some proofs about partial functions. \end{description} \ + subsubsection \Example: evaluation of expressions\ -text \Subsequently, we define mutual datatypes for arithmetic and - boolean expressions, and use @{command primrec} for evaluation - functions that follow the same recursive structure.\ +text \Subsequently, we define mutual datatypes for arithmetic and boolean + expressions, and use @{command primrec} for evaluation functions that + follow the same recursive structure.\ (*<*)experiment begin(*>*) datatype 'a aexp = @@ -413,13 +414,13 @@ text \Since the value of an expression depends on the value of its variables, the functions @{const evala} and @{const evalb} take an - additional parameter, an \emph{environment} that maps variables to - their values. - - \medskip Substitution on expressions can be defined similarly. The - mapping @{text f} of type @{typ "'a \ 'a aexp"} given as a - parameter is lifted canonically on the types @{typ "'a aexp"} and - @{typ "'a bexp"}, respectively. + additional parameter, an \emph{environment} that maps variables to their + values. + + \medskip Substitution on expressions can be defined similarly. The mapping + @{text f} of type @{typ "'a \ 'a aexp"} given as a parameter is lifted + canonically on the types @{typ "'a aexp"} and @{typ "'a bexp"}, + respectively. \ primrec substa :: "('a \ 'b aexp) \ 'a aexp \ 'b aexp" @@ -434,10 +435,10 @@ | "substb f (And b1 b2) = And (substb f b1) (substb f b2)" | "substb f (Neg b) = Neg (substb f b)" -text \In textbooks about semantics one often finds substitution - theorems, which express the relationship between substitution and - evaluation. For @{typ "'a aexp"} and @{typ "'a bexp"}, we can prove - such a theorem by mutual induction, followed by simplification. +text \In textbooks about semantics one often finds substitution theorems, + which express the relationship between substitution and evaluation. For + @{typ "'a aexp"} and @{typ "'a bexp"}, we can prove such a theorem by + mutual induction, followed by simplification. \ lemma subst_one: @@ -487,9 +488,8 @@ subsubsection \Example: a map function for infinitely branching trees\ -text \Defining functions on infinitely branching datatypes by - primitive recursion is just as easy. -\ +text \Defining functions on infinitely branching datatypes by primitive + recursion is just as easy.\ (*<*)experiment begin(*>*) datatype 'a tree = Atom 'a | Branch "nat \ 'a tree" @@ -499,11 +499,12 @@ "map_tree f (Atom a) = Atom (f a)" | "map_tree f (Branch ts) = Branch (\x. map_tree f (ts x))" -text \Note that all occurrences of functions such as @{text ts} - above must be applied to an argument. In particular, @{term - "map_tree f \ ts"} is not allowed here.\ - -text \Here is a simple composition lemma for @{term map_tree}:\ +text \Note that all occurrences of functions such as @{text ts} above must + be applied to an argument. In particular, @{term "map_tree f \ ts"} is not + allowed here. + + \medskip Here is a simple composition lemma for @{term map_tree}: +\ lemma "map_tree g (map_tree f t) = map_tree (g \ f) t" by (induct t) simp_all @@ -645,7 +646,6 @@ definitions. \end{description} - \ @@ -745,9 +745,8 @@ subsubsection \Examples\ -text \We define a type of finite sequences, with slightly different - names than the existing @{typ "'a list"} that is already in @{theory - Main}:\ +text \We define a type of finite sequences, with slightly different names + than the existing @{typ "'a list"} that is already in @{theory Main}:\ (*<*)experiment begin(*>*) datatype 'a seq = Empty | Seq 'a "'a seq" @@ -902,33 +901,30 @@ subsection \Record operations\ -text \ - Any record definition of the form presented above produces certain - standard operations. Selectors and updates are provided for any - field, including the improper one ``@{text more}''. There are also - cumulative record constructor functions. To simplify the - presentation below, we assume for now that @{text "(\\<^sub>1, \, - \\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 :: - \\<^sub>1, \, c\<^sub>n :: \\<^sub>n"}. - - \medskip \textbf{Selectors} and \textbf{updates} are available for - any field (including ``@{text more}''): +text \Any record definition of the form presented above produces certain + standard operations. Selectors and updates are provided for any field, + including the improper one ``@{text more}''. There are also cumulative + record constructor functions. To simplify the presentation below, we + assume for now that @{text "(\\<^sub>1, \, \\<^sub>m) t"} is a root record with fields + @{text "c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n"}. + + \medskip \textbf{Selectors} and \textbf{updates} are available for any + field (including ``@{text more}''): \begin{matharray}{lll} @{text "c\<^sub>i"} & @{text "::"} & @{text "\\<^vec>c :: \<^vec>\, \ :: \\ \ \\<^sub>i"} \\ @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\\<^sub>i \ \\<^vec>c :: \<^vec>\, \ :: \\ \ \\<^vec>c :: \<^vec>\, \ :: \\"} \\ \end{matharray} - There is special syntax for application of updates: @{text "r\x := - a\"} abbreviates term @{text "x_update a r"}. Further notation for - repeated updates is also available: @{text "r\x := a\\y := b\\z := - c\"} may be written @{text "r\x := a, y := b, z := c\"}. Note that - because of postfix notation the order of fields shown here is - reverse than in the actual term. Since repeated updates are just - function applications, fields may be freely permuted in @{text "\x - := a, y := b, z := c\"}, as far as logical equality is concerned. - Thus commutativity of independent updates can be proven within the - logic for any two fields, but not as a general theorem. + There is special syntax for application of updates: @{text "r\x := a\"} + abbreviates term @{text "x_update a r"}. Further notation for repeated + updates is also available: @{text "r\x := a\\y := b\\z := c\"} may be + written @{text "r\x := a, y := b, z := c\"}. Note that because of postfix + notation the order of fields shown here is reverse than in the actual + term. Since repeated updates are just function applications, fields may be + freely permuted in @{text "\x := a, y := b, z := c\"}, as far as logical + equality is concerned. Thus commutativity of independent updates can be + proven within the logic for any two fields, but not as a general theorem. \medskip The \textbf{make} operation provides a cumulative record constructor function: @@ -937,15 +933,14 @@ @{text "t.make"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>n \ \\<^vec>c :: \<^vec>\\"} \\ \end{matharray} - \medskip We now reconsider the case of non-root records, which are - derived of some parent. In general, the latter may depend on - another parent as well, resulting in a list of \emph{ancestor - records}. Appending the lists of fields of all ancestors results in - a certain field prefix. The record package automatically takes care - of this by lifting operations over this context of ancestor fields. - Assuming that @{text "(\\<^sub>1, \, \\<^sub>m) t"} has ancestor - fields @{text "b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k"}, - the above record operations will get the following types: + \medskip We now reconsider the case of non-root records, which are derived + of some parent. In general, the latter may depend on another parent as + well, resulting in a list of \emph{ancestor records}. Appending the lists + of fields of all ancestors results in a certain field prefix. The record + package automatically takes care of this by lifting operations over this + context of ancestor fields. Assuming that @{text "(\\<^sub>1, \, \\<^sub>m) t"} has + ancestor fields @{text "b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k"}, the above record + operations will get the following types: \medskip \begin{tabular}{lll} @@ -959,11 +954,11 @@ \medskip \noindent Some further operations address the extension aspect of a - derived record scheme specifically: @{text "t.fields"} produces a - record fragment consisting of exactly the new fields introduced here - (the result may serve as a more part elsewhere); @{text "t.extend"} - takes a fixed record and adds a given more part; @{text - "t.truncate"} restricts a record scheme to a fixed record. + derived record scheme specifically: @{text "t.fields"} produces a record + fragment consisting of exactly the new fields introduced here (the result + may serve as a more part elsewhere); @{text "t.extend"} takes a fixed + record and adds a given more part; @{text "t.truncate"} restricts a record + scheme to a fixed record. \medskip \begin{tabular}{lll} @@ -974,8 +969,8 @@ \end{tabular} \medskip - \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide - for root records. + \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide for + root records. \ @@ -989,41 +984,40 @@ \begin{enumerate} - \item Standard conversions for selectors or updates applied to - record constructor terms are made part of the default Simplifier - context; thus proofs by reduction of basic operations merely require - the @{method simp} method without further arguments. These rules - are available as @{text "t.simps"}, too. - - \item Selectors applied to updated records are automatically reduced - by an internal simplification procedure, which is also part of the - standard Simplifier setup. - - \item Inject equations of a form analogous to @{prop "(x, y) = (x', - y') \ x = x' \ y = y'"} are declared to the Simplifier and Classical - Reasoner as @{attribute iff} rules. These rules are available as - @{text "t.iffs"}. - - \item The introduction rule for record equality analogous to @{text - "x r = x r' \ y r = y r' \ \ r = r'"} is declared to the Simplifier, - and as the basic rule context as ``@{attribute intro}@{text "?"}''. - The rule is called @{text "t.equality"}. + \item Standard conversions for selectors or updates applied to record + constructor terms are made part of the default Simplifier context; thus + proofs by reduction of basic operations merely require the @{method simp} + method without further arguments. These rules are available as @{text + "t.simps"}, too. + + \item Selectors applied to updated records are automatically reduced by an + internal simplification procedure, which is also part of the standard + Simplifier setup. + + \item Inject equations of a form analogous to @{prop "(x, y) = (x', y') \ + x = x' \ y = y'"} are declared to the Simplifier and Classical Reasoner as + @{attribute iff} rules. These rules are available as @{text "t.iffs"}. + + \item The introduction rule for record equality analogous to @{text "x r = + x r' \ y r = y r' \ \ r = r'"} is declared to the Simplifier, and as the + basic rule context as ``@{attribute intro}@{text "?"}''. The rule is + called @{text "t.equality"}. \item Representations of arbitrary record expressions as canonical constructor terms are provided both in @{method cases} and @{method induct} format (cf.\ the generic proof methods of the same name, - \secref{sec:cases-induct}). Several variations are available, for - fixed records, record schemes, more parts etc. - - The generic proof methods are sufficiently smart to pick the most - sensible rule according to the type of the indicated record - expression: users just need to apply something like ``@{text "(cases - r)"}'' to a certain proof problem. - - \item The derived record operations @{text "t.make"}, @{text - "t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not} - treated automatically, but usually need to be expanded by hand, - using the collective fact @{text "t.defs"}. + \secref{sec:cases-induct}). Several variations are available, for fixed + records, record schemes, more parts etc. + + The generic proof methods are sufficiently smart to pick the most sensible + rule according to the type of the indicated record expression: users just + need to apply something like ``@{text "(cases r)"}'' to a certain proof + problem. + + \item The derived record operations @{text "t.make"}, @{text "t.fields"}, + @{text "t.extend"}, @{text "t.truncate"} are \emph{not} treated + automatically, but usually need to be expanded by hand, using the + collective fact @{text "t.defs"}. \end{enumerate} \ @@ -1033,6 +1027,7 @@ text \See @{file "~~/src/HOL/ex/Records.thy"}, for example.\ + section \Typedef axiomatization \label{sec:hol-typedef}\ text \ @@ -1187,30 +1182,28 @@ \begin{description} - \item @{command (HOL) "functor"}~@{text "prefix: m"} allows to - prove and register properties about the functorial structure of type - constructors. These properties then can be used by other packages - to deal with those type constructors in certain type constructions. - Characteristic theorems are noted in the current local theory. By - default, they are prefixed with the base name of the type - constructor, an explicit prefix can be given alternatively. + \item @{command (HOL) "functor"}~@{text "prefix: m"} allows to prove and + register properties about the functorial structure of type constructors. + These properties then can be used by other packages to deal with those + type constructors in certain type constructions. Characteristic theorems + are noted in the current local theory. By default, they are prefixed with + the base name of the type constructor, an explicit prefix can be given + alternatively. The given term @{text "m"} is considered as \emph{mapper} for the - corresponding type constructor and must conform to the following - type pattern: + corresponding type constructor and must conform to the following type + pattern: \begin{matharray}{lll} @{text "m"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>k \ (\<^vec>\\<^sub>n) t \ (\<^vec>\\<^sub>n) t"} \\ \end{matharray} - \noindent where @{text t} is the type constructor, @{text - "\<^vec>\\<^sub>n"} and @{text "\<^vec>\\<^sub>n"} are distinct - type variables free in the local theory and @{text "\\<^sub>1"}, - \ldots, @{text "\\<^sub>k"} is a subsequence of @{text "\\<^sub>1 \ - \\<^sub>1"}, @{text "\\<^sub>1 \ \\<^sub>1"}, \ldots, - @{text "\\<^sub>n \ \\<^sub>n"}, @{text "\\<^sub>n \ - \\<^sub>n"}. + \noindent where @{text t} is the type constructor, @{text "\<^vec>\\<^sub>n"} + and @{text "\<^vec>\\<^sub>n"} are distinct type variables free in the local + theory and @{text "\\<^sub>1"}, \ldots, @{text "\\<^sub>k"} is a subsequence of @{text + "\\<^sub>1 \ \\<^sub>1"}, @{text "\\<^sub>1 \ \\<^sub>1"}, \ldots, @{text "\\<^sub>n \ \\<^sub>n"}, @{text + "\\<^sub>n \ \\<^sub>n"}. \end{description} \