src/Doc/Isar_Ref/HOL_Specific.thy
 author wenzelm Wed Mar 25 11:39:52 2015 +0100 (2015-03-25) changeset 59809 87641097d0f3 parent 59785 4e6ab5831cc0 child 59845 fafb4d12c307 permissions -rw-r--r--
tuned signature;
     1 theory HOL_Specific

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

     3   "~~/src/Tools/Adhoc_Overloading"

     4 begin

     5

     6 chapter \<open>Higher-Order Logic\<close>

     7

     8 text \<open>Isabelle/HOL is based on Higher-Order Logic, a polymorphic

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

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

    11   logic was first implemented in Gordon's HOL system

    12   @{cite "mgordon-hol"}.  It extends Church's original logic

    13   @{cite "church40"} by explicit type variables (naive polymorphism) and

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

    15   existing types.

    16

    17   Andrews's book @{cite andrews86} is a full description of the

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

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

    20   particular extensions of Gordon-style HOL are explained semantically

    21   in two chapters of the 1993 HOL book @{cite pitts93}.

    22

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

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

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

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

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

    28   which is traditionally considered the standard foundation of regular

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

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

    31

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

    33   functional programming.  Function application is curried.  To apply

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

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

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

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

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

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

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

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

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

    43

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

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

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

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

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

    49   abstraction and application.

    50

    51   These identifications allow Isabelle to support HOL particularly

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

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

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

    55   the standard libraries and applications.  Beginners can set

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

    57   explicit information about the result of type-inference.\<close>

    58

    59

    60 chapter \<open>Derived specification elements\<close>

    61

    62 section \<open>Inductive and coinductive definitions \label{sec:hol-inductive}\<close>

    63

    64 text \<open>

    65   \begin{matharray}{rcl}

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

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

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

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

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

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

    72   \end{matharray}

    73

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

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

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

    77   structural operational semantics is an inductive definition of an

    78   evaluation relation.

    79

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

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

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

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

    84   bisimulation relations to formalise equivalence of processes and

    85   infinite data structures.

    86

    87   Both inductive and coinductive definitions are based on the

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

    89   collection of introduction rules given by the user determines a

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

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

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

    93   works by pushing inclusion through logical connectives and any other

    94   operator that might be wrapped around recursive occurrences of the

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

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

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

    98   already take care of most common situations.

    99

   100   @{rail \<open>

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

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

   103       @{syntax "fixes"} @{syntax "for_fixes"} \<newline>

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

   105     ;

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

   107     ;

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

   109   \<close>}

   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 \<close>

   148

   149

   150 subsection \<open>Derived rules\<close>

   151

   152 text \<open>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 \<close>

   179

   180

   181 subsection \<open>Monotonicity theorems\<close>

   182

   183 text \<open>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 \<close>

   218

   219 subsubsection \<open>Examples\<close>

   220

   221 text \<open>The finite powerset operator can be defined inductively like this:\<close>

   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 \<open>The accessible part of a relation is defined as follows:\<close>

   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 \<open>Common logical connectives can be easily characterized as

   235 non-recursive inductive definitions with parameters, but without

   236 arguments.\<close>

   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 \<open>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.\<close>

   254

   255

   256 section \<open>Recursive functions \label{sec:recursion}\<close>

   257

   258 text \<open>

   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     @{command_def (HOL) "fun_cases"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   265   \end{matharray}

   266

   267   @{rail \<open>

   268     @@{command (HOL) primrec} @{syntax "fixes"} @'where' equations

   269     ;

   270     (@@{command (HOL) fun} | @@{command (HOL) function}) functionopts?

   271       @{syntax "fixes"} \<newline> @'where' equations

   272     ;

   273

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

   275     ;

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

   277     ;

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

   279     ;

   280     @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')

   281   \<close>}

   282

   283   \begin{description}

   284

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

   286   functions over datatypes (see also @{command_ref (HOL) datatype}).

   287   The given @{text equations} specify reduction rules that are produced

   288   by instantiating the generic combinator for primitive recursion that

   289   is available for each datatype.

   290

   291   Each equation needs to be of the form:

   292

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

   294

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

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

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

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

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

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

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

   302   access for users.

   303

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

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

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

   307   datatype constructions, by simulating symbolic computation via

   308   rewriting.

   309

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

   311   wellfounded recursion. A detailed description with examples can be

   312   found in @{cite "isabelle-function"}. The function is specified by a

   313   set of (possibly conditional) recursive equations with arbitrary

   314   pattern matching. The command generates proof obligations for the

   315   completeness and the compatibility of patterns.

   316

   317   The defined function is considered partial, and the resulting

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

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

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

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

   322

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

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

   325   proof attempts regarding pattern matching and termination.  See

   326   @{cite "isabelle-function"} for further details.

   327

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

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

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

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

   332   the induction principle is established.

   333

   334   \item @{command (HOL) "fun_cases"} generates specialized elimination

   335   rules for function equations. It expects one or more function equations

   336   and produces rules that eliminate the given equalities, following the cases

   337   given in the function definition.

   338   \end{description}

   339

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

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

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

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

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

   345   induction principle coincides with structural recursion on the

   346   datatype where the recursion is carried out.

   347

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

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

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

   351   explicitly as well.

   352

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

   354   options.

   355

   356   \begin{description}

   357

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

   359   overlapping patterns by making them mutually disjoint.  Earlier

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

   361   specification in a format very similar to functional programming.

   362   Note that the resulting simplification and induction rules

   363   correspond to the transformed specification, not the one given

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

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

   366   transformation only works for ML-style datatype patterns.

   367

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

   369   introduction rules for the domain predicate. While mostly not

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

   371

   372   \end{description}

   373 \<close>

   374

   375 subsubsection \<open>Example: evaluation of expressions\<close>

   376

   377 text \<open>Subsequently, we define mutual datatypes for arithmetic and

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

   379   functions that follow the same recursive structure.\<close>

   380

   381 datatype 'a aexp =

   382     IF "'a bexp"  "'a aexp"  "'a aexp"

   383   | Sum "'a aexp"  "'a aexp"

   384   | Diff "'a aexp"  "'a aexp"

   385   | Var 'a

   386   | Num nat

   387 and 'a bexp =

   388     Less "'a aexp"  "'a aexp"

   389   | And "'a bexp"  "'a bexp"

   390   | Neg "'a bexp"

   391

   392

   393 text \<open>\medskip Evaluation of arithmetic and boolean expressions\<close>

   394

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

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

   397 where

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

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

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

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

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

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

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

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

   406

   407 text \<open>Since the value of an expression depends on the value of its

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

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

   410   their values.

   411

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

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

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

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

   416 \<close>

   417

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

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

   420 where

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

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

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

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

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

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

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

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

   429

   430 text \<open>In textbooks about semantics one often finds substitution

   431   theorems, which express the relationship between substitution and

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

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

   434 \<close>

   435

   436 lemma subst_one:

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

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

   439   by (induct a and b) simp_all

   440

   441 lemma subst_all:

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

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

   444   by (induct a and b) simp_all

   445

   446

   447 subsubsection \<open>Example: a substitution function for terms\<close>

   448

   449 text \<open>Functions on datatypes with nested recursion are also defined

   450   by mutual primitive recursion.\<close>

   451

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

   453

   454 text \<open>A substitution function on type @{typ "('a, 'b) term"} can be

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

   456   term list"}:\<close>

   457

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

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

   460 where

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

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

   463 | "subst_term_list f [] = []"

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

   465

   466 text \<open>The recursion scheme follows the structure of the unfolded

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

   468   substitution function, mutual induction is needed:

   469 \<close>

   470

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

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

   473   by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all

   474

   475

   476 subsubsection \<open>Example: a map function for infinitely branching trees\<close>

   477

   478 text \<open>Defining functions on infinitely branching datatypes by

   479   primitive recursion is just as easy.

   480 \<close>

   481

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

   483

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

   485 where

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

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

   488

   489 text \<open>Note that all occurrences of functions such as @{text ts}

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

   491   "map_tree f \<circ> ts"} is not allowed here.\<close>

   492

   493 text \<open>Here is a simple composition lemma for @{term map_tree}:\<close>

   494

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

   496   by (induct t) simp_all

   497

   498

   499 subsection \<open>Proof methods related to recursive definitions\<close>

   500

   501 text \<open>

   502   \begin{matharray}{rcl}

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

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

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

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

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

   508   \end{matharray}

   509

   510   @{rail \<open>

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

   512     ;

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

   514     ;

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

   516     ;

   517     @@{method (HOL) induction_schema}

   518     ;

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

   520   \<close>}

   521

   522   \begin{description}

   523

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

   525   solve goals regarding the completeness of pattern matching, as

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

   527   @{cite "isabelle-function"}).

   528

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

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

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

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

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

   534   termination proofs.

   535

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

   537   automated termination proof by searching for a lexicographic

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

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

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

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

   542

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

   544   to analyse the situation (cf.\ @{cite "isabelle-function"}).

   545

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

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

   548   graph decomposition technique (see @{cite krauss_phd} for details).

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

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

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

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

   553   internally.

   554

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

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

   557

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

   559   induction rules from well-founded induction and completeness of

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

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

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

   563

   564   \end{description}

   565 \<close>

   566

   567

   568 subsection \<open>Functions with explicit partiality\<close>

   569

   570 text \<open>

   571   \begin{matharray}{rcl}

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

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

   574   \end{matharray}

   575

   576   @{rail \<open>

   577     @@{command (HOL) partial_function} '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>

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

   579   \<close>}

   580

   581   \begin{description}

   582

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

   584   recursive functions based on fixpoints in complete partial

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

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

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

   588   explicit bottom element.

   589

   590   Pattern matching and mutual recursion are currently not supported.

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

   592   single recursive equation.

   593

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

   595   function, but the induced functional must be provably monotonic

   596   wrt.\ the underlying order.  The monotonicity proof is performed

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

   598   can be influenced by declaring hints using the

   599   @{attribute (HOL) partial_function_mono} attribute.

   600

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

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

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

   604   defined:

   605

   606   \begin{description}

   607

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

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

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

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

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

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

   614

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

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

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

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

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

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

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

   622   definition of arbitrary tail-recursive functions.

   623

   624   \end{description}

   625

   626   Experienced users may define new modes by instantiating the locale

   627   @{const "partial_function_definitions"} appropriately.

   628

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

   630   use in the internal monotonicity proofs of partial function

   631   definitions.

   632

   633   \end{description}

   634

   635 \<close>

   636

   637

   638 subsection \<open>Old-style recursive function definitions (TFL)\<close>

   639

   640 text \<open>

   641   \begin{matharray}{rcl}

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

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

   644   \end{matharray}

   645

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

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

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

   649

   650   @{rail \<open>

   651     @@{command (HOL) recdef} ('(' @'permissive' ')')? \<newline>

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

   653     ;

   654     recdeftc @{syntax thmdecl}? tc

   655     ;

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

   657     ;

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

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

   660     ;

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

   662   \<close>}

   663

   664   \begin{description}

   665

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

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

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

   669   TFL to recover from failed proof attempts, returning unfinished

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

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

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

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

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

   675   \secref{sec:classical}).

   676

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

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

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

   680   constant @{text c}.

   681

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

   683   its internal proofs without manual intervention.

   684

   685   \end{description}

   686

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

   688   globally, using the following attributes.

   689

   690   \begin{matharray}{rcl}

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

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

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

   694   \end{matharray}

   695

   696   @{rail \<open>

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

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

   699   \<close>}

   700 \<close>

   701

   702

   703 section \<open>Old-style datatypes \label{sec:hol-datatype}\<close>

   704

   705 text \<open>

   706   \begin{matharray}{rcl}

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

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

   709   \end{matharray}

   710

   711   @{rail \<open>

   712     @@{command (HOL) old_datatype} (spec + @'and')

   713     ;

   714     @@{command (HOL) old_rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)

   715     ;

   716

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

   718     ;

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

   720   \<close>}

   721

   722   \begin{description}

   723

   724   \item @{command (HOL) "old_datatype"} defines old-style inductive

   725   datatypes in HOL.

   726

   727   \item @{command (HOL) "old_rep_datatype"} represents existing types as

   728   old-style datatypes.

   729

   730   \end{description}

   731

   732   These commands are mostly obsolete; @{command (HOL) "datatype"}

   733   should be used instead.

   734

   735   See @{cite "isabelle-HOL"} for more details on datatypes, but beware of

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

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

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

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

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

   741   internally bound parameters).

   742 \<close>

   743

   744

   745 subsubsection \<open>Examples\<close>

   746

   747 text \<open>We define a type of finite sequences, with slightly different

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

   749   Main}:\<close>

   750

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

   752

   753 text \<open>We can now prove some simple lemma by structural induction:\<close>

   754

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

   756 proof (induct xs arbitrary: x)

   757   case Empty

   758   txt \<open>This case can be proved using the simplifier: the freeness

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

   760     simp} rules.\<close>

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

   762     by simp

   763 next

   764   case (Seq y ys)

   765   txt \<open>The step case is proved similarly.\<close>

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

   767     using \<open>Seq y ys \<noteq> ys\<close> by simp

   768 qed

   769

   770 text \<open>Here is a more succinct version of the same proof:\<close>

   771

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

   773   by (induct xs arbitrary: x) simp_all

   774

   775

   776 section \<open>Records \label{sec:hol-record}\<close>

   777

   778 text \<open>

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

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

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

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

   783   admits operations that are polymorphic with respect to record

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

   785   inheritance.  See also @{cite "NaraschewskiW-TPHOLs98"} for more

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

   787 \<close>

   788

   789

   790 subsection \<open>Basic concepts\<close>

   791

   792 text \<open>

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

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

   795

   796   \begin{center}

   797   \begin{tabular}{l|l|l}

   798     & record terms & record types \\ \hline

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

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

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

   802   \end{tabular}

   803   \end{center}

   804

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

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

   807

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

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

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

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

   812

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

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

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

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

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

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

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

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

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

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

   823   Fixed records are special instances of record schemes, where

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

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

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

   827

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

   829   typed language like HOL work out:

   830

   831   \begin{enumerate}

   832

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

   834   variable,

   835

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

   837   the logic as first-class values.

   838

   839   \end{enumerate}

   840

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

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

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

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

   845   The record package provides several standard operations like

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

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

   848   tutorial @{cite "isabelle-hol-book"} for further instructions on using

   849   records in practice.

   850 \<close>

   851

   852

   853 subsection \<open>Record specifications\<close>

   854

   855 text \<open>

   856   \begin{matharray}{rcl}

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

   858   \end{matharray}

   859

   860   @{rail \<open>

   861     @@{command (HOL) record} @{syntax typespec_sorts} '=' \<newline>

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

   863     ;

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

   865   \<close>}

   866

   867   \begin{description}

   868

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

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

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

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

   873

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

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

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

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

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

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

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

   881   the record name internally.

   882

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

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

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

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

   887   merge multiple parent records!

   888

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

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

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

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

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

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

   895

   896   \end{description}

   897 \<close>

   898

   899

   900 subsection \<open>Record operations\<close>

   901

   902 text \<open>

   903   Any record definition of the form presented above produces certain

   904   standard operations.  Selectors and updates are provided for any

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

   906   cumulative record constructor functions.  To simplify the

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

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

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

   910

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

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

   913

   914   \begin{matharray}{lll}

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

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

   917   \end{matharray}

   918

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

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

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

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

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

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

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

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

   927   Thus commutativity of independent updates can be proven within the

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

   929

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

   931   constructor function:

   932

   933   \begin{matharray}{lll}

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

   935   \end{matharray}

   936

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

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

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

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

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

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

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

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

   945   the above record operations will get the following types:

   946

   947   \medskip

   948   \begin{tabular}{lll}

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

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

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

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

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

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

   955   \end{tabular}

   956   \medskip

   957

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

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

   960   record fragment consisting of exactly the new fields introduced here

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

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

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

   964

   965   \medskip

   966   \begin{tabular}{lll}

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

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

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

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

   971   \end{tabular}

   972   \medskip

   973

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

   975   for root records.

   976 \<close>

   977

   978

   979 subsection \<open>Derived rules and proof tools\<close>

   980

   981 text \<open>

   982   The record package proves several results internally, declaring

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

   984   reason about record structures quite conveniently.  Assume that

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

   986

   987   \begin{enumerate}

   988

   989   \item Standard conversions for selectors or updates applied to

   990   record constructor terms are made part of the default Simplifier

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

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

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

   994

   995   \item Selectors applied to updated records are automatically reduced

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

   997   standard Simplifier setup.

   998

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

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

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

  1002   @{text "t.iffs"}.

  1003

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

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

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

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

  1008

  1009   \item Representations of arbitrary record expressions as canonical

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

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

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

  1013   fixed records, record schemes, more parts etc.

  1014

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

  1016   sensible rule according to the type of the indicated record

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

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

  1019

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

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

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

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

  1024

  1025   \end{enumerate}

  1026 \<close>

  1027

  1028

  1029 subsubsection \<open>Examples\<close>

  1030

  1031 text \<open>See @{file "~~/src/HOL/ex/Records.thy"}, for example.\<close>

  1032

  1033 section \<open>Typedef axiomatization \label{sec:hol-typedef}\<close>

  1034

  1035 text \<open>

  1036   \begin{matharray}{rcl}

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

  1038   \end{matharray}

  1039

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

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

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

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

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

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

  1046   postulated that establish an isomorphism between the new type and

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

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

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

  1050   those type arguments.

  1051

  1052   The axiomatization can be considered a definition'' in the sense of the

  1053   particular set-theoretic interpretation of HOL @{cite pitts93}, where the

  1054   universe of types is required to be downwards-closed wrt.\ arbitrary

  1055   non-empty subsets. Thus genuinely new types introduced by @{command

  1056   "typedef"} stay within the range of HOL models by construction.

  1057

  1058   In contrast, the command @{command_ref type_synonym} from Isabelle/Pure

  1059   merely introduces syntactic abbreviations, without any logical

  1060   significance. Thus it is more faithful to the idea of a genuine type

  1061   definition, but less powerful in practice.

  1062

  1063   @{rail \<open>

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

  1065     ;

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

  1067     ;

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

  1069   \<close>}

  1070

  1071   \begin{description}

  1072

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

  1074   axiomatization (\secref{sec:axiomatizations}) for a type definition in the

  1075   background theory of the current context, depending on a non-emptiness

  1076   result of the set @{text A} that needs to be proven here. The set @{text

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

  1078   LHS, but no term variables.

  1079

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

  1081   constructor cannot depend on parameters or assumptions of the

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

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

  1084   which could result in different interpretations in target contexts:

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

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

  1087   contexts.

  1088

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

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

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

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

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

  1094   allows to provide alternative names.

  1095

  1096   The core axiomatization uses the locale predicate @{const

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

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

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

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

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

  1102

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

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

  1105   provide the most basic characterization as a corresponding

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

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

  1108   type_definition.Abs_inject} provide a more convenient version of

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

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

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

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

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

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

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

  1116   respectively.

  1117

  1118   \end{description}

  1119 \<close>

  1120

  1121 subsubsection \<open>Examples\<close>

  1122

  1123 text \<open>Type definitions permit the introduction of abstract data

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

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

  1126   of a type, this involves two steps:

  1127

  1128   \begin{enumerate}

  1129

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

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

  1132   based on this representation.

  1133

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

  1135   from the representation.

  1136

  1137   \end{enumerate}

  1138

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

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

  1141

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

  1143   into existence within the formal logical environment of HOL.\<close>

  1144

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

  1146   by blast

  1147

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

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

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

  1151

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

  1153   by (simp_all add: One_def Two_def Three_def Abs_three_inject)

  1154

  1155 lemma three_cases:

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

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

  1158

  1159 text \<open>Note that such trivial constructions are better done with

  1160   derived specification mechanisms such as @{command datatype}:\<close>

  1161

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

  1163

  1164 text \<open>This avoids re-doing basic definitions and proofs from the

  1165   primitive @{command typedef} above.\<close>

  1166

  1167

  1168

  1169 section \<open>Functorial structure of types\<close>

  1170

  1171 text \<open>

  1172   \begin{matharray}{rcl}

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

  1174   \end{matharray}

  1175

  1176   @{rail \<open>

  1177     @@{command (HOL) functor} (@{syntax name} ':')? @{syntax term}

  1178   \<close>}

  1179

  1180   \begin{description}

  1181

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

  1183   prove and register properties about the functorial structure of type

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

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

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

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

  1188   constructor, an explicit prefix can be given alternatively.

  1189

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

  1191   corresponding type constructor and must conform to the following

  1192   type pattern:

  1193

  1194   \begin{matharray}{lll}

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

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

  1197   \end{matharray}

  1198

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

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

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

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

  1203   \<beta>\<^sub>1"}, @{text "\<beta>\<^sub>1 \<Rightarrow> \<alpha>\<^sub>1"}, \ldots,

  1204   @{text "\<alpha>\<^sub>n \<Rightarrow> \<beta>\<^sub>n"}, @{text "\<beta>\<^sub>n \<Rightarrow>

  1205   \<alpha>\<^sub>n"}.

  1206

  1207   \end{description}

  1208 \<close>

  1209

  1210

  1211 section \<open>Quotient types\<close>

  1212

  1213 text \<open>

  1214   \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1233   \end{matharray}

  1234

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

  1236   and a partial equivalence relation. The package also historically

  1237   includes automation for transporting definitions and theorems.

  1238   But most of this automation was superseded by the Lifting and Transfer

  1239   packages. The user should consider using these two new packages for

  1240   lifting definitions and transporting theorems.

  1241

  1242   @{rail \<open>

  1243     @@{command (HOL) quotient_type} (spec)

  1244     ;

  1245     spec: @{syntax typespec} @{syntax mixfix}? '=' \<newline>

  1246      @{syntax type} '/' ('partial' ':')? @{syntax term} \<newline>

  1247      (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})?

  1248   \<close>}

  1249

  1250   @{rail \<open>

  1251     @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \<newline>

  1252     @{syntax term} 'is' @{syntax term}

  1253     ;

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

  1255   \<close>}

  1256

  1257   @{rail \<open>

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

  1259     ;

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

  1261   \<close>}

  1262

  1263   \begin{description}

  1264

  1265   \item @{command (HOL) "quotient_type"} defines a new quotient type @{text \<tau>}. The

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

  1267   rep_\<tau>}, its inverse @{text abs_\<tau>} unless explicit @{keyword (HOL)

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

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

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

  1271   user specifies explicitly @{text partial} in which case the

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

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

  1274   automatically.

  1275

  1276   The command internally proves a Quotient theorem and sets up the Lifting

  1277   package by the command @{command (HOL) setup_lifting}. Thus the Lifting

  1278   and Transfer packages can be used also with quotient types defined by

  1279   @{command (HOL) "quotient_type"} without any extra set-up. The parametricity

  1280   theorem for the equivalence relation R can be provided as an extra argument

  1281   of the command and is passed to the corresponding internal call of @{command (HOL) setup_lifting}.

  1282   This theorem allows the Lifting package to generate a stronger transfer rule for equality.

  1283

  1284   \end{description}

  1285

  1286   The most of the rest of the package was superseded by the Lifting and Transfer

  1287   packages. The user should consider using these two new packages for

  1288   lifting definitions and transporting theorems.

  1289

  1290   \begin{description}

  1291

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

  1293   the quotient type.

  1294

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

  1296   functions.

  1297

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

  1299

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

  1301

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

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

  1304     lifted producing three new subgoals: regularization, injection and

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

  1306     heuristics for automatically solving these three subgoals and

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

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

  1309     subgoals unsolved.

  1310

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

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

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

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

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

  1316     to solve the arising regularization, injection and cleaning

  1317     subgoals with the analogous method @{method (HOL)

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

  1319

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

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

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

  1323     equivalence quotients where the non regularized statements would

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

  1325     the injection and cleaning subgoals unchanged.

  1326

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

  1328     heuristics to the current subgoal.

  1329

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

  1331     to the current goal using the stored quotient respectfulness

  1332     theorems.

  1333

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

  1335     heuristics to the current subgoal using the stored quotient

  1336     preservation theorems.

  1337

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

  1339     automatically transport the theorem to the quotient type.

  1340     The attribute uses all the defined quotients types and quotient

  1341     constants often producing undesired results or theorems that

  1342     cannot be lifted.

  1343

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

  1345     quot_preserve} attributes declare a theorem as a respectfulness

  1346     and preservation theorem respectively.  These are stored in the

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

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

  1349

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

  1351     is a quotient extension theorem. Quotient extension theorems

  1352     allow for quotienting inside container types. Given a polymorphic

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

  1354     container using @{command (HOL) "functor"} and a relation

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

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

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

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

  1359     theorems.

  1360

  1361   \end{description}

  1362 \<close>

  1363

  1364

  1365 section \<open>Definition by specification \label{sec:hol-specification}\<close>

  1366

  1367 text \<open>

  1368   \begin{matharray}{rcl}

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

  1370   \end{matharray}

  1371

  1372   @{rail \<open>

  1373     @@{command (HOL) specification} '(' (decl +) ')' \<newline>

  1374       (@{syntax thmdecl}? @{syntax prop} +)

  1375     ;

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

  1377   \<close>}

  1378

  1379   \begin{description}

  1380

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

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

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

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

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

  1386   constants.

  1387

  1388   @{text decl} declares a constant to be defined by the

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

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

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

  1392

  1393   \end{description}

  1394 \<close>

  1395

  1396

  1397 section \<open>Adhoc overloading of constants\<close>

  1398

  1399 text \<open>

  1400   \begin{tabular}{rcll}

  1401   @{command_def "adhoc_overloading"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

  1402   @{command_def "no_adhoc_overloading"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

  1403   @{attribute_def "show_variants"} & : & @{text "attribute"} & default @{text false} \\

  1404   \end{tabular}

  1405

  1406   \medskip

  1407

  1408   Adhoc overloading allows to overload a constant depending on

  1409   its type. Typically this involves the introduction of an

  1410   uninterpreted constant (used for input and output) and the addition

  1411   of some variants (used internally). For examples see

  1412   @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and

  1413   @{file "~~/src/HOL/Library/Monad_Syntax.thy"}.

  1414

  1415   @{rail \<open>

  1416     (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})

  1417       (@{syntax nameref} (@{syntax term} + ) + @'and')

  1418   \<close>}

  1419

  1420   \begin{description}

  1421

  1422   \item @{command "adhoc_overloading"}~@{text "c v\<^sub>1 ... v\<^sub>n"}

  1423   associates variants with an existing constant.

  1424

  1425   \item @{command "no_adhoc_overloading"} is similar to

  1426   @{command "adhoc_overloading"}, but removes the specified variants

  1427   from the present context.

  1428

  1429   \item @{attribute "show_variants"} controls printing of variants

  1430   of overloaded constants. If enabled, the internally used variants

  1431   are printed instead of their respective overloaded constants. This

  1432   is occasionally useful to check whether the system agrees with a

  1433   user's expectations about derived variants.

  1434

  1435   \end{description}

  1436 \<close>

  1437

  1438

  1439 chapter \<open>Proof tools\<close>

  1440

  1441 section \<open>Adhoc tuples\<close>

  1442

  1443 text \<open>

  1444   \begin{matharray}{rcl}

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

  1446   \end{matharray}

  1447

  1448   @{rail \<open>

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

  1450   \<close>}

  1451

  1452   \begin{description}

  1453

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

  1455   arguments in function applications to be represented canonically

  1456   according to their tuple type structure.

  1457

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

  1459   parameters introduced.

  1460

  1461   \end{description}

  1462 \<close>

  1463

  1464

  1465 section \<open>Transfer package\<close>

  1466

  1467 text \<open>

  1468   \begin{matharray}{rcl}

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

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

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

  1472     @{attribute_def (HOL) "Transfer.transferred"} & : & @{text attribute} \\

  1473     @{attribute_def (HOL) "untransferred"} & : & @{text attribute} \\

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

  1475     @{attribute_def (HOL) "transfer_domain_rule"} & : & @{text attribute} \\

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

  1477     @{attribute_def (HOL) "relator_domain"} & : & @{text attribute} \\

  1478   \end{matharray}

  1479

  1480   \begin{description}

  1481

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

  1483     with a logically equivalent one that uses different types and

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

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

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

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

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

  1489

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

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

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

  1493     subgoal involving equality on a quotient type could be replaced

  1494     with a subgoal involving equality (instead of the corresponding

  1495     equivalence relation) on the underlying raw type.

  1496

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

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

  1499     defined in terms of other constants that already have transfer

  1500     rules. It should be applied after unfolding the constant

  1501     definitions.

  1502

  1503   \item @{attribute (HOL) "untransferred"} proves the same equivalent theorem

  1504      as @{method (HOL) "transfer"} internally does.

  1505

  1506   \item @{attribute (HOL) Transfer.transferred} works in the opposite

  1507     direction than @{method (HOL) "transfer'"}. E.g., given the transfer

  1508     relation @{text "ZN x n \<equiv> (x = int n)"}, corresponding transfer rules and the theorem

  1509     @{text "\<forall>x::int \<in> {0..}. x < x + 1"}, the attribute would prove

  1510     @{text "\<forall>n::nat. n < n + 1"}. The attribute is still in experimental

  1511     phase of development.

  1512

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

  1514     collection of transfer rules, which relate constants at two

  1515     different types. Typical transfer rules may relate different type

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

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

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

  1519

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

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

  1522

  1523     Lemmas involving predicates on relations can also be registered

  1524     using the same attribute. For example:

  1525

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

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

  1528

  1529     Preservation of predicates on relations (@{text "bi_unique, bi_total,

  1530     right_unique, right_total, left_unique, left_total"}) with the respect to a relator

  1531     is proved automatically if the involved type is BNF

  1532     @{cite "isabelle-datatypes"} without dead variables.

  1533

  1534   \item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection

  1535     of rules, which specify a domain of a transfer relation by a predicate.

  1536     E.g., given the transfer relation @{text "ZN x n \<equiv> (x = int n)"},

  1537     one can register the following transfer domain rule:

  1538     @{text "Domainp ZN = (\<lambda>x. x \<ge> 0)"}. The rules allow the package to produce

  1539     more readable transferred goals, e.g., when quantifiers are transferred.

  1540

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

  1542     for relators of various type constructors, e.g. @{term "rel_set

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

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

  1545     the fly. For examples see @{file

  1546     "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.

  1547     This property is proved automatically if the involved type is BNF without dead variables.

  1548

  1549   \item @{attribute_def (HOL) "relator_domain"} attribute collects rules

  1550     describing domains of relators by predicators. E.g.,

  1551     @{term "Domainp (rel_set T) = (\<lambda>A. Ball A (Domainp T))"}. This allows the package

  1552     to lift transfer domain rules through type constructors. For examples see @{file

  1553     "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.

  1554     This property is proved automatically if the involved type is BNF without dead variables.

  1555

  1556   \end{description}

  1557

  1558   Theoretical background can be found in @{cite "Huffman-Kuncar:2013:lifting_transfer"}.

  1559 \<close>

  1560

  1561

  1562 section \<open>Lifting package\<close>

  1563

  1564 text \<open>

  1565   The Lifting package allows users to lift terms of the raw type to the abstract type, which is

  1566   a necessary step in building a library for an abstract type. Lifting defines a new constant

  1567   by combining coercion functions (Abs and Rep) with the raw term. It also proves an appropriate

  1568   transfer rule for the Transfer package and, if possible, an equation for the code generator.

  1569

  1570   The Lifting package provides two main commands: @{command (HOL) "setup_lifting"} for initializing

  1571   the package to work with a new type, and @{command (HOL) "lift_definition"} for lifting constants.

  1572   The Lifting package works with all four kinds of type abstraction: type copies, subtypes,

  1573   total quotients and partial quotients.

  1574

  1575   Theoretical background can be found in @{cite "Huffman-Kuncar:2013:lifting_transfer"}.

  1576

  1577   \begin{matharray}{rcl}

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

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

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

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

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

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

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

  1585     @{attribute_def (HOL) "relator_eq_onp"} & : & @{text attribute} \\

  1586     @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\

  1587     @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\

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

  1589     @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\

  1590   \end{matharray}

  1591

  1592   @{rail \<open>

  1593     @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \<newline>

  1594       (@'parametric' @{syntax thmref})?

  1595   \<close>}

  1596

  1597   @{rail \<open>

  1598     @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type}  @{syntax mixfix}? \<newline>

  1599       'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?

  1600   \<close>}

  1601

  1602   @{rail \<open>

  1603     @@{command (HOL) lifting_forget} @{syntax nameref}

  1604   \<close>}

  1605

  1606   @{rail \<open>

  1607     @@{command (HOL) lifting_update} @{syntax nameref}

  1608   \<close>}

  1609

  1610   @{rail \<open>

  1611     @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?

  1612   \<close>}

  1613

  1614   \begin{description}

  1615

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

  1617     to work with a user-defined type.

  1618     The command supports two modes. The first one is a low-level mode when

  1619     the user must provide as a first

  1620     argument of @{command (HOL) "setup_lifting"} a

  1621     quotient theorem @{term "Quotient R Abs Rep T"}. The

  1622     package configures a transfer rule for equality, a domain transfer

  1623     rules and sets up the @{command_def (HOL) "lift_definition"}

  1624     command to work with the abstract type. An optional theorem @{term "reflp R"}, which certifies that

  1625     the equivalence relation R is total,

  1626     can be provided as a second argument. This allows the package to generate stronger transfer

  1627     rules. And finally, the parametricity theorem for R can be provided as a third argument.

  1628     This allows the package to generate a stronger transfer rule for equality.

  1629

  1630     Users generally will not prove the @{text Quotient} theorem manually for

  1631     new types, as special commands exist to automate the process.

  1632

  1633     When a new subtype is defined by @{command (HOL) typedef}, @{command (HOL) "lift_definition"}

  1634     can be used in its

  1635     second mode, where only the type_definition theorem @{text "type_definition Rep Abs A"}

  1636     is used as an argument of the command. The command internally proves the corresponding

  1637     Quotient theorem and registers it with @{command (HOL) setup_lifting} using its first mode.

  1638

  1639     For quotients, the command @{command (HOL) quotient_type} can be used. The command defines

  1640     a new quotient type and similarly to the previous case, the corresponding Quotient theorem is proved

  1641     and registered by @{command (HOL) setup_lifting}.

  1642

  1643     The command @{command (HOL) "setup_lifting"} also sets up the code generator

  1644     for the new type. Later on, when a new constant is defined by @{command (HOL) "lift_definition"},

  1645     the Lifting package proves and registers a code equation (if there is one) for the new constant.

  1646

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

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

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

  1650     representation type. More formally, if @{text "t :: \<sigma>"}, then

  1651     the command builds a term @{text "F"} as a corresponding combination of abstraction

  1652     and representation functions such that @{text "F :: \<sigma> \<Rightarrow> \<tau>" } and

  1653     defines @{text f} is as @{text "f \<equiv> F t"}.

  1654     The term @{text t} does not have to be necessarily a constant but it can be any term.

  1655

  1656     The command opens a proof environment and the user must discharge

  1657     a respectfulness proof obligation. For a type copy, i.e., a typedef with @{text

  1658     UNIV}, the obligation is discharged automatically. The proof goal is

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

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

  1661     @{text f.transfer} for the Transfer package are generated by the

  1662     package.

  1663

  1664     The user can specify a parametricity theorems for @{text t} after the keyword

  1665     @{keyword "parametric"}, which allows the command

  1666     to generate parametric transfer rules for @{text f}.

  1667

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

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

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

  1671

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

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

  1674     the abstraction function.

  1675

  1676     Integration with [@{attribute code} abstract]: For subtypes (e.g.,

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

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

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

  1680

  1681     Integration with [@{attribute code} equation]: For total quotients, @{command

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

  1683

  1684   \item @{command (HOL) lifting_forget} and  @{command (HOL) lifting_update}

  1685     These two commands serve for storing and deleting the set-up of

  1686     the Lifting package and corresponding transfer rules defined by this package.

  1687     This is useful for hiding of type construction details of an abstract type

  1688     when the construction is finished but it still allows additions to this construction

  1689     when this is later necessary.

  1690

  1691     Whenever the Lifting package is set up with a new abstract type @{text "\<tau>"} by

  1692     @{command_def (HOL) "lift_definition"}, the package defines a new bundle

  1693     that is called @{text "\<tau>.lifting"}. This bundle already includes set-up for the Lifting package.

  1694     The new transfer rules

  1695     introduced by @{command (HOL) "lift_definition"} can be stored in the bundle by

  1696     the command @{command (HOL) "lifting_update"} @{text "\<tau>.lifting"}.

  1697

  1698     The command @{command (HOL) "lifting_forget"} @{text "\<tau>.lifting"} deletes set-up of the Lifting

  1699     package

  1700     for @{text \<tau>} and deletes all the transfer rules that were introduced

  1701     by @{command (HOL) "lift_definition"} using @{text \<tau>} as an abstract type.

  1702

  1703     The stored set-up in a bundle can be reintroduced by the Isar commands for including a bundle

  1704     (@{command "include"}, @{keyword "includes"} and @{command "including"}).

  1705

  1706   \item @{command (HOL) "print_quot_maps"} prints stored quotient map

  1707     theorems.

  1708

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

  1710     theorems.

  1711

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

  1713     theorem, a theorem showing how to "lift" quotients over type constructors.

  1714     E.g., @{term "Quotient R Abs Rep T \<Longrightarrow>

  1715     Quotient (rel_set R) (image Abs) (image Rep) (rel_set T)"}.

  1716     For examples see @{file

  1717     "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.

  1718     This property is proved automatically if the involved type is BNF without dead variables.

  1719

  1720   \item @{attribute (HOL) relator_eq_onp} registers a theorem that

  1721     shows that a relator applied to an equality restricted by a predicate @{term P} (i.e., @{term

  1722     "eq_onp P"}) is equal

  1723     to a predicator applied to the @{term P}. The combinator @{const eq_onp} is used for

  1724     internal encoding of proper subtypes. Such theorems allows the package to hide @{text

  1725     eq_onp} from a user in a user-readable form of a

  1726     respectfulness theorem. For examples see @{file

  1727     "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.

  1728     This property is proved automatically if the involved type is BNF without dead variables.

  1729

  1730   \item @{attribute (HOL) "relator_mono"} registers a property describing a monotonicity of a relator.

  1731     E.g., @{term "A \<le> B \<Longrightarrow> rel_set A \<le> rel_set B"}.

  1732     This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}

  1733     when a parametricity theorem for the raw term is specified and also for the reflexivity prover.

  1734     For examples see @{file

  1735     "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.

  1736     This property is proved automatically if the involved type is BNF without dead variables.

  1737

  1738   \item @{attribute (HOL) "relator_distr"} registers a property describing a distributivity

  1739     of the relation composition and a relator. E.g.,

  1740     @{text "rel_set R \<circ>\<circ> rel_set S = rel_set (R \<circ>\<circ> S)"}.

  1741     This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}

  1742     when a parametricity theorem for the raw term is specified.

  1743     When this equality does not hold unconditionally (e.g., for the function type), the user can specified

  1744     each direction separately and also register multiple theorems with different set of assumptions.

  1745     This attribute can be used only after the monotonicity property was already registered by

  1746     @{attribute (HOL) "relator_mono"}. For examples see @{file

  1747     "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.

  1748     This property is proved automatically if the involved type is BNF without dead variables.

  1749

  1750   \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem

  1751     from the Lifting infrastructure and thus de-register the corresponding quotient.

  1752     This effectively causes that @{command (HOL) lift_definition}  will not

  1753     do any lifting for the corresponding type. This attribute is rather used for low-level

  1754     manipulation with set-up of the Lifting package because @{command (HOL) lifting_forget} is

  1755     preferred for normal usage.

  1756

  1757   \item @{attribute (HOL) lifting_restore} @{text "Quotient_thm pcr_def pcr_cr_eq_thm"}

  1758     registers the Quotient theorem @{text Quotient_thm} in the Lifting infrastructure

  1759     and thus sets up lifting for an abstract type @{text \<tau>} (that is defined by @{text Quotient_thm}).

  1760     Optional theorems @{text pcr_def} and @{text pcr_cr_eq_thm} can be specified to register

  1761     the parametrized

  1762     correspondence relation for @{text \<tau>}. E.g., for @{text "'a dlist"}, @{text pcr_def} is

  1763     @{text "pcr_dlist A \<equiv> list_all2 A \<circ>\<circ> cr_dlist"} and @{text pcr_cr_eq_thm} is

  1764     @{text "pcr_dlist op= = op="}.

  1765     This attribute is rather used for low-level

  1766     manipulation with set-up of the Lifting package because using of the bundle @{text \<tau>.lifting}

  1767     together with the commands @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} is

  1768     preferred for normal usage.

  1769

  1770   \item Integration with the BNF package @{cite "isabelle-datatypes"}:

  1771     As already mentioned, the theorems that are registered

  1772     by the following attributes are proved and registered automatically if the involved type

  1773     is BNF without dead variables: @{attribute (HOL) quot_map}, @{attribute (HOL) relator_eq_onp},

  1774     @{attribute (HOL) "relator_mono"}, @{attribute (HOL) "relator_distr"}. Also the definition of a

  1775     relator and predicator is provided automatically. Moreover, if the BNF represents a datatype,

  1776     simplification rules for a predicator are again proved automatically.

  1777

  1778   \end{description}

  1779 \<close>

  1780

  1781

  1782 section \<open>Coercive subtyping\<close>

  1783

  1784 text \<open>

  1785   \begin{matharray}{rcl}

  1786     @{attribute_def (HOL) coercion} & : & @{text attribute} \\

  1787     @{attribute_def (HOL) coercion_enabled} & : & @{text attribute} \\

  1788     @{attribute_def (HOL) coercion_map} & : & @{text attribute} \\

  1789   \end{matharray}

  1790

  1791   Coercive subtyping allows the user to omit explicit type

  1792   conversions, also called \emph{coercions}.  Type inference will add

  1793   them as necessary when parsing a term. See

  1794   @{cite "traytel-berghofer-nipkow-2011"} for details.

  1795

  1796   @{rail \<open>

  1797     @@{attribute (HOL) coercion} (@{syntax term})?

  1798     ;

  1799     @@{attribute (HOL) coercion_map} (@{syntax term})?

  1800   \<close>}

  1801

  1802   \begin{description}

  1803

  1804   \item @{attribute (HOL) "coercion"}~@{text "f"} registers a new

  1805   coercion function @{text "f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2"} where @{text "\<sigma>\<^sub>1"} and

  1806   @{text "\<sigma>\<^sub>2"} are type constructors without arguments.  Coercions are

  1807   composed by the inference algorithm if needed.  Note that the type

  1808   inference algorithm is complete only if the registered coercions

  1809   form a lattice.

  1810

  1811   \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a

  1812   new map function to lift coercions through type constructors. The

  1813   function @{text "map"} must conform to the following type pattern

  1814

  1815   \begin{matharray}{lll}

  1816     @{text "map"} & @{text "::"} &

  1817       @{text "f\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> f\<^sub>n \<Rightarrow> (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Rightarrow> (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t"} \\

  1818   \end{matharray}

  1819

  1820   where @{text "t"} is a type constructor and @{text "f\<^sub>i"} is of type

  1821   @{text "\<alpha>\<^sub>i \<Rightarrow> \<beta>\<^sub>i"} or @{text "\<beta>\<^sub>i \<Rightarrow> \<alpha>\<^sub>i"}.  Registering a map function

  1822   overwrites any existing map function for this particular type

  1823   constructor.

  1824

  1825   \item @{attribute (HOL) "coercion_enabled"} enables the coercion

  1826   inference algorithm.

  1827

  1828   \end{description}

  1829 \<close>

  1830

  1831

  1832 section \<open>Arithmetic proof support\<close>

  1833

  1834 text \<open>

  1835   \begin{matharray}{rcl}

  1836     @{method_def (HOL) arith} & : & @{text method} \\

  1837     @{attribute_def (HOL) arith} & : & @{text attribute} \\

  1838     @{attribute_def (HOL) arith_split} & : & @{text attribute} \\

  1839   \end{matharray}

  1840

  1841   \begin{description}

  1842

  1843   \item @{method (HOL) arith} decides linear arithmetic problems (on

  1844   types @{text nat}, @{text int}, @{text real}).  Any current facts

  1845   are inserted into the goal before running the procedure.

  1846

  1847   \item @{attribute (HOL) arith} declares facts that are supplied to

  1848   the arithmetic provers implicitly.

  1849

  1850   \item @{attribute (HOL) arith_split} attribute declares case split

  1851   rules to be expanded before @{method (HOL) arith} is invoked.

  1852

  1853   \end{description}

  1854

  1855   Note that a simpler (but faster) arithmetic prover is already

  1856   invoked by the Simplifier.

  1857 \<close>

  1858

  1859

  1860 section \<open>Intuitionistic proof search\<close>

  1861

  1862 text \<open>

  1863   \begin{matharray}{rcl}

  1864     @{method_def (HOL) iprover} & : & @{text method} \\

  1865   \end{matharray}

  1866

  1867   @{rail \<open>

  1868     @@{method (HOL) iprover} (@{syntax rulemod} *)

  1869   \<close>}

  1870

  1871   \begin{description}

  1872

  1873   \item @{method (HOL) iprover} performs intuitionistic proof search,

  1874   depending on specifically declared rules from the context, or given

  1875   as explicit arguments.  Chained facts are inserted into the goal

  1876   before commencing proof search.

  1877

  1878   Rules need to be classified as @{attribute (Pure) intro},

  1879   @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the

  1880   @{text "!"}'' indicator refers to safe'' rules, which may be

  1881   applied aggressively (without considering back-tracking later).

  1882   Rules declared with @{text "?"}'' are ignored in proof search (the

  1883   single-step @{method (Pure) rule} method still observes these).  An

  1884   explicit weight annotation may be given as well; otherwise the

  1885   number of rule premises will be taken into account here.

  1886

  1887   \end{description}

  1888 \<close>

  1889

  1890

  1891 section \<open>Model Elimination and Resolution\<close>

  1892

  1893 text \<open>

  1894   \begin{matharray}{rcl}

  1895     @{method_def (HOL) "meson"} & : & @{text method} \\

  1896     @{method_def (HOL) "metis"} & : & @{text method} \\

  1897   \end{matharray}

  1898

  1899   @{rail \<open>

  1900     @@{method (HOL) meson} @{syntax thmrefs}?

  1901     ;

  1902     @@{method (HOL) metis}

  1903       ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?

  1904       @{syntax thmrefs}?

  1905   \<close>}

  1906

  1907   \begin{description}

  1908

  1909   \item @{method (HOL) meson} implements Loveland's model elimination

  1910   procedure @{cite "loveland-78"}.  See @{file

  1911   "~~/src/HOL/ex/Meson_Test.thy"} for examples.

  1912

  1913   \item @{method (HOL) metis} combines ordered resolution and ordered

  1914   paramodulation to find first-order (or mildly higher-order) proofs.

  1915   The first optional argument specifies a type encoding; see the

  1916   Sledgehammer manual @{cite "isabelle-sledgehammer"} for details.  The

  1917   directory @{file "~~/src/HOL/Metis_Examples"} contains several small

  1918   theories developed to a large extent using @{method (HOL) metis}.

  1919

  1920   \end{description}

  1921 \<close>

  1922

  1923

  1924 section \<open>Algebraic reasoning via Gr\"obner bases\<close>

  1925

  1926 text \<open>

  1927   \begin{matharray}{rcl}

  1928     @{method_def (HOL) "algebra"} & : & @{text method} \\

  1929     @{attribute_def (HOL) algebra} & : & @{text attribute} \\

  1930   \end{matharray}

  1931

  1932   @{rail \<open>

  1933     @@{method (HOL) algebra}

  1934       ('add' ':' @{syntax thmrefs})?

  1935       ('del' ':' @{syntax thmrefs})?

  1936     ;

  1937     @@{attribute (HOL) algebra} (() | 'add' | 'del')

  1938   \<close>}

  1939

  1940   \begin{description}

  1941

  1942   \item @{method (HOL) algebra} performs algebraic reasoning via

  1943   Gr\"obner bases, see also @{cite "Chaieb-Wenzel:2007"} and

  1944   @{cite \<open>\S3.2\<close> "Chaieb-thesis"}. The method handles deals with two main

  1945   classes of problems:

  1946

  1947   \begin{enumerate}

  1948

  1949   \item Universal problems over multivariate polynomials in a

  1950   (semi)-ring/field/idom; the capabilities of the method are augmented

  1951   according to properties of these structures. For this problem class

  1952   the method is only complete for algebraically closed fields, since

  1953   the underlying method is based on Hilbert's Nullstellensatz, where

  1954   the equivalence only holds for algebraically closed fields.

  1955

  1956   The problems can contain equations @{text "p = 0"} or inequations

  1957   @{text "q \<noteq> 0"} anywhere within a universal problem statement.

  1958

  1959   \item All-exists problems of the following restricted (but useful)

  1960   form:

  1961

  1962   @{text [display] "\<forall>x\<^sub>1 \<dots> x\<^sub>n.

  1963     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>

  1964     (\<exists>y\<^sub>1 \<dots> y\<^sub>k.

  1965       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>

  1966       \<dots> \<and>

  1967       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)"}

  1968

  1969   Here @{text "e\<^sub>1, \<dots>, e\<^sub>n"} and the @{text "p\<^sub>i\<^sub>j"} are multivariate

  1970   polynomials only in the variables mentioned as arguments.

  1971

  1972   \end{enumerate}

  1973

  1974   The proof method is preceded by a simplification step, which may be

  1975   modified by using the form @{text "(algebra add: ths\<^sub>1 del: ths\<^sub>2)"}.

  1976   This acts like declarations for the Simplifier

  1977   (\secref{sec:simplifier}) on a private simpset for this tool.

  1978

  1979   \item @{attribute algebra} (as attribute) manages the default

  1980   collection of pre-simplification rules of the above proof method.

  1981

  1982   \end{description}

  1983 \<close>

  1984

  1985

  1986 subsubsection \<open>Example\<close>

  1987

  1988 text \<open>The subsequent example is from geometry: collinearity is

  1989   invariant by rotation.\<close>

  1990

  1991 type_synonym point = "int \<times> int"

  1992

  1993 fun collinear :: "point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where

  1994   "collinear (Ax, Ay) (Bx, By) (Cx, Cy) \<longleftrightarrow>

  1995     (Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx)"

  1996

  1997 lemma collinear_inv_rotation:

  1998   assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"

  1999   shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)

  2000     (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"

  2001   using assms by (algebra add: collinear.simps)

  2002

  2003 text \<open>

  2004  See also @{file "~~/src/HOL/ex/Groebner_Examples.thy"}.

  2005 \<close>

  2006

  2007

  2008 section \<open>Coherent Logic\<close>

  2009

  2010 text \<open>

  2011   \begin{matharray}{rcl}

  2012     @{method_def (HOL) "coherent"} & : & @{text method} \\

  2013   \end{matharray}

  2014

  2015   @{rail \<open>

  2016     @@{method (HOL) coherent} @{syntax thmrefs}?

  2017   \<close>}

  2018

  2019   \begin{description}

  2020

  2021   \item @{method (HOL) coherent} solves problems of \emph{Coherent

  2022   Logic} @{cite "Bezem-Coquand:2005"}, which covers applications in

  2023   confluence theory, lattice theory and projective geometry.  See

  2024   @{file "~~/src/HOL/ex/Coherent.thy"} for some examples.

  2025

  2026   \end{description}

  2027 \<close>

  2028

  2029

  2030 section \<open>Proving propositions\<close>

  2031

  2032 text \<open>

  2033   In addition to the standard proof methods, a number of diagnosis

  2034   tools search for proofs and provide an Isar proof snippet on success.

  2035   These tools are available via the following commands.

  2036

  2037   \begin{matharray}{rcl}

  2038     @{command_def (HOL) "solve_direct"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

  2039     @{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

  2040     @{command_def (HOL) "try0"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

  2041     @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

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

  2043   \end{matharray}

  2044

  2045   @{rail \<open>

  2046     @@{command (HOL) try}

  2047     ;

  2048

  2049     @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?

  2050       @{syntax nat}?

  2051     ;

  2052

  2053     @@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?

  2054     ;

  2055

  2056     @@{command (HOL) sledgehammer_params} ( ( '[' args ']' ) ? )

  2057     ;

  2058     args: ( @{syntax name} '=' value + ',' )

  2059     ;

  2060     facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'

  2061   \<close>} % FIXME check args "value"

  2062

  2063   \begin{description}

  2064

  2065   \item @{command (HOL) "solve_direct"} checks whether the current

  2066   subgoals can be solved directly by an existing theorem. Duplicate

  2067   lemmas can be detected in this way.

  2068

  2069   \item @{command (HOL) "try0"} attempts to prove a subgoal

  2070   using a combination of standard proof methods (@{method auto},

  2071   @{method simp}, @{method blast}, etc.).  Additional facts supplied

  2072   via @{text "simp:"}, @{text "intro:"}, @{text "elim:"}, and @{text

  2073   "dest:"} are passed to the appropriate proof methods.

  2074

  2075   \item @{command (HOL) "try"} attempts to prove or disprove a subgoal

  2076   using a combination of provers and disprovers (@{command (HOL)

  2077   "solve_direct"}, @{command (HOL) "quickcheck"}, @{command (HOL)

  2078   "try0"}, @{command (HOL) "sledgehammer"}, @{command (HOL)

  2079   "nitpick"}).

  2080

  2081   \item @{command (HOL) "sledgehammer"} attempts to prove a subgoal

  2082   using external automatic provers (resolution provers and SMT

  2083   solvers). See the Sledgehammer manual @{cite "isabelle-sledgehammer"}

  2084   for details.

  2085

  2086   \item @{command (HOL) "sledgehammer_params"} changes @{command (HOL)

  2087   "sledgehammer"} configuration options persistently.

  2088

  2089   \end{description}

  2090 \<close>

  2091

  2092

  2093 section \<open>Checking and refuting propositions\<close>

  2094

  2095 text \<open>

  2096   Identifying incorrect propositions usually involves evaluation of

  2097   particular assignments and systematic counterexample search.  This

  2098   is supported by the following commands.

  2099

  2100   \begin{matharray}{rcl}

  2101     @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  2102     @{command_def (HOL) "values"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  2103     @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

  2104     @{command_def (HOL) "nitpick"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

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

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

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

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

  2109   \end{matharray}

  2110

  2111   @{rail \<open>

  2112     @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}

  2113     ;

  2114

  2115     @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}

  2116     ;

  2117

  2118     (@@{command (HOL) quickcheck} | @@{command (HOL) nitpick})

  2119       ( '[' args ']' )? @{syntax nat}?

  2120     ;

  2121

  2122     (@@{command (HOL) quickcheck_params} |

  2123       @@{command (HOL) nitpick_params}) ( '[' args ']' )?

  2124     ;

  2125

  2126     @@{command (HOL) quickcheck_generator} @{syntax nameref} \<newline>

  2127       'operations:' ( @{syntax term} +)

  2128     ;

  2129

  2130     @@{command (HOL) find_unused_assms} @{syntax name}?

  2131     ;

  2132     modes: '(' (@{syntax name} +) ')'

  2133     ;

  2134     args: ( @{syntax name} '=' value + ',' )

  2135   \<close>} % FIXME check "value"

  2136

  2137   \begin{description}

  2138

  2139   \item @{command (HOL) "value"}~@{text t} evaluates and prints a

  2140   term; optionally @{text modes} can be specified, which are appended

  2141   to the current print mode; see \secref{sec:print-modes}.

  2142   Evaluation is tried first using ML, falling

  2143   back to normalization by evaluation if this fails.

  2144   Alternatively a specific evaluator can be selected using square

  2145   brackets; typical evaluators use the current set of code equations

  2146   to normalize and include @{text simp} for fully symbolic evaluation

  2147   using the simplifier, @{text nbe} for \emph{normalization by

  2148   evaluation} and \emph{code} for code generation in SML.

  2149

  2150   \item @{command (HOL) "values"}~@{text t} enumerates a set

  2151   comprehension by evaluation and prints its values up to the given

  2152   number of solutions; optionally @{text modes} can be specified,

  2153   which are appended to the current print mode; see

  2154   \secref{sec:print-modes}.

  2155

  2156   \item @{command (HOL) "quickcheck"} tests the current goal for

  2157   counterexamples using a series of assignments for its free

  2158   variables; by default the first subgoal is tested, an other can be

  2159   selected explicitly using an optional goal index.  Assignments can

  2160   be chosen exhausting the search space up to a given size, or using a

  2161   fixed number of random assignments in the search space, or exploring

  2162   the search space symbolically using narrowing.  By default,

  2163   quickcheck uses exhaustive testing.  A number of configuration

  2164   options are supported for @{command (HOL) "quickcheck"}, notably:

  2165

  2166     \begin{description}

  2167

  2168     \item[@{text tester}] specifies which testing approach to apply.

  2169     There are three testers, @{text exhaustive}, @{text random}, and

  2170     @{text narrowing}.  An unknown configuration option is treated as

  2171     an argument to tester, making @{text "tester ="} optional.  When

  2172     multiple testers are given, these are applied in parallel.  If no

  2173     tester is specified, quickcheck uses the testers that are set

  2174     active, i.e., configurations @{attribute

  2175     quickcheck_exhaustive_active}, @{attribute

  2176     quickcheck_random_active}, @{attribute

  2177     quickcheck_narrowing_active} are set to true.

  2178

  2179     \item[@{text size}] specifies the maximum size of the search space

  2180     for assignment values.

  2181

  2182     \item[@{text genuine_only}] sets quickcheck only to return genuine

  2183     counterexample, but not potentially spurious counterexamples due

  2184     to underspecified functions.

  2185

  2186     \item[@{text abort_potential}] sets quickcheck to abort once it

  2187     found a potentially spurious counterexample and to not continue

  2188     to search for a further genuine counterexample.

  2189     For this option to be effective, the @{text genuine_only} option

  2190     must be set to false.

  2191

  2192     \item[@{text eval}] takes a term or a list of terms and evaluates

  2193     these terms under the variable assignment found by quickcheck.

  2194     This option is currently only supported by the default

  2195     (exhaustive) tester.

  2196

  2197     \item[@{text iterations}] sets how many sets of assignments are

  2198     generated for each particular size.

  2199

  2200     \item[@{text no_assms}] specifies whether assumptions in

  2201     structured proofs should be ignored.

  2202

  2203     \item[@{text locale}] specifies how to process conjectures in

  2204     a locale context, i.e., they can be interpreted or expanded.

  2205     The option is a whitespace-separated list of the two words

  2206     @{text interpret} and @{text expand}. The list determines the

  2207     order they are employed. The default setting is to first use

  2208     interpretations and then test the expanded conjecture.

  2209     The option is only provided as attribute declaration, but not

  2210     as parameter to the command.

  2211

  2212     \item[@{text timeout}] sets the time limit in seconds.

  2213

  2214     \item[@{text default_type}] sets the type(s) generally used to

  2215     instantiate type variables.

  2216

  2217     \item[@{text report}] if set quickcheck reports how many tests

  2218     fulfilled the preconditions.

  2219

  2220     \item[@{text use_subtype}] if set quickcheck automatically lifts

  2221     conjectures to registered subtypes if possible, and tests the

  2222     lifted conjecture.

  2223

  2224     \item[@{text quiet}] if set quickcheck does not output anything

  2225     while testing.

  2226

  2227     \item[@{text verbose}] if set quickcheck informs about the current

  2228     size and cardinality while testing.

  2229

  2230     \item[@{text expect}] can be used to check if the user's

  2231     expectation was met (@{text no_expectation}, @{text

  2232     no_counterexample}, or @{text counterexample}).

  2233

  2234     \end{description}

  2235

  2236   These option can be given within square brackets.

  2237

  2238   Using the following type classes, the testers generate values and convert

  2239   them back into Isabelle terms for displaying counterexamples.

  2240     \begin{description}

  2241     \item[@{text exhaustive}] The parameters of the type classes @{class exhaustive}

  2242       and @{class full_exhaustive} implement the testing. They take a

  2243       testing function as a parameter, which takes a value of type @{typ "'a"}

  2244       and optionally produces a counterexample, and a size parameter for the test values.

  2245       In @{class full_exhaustive}, the testing function parameter additionally

  2246       expects a lazy term reconstruction in the type @{typ Code_Evaluation.term}

  2247       of the tested value.

  2248

  2249       The canonical implementation for @{text exhaustive} testers calls the given

  2250       testing function on all values up to the given size and stops as soon

  2251       as a counterexample is found.

  2252

  2253     \item[@{text random}] The operation @{const Quickcheck_Random.random}

  2254       of the type class @{class random} generates a pseudo-random

  2255       value of the given size and a lazy term reconstruction of the value

  2256       in the type @{typ Code_Evaluation.term}. A pseudo-randomness generator

  2257       is defined in theory @{theory Random}.

  2258

  2259     \item[@{text narrowing}] implements Haskell's Lazy Smallcheck @{cite "runciman-naylor-lindblad"}

  2260       using the type classes @{class narrowing} and @{class partial_term_of}.

  2261       Variables in the current goal are initially represented as symbolic variables.

  2262       If the execution of the goal tries to evaluate one of them, the test engine

  2263       replaces it with refinements provided by @{const narrowing}.

  2264       Narrowing views every value as a sum-of-products which is expressed using the operations

  2265       @{const Quickcheck_Narrowing.cons} (embedding a value),

  2266       @{const Quickcheck_Narrowing.apply} (product) and @{const Quickcheck_Narrowing.sum} (sum).

  2267       The refinement should enable further evaluation of the goal.

  2268

  2269       For example, @{const narrowing} for the list type @{typ "'a :: narrowing list"}

  2270       can be recursively defined as

  2271       @{term "Quickcheck_Narrowing.sum (Quickcheck_Narrowing.cons [])

  2272                 (Quickcheck_Narrowing.apply

  2273                   (Quickcheck_Narrowing.apply

  2274                     (Quickcheck_Narrowing.cons (op #))

  2275                     narrowing)

  2276                   narrowing)"}.

  2277       If a symbolic variable of type @{typ "_ list"} is evaluated, it is replaced by (i)~the empty

  2278       list @{term "[]"} and (ii)~by a non-empty list whose head and tail can then be recursively

  2279       refined if needed.

  2280

  2281       To reconstruct counterexamples, the operation @{const partial_term_of} transforms

  2282       @{text narrowing}'s deep representation of terms to the type @{typ Code_Evaluation.term}.

  2283       The deep representation models symbolic variables as

  2284       @{const Quickcheck_Narrowing.Narrowing_variable}, which are normally converted to

  2285       @{const Code_Evaluation.Free}, and refined values as

  2286       @{term "Quickcheck_Narrowing.Narrowing_constructor i args"}, where @{term "i :: integer"}

  2287       denotes the index in the sum of refinements. In the above example for lists,

  2288       @{term "0"} corresponds to @{term "[]"} and @{term "1"}

  2289       to @{term "op #"}.

  2290

  2291       The command @{command (HOL) "code_datatype"} sets up @{const partial_term_of}

  2292       such that the @{term "i"}-th refinement is interpreted as the @{term "i"}-th constructor,

  2293       but it does not ensures consistency with @{const narrowing}.

  2294     \end{description}

  2295

  2296   \item @{command (HOL) "quickcheck_params"} changes @{command (HOL)

  2297   "quickcheck"} configuration options persistently.

  2298

  2299   \item @{command (HOL) "quickcheck_generator"} creates random and

  2300   exhaustive value generators for a given type and operations.  It

  2301   generates values by using the operations as if they were

  2302   constructors of that type.

  2303

  2304   \item @{command (HOL) "nitpick"} tests the current goal for

  2305   counterexamples using a reduction to first-order relational

  2306   logic. See the Nitpick manual @{cite "isabelle-nitpick"} for details.

  2307

  2308   \item @{command (HOL) "nitpick_params"} changes @{command (HOL)

  2309   "nitpick"} configuration options persistently.

  2310

  2311   \item @{command (HOL) "find_unused_assms"} finds potentially superfluous

  2312   assumptions in theorems using quickcheck.

  2313   It takes the theory name to be checked for superfluous assumptions as

  2314   optional argument. If not provided, it checks the current theory.

  2315   Options to the internal quickcheck invocations can be changed with

  2316   common configuration declarations.

  2317

  2318   \end{description}

  2319 \<close>

  2320

  2321

  2322 section \<open>Unstructured case analysis and induction \label{sec:hol-induct-tac}\<close>

  2323

  2324 text \<open>

  2325   The following tools of Isabelle/HOL support cases analysis and

  2326   induction in unstructured tactic scripts; see also

  2327   \secref{sec:cases-induct} for proper Isar versions of similar ideas.

  2328

  2329   \begin{matharray}{rcl}

  2330     @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & @{text method} \\

  2331     @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\

  2332     @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\

  2333     @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

  2334   \end{matharray}

  2335

  2336   @{rail \<open>

  2337     @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?

  2338     ;

  2339     @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?

  2340     ;

  2341     @@{method (HOL) ind_cases} (@{syntax prop}+) (@'for' (@{syntax name}+))?

  2342     ;

  2343     @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')

  2344     ;

  2345     rule: 'rule' ':' @{syntax thmref}

  2346   \<close>}

  2347

  2348   \begin{description}

  2349

  2350   \item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit

  2351   to reason about inductive types.  Rules are selected according to

  2352   the declarations by the @{attribute cases} and @{attribute induct}

  2353   attributes, cf.\ \secref{sec:cases-induct}.  The @{command (HOL)

  2354   datatype} package already takes care of this.

  2355

  2356   These unstructured tactics feature both goal addressing and dynamic

  2357   instantiation.  Note that named rule cases are \emph{not} provided

  2358   as would be by the proper @{method cases} and @{method induct} proof

  2359   methods (see \secref{sec:cases-induct}).  Unlike the @{method

  2360   induct} method, @{method induct_tac} does not handle structured rule

  2361   statements, only the compact object-logic conclusion of the subgoal

  2362   being addressed.

  2363

  2364   \item @{method (HOL) ind_cases} and @{command (HOL)

  2365   "inductive_cases"} provide an interface to the internal @{ML_text

  2366   mk_cases} operation.  Rules are simplified in an unrestricted

  2367   forward manner.

  2368

  2369   While @{method (HOL) ind_cases} is a proof method to apply the

  2370   result immediately as elimination rules, @{command (HOL)

  2371   "inductive_cases"} provides case split theorems at the theory level

  2372   for later use.  The @{keyword "for"} argument of the @{method (HOL)

  2373   ind_cases} method allows to specify a list of variables that should

  2374   be generalized before applying the resulting rule.

  2375

  2376   \end{description}

  2377 \<close>

  2378

  2379

  2380 chapter \<open>Executable code\<close>

  2381

  2382 text \<open>For validation purposes, it is often useful to \emph{execute}

  2383   specifications.  In principle, execution could be simulated by

  2384   Isabelle's inference kernel, i.e. by a combination of resolution and

  2385   simplification.  Unfortunately, this approach is rather inefficient.

  2386   A more efficient way of executing specifications is to translate

  2387   them into a functional programming language such as ML.

  2388

  2389   Isabelle provides a generic framework to support code generation

  2390   from executable specifications.  Isabelle/HOL instantiates these

  2391   mechanisms in a way that is amenable to end-user applications.  Code

  2392   can be generated for functional programs (including overloading

  2393   using type classes) targeting SML @{cite SML}, OCaml @{cite OCaml},

  2394   Haskell @{cite "haskell-revised-report"} and Scala

  2395   @{cite "scala-overview-tech-report"}.  Conceptually, code generation is

  2396   split up in three steps: \emph{selection} of code theorems,

  2397   \emph{translation} into an abstract executable view and

  2398   \emph{serialization} to a specific \emph{target language}.

  2399   Inductive specifications can be executed using the predicate

  2400   compiler which operates within HOL.  See @{cite "isabelle-codegen"} for

  2401   an introduction.

  2402

  2403   \begin{matharray}{rcl}

  2404     @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  2405     @{attribute_def (HOL) code} & : & @{text attribute} \\

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

  2407     @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  2408     @{attribute_def (HOL) code_unfold} & : & @{text attribute} \\

  2409     @{attribute_def (HOL) code_post} & : & @{text attribute} \\

  2410     @{attribute_def (HOL) code_abbrev} & : & @{text attribute} \\

  2411     @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  2412     @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  2413     @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

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

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

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

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

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

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

  2420   \end{matharray}

  2421

  2422   @{rail \<open>

  2423     @@{command (HOL) export_code} ( @'open' ) ? ( constexpr + ) \<newline>

  2424        ( ( @'in' target ( @'module_name' @{syntax string} ) ? \<newline>

  2425         ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?

  2426     ;

  2427

  2428     const: @{syntax term}

  2429     ;

  2430

  2431     constexpr: ( const | 'name._' | '_' )

  2432     ;

  2433

  2434     typeconstructor: @{syntax nameref}

  2435     ;

  2436

  2437     class: @{syntax nameref}

  2438     ;

  2439

  2440     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'

  2441     ;

  2442

  2443     @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract'

  2444       | 'drop:' ( const + ) | 'abort:' ( const + ) )?

  2445     ;

  2446

  2447     @@{command (HOL) code_datatype} ( const + )

  2448     ;

  2449

  2450     @@{attribute (HOL) code_unfold} ( 'del' ) ?

  2451     ;

  2452

  2453     @@{attribute (HOL) code_post} ( 'del' ) ?

  2454     ;

  2455

  2456     @@{attribute (HOL) code_abbrev}

  2457     ;

  2458

  2459     @@{command (HOL) code_thms} ( constexpr + ) ?

  2460     ;

  2461

  2462     @@{command (HOL) code_deps} ( constexpr + ) ?

  2463     ;

  2464

  2465     @@{command (HOL) code_reserved} target ( @{syntax string} + )

  2466     ;

  2467

  2468     symbol_const: ( @'constant' const )

  2469     ;

  2470

  2471     symbol_typeconstructor: ( @'type_constructor' typeconstructor )

  2472     ;

  2473

  2474     symbol_class: ( @'type_class' class )

  2475     ;

  2476

  2477     symbol_class_relation: ( @'class_relation' class ( '<' | '\<subseteq>' ) class )

  2478     ;

  2479

  2480     symbol_class_instance: ( @'class_instance' typeconstructor @'::' class )

  2481     ;

  2482

  2483     symbol_module: ( @'code_module' name )

  2484     ;

  2485

  2486     syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}

  2487     ;

  2488

  2489     printing_const: symbol_const ( '\<rightharpoonup>' | '=>' ) \<newline>

  2490       ( '(' target ')' syntax ? + @'and' )

  2491     ;

  2492

  2493     printing_typeconstructor: symbol_typeconstructor ( '\<rightharpoonup>' | '=>' ) \<newline>

  2494       ( '(' target ')' syntax ? + @'and' )

  2495     ;

  2496

  2497     printing_class: symbol_class ( '\<rightharpoonup>' | '=>' ) \<newline>

  2498       ( '(' target ')' @{syntax string} ? + @'and' )

  2499     ;

  2500

  2501     printing_class_relation: symbol_class_relation ( '\<rightharpoonup>' | '=>' ) \<newline>

  2502       ( '(' target ')' @{syntax string} ? + @'and' )

  2503     ;

  2504

  2505     printing_class_instance: symbol_class_instance ( '\<rightharpoonup>' | '=>' ) \<newline>

  2506       ( '(' target ')' '-' ? + @'and' )

  2507     ;

  2508

  2509     printing_module: symbol_module ( '\<rightharpoonup>' | '=>' ) \<newline>

  2510       ( '(' target ')' ( @{syntax string} ( @'attach' ( const + ) ) ? ) ? + @'and' )

  2511     ;

  2512

  2513     @@{command (HOL) code_printing} ( ( printing_const | printing_typeconstructor

  2514       | printing_class | printing_class_relation | printing_class_instance

  2515       | printing_module ) + '|' )

  2516     ;

  2517

  2518     @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor

  2519       | symbol_class | symbol_class_relation | symbol_class_instance

  2520       | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \<newline>

  2521       ( '(' target ')' @{syntax string} ? + @'and' ) + '|' )

  2522     ;

  2523

  2524     @@{command (HOL) code_monad} const const target

  2525     ;

  2526

  2527     @@{command (HOL) code_reflect} @{syntax string} \<newline>

  2528       ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \<newline>

  2529       ( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?

  2530     ;

  2531

  2532     @@{command (HOL) code_pred} \<newline> ('(' @'modes' ':' modedecl ')')? \<newline> const

  2533     ;

  2534

  2535     modedecl: (modes | ((const ':' modes) \<newline>

  2536         (@'and' ((const ':' modes @'and') +))?))

  2537     ;

  2538

  2539     modes: mode @'as' const

  2540   \<close>}

  2541

  2542   \begin{description}

  2543

  2544   \item @{command (HOL) "export_code"} generates code for a given list

  2545   of constants in the specified target language(s).  If no

  2546   serialization instruction is given, only abstract code is generated

  2547   internally.

  2548

  2549   Constants may be specified by giving them literally, referring to

  2550   all executable constants within a certain theory by giving @{text

  2551   "name._"}, or referring to \emph{all} executable constants currently

  2552   available by giving @{text "_"}.

  2553

  2554   By default, exported identifiers are minimized per module.  This

  2555   can be suppressed by prepending @{keyword "open"} before the list

  2556   of contants.

  2557

  2558   By default, for each involved theory one corresponding name space

  2559   module is generated.  Alternatively, a module name may be specified

  2560   after the @{keyword "module_name"} keyword; then \emph{all} code is

  2561   placed in this module.

  2562

  2563   For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification

  2564   refers to a single file; for \emph{Haskell}, it refers to a whole

  2565   directory, where code is generated in multiple files reflecting the

  2566   module hierarchy.  Omitting the file specification denotes standard

  2567   output.

  2568

  2569   Serializers take an optional list of arguments in parentheses.

  2570   For \emph{Haskell} a module name prefix may be given using the

  2571   @{text "root:"}'' argument; @{text string_classes}'' adds a

  2572   @{verbatim "deriving (Read, Show)"}'' clause to each appropriate

  2573   datatype declaration.

  2574

  2575   \item @{attribute (HOL) code} declare code equations for code

  2576   generation.  Variant @{text "code equation"} declares a conventional

  2577   equation as code equation.  Variants @{text "code abstype"} and

  2578   @{text "code abstract"} declare abstract datatype certificates or

  2579   code equations on abstract datatype representations respectively.

  2580   Vanilla @{text "code"} falls back to @{text "code equation"}

  2581   or @{text "code abstype"} depending on the syntactic shape

  2582   of the underlying equation.  Variant @{text "code del"}

  2583   deselects a code equation for code generation.

  2584

  2585   Variants @{text "code drop:"} and @{text "code abort:"} take

  2586   a list of constant as arguments and drop all code equations declared

  2587   for them.  In the case of {text abort}, these constants then are

  2588   are not required to have a definition by means of code equations;

  2589   if needed these are implemented by program abort (exception) instead.

  2590

  2591   Usually packages introducing code equations provide a reasonable

  2592   default setup for selection.

  2593

  2594   \item @{command (HOL) "code_datatype"} specifies a constructor set

  2595   for a logical type.

  2596

  2597   \item @{command (HOL) "print_codesetup"} gives an overview on

  2598   selected code equations and code generator datatypes.

  2599

  2600   \item @{attribute (HOL) code_unfold} declares (or with option

  2601   @{text "del"}'' removes) theorems which during preprocessing

  2602   are applied as rewrite rules to any code equation or evaluation

  2603   input.

  2604

  2605   \item @{attribute (HOL) code_post} declares (or with option @{text

  2606   "del"}'' removes) theorems which are applied as rewrite rules to any

  2607   result of an evaluation.

  2608

  2609   \item @{attribute (HOL) code_abbrev} declares (or with option @{text

  2610   "del"}'' removes) equations which are

  2611   applied as rewrite rules to any result of an evaluation and

  2612   symmetrically during preprocessing to any code equation or evaluation

  2613   input.

  2614

  2615   \item @{command (HOL) "print_codeproc"} prints the setup of the code

  2616   generator preprocessor.

  2617

  2618   \item @{command (HOL) "code_thms"} prints a list of theorems

  2619   representing the corresponding program containing all given

  2620   constants after preprocessing.

  2621

  2622   \item @{command (HOL) "code_deps"} visualizes dependencies of

  2623   theorems representing the corresponding program containing all given

  2624   constants after preprocessing.

  2625

  2626   \item @{command (HOL) "code_reserved"} declares a list of names as

  2627   reserved for a given target, preventing it to be shadowed by any

  2628   generated code.

  2629

  2630   \item @{command (HOL) "code_printing"} associates a series of symbols

  2631   (constants, type constructors, classes, class relations, instances,

  2632   module names) with target-specific serializations; omitting a serialization

  2633   deletes an existing serialization.

  2634

  2635   \item @{command (HOL) "code_monad"} provides an auxiliary mechanism

  2636   to generate monadic code for Haskell.

  2637

  2638   \item @{command (HOL) "code_identifier"} associates a a series of symbols

  2639   (constants, type constructors, classes, class relations, instances,

  2640   module names) with target-specific hints how these symbols shall be named.

  2641   These hints gain precedence over names for symbols with no hints at all.

  2642   Conflicting hints are subject to name disambiguation.

  2643   \emph{Warning:} It is at the discretion

  2644   of the user to ensure that name prefixes of identifiers in compound

  2645   statements like type classes or datatypes are still the same.

  2646

  2647   \item @{command (HOL) "code_reflect"} without a @{text "file"}''

  2648   argument compiles code into the system runtime environment and

  2649   modifies the code generator setup that future invocations of system

  2650   runtime code generation referring to one of the @{text

  2651   "datatypes"}'' or @{text "functions"}'' entities use these

  2652   precompiled entities.  With a @{text "file"}'' argument, the

  2653   corresponding code is generated into that specified file without

  2654   modifying the code generator setup.

  2655

  2656   \item @{command (HOL) "code_pred"} creates code equations for a

  2657     predicate given a set of introduction rules. Optional mode

  2658     annotations determine which arguments are supposed to be input or

  2659     output. If alternative introduction rules are declared, one must

  2660     prove a corresponding elimination rule.

  2661

  2662   \end{description}

  2663 \<close>

  2664

  2665 end