src/Doc/IsarRef/HOL_Specific.thy
 author haftmann Sat Jun 15 17:19:23 2013 +0200 (2013-06-15) changeset 52378 08dbf9ff2140 parent 50879 fc394c83e490 child 52435 6646bb548c6b permissions -rw-r--r--
documentation on code_printing and code_identifier
     1 theory HOL_Specific

     2 imports Base Main "~~/src/HOL/Library/Old_Recdef"

     3 begin

     4

     5 chapter {* Higher-Order Logic *}

     6

     7 text {* Isabelle/HOL is based on Higher-Order Logic, a polymorphic

     8   version of Church's Simple Theory of Types.  HOL can be best

     9   understood as a simply-typed version of classical set theory.  The

    10   logic was first implemented in Gordon's HOL system

    11   \cite{mgordon-hol}.  It extends Church's original logic

    12   \cite{church40} by explicit type variables (naive polymorphism) and

    13   a sound axiomatization scheme for new types based on subsets of

    14   existing types.

    15

    16   Andrews's book \cite{andrews86} is a full description of the

    17   original Church-style higher-order logic, with proofs of correctness

    18   and completeness wrt.\ certain set-theoretic interpretations.  The

    19   particular extensions of Gordon-style HOL are explained semantically

    20   in two chapters of the 1993 HOL book \cite{pitts93}.

    21

    22   Experience with HOL over decades has demonstrated that higher-order

    23   logic is widely applicable in many areas of mathematics and computer

    24   science.  In a sense, Higher-Order Logic is simpler than First-Order

    25   Logic, because there are fewer restrictions and special cases.  Note

    26   that HOL is \emph{weaker} than FOL with axioms for ZF set theory,

    27   which is traditionally considered the standard foundation of regular

    28   mathematics, but for most applications this does not matter.  If you

    29   prefer ML to Lisp, you will probably prefer HOL to ZF.

    30

    31   \medskip The syntax of HOL follows @{text "\<lambda>"}-calculus and

    32   functional programming.  Function application is curried.  To apply

    33   the function @{text f} of type @{text "\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"} to the

    34   arguments @{text a} and @{text b} in HOL, you simply write @{text "f

    35   a b"} (as in ML or Haskell).  There is no apply'' operator; the

    36   existing application of the Pure @{text "\<lambda>"}-calculus is re-used.

    37   Note that in HOL @{text "f (a, b)"} means @{text "f"} applied to

    38   the pair @{text "(a, b)"} (which is notation for @{text "Pair a

    39   b"}).  The latter typically introduces extra formal efforts that can

    40   be avoided by currying functions by default.  Explicit tuples are as

    41   infrequent in HOL formalizations as in good ML or Haskell programs.

    42

    43   \medskip Isabelle/HOL has a distinct feel, compared to other

    44   object-logics like Isabelle/ZF.  It identifies object-level types

    45   with meta-level types, taking advantage of the default

    46   type-inference mechanism of Isabelle/Pure.  HOL fully identifies

    47   object-level functions with meta-level functions, with native

    48   abstraction and application.

    49

    50   These identifications allow Isabelle to support HOL particularly

    51   nicely, but they also mean that HOL requires some sophistication

    52   from the user.  In particular, an understanding of Hindley-Milner

    53   type-inference with type-classes, which are both used extensively in

    54   the standard libraries and applications.  Beginners can set

    55   @{attribute show_types} or even @{attribute show_sorts} to get more

    56   explicit information about the result of type-inference.  *}

    57

    58

    59 chapter {* Derived specification elements *}

    60

    61 section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}

    62

    63 text {*

    64   \begin{matharray}{rcl}

    65     @{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

    66     @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

    67     @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

    68     @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

    69     @{command_def "print_inductives"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

    70     @{attribute_def (HOL) mono} & : & @{text attribute} \\

    71   \end{matharray}

    72

    73   An \emph{inductive definition} specifies the least predicate or set

    74   @{text R} closed under given rules: applying a rule to elements of

    75   @{text R} yields a result within @{text R}.  For example, a

    76   structural operational semantics is an inductive definition of an

    77   evaluation relation.

    78

    79   Dually, a \emph{coinductive definition} specifies the greatest

    80   predicate or set @{text R} that is consistent with given rules:

    81   every element of @{text R} can be seen as arising by applying a rule

    82   to elements of @{text R}.  An important example is using

    83   bisimulation relations to formalise equivalence of processes and

    84   infinite data structures.

    85

    86   Both inductive and coinductive definitions are based on the

    87   Knaster-Tarski fixed-point theorem for complete lattices.  The

    88   collection of introduction rules given by the user determines a

    89   functor on subsets of set-theoretic relations.  The required

    90   monotonicity of the recursion scheme is proven as a prerequisite to

    91   the fixed-point definition and the resulting consequences.  This

    92   works by pushing inclusion through logical connectives and any other

    93   operator that might be wrapped around recursive occurrences of the

    94   defined relation: there must be a monotonicity theorem of the form

    95   @{text "A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B"}, for each premise @{text "\<M> R t"} in an

    96   introduction rule.  The default rule declarations of Isabelle/HOL

    97   already take care of most common situations.

    98

    99   @{rail "

   100     (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |

   101       @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})

   102     @{syntax target}? \\

   103     @{syntax \"fixes\"} (@'for' @{syntax \"fixes\"})? (@'where' clauses)? \\

   104     (@'monos' @{syntax thmrefs})?

   105     ;

   106     clauses: (@{syntax thmdecl}? @{syntax prop} + '|')

   107     ;

   108     @@{attribute (HOL) mono} (() | 'add' | 'del')

   109   "}

   110

   111   \begin{description}

   112

   113   \item @{command (HOL) "inductive"} and @{command (HOL)

   114   "coinductive"} define (co)inductive predicates from the introduction

   115   rules.

   116

   117   The propositions given as @{text "clauses"} in the @{keyword

   118   "where"} part are either rules of the usual @{text "\<And>/\<Longrightarrow>"} format

   119   (with arbitrary nesting), or equalities using @{text "\<equiv>"}.  The

   120   latter specifies extra-logical abbreviations in the sense of

   121   @{command_ref abbreviation}.  Introducing abstract syntax

   122   simultaneously with the actual introduction rules is occasionally

   123   useful for complex specifications.

   124

   125   The optional @{keyword "for"} part contains a list of parameters of

   126   the (co)inductive predicates that remain fixed throughout the

   127   definition, in contrast to arguments of the relation that may vary

   128   in each occurrence within the given @{text "clauses"}.

   129

   130   The optional @{keyword "monos"} declaration contains additional

   131   \emph{monotonicity theorems}, which are required for each operator

   132   applied to a recursive set in the introduction rules.

   133

   134   \item @{command (HOL) "inductive_set"} and @{command (HOL)

   135   "coinductive_set"} are wrappers for to the previous commands for

   136   native HOL predicates.  This allows to define (co)inductive sets,

   137   where multiple arguments are simulated via tuples.

   138

   139   \item @{command "print_inductives"} prints (co)inductive definitions and

   140   monotonicity rules.

   141

   142   \item @{attribute (HOL) mono} declares monotonicity rules in the

   143   context.  These rule are involved in the automated monotonicity

   144   proof of the above inductive and coinductive definitions.

   145

   146   \end{description}

   147 *}

   148

   149

   150 subsection {* Derived rules *}

   151

   152 text {* A (co)inductive definition of @{text R} provides the following

   153   main theorems:

   154

   155   \begin{description}

   156

   157   \item @{text R.intros} is the list of introduction rules as proven

   158   theorems, for the recursive predicates (or sets).  The rules are

   159   also available individually, using the names given them in the

   160   theory file;

   161

   162   \item @{text R.cases} is the case analysis (or elimination) rule;

   163

   164   \item @{text R.induct} or @{text R.coinduct} is the (co)induction

   165   rule;

   166

   167   \item @{text R.simps} is the equation unrolling the fixpoint of the

   168   predicate one step.

   169

   170   \end{description}

   171

   172   When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are

   173   defined simultaneously, the list of introduction rules is called

   174   @{text "R\<^sub>1_\<dots>_R\<^sub>n.intros"}, the case analysis rules are

   175   called @{text "R\<^sub>1.cases, \<dots>, R\<^sub>n.cases"}, and the list

   176   of mutual induction rules is called @{text

   177   "R\<^sub>1_\<dots>_R\<^sub>n.inducts"}.

   178 *}

   179

   180

   181 subsection {* Monotonicity theorems *}

   182

   183 text {* The context maintains a default set of theorems that are used

   184   in monotonicity proofs.  New rules can be declared via the

   185   @{attribute (HOL) mono} attribute.  See the main Isabelle/HOL

   186   sources for some examples.  The general format of such monotonicity

   187   theorems is as follows:

   188

   189   \begin{itemize}

   190

   191   \item Theorems of the form @{text "A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B"}, for proving

   192   monotonicity of inductive definitions whose introduction rules have

   193   premises involving terms such as @{text "\<M> R t"}.

   194

   195   \item Monotonicity theorems for logical operators, which are of the

   196   general form @{text "(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>"}.  For example, in

   197   the case of the operator @{text "\<or>"}, the corresponding theorem is

   198   $  199 \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"}}   200$

   201

   202   \item De Morgan style equations for reasoning about the polarity''

   203   of expressions, e.g.

   204   $  205 @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad   206 @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}   207$

   208

   209   \item Equations for reducing complex operators to more primitive

   210   ones whose monotonicity can easily be proved, e.g.

   211   $  212 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad   213 @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}   214$

   215

   216   \end{itemize}

   217 *}

   218

   219 subsubsection {* Examples *}

   220

   221 text {* The finite powerset operator can be defined inductively like this: *}

   222

   223 inductive_set Fin :: "'a set \<Rightarrow> 'a set set" for A :: "'a set"

   224 where

   225   empty: "{} \<in> Fin A"

   226 | insert: "a \<in> A \<Longrightarrow> B \<in> Fin A \<Longrightarrow> insert a B \<in> Fin A"

   227

   228 text {* The accessible part of a relation is defined as follows: *}

   229

   230 inductive acc :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"

   231   for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<prec>" 50)

   232 where acc: "(\<And>y. y \<prec> x \<Longrightarrow> acc r y) \<Longrightarrow> acc r x"

   233

   234 text {* Common logical connectives can be easily characterized as

   235 non-recursive inductive definitions with parameters, but without

   236 arguments. *}

   237

   238 inductive AND for A B :: bool

   239 where "A \<Longrightarrow> B \<Longrightarrow> AND A B"

   240

   241 inductive OR for A B :: bool

   242 where "A \<Longrightarrow> OR A B"

   243   | "B \<Longrightarrow> OR A B"

   244

   245 inductive EXISTS for B :: "'a \<Rightarrow> bool"

   246 where "B a \<Longrightarrow> EXISTS B"

   247

   248 text {* Here the @{text "cases"} or @{text "induct"} rules produced by

   249   the @{command inductive} package coincide with the expected

   250   elimination rules for Natural Deduction.  Already in the original

   251   article by Gerhard Gentzen \cite{Gentzen:1935} there is a hint that

   252   each connective can be characterized by its introductions, and the

   253   elimination can be constructed systematically. *}

   254

   255

   256 section {* Recursive functions \label{sec:recursion} *}

   257

   258 text {*

   259   \begin{matharray}{rcl}

   260     @{command_def (HOL) "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   261     @{command_def (HOL) "fun"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   262     @{command_def (HOL) "function"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

   263     @{command_def (HOL) "termination"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

   264   \end{matharray}

   265

   266   @{rail "

   267     @@{command (HOL) primrec} @{syntax target}? @{syntax \"fixes\"} @'where' equations

   268     ;

   269     (@@{command (HOL) fun} | @@{command (HOL) function}) @{syntax target}? functionopts?

   270       @{syntax \"fixes\"} \\ @'where' equations

   271     ;

   272

   273     equations: (@{syntax thmdecl}? @{syntax prop} + '|')

   274     ;

   275     functionopts: '(' (('sequential' | 'domintros') + ',') ')'

   276     ;

   277     @@{command (HOL) termination} @{syntax term}?

   278   "}

   279

   280   \begin{description}

   281

   282   \item @{command (HOL) "primrec"} defines primitive recursive

   283   functions over datatypes (see also @{command_ref (HOL) datatype} and

   284   @{command_ref (HOL) rep_datatype}).  The given @{text equations}

   285   specify reduction rules that are produced by instantiating the

   286   generic combinator for primitive recursion that is available for

   287   each datatype.

   288

   289   Each equation needs to be of the form:

   290

   291   @{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"}

   292

   293   such that @{text C} is a datatype constructor, @{text rhs} contains

   294   only the free variables on the left-hand side (or from the context),

   295   and all recursive occurrences of @{text "f"} in @{text "rhs"} are of

   296   the form @{text "f \<dots> y\<^sub>i \<dots>"} for some @{text i}.  At most one

   297   reduction rule for each constructor can be given.  The order does

   298   not matter.  For missing constructors, the function is defined to

   299   return a default value, but this equation is made difficult to

   300   access for users.

   301

   302   The reduction rules are declared as @{attribute simp} by default,

   303   which enables standard proof methods like @{method simp} and

   304   @{method auto} to normalize expressions of @{text "f"} applied to

   305   datatype constructions, by simulating symbolic computation via

   306   rewriting.

   307

   308   \item @{command (HOL) "function"} defines functions by general

   309   wellfounded recursion. A detailed description with examples can be

   310   found in \cite{isabelle-function}. The function is specified by a

   311   set of (possibly conditional) recursive equations with arbitrary

   312   pattern matching. The command generates proof obligations for the

   313   completeness and the compatibility of patterns.

   314

   315   The defined function is considered partial, and the resulting

   316   simplification rules (named @{text "f.psimps"}) and induction rule

   317   (named @{text "f.pinduct"}) are guarded by a generated domain

   318   predicate @{text "f_dom"}. The @{command (HOL) "termination"}

   319   command can then be used to establish that the function is total.

   320

   321   \item @{command (HOL) "fun"} is a shorthand notation for @{command

   322   (HOL) "function"}~@{text "(sequential)"}, followed by automated

   323   proof attempts regarding pattern matching and termination.  See

   324   \cite{isabelle-function} for further details.

   325

   326   \item @{command (HOL) "termination"}~@{text f} commences a

   327   termination proof for the previously defined function @{text f}.  If

   328   this is omitted, the command refers to the most recent function

   329   definition.  After the proof is closed, the recursive equations and

   330   the induction principle is established.

   331

   332   \end{description}

   333

   334   Recursive definitions introduced by the @{command (HOL) "function"}

   335   command accommodate reasoning by induction (cf.\ @{method induct}):

   336   rule @{text "f.induct"} refers to a specific induction rule, with

   337   parameters named according to the user-specified equations. Cases

   338   are numbered starting from 1.  For @{command (HOL) "primrec"}, the

   339   induction principle coincides with structural recursion on the

   340   datatype where the recursion is carried out.

   341

   342   The equations provided by these packages may be referred later as

   343   theorem list @{text "f.simps"}, where @{text f} is the (collective)

   344   name of the functions defined.  Individual equations may be named

   345   explicitly as well.

   346

   347   The @{command (HOL) "function"} command accepts the following

   348   options.

   349

   350   \begin{description}

   351

   352   \item @{text sequential} enables a preprocessor which disambiguates

   353   overlapping patterns by making them mutually disjoint.  Earlier

   354   equations take precedence over later ones.  This allows to give the

   355   specification in a format very similar to functional programming.

   356   Note that the resulting simplification and induction rules

   357   correspond to the transformed specification, not the one given

   358   originally. This usually means that each equation given by the user

   359   may result in several theorems.  Also note that this automatic

   360   transformation only works for ML-style datatype patterns.

   361

   362   \item @{text domintros} enables the automated generation of

   363   introduction rules for the domain predicate. While mostly not

   364   needed, they can be helpful in some proofs about partial functions.

   365

   366   \end{description}

   367 *}

   368

   369 subsubsection {* Example: evaluation of expressions *}

   370

   371 text {* Subsequently, we define mutual datatypes for arithmetic and

   372   boolean expressions, and use @{command primrec} for evaluation

   373   functions that follow the same recursive structure. *}

   374

   375 datatype 'a aexp =

   376     IF "'a bexp"  "'a aexp"  "'a aexp"

   377   | Sum "'a aexp"  "'a aexp"

   378   | Diff "'a aexp"  "'a aexp"

   379   | Var 'a

   380   | Num nat

   381 and 'a bexp =

   382     Less "'a aexp"  "'a aexp"

   383   | And "'a bexp"  "'a bexp"

   384   | Neg "'a bexp"

   385

   386

   387 text {* \medskip Evaluation of arithmetic and boolean expressions *}

   388

   389 primrec evala :: "('a \<Rightarrow> nat) \<Rightarrow> 'a aexp \<Rightarrow> nat"

   390   and evalb :: "('a \<Rightarrow> nat) \<Rightarrow> 'a bexp \<Rightarrow> bool"

   391 where

   392   "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"

   393 | "evala env (Sum a1 a2) = evala env a1 + evala env a2"

   394 | "evala env (Diff a1 a2) = evala env a1 - evala env a2"

   395 | "evala env (Var v) = env v"

   396 | "evala env (Num n) = n"

   397 | "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"

   398 | "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"

   399 | "evalb env (Neg b) = (\<not> evalb env b)"

   400

   401 text {* Since the value of an expression depends on the value of its

   402   variables, the functions @{const evala} and @{const evalb} take an

   403   additional parameter, an \emph{environment} that maps variables to

   404   their values.

   405

   406   \medskip Substitution on expressions can be defined similarly.  The

   407   mapping @{text f} of type @{typ "'a \<Rightarrow> 'a aexp"} given as a

   408   parameter is lifted canonically on the types @{typ "'a aexp"} and

   409   @{typ "'a bexp"}, respectively.

   410 *}

   411

   412 primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"

   413   and substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp"

   414 where

   415   "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"

   416 | "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"

   417 | "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"

   418 | "substa f (Var v) = f v"

   419 | "substa f (Num n) = Num n"

   420 | "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"

   421 | "substb f (And b1 b2) = And (substb f b1) (substb f b2)"

   422 | "substb f (Neg b) = Neg (substb f b)"

   423

   424 text {* In textbooks about semantics one often finds substitution

   425   theorems, which express the relationship between substitution and

   426   evaluation.  For @{typ "'a aexp"} and @{typ "'a bexp"}, we can prove

   427   such a theorem by mutual induction, followed by simplification.

   428 *}

   429

   430 lemma subst_one:

   431   "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"

   432   "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"

   433   by (induct a and b) simp_all

   434

   435 lemma subst_all:

   436   "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"

   437   "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"

   438   by (induct a and b) simp_all

   439

   440

   441 subsubsection {* Example: a substitution function for terms *}

   442

   443 text {* Functions on datatypes with nested recursion are also defined

   444   by mutual primitive recursion. *}

   445

   446 datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"

   447

   448 text {* A substitution function on type @{typ "('a, 'b) term"} can be

   449   defined as follows, by working simultaneously on @{typ "('a, 'b)

   450   term list"}: *}

   451

   452 primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term" and

   453   subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"

   454 where

   455   "subst_term f (Var a) = f a"

   456 | "subst_term f (App b ts) = App b (subst_term_list f ts)"

   457 | "subst_term_list f [] = []"

   458 | "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"

   459

   460 text {* The recursion scheme follows the structure of the unfolded

   461   definition of type @{typ "('a, 'b) term"}.  To prove properties of this

   462   substitution function, mutual induction is needed:

   463 *}

   464

   465 lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)" and

   466   "subst_term_list (subst_term f1 \<circ> f2) ts = subst_term_list f1 (subst_term_list f2 ts)"

   467   by (induct t and ts) simp_all

   468

   469

   470 subsubsection {* Example: a map function for infinitely branching trees *}

   471

   472 text {* Defining functions on infinitely branching datatypes by

   473   primitive recursion is just as easy.

   474 *}

   475

   476 datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"

   477

   478 primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"

   479 where

   480   "map_tree f (Atom a) = Atom (f a)"

   481 | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"

   482

   483 text {* Note that all occurrences of functions such as @{text ts}

   484   above must be applied to an argument.  In particular, @{term

   485   "map_tree f \<circ> ts"} is not allowed here. *}

   486

   487 text {* Here is a simple composition lemma for @{term map_tree}: *}

   488

   489 lemma "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"

   490   by (induct t) simp_all

   491

   492

   493 subsection {* Proof methods related to recursive definitions *}

   494

   495 text {*

   496   \begin{matharray}{rcl}

   497     @{method_def (HOL) pat_completeness} & : & @{text method} \\

   498     @{method_def (HOL) relation} & : & @{text method} \\

   499     @{method_def (HOL) lexicographic_order} & : & @{text method} \\

   500     @{method_def (HOL) size_change} & : & @{text method} \\

   501     @{method_def (HOL) induction_schema} & : & @{text method} \\

   502   \end{matharray}

   503

   504   @{rail "

   505     @@{method (HOL) relation} @{syntax term}

   506     ;

   507     @@{method (HOL) lexicographic_order} (@{syntax clasimpmod} * )

   508     ;

   509     @@{method (HOL) size_change} ( orders (@{syntax clasimpmod} * ) )

   510     ;

   511     @@{method (HOL) induction_schema}

   512     ;

   513     orders: ( 'max' | 'min' | 'ms' ) *

   514   "}

   515

   516   \begin{description}

   517

   518   \item @{method (HOL) pat_completeness} is a specialized method to

   519   solve goals regarding the completeness of pattern matching, as

   520   required by the @{command (HOL) "function"} package (cf.\

   521   \cite{isabelle-function}).

   522

   523   \item @{method (HOL) relation}~@{text R} introduces a termination

   524   proof using the relation @{text R}.  The resulting proof state will

   525   contain goals expressing that @{text R} is wellfounded, and that the

   526   arguments of recursive calls decrease with respect to @{text R}.

   527   Usually, this method is used as the initial proof step of manual

   528   termination proofs.

   529

   530   \item @{method (HOL) "lexicographic_order"} attempts a fully

   531   automated termination proof by searching for a lexicographic

   532   combination of size measures on the arguments of the function. The

   533   method accepts the same arguments as the @{method auto} method,

   534   which it uses internally to prove local descents.  The @{syntax

   535   clasimpmod} modifiers are accepted (as for @{method auto}).

   536

   537   In case of failure, extensive information is printed, which can help

   538   to analyse the situation (cf.\ \cite{isabelle-function}).

   539

   540   \item @{method (HOL) "size_change"} also works on termination goals,

   541   using a variation of the size-change principle, together with a

   542   graph decomposition technique (see \cite{krauss_phd} for details).

   543   Three kinds of orders are used internally: @{text max}, @{text min},

   544   and @{text ms} (multiset), which is only available when the theory

   545   @{text Multiset} is loaded. When no order kinds are given, they are

   546   tried in order. The search for a termination proof uses SAT solving

   547   internally.

   548

   549   For local descent proofs, the @{syntax clasimpmod} modifiers are

   550   accepted (as for @{method auto}).

   551

   552   \item @{method (HOL) induction_schema} derives user-specified

   553   induction rules from well-founded induction and completeness of

   554   patterns. This factors out some operations that are done internally

   555   by the function package and makes them available separately. See

   556   @{file "~~/src/HOL/ex/Induction_Schema.thy"} for examples.

   557

   558   \end{description}

   559 *}

   560

   561

   562 subsection {* Functions with explicit partiality *}

   563

   564 text {*

   565   \begin{matharray}{rcl}

   566     @{command_def (HOL) "partial_function"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   567     @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\

   568   \end{matharray}

   569

   570   @{rail "

   571     @@{command (HOL) partial_function} @{syntax target}?

   572       '(' @{syntax nameref} ')' @{syntax \"fixes\"} \\

   573       @'where' @{syntax thmdecl}? @{syntax prop}

   574   "}

   575

   576   \begin{description}

   577

   578   \item @{command (HOL) "partial_function"}~@{text "(mode)"} defines

   579   recursive functions based on fixpoints in complete partial

   580   orders. No termination proof is required from the user or

   581   constructed internally. Instead, the possibility of non-termination

   582   is modelled explicitly in the result type, which contains an

   583   explicit bottom element.

   584

   585   Pattern matching and mutual recursion are currently not supported.

   586   Thus, the specification consists of a single function described by a

   587   single recursive equation.

   588

   589   There are no fixed syntactic restrictions on the body of the

   590   function, but the induced functional must be provably monotonic

   591   wrt.\ the underlying order.  The monotonicitity proof is performed

   592   internally, and the definition is rejected when it fails. The proof

   593   can be influenced by declaring hints using the

   594   @{attribute (HOL) partial_function_mono} attribute.

   595

   596   The mandatory @{text mode} argument specifies the mode of operation

   597   of the command, which directly corresponds to a complete partial

   598   order on the result type. By default, the following modes are

   599   defined:

   600

   601   \begin{description}

   602

   603   \item @{text option} defines functions that map into the @{type

   604   option} type. Here, the value @{term None} is used to model a

   605   non-terminating computation. Monotonicity requires that if @{term

   606   None} is returned by a recursive call, then the overall result must

   607   also be @{term None}. This is best achieved through the use of the

   608   monadic operator @{const "Option.bind"}.

   609

   610   \item @{text tailrec} defines functions with an arbitrary result

   611   type and uses the slightly degenerated partial order where @{term

   612   "undefined"} is the bottom element.  Now, monotonicity requires that

   613   if @{term undefined} is returned by a recursive call, then the

   614   overall result must also be @{term undefined}. In practice, this is

   615   only satisfied when each recursive call is a tail call, whose result

   616   is directly returned. Thus, this mode of operation allows the

   617   definition of arbitrary tail-recursive functions.

   618

   619   \end{description}

   620

   621   Experienced users may define new modes by instantiating the locale

   622   @{const "partial_function_definitions"} appropriately.

   623

   624   \item @{attribute (HOL) partial_function_mono} declares rules for

   625   use in the internal monononicity proofs of partial function

   626   definitions.

   627

   628   \end{description}

   629

   630 *}

   631

   632

   633 subsection {* Old-style recursive function definitions (TFL) *}

   634

   635 text {*

   636   \begin{matharray}{rcl}

   637     @{command_def (HOL) "recdef"} & : & @{text "theory \<rightarrow> theory)"} \\

   638     @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow> proof(prove)"} \\

   639   \end{matharray}

   640

   641   The old TFL commands @{command (HOL) "recdef"} and @{command (HOL)

   642   "recdef_tc"} for defining recursive are mostly obsolete; @{command

   643   (HOL) "function"} or @{command (HOL) "fun"} should be used instead.

   644

   645   @{rail "

   646     @@{command (HOL) recdef} ('(' @'permissive' ')')? \\

   647       @{syntax name} @{syntax term} (@{syntax prop} +) hints?

   648     ;

   649     recdeftc @{syntax thmdecl}? tc

   650     ;

   651     hints: '(' @'hints' ( recdefmod * ) ')'

   652     ;

   653     recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf')

   654       (() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod}

   655     ;

   656     tc: @{syntax nameref} ('(' @{syntax nat} ')')?

   657   "}

   658

   659   \begin{description}

   660

   661   \item @{command (HOL) "recdef"} defines general well-founded

   662   recursive functions (using the TFL package), see also

   663   \cite{isabelle-HOL}.  The @{text "(permissive)"}'' option tells

   664   TFL to recover from failed proof attempts, returning unfinished

   665   results.  The @{text recdef_simp}, @{text recdef_cong}, and @{text

   666   recdef_wf} hints refer to auxiliary rules to be used in the internal

   667   automated proof process of TFL.  Additional @{syntax clasimpmod}

   668   declarations may be given to tune the context of the Simplifier

   669   (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\

   670   \secref{sec:classical}).

   671

   672   \item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the

   673   proof for leftover termination condition number @{text i} (default

   674   1) as generated by a @{command (HOL) "recdef"} definition of

   675   constant @{text c}.

   676

   677   Note that in most cases, @{command (HOL) "recdef"} is able to finish

   678   its internal proofs without manual intervention.

   679

   680   \end{description}

   681

   682   \medskip Hints for @{command (HOL) "recdef"} may be also declared

   683   globally, using the following attributes.

   684

   685   \begin{matharray}{rcl}

   686     @{attribute_def (HOL) recdef_simp} & : & @{text attribute} \\

   687     @{attribute_def (HOL) recdef_cong} & : & @{text attribute} \\

   688     @{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\

   689   \end{matharray}

   690

   691   @{rail "

   692     (@@{attribute (HOL) recdef_simp} | @@{attribute (HOL) recdef_cong} |

   693       @@{attribute (HOL) recdef_wf}) (() | 'add' | 'del')

   694   "}

   695 *}

   696

   697

   698 section {* Datatypes \label{sec:hol-datatype} *}

   699

   700 text {*

   701   \begin{matharray}{rcl}

   702     @{command_def (HOL) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\

   703     @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\

   704   \end{matharray}

   705

   706   @{rail "

   707     @@{command (HOL) datatype} (spec + @'and')

   708     ;

   709     @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)

   710     ;

   711

   712     spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|')

   713     ;

   714     cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?

   715   "}

   716

   717   \begin{description}

   718

   719   \item @{command (HOL) "datatype"} defines inductive datatypes in

   720   HOL.

   721

   722   \item @{command (HOL) "rep_datatype"} represents existing types as

   723   datatypes.

   724

   725   For foundational reasons, some basic types such as @{typ nat}, @{typ

   726   "'a \<times> 'b"}, @{typ "'a + 'b"}, @{typ bool} and @{typ unit} are

   727   introduced by more primitive means using @{command_ref typedef}.  To

   728   recover the rich infrastructure of @{command datatype} (e.g.\ rules

   729   for @{method cases} and @{method induct} and the primitive recursion

   730   combinators), such types may be represented as actual datatypes

   731   later.  This is done by specifying the constructors of the desired

   732   type, and giving a proof of the induction rule, distinctness and

   733   injectivity of constructors.

   734

   735   For example, see @{file "~~/src/HOL/Sum_Type.thy"} for the

   736   representation of the primitive sum type as fully-featured datatype.

   737

   738   \end{description}

   739

   740   The generated rules for @{method induct} and @{method cases} provide

   741   case names according to the given constructors, while parameters are

   742   named after the types (see also \secref{sec:cases-induct}).

   743

   744   See \cite{isabelle-HOL} for more details on datatypes, but beware of

   745   the old-style theory syntax being used there!  Apart from proper

   746   proof methods for case-analysis and induction, there are also

   747   emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)

   748   induct_tac} available, see \secref{sec:hol-induct-tac}; these admit

   749   to refer directly to the internal structure of subgoals (including

   750   internally bound parameters).

   751 *}

   752

   753

   754 subsubsection {* Examples *}

   755

   756 text {* We define a type of finite sequences, with slightly different

   757   names than the existing @{typ "'a list"} that is already in @{theory

   758   Main}: *}

   759

   760 datatype 'a seq = Empty | Seq 'a "'a seq"

   761

   762 text {* We can now prove some simple lemma by structural induction: *}

   763

   764 lemma "Seq x xs \<noteq> xs"

   765 proof (induct xs arbitrary: x)

   766   case Empty

   767   txt {* This case can be proved using the simplifier: the freeness

   768     properties of the datatype are already declared as @{attribute

   769     simp} rules. *}

   770   show "Seq x Empty \<noteq> Empty"

   771     by simp

   772 next

   773   case (Seq y ys)

   774   txt {* The step case is proved similarly. *}

   775   show "Seq x (Seq y ys) \<noteq> Seq y ys"

   776     using Seq y ys \<noteq> ys by simp

   777 qed

   778

   779 text {* Here is a more succinct version of the same proof: *}

   780

   781 lemma "Seq x xs \<noteq> xs"

   782   by (induct xs arbitrary: x) simp_all

   783

   784

   785 section {* Records \label{sec:hol-record} *}

   786

   787 text {*

   788   In principle, records merely generalize the concept of tuples, where

   789   components may be addressed by labels instead of just position.  The

   790   logical infrastructure of records in Isabelle/HOL is slightly more

   791   advanced, though, supporting truly extensible record schemes.  This

   792   admits operations that are polymorphic with respect to record

   793   extension, yielding object-oriented'' effects like (single)

   794   inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for more

   795   details on object-oriented verification and record subtyping in HOL.

   796 *}

   797

   798

   799 subsection {* Basic concepts *}

   800

   801 text {*

   802   Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records

   803   at the level of terms and types.  The notation is as follows:

   804

   805   \begin{center}

   806   \begin{tabular}{l|l|l}

   807     & record terms & record types \\ \hline

   808     fixed & @{text "\<lparr>x = a, y = b\<rparr>"} & @{text "\<lparr>x :: A, y :: B\<rparr>"} \\

   809     schematic & @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} &

   810       @{text "\<lparr>x :: A, y :: B, \<dots> :: M\<rparr>"} \\

   811   \end{tabular}

   812   \end{center}

   813

   814   \noindent The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text

   815   "(| x = a |)"}.

   816

   817   A fixed record @{text "\<lparr>x = a, y = b\<rparr>"} has field @{text x} of value

   818   @{text a} and field @{text y} of value @{text b}.  The corresponding

   819   type is @{text "\<lparr>x :: A, y :: B\<rparr>"}, assuming that @{text "a :: A"}

   820   and @{text "b :: B"}.

   821

   822   A record scheme like @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} contains fields

   823   @{text x} and @{text y} as before, but also possibly further fields

   824   as indicated by the @{text "\<dots>"}'' notation (which is actually part

   825   of the syntax).  The improper field @{text "\<dots>"}'' of a record

   826   scheme is called the \emph{more part}.  Logically it is just a free

   827   variable, which is occasionally referred to as row variable'' in

   828   the literature.  The more part of a record scheme may be

   829   instantiated by zero or more further components.  For example, the

   830   previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z =

   831   c, \<dots> = m'\<rparr>"}, where @{text m'} refers to a different more part.

   832   Fixed records are special instances of record schemes, where

   833   @{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"}

   834   element.  In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation

   835   for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}.

   836

   837   \medskip Two key observations make extensible records in a simply

   838   typed language like HOL work out:

   839

   840   \begin{enumerate}

   841

   842   \item the more part is internalized, as a free term or type

   843   variable,

   844

   845   \item field names are externalized, they cannot be accessed within

   846   the logic as first-class values.

   847

   848   \end{enumerate}

   849

   850   \medskip In Isabelle/HOL record types have to be defined explicitly,

   851   fixing their field names and types, and their (optional) parent

   852   record.  Afterwards, records may be formed using above syntax, while

   853   obeying the canonical order of fields as given by their declaration.

   854   The record package provides several standard operations like

   855   selectors and updates.  The common setup for various generic proof

   856   tools enable succinct reasoning patterns.  See also the Isabelle/HOL

   857   tutorial \cite{isabelle-hol-book} for further instructions on using

   858   records in practice.

   859 *}

   860

   861

   862 subsection {* Record specifications *}

   863

   864 text {*

   865   \begin{matharray}{rcl}

   866     @{command_def (HOL) "record"} & : & @{text "theory \<rightarrow> theory"} \\

   867   \end{matharray}

   868

   869   @{rail "

   870     @@{command (HOL) record} @{syntax typespec_sorts} '=' \\

   871       (@{syntax type} '+')? (constdecl +)

   872     ;

   873     constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?

   874   "}

   875

   876   \begin{description}

   877

   878   \item @{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1

   879   \<dots> c\<^sub>n :: \<sigma>\<^sub>n"} defines extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"},

   880   derived from the optional parent record @{text "\<tau>"} by adding new

   881   field components @{text "c\<^sub>i :: \<sigma>\<^sub>i"} etc.

   882

   883   The type variables of @{text "\<tau>"} and @{text "\<sigma>\<^sub>i"} need to be

   884   covered by the (distinct) parameters @{text "\<alpha>\<^sub>1, \<dots>,

   885   \<alpha>\<^sub>m"}.  Type constructor @{text t} has to be new, while @{text

   886   \<tau>} needs to specify an instance of an existing record type.  At

   887   least one new field @{text "c\<^sub>i"} has to be specified.

   888   Basically, field names need to belong to a unique record.  This is

   889   not a real restriction in practice, since fields are qualified by

   890   the record name internally.

   891

   892   The parent record specification @{text \<tau>} is optional; if omitted

   893   @{text t} becomes a root record.  The hierarchy of all records

   894   declared within a theory context forms a forest structure, i.e.\ a

   895   set of trees starting with a root record each.  There is no way to

   896   merge multiple parent records!

   897

   898   For convenience, @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} is made a

   899   type abbreviation for the fixed record type @{text "\<lparr>c\<^sub>1 ::

   900   \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"}, likewise is @{text

   901   "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>) t_scheme"} made an abbreviation for

   902   @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> ::

   903   \<zeta>\<rparr>"}.

   904

   905   \end{description}

   906 *}

   907

   908

   909 subsection {* Record operations *}

   910

   911 text {*

   912   Any record definition of the form presented above produces certain

   913   standard operations.  Selectors and updates are provided for any

   914   field, including the improper one @{text more}''.  There are also

   915   cumulative record constructor functions.  To simplify the

   916   presentation below, we assume for now that @{text "(\<alpha>\<^sub>1, \<dots>,

   917   \<alpha>\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 ::

   918   \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"}.

   919

   920   \medskip \textbf{Selectors} and \textbf{updates} are available for

   921   any field (including @{text more}''):

   922

   923   \begin{matharray}{lll}

   924     @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\

   925     @{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>"} \\

   926   \end{matharray}

   927

   928   There is special syntax for application of updates: @{text "r\<lparr>x :=

   929   a\<rparr>"} abbreviates term @{text "x_update a r"}.  Further notation for

   930   repeated updates is also available: @{text "r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z :=

   931   c\<rparr>"} may be written @{text "r\<lparr>x := a, y := b, z := c\<rparr>"}.  Note that

   932   because of postfix notation the order of fields shown here is

   933   reverse than in the actual term.  Since repeated updates are just

   934   function applications, fields may be freely permuted in @{text "\<lparr>x

   935   := a, y := b, z := c\<rparr>"}, as far as logical equality is concerned.

   936   Thus commutativity of independent updates can be proven within the

   937   logic for any two fields, but not as a general theorem.

   938

   939   \medskip The \textbf{make} operation provides a cumulative record

   940   constructor function:

   941

   942   \begin{matharray}{lll}

   943     @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\

   944   \end{matharray}

   945

   946   \medskip We now reconsider the case of non-root records, which are

   947   derived of some parent.  In general, the latter may depend on

   948   another parent as well, resulting in a list of \emph{ancestor

   949   records}.  Appending the lists of fields of all ancestors results in

   950   a certain field prefix.  The record package automatically takes care

   951   of this by lifting operations over this context of ancestor fields.

   952   Assuming that @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} has ancestor

   953   fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"},

   954   the above record operations will get the following types:

   955

   956   \medskip

   957   \begin{tabular}{lll}

   958     @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\

   959     @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow>

   960       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>

   961       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\

   962     @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>

   963       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\

   964   \end{tabular}

   965   \medskip

   966

   967   \noindent Some further operations address the extension aspect of a

   968   derived record scheme specifically: @{text "t.fields"} produces a

   969   record fragment consisting of exactly the new fields introduced here

   970   (the result may serve as a more part elsewhere); @{text "t.extend"}

   971   takes a fixed record and adds a given more part; @{text

   972   "t.truncate"} restricts a record scheme to a fixed record.

   973

   974   \medskip

   975   \begin{tabular}{lll}

   976     @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\

   977     @{text "t.extend"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow>

   978       \<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\

   979     @{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>"} \\

   980   \end{tabular}

   981   \medskip

   982

   983   \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide

   984   for root records.

   985 *}

   986

   987

   988 subsection {* Derived rules and proof tools *}

   989

   990 text {*

   991   The record package proves several results internally, declaring

   992   these facts to appropriate proof tools.  This enables users to

   993   reason about record structures quite conveniently.  Assume that

   994   @{text t} is a record type as specified above.

   995

   996   \begin{enumerate}

   997

   998   \item Standard conversions for selectors or updates applied to

   999   record constructor terms are made part of the default Simplifier

  1000   context; thus proofs by reduction of basic operations merely require

  1001   the @{method simp} method without further arguments.  These rules

  1002   are available as @{text "t.simps"}, too.

  1003

  1004   \item Selectors applied to updated records are automatically reduced

  1005   by an internal simplification procedure, which is also part of the

  1006   standard Simplifier setup.

  1007

  1008   \item Inject equations of a form analogous to @{prop "(x, y) = (x',

  1009   y') \<equiv> x = x' \<and> y = y'"} are declared to the Simplifier and Classical

  1010   Reasoner as @{attribute iff} rules.  These rules are available as

  1011   @{text "t.iffs"}.

  1012

  1013   \item The introduction rule for record equality analogous to @{text

  1014   "x r = x r' \<Longrightarrow> y r = y r' \<dots> \<Longrightarrow> r = r'"} is declared to the Simplifier,

  1015   and as the basic rule context as @{attribute intro}@{text "?"}''.

  1016   The rule is called @{text "t.equality"}.

  1017

  1018   \item Representations of arbitrary record expressions as canonical

  1019   constructor terms are provided both in @{method cases} and @{method

  1020   induct} format (cf.\ the generic proof methods of the same name,

  1021   \secref{sec:cases-induct}).  Several variations are available, for

  1022   fixed records, record schemes, more parts etc.

  1023

  1024   The generic proof methods are sufficiently smart to pick the most

  1025   sensible rule according to the type of the indicated record

  1026   expression: users just need to apply something like @{text "(cases

  1027   r)"}'' to a certain proof problem.

  1028

  1029   \item The derived record operations @{text "t.make"}, @{text

  1030   "t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not}

  1031   treated automatically, but usually need to be expanded by hand,

  1032   using the collective fact @{text "t.defs"}.

  1033

  1034   \end{enumerate}

  1035 *}

  1036

  1037

  1038 subsubsection {* Examples *}

  1039

  1040 text {* See @{file "~~/src/HOL/ex/Records.thy"}, for example. *}

  1041

  1042 section {* Typedef axiomatization \label{sec:hol-typedef} *}

  1043

  1044 text {*

  1045   \begin{matharray}{rcl}

  1046     @{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

  1047   \end{matharray}

  1048

  1049   A Gordon/HOL-style type definition is a certain axiom scheme that

  1050   identifies a new type with a subset of an existing type.  More

  1051   precisely, the new type is defined by exhibiting an existing type

  1052   @{text \<tau>}, a set @{text "A :: \<tau> set"}, and a theorem that proves

  1053   @{prop "\<exists>x. x \<in> A"}.  Thus @{text A} is a non-empty subset of @{text

  1054   \<tau>}, and the new type denotes this subset.  New functions are

  1055   postulated that establish an isomorphism between the new type and

  1056   the subset.  In general, the type @{text \<tau>} may involve type

  1057   variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} which means that the type definition

  1058   produces a type constructor @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} depending on

  1059   those type arguments.

  1060

  1061   The axiomatization can be considered a definition'' in the sense

  1062   of the particular set-theoretic interpretation of HOL

  1063   \cite{pitts93}, where the universe of types is required to be

  1064   downwards-closed wrt.\ arbitrary non-empty subsets.  Thus genuinely

  1065   new types introduced by @{command "typedef"} stay within the range

  1066   of HOL models by construction.  Note that @{command_ref

  1067   type_synonym} from Isabelle/Pure merely introduces syntactic

  1068   abbreviations, without any logical significance.

  1069

  1070   @{rail "

  1071     @@{command (HOL) typedef} abs_type '=' rep_set

  1072     ;

  1073

  1074     abs_type: @{syntax typespec_sorts} @{syntax mixfix}?

  1075     ;

  1076     rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?

  1077   "}

  1078

  1079   \begin{description}

  1080

  1081   \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}

  1082   axiomatizes a type definition in the background theory of the

  1083   current context, depending on a non-emptiness result of the set

  1084   @{text A} that needs to be proven here.  The set @{text A} may

  1085   contain type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} as specified on the LHS,

  1086   but no term variables.

  1087

  1088   Even though a local theory specification, the newly introduced type

  1089   constructor cannot depend on parameters or assumptions of the

  1090   context: this is structurally impossible in HOL.  In contrast, the

  1091   non-emptiness proof may use local assumptions in unusual situations,

  1092   which could result in different interpretations in target contexts:

  1093   the meaning of the bijection between the representing set @{text A}

  1094   and the new type @{text t} may then change in different application

  1095   contexts.

  1096

  1097   For @{command (HOL) "typedef"}~@{text "t = A"} the newly introduced

  1098   type @{text t} is accompanied by a pair of morphisms to relate it to

  1099   the representing set over the old type.  By default, the injection

  1100   from type to set is called @{text Rep_t} and its inverse @{text

  1101   Abs_t}: An explicit @{keyword (HOL) "morphisms"} specification

  1102   allows to provide alternative names.

  1103

  1104   The core axiomatization uses the locale predicate @{const

  1105   type_definition} as defined in Isabelle/HOL.  Various basic

  1106   consequences of that are instantiated accordingly, re-using the

  1107   locale facts with names derived from the new type constructor.  Thus

  1108   the generic @{thm type_definition.Rep} is turned into the specific

  1109   @{text "Rep_t"}, for example.

  1110

  1111   Theorems @{thm type_definition.Rep}, @{thm

  1112   type_definition.Rep_inverse}, and @{thm type_definition.Abs_inverse}

  1113   provide the most basic characterization as a corresponding

  1114   injection/surjection pair (in both directions).  The derived rules

  1115   @{thm type_definition.Rep_inject} and @{thm

  1116   type_definition.Abs_inject} provide a more convenient version of

  1117   injectivity, suitable for automated proof tools (e.g.\ in

  1118   declarations involving @{attribute simp} or @{attribute iff}).

  1119   Furthermore, the rules @{thm type_definition.Rep_cases}~/ @{thm

  1120   type_definition.Rep_induct}, and @{thm type_definition.Abs_cases}~/

  1121   @{thm type_definition.Abs_induct} provide alternative views on

  1122   surjectivity.  These rules are already declared as set or type rules

  1123   for the generic @{method cases} and @{method induct} methods,

  1124   respectively.

  1125

  1126   \end{description}

  1127

  1128   \begin{warn}

  1129   If you introduce a new type axiomatically, i.e.\ via @{command_ref

  1130   typedecl} and @{command_ref axiomatization}, the minimum requirement

  1131   is that it has a non-empty model, to avoid immediate collapse of the

  1132   HOL logic.  Moreover, one needs to demonstrate that the

  1133   interpretation of such free-form axiomatizations can coexist with

  1134   that of the regular @{command_def typedef} scheme, and any extension

  1135   that other people might have introduced elsewhere.

  1136   \end{warn}

  1137 *}

  1138

  1139 subsubsection {* Examples *}

  1140

  1141 text {* Type definitions permit the introduction of abstract data

  1142   types in a safe way, namely by providing models based on already

  1143   existing types.  Given some abstract axiomatic description @{text P}

  1144   of a type, this involves two steps:

  1145

  1146   \begin{enumerate}

  1147

  1148   \item Find an appropriate type @{text \<tau>} and subset @{text A} which

  1149   has the desired properties @{text P}, and make a type definition

  1150   based on this representation.

  1151

  1152   \item Prove that @{text P} holds for @{text \<tau>} by lifting @{text P}

  1153   from the representation.

  1154

  1155   \end{enumerate}

  1156

  1157   You can later forget about the representation and work solely in

  1158   terms of the abstract properties @{text P}.

  1159

  1160   \medskip The following trivial example pulls a three-element type

  1161   into existence within the formal logical environment of HOL. *}

  1162

  1163 typedef three = "{(True, True), (True, False), (False, True)}"

  1164   by blast

  1165

  1166 definition "One = Abs_three (True, True)"

  1167 definition "Two = Abs_three (True, False)"

  1168 definition "Three = Abs_three (False, True)"

  1169

  1170 lemma three_distinct: "One \<noteq> Two"  "One \<noteq> Three"  "Two \<noteq> Three"

  1171   by (simp_all add: One_def Two_def Three_def Abs_three_inject)

  1172

  1173 lemma three_cases:

  1174   fixes x :: three obtains "x = One" | "x = Two" | "x = Three"

  1175   by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)

  1176

  1177 text {* Note that such trivial constructions are better done with

  1178   derived specification mechanisms such as @{command datatype}: *}

  1179

  1180 datatype three' = One' | Two' | Three'

  1181

  1182 text {* This avoids re-doing basic definitions and proofs from the

  1183   primitive @{command typedef} above. *}

  1184

  1185

  1186

  1187 section {* Functorial structure of types *}

  1188

  1189 text {*

  1190   \begin{matharray}{rcl}

  1191     @{command_def (HOL) "enriched_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}

  1192   \end{matharray}

  1193

  1194   @{rail "

  1195     @@{command (HOL) enriched_type} (@{syntax name} ':')? @{syntax term}

  1196     ;

  1197   "}

  1198

  1199   \begin{description}

  1200

  1201   \item @{command (HOL) "enriched_type"}~@{text "prefix: m"} allows to

  1202   prove and register properties about the functorial structure of type

  1203   constructors.  These properties then can be used by other packages

  1204   to deal with those type constructors in certain type constructions.

  1205   Characteristic theorems are noted in the current local theory.  By

  1206   default, they are prefixed with the base name of the type

  1207   constructor, an explicit prefix can be given alternatively.

  1208

  1209   The given term @{text "m"} is considered as \emph{mapper} for the

  1210   corresponding type constructor and must conform to the following

  1211   type pattern:

  1212

  1213   \begin{matharray}{lll}

  1214     @{text "m"} & @{text "::"} &

  1215       @{text "\<sigma>\<^isub>1 \<Rightarrow> \<dots> \<sigma>\<^isub>k \<Rightarrow> (\<^vec>\<alpha>\<^isub>n) t \<Rightarrow> (\<^vec>\<beta>\<^isub>n) t"} \\

  1216   \end{matharray}

  1217

  1218   \noindent where @{text t} is the type constructor, @{text

  1219   "\<^vec>\<alpha>\<^isub>n"} and @{text "\<^vec>\<beta>\<^isub>n"} are distinct

  1220   type variables free in the local theory and @{text "\<sigma>\<^isub>1"},

  1221   \ldots, @{text "\<sigma>\<^isub>k"} is a subsequence of @{text "\<alpha>\<^isub>1 \<Rightarrow>

  1222   \<beta>\<^isub>1"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<alpha>\<^isub>1"}, \ldots,

  1223   @{text "\<alpha>\<^isub>n \<Rightarrow> \<beta>\<^isub>n"}, @{text "\<beta>\<^isub>n \<Rightarrow>

  1224   \<alpha>\<^isub>n"}.

  1225

  1226   \end{description}

  1227 *}

  1228

  1229

  1230 section {* Quotient types *}

  1231

  1232 text {*

  1233   \begin{matharray}{rcl}

  1234     @{command_def (HOL) "quotient_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\

  1235     @{command_def (HOL) "quotient_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\

  1236     @{command_def (HOL) "print_quotmapsQ3"} & : & @{text "context \<rightarrow>"}\\

  1237     @{command_def (HOL) "print_quotientsQ3"} & : & @{text "context \<rightarrow>"}\\

  1238     @{command_def (HOL) "print_quotconsts"} & : & @{text "context \<rightarrow>"}\\

  1239     @{method_def (HOL) "lifting"} & : & @{text method} \\

  1240     @{method_def (HOL) "lifting_setup"} & : & @{text method} \\

  1241     @{method_def (HOL) "descending"} & : & @{text method} \\

  1242     @{method_def (HOL) "descending_setup"} & : & @{text method} \\

  1243     @{method_def (HOL) "partiality_descending"} & : & @{text method} \\

  1244     @{method_def (HOL) "partiality_descending_setup"} & : & @{text method} \\

  1245     @{method_def (HOL) "regularize"} & : & @{text method} \\

  1246     @{method_def (HOL) "injection"} & : & @{text method} \\

  1247     @{method_def (HOL) "cleaning"} & : & @{text method} \\

  1248     @{attribute_def (HOL) "quot_thm"} & : & @{text attribute} \\

  1249     @{attribute_def (HOL) "quot_lifted"} & : & @{text attribute} \\

  1250     @{attribute_def (HOL) "quot_respect"} & : & @{text attribute} \\

  1251     @{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\

  1252   \end{matharray}

  1253

  1254   The quotient package defines a new quotient type given a raw type

  1255   and a partial equivalence relation.  It also includes automation for

  1256   transporting definitions and theorems.  It can automatically produce

  1257   definitions and theorems on the quotient type, given the

  1258   corresponding constants and facts on the raw type.

  1259

  1260   @{rail "

  1261     @@{command (HOL) quotient_type} (spec);

  1262

  1263     spec: @{syntax typespec} @{syntax mixfix}? '=' \\

  1264      @{syntax type} '/' ('partial' ':')? @{syntax term} \\

  1265      (@'morphisms' @{syntax name} @{syntax name})?;

  1266   "}

  1267

  1268   @{rail "

  1269     @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \\

  1270     @{syntax term} 'is' @{syntax term};

  1271

  1272     constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?

  1273   "}

  1274

  1275   @{rail "

  1276     @@{method (HOL) lifting} @{syntax thmrefs}?

  1277     ;

  1278

  1279     @@{method (HOL) lifting_setup} @{syntax thmrefs}?

  1280     ;

  1281   "}

  1282

  1283   \begin{description}

  1284

  1285   \item @{command (HOL) "quotient_type"} defines quotient types. The

  1286   injection from a quotient type to a raw type is called @{text

  1287   rep_t}, its inverse @{text abs_t} unless explicit @{keyword (HOL)

  1288   "morphisms"} specification provides alternative names. @{command

  1289   (HOL) "quotient_type"} requires the user to prove that the relation

  1290   is an equivalence relation (predicate @{text equivp}), unless the

  1291   user specifies explicitely @{text partial} in which case the

  1292   obligation is @{text part_equivp}.  A quotient defined with @{text

  1293   partial} is weaker in the sense that less things can be proved

  1294   automatically.

  1295

  1296   \item @{command (HOL) "quotient_definition"} defines a constant on

  1297   the quotient type.

  1298

  1299   \item @{command (HOL) "print_quotmapsQ3"} prints quotient map

  1300   functions.

  1301

  1302   \item @{command (HOL) "print_quotientsQ3"} prints quotients.

  1303

  1304   \item @{command (HOL) "print_quotconsts"} prints quotient constants.

  1305

  1306   \item @{method (HOL) "lifting"} and @{method (HOL) "lifting_setup"}

  1307     methods match the current goal with the given raw theorem to be

  1308     lifted producing three new subgoals: regularization, injection and

  1309     cleaning subgoals. @{method (HOL) "lifting"} tries to apply the

  1310     heuristics for automatically solving these three subgoals and

  1311     leaves only the subgoals unsolved by the heuristics to the user as

  1312     opposed to @{method (HOL) "lifting_setup"} which leaves the three

  1313     subgoals unsolved.

  1314

  1315   \item @{method (HOL) "descending"} and @{method (HOL)

  1316     "descending_setup"} try to guess a raw statement that would lift

  1317     to the current subgoal. Such statement is assumed as a new subgoal

  1318     and @{method (HOL) "descending"} continues in the same way as

  1319     @{method (HOL) "lifting"} does. @{method (HOL) "descending"} tries

  1320     to solve the arising regularization, injection and cleaning

  1321     subgoals with the analoguous method @{method (HOL)

  1322     "descending_setup"} which leaves the four unsolved subgoals.

  1323

  1324   \item @{method (HOL) "partiality_descending"} finds the regularized

  1325     theorem that would lift to the current subgoal, lifts it and

  1326     leaves as a subgoal. This method can be used with partial

  1327     equivalence quotients where the non regularized statements would

  1328     not be true. @{method (HOL) "partiality_descending_setup"} leaves

  1329     the injection and cleaning subgoals unchanged.

  1330

  1331   \item @{method (HOL) "regularize"} applies the regularization

  1332     heuristics to the current subgoal.

  1333

  1334   \item @{method (HOL) "injection"} applies the injection heuristics

  1335     to the current goal using the stored quotient respectfulness

  1336     theorems.

  1337

  1338   \item @{method (HOL) "cleaning"} applies the injection cleaning

  1339     heuristics to the current subgoal using the stored quotient

  1340     preservation theorems.

  1341

  1342   \item @{attribute (HOL) quot_lifted} attribute tries to

  1343     automatically transport the theorem to the quotient type.

  1344     The attribute uses all the defined quotients types and quotient

  1345     constants often producing undesired results or theorems that

  1346     cannot be lifted.

  1347

  1348   \item @{attribute (HOL) quot_respect} and @{attribute (HOL)

  1349     quot_preserve} attributes declare a theorem as a respectfulness

  1350     and preservation theorem respectively.  These are stored in the

  1351     local theory store and used by the @{method (HOL) "injection"}

  1352     and @{method (HOL) "cleaning"} methods respectively.

  1353

  1354   \item @{attribute (HOL) quot_thm} declares that a certain theorem

  1355     is a quotient extension theorem. Quotient extension theorems

  1356     allow for quotienting inside container types. Given a polymorphic

  1357     type that serves as a container, a map function defined for this

  1358     container using @{command (HOL) "enriched_type"} and a relation

  1359     map defined for for the container type, the quotient extension

  1360     theorem should be @{term "Quotient3 R Abs Rep \<Longrightarrow> Quotient3

  1361     (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems

  1362     are stored in a database and are used all the steps of lifting

  1363     theorems.

  1364

  1365   \end{description}

  1366 *}

  1367

  1368

  1369

  1370 section {* Definition by specification \label{sec:hol-specification} *}

  1371

  1372 text {*

  1373   \begin{matharray}{rcl}

  1374     @{command_def (HOL) "specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\

  1375     @{command_def (HOL) "ax_specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\

  1376   \end{matharray}

  1377

  1378   @{rail "

  1379   (@@{command (HOL) specification} | @@{command (HOL) ax_specification})

  1380     '(' (decl +) ')' \\ (@{syntax thmdecl}? @{syntax prop} +)

  1381   ;

  1382   decl: ((@{syntax name} ':')? @{syntax term} '(' @'overloaded' ')'?)

  1383   "}

  1384

  1385   \begin{description}

  1386

  1387   \item @{command (HOL) "specification"}~@{text "decls \<phi>"} sets up a

  1388   goal stating the existence of terms with the properties specified to

  1389   hold for the constants given in @{text decls}.  After finishing the

  1390   proof, the theory will be augmented with definitions for the given

  1391   constants, as well as with theorems stating the properties for these

  1392   constants.

  1393

  1394   \item @{command (HOL) "ax_specification"}~@{text "decls \<phi>"} sets up

  1395   a goal stating the existence of terms with the properties specified

  1396   to hold for the constants given in @{text decls}.  After finishing

  1397   the proof, the theory will be augmented with axioms expressing the

  1398   properties given in the first place.

  1399

  1400   \item @{text decl} declares a constant to be defined by the

  1401   specification given.  The definition for the constant @{text c} is

  1402   bound to the name @{text c_def} unless a theorem name is given in

  1403   the declaration.  Overloaded constants should be declared as such.

  1404

  1405   \end{description}

  1406

  1407   Whether to use @{command (HOL) "specification"} or @{command (HOL)

  1408   "ax_specification"} is to some extent a matter of style.  @{command

  1409   (HOL) "specification"} introduces no new axioms, and so by

  1410   construction cannot introduce inconsistencies, whereas @{command

  1411   (HOL) "ax_specification"} does introduce axioms, but only after the

  1412   user has explicitly proven it to be safe.  A practical issue must be

  1413   considered, though: After introducing two constants with the same

  1414   properties using @{command (HOL) "specification"}, one can prove

  1415   that the two constants are, in fact, equal.  If this might be a

  1416   problem, one should use @{command (HOL) "ax_specification"}.

  1417 *}

  1418

  1419

  1420 chapter {* Proof tools *}

  1421

  1422 section {* Adhoc tuples *}

  1423

  1424 text {*

  1425   \begin{matharray}{rcl}

  1426     @{attribute_def (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\

  1427   \end{matharray}

  1428

  1429   @{rail "

  1430     @@{attribute (HOL) split_format} ('(' 'complete' ')')?

  1431   "}

  1432

  1433   \begin{description}

  1434

  1435   \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes

  1436   arguments in function applications to be represented canonically

  1437   according to their tuple type structure.

  1438

  1439   Note that this operation tends to invent funny names for new local

  1440   parameters introduced.

  1441

  1442   \end{description}

  1443 *}

  1444

  1445

  1446 section {* Transfer package *}

  1447

  1448 text {*

  1449   \begin{matharray}{rcl}

  1450     @{method_def (HOL) "transfer"} & : & @{text method} \\

  1451     @{method_def (HOL) "transfer'"} & : & @{text method} \\

  1452     @{method_def (HOL) "transfer_prover"} & : & @{text method} \\

  1453     @{attribute_def (HOL) "transfer_rule"} & : & @{text attribute} \\

  1454     @{attribute_def (HOL) "relator_eq"} & : & @{text attribute} \\

  1455   \end{matharray}

  1456

  1457   \begin{description}

  1458

  1459   \item @{method (HOL) "transfer"} method replaces the current subgoal

  1460     with a logically equivalent one that uses different types and

  1461     constants. The replacement of types and constants is guided by the

  1462     database of transfer rules. Goals are generalized over all free

  1463     variables by default; this is necessary for variables whose types

  1464     change, but can be overridden for specific variables with e.g.

  1465     @{text "transfer fixing: x y z"}.

  1466

  1467   \item @{method (HOL) "transfer'"} is a variant of @{method (HOL)

  1468     transfer} that allows replacing a subgoal with one that is

  1469     logically stronger (rather than equivalent). For example, a

  1470     subgoal involving equality on a quotient type could be replaced

  1471     with a subgoal involving equality (instead of the corresponding

  1472     equivalence relation) on the underlying raw type.

  1473

  1474   \item @{method (HOL) "transfer_prover"} method assists with proving

  1475     a transfer rule for a new constant, provided the constant is

  1476     defined in terms of other constants that already have transfer

  1477     rules. It should be applied after unfolding the constant

  1478     definitions.

  1479

  1480   \item @{attribute (HOL) "transfer_rule"} attribute maintains a

  1481     collection of transfer rules, which relate constants at two

  1482     different types. Typical transfer rules may relate different type

  1483     instances of the same polymorphic constant, or they may relate an

  1484     operation on a raw type to a corresponding operation on an

  1485     abstract type (quotient or subtype). For example:

  1486

  1487     @{text "((A ===> B) ===> list_all2 A ===> list_all2 B) map map"}\\

  1488     @{text "(cr_int ===> cr_int ===> cr_int) (\<lambda>(x,y) (u,v). (x+u, y+v)) plus"}

  1489

  1490     Lemmas involving predicates on relations can also be registered

  1491     using the same attribute. For example:

  1492

  1493     @{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"}\\

  1494     @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (prod_rel A B)"}

  1495

  1496   \item @{attribute (HOL) relator_eq} attribute collects identity laws

  1497     for relators of various type constructors, e.g. @{text "list_all2

  1498     (op =) = (op =)"}. The @{method (HOL) transfer} method uses these

  1499     lemmas to infer transfer rules for non-polymorphic constants on

  1500     the fly.

  1501

  1502   \end{description}

  1503

  1504 *}

  1505

  1506

  1507 section {* Lifting package *}

  1508

  1509 text {*

  1510   \begin{matharray}{rcl}

  1511     @{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \<rightarrow> local_theory"}\\

  1512     @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\

  1513     @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\

  1514     @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\

  1515     @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\

  1516     @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\

  1517     @{attribute_def (HOL) "reflexivity_rule"} & : & @{text attribute} \\

  1518     @{attribute_def (HOL) "quot_del"} & : & @{text attribute}

  1519   \end{matharray}

  1520

  1521   @{rail "

  1522     @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \\

  1523       @{syntax thmref} @{syntax thmref}?;

  1524   "}

  1525

  1526   @{rail "

  1527     @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type}  @{syntax mixfix}? \\

  1528       'is' @{syntax term};

  1529   "}

  1530

  1531   \begin{description}

  1532

  1533   \item @{command (HOL) "setup_lifting"} Sets up the Lifting package

  1534     to work with a user-defined type. The user must provide either a

  1535     quotient theorem @{text "Quotient R Abs Rep T"} or a

  1536     type_definition theorem @{text "type_definition Rep Abs A"}.  The

  1537     package configures transfer rules for equality and quantifiers on

  1538     the type, and sets up the @{command_def (HOL) "lift_definition"}

  1539     command to work with the type.  In the case of a quotient theorem,

  1540     an optional theorem @{text "reflp R"} can be provided as a second

  1541     argument.  This allows the package to generate stronger transfer

  1542     rules.

  1543

  1544     @{command (HOL) "setup_lifting"} is called automatically if a

  1545     quotient type is defined by the command @{command (HOL)

  1546     "quotient_type"} from the Quotient package.

  1547

  1548     If @{command (HOL) "setup_lifting"} is called with a

  1549     type_definition theorem, the abstract type implicitly defined by

  1550     the theorem is declared as an abstract type in the code

  1551     generator. This allows @{command (HOL) "lift_definition"} to

  1552     register (generated) code certificate theorems as abstract code

  1553     equations in the code generator.  The option @{text "no_code"}

  1554     of the command @{command (HOL) "setup_lifting"} can turn off that

  1555     behavior and causes that code certificate theorems generated by

  1556     @{command (HOL) "lift_definition"} are not registred as abstract

  1557     code equations.

  1558

  1559   \item @{command (HOL) "lift_definition"} @{text "f :: \<tau> is t"}

  1560     Defines a new function @{text f} with an abstract type @{text \<tau>}

  1561     in terms of a corresponding operation @{text t} on a

  1562     representation type.  The term @{text t} doesn't have to be

  1563     necessarily a constant but it can be any term.

  1564

  1565     Users must discharge a respectfulness proof obligation when each

  1566     constant is defined. For a type copy, i.e. a typedef with @{text

  1567     UNIV}, the proof is discharged automatically. The obligation is

  1568     presented in a user-friendly, readable form. A respectfulness

  1569     theorem in the standard format @{text f.rsp} and a transfer rule

  1570     @{text f.tranfer} for the Transfer package are generated by the

  1571     package.

  1572

  1573     For each constant defined through trivial quotients (type copies or

  1574     subtypes) @{text f.rep_eq} is generated. The equation is a code certificate

  1575     that defines @{text f} using the representation function.

  1576

  1577     For each constant @{text f.abs_eq} is generated. The equation is unconditional

  1578     for total quotients. The equation defines @{text f} using

  1579     the abstraction function.

  1580

  1581     Integration with code_abstype: For subtypes (e.g.,

  1582     corresponding to a datatype invariant, such as dlist), @{command

  1583     (HOL) "lift_definition"} uses a code certificate theorem

  1584     @{text f.rep_eq} as a code equation.

  1585

  1586     Integration with code: For total quotients, @{command

  1587     (HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation.

  1588

  1589   \item @{command (HOL) "print_quotmaps"} prints stored quotient map

  1590     theorems.

  1591

  1592   \item @{command (HOL) "print_quotients"} prints stored quotient

  1593     theorems.

  1594

  1595   \item @{attribute (HOL) quot_map} registers a quotient map

  1596     theorem. For examples see @{file

  1597     "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy

  1598     files.

  1599

  1600   \item @{attribute (HOL) invariant_commute} registers a theorem that

  1601     shows a relationship between the constant @{text

  1602     Lifting.invariant} (used for internal encoding of proper subtypes)

  1603     and a relator.  Such theorems allows the package to hide @{text

  1604     Lifting.invariant} from a user in a user-readable form of a

  1605     respectfulness theorem. For examples see @{file

  1606     "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy

  1607     files.

  1608

  1609   \item @{attribute (HOL) reflexivity_rule} registers a theorem that shows

  1610     that a relator respects reflexivity and left-totality. For exampless

  1611     see @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy

  1612     The property is used in generation of abstraction function equations.

  1613

  1614   \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem

  1615     from the Lifting infrastructure and thus de-register the corresponding quotient.

  1616     This effectively causes that @{command (HOL) lift_definition}  will not

  1617     do any lifting for the corresponding type. It serves mainly for hiding

  1618     of type construction details when the construction is done. See for example

  1619     @{file "~~/src/HOL/Int.thy"}.

  1620   \end{description}

  1621 *}

  1622

  1623

  1624 section {* Coercive subtyping *}

  1625

  1626 text {*

  1627   \begin{matharray}{rcl}

  1628     @{attribute_def (HOL) coercion} & : & @{text attribute} \\

  1629     @{attribute_def (HOL) coercion_enabled} & : & @{text attribute} \\

  1630     @{attribute_def (HOL) coercion_map} & : & @{text attribute} \\

  1631   \end{matharray}

  1632

  1633   Coercive subtyping allows the user to omit explicit type

  1634   conversions, also called \emph{coercions}.  Type inference will add

  1635   them as necessary when parsing a term. See

  1636   \cite{traytel-berghofer-nipkow-2011} for details.

  1637

  1638   @{rail "

  1639     @@{attribute (HOL) coercion} (@{syntax term})?

  1640     ;

  1641   "}

  1642   @{rail "

  1643     @@{attribute (HOL) coercion_map} (@{syntax term})?

  1644     ;

  1645   "}

  1646

  1647   \begin{description}

  1648

  1649   \item @{attribute (HOL) "coercion"}~@{text "f"} registers a new

  1650   coercion function @{text "f :: \<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2"} where @{text "\<sigma>\<^isub>1"} and

  1651   @{text "\<sigma>\<^isub>2"} are type constructors without arguments.  Coercions are

  1652   composed by the inference algorithm if needed.  Note that the type

  1653   inference algorithm is complete only if the registered coercions

  1654   form a lattice.

  1655

  1656   \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a

  1657   new map function to lift coercions through type constructors. The

  1658   function @{text "map"} must conform to the following type pattern

  1659

  1660   \begin{matharray}{lll}

  1661     @{text "map"} & @{text "::"} &

  1662       @{text "f\<^isub>1 \<Rightarrow> \<dots> \<Rightarrow> f\<^isub>n \<Rightarrow> (\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n) t \<Rightarrow> (\<beta>\<^isub>1, \<dots>, \<beta>\<^isub>n) t"} \\

  1663   \end{matharray}

  1664

  1665   where @{text "t"} is a type constructor and @{text "f\<^isub>i"} is of type

  1666   @{text "\<alpha>\<^isub>i \<Rightarrow> \<beta>\<^isub>i"} or @{text "\<beta>\<^isub>i \<Rightarrow> \<alpha>\<^isub>i"}.  Registering a map function

  1667   overwrites any existing map function for this particular type

  1668   constructor.

  1669

  1670   \item @{attribute (HOL) "coercion_enabled"} enables the coercion

  1671   inference algorithm.

  1672

  1673   \end{description}

  1674 *}

  1675

  1676

  1677 section {* Arithmetic proof support *}

  1678

  1679 text {*

  1680   \begin{matharray}{rcl}

  1681     @{method_def (HOL) arith} & : & @{text method} \\

  1682     @{attribute_def (HOL) arith} & : & @{text attribute} \\

  1683     @{attribute_def (HOL) arith_split} & : & @{text attribute} \\

  1684   \end{matharray}

  1685

  1686   \begin{description}

  1687

  1688   \item @{method (HOL) arith} decides linear arithmetic problems (on

  1689   types @{text nat}, @{text int}, @{text real}).  Any current facts

  1690   are inserted into the goal before running the procedure.

  1691

  1692   \item @{attribute (HOL) arith} declares facts that are supplied to

  1693   the arithmetic provers implicitly.

  1694

  1695   \item @{attribute (HOL) arith_split} attribute declares case split

  1696   rules to be expanded before @{method (HOL) arith} is invoked.

  1697

  1698   \end{description}

  1699

  1700   Note that a simpler (but faster) arithmetic prover is already

  1701   invoked by the Simplifier.

  1702 *}

  1703

  1704

  1705 section {* Intuitionistic proof search *}

  1706

  1707 text {*

  1708   \begin{matharray}{rcl}

  1709     @{method_def (HOL) iprover} & : & @{text method} \\

  1710   \end{matharray}

  1711

  1712   @{rail "

  1713     @@{method (HOL) iprover} ( @{syntax rulemod} * )

  1714   "}

  1715

  1716   \begin{description}

  1717

  1718   \item @{method (HOL) iprover} performs intuitionistic proof search,

  1719   depending on specifically declared rules from the context, or given

  1720   as explicit arguments.  Chained facts are inserted into the goal

  1721   before commencing proof search.

  1722

  1723   Rules need to be classified as @{attribute (Pure) intro},

  1724   @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the

  1725   @{text "!"}'' indicator refers to safe'' rules, which may be

  1726   applied aggressively (without considering back-tracking later).

  1727   Rules declared with @{text "?"}'' are ignored in proof search (the

  1728   single-step @{method (Pure) rule} method still observes these).  An

  1729   explicit weight annotation may be given as well; otherwise the

  1730   number of rule premises will be taken into account here.

  1731

  1732   \end{description}

  1733 *}

  1734

  1735

  1736 section {* Model Elimination and Resolution *}

  1737

  1738 text {*

  1739   \begin{matharray}{rcl}

  1740     @{method_def (HOL) "meson"} & : & @{text method} \\

  1741     @{method_def (HOL) "metis"} & : & @{text method} \\

  1742   \end{matharray}

  1743

  1744   @{rail "

  1745     @@{method (HOL) meson} @{syntax thmrefs}?

  1746     ;

  1747

  1748     @@{method (HOL) metis}

  1749       ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?

  1750       @{syntax thmrefs}?

  1751   "}

  1752

  1753   \begin{description}

  1754

  1755   \item @{method (HOL) meson} implements Loveland's model elimination

  1756   procedure \cite{loveland-78}.  See @{file

  1757   "~~/src/HOL/ex/Meson_Test.thy"} for examples.

  1758

  1759   \item @{method (HOL) metis} combines ordered resolution and ordered

  1760   paramodulation to find first-order (or mildly higher-order) proofs.

  1761   The first optional argument specifies a type encoding; see the

  1762   Sledgehammer manual \cite{isabelle-sledgehammer} for details.  The

  1763   directory @{file "~~/src/HOL/Metis_Examples"} contains several small

  1764   theories developed to a large extent using @{method (HOL) metis}.

  1765

  1766   \end{description}

  1767 *}

  1768

  1769

  1770 section {* Algebraic reasoning via Gr\"obner bases *}

  1771

  1772 text {*

  1773   \begin{matharray}{rcl}

  1774     @{method_def (HOL) "algebra"} & : & @{text method} \\

  1775     @{attribute_def (HOL) algebra} & : & @{text attribute} \\

  1776   \end{matharray}

  1777

  1778   @{rail "

  1779     @@{method (HOL) algebra}

  1780       ('add' ':' @{syntax thmrefs})?

  1781       ('del' ':' @{syntax thmrefs})?

  1782     ;

  1783     @@{attribute (HOL) algebra} (() | 'add' | 'del')

  1784   "}

  1785

  1786   \begin{description}

  1787

  1788   \item @{method (HOL) algebra} performs algebraic reasoning via

  1789   Gr\"obner bases, see also \cite{Chaieb-Wenzel:2007} and

  1790   \cite[\S3.2]{Chaieb-thesis}. The method handles deals with two main

  1791   classes of problems:

  1792

  1793   \begin{enumerate}

  1794

  1795   \item Universal problems over multivariate polynomials in a

  1796   (semi)-ring/field/idom; the capabilities of the method are augmented

  1797   according to properties of these structures. For this problem class

  1798   the method is only complete for algebraically closed fields, since

  1799   the underlying method is based on Hilbert's Nullstellensatz, where

  1800   the equivalence only holds for algebraically closed fields.

  1801

  1802   The problems can contain equations @{text "p = 0"} or inequations

  1803   @{text "q \<noteq> 0"} anywhere within a universal problem statement.

  1804

  1805   \item All-exists problems of the following restricted (but useful)

  1806   form:

  1807

  1808   @{text [display] "\<forall>x\<^sub>1 \<dots> x\<^sub>n.

  1809     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>

  1810     (\<exists>y\<^sub>1 \<dots> y\<^sub>k.

  1811       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>

  1812       \<dots> \<and>

  1813       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)"}

  1814

  1815   Here @{text "e\<^sub>1, \<dots>, e\<^sub>n"} and the @{text "p\<^sub>i\<^sub>j"} are multivariate

  1816   polynomials only in the variables mentioned as arguments.

  1817

  1818   \end{enumerate}

  1819

  1820   The proof method is preceded by a simplification step, which may be

  1821   modified by using the form @{text "(algebra add: ths\<^sub>1 del: ths\<^sub>2)"}.

  1822   This acts like declarations for the Simplifier

  1823   (\secref{sec:simplifier}) on a private simpset for this tool.

  1824

  1825   \item @{attribute algebra} (as attribute) manages the default

  1826   collection of pre-simplification rules of the above proof method.

  1827

  1828   \end{description}

  1829 *}

  1830

  1831

  1832 subsubsection {* Example *}

  1833

  1834 text {* The subsequent example is from geometry: collinearity is

  1835   invariant by rotation.  *}

  1836

  1837 type_synonym point = "int \<times> int"

  1838

  1839 fun collinear :: "point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where

  1840   "collinear (Ax, Ay) (Bx, By) (Cx, Cy) \<longleftrightarrow>

  1841     (Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx)"

  1842

  1843 lemma collinear_inv_rotation:

  1844   assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<twosuperior> + s\<twosuperior> = 1"

  1845   shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)

  1846     (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"

  1847   using assms by (algebra add: collinear.simps)

  1848

  1849 text {*

  1850  See also @{"file" "~~/src/HOL/ex/Groebner_Examples.thy"}.

  1851 *}

  1852

  1853

  1854 section {* Coherent Logic *}

  1855

  1856 text {*

  1857   \begin{matharray}{rcl}

  1858     @{method_def (HOL) "coherent"} & : & @{text method} \\

  1859   \end{matharray}

  1860

  1861   @{rail "

  1862     @@{method (HOL) coherent} @{syntax thmrefs}?

  1863   "}

  1864

  1865   \begin{description}

  1866

  1867   \item @{method (HOL) coherent} solves problems of \emph{Coherent

  1868   Logic} \cite{Bezem-Coquand:2005}, which covers applications in

  1869   confluence theory, lattice theory and projective geometry.  See

  1870   @{file "~~/src/HOL/ex/Coherent.thy"} for some examples.

  1871

  1872   \end{description}

  1873 *}

  1874

  1875

  1876 section {* Proving propositions *}

  1877

  1878 text {*

  1879   In addition to the standard proof methods, a number of diagnosis

  1880   tools search for proofs and provide an Isar proof snippet on success.

  1881   These tools are available via the following commands.

  1882

  1883   \begin{matharray}{rcl}

  1884     @{command_def (HOL) "solve_direct"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

  1885     @{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

  1886     @{command_def (HOL) "try0"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

  1887     @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

  1888     @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \<rightarrow> theory"}

  1889   \end{matharray}

  1890

  1891   @{rail "

  1892     @@{command (HOL) try}

  1893     ;

  1894

  1895     @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?

  1896       @{syntax nat}?

  1897     ;

  1898

  1899     @@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?

  1900     ;

  1901

  1902     @@{command (HOL) sledgehammer_params} ( ( '[' args ']' ) ? )

  1903     ;

  1904

  1905     args: ( @{syntax name} '=' value + ',' )

  1906     ;

  1907

  1908     facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'

  1909     ;

  1910   "} % FIXME check args "value"

  1911

  1912   \begin{description}

  1913

  1914   \item @{command (HOL) "solve_direct"} checks whether the current

  1915   subgoals can be solved directly by an existing theorem. Duplicate

  1916   lemmas can be detected in this way.

  1917

  1918   \item @{command (HOL) "try0"} attempts to prove a subgoal

  1919   using a combination of standard proof methods (@{method auto},

  1920   @{method simp}, @{method blast}, etc.).  Additional facts supplied

  1921   via @{text "simp:"}, @{text "intro:"}, @{text "elim:"}, and @{text

  1922   "dest:"} are passed to the appropriate proof methods.

  1923

  1924   \item @{command (HOL) "try"} attempts to prove or disprove a subgoal

  1925   using a combination of provers and disprovers (@{command (HOL)

  1926   "solve_direct"}, @{command (HOL) "quickcheck"}, @{command (HOL)

  1927   "try0"}, @{command (HOL) "sledgehammer"}, @{command (HOL)

  1928   "nitpick"}).

  1929

  1930   \item @{command (HOL) "sledgehammer"} attempts to prove a subgoal

  1931   using external automatic provers (resolution provers and SMT

  1932   solvers). See the Sledgehammer manual \cite{isabelle-sledgehammer}

  1933   for details.

  1934

  1935   \item @{command (HOL) "sledgehammer_params"} changes @{command (HOL)

  1936   "sledgehammer"} configuration options persistently.

  1937

  1938   \end{description}

  1939 *}

  1940

  1941

  1942 section {* Checking and refuting propositions *}

  1943

  1944 text {*

  1945   Identifying incorrect propositions usually involves evaluation of

  1946   particular assignments and systematic counterexample search.  This

  1947   is supported by the following commands.

  1948

  1949   \begin{matharray}{rcl}

  1950     @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  1951     @{command_def (HOL) "values"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  1952     @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

  1953     @{command_def (HOL) "nitpick"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

  1954     @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"} \\

  1955     @{command_def (HOL) "nitpick_params"} & : & @{text "theory \<rightarrow> theory"} \\

  1956     @{command_def (HOL) "quickcheck_generator"} & : & @{text "theory \<rightarrow> theory"} \\

  1957     @{command_def (HOL) "find_unused_assms"} & : & @{text "context \<rightarrow>"}

  1958   \end{matharray}

  1959

  1960   @{rail "

  1961     @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}

  1962     ;

  1963

  1964     @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}

  1965     ;

  1966

  1967     (@@{command (HOL) quickcheck} | @@{command (HOL) nitpick})

  1968       ( '[' args ']' )? @{syntax nat}?

  1969     ;

  1970

  1971     (@@{command (HOL) quickcheck_params} |

  1972       @@{command (HOL) nitpick_params}) ( '[' args ']' )?

  1973     ;

  1974

  1975     @@{command (HOL) quickcheck_generator} @{syntax nameref} \\

  1976       'operations:' ( @{syntax term} +)

  1977     ;

  1978

  1979     @@{command (HOL) find_unused_assms} @{syntax name}?

  1980     ;

  1981

  1982     modes: '(' (@{syntax name} +) ')'

  1983     ;

  1984

  1985     args: ( @{syntax name} '=' value + ',' )

  1986     ;

  1987   "} % FIXME check "value"

  1988

  1989   \begin{description}

  1990

  1991   \item @{command (HOL) "value"}~@{text t} evaluates and prints a

  1992   term; optionally @{text modes} can be specified, which are appended

  1993   to the current print mode; see \secref{sec:print-modes}.

  1994   Internally, the evaluation is performed by registered evaluators,

  1995   which are invoked sequentially until a result is returned.

  1996   Alternatively a specific evaluator can be selected using square

  1997   brackets; typical evaluators use the current set of code equations

  1998   to normalize and include @{text simp} for fully symbolic evaluation

  1999   using the simplifier, @{text nbe} for \emph{normalization by

  2000   evaluation} and \emph{code} for code generation in SML.

  2001

  2002   \item @{command (HOL) "values"}~@{text t} enumerates a set

  2003   comprehension by evaluation and prints its values up to the given

  2004   number of solutions; optionally @{text modes} can be specified,

  2005   which are appended to the current print mode; see

  2006   \secref{sec:print-modes}.

  2007

  2008   \item @{command (HOL) "quickcheck"} tests the current goal for

  2009   counterexamples using a series of assignments for its free

  2010   variables; by default the first subgoal is tested, an other can be

  2011   selected explicitly using an optional goal index.  Assignments can

  2012   be chosen exhausting the search space upto a given size, or using a

  2013   fixed number of random assignments in the search space, or exploring

  2014   the search space symbolically using narrowing.  By default,

  2015   quickcheck uses exhaustive testing.  A number of configuration

  2016   options are supported for @{command (HOL) "quickcheck"}, notably:

  2017

  2018     \begin{description}

  2019

  2020     \item[@{text tester}] specifies which testing approach to apply.

  2021     There are three testers, @{text exhaustive}, @{text random}, and

  2022     @{text narrowing}.  An unknown configuration option is treated as

  2023     an argument to tester, making @{text "tester ="} optional.  When

  2024     multiple testers are given, these are applied in parallel.  If no

  2025     tester is specified, quickcheck uses the testers that are set

  2026     active, i.e., configurations @{attribute

  2027     quickcheck_exhaustive_active}, @{attribute

  2028     quickcheck_random_active}, @{attribute

  2029     quickcheck_narrowing_active} are set to true.

  2030

  2031     \item[@{text size}] specifies the maximum size of the search space

  2032     for assignment values.

  2033

  2034     \item[@{text genuine_only}] sets quickcheck only to return genuine

  2035     counterexample, but not potentially spurious counterexamples due

  2036     to underspecified functions.

  2037

  2038     \item[@{text abort_potential}] sets quickcheck to abort once it

  2039     found a potentially spurious counterexample and to not continue

  2040     to search for a further genuine counterexample.

  2041     For this option to be effective, the @{text genuine_only} option

  2042     must be set to false.

  2043

  2044     \item[@{text eval}] takes a term or a list of terms and evaluates

  2045     these terms under the variable assignment found by quickcheck.

  2046     This option is currently only supported by the default

  2047     (exhaustive) tester.

  2048

  2049     \item[@{text iterations}] sets how many sets of assignments are

  2050     generated for each particular size.

  2051

  2052     \item[@{text no_assms}] specifies whether assumptions in

  2053     structured proofs should be ignored.

  2054

  2055     \item[@{text locale}] specifies how to process conjectures in

  2056     a locale context, i.e., they can be interpreted or expanded.

  2057     The option is a whitespace-separated list of the two words

  2058     @{text interpret} and @{text expand}. The list determines the

  2059     order they are employed. The default setting is to first use

  2060     interpretations and then test the expanded conjecture.

  2061     The option is only provided as attribute declaration, but not

  2062     as parameter to the command.

  2063

  2064     \item[@{text timeout}] sets the time limit in seconds.

  2065

  2066     \item[@{text default_type}] sets the type(s) generally used to

  2067     instantiate type variables.

  2068

  2069     \item[@{text report}] if set quickcheck reports how many tests

  2070     fulfilled the preconditions.

  2071

  2072     \item[@{text use_subtype}] if set quickcheck automatically lifts

  2073     conjectures to registered subtypes if possible, and tests the

  2074     lifted conjecture.

  2075

  2076     \item[@{text quiet}] if set quickcheck does not output anything

  2077     while testing.

  2078

  2079     \item[@{text verbose}] if set quickcheck informs about the current

  2080     size and cardinality while testing.

  2081

  2082     \item[@{text expect}] can be used to check if the user's

  2083     expectation was met (@{text no_expectation}, @{text

  2084     no_counterexample}, or @{text counterexample}).

  2085

  2086     \end{description}

  2087

  2088   These option can be given within square brackets.

  2089

  2090   \item @{command (HOL) "quickcheck_params"} changes @{command (HOL)

  2091   "quickcheck"} configuration options persistently.

  2092

  2093   \item @{command (HOL) "quickcheck_generator"} creates random and

  2094   exhaustive value generators for a given type and operations.  It

  2095   generates values by using the operations as if they were

  2096   constructors of that type.

  2097

  2098   \item @{command (HOL) "nitpick"} tests the current goal for

  2099   counterexamples using a reduction to first-order relational

  2100   logic. See the Nitpick manual \cite{isabelle-nitpick} for details.

  2101

  2102   \item @{command (HOL) "nitpick_params"} changes @{command (HOL)

  2103   "nitpick"} configuration options persistently.

  2104

  2105   \item @{command (HOL) "find_unused_assms"} finds potentially superfluous

  2106   assumptions in theorems using quickcheck.

  2107   It takes the theory name to be checked for superfluous assumptions as

  2108   optional argument. If not provided, it checks the current theory.

  2109   Options to the internal quickcheck invocations can be changed with

  2110   common configuration declarations.

  2111

  2112   \end{description}

  2113 *}

  2114

  2115

  2116 section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *}

  2117

  2118 text {*

  2119   The following tools of Isabelle/HOL support cases analysis and

  2120   induction in unstructured tactic scripts; see also

  2121   \secref{sec:cases-induct} for proper Isar versions of similar ideas.

  2122

  2123   \begin{matharray}{rcl}

  2124     @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & @{text method} \\

  2125     @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\

  2126     @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\

  2127     @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

  2128   \end{matharray}

  2129

  2130   @{rail "

  2131     @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?

  2132     ;

  2133     @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?

  2134     ;

  2135     @@{method (HOL) ind_cases} (@{syntax prop}+) (@'for' (@{syntax name}+))?

  2136     ;

  2137     @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')

  2138     ;

  2139

  2140     rule: 'rule' ':' @{syntax thmref}

  2141   "}

  2142

  2143   \begin{description}

  2144

  2145   \item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit

  2146   to reason about inductive types.  Rules are selected according to

  2147   the declarations by the @{attribute cases} and @{attribute induct}

  2148   attributes, cf.\ \secref{sec:cases-induct}.  The @{command (HOL)

  2149   datatype} package already takes care of this.

  2150

  2151   These unstructured tactics feature both goal addressing and dynamic

  2152   instantiation.  Note that named rule cases are \emph{not} provided

  2153   as would be by the proper @{method cases} and @{method induct} proof

  2154   methods (see \secref{sec:cases-induct}).  Unlike the @{method

  2155   induct} method, @{method induct_tac} does not handle structured rule

  2156   statements, only the compact object-logic conclusion of the subgoal

  2157   being addressed.

  2158

  2159   \item @{method (HOL) ind_cases} and @{command (HOL)

  2160   "inductive_cases"} provide an interface to the internal @{ML_text

  2161   mk_cases} operation.  Rules are simplified in an unrestricted

  2162   forward manner.

  2163

  2164   While @{method (HOL) ind_cases} is a proof method to apply the

  2165   result immediately as elimination rules, @{command (HOL)

  2166   "inductive_cases"} provides case split theorems at the theory level

  2167   for later use.  The @{keyword "for"} argument of the @{method (HOL)

  2168   ind_cases} method allows to specify a list of variables that should

  2169   be generalized before applying the resulting rule.

  2170

  2171   \end{description}

  2172 *}

  2173

  2174

  2175 chapter {* Executable code *}

  2176

  2177 text {* For validation purposes, it is often useful to \emph{execute}

  2178   specifications.  In principle, execution could be simulated by

  2179   Isabelle's inference kernel, i.e. by a combination of resolution and

  2180   simplification.  Unfortunately, this approach is rather inefficient.

  2181   A more efficient way of executing specifications is to translate

  2182   them into a functional programming language such as ML.

  2183

  2184   Isabelle provides a generic framework to support code generation

  2185   from executable specifications.  Isabelle/HOL instantiates these

  2186   mechanisms in a way that is amenable to end-user applications.  Code

  2187   can be generated for functional programs (including overloading

  2188   using type classes) targeting SML \cite{SML}, OCaml \cite{OCaml},

  2189   Haskell \cite{haskell-revised-report} and Scala

  2190   \cite{scala-overview-tech-report}.  Conceptually, code generation is

  2191   split up in three steps: \emph{selection} of code theorems,

  2192   \emph{translation} into an abstract executable view and

  2193   \emph{serialization} to a specific \emph{target language}.

  2194   Inductive specifications can be executed using the predicate

  2195   compiler which operates within HOL.  See \cite{isabelle-codegen} for

  2196   an introduction.

  2197

  2198   \begin{matharray}{rcl}

  2199     @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  2200     @{attribute_def (HOL) code} & : & @{text attribute} \\

  2201     @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\

  2202     @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\

  2203     @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  2204     @{attribute_def (HOL) code_unfold} & : & @{text attribute} \\

  2205     @{attribute_def (HOL) code_post} & : & @{text attribute} \\

  2206     @{attribute_def (HOL) code_abbrev} & : & @{text attribute} \\

  2207     @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  2208     @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  2209     @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  2210     @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\

  2211     @{command_def (HOL) "code_printing"} & : & @{text "theory \<rightarrow> theory"} \\

  2212     @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\

  2213     @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\

  2214     @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\

  2215     @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\

  2216     @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\

  2217     @{command_def (HOL) "code_identifier"} & : & @{text "theory \<rightarrow> theory"} \\

  2218     @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\

  2219     @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\

  2220     @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"} \\

  2221     @{command_def (HOL) "code_pred"} & : & @{text "theory \<rightarrow> proof(prove)"}

  2222   \end{matharray}

  2223

  2224   @{rail "

  2225     @@{command (HOL) export_code} ( constexpr + ) \\

  2226        ( ( @'in' target ( @'module_name' @{syntax string} ) ? \\

  2227         ( @'file' ( @{syntax string} | '-' ) ) ? ( '(' args ')' ) ?) + ) ?

  2228     ;

  2229

  2230     const: @{syntax term}

  2231     ;

  2232

  2233     constexpr: ( const | 'name._' | '_' )

  2234     ;

  2235

  2236     typeconstructor: @{syntax nameref}

  2237     ;

  2238

  2239     class: @{syntax nameref}

  2240     ;

  2241

  2242     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'

  2243     ;

  2244

  2245     @@{attribute (HOL) code} ( 'del' | 'abstype' | 'abstract' )?

  2246     ;

  2247

  2248     @@{command (HOL) code_abort} ( const + )

  2249     ;

  2250

  2251     @@{command (HOL) code_datatype} ( const + )

  2252     ;

  2253

  2254     @@{attribute (HOL) code_unfold} ( 'del' ) ?

  2255     ;

  2256

  2257     @@{attribute (HOL) code_post} ( 'del' ) ?

  2258     ;

  2259

  2260     @@{attribute (HOL) code_abbrev}

  2261     ;

  2262

  2263     @@{command (HOL) code_thms} ( constexpr + ) ?

  2264     ;

  2265

  2266     @@{command (HOL) code_deps} ( constexpr + ) ?

  2267     ;

  2268

  2269     @@{command (HOL) code_reserved} target ( @{syntax string} + )

  2270     ;

  2271

  2272     symbol_const: ( @'constant' const )

  2273     ;

  2274

  2275     symbol_typeconstructor: ( @'type_constructor' typeconstructor )

  2276     ;

  2277

  2278     symbol_class: ( @'type_class' class )

  2279     ;

  2280

  2281     symbol_class_relation: ( @'class_relation' class ( '<' | '\<subseteq>' ) class )

  2282     ;

  2283

  2284     symbol_class_instance: ( @'class_instance' typeconstructor @'::' class )

  2285     ;

  2286

  2287     symbol_module: ( @'code_module' name )

  2288     ;

  2289

  2290     syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}

  2291     ;

  2292

  2293     printing_const: symbol_const ( '\<rightharpoonup>' | '=>' ) \\

  2294       ( '(' target ')' syntax ? + @'and' )

  2295     ;

  2296

  2297     printing_typeconstructor: symbol_typeconstructor ( '\<rightharpoonup>' | '=>' ) \\

  2298       ( '(' target ')' syntax ? + @'and' )

  2299     ;

  2300

  2301     printing_class: symbol_class ( '\<rightharpoonup>' | '=>' )  \\

  2302       ( '(' target ')' @{syntax string} ? + @'and' )

  2303     ;

  2304

  2305     printing_class_relation: symbol_class_relation ( '\<rightharpoonup>' | '=>' )  \\

  2306       ( '(' target ')' @{syntax string} ? + @'and' )

  2307     ;

  2308

  2309     printing_class_instance: symbol_class_instance ( '\<rightharpoonup>' | '=>' )  \\

  2310       ( '(' target ')' '-' ? + @'and' )

  2311     ;

  2312

  2313     printing_module: symbol_module ( '\<rightharpoonup>' | '=>' )  \\

  2314       ( '(' target ')' ( @{syntax string} ( @'attach' ( const + ) ) ? ) ? + @'and' )

  2315     ;

  2316

  2317     @@{command (HOL) code_printing} ( ( printing_const | printing_typeconstructor

  2318       | printing_class | printing_class_relation | printing_class_instance

  2319       | printing_module ) + '|' )

  2320     ;

  2321

  2322     @@{command (HOL) code_const} (const + @'and') \\

  2323       ( ( '(' target ( syntax ? + @'and' ) ')' ) + )

  2324     ;

  2325

  2326     @@{command (HOL) code_type} (typeconstructor + @'and') \\

  2327       ( ( '(' target ( syntax ? + @'and' ) ')' ) + )

  2328     ;

  2329

  2330     @@{command (HOL) code_class} (class + @'and') \\

  2331       ( ( '(' target \\ ( @{syntax string} ? + @'and' ) ')' ) + )

  2332     ;

  2333

  2334     @@{command (HOL) code_instance} (( typeconstructor '::' class ) + @'and') \\

  2335       ( ( '(' target ( '-' ? + @'and' ) ')' ) + )

  2336     ;

  2337

  2338     @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )

  2339     ;

  2340

  2341     @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor

  2342       | symbol_class | symbol_class_relation | symbol_class_instance

  2343       | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \\

  2344       ( '(' target ')' @{syntax string} ? + @'and' ) + '|' )

  2345     ;

  2346

  2347     @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )

  2348     ;

  2349

  2350     @@{command (HOL) code_monad} const const target

  2351     ;

  2352

  2353     @@{command (HOL) code_reflect} @{syntax string} \\

  2354       ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \\

  2355       ( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?

  2356     ;

  2357

  2358     @@{command (HOL) code_pred} \\( '(' @'modes' ':' modedecl ')')? \\ const

  2359     ;

  2360

  2361     modedecl: (modes | ((const ':' modes) \\

  2362          (@'and' ((const ':' modes @'and') +))?))

  2363     ;

  2364

  2365     modes: mode @'as' const

  2366   "}

  2367

  2368   \begin{description}

  2369

  2370   \item @{command (HOL) "export_code"} generates code for a given list

  2371   of constants in the specified target language(s).  If no

  2372   serialization instruction is given, only abstract code is generated

  2373   internally.

  2374

  2375   Constants may be specified by giving them literally, referring to

  2376   all executable contants within a certain theory by giving @{text

  2377   "name.*"}, or referring to \emph{all} executable constants currently

  2378   available by giving @{text "*"}.

  2379

  2380   By default, for each involved theory one corresponding name space

  2381   module is generated.  Alternativly, a module name may be specified

  2382   after the @{keyword "module_name"} keyword; then \emph{all} code is

  2383   placed in this module.

  2384

  2385   For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification

  2386   refers to a single file; for \emph{Haskell}, it refers to a whole

  2387   directory, where code is generated in multiple files reflecting the

  2388   module hierarchy.  Omitting the file specification denotes standard

  2389   output.

  2390

  2391   Serializers take an optional list of arguments in parentheses.  For

  2392   \emph{SML} and \emph{OCaml}, @{text no_signatures} omits

  2393   explicit module signatures.

  2394

  2395   For \emph{Haskell} a module name prefix may be given using the

  2396   @{text "root:"}'' argument; @{text string_classes}'' adds a

  2397   @{verbatim "deriving (Read, Show)"}'' clause to each appropriate

  2398   datatype declaration.

  2399

  2400   \item @{attribute (HOL) code} explicitly selects (or with option

  2401   @{text "del"}'' deselects) a code equation for code generation.

  2402   Usually packages introducing code equations provide a reasonable

  2403   default setup for selection.  Variants @{text "code abstype"} and

  2404   @{text "code abstract"} declare abstract datatype certificates or

  2405   code equations on abstract datatype representations respectively.

  2406

  2407   \item @{command (HOL) "code_abort"} declares constants which are not

  2408   required to have a definition by means of code equations; if needed

  2409   these are implemented by program abort instead.

  2410

  2411   \item @{command (HOL) "code_datatype"} specifies a constructor set

  2412   for a logical type.

  2413

  2414   \item @{command (HOL) "print_codesetup"} gives an overview on

  2415   selected code equations and code generator datatypes.

  2416

  2417   \item @{attribute (HOL) code_unfold} declares (or with option

  2418   @{text "del"}'' removes) theorems which during preprocessing

  2419   are applied as rewrite rules to any code equation or evaluation

  2420   input.

  2421

  2422   \item @{attribute (HOL) code_post} declares (or with option @{text

  2423   "del"}'' removes) theorems which are applied as rewrite rules to any

  2424   result of an evaluation.

  2425

  2426   \item @{attribute (HOL) code_abbrev} declares equations which are

  2427   applied as rewrite rules to any result of an evaluation and

  2428   symmetrically during preprocessing to any code equation or evaluation

  2429   input.

  2430

  2431   \item @{command (HOL) "print_codeproc"} prints the setup of the code

  2432   generator preprocessor.

  2433

  2434   \item @{command (HOL) "code_thms"} prints a list of theorems

  2435   representing the corresponding program containing all given

  2436   constants after preprocessing.

  2437

  2438   \item @{command (HOL) "code_deps"} visualizes dependencies of

  2439   theorems representing the corresponding program containing all given

  2440   constants after preprocessing.

  2441

  2442   \item @{command (HOL) "code_reserved"} declares a list of names as

  2443   reserved for a given target, preventing it to be shadowed by any

  2444   generated code.

  2445

  2446   \item @{command (HOL) "code_printing"} associates a series of symbols

  2447   (constants, type constructors, classes, class relations, instances,

  2448   module names) with target-specific serializations; omitting a serialization

  2449   deletes an existing serialization.  Legacy variants of this are

  2450   @{command (HOL) "code_const"}, @{command (HOL) "code_type"},

  2451   @{command (HOL) "code_class"}, @{command (HOL) "code_instance"},

  2452   @{command (HOL) "code_include"}.

  2453

  2454   \item @{command (HOL) "code_monad"} provides an auxiliary mechanism

  2455   to generate monadic code for Haskell.

  2456

  2457   \item @{command (HOL) "code_identifier"} associates a a series of symbols

  2458   (constants, type constructors, classes, class relations, instances,

  2459   module names) with target-specific hints how these symbols shall be named.

  2460   \emph{Warning:} These hints are still subject to name disambiguation.

  2461   @{command (HOL) "code_modulename"} is a legacy variant for

  2462   @{command (HOL) "code_identifier"} on module names.

  2463

  2464   \item @{command (HOL) "code_reflect"} without a @{text "file"}''

  2465   argument compiles code into the system runtime environment and

  2466   modifies the code generator setup that future invocations of system

  2467   runtime code generation referring to one of the @{text

  2468   "datatypes"}'' or @{text "functions"}'' entities use these

  2469   precompiled entities.  With a @{text "file"}'' argument, the

  2470   corresponding code is generated into that specified file without

  2471   modifying the code generator setup.

  2472

  2473   \item @{command (HOL) "code_pred"} creates code equations for a

  2474     predicate given a set of introduction rules. Optional mode

  2475     annotations determine which arguments are supposed to be input or

  2476     output. If alternative introduction rules are declared, one must

  2477     prove a corresponding elimination rule.

  2478

  2479   \end{description}

  2480 *}

  2481

  2482 end