--- a/src/Doc/IsarRef/HOL_Specific.thy Sat Apr 05 17:52:29 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2677 +0,0 @@
-theory HOL_Specific
-imports Base Main "~~/src/HOL/Library/Old_Recdef" "~~/src/Tools/Adhoc_Overloading"
-begin
-
-chapter {* Higher-Order Logic *}
-
-text {* Isabelle/HOL is based on Higher-Order Logic, a polymorphic
- version of Church's Simple Theory of Types. HOL can be best
- understood as a simply-typed version of classical set theory. The
- logic was first implemented in Gordon's HOL system
- \cite{mgordon-hol}. It extends Church's original logic
- \cite{church40} by explicit type variables (naive polymorphism) and
- a sound axiomatization scheme for new types based on subsets of
- existing types.
-
- Andrews's book \cite{andrews86} is a full description of the
- original Church-style higher-order logic, with proofs of correctness
- and completeness wrt.\ certain set-theoretic interpretations. The
- particular extensions of Gordon-style HOL are explained semantically
- in two chapters of the 1993 HOL book \cite{pitts93}.
-
- Experience with HOL over decades has demonstrated that higher-order
- logic is widely applicable in many areas of mathematics and computer
- science. In a sense, Higher-Order Logic is simpler than First-Order
- Logic, because there are fewer restrictions and special cases. Note
- that HOL is \emph{weaker} than FOL with axioms for ZF set theory,
- which is traditionally considered the standard foundation of regular
- mathematics, but for most applications this does not matter. If you
- prefer ML to Lisp, you will probably prefer HOL to ZF.
-
- \medskip The syntax of HOL follows @{text "\<lambda>"}-calculus and
- functional programming. Function application is curried. To apply
- the function @{text f} of type @{text "\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"} to the
- arguments @{text a} and @{text b} in HOL, you simply write @{text "f
- a b"} (as in ML or Haskell). There is no ``apply'' operator; the
- existing application of the Pure @{text "\<lambda>"}-calculus is re-used.
- Note that in HOL @{text "f (a, b)"} means ``@{text "f"} applied to
- the pair @{text "(a, b)"} (which is notation for @{text "Pair a
- b"}). The latter typically introduces extra formal efforts that can
- be avoided by currying functions by default. Explicit tuples are as
- infrequent in HOL formalizations as in good ML or Haskell programs.
-
- \medskip Isabelle/HOL has a distinct feel, compared to other
- object-logics like Isabelle/ZF. It identifies object-level types
- with meta-level types, taking advantage of the default
- type-inference mechanism of Isabelle/Pure. HOL fully identifies
- object-level functions with meta-level functions, with native
- abstraction and application.
-
- These identifications allow Isabelle to support HOL particularly
- nicely, but they also mean that HOL requires some sophistication
- from the user. In particular, an understanding of Hindley-Milner
- type-inference with type-classes, which are both used extensively in
- the standard libraries and applications. Beginners can set
- @{attribute show_types} or even @{attribute show_sorts} to get more
- explicit information about the result of type-inference. *}
-
-
-chapter {* Derived specification elements *}
-
-section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "print_inductives"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{attribute_def (HOL) mono} & : & @{text attribute} \\
- \end{matharray}
-
- An \emph{inductive definition} specifies the least predicate or set
- @{text R} closed under given rules: applying a rule to elements of
- @{text R} yields a result within @{text R}. For example, a
- structural operational semantics is an inductive definition of an
- evaluation relation.
-
- Dually, a \emph{coinductive definition} specifies the greatest
- predicate or set @{text R} that is consistent with given rules:
- every element of @{text R} can be seen as arising by applying a rule
- to elements of @{text R}. An important example is using
- bisimulation relations to formalise equivalence of processes and
- infinite data structures.
-
- Both inductive and coinductive definitions are based on the
- Knaster-Tarski fixed-point theorem for complete lattices. The
- collection of introduction rules given by the user determines a
- functor on subsets of set-theoretic relations. The required
- monotonicity of the recursion scheme is proven as a prerequisite to
- the fixed-point definition and the resulting consequences. This
- works by pushing inclusion through logical connectives and any other
- operator that might be wrapped around recursive occurrences of the
- defined relation: there must be a monotonicity theorem of the form
- @{text "A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B"}, for each premise @{text "\<M> R t"} in an
- introduction rule. The default rule declarations of Isabelle/HOL
- already take care of most common situations.
-
- @{rail \<open>
- (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
- @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
- @{syntax target}? \<newline>
- @{syntax "fixes"} (@'for' @{syntax "fixes"})? (@'where' clauses)? \<newline>
- (@'monos' @{syntax thmrefs})?
- ;
- clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
- ;
- @@{attribute (HOL) mono} (() | 'add' | 'del')
- \<close>}
-
- \begin{description}
-
- \item @{command (HOL) "inductive"} and @{command (HOL)
- "coinductive"} define (co)inductive predicates from the introduction
- rules.
-
- The propositions given as @{text "clauses"} in the @{keyword
- "where"} part are either rules of the usual @{text "\<And>/\<Longrightarrow>"} format
- (with arbitrary nesting), or equalities using @{text "\<equiv>"}. The
- latter specifies extra-logical abbreviations in the sense of
- @{command_ref abbreviation}. Introducing abstract syntax
- simultaneously with the actual introduction rules is occasionally
- useful for complex specifications.
-
- The optional @{keyword "for"} part contains a list of parameters of
- the (co)inductive predicates that remain fixed throughout the
- definition, in contrast to arguments of the relation that may vary
- in each occurrence within the given @{text "clauses"}.
-
- The optional @{keyword "monos"} declaration contains additional
- \emph{monotonicity theorems}, which are required for each operator
- applied to a recursive set in the introduction rules.
-
- \item @{command (HOL) "inductive_set"} and @{command (HOL)
- "coinductive_set"} are wrappers for to the previous commands for
- native HOL predicates. This allows to define (co)inductive sets,
- where multiple arguments are simulated via tuples.
-
- \item @{command "print_inductives"} prints (co)inductive definitions and
- monotonicity rules.
-
- \item @{attribute (HOL) mono} declares monotonicity rules in the
- context. These rule are involved in the automated monotonicity
- proof of the above inductive and coinductive definitions.
-
- \end{description}
-*}
-
-
-subsection {* Derived rules *}
-
-text {* A (co)inductive definition of @{text R} provides the following
- main theorems:
-
- \begin{description}
-
- \item @{text R.intros} is the list of introduction rules as proven
- theorems, for the recursive predicates (or sets). The rules are
- also available individually, using the names given them in the
- theory file;
-
- \item @{text R.cases} is the case analysis (or elimination) rule;
-
- \item @{text R.induct} or @{text R.coinduct} is the (co)induction
- rule;
-
- \item @{text R.simps} is the equation unrolling the fixpoint of the
- predicate one step.
-
- \end{description}
-
- When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are
- defined simultaneously, the list of introduction rules is called
- @{text "R\<^sub>1_\<dots>_R\<^sub>n.intros"}, the case analysis rules are
- called @{text "R\<^sub>1.cases, \<dots>, R\<^sub>n.cases"}, and the list
- of mutual induction rules is called @{text
- "R\<^sub>1_\<dots>_R\<^sub>n.inducts"}.
-*}
-
-
-subsection {* Monotonicity theorems *}
-
-text {* The context maintains a default set of theorems that are used
- in monotonicity proofs. New rules can be declared via the
- @{attribute (HOL) mono} attribute. See the main Isabelle/HOL
- sources for some examples. The general format of such monotonicity
- theorems is as follows:
-
- \begin{itemize}
-
- \item Theorems of the form @{text "A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B"}, for proving
- monotonicity of inductive definitions whose introduction rules have
- premises involving terms such as @{text "\<M> R t"}.
-
- \item Monotonicity theorems for logical operators, which are of the
- general form @{text "(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>"}. For example, in
- the case of the operator @{text "\<or>"}, the corresponding theorem is
- \[
- \infer{@{text "P\<^sub>1 \<or> P\<^sub>2 \<longrightarrow> Q\<^sub>1 \<or> Q\<^sub>2"}}{@{text "P\<^sub>1 \<longrightarrow> Q\<^sub>1"} & @{text "P\<^sub>2 \<longrightarrow> Q\<^sub>2"}}
- \]
-
- \item De Morgan style equations for reasoning about the ``polarity''
- of expressions, e.g.
- \[
- @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad
- @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}
- \]
-
- \item Equations for reducing complex operators to more primitive
- ones whose monotonicity can easily be proved, e.g.
- \[
- @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad
- @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}
- \]
-
- \end{itemize}
-*}
-
-subsubsection {* Examples *}
-
-text {* The finite powerset operator can be defined inductively like this: *}
-
-inductive_set Fin :: "'a set \<Rightarrow> 'a set set" for A :: "'a set"
-where
- empty: "{} \<in> Fin A"
-| insert: "a \<in> A \<Longrightarrow> B \<in> Fin A \<Longrightarrow> insert a B \<in> Fin A"
-
-text {* The accessible part of a relation is defined as follows: *}
-
-inductive acc :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
- for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
-where acc: "(\<And>y. y \<prec> x \<Longrightarrow> acc r y) \<Longrightarrow> acc r x"
-
-text {* Common logical connectives can be easily characterized as
-non-recursive inductive definitions with parameters, but without
-arguments. *}
-
-inductive AND for A B :: bool
-where "A \<Longrightarrow> B \<Longrightarrow> AND A B"
-
-inductive OR for A B :: bool
-where "A \<Longrightarrow> OR A B"
- | "B \<Longrightarrow> OR A B"
-
-inductive EXISTS for B :: "'a \<Rightarrow> bool"
-where "B a \<Longrightarrow> EXISTS B"
-
-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} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOL) "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def (HOL) "fun"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def (HOL) "function"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- @{command_def (HOL) "termination"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- @{command_def (HOL) "fun_cases"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- \end{matharray}
-
- @{rail \<open>
- @@{command (HOL) primrec} @{syntax target}? @{syntax "fixes"} @'where' equations
- ;
- (@@{command (HOL) fun} | @@{command (HOL) function}) @{syntax target}? functionopts?
- @{syntax "fixes"} \<newline> @'where' equations
- ;
-
- equations: (@{syntax thmdecl}? @{syntax prop} + '|')
- ;
- functionopts: '(' (('sequential' | 'domintros') + ',') ')'
- ;
- @@{command (HOL) termination} @{syntax term}?
- ;
- @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')
- \<close>}
-
- \begin{description}
-
- \item @{command (HOL) "primrec"} defines primitive recursive
- functions over datatypes (see also @{command_ref (HOL) datatype} and
- @{command_ref (HOL) rep_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 \<dots> x\<^sub>m (C y\<^sub>1 \<dots> y\<^sub>k) z\<^sub>1 \<dots> 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 \<dots> y\<^sub>i \<dots>"} 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
- 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.
-
- \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.
-
- \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. *}
-
-datatype 'a aexp =
- IF "'a bexp" "'a aexp" "'a aexp"
- | Sum "'a aexp" "'a aexp"
- | Diff "'a aexp" "'a aexp"
- | Var 'a
- | Num nat
-and 'a bexp =
- Less "'a aexp" "'a aexp"
- | And "'a bexp" "'a bexp"
- | Neg "'a bexp"
-
-
-text {* \medskip Evaluation of arithmetic and boolean expressions *}
-
-primrec evala :: "('a \<Rightarrow> nat) \<Rightarrow> 'a aexp \<Rightarrow> nat"
- and evalb :: "('a \<Rightarrow> nat) \<Rightarrow> 'a bexp \<Rightarrow> bool"
-where
- "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
-| "evala env (Sum a1 a2) = evala env a1 + evala env a2"
-| "evala env (Diff a1 a2) = evala env a1 - evala env a2"
-| "evala env (Var v) = env v"
-| "evala env (Num n) = n"
-| "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
-| "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
-| "evalb env (Neg b) = (\<not> evalb env b)"
-
-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 \<Rightarrow> 'a aexp"} given as a
- parameter is lifted canonically on the types @{typ "'a aexp"} and
- @{typ "'a bexp"}, respectively.
-*}
-
-primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
- and substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp"
-where
- "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
-| "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
-| "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
-| "substa f (Var v) = f v"
-| "substa f (Num n) = Num n"
-| "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
-| "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.
-*}
-
-lemma subst_one:
- "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
- "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
- by (induct a and b) simp_all
-
-lemma subst_all:
- "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
- "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
- by (induct a and b) simp_all
-
-
-subsubsection {* Example: a substitution function for terms *}
-
-text {* Functions on datatypes with nested recursion are also defined
- by mutual primitive recursion. *}
-
-datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
-
-text {* A substitution function on type @{typ "('a, 'b) term"} can be
- defined as follows, by working simultaneously on @{typ "('a, 'b)
- term list"}: *}
-
-primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term" and
- subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
-where
- "subst_term f (Var a) = f a"
-| "subst_term f (App b ts) = App b (subst_term_list f ts)"
-| "subst_term_list f [] = []"
-| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
-
-text {* The recursion scheme follows the structure of the unfolded
- definition of type @{typ "('a, 'b) term"}. To prove properties of this
- substitution function, mutual induction is needed:
-*}
-
-lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)" and
- "subst_term_list (subst_term f1 \<circ> f2) ts = subst_term_list f1 (subst_term_list f2 ts)"
- by (induct t and ts) simp_all
-
-
-subsubsection {* Example: a map function for infinitely branching trees *}
-
-text {* Defining functions on infinitely branching datatypes by
- primitive recursion is just as easy.
-*}
-
-datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
-
-primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
-where
- "map_tree f (Atom a) = Atom (f a)"
-| "map_tree f (Branch ts) = Branch (\<lambda>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 \<circ> ts"} is not allowed here. *}
-
-text {* Here is a simple composition lemma for @{term map_tree}: *}
-
-lemma "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
- by (induct t) simp_all
-
-
-subsection {* Proof methods related to recursive definitions *}
-
-text {*
- \begin{matharray}{rcl}
- @{method_def (HOL) pat_completeness} & : & @{text method} \\
- @{method_def (HOL) relation} & : & @{text method} \\
- @{method_def (HOL) lexicographic_order} & : & @{text method} \\
- @{method_def (HOL) size_change} & : & @{text method} \\
- @{method_def (HOL) induction_schema} & : & @{text method} \\
- \end{matharray}
-
- @{rail \<open>
- @@{method (HOL) relation} @{syntax term}
- ;
- @@{method (HOL) lexicographic_order} (@{syntax clasimpmod} * )
- ;
- @@{method (HOL) size_change} ( orders (@{syntax clasimpmod} * ) )
- ;
- @@{method (HOL) induction_schema}
- ;
- orders: ( 'max' | 'min' | 'ms' ) *
- \<close>}
-
- \begin{description}
-
- \item @{method (HOL) pat_completeness} is a specialized method to
- solve goals regarding the completeness of pattern matching, as
- required by the @{command (HOL) "function"} package (cf.\
- \cite{isabelle-function}).
-
- \item @{method (HOL) relation}~@{text R} introduces a termination
- proof using the relation @{text R}. The resulting proof state will
- contain goals expressing that @{text R} is wellfounded, and that the
- arguments of recursive calls decrease with respect to @{text R}.
- Usually, this method is used as the initial proof step of manual
- termination proofs.
-
- \item @{method (HOL) "lexicographic_order"} attempts a fully
- automated termination proof by searching for a lexicographic
- combination of size measures on the arguments of the function. The
- method accepts the same arguments as the @{method auto} method,
- which it uses internally to prove local descents. The @{syntax
- clasimpmod} modifiers are accepted (as for @{method auto}).
-
- In case of failure, extensive information is printed, which can help
- to analyse the situation (cf.\ \cite{isabelle-function}).
-
- \item @{method (HOL) "size_change"} also works on termination goals,
- using a variation of the size-change principle, together with a
- graph decomposition technique (see \cite{krauss_phd} for details).
- Three kinds of orders are used internally: @{text max}, @{text min},
- and @{text ms} (multiset), which is only available when the theory
- @{text Multiset} is loaded. When no order kinds are given, they are
- tried in order. The search for a termination proof uses SAT solving
- internally.
-
- For local descent proofs, the @{syntax clasimpmod} modifiers are
- accepted (as for @{method auto}).
-
- \item @{method (HOL) induction_schema} derives user-specified
- induction rules from well-founded induction and completeness of
- patterns. This factors out some operations that are done internally
- by the function package and makes them available separately. See
- @{file "~~/src/HOL/ex/Induction_Schema.thy"} for examples.
-
- \end{description}
-*}
-
-
-subsection {* Functions with explicit partiality *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOL) "partial_function"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\
- \end{matharray}
-
- @{rail \<open>
- @@{command (HOL) partial_function} @{syntax target}?
- '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
- @'where' @{syntax thmdecl}? @{syntax prop}
- \<close>}
-
- \begin{description}
-
- \item @{command (HOL) "partial_function"}~@{text "(mode)"} defines
- recursive functions based on fixpoints in complete partial
- orders. No termination proof is required from the user or
- constructed internally. Instead, the possibility of non-termination
- is modelled explicitly in the result type, which contains an
- explicit bottom element.
-
- Pattern matching and mutual recursion are currently not supported.
- Thus, the specification consists of a single function described by a
- single recursive equation.
-
- There are no fixed syntactic restrictions on the body of the
- function, but the induced functional must be provably monotonic
- wrt.\ the underlying order. The monotonicity proof is performed
- internally, and the definition is rejected when it fails. The proof
- can be influenced by declaring hints using the
- @{attribute (HOL) partial_function_mono} attribute.
-
- The mandatory @{text mode} argument specifies the mode of operation
- of the command, which directly corresponds to a complete partial
- order on the result type. By default, the following modes are
- defined:
-
- \begin{description}
-
- \item @{text option} defines functions that map into the @{type
- option} type. Here, the value @{term None} is used to model a
- non-terminating computation. Monotonicity requires that if @{term
- None} is returned by a recursive call, then the overall result must
- also be @{term None}. This is best achieved through the use of the
- monadic operator @{const "Option.bind"}.
-
- \item @{text tailrec} defines functions with an arbitrary result
- type and uses the slightly degenerated partial order where @{term
- "undefined"} is the bottom element. Now, monotonicity requires that
- if @{term undefined} is returned by a recursive call, then the
- overall result must also be @{term undefined}. In practice, this is
- only satisfied when each recursive call is a tail call, whose result
- is directly returned. Thus, this mode of operation allows the
- definition of arbitrary tail-recursive functions.
-
- \end{description}
-
- Experienced users may define new modes by instantiating the locale
- @{const "partial_function_definitions"} appropriately.
-
- \item @{attribute (HOL) partial_function_mono} declares rules for
- use in the internal monotonicity proofs of partial function
- definitions.
-
- \end{description}
-
-*}
-
-
-subsection {* Old-style recursive function definitions (TFL) *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOL) "recdef"} & : & @{text "theory \<rightarrow> theory)"} \\
- @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
- \end{matharray}
-
- The old TFL commands @{command (HOL) "recdef"} and @{command (HOL)
- "recdef_tc"} for defining recursive are mostly obsolete; @{command
- (HOL) "function"} or @{command (HOL) "fun"} should be used instead.
-
- @{rail \<open>
- @@{command (HOL) recdef} ('(' @'permissive' ')')? \<newline>
- @{syntax name} @{syntax term} (@{syntax prop} +) hints?
- ;
- recdeftc @{syntax thmdecl}? tc
- ;
- hints: '(' @'hints' ( recdefmod * ) ')'
- ;
- recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf')
- (() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod}
- ;
- tc: @{syntax nameref} ('(' @{syntax nat} ')')?
- \<close>}
-
- \begin{description}
-
- \item @{command (HOL) "recdef"} defines general well-founded
- recursive functions (using the TFL package), see also
- \cite{isabelle-HOL}. The ``@{text "(permissive)"}'' option tells
- TFL to recover from failed proof attempts, returning unfinished
- results. The @{text recdef_simp}, @{text recdef_cong}, and @{text
- recdef_wf} hints refer to auxiliary rules to be used in the internal
- automated proof process of TFL. Additional @{syntax clasimpmod}
- declarations may be given to tune the context of the Simplifier
- (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\
- \secref{sec:classical}).
-
- \item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the
- proof for leftover termination condition number @{text i} (default
- 1) as generated by a @{command (HOL) "recdef"} definition of
- constant @{text c}.
-
- Note that in most cases, @{command (HOL) "recdef"} is able to finish
- its internal proofs without manual intervention.
-
- \end{description}
-
- \medskip Hints for @{command (HOL) "recdef"} may be also declared
- globally, using the following attributes.
-
- \begin{matharray}{rcl}
- @{attribute_def (HOL) recdef_simp} & : & @{text attribute} \\
- @{attribute_def (HOL) recdef_cong} & : & @{text attribute} \\
- @{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\
- \end{matharray}
-
- @{rail \<open>
- (@@{attribute (HOL) recdef_simp} | @@{attribute (HOL) recdef_cong} |
- @@{attribute (HOL) recdef_wf}) (() | 'add' | 'del')
- \<close>}
-*}
-
-
-section {* Datatypes \label{sec:hol-datatype} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOL) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
- \end{matharray}
-
- @{rail \<open>
- @@{command (HOL) datatype} (spec + @'and')
- ;
- @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
- ;
-
- spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|')
- ;
- cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
- \<close>}
-
- \begin{description}
-
- \item @{command (HOL) "datatype"} defines inductive datatypes in
- HOL.
-
- \item @{command (HOL) "rep_datatype"} represents existing types as
- datatypes.
-
- For foundational reasons, some basic types such as @{typ nat}, @{typ
- "'a \<times> 'b"}, @{typ "'a + 'b"}, @{typ bool} and @{typ unit} are
- introduced by more primitive means using @{command_ref typedef}. To
- recover the rich infrastructure of @{command datatype} (e.g.\ rules
- for @{method cases} and @{method induct} and the primitive recursion
- combinators), such types may be represented as actual datatypes
- later. This is done by specifying the constructors of the desired
- type, and giving a proof of the induction rule, distinctness and
- injectivity of constructors.
-
- For example, see @{file "~~/src/HOL/Sum_Type.thy"} for the
- representation of the primitive sum type as fully-featured datatype.
-
- \end{description}
-
- The generated rules for @{method induct} and @{method cases} provide
- case names according to the given constructors, while parameters are
- named after the types (see also \secref{sec:cases-induct}).
-
- See \cite{isabelle-HOL} for more details on datatypes, but beware of
- the old-style theory syntax being used there! Apart from proper
- proof methods for case-analysis and induction, there are also
- emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
- induct_tac} available, see \secref{sec:hol-induct-tac}; these admit
- to refer directly to the internal structure of subgoals (including
- internally bound parameters).
-*}
-
-
-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}: *}
-
-datatype 'a seq = Empty | Seq 'a "'a seq"
-
-text {* We can now prove some simple lemma by structural induction: *}
-
-lemma "Seq x xs \<noteq> xs"
-proof (induct xs arbitrary: x)
- case Empty
- txt {* This case can be proved using the simplifier: the freeness
- properties of the datatype are already declared as @{attribute
- simp} rules. *}
- show "Seq x Empty \<noteq> Empty"
- by simp
-next
- case (Seq y ys)
- txt {* The step case is proved similarly. *}
- show "Seq x (Seq y ys) \<noteq> Seq y ys"
- using `Seq y ys \<noteq> ys` by simp
-qed
-
-text {* Here is a more succinct version of the same proof: *}
-
-lemma "Seq x xs \<noteq> xs"
- by (induct xs arbitrary: x) simp_all
-
-
-section {* Records \label{sec:hol-record} *}
-
-text {*
- In principle, records merely generalize the concept of tuples, where
- components may be addressed by labels instead of just position. The
- logical infrastructure of records in Isabelle/HOL is slightly more
- advanced, though, supporting truly extensible record schemes. This
- admits operations that are polymorphic with respect to record
- extension, yielding ``object-oriented'' effects like (single)
- inheritance. See also \cite{NaraschewskiW-TPHOLs98} for more
- details on object-oriented verification and record subtyping in HOL.
-*}
-
-
-subsection {* Basic concepts *}
-
-text {*
- Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records
- at the level of terms and types. The notation is as follows:
-
- \begin{center}
- \begin{tabular}{l|l|l}
- & record terms & record types \\ \hline
- fixed & @{text "\<lparr>x = a, y = b\<rparr>"} & @{text "\<lparr>x :: A, y :: B\<rparr>"} \\
- schematic & @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} &
- @{text "\<lparr>x :: A, y :: B, \<dots> :: M\<rparr>"} \\
- \end{tabular}
- \end{center}
-
- \noindent The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text
- "(| x = a |)"}.
-
- A fixed record @{text "\<lparr>x = a, y = b\<rparr>"} has field @{text x} of value
- @{text a} and field @{text y} of value @{text b}. The corresponding
- type is @{text "\<lparr>x :: A, y :: B\<rparr>"}, assuming that @{text "a :: A"}
- and @{text "b :: B"}.
-
- A record scheme like @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} contains fields
- @{text x} and @{text y} as before, but also possibly further fields
- as indicated by the ``@{text "\<dots>"}'' notation (which is actually part
- of the syntax). The improper field ``@{text "\<dots>"}'' of a record
- scheme is called the \emph{more part}. Logically it is just a free
- variable, which is occasionally referred to as ``row variable'' in
- the literature. The more part of a record scheme may be
- instantiated by zero or more further components. For example, the
- previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z =
- c, \<dots> = m'\<rparr>"}, where @{text m'} refers to a different more part.
- Fixed records are special instances of record schemes, where
- ``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"}
- element. In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation
- for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}.
-
- \medskip Two key observations make extensible records in a simply
- typed language like HOL work out:
-
- \begin{enumerate}
-
- \item the more part is internalized, as a free term or type
- variable,
-
- \item field names are externalized, they cannot be accessed within
- the logic as first-class values.
-
- \end{enumerate}
-
- \medskip In Isabelle/HOL record types have to be defined explicitly,
- fixing their field names and types, and their (optional) parent
- record. Afterwards, records may be formed using above syntax, while
- obeying the canonical order of fields as given by their declaration.
- The record package provides several standard operations like
- selectors and updates. The common setup for various generic proof
- tools enable succinct reasoning patterns. See also the Isabelle/HOL
- tutorial \cite{isabelle-hol-book} for further instructions on using
- records in practice.
-*}
-
-
-subsection {* Record specifications *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOL) "record"} & : & @{text "theory \<rightarrow> theory"} \\
- \end{matharray}
-
- @{rail \<open>
- @@{command (HOL) record} @{syntax typespec_sorts} '=' \<newline>
- (@{syntax type} '+')? (constdecl +)
- ;
- constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
- \<close>}
-
- \begin{description}
-
- \item @{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1
- \<dots> c\<^sub>n :: \<sigma>\<^sub>n"} defines extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"},
- derived from the optional parent record @{text "\<tau>"} by adding new
- field components @{text "c\<^sub>i :: \<sigma>\<^sub>i"} etc.
-
- The type variables of @{text "\<tau>"} and @{text "\<sigma>\<^sub>i"} need to be
- covered by the (distinct) parameters @{text "\<alpha>\<^sub>1, \<dots>,
- \<alpha>\<^sub>m"}. Type constructor @{text t} has to be new, while @{text
- \<tau>} needs to specify an instance of an existing record type. At
- least one new field @{text "c\<^sub>i"} has to be specified.
- Basically, field names need to belong to a unique record. This is
- not a real restriction in practice, since fields are qualified by
- the record name internally.
-
- The parent record specification @{text \<tau>} is optional; if omitted
- @{text t} becomes a root record. The hierarchy of all records
- declared within a theory context forms a forest structure, i.e.\ a
- set of trees starting with a root record each. There is no way to
- merge multiple parent records!
-
- For convenience, @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} is made a
- type abbreviation for the fixed record type @{text "\<lparr>c\<^sub>1 ::
- \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"}, likewise is @{text
- "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>) t_scheme"} made an abbreviation for
- @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> ::
- \<zeta>\<rparr>"}.
-
- \end{description}
-*}
-
-
-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 "(\<alpha>\<^sub>1, \<dots>,
- \<alpha>\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 ::
- \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^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 "\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
- @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
- \end{matharray}
-
- There is special syntax for application of updates: @{text "r\<lparr>x :=
- a\<rparr>"} abbreviates term @{text "x_update a r"}. Further notation for
- repeated updates is also available: @{text "r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z :=
- c\<rparr>"} may be written @{text "r\<lparr>x := a, y := b, z := c\<rparr>"}. 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 "\<lparr>x
- := a, y := b, z := c\<rparr>"}, 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:
-
- \begin{matharray}{lll}
- @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
- \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 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} has ancestor
- fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"},
- the above record operations will get the following types:
-
- \medskip
- \begin{tabular}{lll}
- @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
- @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow>
- \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
- \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
- @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>
- \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
- \end{tabular}
- \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.
-
- \medskip
- \begin{tabular}{lll}
- @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
- @{text "t.extend"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow>
- \<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
- @{text "t.truncate"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
- \end{tabular}
- \medskip
-
- \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide
- for root records.
-*}
-
-
-subsection {* Derived rules and proof tools *}
-
-text {*
- The record package proves several results internally, declaring
- these facts to appropriate proof tools. This enables users to
- reason about record structures quite conveniently. Assume that
- @{text t} is a record type as specified above.
-
- \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') \<equiv> x = x' \<and> 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' \<Longrightarrow> y r = y r' \<dots> \<Longrightarrow> 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"}.
-
- \end{enumerate}
-*}
-
-
-subsubsection {* Examples *}
-
-text {* See @{file "~~/src/HOL/ex/Records.thy"}, for example. *}
-
-section {* Typedef axiomatization \label{sec:hol-typedef} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- \end{matharray}
-
- A Gordon/HOL-style type definition is a certain axiom scheme that
- identifies a new type with a subset of an existing type. More
- precisely, the new type is defined by exhibiting an existing type
- @{text \<tau>}, a set @{text "A :: \<tau> set"}, and a theorem that proves
- @{prop "\<exists>x. x \<in> A"}. Thus @{text A} is a non-empty subset of @{text
- \<tau>}, and the new type denotes this subset. New functions are
- postulated that establish an isomorphism between the new type and
- the subset. In general, the type @{text \<tau>} may involve type
- variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} which means that the type definition
- produces a type constructor @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} depending on
- those type arguments.
-
- The axiomatization can be considered a ``definition'' in the sense
- of the particular set-theoretic interpretation of HOL
- \cite{pitts93}, where the universe of types is required to be
- downwards-closed wrt.\ arbitrary non-empty subsets. Thus genuinely
- new types introduced by @{command "typedef"} stay within the range
- of HOL models by construction. Note that @{command_ref
- type_synonym} from Isabelle/Pure merely introduces syntactic
- abbreviations, without any logical significance.
-
- @{rail \<open>
- @@{command (HOL) typedef} abs_type '=' rep_set
- ;
- abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
- ;
- rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
- \<close>}
-
- \begin{description}
-
- \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}
- axiomatizes a type definition in the background theory of the
- current context, depending on a non-emptiness result of the set
- @{text A} that needs to be proven here. The set @{text A} may
- contain type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} as specified on the LHS,
- but no term variables.
-
- Even though a local theory specification, the newly introduced type
- constructor cannot depend on parameters or assumptions of the
- context: this is structurally impossible in HOL. In contrast, the
- non-emptiness proof may use local assumptions in unusual situations,
- which could result in different interpretations in target contexts:
- the meaning of the bijection between the representing set @{text A}
- and the new type @{text t} may then change in different application
- contexts.
-
- For @{command (HOL) "typedef"}~@{text "t = A"} the newly introduced
- type @{text t} is accompanied by a pair of morphisms to relate it to
- the representing set over the old type. By default, the injection
- from type to set is called @{text Rep_t} and its inverse @{text
- Abs_t}: An explicit @{keyword (HOL) "morphisms"} specification
- allows to provide alternative names.
-
- The core axiomatization uses the locale predicate @{const
- type_definition} as defined in Isabelle/HOL. Various basic
- consequences of that are instantiated accordingly, re-using the
- locale facts with names derived from the new type constructor. Thus
- the generic @{thm type_definition.Rep} is turned into the specific
- @{text "Rep_t"}, for example.
-
- Theorems @{thm type_definition.Rep}, @{thm
- type_definition.Rep_inverse}, and @{thm type_definition.Abs_inverse}
- provide the most basic characterization as a corresponding
- injection/surjection pair (in both directions). The derived rules
- @{thm type_definition.Rep_inject} and @{thm
- type_definition.Abs_inject} provide a more convenient version of
- injectivity, suitable for automated proof tools (e.g.\ in
- declarations involving @{attribute simp} or @{attribute iff}).
- Furthermore, the rules @{thm type_definition.Rep_cases}~/ @{thm
- type_definition.Rep_induct}, and @{thm type_definition.Abs_cases}~/
- @{thm type_definition.Abs_induct} provide alternative views on
- surjectivity. These rules are already declared as set or type rules
- for the generic @{method cases} and @{method induct} methods,
- respectively.
-
- \end{description}
-
- \begin{warn}
- If you introduce a new type axiomatically, i.e.\ via @{command_ref
- typedecl} and @{command_ref axiomatization}, the minimum requirement
- is that it has a non-empty model, to avoid immediate collapse of the
- HOL logic. Moreover, one needs to demonstrate that the
- interpretation of such free-form axiomatizations can coexist with
- that of the regular @{command_def typedef} scheme, and any extension
- that other people might have introduced elsewhere.
- \end{warn}
-*}
-
-subsubsection {* Examples *}
-
-text {* Type definitions permit the introduction of abstract data
- types in a safe way, namely by providing models based on already
- existing types. Given some abstract axiomatic description @{text P}
- of a type, this involves two steps:
-
- \begin{enumerate}
-
- \item Find an appropriate type @{text \<tau>} and subset @{text A} which
- has the desired properties @{text P}, and make a type definition
- based on this representation.
-
- \item Prove that @{text P} holds for @{text \<tau>} by lifting @{text P}
- from the representation.
-
- \end{enumerate}
-
- You can later forget about the representation and work solely in
- terms of the abstract properties @{text P}.
-
- \medskip The following trivial example pulls a three-element type
- into existence within the formal logical environment of HOL. *}
-
-typedef three = "{(True, True), (True, False), (False, True)}"
- by blast
-
-definition "One = Abs_three (True, True)"
-definition "Two = Abs_three (True, False)"
-definition "Three = Abs_three (False, True)"
-
-lemma three_distinct: "One \<noteq> Two" "One \<noteq> Three" "Two \<noteq> Three"
- by (simp_all add: One_def Two_def Three_def Abs_three_inject)
-
-lemma three_cases:
- fixes x :: three obtains "x = One" | "x = Two" | "x = Three"
- by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
-
-text {* Note that such trivial constructions are better done with
- derived specification mechanisms such as @{command datatype}: *}
-
-datatype three' = One' | Two' | Three'
-
-text {* This avoids re-doing basic definitions and proofs from the
- primitive @{command typedef} above. *}
-
-
-
-section {* Functorial structure of types *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOL) "functor"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
- \end{matharray}
-
- @{rail \<open>
- @@{command (HOL) functor} (@{syntax name} ':')? @{syntax term}
- \<close>}
-
- \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.
-
- The given term @{text "m"} is considered as \emph{mapper} for the
- corresponding type constructor and must conform to the following
- type pattern:
-
- \begin{matharray}{lll}
- @{text "m"} & @{text "::"} &
- @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>k \<Rightarrow> (\<^vec>\<alpha>\<^sub>n) t \<Rightarrow> (\<^vec>\<beta>\<^sub>n) t"} \\
- \end{matharray}
-
- \noindent where @{text t} is the type constructor, @{text
- "\<^vec>\<alpha>\<^sub>n"} and @{text "\<^vec>\<beta>\<^sub>n"} are distinct
- type variables free in the local theory and @{text "\<sigma>\<^sub>1"},
- \ldots, @{text "\<sigma>\<^sub>k"} is a subsequence of @{text "\<alpha>\<^sub>1 \<Rightarrow>
- \<beta>\<^sub>1"}, @{text "\<beta>\<^sub>1 \<Rightarrow> \<alpha>\<^sub>1"}, \ldots,
- @{text "\<alpha>\<^sub>n \<Rightarrow> \<beta>\<^sub>n"}, @{text "\<beta>\<^sub>n \<Rightarrow>
- \<alpha>\<^sub>n"}.
-
- \end{description}
-*}
-
-
-section {* Quotient types *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOL) "quotient_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
- @{command_def (HOL) "quotient_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
- @{command_def (HOL) "print_quotmapsQ3"} & : & @{text "context \<rightarrow>"}\\
- @{command_def (HOL) "print_quotientsQ3"} & : & @{text "context \<rightarrow>"}\\
- @{command_def (HOL) "print_quotconsts"} & : & @{text "context \<rightarrow>"}\\
- @{method_def (HOL) "lifting"} & : & @{text method} \\
- @{method_def (HOL) "lifting_setup"} & : & @{text method} \\
- @{method_def (HOL) "descending"} & : & @{text method} \\
- @{method_def (HOL) "descending_setup"} & : & @{text method} \\
- @{method_def (HOL) "partiality_descending"} & : & @{text method} \\
- @{method_def (HOL) "partiality_descending_setup"} & : & @{text method} \\
- @{method_def (HOL) "regularize"} & : & @{text method} \\
- @{method_def (HOL) "injection"} & : & @{text method} \\
- @{method_def (HOL) "cleaning"} & : & @{text method} \\
- @{attribute_def (HOL) "quot_thm"} & : & @{text attribute} \\
- @{attribute_def (HOL) "quot_lifted"} & : & @{text attribute} \\
- @{attribute_def (HOL) "quot_respect"} & : & @{text attribute} \\
- @{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\
- \end{matharray}
-
- The quotient package defines a new quotient type given a raw type
- and a partial equivalence relation. The package also historically
- includes automation for transporting definitions and theorems.
- But most of this automation was superseded by the Lifting and Transfer
- packages. The user should consider using these two new packages for
- lifting definitions and transporting theorems.
-
- @{rail \<open>
- @@{command (HOL) quotient_type} (spec)
- ;
- spec: @{syntax typespec} @{syntax mixfix}? '=' \<newline>
- @{syntax type} '/' ('partial' ':')? @{syntax term} \<newline>
- (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})?
- \<close>}
-
- @{rail \<open>
- @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \<newline>
- @{syntax term} 'is' @{syntax term}
- ;
- constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
- \<close>}
-
- @{rail \<open>
- @@{method (HOL) lifting} @{syntax thmrefs}?
- ;
- @@{method (HOL) lifting_setup} @{syntax thmrefs}?
- \<close>}
-
- \begin{description}
-
- \item @{command (HOL) "quotient_type"} defines a new quotient type @{text \<tau>}. The
- injection from a quotient type to a raw type is called @{text
- rep_\<tau>}, its inverse @{text abs_\<tau>} unless explicit @{keyword (HOL)
- "morphisms"} specification provides alternative names. @{command
- (HOL) "quotient_type"} requires the user to prove that the relation
- is an equivalence relation (predicate @{text equivp}), unless the
- user specifies explicitly @{text partial} in which case the
- obligation is @{text part_equivp}. A quotient defined with @{text
- partial} is weaker in the sense that less things can be proved
- automatically.
-
- The command internally proves a Quotient theorem and sets up the Lifting
- package by the command @{command (HOL) setup_lifting}. Thus the Lifting
- and Transfer packages can be used also with quotient types defined by
- @{command (HOL) "quotient_type"} without any extra set-up. The parametricity
- theorem for the equivalence relation R can be provided as an extra argument
- of the command and is passed to the corresponding internal call of @{command (HOL) setup_lifting}.
- This theorem allows the Lifting package to generate a stronger transfer rule for equality.
-
- \end{description}
-
- The most of the rest of the package was superseded by the Lifting and Transfer
- packages. The user should consider using these two new packages for
- lifting definitions and transporting theorems.
-
- \begin{description}
-
- \item @{command (HOL) "quotient_definition"} defines a constant on
- the quotient type.
-
- \item @{command (HOL) "print_quotmapsQ3"} prints quotient map
- functions.
-
- \item @{command (HOL) "print_quotientsQ3"} prints quotients.
-
- \item @{command (HOL) "print_quotconsts"} prints quotient constants.
-
- \item @{method (HOL) "lifting"} and @{method (HOL) "lifting_setup"}
- methods match the current goal with the given raw theorem to be
- lifted producing three new subgoals: regularization, injection and
- cleaning subgoals. @{method (HOL) "lifting"} tries to apply the
- heuristics for automatically solving these three subgoals and
- leaves only the subgoals unsolved by the heuristics to the user as
- opposed to @{method (HOL) "lifting_setup"} which leaves the three
- subgoals unsolved.
-
- \item @{method (HOL) "descending"} and @{method (HOL)
- "descending_setup"} try to guess a raw statement that would lift
- to the current subgoal. Such statement is assumed as a new subgoal
- and @{method (HOL) "descending"} continues in the same way as
- @{method (HOL) "lifting"} does. @{method (HOL) "descending"} tries
- to solve the arising regularization, injection and cleaning
- subgoals with the analogous method @{method (HOL)
- "descending_setup"} which leaves the four unsolved subgoals.
-
- \item @{method (HOL) "partiality_descending"} finds the regularized
- theorem that would lift to the current subgoal, lifts it and
- leaves as a subgoal. This method can be used with partial
- equivalence quotients where the non regularized statements would
- not be true. @{method (HOL) "partiality_descending_setup"} leaves
- the injection and cleaning subgoals unchanged.
-
- \item @{method (HOL) "regularize"} applies the regularization
- heuristics to the current subgoal.
-
- \item @{method (HOL) "injection"} applies the injection heuristics
- to the current goal using the stored quotient respectfulness
- theorems.
-
- \item @{method (HOL) "cleaning"} applies the injection cleaning
- heuristics to the current subgoal using the stored quotient
- preservation theorems.
-
- \item @{attribute (HOL) quot_lifted} attribute tries to
- automatically transport the theorem to the quotient type.
- The attribute uses all the defined quotients types and quotient
- constants often producing undesired results or theorems that
- cannot be lifted.
-
- \item @{attribute (HOL) quot_respect} and @{attribute (HOL)
- quot_preserve} attributes declare a theorem as a respectfulness
- and preservation theorem respectively. These are stored in the
- local theory store and used by the @{method (HOL) "injection"}
- and @{method (HOL) "cleaning"} methods respectively.
-
- \item @{attribute (HOL) quot_thm} declares that a certain theorem
- is a quotient extension theorem. Quotient extension theorems
- allow for quotienting inside container types. Given a polymorphic
- type that serves as a container, a map function defined for this
- container using @{command (HOL) "functor"} and a relation
- map defined for for the container type, the quotient extension
- theorem should be @{term "Quotient3 R Abs Rep \<Longrightarrow> Quotient3
- (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems
- are stored in a database and are used all the steps of lifting
- theorems.
-
- \end{description}
-*}
-
-
-section {* Definition by specification \label{sec:hol-specification} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOL) "specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
- \end{matharray}
-
- @{rail \<open>
- @@{command (HOL) specification} '(' (decl +) ')' \<newline>
- (@{syntax thmdecl}? @{syntax prop} +)
- ;
- decl: (@{syntax name} ':')? @{syntax term} ('(' @'overloaded' ')')?
- \<close>}
-
- \begin{description}
-
- \item @{command (HOL) "specification"}~@{text "decls \<phi>"} sets up a
- goal stating the existence of terms with the properties specified to
- hold for the constants given in @{text decls}. After finishing the
- proof, the theory will be augmented with definitions for the given
- constants, as well as with theorems stating the properties for these
- constants.
-
- @{text decl} declares a constant to be defined by the
- specification given. The definition for the constant @{text c} is
- bound to the name @{text c_def} unless a theorem name is given in
- the declaration. Overloaded constants should be declared as such.
-
- \end{description}
-*}
-
-
-section {* Adhoc overloading of constants *}
-
-text {*
- \begin{tabular}{rcll}
- @{command_def "adhoc_overloading"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "no_adhoc_overloading"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{attribute_def "show_variants"} & : & @{text "attribute"} & default @{text false} \\
- \end{tabular}
-
- \medskip
-
- Adhoc overloading allows to overload a constant depending on
- its type. Typically this involves the introduction of an
- uninterpreted constant (used for input and output) and the addition
- of some variants (used internally). For examples see
- @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and
- @{file "~~/src/HOL/Library/Monad_Syntax.thy"}.
-
- @{rail \<open>
- (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
- (@{syntax nameref} (@{syntax term} + ) + @'and')
- \<close>}
-
- \begin{description}
-
- \item @{command "adhoc_overloading"}~@{text "c v\<^sub>1 ... v\<^sub>n"}
- associates variants with an existing constant.
-
- \item @{command "no_adhoc_overloading"} is similar to
- @{command "adhoc_overloading"}, but removes the specified variants
- from the present context.
-
- \item @{attribute "show_variants"} controls printing of variants
- of overloaded constants. If enabled, the internally used variants
- are printed instead of their respective overloaded constants. This
- is occasionally useful to check whether the system agrees with a
- user's expectations about derived variants.
-
- \end{description}
-*}
-
-chapter {* Proof tools *}
-
-section {* Adhoc tuples *}
-
-text {*
- \begin{matharray}{rcl}
- @{attribute_def (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\
- \end{matharray}
-
- @{rail \<open>
- @@{attribute (HOL) split_format} ('(' 'complete' ')')?
- \<close>}
-
- \begin{description}
-
- \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes
- arguments in function applications to be represented canonically
- according to their tuple type structure.
-
- Note that this operation tends to invent funny names for new local
- parameters introduced.
-
- \end{description}
-*}
-
-
-section {* Transfer package *}
-
-text {*
- \begin{matharray}{rcl}
- @{method_def (HOL) "transfer"} & : & @{text method} \\
- @{method_def (HOL) "transfer'"} & : & @{text method} \\
- @{method_def (HOL) "transfer_prover"} & : & @{text method} \\
- @{attribute_def (HOL) "Transfer.transferred"} & : & @{text attribute} \\
- @{attribute_def (HOL) "untransferred"} & : & @{text attribute} \\
- @{attribute_def (HOL) "transfer_rule"} & : & @{text attribute} \\
- @{attribute_def (HOL) "transfer_domain_rule"} & : & @{text attribute} \\
- @{attribute_def (HOL) "relator_eq"} & : & @{text attribute} \\
- @{attribute_def (HOL) "relator_domain"} & : & @{text attribute} \\
- \end{matharray}
-
- \begin{description}
-
- \item @{method (HOL) "transfer"} method replaces the current subgoal
- with a logically equivalent one that uses different types and
- constants. The replacement of types and constants is guided by the
- database of transfer rules. Goals are generalized over all free
- variables by default; this is necessary for variables whose types
- change, but can be overridden for specific variables with e.g.
- @{text "transfer fixing: x y z"}.
-
- \item @{method (HOL) "transfer'"} is a variant of @{method (HOL)
- transfer} that allows replacing a subgoal with one that is
- logically stronger (rather than equivalent). For example, a
- subgoal involving equality on a quotient type could be replaced
- with a subgoal involving equality (instead of the corresponding
- equivalence relation) on the underlying raw type.
-
- \item @{method (HOL) "transfer_prover"} method assists with proving
- a transfer rule for a new constant, provided the constant is
- defined in terms of other constants that already have transfer
- rules. It should be applied after unfolding the constant
- definitions.
-
- \item @{attribute (HOL) "untransferred"} proves the same equivalent theorem
- as @{method (HOL) "transfer"} internally does.
-
- \item @{attribute (HOL) Transfer.transferred} works in the opposite
- direction than @{method (HOL) "transfer'"}. E.g., given the transfer
- relation @{text "ZN x n \<equiv> (x = int n)"}, corresponding transfer rules and the theorem
- @{text "\<forall>x::int \<in> {0..}. x < x + 1"}, the attribute would prove
- @{text "\<forall>n::nat. n < n + 1"}. The attribute is still in experimental
- phase of development.
-
- \item @{attribute (HOL) "transfer_rule"} attribute maintains a
- collection of transfer rules, which relate constants at two
- different types. Typical transfer rules may relate different type
- instances of the same polymorphic constant, or they may relate an
- operation on a raw type to a corresponding operation on an
- abstract type (quotient or subtype). For example:
-
- @{text "((A ===> B) ===> list_all2 A ===> list_all2 B) map map"}\\
- @{text "(cr_int ===> cr_int ===> cr_int) (\<lambda>(x,y) (u,v). (x+u, y+v)) plus"}
-
- Lemmas involving predicates on relations can also be registered
- using the same attribute. For example:
-
- @{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"}\\
- @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)"}
-
- \item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
- of rules, which specify a domain of a transfer relation by a predicate.
- E.g., given the transfer relation @{text "ZN x n \<equiv> (x = int n)"},
- one can register the following transfer domain rule:
- @{text "Domainp ZN = (\<lambda>x. x \<ge> 0)"}. The rules allow the package to produce
- more readable transferred goals, e.g., when quantifiers are transferred.
-
- \item @{attribute (HOL) relator_eq} attribute collects identity laws
- for relators of various type constructors, e.g. @{text "list_all2
- (op =) = (op =)"}. The @{method (HOL) transfer} method uses these
- lemmas to infer transfer rules for non-polymorphic constants on
- the fly.
-
- \item @{attribute_def (HOL) "relator_domain"} attribute collects rules
- describing domains of relators by predicators. E.g., @{text "Domainp A = P \<Longrightarrow>
- Domainp (list_all2 A) = (list_all P)"}. This allows the package to lift transfer
- domain rules through type constructors.
-
- \end{description}
-
- Theoretical background can be found in \cite{Huffman-Kuncar:2013:lifting_transfer}.
-*}
-
-
-section {* Lifting package *}
-
-text {*
- The Lifting package allows users to lift terms of the raw type to the abstract type, which is
- a necessary step in building a library for an abstract type. Lifting defines a new constant
- by combining coercion functions (Abs and Rep) with the raw term. It also proves an appropriate
- transfer rule for the Transfer package and, if possible, an equation for the code generator.
-
- The Lifting package provides two main commands: @{command (HOL) "setup_lifting"} for initializing
- the package to work with a new type, and @{command (HOL) "lift_definition"} for lifting constants.
- The Lifting package works with all four kinds of type abstraction: type copies, subtypes,
- total quotients and partial quotients.
-
- Theoretical background can be found in \cite{Huffman-Kuncar:2013:lifting_transfer}.
-
- \begin{matharray}{rcl}
- @{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
- @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
- @{command_def (HOL) "lifting_forget"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
- @{command_def (HOL) "lifting_update"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
- @{command_def (HOL) "print_quot_maps"} & : & @{text "context \<rightarrow>"}\\
- @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
- @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
- @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
- @{attribute_def (HOL) "reflexivity_rule"} & : & @{text attribute} \\
- @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\
- @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\
- @{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\
- @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\
- \end{matharray}
-
- @{rail \<open>
- @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \<newline>
- @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
- \<close>}
-
- @{rail \<open>
- @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \<newline>
- 'is' @{syntax term} (@'parametric' @{syntax thmref})?;
- \<close>}
-
- @{rail \<open>
- @@{command (HOL) lifting_forget} @{syntax nameref};
- \<close>}
-
- @{rail \<open>
- @@{command (HOL) lifting_update} @{syntax nameref};
- \<close>}
-
- @{rail \<open>
- @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?;
- \<close>}
-
- \begin{description}
-
- \item @{command (HOL) "setup_lifting"} Sets up the Lifting package
- to work with a user-defined type.
- The command supports two modes. The first one is a low-level mode when
- the user must provide as a first
- argument of @{command (HOL) "setup_lifting"} a
- quotient theorem @{text "Quotient R Abs Rep T"}. The
- package configures a transfer rule for equality, a domain transfer
- rules and sets up the @{command_def (HOL) "lift_definition"}
- command to work with the abstract type. An optional theorem @{text "reflp R"}, which certifies that
- the equivalence relation R is total,
- can be provided as a second argument. This allows the package to generate stronger transfer
- rules. And finally, the parametricity theorem for R can be provided as a third argument.
- This allows the package to generate a stronger transfer rule for equality.
-
- Users generally will not prove the @{text Quotient} theorem manually for
- new types, as special commands exist to automate the process.
-
- When a new subtype is defined by @{command (HOL) typedef}, @{command (HOL) "lift_definition"}
- can be used in its
- second mode, where only the type_definition theorem @{text "type_definition Rep Abs A"}
- is used as an argument of the command. The command internally proves the corresponding
- Quotient theorem and registers it with @{command (HOL) setup_lifting} using its first mode.
-
- For quotients, the command @{command (HOL) quotient_type} can be used. The command defines
- a new quotient type and similarly to the previous case, the corresponding Quotient theorem is proved
- and registered by @{command (HOL) setup_lifting}.
-
- The command @{command (HOL) "setup_lifting"} also sets up the code generator
- for the new type. Later on, when a new constant is defined by @{command (HOL) "lift_definition"},
- the Lifting package proves and registers a code equation (if there is one) for the new constant.
- If the option @{text "no_code"} is specified, the Lifting package does not set up the code
- generator and as a consequence no code equations involving an abstract type are registered
- by @{command (HOL) "lift_definition"}.
-
- \item @{command (HOL) "lift_definition"} @{text "f :: \<tau>"} @{keyword (HOL) "is"} @{text t}
- Defines a new function @{text f} with an abstract type @{text \<tau>}
- in terms of a corresponding operation @{text t} on a
- representation type. More formally, if @{text "t :: \<sigma>"}, then
- the command builds a term @{text "F"} as a corresponding combination of abstraction
- and representation functions such that @{text "F :: \<sigma> \<Rightarrow> \<tau>" } and
- defines @{text f} is as @{text "f \<equiv> F t"}.
- The term @{text t} does not have to be necessarily a constant but it can be any term.
-
- The command opens a proof environment and the user must discharge
- a respectfulness proof obligation. For a type copy, i.e., a typedef with @{text
- UNIV}, the obligation is discharged automatically. The proof goal is
- presented in a user-friendly, readable form. A respectfulness
- theorem in the standard format @{text f.rsp} and a transfer rule
- @{text f.transfer} for the Transfer package are generated by the
- package.
-
- The user can specify a parametricity theorem for @{text t} after the keyword
- @{keyword "parametric"}, which allows the command
- to generate a parametric transfer rule for @{text f}.
-
- For each constant defined through trivial quotients (type copies or
- subtypes) @{text f.rep_eq} is generated. The equation is a code certificate
- that defines @{text f} using the representation function.
-
- For each constant @{text f.abs_eq} is generated. The equation is unconditional
- for total quotients. The equation defines @{text f} using
- the abstraction function.
-
- Integration with [@{attribute code} abstract]: For subtypes (e.g.,
- corresponding to a datatype invariant, such as dlist), @{command
- (HOL) "lift_definition"} uses a code certificate theorem
- @{text f.rep_eq} as a code equation.
-
- Integration with [@{attribute code} equation]: For total quotients, @{command
- (HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation.
-
- \item @{command (HOL) lifting_forget} and @{command (HOL) lifting_update}
- These two commands serve for storing and deleting the set-up of
- the Lifting package and corresponding transfer rules defined by this package.
- This is useful for hiding of type construction details of an abstract type
- when the construction is finished but it still allows additions to this construction
- when this is later necessary.
-
- Whenever the Lifting package is set up with a new abstract type @{text "\<tau>"} by
- @{command_def (HOL) "lift_definition"}, the package defines a new bundle
- that is called @{text "\<tau>.lifting"}. This bundle already includes set-up for the Lifting package.
- The new transfer rules
- introduced by @{command (HOL) "lift_definition"} can be stored in the bundle by
- the command @{command (HOL) "lifting_update"} @{text "\<tau>.lifting"}.
-
- The command @{command (HOL) "lifting_forget"} @{text "\<tau>.lifting"} deletes set-up of the Lifting
- package
- for @{text \<tau>} and deletes all the transfer rules that were introduced
- by @{command (HOL) "lift_definition"} using @{text \<tau>} as an abstract type.
-
- The stored set-up in a bundle can be reintroduced by the Isar commands for including a bundle
- (@{command "include"}, @{keyword "includes"} and @{command "including"}).
-
- \item @{command (HOL) "print_quot_maps"} prints stored quotient map
- theorems.
-
- \item @{command (HOL) "print_quotients"} prints stored quotient
- theorems.
-
- \item @{attribute (HOL) quot_map} registers a quotient map
- theorem. E.g., @{text "Quotient R Abs Rep T \<Longrightarrow>
- Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"}.
- For examples see @{file
- "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
- in the same directory.
-
- \item @{attribute (HOL) invariant_commute} registers a theorem that
- shows a relationship between the constant @{text
- Lifting.invariant} (used for internal encoding of proper subtypes)
- and a relator. Such theorems allows the package to hide @{text
- Lifting.invariant} from a user in a user-readable form of a
- respectfulness theorem. For examples see @{file
- "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
-
- \item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
- that a relator respects left-totality and left_uniqueness. For examples
- see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
- in the same directory.
- The property is used in a reflexivity prover, which is used for discharging respectfulness
- theorems for type copies and also for discharging assumptions of abstraction function equations.
-
- \item @{attribute (HOL) "relator_mono"} registers a property describing a monotonicity of a relator.
- E.g., @{text "A \<le> B \<Longrightarrow> list_all2 A \<le> list_all2 B"}. For examples
- see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"}
- or Lifting_*.thy files in the same directory.
- This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
- when a parametricity theorem for the raw term is specified.
-
- \item @{attribute (HOL) "relator_distr"} registers a property describing a distributivity
- of the relation composition and a relator. E.g.,
- @{text "list_all2 R \<circ>\<circ> list_all2 S = list_all2 (R \<circ>\<circ> S)"}.
- This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
- when a parametricity theorem for the raw term is specified.
- When this equality does not hold unconditionally (e.g., for the function type), the user can specified
- each direction separately and also register multiple theorems with different set of assumptions.
- This attribute can be used only after the monotonicity property was already registered by
- @{attribute (HOL) "relator_mono"}. For examples
- see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"}
- or Lifting_*.thy files in the same directory.
-
- \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
- from the Lifting infrastructure and thus de-register the corresponding quotient.
- This effectively causes that @{command (HOL) lift_definition} will not
- do any lifting for the corresponding type. This attribute is rather used for low-level
- manipulation with set-up of the Lifting package because @{command (HOL) lifting_forget} is
- preferred for normal usage.
-
- \item @{attribute (HOL) lifting_restore} @{text "Quotient_thm pcr_def pcr_cr_eq_thm"}
- registers the Quotient theorem @{text Quotient_thm} in the Lifting infrastructure
- and thus sets up lifting for an abstract type @{text \<tau>} (that is defined by @{text Quotient_thm}).
- Optional theorems @{text pcr_def} and @{text pcr_cr_eq_thm} can be specified to register
- the parametrized
- correspondence relation for @{text \<tau>}. E.g., for @{text "'a dlist"}, @{text pcr_def} is
- @{text "pcr_dlist A \<equiv> list_all2 A \<circ>\<circ> cr_dlist"} and @{text pcr_cr_eq_thm} is
- @{text "pcr_dlist op= = op="}.
- This attribute is rather used for low-level
- manipulation with set-up of the Lifting package because using of the bundle @{text \<tau>.lifting}
- together with the commands @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} is
- preferred for normal usage.
-
- \end{description}
-*}
-
-
-section {* Coercive subtyping *}
-
-text {*
- \begin{matharray}{rcl}
- @{attribute_def (HOL) coercion} & : & @{text attribute} \\
- @{attribute_def (HOL) coercion_enabled} & : & @{text attribute} \\
- @{attribute_def (HOL) coercion_map} & : & @{text attribute} \\
- \end{matharray}
-
- Coercive subtyping allows the user to omit explicit type
- conversions, also called \emph{coercions}. Type inference will add
- them as necessary when parsing a term. See
- \cite{traytel-berghofer-nipkow-2011} for details.
-
- @{rail \<open>
- @@{attribute (HOL) coercion} (@{syntax term})?
- ;
- @@{attribute (HOL) coercion_map} (@{syntax term})?
- \<close>}
-
- \begin{description}
-
- \item @{attribute (HOL) "coercion"}~@{text "f"} registers a new
- coercion function @{text "f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2"} where @{text "\<sigma>\<^sub>1"} and
- @{text "\<sigma>\<^sub>2"} are type constructors without arguments. Coercions are
- composed by the inference algorithm if needed. Note that the type
- inference algorithm is complete only if the registered coercions
- form a lattice.
-
- \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a
- new map function to lift coercions through type constructors. The
- function @{text "map"} must conform to the following type pattern
-
- \begin{matharray}{lll}
- @{text "map"} & @{text "::"} &
- @{text "f\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> f\<^sub>n \<Rightarrow> (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Rightarrow> (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t"} \\
- \end{matharray}
-
- where @{text "t"} is a type constructor and @{text "f\<^sub>i"} is of type
- @{text "\<alpha>\<^sub>i \<Rightarrow> \<beta>\<^sub>i"} or @{text "\<beta>\<^sub>i \<Rightarrow> \<alpha>\<^sub>i"}. Registering a map function
- overwrites any existing map function for this particular type
- constructor.
-
- \item @{attribute (HOL) "coercion_enabled"} enables the coercion
- inference algorithm.
-
- \end{description}
-*}
-
-
-section {* Arithmetic proof support *}
-
-text {*
- \begin{matharray}{rcl}
- @{method_def (HOL) arith} & : & @{text method} \\
- @{attribute_def (HOL) arith} & : & @{text attribute} \\
- @{attribute_def (HOL) arith_split} & : & @{text attribute} \\
- \end{matharray}
-
- \begin{description}
-
- \item @{method (HOL) arith} decides linear arithmetic problems (on
- types @{text nat}, @{text int}, @{text real}). Any current facts
- are inserted into the goal before running the procedure.
-
- \item @{attribute (HOL) arith} declares facts that are supplied to
- the arithmetic provers implicitly.
-
- \item @{attribute (HOL) arith_split} attribute declares case split
- rules to be expanded before @{method (HOL) arith} is invoked.
-
- \end{description}
-
- Note that a simpler (but faster) arithmetic prover is already
- invoked by the Simplifier.
-*}
-
-
-section {* Intuitionistic proof search *}
-
-text {*
- \begin{matharray}{rcl}
- @{method_def (HOL) iprover} & : & @{text method} \\
- \end{matharray}
-
- @{rail \<open>
- @@{method (HOL) iprover} (@{syntax rulemod} *)
- \<close>}
-
- \begin{description}
-
- \item @{method (HOL) iprover} performs intuitionistic proof search,
- depending on specifically declared rules from the context, or given
- as explicit arguments. Chained facts are inserted into the goal
- before commencing proof search.
-
- Rules need to be classified as @{attribute (Pure) intro},
- @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
- ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
- applied aggressively (without considering back-tracking later).
- Rules declared with ``@{text "?"}'' are ignored in proof search (the
- single-step @{method (Pure) rule} method still observes these). An
- explicit weight annotation may be given as well; otherwise the
- number of rule premises will be taken into account here.
-
- \end{description}
-*}
-
-
-section {* Model Elimination and Resolution *}
-
-text {*
- \begin{matharray}{rcl}
- @{method_def (HOL) "meson"} & : & @{text method} \\
- @{method_def (HOL) "metis"} & : & @{text method} \\
- \end{matharray}
-
- @{rail \<open>
- @@{method (HOL) meson} @{syntax thmrefs}?
- ;
- @@{method (HOL) metis}
- ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
- @{syntax thmrefs}?
- \<close>}
-
- \begin{description}
-
- \item @{method (HOL) meson} implements Loveland's model elimination
- procedure \cite{loveland-78}. See @{file
- "~~/src/HOL/ex/Meson_Test.thy"} for examples.
-
- \item @{method (HOL) metis} combines ordered resolution and ordered
- paramodulation to find first-order (or mildly higher-order) proofs.
- The first optional argument specifies a type encoding; see the
- Sledgehammer manual \cite{isabelle-sledgehammer} for details. The
- directory @{file "~~/src/HOL/Metis_Examples"} contains several small
- theories developed to a large extent using @{method (HOL) metis}.
-
- \end{description}
-*}
-
-
-section {* Algebraic reasoning via Gr\"obner bases *}
-
-text {*
- \begin{matharray}{rcl}
- @{method_def (HOL) "algebra"} & : & @{text method} \\
- @{attribute_def (HOL) algebra} & : & @{text attribute} \\
- \end{matharray}
-
- @{rail \<open>
- @@{method (HOL) algebra}
- ('add' ':' @{syntax thmrefs})?
- ('del' ':' @{syntax thmrefs})?
- ;
- @@{attribute (HOL) algebra} (() | 'add' | 'del')
- \<close>}
-
- \begin{description}
-
- \item @{method (HOL) algebra} performs algebraic reasoning via
- Gr\"obner bases, see also \cite{Chaieb-Wenzel:2007} and
- \cite[\S3.2]{Chaieb-thesis}. The method handles deals with two main
- classes of problems:
-
- \begin{enumerate}
-
- \item Universal problems over multivariate polynomials in a
- (semi)-ring/field/idom; the capabilities of the method are augmented
- according to properties of these structures. For this problem class
- the method is only complete for algebraically closed fields, since
- the underlying method is based on Hilbert's Nullstellensatz, where
- the equivalence only holds for algebraically closed fields.
-
- The problems can contain equations @{text "p = 0"} or inequations
- @{text "q \<noteq> 0"} anywhere within a universal problem statement.
-
- \item All-exists problems of the following restricted (but useful)
- form:
-
- @{text [display] "\<forall>x\<^sub>1 \<dots> x\<^sub>n.
- e\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<and> \<dots> \<and> e\<^sub>m(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<longrightarrow>
- (\<exists>y\<^sub>1 \<dots> y\<^sub>k.
- p\<^sub>1\<^sub>1(x\<^sub>1, \<dots> ,x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>1\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0 \<and>
- \<dots> \<and>
- p\<^sub>t\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>t\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0)"}
-
- Here @{text "e\<^sub>1, \<dots>, e\<^sub>n"} and the @{text "p\<^sub>i\<^sub>j"} are multivariate
- polynomials only in the variables mentioned as arguments.
-
- \end{enumerate}
-
- The proof method is preceded by a simplification step, which may be
- modified by using the form @{text "(algebra add: ths\<^sub>1 del: ths\<^sub>2)"}.
- This acts like declarations for the Simplifier
- (\secref{sec:simplifier}) on a private simpset for this tool.
-
- \item @{attribute algebra} (as attribute) manages the default
- collection of pre-simplification rules of the above proof method.
-
- \end{description}
-*}
-
-
-subsubsection {* Example *}
-
-text {* The subsequent example is from geometry: collinearity is
- invariant by rotation. *}
-
-type_synonym point = "int \<times> int"
-
-fun collinear :: "point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
- "collinear (Ax, Ay) (Bx, By) (Cx, Cy) \<longleftrightarrow>
- (Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx)"
-
-lemma collinear_inv_rotation:
- assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"
- shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
- (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
- using assms by (algebra add: collinear.simps)
-
-text {*
- See also @{file "~~/src/HOL/ex/Groebner_Examples.thy"}.
-*}
-
-
-section {* Coherent Logic *}
-
-text {*
- \begin{matharray}{rcl}
- @{method_def (HOL) "coherent"} & : & @{text method} \\
- \end{matharray}
-
- @{rail \<open>
- @@{method (HOL) coherent} @{syntax thmrefs}?
- \<close>}
-
- \begin{description}
-
- \item @{method (HOL) coherent} solves problems of \emph{Coherent
- Logic} \cite{Bezem-Coquand:2005}, which covers applications in
- confluence theory, lattice theory and projective geometry. See
- @{file "~~/src/HOL/ex/Coherent.thy"} for some examples.
-
- \end{description}
-*}
-
-
-section {* Proving propositions *}
-
-text {*
- In addition to the standard proof methods, a number of diagnosis
- tools search for proofs and provide an Isar proof snippet on success.
- These tools are available via the following commands.
-
- \begin{matharray}{rcl}
- @{command_def (HOL) "solve_direct"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
- @{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
- @{command_def (HOL) "try0"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
- @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
- @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \<rightarrow> theory"}
- \end{matharray}
-
- @{rail \<open>
- @@{command (HOL) try}
- ;
-
- @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
- @{syntax nat}?
- ;
-
- @@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?
- ;
-
- @@{command (HOL) sledgehammer_params} ( ( '[' args ']' ) ? )
- ;
- args: ( @{syntax name} '=' value + ',' )
- ;
- facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'
- \<close>} % FIXME check args "value"
-
- \begin{description}
-
- \item @{command (HOL) "solve_direct"} checks whether the current
- subgoals can be solved directly by an existing theorem. Duplicate
- lemmas can be detected in this way.
-
- \item @{command (HOL) "try0"} attempts to prove a subgoal
- using a combination of standard proof methods (@{method auto},
- @{method simp}, @{method blast}, etc.). Additional facts supplied
- via @{text "simp:"}, @{text "intro:"}, @{text "elim:"}, and @{text
- "dest:"} are passed to the appropriate proof methods.
-
- \item @{command (HOL) "try"} attempts to prove or disprove a subgoal
- using a combination of provers and disprovers (@{command (HOL)
- "solve_direct"}, @{command (HOL) "quickcheck"}, @{command (HOL)
- "try0"}, @{command (HOL) "sledgehammer"}, @{command (HOL)
- "nitpick"}).
-
- \item @{command (HOL) "sledgehammer"} attempts to prove a subgoal
- using external automatic provers (resolution provers and SMT
- solvers). See the Sledgehammer manual \cite{isabelle-sledgehammer}
- for details.
-
- \item @{command (HOL) "sledgehammer_params"} changes @{command (HOL)
- "sledgehammer"} configuration options persistently.
-
- \end{description}
-*}
-
-
-section {* Checking and refuting propositions *}
-
-text {*
- Identifying incorrect propositions usually involves evaluation of
- particular assignments and systematic counterexample search. This
- is supported by the following commands.
-
- \begin{matharray}{rcl}
- @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def (HOL) "values"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
- @{command_def (HOL) "nitpick"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
- @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "nitpick_params"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "quickcheck_generator"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "find_unused_assms"} & : & @{text "context \<rightarrow>"}
- \end{matharray}
-
- @{rail \<open>
- @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
- ;
-
- @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
- ;
-
- (@@{command (HOL) quickcheck} | @@{command (HOL) nitpick})
- ( '[' args ']' )? @{syntax nat}?
- ;
-
- (@@{command (HOL) quickcheck_params} |
- @@{command (HOL) nitpick_params}) ( '[' args ']' )?
- ;
-
- @@{command (HOL) quickcheck_generator} @{syntax nameref} \<newline>
- 'operations:' ( @{syntax term} +)
- ;
-
- @@{command (HOL) find_unused_assms} @{syntax name}?
- ;
- modes: '(' (@{syntax name} +) ')'
- ;
- args: ( @{syntax name} '=' value + ',' )
- \<close>} % FIXME check "value"
-
- \begin{description}
-
- \item @{command (HOL) "value"}~@{text t} evaluates and prints a
- term; optionally @{text modes} can be specified, which are appended
- to the current print mode; see \secref{sec:print-modes}.
- Internally, the evaluation is performed by registered evaluators,
- which are invoked sequentially until a result is returned.
- Alternatively a specific evaluator can be selected using square
- brackets; typical evaluators use the current set of code equations
- to normalize and include @{text simp} for fully symbolic evaluation
- using the simplifier, @{text nbe} for \emph{normalization by
- evaluation} and \emph{code} for code generation in SML.
-
- \item @{command (HOL) "values"}~@{text t} enumerates a set
- comprehension by evaluation and prints its values up to the given
- number of solutions; optionally @{text modes} can be specified,
- which are appended to the current print mode; see
- \secref{sec:print-modes}.
-
- \item @{command (HOL) "quickcheck"} tests the current goal for
- counterexamples using a series of assignments for its free
- variables; by default the first subgoal is tested, an other can be
- selected explicitly using an optional goal index. Assignments can
- be chosen exhausting the search space up to a given size, or using a
- fixed number of random assignments in the search space, or exploring
- the search space symbolically using narrowing. By default,
- quickcheck uses exhaustive testing. A number of configuration
- options are supported for @{command (HOL) "quickcheck"}, notably:
-
- \begin{description}
-
- \item[@{text tester}] specifies which testing approach to apply.
- There are three testers, @{text exhaustive}, @{text random}, and
- @{text narrowing}. An unknown configuration option is treated as
- an argument to tester, making @{text "tester ="} optional. When
- multiple testers are given, these are applied in parallel. If no
- tester is specified, quickcheck uses the testers that are set
- active, i.e., configurations @{attribute
- quickcheck_exhaustive_active}, @{attribute
- quickcheck_random_active}, @{attribute
- quickcheck_narrowing_active} are set to true.
-
- \item[@{text size}] specifies the maximum size of the search space
- for assignment values.
-
- \item[@{text genuine_only}] sets quickcheck only to return genuine
- counterexample, but not potentially spurious counterexamples due
- to underspecified functions.
-
- \item[@{text abort_potential}] sets quickcheck to abort once it
- found a potentially spurious counterexample and to not continue
- to search for a further genuine counterexample.
- For this option to be effective, the @{text genuine_only} option
- must be set to false.
-
- \item[@{text eval}] takes a term or a list of terms and evaluates
- these terms under the variable assignment found by quickcheck.
- This option is currently only supported by the default
- (exhaustive) tester.
-
- \item[@{text iterations}] sets how many sets of assignments are
- generated for each particular size.
-
- \item[@{text no_assms}] specifies whether assumptions in
- structured proofs should be ignored.
-
- \item[@{text locale}] specifies how to process conjectures in
- a locale context, i.e., they can be interpreted or expanded.
- The option is a whitespace-separated list of the two words
- @{text interpret} and @{text expand}. The list determines the
- order they are employed. The default setting is to first use
- interpretations and then test the expanded conjecture.
- The option is only provided as attribute declaration, but not
- as parameter to the command.
-
- \item[@{text timeout}] sets the time limit in seconds.
-
- \item[@{text default_type}] sets the type(s) generally used to
- instantiate type variables.
-
- \item[@{text report}] if set quickcheck reports how many tests
- fulfilled the preconditions.
-
- \item[@{text use_subtype}] if set quickcheck automatically lifts
- conjectures to registered subtypes if possible, and tests the
- lifted conjecture.
-
- \item[@{text quiet}] if set quickcheck does not output anything
- while testing.
-
- \item[@{text verbose}] if set quickcheck informs about the current
- size and cardinality while testing.
-
- \item[@{text expect}] can be used to check if the user's
- expectation was met (@{text no_expectation}, @{text
- no_counterexample}, or @{text counterexample}).
-
- \end{description}
-
- These option can be given within square brackets.
-
- Using the following type classes, the testers generate values and convert
- them back into Isabelle terms for displaying counterexamples.
- \begin{description}
- \item[@{text exhaustive}] The parameters of the type classes @{class exhaustive}
- and @{class full_exhaustive} implement the testing. They take a
- testing function as a parameter, which takes a value of type @{typ "'a"}
- and optionally produces a counterexample, and a size parameter for the test values.
- In @{class full_exhaustive}, the testing function parameter additionally
- expects a lazy term reconstruction in the type @{typ Code_Evaluation.term}
- of the tested value.
-
- The canonical implementation for @{text exhaustive} testers calls the given
- testing function on all values up to the given size and stops as soon
- as a counterexample is found.
-
- \item[@{text random}] The operation @{const Quickcheck_Random.random}
- of the type class @{class random} generates a pseudo-random
- value of the given size and a lazy term reconstruction of the value
- in the type @{typ Code_Evaluation.term}. A pseudo-randomness generator
- is defined in theory @{theory Random}.
-
- \item[@{text narrowing}] implements Haskell's Lazy Smallcheck~\cite{runciman-naylor-lindblad}
- using the type classes @{class narrowing} and @{class partial_term_of}.
- Variables in the current goal are initially represented as symbolic variables.
- If the execution of the goal tries to evaluate one of them, the test engine
- replaces it with refinements provided by @{const narrowing}.
- Narrowing views every value as a sum-of-products which is expressed using the operations
- @{const Quickcheck_Narrowing.cons} (embedding a value),
- @{const Quickcheck_Narrowing.apply} (product) and @{const Quickcheck_Narrowing.sum} (sum).
- The refinement should enable further evaluation of the goal.
-
- For example, @{const narrowing} for the list type @{typ "'a :: narrowing list"}
- can be recursively defined as
- @{term "Quickcheck_Narrowing.sum (Quickcheck_Narrowing.cons [])
- (Quickcheck_Narrowing.apply
- (Quickcheck_Narrowing.apply
- (Quickcheck_Narrowing.cons (op #))
- narrowing)
- narrowing)"}.
- If a symbolic variable of type @{typ "_ list"} is evaluated, it is replaced by (i)~the empty
- list @{term "[]"} and (ii)~by a non-empty list whose head and tail can then be recursively
- refined if needed.
-
- To reconstruct counterexamples, the operation @{const partial_term_of} transforms
- @{text narrowing}'s deep representation of terms to the type @{typ Code_Evaluation.term}.
- The deep representation models symbolic variables as
- @{const Quickcheck_Narrowing.Narrowing_variable}, which are normally converted to
- @{const Code_Evaluation.Free}, and refined values as
- @{term "Quickcheck_Narrowing.Narrowing_constructor i args"}, where @{term "i :: integer"}
- denotes the index in the sum of refinements. In the above example for lists,
- @{term "0"} corresponds to @{term "[]"} and @{term "1"}
- to @{term "op #"}.
-
- The command @{command (HOL) "code_datatype"} sets up @{const partial_term_of}
- such that the @{term "i"}-th refinement is interpreted as the @{term "i"}-th constructor,
- but it does not ensures consistency with @{const narrowing}.
- \end{description}
-
- \item @{command (HOL) "quickcheck_params"} changes @{command (HOL)
- "quickcheck"} configuration options persistently.
-
- \item @{command (HOL) "quickcheck_generator"} creates random and
- exhaustive value generators for a given type and operations. It
- generates values by using the operations as if they were
- constructors of that type.
-
- \item @{command (HOL) "nitpick"} tests the current goal for
- counterexamples using a reduction to first-order relational
- logic. See the Nitpick manual \cite{isabelle-nitpick} for details.
-
- \item @{command (HOL) "nitpick_params"} changes @{command (HOL)
- "nitpick"} configuration options persistently.
-
- \item @{command (HOL) "find_unused_assms"} finds potentially superfluous
- assumptions in theorems using quickcheck.
- It takes the theory name to be checked for superfluous assumptions as
- optional argument. If not provided, it checks the current theory.
- Options to the internal quickcheck invocations can be changed with
- common configuration declarations.
-
- \end{description}
-*}
-
-
-section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *}
-
-text {*
- The following tools of Isabelle/HOL support cases analysis and
- induction in unstructured tactic scripts; see also
- \secref{sec:cases-induct} for proper Isar versions of similar ideas.
-
- \begin{matharray}{rcl}
- @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\
- @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- \end{matharray}
-
- @{rail \<open>
- @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?
- ;
- @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
- ;
- @@{method (HOL) ind_cases} (@{syntax prop}+) (@'for' (@{syntax name}+))?
- ;
- @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
- ;
- rule: 'rule' ':' @{syntax thmref}
- \<close>}
-
- \begin{description}
-
- \item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit
- to reason about inductive types. Rules are selected according to
- the declarations by the @{attribute cases} and @{attribute induct}
- attributes, cf.\ \secref{sec:cases-induct}. The @{command (HOL)
- datatype} package already takes care of this.
-
- These unstructured tactics feature both goal addressing and dynamic
- instantiation. Note that named rule cases are \emph{not} provided
- as would be by the proper @{method cases} and @{method induct} proof
- methods (see \secref{sec:cases-induct}). Unlike the @{method
- induct} method, @{method induct_tac} does not handle structured rule
- statements, only the compact object-logic conclusion of the subgoal
- being addressed.
-
- \item @{method (HOL) ind_cases} and @{command (HOL)
- "inductive_cases"} provide an interface to the internal @{ML_text
- mk_cases} operation. Rules are simplified in an unrestricted
- forward manner.
-
- While @{method (HOL) ind_cases} is a proof method to apply the
- result immediately as elimination rules, @{command (HOL)
- "inductive_cases"} provides case split theorems at the theory level
- for later use. The @{keyword "for"} argument of the @{method (HOL)
- ind_cases} method allows to specify a list of variables that should
- be generalized before applying the resulting rule.
-
- \end{description}
-*}
-
-
-chapter {* Executable code *}
-
-text {* For validation purposes, it is often useful to \emph{execute}
- specifications. In principle, execution could be simulated by
- Isabelle's inference kernel, i.e. by a combination of resolution and
- simplification. Unfortunately, this approach is rather inefficient.
- A more efficient way of executing specifications is to translate
- them into a functional programming language such as ML.
-
- Isabelle provides a generic framework to support code generation
- from executable specifications. Isabelle/HOL instantiates these
- mechanisms in a way that is amenable to end-user applications. Code
- can be generated for functional programs (including overloading
- using type classes) targeting SML \cite{SML}, OCaml \cite{OCaml},
- Haskell \cite{haskell-revised-report} and Scala
- \cite{scala-overview-tech-report}. Conceptually, code generation is
- split up in three steps: \emph{selection} of code theorems,
- \emph{translation} into an abstract executable view and
- \emph{serialization} to a specific \emph{target language}.
- Inductive specifications can be executed using the predicate
- compiler which operates within HOL. See \cite{isabelle-codegen} for
- an introduction.
-
- \begin{matharray}{rcl}
- @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{attribute_def (HOL) code} & : & @{text attribute} \\
- @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{attribute_def (HOL) code_unfold} & : & @{text attribute} \\
- @{attribute_def (HOL) code_post} & : & @{text attribute} \\
- @{attribute_def (HOL) code_abbrev} & : & @{text attribute} \\
- @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_printing"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_identifier"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_pred"} & : & @{text "theory \<rightarrow> proof(prove)"}
- \end{matharray}
-
- @{rail \<open>
- @@{command (HOL) export_code} ( @'open' ) ? ( constexpr + ) \<newline>
- ( ( @'in' target ( @'module_name' @{syntax string} ) ? \<newline>
- ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
- ;
-
- const: @{syntax term}
- ;
-
- constexpr: ( const | 'name._' | '_' )
- ;
-
- typeconstructor: @{syntax nameref}
- ;
-
- class: @{syntax nameref}
- ;
-
- target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
- ;
-
- @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract'
- | 'drop:' ( const + ) | 'abort:' ( const + ) )?
- ;
-
- @@{command (HOL) code_datatype} ( const + )
- ;
-
- @@{attribute (HOL) code_unfold} ( 'del' ) ?
- ;
-
- @@{attribute (HOL) code_post} ( 'del' ) ?
- ;
-
- @@{attribute (HOL) code_abbrev}
- ;
-
- @@{command (HOL) code_thms} ( constexpr + ) ?
- ;
-
- @@{command (HOL) code_deps} ( constexpr + ) ?
- ;
-
- @@{command (HOL) code_reserved} target ( @{syntax string} + )
- ;
-
- symbol_const: ( @'constant' const )
- ;
-
- symbol_typeconstructor: ( @'type_constructor' typeconstructor )
- ;
-
- symbol_class: ( @'type_class' class )
- ;
-
- symbol_class_relation: ( @'class_relation' class ( '<' | '\<subseteq>' ) class )
- ;
-
- symbol_class_instance: ( @'class_instance' typeconstructor @'::' class )
- ;
-
- symbol_module: ( @'code_module' name )
- ;
-
- syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
- ;
-
- printing_const: symbol_const ( '\<rightharpoonup>' | '=>' ) \<newline>
- ( '(' target ')' syntax ? + @'and' )
- ;
-
- printing_typeconstructor: symbol_typeconstructor ( '\<rightharpoonup>' | '=>' ) \<newline>
- ( '(' target ')' syntax ? + @'and' )
- ;
-
- printing_class: symbol_class ( '\<rightharpoonup>' | '=>' ) \<newline>
- ( '(' target ')' @{syntax string} ? + @'and' )
- ;
-
- printing_class_relation: symbol_class_relation ( '\<rightharpoonup>' | '=>' ) \<newline>
- ( '(' target ')' @{syntax string} ? + @'and' )
- ;
-
- printing_class_instance: symbol_class_instance ( '\<rightharpoonup>' | '=>' ) \<newline>
- ( '(' target ')' '-' ? + @'and' )
- ;
-
- printing_module: symbol_module ( '\<rightharpoonup>' | '=>' ) \<newline>
- ( '(' target ')' ( @{syntax string} ( @'attach' ( const + ) ) ? ) ? + @'and' )
- ;
-
- @@{command (HOL) code_printing} ( ( printing_const | printing_typeconstructor
- | printing_class | printing_class_relation | printing_class_instance
- | printing_module ) + '|' )
- ;
-
- @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
- | symbol_class | symbol_class_relation | symbol_class_instance
- | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \<newline>
- ( '(' target ')' @{syntax string} ? + @'and' ) + '|' )
- ;
-
- @@{command (HOL) code_monad} const const target
- ;
-
- @@{command (HOL) code_reflect} @{syntax string} \<newline>
- ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \<newline>
- ( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?
- ;
-
- @@{command (HOL) code_pred} \<newline> ('(' @'modes' ':' modedecl ')')? \<newline> const
- ;
-
- modedecl: (modes | ((const ':' modes) \<newline>
- (@'and' ((const ':' modes @'and') +))?))
- ;
-
- modes: mode @'as' const
- \<close>}
-
- \begin{description}
-
- \item @{command (HOL) "export_code"} generates code for a given list
- of constants in the specified target language(s). If no
- serialization instruction is given, only abstract code is generated
- internally.
-
- Constants may be specified by giving them literally, referring to
- all executable constants within a certain theory by giving @{text
- "name._"}, or referring to \emph{all} executable constants currently
- available by giving @{text "_"}.
-
- By default, exported identifiers are minimized per module. This
- can be suppressed by prepending @{keyword "open"} before the list
- of contants.
-
- By default, for each involved theory one corresponding name space
- module is generated. Alternatively, a module name may be specified
- after the @{keyword "module_name"} keyword; then \emph{all} code is
- placed in this module.
-
- For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
- refers to a single file; for \emph{Haskell}, it refers to a whole
- directory, where code is generated in multiple files reflecting the
- module hierarchy. Omitting the file specification denotes standard
- output.
-
- Serializers take an optional list of arguments in parentheses.
- For \emph{Haskell} a module name prefix may be given using the
- ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
- ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
- datatype declaration.
-
- \item @{attribute (HOL) code} declare code equations for code
- generation. Variant @{text "code equation"} declares a conventional
- equation as code equation. Variants @{text "code abstype"} and
- @{text "code abstract"} declare abstract datatype certificates or
- code equations on abstract datatype representations respectively.
- Vanilla @{text "code"} falls back to @{text "code equation"}
- or @{text "code abstype"} depending on the syntactic shape
- of the underlying equation. Variant @{text "code del"}
- deselects a code equation for code generation.
-
- Variants @{text "code drop:"} and @{text "code abort:"} take
- a list of constant as arguments and drop all code equations declared
- for them. In the case of {text abort}, these constants then are
- are not required to have a definition by means of code equations;
- if needed these are implemented by program abort (exception) instead.
-
- Usually packages introducing code equations provide a reasonable
- default setup for selection.
-
- \item @{command (HOL) "code_datatype"} specifies a constructor set
- for a logical type.
-
- \item @{command (HOL) "print_codesetup"} gives an overview on
- selected code equations and code generator datatypes.
-
- \item @{attribute (HOL) code_unfold} declares (or with option
- ``@{text "del"}'' removes) theorems which during preprocessing
- are applied as rewrite rules to any code equation or evaluation
- input.
-
- \item @{attribute (HOL) code_post} declares (or with option ``@{text
- "del"}'' removes) theorems which are applied as rewrite rules to any
- result of an evaluation.
-
- \item @{attribute (HOL) code_abbrev} declares equations which are
- applied as rewrite rules to any result of an evaluation and
- symmetrically during preprocessing to any code equation or evaluation
- input.
-
- \item @{command (HOL) "print_codeproc"} prints the setup of the code
- generator preprocessor.
-
- \item @{command (HOL) "code_thms"} prints a list of theorems
- representing the corresponding program containing all given
- constants after preprocessing.
-
- \item @{command (HOL) "code_deps"} visualizes dependencies of
- theorems representing the corresponding program containing all given
- constants after preprocessing.
-
- \item @{command (HOL) "code_reserved"} declares a list of names as
- reserved for a given target, preventing it to be shadowed by any
- generated code.
-
- \item @{command (HOL) "code_printing"} associates a series of symbols
- (constants, type constructors, classes, class relations, instances,
- module names) with target-specific serializations; omitting a serialization
- deletes an existing serialization.
-
- \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
- to generate monadic code for Haskell.
-
- \item @{command (HOL) "code_identifier"} associates a a series of symbols
- (constants, type constructors, classes, class relations, instances,
- module names) with target-specific hints how these symbols shall be named.
- These hints gain precedence over names for symbols with no hints at all.
- Conflicting hints are subject to name disambiguation.
- \emph{Warning:} It is at the discretion
- of the user to ensure that name prefixes of identifiers in compound
- statements like type classes or datatypes are still the same.
-
- \item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
- argument compiles code into the system runtime environment and
- modifies the code generator setup that future invocations of system
- runtime code generation referring to one of the ``@{text
- "datatypes"}'' or ``@{text "functions"}'' entities use these
- precompiled entities. With a ``@{text "file"}'' argument, the
- corresponding code is generated into that specified file without
- modifying the code generator setup.
-
- \item @{command (HOL) "code_pred"} creates code equations for a
- predicate given a set of introduction rules. Optional mode
- annotations determine which arguments are supposed to be input or
- output. If alternative introduction rules are declared, one must
- prove a corresponding elimination rule.
-
- \end{description}
-*}
-
-end