src/Doc/Isar_Ref/HOL_Specific.thy
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (23 months ago)
changeset 66822 4642cf4a7ebb
parent 66453 cc19f7ca2ed6
child 67207 ad538f6c5d2f
permissions -rw-r--r--
tuned signature;
wenzelm@61656
     1
(*:maxLineLen=78:*)
wenzelm@61656
     2
wenzelm@26840
     3
theory HOL_Specific
wenzelm@63531
     4
  imports
wenzelm@63531
     5
    Main
wenzelm@66453
     6
    "HOL-Library.Old_Datatype"
wenzelm@66453
     7
    "HOL-Library.Old_Recdef"
wenzelm@66453
     8
    "HOL-Library.Adhoc_Overloading"
wenzelm@66453
     9
    "HOL-Library.Dlist"
wenzelm@66453
    10
    "HOL-Library.FSet"
wenzelm@63531
    11
    Base
wenzelm@26840
    12
begin
wenzelm@26840
    13
wenzelm@60654
    14
wenzelm@58618
    15
chapter \<open>Higher-Order Logic\<close>
wenzelm@58618
    16
wenzelm@63531
    17
text \<open>
wenzelm@63531
    18
  Isabelle/HOL is based on Higher-Order Logic, a polymorphic version of
wenzelm@63531
    19
  Church's Simple Theory of Types. HOL can be best understood as a
wenzelm@63531
    20
  simply-typed version of classical set theory. The logic was first
wenzelm@63531
    21
  implemented in Gordon's HOL system @{cite "mgordon-hol"}. It extends
wenzelm@63531
    22
  Church's original logic @{cite "church40"} by explicit type variables (naive
wenzelm@63531
    23
  polymorphism) and a sound axiomatization scheme for new types based on
wenzelm@63531
    24
  subsets of existing types.
wenzelm@63531
    25
wenzelm@63531
    26
  Andrews's book @{cite andrews86} is a full description of the original
wenzelm@63531
    27
  Church-style higher-order logic, with proofs of correctness and completeness
wenzelm@63531
    28
  wrt.\ certain set-theoretic interpretations. The particular extensions of
wenzelm@63531
    29
  Gordon-style HOL are explained semantically in two chapters of the 1993 HOL
wenzelm@63531
    30
  book @{cite pitts93}.
wenzelm@63531
    31
wenzelm@63531
    32
  Experience with HOL over decades has demonstrated that higher-order logic is
wenzelm@63531
    33
  widely applicable in many areas of mathematics and computer science. In a
wenzelm@63531
    34
  sense, Higher-Order Logic is simpler than First-Order Logic, because there
wenzelm@63531
    35
  are fewer restrictions and special cases. Note that HOL is \<^emph>\<open>weaker\<close> than
wenzelm@63531
    36
  FOL with axioms for ZF set theory, which is traditionally considered the
wenzelm@63531
    37
  standard foundation of regular mathematics, but for most applications this
wenzelm@63531
    38
  does not matter. If you prefer ML to Lisp, you will probably prefer HOL to
wenzelm@63531
    39
  ZF.
wenzelm@63531
    40
wenzelm@63531
    41
  \<^medskip> The syntax of HOL follows \<open>\<lambda>\<close>-calculus and functional programming.
wenzelm@63531
    42
  Function application is curried. To apply the function \<open>f\<close> of type \<open>\<tau>\<^sub>1 \<Rightarrow>
wenzelm@63531
    43
  \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3\<close> to the arguments \<open>a\<close> and \<open>b\<close> in HOL, you simply write \<open>f a b\<close> (as
wenzelm@63531
    44
  in ML or Haskell). There is no ``apply'' operator; the existing application
wenzelm@63531
    45
  of the Pure \<open>\<lambda>\<close>-calculus is re-used. Note that in HOL \<open>f (a, b)\<close> means ``\<open>f\<close>
wenzelm@63531
    46
  applied to the pair \<open>(a, b)\<close> (which is notation for \<open>Pair a b\<close>). The latter
wenzelm@63531
    47
  typically introduces extra formal efforts that can be avoided by currying
wenzelm@63531
    48
  functions by default. Explicit tuples are as infrequent in HOL
wenzelm@63531
    49
  formalizations as in good ML or Haskell programs.
wenzelm@63531
    50
wenzelm@63531
    51
  \<^medskip> Isabelle/HOL has a distinct feel, compared to other object-logics like
wenzelm@63531
    52
  Isabelle/ZF. It identifies object-level types with meta-level types, taking
wenzelm@63531
    53
  advantage of the default type-inference mechanism of Isabelle/Pure. HOL
wenzelm@63531
    54
  fully identifies object-level functions with meta-level functions, with
wenzelm@63531
    55
  native abstraction and application.
wenzelm@63531
    56
wenzelm@63531
    57
  These identifications allow Isabelle to support HOL particularly nicely, but
wenzelm@63531
    58
  they also mean that HOL requires some sophistication from the user. In
wenzelm@63531
    59
  particular, an understanding of Hindley-Milner type-inference with
wenzelm@63531
    60
  type-classes, which are both used extensively in the standard libraries and
wenzelm@63531
    61
  applications.
wenzelm@63531
    62
\<close>
wenzelm@58618
    63
wenzelm@58618
    64
wenzelm@58618
    65
chapter \<open>Derived specification elements\<close>
wenzelm@58618
    66
wenzelm@58618
    67
section \<open>Inductive and coinductive definitions \label{sec:hol-inductive}\<close>
wenzelm@58618
    68
wenzelm@58618
    69
text \<open>
wenzelm@46280
    70
  \begin{matharray}{rcl}
wenzelm@61493
    71
    @{command_def (HOL) "inductive"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@61493
    72
    @{command_def (HOL) "inductive_set"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@61493
    73
    @{command_def (HOL) "coinductive"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@61493
    74
    @{command_def (HOL) "coinductive_set"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@61493
    75
    @{command_def "print_inductives"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
    76
    @{attribute_def (HOL) mono} & : & \<open>attribute\<close> \\
wenzelm@46280
    77
  \end{matharray}
wenzelm@46280
    78
wenzelm@63531
    79
  An \<^emph>\<open>inductive definition\<close> specifies the least predicate or set \<open>R\<close> closed
wenzelm@63531
    80
  under given rules: applying a rule to elements of \<open>R\<close> yields a result within
wenzelm@63531
    81
  \<open>R\<close>. For example, a structural operational semantics is an inductive
wenzelm@63531
    82
  definition of an evaluation relation.
wenzelm@63531
    83
wenzelm@63531
    84
  Dually, a \<^emph>\<open>coinductive definition\<close> specifies the greatest predicate or set
wenzelm@63531
    85
  \<open>R\<close> that is consistent with given rules: every element of \<open>R\<close> can be seen as
wenzelm@63531
    86
  arising by applying a rule to elements of \<open>R\<close>. An important example is using
wenzelm@63531
    87
  bisimulation relations to formalise equivalence of processes and infinite
wenzelm@63531
    88
  data structures.
wenzelm@63531
    89
wenzelm@63531
    90
  Both inductive and coinductive definitions are based on the Knaster-Tarski
wenzelm@63531
    91
  fixed-point theorem for complete lattices. The collection of introduction
wenzelm@63531
    92
  rules given by the user determines a functor on subsets of set-theoretic
wenzelm@63531
    93
  relations. The required monotonicity of the recursion scheme is proven as a
wenzelm@63531
    94
  prerequisite to the fixed-point definition and the resulting consequences.
wenzelm@63531
    95
  This works by pushing inclusion through logical connectives and any other
wenzelm@63531
    96
  operator that might be wrapped around recursive occurrences of the defined
wenzelm@63531
    97
  relation: there must be a monotonicity theorem of the form \<open>A \<le> B \<Longrightarrow> \<M> A \<le> \<M>
wenzelm@63531
    98
  B\<close>, for each premise \<open>\<M> R t\<close> in an introduction rule. The default rule
wenzelm@63531
    99
  declarations of Isabelle/HOL already take care of most common situations.
wenzelm@42907
   100
wenzelm@55112
   101
  @{rail \<open>
wenzelm@42908
   102
    (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
wenzelm@59785
   103
      @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
wenzelm@63285
   104
      @{syntax vars} @{syntax for_fixes} \<newline>
wenzelm@63182
   105
      (@'where' @{syntax multi_specs})? (@'monos' @{syntax thms})?
wenzelm@42908
   106
    ;
wenzelm@59917
   107
    @@{command print_inductives} ('!'?)
wenzelm@59917
   108
    ;
wenzelm@42908
   109
    @@{attribute (HOL) mono} (() | 'add' | 'del')
wenzelm@55112
   110
  \<close>}
wenzelm@42908
   111
wenzelm@63531
   112
  \<^descr> @{command (HOL) "inductive"} and @{command (HOL) "coinductive"} define
wenzelm@63531
   113
  (co)inductive predicates from the introduction rules.
wenzelm@63531
   114
wenzelm@63531
   115
  The propositions given as \<open>clauses\<close> in the @{keyword "where"} part are
wenzelm@63531
   116
  either rules of the usual \<open>\<And>/\<Longrightarrow>\<close> format (with arbitrary nesting), or
wenzelm@63531
   117
  equalities using \<open>\<equiv>\<close>. The latter specifies extra-logical abbreviations in
wenzelm@63531
   118
  the sense of @{command_ref abbreviation}. Introducing abstract syntax
wenzelm@63531
   119
  simultaneously with the actual introduction rules is occasionally useful for
wenzelm@63531
   120
  complex specifications.
wenzelm@63531
   121
wenzelm@63531
   122
  The optional @{keyword "for"} part contains a list of parameters of the
wenzelm@63531
   123
  (co)inductive predicates that remain fixed throughout the definition, in
wenzelm@63531
   124
  contrast to arguments of the relation that may vary in each occurrence
wenzelm@63531
   125
  within the given \<open>clauses\<close>.
wenzelm@42913
   126
wenzelm@42913
   127
  The optional @{keyword "monos"} declaration contains additional
wenzelm@63531
   128
  \<^emph>\<open>monotonicity theorems\<close>, which are required for each operator applied to a
wenzelm@63531
   129
  recursive set in the introduction rules.
wenzelm@63531
   130
wenzelm@63531
   131
  \<^descr> @{command (HOL) "inductive_set"} and @{command (HOL) "coinductive_set"}
wenzelm@63531
   132
  are wrappers for to the previous commands for native HOL predicates. This
wenzelm@63531
   133
  allows to define (co)inductive sets, where multiple arguments are simulated
wenzelm@63531
   134
  via tuples.
wenzelm@42908
   135
wenzelm@61439
   136
  \<^descr> @{command "print_inductives"} prints (co)inductive definitions and
wenzelm@61493
   137
  monotonicity rules; the ``\<open>!\<close>'' option indicates extra verbosity.
wenzelm@50302
   138
wenzelm@63531
   139
  \<^descr> @{attribute (HOL) mono} declares monotonicity rules in the context. These
wenzelm@63531
   140
  rule are involved in the automated monotonicity proof of the above inductive
wenzelm@63531
   141
  and coinductive definitions.
wenzelm@58618
   142
\<close>
wenzelm@58618
   143
wenzelm@58618
   144
wenzelm@58618
   145
subsection \<open>Derived rules\<close>
wenzelm@58618
   146
wenzelm@63531
   147
text \<open>
wenzelm@63531
   148
  A (co)inductive definition of \<open>R\<close> provides the following main theorems:
wenzelm@63531
   149
wenzelm@63531
   150
  \<^descr> \<open>R.intros\<close> is the list of introduction rules as proven theorems, for the
wenzelm@63531
   151
  recursive predicates (or sets). The rules are also available individually,
wenzelm@63531
   152
  using the names given them in the theory file;
wenzelm@42908
   153
wenzelm@61493
   154
  \<^descr> \<open>R.cases\<close> is the case analysis (or elimination) rule;
wenzelm@61493
   155
wenzelm@63531
   156
  \<^descr> \<open>R.induct\<close> or \<open>R.coinduct\<close> is the (co)induction rule;
wenzelm@63531
   157
wenzelm@63531
   158
  \<^descr> \<open>R.simps\<close> is the equation unrolling the fixpoint of the predicate one
wenzelm@63531
   159
  step.
wenzelm@63531
   160
wenzelm@63531
   161
wenzelm@63531
   162
  When several predicates \<open>R\<^sub>1, \<dots>, R\<^sub>n\<close> are defined simultaneously, the list
wenzelm@63531
   163
  of introduction rules is called \<open>R\<^sub>1_\<dots>_R\<^sub>n.intros\<close>, the case analysis rules
wenzelm@63531
   164
  are called \<open>R\<^sub>1.cases, \<dots>, R\<^sub>n.cases\<close>, and the list of mutual induction rules
wenzelm@63531
   165
  is called \<open>R\<^sub>1_\<dots>_R\<^sub>n.inducts\<close>.
wenzelm@58618
   166
\<close>
wenzelm@58618
   167
wenzelm@58618
   168
wenzelm@58618
   169
subsection \<open>Monotonicity theorems\<close>
wenzelm@58618
   170
wenzelm@63531
   171
text \<open>
wenzelm@63531
   172
  The context maintains a default set of theorems that are used in
wenzelm@63531
   173
  monotonicity proofs. New rules can be declared via the @{attribute (HOL)
wenzelm@63531
   174
  mono} attribute. See the main Isabelle/HOL sources for some examples. The
wenzelm@63531
   175
  general format of such monotonicity theorems is as follows:
wenzelm@63531
   176
wenzelm@63531
   177
  \<^item> Theorems of the form \<open>A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B\<close>, for proving monotonicity of
wenzelm@63531
   178
  inductive definitions whose introduction rules have premises involving terms
wenzelm@63531
   179
  such as \<open>\<M> R t\<close>.
wenzelm@63531
   180
wenzelm@63531
   181
  \<^item> Monotonicity theorems for logical operators, which are of the general form
wenzelm@63531
   182
  \<open>(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>\<close>. For example, in the case of the operator \<open>\<or>\<close>,
wenzelm@63531
   183
  the corresponding theorem is
wenzelm@42908
   184
  \[
wenzelm@61493
   185
  \infer{\<open>P\<^sub>1 \<or> P\<^sub>2 \<longrightarrow> Q\<^sub>1 \<or> Q\<^sub>2\<close>}{\<open>P\<^sub>1 \<longrightarrow> Q\<^sub>1\<close> & \<open>P\<^sub>2 \<longrightarrow> Q\<^sub>2\<close>}
wenzelm@42908
   186
  \]
wenzelm@42908
   187
wenzelm@63531
   188
  \<^item> De Morgan style equations for reasoning about the ``polarity'' of
wenzelm@63531
   189
  expressions, e.g.
wenzelm@42908
   190
  \[
wenzelm@42908
   191
  @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad
wenzelm@42908
   192
  @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}
wenzelm@42908
   193
  \]
wenzelm@42908
   194
wenzelm@63531
   195
  \<^item> Equations for reducing complex operators to more primitive ones whose
wenzelm@63531
   196
  monotonicity can easily be proved, e.g.
wenzelm@42908
   197
  \[
wenzelm@42908
   198
  @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad
wenzelm@42908
   199
  @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}
wenzelm@42908
   200
  \]
wenzelm@58618
   201
\<close>
wenzelm@58618
   202
wenzelm@63531
   203
wenzelm@58618
   204
subsubsection \<open>Examples\<close>
wenzelm@58618
   205
wenzelm@58618
   206
text \<open>The finite powerset operator can be defined inductively like this:\<close>
wenzelm@42913
   207
wenzelm@59905
   208
(*<*)experiment begin(*>*)
wenzelm@42913
   209
inductive_set Fin :: "'a set \<Rightarrow> 'a set set" for A :: "'a set"
wenzelm@42913
   210
where
wenzelm@42913
   211
  empty: "{} \<in> Fin A"
wenzelm@42913
   212
| insert: "a \<in> A \<Longrightarrow> B \<in> Fin A \<Longrightarrow> insert a B \<in> Fin A"
wenzelm@42913
   213
wenzelm@58618
   214
text \<open>The accessible part of a relation is defined as follows:\<close>
wenzelm@42913
   215
wenzelm@42913
   216
inductive acc :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
wenzelm@42913
   217
  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<prec>" 50)
wenzelm@42913
   218
where acc: "(\<And>y. y \<prec> x \<Longrightarrow> acc r y) \<Longrightarrow> acc r x"
wenzelm@59905
   219
(*<*)end(*>*)
wenzelm@42913
   220
wenzelm@63531
   221
text \<open>
wenzelm@63531
   222
  Common logical connectives can be easily characterized as non-recursive
wenzelm@63531
   223
  inductive definitions with parameters, but without arguments.
wenzelm@63531
   224
\<close>
wenzelm@42913
   225
wenzelm@59905
   226
(*<*)experiment begin(*>*)
wenzelm@42913
   227
inductive AND for A B :: bool
wenzelm@42913
   228
where "A \<Longrightarrow> B \<Longrightarrow> AND A B"
wenzelm@42913
   229
wenzelm@42913
   230
inductive OR for A B :: bool
wenzelm@42913
   231
where "A \<Longrightarrow> OR A B"
wenzelm@42913
   232
  | "B \<Longrightarrow> OR A B"
wenzelm@42913
   233
wenzelm@42913
   234
inductive EXISTS for B :: "'a \<Rightarrow> bool"
wenzelm@42913
   235
where "B a \<Longrightarrow> EXISTS B"
wenzelm@59905
   236
(*<*)end(*>*)
wenzelm@42913
   237
wenzelm@63531
   238
text \<open>
wenzelm@63531
   239
  Here the \<open>cases\<close> or \<open>induct\<close> rules produced by the @{command inductive}
wenzelm@63531
   240
  package coincide with the expected elimination rules for Natural Deduction.
wenzelm@63531
   241
  Already in the original article by Gerhard Gentzen @{cite "Gentzen:1935"}
wenzelm@63531
   242
  there is a hint that each connective can be characterized by its
wenzelm@63531
   243
  introductions, and the elimination can be constructed systematically.
wenzelm@63531
   244
\<close>
wenzelm@58618
   245
wenzelm@58618
   246
wenzelm@58618
   247
section \<open>Recursive functions \label{sec:recursion}\<close>
wenzelm@58618
   248
wenzelm@58618
   249
text \<open>
wenzelm@42908
   250
  \begin{matharray}{rcl}
wenzelm@61493
   251
    @{command_def (HOL) "primrec"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@61493
   252
    @{command_def (HOL) "fun"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@61493
   253
    @{command_def (HOL) "function"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   254
    @{command_def (HOL) "termination"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   255
    @{command_def (HOL) "fun_cases"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@42908
   256
  \end{matharray}
wenzelm@42908
   257
wenzelm@55112
   258
  @{rail \<open>
wenzelm@63183
   259
    @@{command (HOL) primrec} @{syntax specification}
wenzelm@26849
   260
    ;
wenzelm@63183
   261
    (@@{command (HOL) fun} | @@{command (HOL) function}) opts? @{syntax specification}
wenzelm@26849
   262
    ;
wenzelm@63183
   263
    opts: '(' (('sequential' | 'domintros') + ',') ')'
wenzelm@26849
   264
    ;
wenzelm@42908
   265
    @@{command (HOL) termination} @{syntax term}?
krauss@54017
   266
    ;
krauss@54017
   267
    @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')
wenzelm@55112
   268
  \<close>}
wenzelm@26849
   269
wenzelm@63531
   270
  \<^descr> @{command (HOL) "primrec"} defines primitive recursive functions over
wenzelm@63531
   271
  datatypes (see also @{command_ref (HOL) datatype}). The given \<open>equations\<close>
wenzelm@63531
   272
  specify reduction rules that are produced by instantiating the generic
wenzelm@63531
   273
  combinator for primitive recursion that is available for each datatype.
wenzelm@42912
   274
wenzelm@42912
   275
  Each equation needs to be of the form:
wenzelm@42912
   276
wenzelm@42912
   277
  @{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"}
wenzelm@42912
   278
wenzelm@63531
   279
  such that \<open>C\<close> is a datatype constructor, \<open>rhs\<close> contains only the free
wenzelm@63531
   280
  variables on the left-hand side (or from the context), and all recursive
wenzelm@63531
   281
  occurrences of \<open>f\<close> in \<open>rhs\<close> are of the form \<open>f \<dots> y\<^sub>i \<dots>\<close> for some \<open>i\<close>. At
wenzelm@63531
   282
  most one reduction rule for each constructor can be given. The order does
wenzelm@63531
   283
  not matter. For missing constructors, the function is defined to return a
wenzelm@63531
   284
  default value, but this equation is made difficult to access for users.
wenzelm@60654
   285
wenzelm@60654
   286
  The reduction rules are declared as @{attribute simp} by default, which
wenzelm@60654
   287
  enables standard proof methods like @{method simp} and @{method auto} to
wenzelm@61493
   288
  normalize expressions of \<open>f\<close> applied to datatype constructions, by
wenzelm@60654
   289
  simulating symbolic computation via rewriting.
wenzelm@60654
   290
wenzelm@61439
   291
  \<^descr> @{command (HOL) "function"} defines functions by general wellfounded
wenzelm@60654
   292
  recursion. A detailed description with examples can be found in @{cite
wenzelm@60654
   293
  "isabelle-function"}. The function is specified by a set of (possibly
wenzelm@60654
   294
  conditional) recursive equations with arbitrary pattern matching. The
wenzelm@60654
   295
  command generates proof obligations for the completeness and the
wenzelm@60654
   296
  compatibility of patterns.
wenzelm@42907
   297
wenzelm@63531
   298
  The defined function is considered partial, and the resulting simplification
wenzelm@63531
   299
  rules (named \<open>f.psimps\<close>) and induction rule (named \<open>f.pinduct\<close>) are guarded
wenzelm@63531
   300
  by a generated domain predicate \<open>f_dom\<close>. The @{command (HOL) "termination"}
wenzelm@63531
   301
  command can then be used to establish that the function is total.
wenzelm@60654
   302
wenzelm@61439
   303
  \<^descr> @{command (HOL) "fun"} is a shorthand notation for ``@{command (HOL)
wenzelm@63531
   304
  "function"}~\<open>(sequential)\<close>'', followed by automated proof attempts regarding
wenzelm@63531
   305
  pattern matching and termination. See @{cite "isabelle-function"} for
wenzelm@63531
   306
  further details.
wenzelm@63531
   307
wenzelm@63531
   308
  \<^descr> @{command (HOL) "termination"}~\<open>f\<close> commences a termination proof for the
wenzelm@63531
   309
  previously defined function \<open>f\<close>. If this is omitted, the command refers to
wenzelm@63531
   310
  the most recent function definition. After the proof is closed, the
wenzelm@63531
   311
  recursive equations and the induction principle is established.
wenzelm@63531
   312
wenzelm@63531
   313
  \<^descr> @{command (HOL) "fun_cases"} generates specialized elimination rules for
wenzelm@63531
   314
  function equations. It expects one or more function equations and produces
wenzelm@63531
   315
  rules that eliminate the given equalities, following the cases given in the
wenzelm@63531
   316
  function definition.
wenzelm@63531
   317
wenzelm@63531
   318
wenzelm@63531
   319
  Recursive definitions introduced by the @{command (HOL) "function"} command
wenzelm@63531
   320
  accommodate reasoning by induction (cf.\ @{method induct}): rule \<open>f.induct\<close>
wenzelm@63531
   321
  refers to a specific induction rule, with parameters named according to the
wenzelm@63531
   322
  user-specified equations. Cases are numbered starting from 1. For @{command
wenzelm@63531
   323
  (HOL) "primrec"}, the induction principle coincides with structural
wenzelm@63531
   324
  recursion on the datatype where the recursion is carried out.
wenzelm@60654
   325
wenzelm@60654
   326
  The equations provided by these packages may be referred later as theorem
wenzelm@63531
   327
  list \<open>f.simps\<close>, where \<open>f\<close> is the (collective) name of the functions defined.
wenzelm@63531
   328
  Individual equations may be named explicitly as well.
wenzelm@60654
   329
wenzelm@60654
   330
  The @{command (HOL) "function"} command accepts the following options.
wenzelm@42908
   331
wenzelm@63531
   332
  \<^descr> \<open>sequential\<close> enables a preprocessor which disambiguates overlapping
wenzelm@63531
   333
  patterns by making them mutually disjoint. Earlier equations take precedence
wenzelm@63531
   334
  over later ones. This allows to give the specification in a format very
wenzelm@63531
   335
  similar to functional programming. Note that the resulting simplification
wenzelm@63531
   336
  and induction rules correspond to the transformed specification, not the one
wenzelm@63531
   337
  given originally. This usually means that each equation given by the user
wenzelm@63531
   338
  may result in several theorems. Also note that this automatic transformation
wenzelm@63531
   339
  only works for ML-style datatype patterns.
wenzelm@63531
   340
wenzelm@63531
   341
  \<^descr> \<open>domintros\<close> enables the automated generation of introduction rules for the
wenzelm@63531
   342
  domain predicate. While mostly not needed, they can be helpful in some
wenzelm@63531
   343
  proofs about partial functions.
wenzelm@58618
   344
\<close>
wenzelm@58618
   345
wenzelm@60654
   346
wenzelm@58618
   347
subsubsection \<open>Example: evaluation of expressions\<close>
wenzelm@58618
   348
wenzelm@63531
   349
text \<open>
wenzelm@63531
   350
  Subsequently, we define mutual datatypes for arithmetic and boolean
wenzelm@63531
   351
  expressions, and use @{command primrec} for evaluation functions that follow
wenzelm@63531
   352
  the same recursive structure.
wenzelm@63531
   353
\<close>
wenzelm@42912
   354
wenzelm@59905
   355
(*<*)experiment begin(*>*)
blanchet@58310
   356
datatype 'a aexp =
wenzelm@42912
   357
    IF "'a bexp"  "'a aexp"  "'a aexp"
wenzelm@42912
   358
  | Sum "'a aexp"  "'a aexp"
wenzelm@42912
   359
  | Diff "'a aexp"  "'a aexp"
wenzelm@42912
   360
  | Var 'a
wenzelm@42912
   361
  | Num nat
wenzelm@42912
   362
and 'a bexp =
wenzelm@42912
   363
    Less "'a aexp"  "'a aexp"
wenzelm@42912
   364
  | And "'a bexp"  "'a bexp"
wenzelm@42912
   365
  | Neg "'a bexp"
wenzelm@42912
   366
wenzelm@61421
   367
text \<open>\<^medskip> Evaluation of arithmetic and boolean expressions\<close>
wenzelm@42912
   368
wenzelm@42912
   369
primrec evala :: "('a \<Rightarrow> nat) \<Rightarrow> 'a aexp \<Rightarrow> nat"
wenzelm@42912
   370
  and evalb :: "('a \<Rightarrow> nat) \<Rightarrow> 'a bexp \<Rightarrow> bool"
wenzelm@42912
   371
where
wenzelm@42912
   372
  "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
wenzelm@42912
   373
| "evala env (Sum a1 a2) = evala env a1 + evala env a2"
wenzelm@42912
   374
| "evala env (Diff a1 a2) = evala env a1 - evala env a2"
wenzelm@42912
   375
| "evala env (Var v) = env v"
wenzelm@42912
   376
| "evala env (Num n) = n"
wenzelm@42912
   377
| "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
wenzelm@42912
   378
| "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
wenzelm@42912
   379
| "evalb env (Neg b) = (\<not> evalb env b)"
wenzelm@42912
   380
wenzelm@63531
   381
text \<open>
wenzelm@63531
   382
  Since the value of an expression depends on the value of its variables, the
wenzelm@63531
   383
  functions @{const evala} and @{const evalb} take an additional parameter, an
wenzelm@63531
   384
  \<^emph>\<open>environment\<close> that maps variables to their values.
wenzelm@60654
   385
wenzelm@61421
   386
  \<^medskip>
wenzelm@63531
   387
  Substitution on expressions can be defined similarly. The mapping \<open>f\<close> of
wenzelm@63531
   388
  type @{typ "'a \<Rightarrow> 'a aexp"} given as a parameter is lifted canonically on the
wenzelm@63531
   389
  types @{typ "'a aexp"} and @{typ "'a bexp"}, respectively.
wenzelm@58618
   390
\<close>
wenzelm@42912
   391
wenzelm@42912
   392
primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
wenzelm@42912
   393
  and substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp"
wenzelm@42912
   394
where
wenzelm@42912
   395
  "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
wenzelm@42912
   396
| "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
wenzelm@42912
   397
| "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
wenzelm@42912
   398
| "substa f (Var v) = f v"
wenzelm@42912
   399
| "substa f (Num n) = Num n"
wenzelm@42912
   400
| "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
wenzelm@42912
   401
| "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
wenzelm@42912
   402
| "substb f (Neg b) = Neg (substb f b)"
wenzelm@42912
   403
wenzelm@63531
   404
text \<open>
wenzelm@63531
   405
  In textbooks about semantics one often finds substitution theorems, which
wenzelm@63531
   406
  express the relationship between substitution and evaluation. For @{typ "'a
wenzelm@63531
   407
  aexp"} and @{typ "'a bexp"}, we can prove such a theorem by mutual
wenzelm@63531
   408
  induction, followed by simplification.
wenzelm@58618
   409
\<close>
wenzelm@42912
   410
wenzelm@42912
   411
lemma subst_one:
wenzelm@42912
   412
  "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
wenzelm@42912
   413
  "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
wenzelm@42912
   414
  by (induct a and b) simp_all
wenzelm@42912
   415
wenzelm@42912
   416
lemma subst_all:
wenzelm@42912
   417
  "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
wenzelm@42912
   418
  "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
wenzelm@42912
   419
  by (induct a and b) simp_all
wenzelm@59905
   420
(*<*)end(*>*)
wenzelm@42912
   421
wenzelm@42912
   422
wenzelm@58618
   423
subsubsection \<open>Example: a substitution function for terms\<close>
wenzelm@58618
   424
wenzelm@58618
   425
text \<open>Functions on datatypes with nested recursion are also defined
wenzelm@58618
   426
  by mutual primitive recursion.\<close>
wenzelm@42912
   427
wenzelm@59905
   428
(*<*)experiment begin(*>*)
blanchet@58310
   429
datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
wenzelm@42912
   430
wenzelm@63531
   431
text \<open>
wenzelm@63531
   432
  A substitution function on type @{typ "('a, 'b) term"} can be defined as
wenzelm@63531
   433
  follows, by working simultaneously on @{typ "('a, 'b) term list"}:
wenzelm@63531
   434
\<close>
wenzelm@42912
   435
wenzelm@42912
   436
primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term" and
wenzelm@42912
   437
  subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
wenzelm@42912
   438
where
wenzelm@42912
   439
  "subst_term f (Var a) = f a"
wenzelm@42912
   440
| "subst_term f (App b ts) = App b (subst_term_list f ts)"
wenzelm@42912
   441
| "subst_term_list f [] = []"
wenzelm@42912
   442
| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
wenzelm@42912
   443
wenzelm@63531
   444
text \<open>
wenzelm@63531
   445
  The recursion scheme follows the structure of the unfolded definition of
wenzelm@63531
   446
  type @{typ "('a, 'b) term"}. To prove properties of this substitution
wenzelm@63531
   447
  function, mutual induction is needed:
wenzelm@58618
   448
\<close>
wenzelm@42912
   449
wenzelm@59905
   450
lemma "subst_term (subst_term f1 \<circ> f2) t =
wenzelm@59905
   451
    subst_term f1 (subst_term f2 t)" and
wenzelm@59905
   452
  "subst_term_list (subst_term f1 \<circ> f2) ts =
wenzelm@59905
   453
    subst_term_list f1 (subst_term_list f2 ts)"
blanchet@58305
   454
  by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
wenzelm@59905
   455
(*<*)end(*>*)
wenzelm@42912
   456
wenzelm@42912
   457
wenzelm@58618
   458
subsubsection \<open>Example: a map function for infinitely branching trees\<close>
wenzelm@58618
   459
wenzelm@60654
   460
text \<open>Defining functions on infinitely branching datatypes by primitive
wenzelm@60654
   461
  recursion is just as easy.\<close>
wenzelm@42912
   462
wenzelm@59905
   463
(*<*)experiment begin(*>*)
blanchet@58310
   464
datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
wenzelm@42912
   465
wenzelm@42912
   466
primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
wenzelm@42912
   467
where
wenzelm@42912
   468
  "map_tree f (Atom a) = Atom (f a)"
wenzelm@42912
   469
| "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
wenzelm@42912
   470
wenzelm@63531
   471
text \<open>
wenzelm@63531
   472
  Note that all occurrences of functions such as \<open>ts\<close> above must be applied to
wenzelm@63531
   473
  an argument. In particular, @{term "map_tree f \<circ> ts"} is not allowed here.
wenzelm@60654
   474
wenzelm@61421
   475
  \<^medskip>
wenzelm@61421
   476
  Here is a simple composition lemma for @{term map_tree}:
wenzelm@60654
   477
\<close>
wenzelm@42912
   478
wenzelm@42912
   479
lemma "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
wenzelm@42912
   480
  by (induct t) simp_all
wenzelm@59905
   481
(*<*)end(*>*)
wenzelm@42912
   482
wenzelm@42907
   483
wenzelm@58618
   484
subsection \<open>Proof methods related to recursive definitions\<close>
wenzelm@58618
   485
wenzelm@58618
   486
text \<open>
wenzelm@26849
   487
  \begin{matharray}{rcl}
wenzelm@61493
   488
    @{method_def (HOL) pat_completeness} & : & \<open>method\<close> \\
wenzelm@61493
   489
    @{method_def (HOL) relation} & : & \<open>method\<close> \\
wenzelm@61493
   490
    @{method_def (HOL) lexicographic_order} & : & \<open>method\<close> \\
wenzelm@61493
   491
    @{method_def (HOL) size_change} & : & \<open>method\<close> \\
wenzelm@61493
   492
    @{method_def (HOL) induction_schema} & : & \<open>method\<close> \\
wenzelm@26849
   493
  \end{matharray}
wenzelm@26849
   494
wenzelm@55112
   495
  @{rail \<open>
wenzelm@42908
   496
    @@{method (HOL) relation} @{syntax term}
wenzelm@42908
   497
    ;
wenzelm@42908
   498
    @@{method (HOL) lexicographic_order} (@{syntax clasimpmod} * )
wenzelm@42908
   499
    ;
wenzelm@42908
   500
    @@{method (HOL) size_change} ( orders (@{syntax clasimpmod} * ) )
wenzelm@42908
   501
    ;
bulwahn@45944
   502
    @@{method (HOL) induction_schema}
bulwahn@45944
   503
    ;
wenzelm@42908
   504
    orders: ( 'max' | 'min' | 'ms' ) *
wenzelm@55112
   505
  \<close>}
wenzelm@42908
   506
wenzelm@63531
   507
  \<^descr> @{method (HOL) pat_completeness} is a specialized method to solve goals
wenzelm@63531
   508
  regarding the completeness of pattern matching, as required by the @{command
wenzelm@63531
   509
  (HOL) "function"} package (cf.\ @{cite "isabelle-function"}).
wenzelm@63531
   510
wenzelm@63531
   511
  \<^descr> @{method (HOL) relation}~\<open>R\<close> introduces a termination proof using the
wenzelm@63531
   512
  relation \<open>R\<close>. The resulting proof state will contain goals expressing that
wenzelm@63531
   513
  \<open>R\<close> is wellfounded, and that the arguments of recursive calls decrease with
wenzelm@63531
   514
  respect to \<open>R\<close>. Usually, this method is used as the initial proof step of
wenzelm@63531
   515
  manual termination proofs.
wenzelm@63531
   516
wenzelm@63531
   517
  \<^descr> @{method (HOL) "lexicographic_order"} attempts a fully automated
wenzelm@63531
   518
  termination proof by searching for a lexicographic combination of size
wenzelm@63531
   519
  measures on the arguments of the function. The method accepts the same
wenzelm@63531
   520
  arguments as the @{method auto} method, which it uses internally to prove
wenzelm@63531
   521
  local descents. The @{syntax clasimpmod} modifiers are accepted (as for
wenzelm@63531
   522
  @{method auto}).
wenzelm@63531
   523
wenzelm@63531
   524
  In case of failure, extensive information is printed, which can help to
wenzelm@63531
   525
  analyse the situation (cf.\ @{cite "isabelle-function"}).
wenzelm@63531
   526
wenzelm@63531
   527
  \<^descr> @{method (HOL) "size_change"} also works on termination goals, using a
wenzelm@63531
   528
  variation of the size-change principle, together with a graph decomposition
wenzelm@63531
   529
  technique (see @{cite krauss_phd} for details). Three kinds of orders are
wenzelm@63531
   530
  used internally: \<open>max\<close>, \<open>min\<close>, and \<open>ms\<close> (multiset), which is only available
wenzelm@63531
   531
  when the theory \<open>Multiset\<close> is loaded. When no order kinds are given, they
wenzelm@63531
   532
  are tried in order. The search for a termination proof uses SAT solving
wenzelm@42908
   533
  internally.
wenzelm@42908
   534
wenzelm@63531
   535
  For local descent proofs, the @{syntax clasimpmod} modifiers are accepted
wenzelm@63531
   536
  (as for @{method auto}).
wenzelm@63531
   537
wenzelm@63531
   538
  \<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
wenzelm@63531
   539
  from well-founded induction and completeness of patterns. This factors out
wenzelm@63531
   540
  some operations that are done internally by the function package and makes
wenzelm@63680
   541
  them available separately. See \<^file>\<open>~~/src/HOL/ex/Induction_Schema.thy\<close> for
wenzelm@63680
   542
  examples.
wenzelm@58618
   543
\<close>
wenzelm@58618
   544
wenzelm@58618
   545
wenzelm@58618
   546
subsection \<open>Functions with explicit partiality\<close>
wenzelm@58618
   547
wenzelm@58618
   548
text \<open>
wenzelm@42908
   549
  \begin{matharray}{rcl}
wenzelm@61493
   550
    @{command_def (HOL) "partial_function"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@61493
   551
    @{attribute_def (HOL) "partial_function_mono"} & : & \<open>attribute\<close> \\
wenzelm@42908
   552
  \end{matharray}
wenzelm@42908
   553
wenzelm@55112
   554
  @{rail \<open>
wenzelm@63183
   555
    @@{command (HOL) partial_function} '(' @{syntax name} ')'
wenzelm@63183
   556
      @{syntax specification}
wenzelm@55112
   557
  \<close>}
wenzelm@26849
   558
wenzelm@63531
   559
  \<^descr> @{command (HOL) "partial_function"}~\<open>(mode)\<close> defines recursive functions
wenzelm@63531
   560
  based on fixpoints in complete partial orders. No termination proof is
wenzelm@63531
   561
  required from the user or constructed internally. Instead, the possibility
wenzelm@63531
   562
  of non-termination is modelled explicitly in the result type, which contains
wenzelm@63531
   563
  an explicit bottom element.
wenzelm@63531
   564
wenzelm@63531
   565
  Pattern matching and mutual recursion are currently not supported. Thus, the
wenzelm@63531
   566
  specification consists of a single function described by a single recursive
wenzelm@63531
   567
  equation.
wenzelm@63531
   568
wenzelm@63531
   569
  There are no fixed syntactic restrictions on the body of the function, but
wenzelm@63531
   570
  the induced functional must be provably monotonic wrt.\ the underlying
wenzelm@63531
   571
  order. The monotonicity proof is performed internally, and the definition is
wenzelm@63531
   572
  rejected when it fails. The proof can be influenced by declaring hints using
wenzelm@63531
   573
  the @{attribute (HOL) partial_function_mono} attribute.
wenzelm@63531
   574
wenzelm@63531
   575
  The mandatory \<open>mode\<close> argument specifies the mode of operation of the
wenzelm@63531
   576
  command, which directly corresponds to a complete partial order on the
wenzelm@63531
   577
  result type. By default, the following modes are defined:
wenzelm@63531
   578
wenzelm@63531
   579
    \<^descr> \<open>option\<close> defines functions that map into the @{type option} type. Here,
wenzelm@63531
   580
    the value @{term None} is used to model a non-terminating computation.
wenzelm@63531
   581
    Monotonicity requires that if @{term None} is returned by a recursive
wenzelm@63531
   582
    call, then the overall result must also be @{term None}. This is best
wenzelm@63531
   583
    achieved through the use of the monadic operator @{const "Option.bind"}.
wenzelm@63531
   584
wenzelm@63531
   585
    \<^descr> \<open>tailrec\<close> defines functions with an arbitrary result type and uses the
wenzelm@63531
   586
    slightly degenerated partial order where @{term "undefined"} is the bottom
wenzelm@63531
   587
    element. Now, monotonicity requires that if @{term undefined} is returned
wenzelm@63531
   588
    by a recursive call, then the overall result must also be @{term
wenzelm@63531
   589
    undefined}. In practice, this is only satisfied when each recursive call
wenzelm@63531
   590
    is a tail call, whose result is directly returned. Thus, this mode of
wenzelm@63531
   591
    operation allows the definition of arbitrary tail-recursive functions.
wenzelm@63531
   592
wenzelm@63531
   593
  Experienced users may define new modes by instantiating the locale @{const
wenzelm@63531
   594
  "partial_function_definitions"} appropriately.
wenzelm@63531
   595
wenzelm@63531
   596
  \<^descr> @{attribute (HOL) partial_function_mono} declares rules for use in the
wenzelm@63531
   597
  internal monotonicity proofs of partial function definitions.
wenzelm@58618
   598
\<close>
wenzelm@58618
   599
wenzelm@58618
   600
wenzelm@58618
   601
subsection \<open>Old-style recursive function definitions (TFL)\<close>
wenzelm@58618
   602
wenzelm@58618
   603
text \<open>
wenzelm@42908
   604
  \begin{matharray}{rcl}
wenzelm@61493
   605
    @{command_def (HOL) "recdef"} & : & \<open>theory \<rightarrow> theory)\<close> \\
wenzelm@42908
   606
  \end{matharray}
wenzelm@42908
   607
wenzelm@60523
   608
  The old TFL command @{command (HOL) "recdef"} for defining recursive is
wenzelm@60523
   609
  mostly obsolete; @{command (HOL) "function"} or @{command (HOL) "fun"}
wenzelm@60523
   610
  should be used instead.
wenzelm@46280
   611
wenzelm@55112
   612
  @{rail \<open>
wenzelm@55029
   613
    @@{command (HOL) recdef} ('(' @'permissive' ')')? \<newline>
wenzelm@42908
   614
      @{syntax name} @{syntax term} (@{syntax prop} +) hints?
wenzelm@42908
   615
    ;
wenzelm@42908
   616
    hints: '(' @'hints' ( recdefmod * ) ')'
wenzelm@42908
   617
    ;
wenzelm@42908
   618
    recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf')
wenzelm@62969
   619
      (() | 'add' | 'del') ':' @{syntax thms}) | @{syntax clasimpmod}
wenzelm@55112
   620
  \<close>}
wenzelm@42908
   621
wenzelm@63531
   622
  \<^descr> @{command (HOL) "recdef"} defines general well-founded recursive functions
wenzelm@63531
   623
  (using the TFL package). The ``\<open>(permissive)\<close>'' option tells TFL to recover
wenzelm@63531
   624
  from failed proof attempts, returning unfinished results. The \<open>recdef_simp\<close>,
wenzelm@63531
   625
  \<open>recdef_cong\<close>, and \<open>recdef_wf\<close> hints refer to auxiliary rules to be used in
wenzelm@63531
   626
  the internal automated proof process of TFL. Additional @{syntax clasimpmod}
wenzelm@63531
   627
  declarations may be given to tune the context of the Simplifier (cf.\
wenzelm@63531
   628
  \secref{sec:simplifier}) and Classical reasoner (cf.\
wenzelm@63531
   629
  \secref{sec:classical}).
wenzelm@42908
   630
wenzelm@42908
   631
wenzelm@61421
   632
  \<^medskip>
wenzelm@63531
   633
  Hints for @{command (HOL) "recdef"} may be also declared globally, using the
wenzelm@63531
   634
  following attributes.
wenzelm@42908
   635
wenzelm@42908
   636
  \begin{matharray}{rcl}
wenzelm@61493
   637
    @{attribute_def (HOL) recdef_simp} & : & \<open>attribute\<close> \\
wenzelm@61493
   638
    @{attribute_def (HOL) recdef_cong} & : & \<open>attribute\<close> \\
wenzelm@61493
   639
    @{attribute_def (HOL) recdef_wf} & : & \<open>attribute\<close> \\
wenzelm@42908
   640
  \end{matharray}
wenzelm@42908
   641
wenzelm@55112
   642
  @{rail \<open>
wenzelm@42908
   643
    (@@{attribute (HOL) recdef_simp} | @@{attribute (HOL) recdef_cong} |
wenzelm@42908
   644
      @@{attribute (HOL) recdef_wf}) (() | 'add' | 'del')
wenzelm@55112
   645
  \<close>}
wenzelm@58618
   646
\<close>
wenzelm@58618
   647
wenzelm@58618
   648
wenzelm@60657
   649
section \<open>Adhoc overloading of constants\<close>
wenzelm@60657
   650
wenzelm@60657
   651
text \<open>
wenzelm@60657
   652
  \begin{tabular}{rcll}
wenzelm@61493
   653
  @{command_def "adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@61493
   654
  @{command_def "no_adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@61493
   655
  @{attribute_def "show_variants"} & : & \<open>attribute\<close> & default \<open>false\<close> \\
wenzelm@60657
   656
  \end{tabular}
wenzelm@60657
   657
wenzelm@61421
   658
  \<^medskip>
wenzelm@63531
   659
  Adhoc overloading allows to overload a constant depending on its type.
wenzelm@63531
   660
  Typically this involves the introduction of an uninterpreted constant (used
wenzelm@63531
   661
  for input and output) and the addition of some variants (used internally).
wenzelm@63680
   662
  For examples see \<^file>\<open>~~/src/HOL/ex/Adhoc_Overloading_Examples.thy\<close> and
wenzelm@63680
   663
  \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
wenzelm@60657
   664
wenzelm@60657
   665
  @{rail \<open>
wenzelm@60657
   666
    (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
wenzelm@62969
   667
      (@{syntax name} (@{syntax term} + ) + @'and')
wenzelm@60657
   668
  \<close>}
wenzelm@60657
   669
wenzelm@63531
   670
  \<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close> associates variants with an
wenzelm@63531
   671
  existing constant.
wenzelm@63531
   672
wenzelm@63531
   673
  \<^descr> @{command "no_adhoc_overloading"} is similar to @{command
wenzelm@63531
   674
  "adhoc_overloading"}, but removes the specified variants from the present
wenzelm@63531
   675
  context.
wenzelm@63531
   676
wenzelm@63531
   677
  \<^descr> @{attribute "show_variants"} controls printing of variants of overloaded
wenzelm@63531
   678
  constants. If enabled, the internally used variants are printed instead of
wenzelm@63531
   679
  their respective overloaded constants. This is occasionally useful to check
wenzelm@63531
   680
  whether the system agrees with a user's expectations about derived variants.
wenzelm@60657
   681
\<close>
wenzelm@60657
   682
wenzelm@60657
   683
wenzelm@60657
   684
section \<open>Definition by specification \label{sec:hol-specification}\<close>
wenzelm@60657
   685
wenzelm@60657
   686
text \<open>
wenzelm@60657
   687
  \begin{matharray}{rcl}
wenzelm@61493
   688
    @{command_def (HOL) "specification"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
wenzelm@60657
   689
  \end{matharray}
wenzelm@60657
   690
wenzelm@60657
   691
  @{rail \<open>
wenzelm@60657
   692
    @@{command (HOL) specification} '(' (decl +) ')' \<newline>
wenzelm@60657
   693
      (@{syntax thmdecl}? @{syntax prop} +)
wenzelm@60657
   694
    ;
wenzelm@60657
   695
    decl: (@{syntax name} ':')? @{syntax term} ('(' @'overloaded' ')')?
wenzelm@60657
   696
  \<close>}
wenzelm@60657
   697
wenzelm@63531
   698
  \<^descr> @{command (HOL) "specification"}~\<open>decls \<phi>\<close> sets up a goal stating the
wenzelm@63531
   699
  existence of terms with the properties specified to hold for the constants
wenzelm@63531
   700
  given in \<open>decls\<close>. After finishing the proof, the theory will be augmented
wenzelm@63531
   701
  with definitions for the given constants, as well as with theorems stating
wenzelm@63531
   702
  the properties for these constants.
wenzelm@63531
   703
wenzelm@63531
   704
  \<open>decl\<close> declares a constant to be defined by the specification given. The
wenzelm@63531
   705
  definition for the constant \<open>c\<close> is bound to the name \<open>c_def\<close> unless a
wenzelm@63531
   706
  theorem name is given in the declaration. Overloaded constants should be
wenzelm@63531
   707
  declared as such.
wenzelm@60657
   708
\<close>
wenzelm@60657
   709
wenzelm@60657
   710
wenzelm@58618
   711
section \<open>Old-style datatypes \label{sec:hol-datatype}\<close>
wenzelm@58618
   712
wenzelm@58618
   713
text \<open>
wenzelm@42908
   714
  \begin{matharray}{rcl}
wenzelm@61493
   715
    @{command_def (HOL) "old_datatype"} & : & \<open>theory \<rightarrow> theory\<close> \\
wenzelm@61493
   716
    @{command_def (HOL) "old_rep_datatype"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
wenzelm@42908
   717
  \end{matharray}
wenzelm@42908
   718
wenzelm@55112
   719
  @{rail \<open>
blanchet@58305
   720
    @@{command (HOL) old_datatype} (spec + @'and')
wenzelm@42908
   721
    ;
blanchet@58306
   722
    @@{command (HOL) old_rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
wenzelm@42908
   723
    ;
wenzelm@42908
   724
wenzelm@45839
   725
    spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|')
wenzelm@42908
   726
    ;
wenzelm@42908
   727
    cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
wenzelm@55112
   728
  \<close>}
wenzelm@42908
   729
wenzelm@61439
   730
  \<^descr> @{command (HOL) "old_datatype"} defines old-style inductive
blanchet@58305
   731
  datatypes in HOL.
wenzelm@42908
   732
wenzelm@61439
   733
  \<^descr> @{command (HOL) "old_rep_datatype"} represents existing types as
blanchet@58305
   734
  old-style datatypes.
wenzelm@42908
   735
wenzelm@42908
   736
wenzelm@63531
   737
  These commands are mostly obsolete; @{command (HOL) "datatype"} should be
wenzelm@63531
   738
  used instead.
wenzelm@63531
   739
wenzelm@63531
   740
  See @{cite "isabelle-datatypes"} for more details on datatypes. Apart from
wenzelm@63531
   741
  proper proof methods for case analysis and induction, there are also
wenzelm@42908
   742
  emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
wenzelm@63531
   743
  induct_tac} available, see \secref{sec:hol-induct-tac}; these admit to refer
wenzelm@63531
   744
  directly to the internal structure of subgoals (including internally bound
wenzelm@63531
   745
  parameters).
wenzelm@58618
   746
\<close>
wenzelm@58618
   747
wenzelm@58618
   748
wenzelm@58618
   749
subsubsection \<open>Examples\<close>
wenzelm@58618
   750
wenzelm@63531
   751
text \<open>
wenzelm@63531
   752
  We define a type of finite sequences, with slightly different names than the
wenzelm@63531
   753
  existing @{typ "'a list"} that is already in @{theory Main}:
wenzelm@63531
   754
\<close>
wenzelm@42910
   755
wenzelm@59905
   756
(*<*)experiment begin(*>*)
blanchet@58310
   757
datatype 'a seq = Empty | Seq 'a "'a seq"
wenzelm@42910
   758
wenzelm@58618
   759
text \<open>We can now prove some simple lemma by structural induction:\<close>
wenzelm@42910
   760
wenzelm@42910
   761
lemma "Seq x xs \<noteq> xs"
wenzelm@42910
   762
proof (induct xs arbitrary: x)
wenzelm@42910
   763
  case Empty
wenzelm@58618
   764
  txt \<open>This case can be proved using the simplifier: the freeness
wenzelm@42910
   765
    properties of the datatype are already declared as @{attribute
wenzelm@58618
   766
    simp} rules.\<close>
wenzelm@42910
   767
  show "Seq x Empty \<noteq> Empty"
wenzelm@42910
   768
    by simp
wenzelm@42910
   769
next
wenzelm@42910
   770
  case (Seq y ys)
wenzelm@58618
   771
  txt \<open>The step case is proved similarly.\<close>
wenzelm@42910
   772
  show "Seq x (Seq y ys) \<noteq> Seq y ys"
wenzelm@58618
   773
    using \<open>Seq y ys \<noteq> ys\<close> by simp
wenzelm@42910
   774
qed
wenzelm@42910
   775
wenzelm@58618
   776
text \<open>Here is a more succinct version of the same proof:\<close>
wenzelm@42910
   777
wenzelm@42910
   778
lemma "Seq x xs \<noteq> xs"
wenzelm@42910
   779
  by (induct xs arbitrary: x) simp_all
wenzelm@59905
   780
(*<*)end(*>*)
wenzelm@42910
   781
wenzelm@42910
   782
wenzelm@58618
   783
section \<open>Records \label{sec:hol-record}\<close>
wenzelm@58618
   784
wenzelm@58618
   785
text \<open>
wenzelm@26849
   786
  In principle, records merely generalize the concept of tuples, where
wenzelm@63531
   787
  components may be addressed by labels instead of just position. The logical
wenzelm@63531
   788
  infrastructure of records in Isabelle/HOL is slightly more advanced, though,
wenzelm@63531
   789
  supporting truly extensible record schemes. This admits operations that are
wenzelm@63531
   790
  polymorphic with respect to record extension, yielding ``object-oriented''
wenzelm@63531
   791
  effects like (single) inheritance. See also @{cite "NaraschewskiW-TPHOLs98"}
wenzelm@63531
   792
  for more details on object-oriented verification and record subtyping in
wenzelm@63531
   793
  HOL.
wenzelm@58618
   794
\<close>
wenzelm@58618
   795
wenzelm@58618
   796
wenzelm@58618
   797
subsection \<open>Basic concepts\<close>
wenzelm@58618
   798
wenzelm@58618
   799
text \<open>
wenzelm@63531
   800
  Isabelle/HOL supports both \<^emph>\<open>fixed\<close> and \<^emph>\<open>schematic\<close> records at the level of
wenzelm@63531
   801
  terms and types. The notation is as follows:
wenzelm@26849
   802
wenzelm@26849
   803
  \begin{center}
wenzelm@26849
   804
  \begin{tabular}{l|l|l}
wenzelm@26849
   805
    & record terms & record types \\ \hline
wenzelm@61493
   806
    fixed & \<open>\<lparr>x = a, y = b\<rparr>\<close> & \<open>\<lparr>x :: A, y :: B\<rparr>\<close> \\
wenzelm@61493
   807
    schematic & \<open>\<lparr>x = a, y = b, \<dots> = m\<rparr>\<close> &
wenzelm@61493
   808
      \<open>\<lparr>x :: A, y :: B, \<dots> :: M\<rparr>\<close> \\
wenzelm@26849
   809
  \end{tabular}
wenzelm@26849
   810
  \end{center}
wenzelm@26849
   811
wenzelm@61493
   812
  The ASCII representation of \<open>\<lparr>x = a\<rparr>\<close> is \<open>(| x = a |)\<close>.
wenzelm@61493
   813
wenzelm@63531
   814
  A fixed record \<open>\<lparr>x = a, y = b\<rparr>\<close> has field \<open>x\<close> of value \<open>a\<close> and field \<open>y\<close> of
wenzelm@63531
   815
  value \<open>b\<close>. The corresponding type is \<open>\<lparr>x :: A, y :: B\<rparr>\<close>, assuming that \<open>a ::
wenzelm@63531
   816
  A\<close> and \<open>b :: B\<close>.
wenzelm@63531
   817
wenzelm@63531
   818
  A record scheme like \<open>\<lparr>x = a, y = b, \<dots> = m\<rparr>\<close> contains fields \<open>x\<close> and \<open>y\<close> as
wenzelm@63531
   819
  before, but also possibly further fields as indicated by the ``\<open>\<dots>\<close>''
wenzelm@63531
   820
  notation (which is actually part of the syntax). The improper field ``\<open>\<dots>\<close>''
wenzelm@63531
   821
  of a record scheme is called the \<^emph>\<open>more part\<close>. Logically it is just a free
wenzelm@63531
   822
  variable, which is occasionally referred to as ``row variable'' in the
wenzelm@63531
   823
  literature. The more part of a record scheme may be instantiated by zero or
wenzelm@63531
   824
  more further components. For example, the previous scheme may get
wenzelm@63531
   825
  instantiated to \<open>\<lparr>x = a, y = b, z = c, \<dots> = m'\<rparr>\<close>, where \<open>m'\<close> refers to a
wenzelm@63531
   826
  different more part. Fixed records are special instances of record schemes,
wenzelm@63531
   827
  where ``\<open>\<dots>\<close>'' is properly terminated by the \<open>() :: unit\<close> element. In fact,
wenzelm@63531
   828
  \<open>\<lparr>x = a, y = b\<rparr>\<close> is just an abbreviation for \<open>\<lparr>x = a, y = b, \<dots> = ()\<rparr>\<close>.
wenzelm@42123
   829
wenzelm@61421
   830
  \<^medskip>
wenzelm@63531
   831
  Two key observations make extensible records in a simply typed language like
wenzelm@63531
   832
  HOL work out:
wenzelm@63531
   833
wenzelm@63531
   834
  \<^enum> the more part is internalized, as a free term or type variable,
wenzelm@63531
   835
wenzelm@63531
   836
  \<^enum> field names are externalized, they cannot be accessed within the logic as
wenzelm@63531
   837
  first-class values.
wenzelm@26849
   838
wenzelm@26849
   839
wenzelm@61421
   840
  \<^medskip>
wenzelm@63531
   841
  In Isabelle/HOL record types have to be defined explicitly, fixing their
wenzelm@63531
   842
  field names and types, and their (optional) parent record. Afterwards,
wenzelm@63531
   843
  records may be formed using above syntax, while obeying the canonical order
wenzelm@63531
   844
  of fields as given by their declaration. The record package provides several
wenzelm@63531
   845
  standard operations like selectors and updates. The common setup for various
wenzelm@63531
   846
  generic proof tools enable succinct reasoning patterns. See also the
wenzelm@63531
   847
  Isabelle/HOL tutorial @{cite "isabelle-hol-book"} for further instructions
wenzelm@63531
   848
  on using records in practice.
wenzelm@58618
   849
\<close>
wenzelm@58618
   850
wenzelm@58618
   851
wenzelm@58618
   852
subsection \<open>Record specifications\<close>
wenzelm@58618
   853
wenzelm@58618
   854
text \<open>
wenzelm@26849
   855
  \begin{matharray}{rcl}
wenzelm@61493
   856
    @{command_def (HOL) "record"} & : & \<open>theory \<rightarrow> theory\<close> \\
kleing@62120
   857
    @{command_def (HOL) "print_record"} & : & \<open>context \<rightarrow>\<close> \\
wenzelm@26849
   858
  \end{matharray}
wenzelm@26849
   859
wenzelm@55112
   860
  @{rail \<open>
wenzelm@61260
   861
    @@{command (HOL) record} @{syntax "overloaded"}? @{syntax typespec_sorts} '=' \<newline>
wenzelm@46494
   862
      (@{syntax type} '+')? (constdecl +)
wenzelm@46494
   863
    ;
wenzelm@46494
   864
    constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
kleing@62120
   865
    ;
kleing@62120
   866
    @@{command (HOL) print_record} modes? @{syntax typespec_sorts}
kleing@62120
   867
    ;
kleing@62120
   868
    modes: '(' (@{syntax name} +) ')'
wenzelm@55112
   869
  \<close>}
wenzelm@26849
   870
wenzelm@63531
   871
  \<^descr> @{command (HOL) "record"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1 \<dots> c\<^sub>n :: \<sigma>\<^sub>n\<close>
wenzelm@63531
   872
  defines extensible record type \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close>, derived from the optional
wenzelm@63531
   873
  parent record \<open>\<tau>\<close> by adding new field components \<open>c\<^sub>i :: \<sigma>\<^sub>i\<close> etc.
wenzelm@63531
   874
wenzelm@63531
   875
  The type variables of \<open>\<tau>\<close> and \<open>\<sigma>\<^sub>i\<close> need to be covered by the (distinct)
wenzelm@63531
   876
  parameters \<open>\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m\<close>. Type constructor \<open>t\<close> has to be new, while \<open>\<tau>\<close>
wenzelm@63531
   877
  needs to specify an instance of an existing record type. At least one new
wenzelm@63531
   878
  field \<open>c\<^sub>i\<close> has to be specified. Basically, field names need to belong to a
wenzelm@63531
   879
  unique record. This is not a real restriction in practice, since fields are
wenzelm@63531
   880
  qualified by the record name internally.
wenzelm@63531
   881
wenzelm@63531
   882
  The parent record specification \<open>\<tau>\<close> is optional; if omitted \<open>t\<close> becomes a
wenzelm@63531
   883
  root record. The hierarchy of all records declared within a theory context
wenzelm@63531
   884
  forms a forest structure, i.e.\ a set of trees starting with a root record
wenzelm@63531
   885
  each. There is no way to merge multiple parent records!
wenzelm@63531
   886
wenzelm@63531
   887
  For convenience, \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> is made a type abbreviation for the fixed
wenzelm@63531
   888
  record type \<open>\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>\<close>, likewise is \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>)
wenzelm@63531
   889
  t_scheme\<close> made an abbreviation for \<open>\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>\<close>.
wenzelm@63531
   890
wenzelm@63531
   891
  \<^descr> @{command (HOL) "print_record"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> prints the definition of
wenzelm@63531
   892
  record \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close>. Optionally \<open>modes\<close> can be specified, which are
wenzelm@63531
   893
  appended to the current print mode; see \secref{sec:print-modes}.
wenzelm@58618
   894
\<close>
wenzelm@58618
   895
wenzelm@58618
   896
wenzelm@58618
   897
subsection \<open>Record operations\<close>
wenzelm@58618
   898
wenzelm@63531
   899
text \<open>
wenzelm@63531
   900
  Any record definition of the form presented above produces certain standard
wenzelm@63531
   901
  operations. Selectors and updates are provided for any field, including the
wenzelm@63531
   902
  improper one ``\<open>more\<close>''. There are also cumulative record constructor
wenzelm@63531
   903
  functions. To simplify the presentation below, we assume for now that \<open>(\<alpha>\<^sub>1,
wenzelm@63531
   904
  \<dots>, \<alpha>\<^sub>m) t\<close> is a root record with fields \<open>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<close>.
wenzelm@60654
   905
wenzelm@61421
   906
  \<^medskip>
wenzelm@61477
   907
  \<^bold>\<open>Selectors\<close> and \<^bold>\<open>updates\<close> are available for any
wenzelm@61493
   908
  field (including ``\<open>more\<close>''):
wenzelm@26849
   909
wenzelm@26849
   910
  \begin{matharray}{lll}
wenzelm@61493
   911
    \<open>c\<^sub>i\<close> & \<open>::\<close> & \<open>\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i\<close> \\
wenzelm@61493
   912
    \<open>c\<^sub>i_update\<close> & \<open>::\<close> & \<open>\<sigma>\<^sub>i \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>\<close> \\
wenzelm@26849
   913
  \end{matharray}
wenzelm@26849
   914
wenzelm@63531
   915
  There is special syntax for application of updates: \<open>r\<lparr>x := a\<rparr>\<close> abbreviates
wenzelm@63531
   916
  term \<open>x_update a r\<close>. Further notation for repeated updates is also
wenzelm@63531
   917
  available: \<open>r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z := c\<rparr>\<close> may be written \<open>r\<lparr>x := a, y := b, z
wenzelm@63531
   918
  := c\<rparr>\<close>. Note that because of postfix notation the order of fields shown here
wenzelm@63531
   919
  is reverse than in the actual term. Since repeated updates are just function
wenzelm@63531
   920
  applications, fields may be freely permuted in \<open>\<lparr>x := a, y := b, z := c\<rparr>\<close>,
wenzelm@63531
   921
  as far as logical equality is concerned. Thus commutativity of independent
wenzelm@63531
   922
  updates can be proven within the logic for any two fields, but not as a
wenzelm@63531
   923
  general theorem.
wenzelm@26849
   924
wenzelm@61421
   925
  \<^medskip>
wenzelm@63531
   926
  The \<^bold>\<open>make\<close> operation provides a cumulative record constructor function:
wenzelm@26849
   927
wenzelm@26849
   928
  \begin{matharray}{lll}
wenzelm@61493
   929
    \<open>t.make\<close> & \<open>::\<close> & \<open>\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>\<close> \\
wenzelm@26849
   930
  \end{matharray}
wenzelm@26849
   931
wenzelm@61421
   932
  \<^medskip>
wenzelm@63531
   933
  We now reconsider the case of non-root records, which are derived of some
wenzelm@63531
   934
  parent. In general, the latter may depend on another parent as well,
wenzelm@63531
   935
  resulting in a list of \<^emph>\<open>ancestor records\<close>. Appending the lists of fields of
wenzelm@63531
   936
  all ancestors results in a certain field prefix. The record package
wenzelm@63531
   937
  automatically takes care of this by lifting operations over this context of
wenzelm@63531
   938
  ancestor fields. Assuming that \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> has ancestor fields \<open>b\<^sub>1 ::
wenzelm@63531
   939
  \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k\<close>, the above record operations will get the following
wenzelm@63531
   940
  types:
wenzelm@26849
   941
wenzelm@61421
   942
  \<^medskip>
wenzelm@26852
   943
  \begin{tabular}{lll}
wenzelm@61493
   944
    \<open>c\<^sub>i\<close> & \<open>::\<close> & \<open>\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i\<close> \\
wenzelm@61493
   945
    \<open>c\<^sub>i_update\<close> & \<open>::\<close> & \<open>\<sigma>\<^sub>i \<Rightarrow>
wenzelm@26852
   946
      \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
wenzelm@61493
   947
      \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>\<close> \\
wenzelm@61493
   948
    \<open>t.make\<close> & \<open>::\<close> & \<open>\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>
wenzelm@61493
   949
      \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>\<close> \\
wenzelm@26852
   950
  \end{tabular}
wenzelm@61421
   951
  \<^medskip>
wenzelm@26849
   952
wenzelm@63531
   953
  Some further operations address the extension aspect of a derived record
wenzelm@63531
   954
  scheme specifically: \<open>t.fields\<close> produces a record fragment consisting of
wenzelm@63531
   955
  exactly the new fields introduced here (the result may serve as a more part
wenzelm@63531
   956
  elsewhere); \<open>t.extend\<close> takes a fixed record and adds a given more part;
wenzelm@63531
   957
  \<open>t.truncate\<close> restricts a record scheme to a fixed record.
wenzelm@26849
   958
wenzelm@61421
   959
  \<^medskip>
wenzelm@26852
   960
  \begin{tabular}{lll}
wenzelm@61493
   961
    \<open>t.fields\<close> & \<open>::\<close> & \<open>\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>\<close> \\
wenzelm@61493
   962
    \<open>t.extend\<close> & \<open>::\<close> & \<open>\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow>
wenzelm@61493
   963
      \<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>\<close> \\
wenzelm@61493
   964
    \<open>t.truncate\<close> & \<open>::\<close> & \<open>\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>\<close> \\
wenzelm@26852
   965
  \end{tabular}
wenzelm@61421
   966
  \<^medskip>
wenzelm@26849
   967
wenzelm@63531
   968
  Note that \<open>t.make\<close> and \<open>t.fields\<close> coincide for root records.
wenzelm@58618
   969
\<close>
wenzelm@58618
   970
wenzelm@58618
   971
wenzelm@58618
   972
subsection \<open>Derived rules and proof tools\<close>
wenzelm@58618
   973
wenzelm@58618
   974
text \<open>
wenzelm@63531
   975
  The record package proves several results internally, declaring these facts
wenzelm@63531
   976
  to appropriate proof tools. This enables users to reason about record
wenzelm@63531
   977
  structures quite conveniently. Assume that \<open>t\<close> is a record type as specified
wenzelm@63531
   978
  above.
wenzelm@26849
   979
wenzelm@61421
   980
  \<^enum> Standard conversions for selectors or updates applied to record
wenzelm@60654
   981
  constructor terms are made part of the default Simplifier context; thus
wenzelm@60654
   982
  proofs by reduction of basic operations merely require the @{method simp}
wenzelm@63531
   983
  method without further arguments. These rules are available as \<open>t.simps\<close>,
wenzelm@63531
   984
  too.
wenzelm@60654
   985
wenzelm@61421
   986
  \<^enum> Selectors applied to updated records are automatically reduced by an
wenzelm@60654
   987
  internal simplification procedure, which is also part of the standard
wenzelm@60654
   988
  Simplifier setup.
wenzelm@60654
   989
wenzelm@63531
   990
  \<^enum> Inject equations of a form analogous to @{prop "(x, y) = (x', y') \<equiv> x = x'
wenzelm@63531
   991
  \<and> y = y'"} are declared to the Simplifier and Classical Reasoner as
wenzelm@61493
   992
  @{attribute iff} rules. These rules are available as \<open>t.iffs\<close>.
wenzelm@61493
   993
wenzelm@63531
   994
  \<^enum> The introduction rule for record equality analogous to \<open>x r = x r' \<Longrightarrow> y r =
wenzelm@63531
   995
  y r' \<dots> \<Longrightarrow> r = r'\<close> is declared to the Simplifier, and as the basic rule
wenzelm@63531
   996
  context as ``@{attribute intro}\<open>?\<close>''. The rule is called \<open>t.equality\<close>.
wenzelm@63531
   997
wenzelm@63531
   998
  \<^enum> Representations of arbitrary record expressions as canonical constructor
wenzelm@63531
   999
  terms are provided both in @{method cases} and @{method induct} format (cf.\
wenzelm@63531
  1000
  the generic proof methods of the same name, \secref{sec:cases-induct}).
wenzelm@63531
  1001
  Several variations are available, for fixed records, record schemes, more
wenzelm@63531
  1002
  parts etc.
wenzelm@60654
  1003
wenzelm@60654
  1004
  The generic proof methods are sufficiently smart to pick the most sensible
wenzelm@60654
  1005
  rule according to the type of the indicated record expression: users just
wenzelm@63531
  1006
  need to apply something like ``\<open>(cases r)\<close>'' to a certain proof problem.
wenzelm@63531
  1007
wenzelm@63531
  1008
  \<^enum> The derived record operations \<open>t.make\<close>, \<open>t.fields\<close>, \<open>t.extend\<close>,
wenzelm@63531
  1009
  \<open>t.truncate\<close> are \<^emph>\<open>not\<close> treated automatically, but usually need to be
wenzelm@63531
  1010
  expanded by hand, using the collective fact \<open>t.defs\<close>.
wenzelm@58618
  1011
\<close>
wenzelm@58618
  1012
wenzelm@58618
  1013
wenzelm@58618
  1014
subsubsection \<open>Examples\<close>
wenzelm@58618
  1015
wenzelm@63680
  1016
text \<open>See \<^file>\<open>~~/src/HOL/ex/Records.thy\<close>, for example.\<close>
wenzelm@58618
  1017
wenzelm@60654
  1018
wenzelm@61269
  1019
section \<open>Semantic subtype definitions \label{sec:hol-typedef}\<close>
wenzelm@58618
  1020
wenzelm@58618
  1021
text \<open>
wenzelm@46280
  1022
  \begin{matharray}{rcl}
wenzelm@61493
  1023
    @{command_def (HOL) "typedef"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
wenzelm@46280
  1024
  \end{matharray}
wenzelm@46280
  1025
wenzelm@61269
  1026
  A type definition identifies a new type with a non-empty subset of an
wenzelm@61269
  1027
  existing type. More precisely, the new type is defined by exhibiting an
wenzelm@63531
  1028
  existing type \<open>\<tau>\<close>, a set \<open>A :: \<tau> set\<close>, and proving @{prop "\<exists>x. x \<in> A"}. Thus
wenzelm@63531
  1029
  \<open>A\<close> is a non-empty subset of \<open>\<tau>\<close>, and the new type denotes this subset. New
wenzelm@63531
  1030
  functions are postulated that establish an isomorphism between the new type
wenzelm@63531
  1031
  and the subset. In general, the type \<open>\<tau>\<close> may involve type variables \<open>\<alpha>\<^sub>1, \<dots>,
wenzelm@63531
  1032
  \<alpha>\<^sub>n\<close> which means that the type definition produces a type constructor \<open>(\<alpha>\<^sub>1,
wenzelm@63531
  1033
  \<dots>, \<alpha>\<^sub>n) t\<close> depending on those type arguments.
wenzelm@47859
  1034
wenzelm@55112
  1035
  @{rail \<open>
wenzelm@61260
  1036
    @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set
wenzelm@61260
  1037
    ;
wenzelm@61260
  1038
    @{syntax_def "overloaded"}: ('(' @'overloaded' ')')
wenzelm@26849
  1039
    ;
wenzelm@42908
  1040
    abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
wenzelm@42908
  1041
    ;
wenzelm@42908
  1042
    rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
wenzelm@55112
  1043
  \<close>}
wenzelm@26849
  1044
wenzelm@63531
  1045
  To understand the concept of type definition better, we need to recount its
wenzelm@63531
  1046
  somewhat complex history. The HOL logic goes back to the ``Simple Theory of
wenzelm@63531
  1047
  Types'' (STT) of A. Church @{cite "church40"}, which is further explained in
wenzelm@63531
  1048
  the book by P. Andrews @{cite "andrews86"}. The overview article by W.
wenzelm@63531
  1049
  Farmer @{cite "Farmer:2008"} points out the ``seven virtues'' of this
wenzelm@63531
  1050
  relatively simple family of logics. STT has only ground types, without
wenzelm@63531
  1051
  polymorphism and without type definitions.
wenzelm@61269
  1052
wenzelm@61421
  1053
  \<^medskip>
wenzelm@63531
  1054
  M. Gordon @{cite "Gordon:1985:HOL"} augmented Church's STT by adding
wenzelm@63531
  1055
  schematic polymorphism (type variables and type constructors) and a facility
wenzelm@63531
  1056
  to introduce new types as semantic subtypes from existing types. This
wenzelm@63531
  1057
  genuine extension of the logic was explained semantically by A. Pitts in the
wenzelm@63531
  1058
  book of the original Cambridge HOL88 system @{cite "pitts93"}. Type
wenzelm@63531
  1059
  definitions work in this setting, because the general model-theory of STT is
wenzelm@63531
  1060
  restricted to models that ensure that the universe of type interpretations
wenzelm@63531
  1061
  is closed by forming subsets (via predicates taken from the logic).
wenzelm@61269
  1062
wenzelm@61421
  1063
  \<^medskip>
wenzelm@63531
  1064
  Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded constant
wenzelm@63531
  1065
  definitions @{cite "Wenzel:1997:TPHOL" and "Haftmann-Wenzel:2006:classes"},
wenzelm@63531
  1066
  which are actually a concept of Isabelle/Pure and do not depend on
wenzelm@63531
  1067
  particular set-theoretic semantics of HOL. Over many years, there was no
wenzelm@63531
  1068
  formal checking of semantic type definitions in Isabelle/HOL versus
wenzelm@63531
  1069
  syntactic constant definitions in Isabelle/Pure. So the @{command typedef}
wenzelm@63531
  1070
  command was described as ``axiomatic'' in the sense of
wenzelm@63531
  1071
  \secref{sec:axiomatizations}, only with some local checks of the given type
wenzelm@63531
  1072
  and its representing set.
wenzelm@61269
  1073
wenzelm@61269
  1074
  Recent clarification of overloading in the HOL logic proper @{cite
wenzelm@62206
  1075
  "Kuncar-Popescu:2015"} demonstrates how the dissimilar concepts of constant
wenzelm@61269
  1076
  definitions versus type definitions may be understood uniformly. This
wenzelm@61269
  1077
  requires an interpretation of Isabelle/HOL that substantially reforms the
wenzelm@61269
  1078
  set-theoretic model of A. Pitts @{cite "pitts93"}, by taking a schematic
wenzelm@63531
  1079
  view on polymorphism and interpreting only ground types in the set-theoretic
wenzelm@63531
  1080
  sense of HOL88. Moreover, type-constructors may be explicitly overloaded,
wenzelm@63531
  1081
  e.g.\ by making the subset depend on type-class parameters (cf.\
wenzelm@63531
  1082
  \secref{sec:class}). This is semantically like a dependent type: the meaning
wenzelm@63531
  1083
  relies on the operations provided by different type-class instances.
wenzelm@63531
  1084
wenzelm@63531
  1085
  \<^descr> @{command (HOL) "typedef"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A\<close> defines a new type \<open>(\<alpha>\<^sub>1,
wenzelm@63531
  1086
  \<dots>, \<alpha>\<^sub>n) t\<close> from the set \<open>A\<close> over an existing type. The set \<open>A\<close> may contain
wenzelm@63531
  1087
  type variables \<open>\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n\<close> as specified on the LHS, but no term variables.
wenzelm@63531
  1088
  Non-emptiness of \<open>A\<close> needs to be proven on the spot, in order to turn the
wenzelm@63531
  1089
  internal conditional characterization into usable theorems.
wenzelm@63531
  1090
wenzelm@63531
  1091
  The ``\<open>(overloaded)\<close>'' option allows the @{command "typedef"} specification
wenzelm@63531
  1092
  to depend on constants that are not (yet) specified and thus left open as
wenzelm@63531
  1093
  parameters, e.g.\ type-class parameters.
wenzelm@61269
  1094
wenzelm@61269
  1095
  Within a local theory specification, the newly introduced type constructor
wenzelm@61269
  1096
  cannot depend on parameters or assumptions of the context: this is
wenzelm@63531
  1097
  syntactically impossible in HOL. The non-emptiness proof may formally depend
wenzelm@63531
  1098
  on local assumptions, but this has little practical relevance.
wenzelm@63531
  1099
wenzelm@63531
  1100
  For @{command (HOL) "typedef"}~\<open>t = A\<close> the newly introduced type \<open>t\<close> is
wenzelm@63531
  1101
  accompanied by a pair of morphisms to relate it to the representing set over
wenzelm@63531
  1102
  the old type. By default, the injection from type to set is called \<open>Rep_t\<close>
wenzelm@63531
  1103
  and its inverse \<open>Abs_t\<close>: An explicit @{keyword (HOL) "morphisms"}
wenzelm@63531
  1104
  specification allows to provide alternative names.
wenzelm@26849
  1105
wenzelm@61269
  1106
  The logical characterization of @{command typedef} uses the predicate of
wenzelm@61269
  1107
  locale @{const type_definition} that is defined in Isabelle/HOL. Various
wenzelm@63531
  1108
  basic consequences of that are instantiated accordingly, re-using the locale
wenzelm@63531
  1109
  facts with names derived from the new type constructor. Thus the generic
wenzelm@63531
  1110
  theorem @{thm type_definition.Rep} is turned into the specific \<open>Rep_t\<close>, for
wenzelm@63531
  1111
  example.
wenzelm@63531
  1112
wenzelm@63531
  1113
  Theorems @{thm type_definition.Rep}, @{thm type_definition.Rep_inverse}, and
wenzelm@63531
  1114
  @{thm type_definition.Abs_inverse} provide the most basic characterization
wenzelm@63531
  1115
  as a corresponding injection/surjection pair (in both directions). The
wenzelm@63531
  1116
  derived rules @{thm type_definition.Rep_inject} and @{thm
wenzelm@42908
  1117
  type_definition.Abs_inject} provide a more convenient version of
wenzelm@63531
  1118
  injectivity, suitable for automated proof tools (e.g.\ in declarations
wenzelm@63531
  1119
  involving @{attribute simp} or @{attribute iff}). Furthermore, the rules
wenzelm@63531
  1120
  @{thm type_definition.Rep_cases}~/ @{thm type_definition.Rep_induct}, and
wenzelm@63531
  1121
  @{thm type_definition.Abs_cases}~/ @{thm type_definition.Abs_induct} provide
wenzelm@63531
  1122
  alternative views on surjectivity. These rules are already declared as set
wenzelm@63531
  1123
  or type rules for the generic @{method cases} and @{method induct} methods,
wenzelm@42908
  1124
  respectively.
wenzelm@58618
  1125
\<close>
wenzelm@58618
  1126
wenzelm@59905
  1127
wenzelm@58618
  1128
subsubsection \<open>Examples\<close>
wenzelm@58618
  1129
wenzelm@63531
  1130
text \<open>
wenzelm@63531
  1131
  The following trivial example pulls a three-element type into existence
wenzelm@63531
  1132
  within the formal logical environment of Isabelle/HOL.\<close>
wenzelm@42908
  1133
wenzelm@59905
  1134
(*<*)experiment begin(*>*)
wenzelm@49834
  1135
typedef three = "{(True, True), (True, False), (False, True)}"
wenzelm@42908
  1136
  by blast
wenzelm@42908
  1137
wenzelm@42908
  1138
definition "One = Abs_three (True, True)"
wenzelm@42908
  1139
definition "Two = Abs_three (True, False)"
wenzelm@42908
  1140
definition "Three = Abs_three (False, True)"
wenzelm@42908
  1141
wenzelm@42908
  1142
lemma three_distinct: "One \<noteq> Two"  "One \<noteq> Three"  "Two \<noteq> Three"
wenzelm@49812
  1143
  by (simp_all add: One_def Two_def Three_def Abs_three_inject)
wenzelm@42908
  1144
wenzelm@42908
  1145
lemma three_cases:
wenzelm@42908
  1146
  fixes x :: three obtains "x = One" | "x = Two" | "x = Three"
wenzelm@49812
  1147
  by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
wenzelm@59905
  1148
(*<*)end(*>*)
wenzelm@42908
  1149
wenzelm@58618
  1150
text \<open>Note that such trivial constructions are better done with
wenzelm@58618
  1151
  derived specification mechanisms such as @{command datatype}:\<close>
blanchet@58310
  1152
wenzelm@59905
  1153
(*<*)experiment begin(*>*)
wenzelm@59905
  1154
datatype three = One | Two | Three
wenzelm@59905
  1155
(*<*)end(*>*)
wenzelm@42908
  1156
wenzelm@58618
  1157
text \<open>This avoids re-doing basic definitions and proofs from the
wenzelm@58618
  1158
  primitive @{command typedef} above.\<close>
wenzelm@58618
  1159
wenzelm@58618
  1160
wenzelm@58618
  1161
wenzelm@58618
  1162
section \<open>Functorial structure of types\<close>
wenzelm@58618
  1163
wenzelm@58618
  1164
text \<open>
haftmann@41396
  1165
  \begin{matharray}{rcl}
wenzelm@61493
  1166
    @{command_def (HOL) "functor"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close>
haftmann@41396
  1167
  \end{matharray}
haftmann@41396
  1168
wenzelm@55112
  1169
  @{rail \<open>
blanchet@55467
  1170
    @@{command (HOL) functor} (@{syntax name} ':')? @{syntax term}
wenzelm@55112
  1171
  \<close>}
haftmann@41396
  1172
wenzelm@63531
  1173
  \<^descr> @{command (HOL) "functor"}~\<open>prefix: m\<close> allows to prove and register
wenzelm@63531
  1174
  properties about the functorial structure of type constructors. These
wenzelm@63531
  1175
  properties then can be used by other packages to deal with those type
wenzelm@63531
  1176
  constructors in certain type constructions. Characteristic theorems are
wenzelm@63531
  1177
  noted in the current local theory. By default, they are prefixed with the
wenzelm@63531
  1178
  base name of the type constructor, an explicit prefix can be given
wenzelm@60654
  1179
  alternatively.
haftmann@41396
  1180
wenzelm@63531
  1181
  The given term \<open>m\<close> is considered as \<^emph>\<open>mapper\<close> for the corresponding type
wenzelm@63531
  1182
  constructor and must conform to the following type pattern:
haftmann@41396
  1183
haftmann@41396
  1184
  \begin{matharray}{lll}
wenzelm@61493
  1185
    \<open>m\<close> & \<open>::\<close> &
wenzelm@61493
  1186
      \<open>\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>k \<Rightarrow> (\<^vec>\<alpha>\<^sub>n) t \<Rightarrow> (\<^vec>\<beta>\<^sub>n) t\<close> \\
haftmann@41396
  1187
  \end{matharray}
haftmann@41396
  1188
wenzelm@63531
  1189
  where \<open>t\<close> is the type constructor, \<open>\<^vec>\<alpha>\<^sub>n\<close> and \<open>\<^vec>\<beta>\<^sub>n\<close> are
wenzelm@63531
  1190
  distinct type variables free in the local theory and \<open>\<sigma>\<^sub>1\<close>, \ldots, \<open>\<sigma>\<^sub>k\<close> is
wenzelm@63531
  1191
  a subsequence of \<open>\<alpha>\<^sub>1 \<Rightarrow> \<beta>\<^sub>1\<close>, \<open>\<beta>\<^sub>1 \<Rightarrow> \<alpha>\<^sub>1\<close>, \ldots, \<open>\<alpha>\<^sub>n \<Rightarrow> \<beta>\<^sub>n\<close>, \<open>\<beta>\<^sub>n \<Rightarrow> \<alpha>\<^sub>n\<close>.
wenzelm@58618
  1192
\<close>
wenzelm@58618
  1193
wenzelm@58618
  1194
wenzelm@60671
  1195
section \<open>Quotient types with lifting and transfer\<close>
wenzelm@60671
  1196
wenzelm@63531
  1197
text \<open>
wenzelm@63531
  1198
  The quotient package defines a new quotient type given a raw type and a
wenzelm@63531
  1199
  partial equivalence relation (\secref{sec:quotient-type}). The package also
wenzelm@63531
  1200
  historically includes automation for transporting definitions and theorems
wenzelm@63531
  1201
  (\secref{sec:old-quotient}), but most of this automation was superseded by
wenzelm@63531
  1202
  the Lifting (\secref{sec:lifting}) and Transfer (\secref{sec:transfer})
wenzelm@63531
  1203
  packages.
wenzelm@63531
  1204
\<close>
wenzelm@60671
  1205
wenzelm@60671
  1206
wenzelm@60671
  1207
subsection \<open>Quotient type definition \label{sec:quotient-type}\<close>
wenzelm@58618
  1208
wenzelm@58618
  1209
text \<open>
wenzelm@50109
  1210
  \begin{matharray}{rcl}
wenzelm@61493
  1211
    @{command_def (HOL) "quotient_type"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close>\\
wenzelm@50109
  1212
  \end{matharray}
wenzelm@50109
  1213
wenzelm@55112
  1214
  @{rail \<open>
wenzelm@61260
  1215
    @@{command (HOL) quotient_type} @{syntax "overloaded"}? \<newline>
wenzelm@61260
  1216
      @{syntax typespec} @{syntax mixfix}? '=' quot_type \<newline>
wenzelm@61260
  1217
      quot_morphisms? quot_parametric?
wenzelm@60658
  1218
    ;
wenzelm@60658
  1219
    quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term}
wenzelm@55112
  1220
    ;
wenzelm@60658
  1221
    quot_morphisms: @'morphisms' @{syntax name} @{syntax name}
wenzelm@60658
  1222
    ;
wenzelm@62969
  1223
    quot_parametric: @'parametric' @{syntax thm}
wenzelm@55112
  1224
  \<close>}
wenzelm@50109
  1225
wenzelm@63531
  1226
  \<^descr> @{command (HOL) "quotient_type"} defines a new quotient type \<open>\<tau>\<close>. The
wenzelm@63531
  1227
  injection from a quotient type to a raw type is called \<open>rep_\<tau>\<close>, its inverse
wenzelm@63531
  1228
  \<open>abs_\<tau>\<close> unless explicit @{keyword (HOL) "morphisms"} specification provides
wenzelm@63531
  1229
  alternative names. @{command (HOL) "quotient_type"} requires the user to
wenzelm@63531
  1230
  prove that the relation is an equivalence relation (predicate \<open>equivp\<close>),
wenzelm@63531
  1231
  unless the user specifies explicitly \<open>partial\<close> in which case the obligation
wenzelm@63531
  1232
  is \<open>part_equivp\<close>. A quotient defined with \<open>partial\<close> is weaker in the sense
wenzelm@63531
  1233
  that less things can be proved automatically.
wenzelm@50109
  1234
kuncar@54334
  1235
  The command internally proves a Quotient theorem and sets up the Lifting
wenzelm@63531
  1236
  package by the command @{command (HOL) setup_lifting}. Thus the Lifting and
wenzelm@63531
  1237
  Transfer packages can be used also with quotient types defined by @{command
wenzelm@63531
  1238
  (HOL) "quotient_type"} without any extra set-up. The parametricity theorem
wenzelm@63531
  1239
  for the equivalence relation R can be provided as an extra argument of the
wenzelm@63531
  1240
  command and is passed to the corresponding internal call of @{command (HOL)
wenzelm@63531
  1241
  setup_lifting}. This theorem allows the Lifting package to generate a
wenzelm@63531
  1242
  stronger transfer rule for equality.
wenzelm@58618
  1243
\<close>
wenzelm@58618
  1244
wenzelm@58618
  1245
wenzelm@60671
  1246
subsection \<open>Lifting package \label{sec:lifting}\<close>
wenzelm@58618
  1247
wenzelm@58618
  1248
text \<open>
wenzelm@60660
  1249
  The Lifting package allows users to lift terms of the raw type to the
wenzelm@60660
  1250
  abstract type, which is a necessary step in building a library for an
wenzelm@60660
  1251
  abstract type. Lifting defines a new constant by combining coercion
wenzelm@63531
  1252
  functions (@{term Abs} and @{term Rep}) with the raw term. It also proves an
wenzelm@63531
  1253
  appropriate transfer rule for the Transfer (\secref{sec:transfer}) package
wenzelm@63531
  1254
  and, if possible, an equation for the code generator.
wenzelm@60660
  1255
wenzelm@60660
  1256
  The Lifting package provides two main commands: @{command (HOL)
wenzelm@60660
  1257
  "setup_lifting"} for initializing the package to work with a new type, and
wenzelm@60660
  1258
  @{command (HOL) "lift_definition"} for lifting constants. The Lifting
wenzelm@60660
  1259
  package works with all four kinds of type abstraction: type copies,
wenzelm@60660
  1260
  subtypes, total quotients and partial quotients.
wenzelm@60660
  1261
wenzelm@60660
  1262
  Theoretical background can be found in @{cite
wenzelm@60660
  1263
  "Huffman-Kuncar:2013:lifting_transfer"}.
wenzelm@60660
  1264
wenzelm@60671
  1265
  \begin{matharray}{rcl}
wenzelm@61493
  1266
    @{command_def (HOL) "setup_lifting"} & : & \<open>local_theory \<rightarrow> local_theory\<close>\\
wenzelm@61493
  1267
    @{command_def (HOL) "lift_definition"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close>\\
wenzelm@61493
  1268
    @{command_def (HOL) "lifting_forget"} & : & \<open>local_theory \<rightarrow> local_theory\<close>\\
wenzelm@61493
  1269
    @{command_def (HOL) "lifting_update"} & : & \<open>local_theory \<rightarrow> local_theory\<close>\\
wenzelm@61493
  1270
    @{command_def (HOL) "print_quot_maps"} & : & \<open>context \<rightarrow>\<close>\\
wenzelm@61493
  1271
    @{command_def (HOL) "print_quotients"} & : & \<open>context \<rightarrow>\<close>\\
wenzelm@61493
  1272
    @{attribute_def (HOL) "quot_map"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1273
    @{attribute_def (HOL) "relator_eq_onp"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1274
    @{attribute_def (HOL) "relator_mono"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1275
    @{attribute_def (HOL) "relator_distr"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1276
    @{attribute_def (HOL) "quot_del"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1277
    @{attribute_def (HOL) "lifting_restore"} & : & \<open>attribute\<close> \\
wenzelm@60671
  1278
  \end{matharray}
wenzelm@60671
  1279
wenzelm@55112
  1280
  @{rail \<open>
wenzelm@62969
  1281
    @@{command (HOL) setup_lifting} @{syntax thm} @{syntax thm}? \<newline>
wenzelm@62969
  1282
      (@'parametric' @{syntax thm})?
wenzelm@60661
  1283
    ;
wenzelm@60661
  1284
    @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? \<newline>
wenzelm@60661
  1285
      @{syntax name} '::' @{syntax type} @{syntax mixfix}? 'is' @{syntax term} \<newline>
wenzelm@62969
  1286
      (@'parametric' (@{syntax thm}+))?
wenzelm@60661
  1287
    ;
wenzelm@62969
  1288
    @@{command (HOL) lifting_forget} @{syntax name}
wenzelm@60661
  1289
    ;
wenzelm@62969
  1290
    @@{command (HOL) lifting_update} @{syntax name}
wenzelm@60661
  1291
    ;
wenzelm@60670
  1292
    @@{attribute (HOL) lifting_restore}
wenzelm@62969
  1293
      @{syntax thm} (@{syntax thm} @{syntax thm})?
wenzelm@55112
  1294
  \<close>}
kuncar@47802
  1295
wenzelm@63531
  1296
  \<^descr> @{command (HOL) "setup_lifting"} Sets up the Lifting package to work with
wenzelm@63531
  1297
  a user-defined type. The command supports two modes.
wenzelm@63531
  1298
wenzelm@63531
  1299
    \<^enum> The first one is a low-level mode when the user must provide as a first
wenzelm@63531
  1300
    argument of @{command (HOL) "setup_lifting"} a quotient theorem @{term
wenzelm@63531
  1301
    "Quotient R Abs Rep T"}. The package configures a transfer rule for
wenzelm@61458
  1302
    equality, a domain transfer rules and sets up the @{command_def (HOL)
wenzelm@61458
  1303
    "lift_definition"} command to work with the abstract type. An optional
wenzelm@61458
  1304
    theorem @{term "reflp R"}, which certifies that the equivalence relation R
wenzelm@61458
  1305
    is total, can be provided as a second argument. This allows the package to
wenzelm@61458
  1306
    generate stronger transfer rules. And finally, the parametricity theorem
wenzelm@61458
  1307
    for @{term R} can be provided as a third argument. This allows the package
wenzelm@61458
  1308
    to generate a stronger transfer rule for equality.
wenzelm@61458
  1309
wenzelm@63531
  1310
    Users generally will not prove the \<open>Quotient\<close> theorem manually for new
wenzelm@63531
  1311
    types, as special commands exist to automate the process.
wenzelm@61458
  1312
wenzelm@61459
  1313
    \<^enum> When a new subtype is defined by @{command (HOL) typedef}, @{command
wenzelm@61458
  1314
    (HOL) "lift_definition"} can be used in its second mode, where only the
wenzelm@61458
  1315
    @{term type_definition} theorem @{term "type_definition Rep Abs A"} is
wenzelm@61458
  1316
    used as an argument of the command. The command internally proves the
wenzelm@61458
  1317
    corresponding @{term Quotient} theorem and registers it with @{command
wenzelm@61458
  1318
    (HOL) setup_lifting} using its first mode.
wenzelm@60660
  1319
wenzelm@60660
  1320
  For quotients, the command @{command (HOL) quotient_type} can be used. The
wenzelm@63531
  1321
  command defines a new quotient type and similarly to the previous case, the
wenzelm@63531
  1322
  corresponding Quotient theorem is proved and registered by @{command (HOL)
wenzelm@63531
  1323
  setup_lifting}.
wenzelm@60660
  1324
wenzelm@61421
  1325
  \<^medskip>
wenzelm@63531
  1326
  The command @{command (HOL) "setup_lifting"} also sets up the code generator
wenzelm@63531
  1327
  for the new type. Later on, when a new constant is defined by @{command
wenzelm@63531
  1328
  (HOL) "lift_definition"}, the Lifting package proves and registers a code
wenzelm@63531
  1329
  equation (if there is one) for the new constant.
wenzelm@63531
  1330
wenzelm@63531
  1331
  \<^descr> @{command (HOL) "lift_definition"} \<open>f :: \<tau>\<close> @{keyword (HOL) "is"} \<open>t\<close>
wenzelm@63531
  1332
  Defines a new function \<open>f\<close> with an abstract type \<open>\<tau>\<close> in terms of a
wenzelm@63531
  1333
  corresponding operation \<open>t\<close> on a representation type. More formally, if \<open>t
wenzelm@63531
  1334
  :: \<sigma>\<close>, then the command builds a term \<open>F\<close> as a corresponding combination of
wenzelm@63531
  1335
  abstraction and representation functions such that \<open>F :: \<sigma> \<Rightarrow> \<tau>\<close> and defines
wenzelm@63531
  1336
  \<open>f \<equiv> F t\<close>. The term \<open>t\<close> does not have to be necessarily a constant but it
wenzelm@63531
  1337
  can be any term.
wenzelm@63531
  1338
wenzelm@63531
  1339
  The command opens a proof and the user must discharge a respectfulness proof
wenzelm@63531
  1340
  obligation. For a type copy, i.e.\ a typedef with \<open>UNIV\<close>, the obligation is
wenzelm@63531
  1341
  discharged automatically. The proof goal is presented in a user-friendly,
wenzelm@63531
  1342
  readable form. A respectfulness theorem in the standard format \<open>f.rsp\<close> and a
wenzelm@63531
  1343
  transfer rule \<open>f.transfer\<close> for the Transfer package are generated by the
wenzelm@63531
  1344
  package.
wenzelm@63531
  1345
wenzelm@63531
  1346
  The user can specify a parametricity theorems for \<open>t\<close> after the keyword
wenzelm@63531
  1347
  @{keyword "parametric"}, which allows the command to generate parametric
wenzelm@63531
  1348
  transfer rules for \<open>f\<close>.
wenzelm@60660
  1349
wenzelm@60660
  1350
  For each constant defined through trivial quotients (type copies or
wenzelm@63531
  1351
  subtypes) \<open>f.rep_eq\<close> is generated. The equation is a code certificate that
wenzelm@63531
  1352
  defines \<open>f\<close> using the representation function.
wenzelm@63531
  1353
wenzelm@63531
  1354
  For each constant \<open>f.abs_eq\<close> is generated. The equation is unconditional for
wenzelm@63531
  1355
  total quotients. The equation defines \<open>f\<close> using the abstraction function.
wenzelm@60660
  1356
wenzelm@61421
  1357
  \<^medskip>
wenzelm@63531
  1358
  Integration with [@{attribute code} abstract]: For subtypes (e.g.\
wenzelm@63531
  1359
  corresponding to a datatype invariant, such as @{typ "'a dlist"}), @{command
wenzelm@63531
  1360
  (HOL) "lift_definition"} uses a code certificate theorem \<open>f.rep_eq\<close> as a
wenzelm@63531
  1361
  code equation. Because of the limitation of the code generator, \<open>f.rep_eq\<close>
wenzelm@63531
  1362
  cannot be used as a code equation if the subtype occurs inside the result
wenzelm@63531
  1363
  type rather than at the top level (e.g.\ function returning @{typ "'a dlist
wenzelm@63531
  1364
  option"} vs. @{typ "'a dlist"}).
wenzelm@60670
  1365
wenzelm@60670
  1366
  In this case, an extension of @{command (HOL) "lift_definition"} can be
wenzelm@63531
  1367
  invoked by specifying the flag \<open>code_dt\<close>. This extension enables code
wenzelm@63531
  1368
  execution through series of internal type and lifting definitions if the
wenzelm@63531
  1369
  return type \<open>\<tau>\<close> meets the following inductive conditions:
wenzelm@61493
  1370
wenzelm@61493
  1371
    \<^descr> \<open>\<tau>\<close> is a type variable
wenzelm@61493
  1372
wenzelm@63531
  1373
    \<^descr> \<open>\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>\<close>, where \<open>\<kappa>\<close> is an abstract type constructor and \<open>\<tau>\<^sub>1 \<dots>
wenzelm@63531
  1374
    \<tau>\<^sub>n\<close> do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed
wenzelm@63531
  1375
    whereas @{typ "int dlist dlist"} not)
wenzelm@63531
  1376
wenzelm@63531
  1377
    \<^descr> \<open>\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>\<close>, \<open>\<kappa>\<close> is a type constructor that was defined as a
wenzelm@63531
  1378
    (co)datatype whose constructor argument types do not contain either
wenzelm@63531
  1379
    non-free datatypes or the function type.
wenzelm@60670
  1380
wenzelm@60660
  1381
  Integration with [@{attribute code} equation]: For total quotients,
wenzelm@63531
  1382
  @{command (HOL) "lift_definition"} uses \<open>f.abs_eq\<close> as a code equation.
wenzelm@63531
  1383
wenzelm@63531
  1384
  \<^descr> @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} These
wenzelm@63531
  1385
  two commands serve for storing and deleting the set-up of the Lifting
wenzelm@63531
  1386
  package and corresponding transfer rules defined by this package. This is
wenzelm@63531
  1387
  useful for hiding of type construction details of an abstract type when the
wenzelm@63531
  1388
  construction is finished but it still allows additions to this construction
wenzelm@63531
  1389
  when this is later necessary.
wenzelm@63531
  1390
wenzelm@63531
  1391
  Whenever the Lifting package is set up with a new abstract type \<open>\<tau>\<close> by
wenzelm@63531
  1392
  @{command_def (HOL) "lift_definition"}, the package defines a new bundle
wenzelm@63531
  1393
  that is called \<open>\<tau>.lifting\<close>. This bundle already includes set-up for the
wenzelm@63531
  1394
  Lifting package. The new transfer rules introduced by @{command (HOL)
wenzelm@63531
  1395
  "lift_definition"} can be stored in the bundle by the command @{command
wenzelm@63531
  1396
  (HOL) "lifting_update"} \<open>\<tau>.lifting\<close>.
wenzelm@63531
  1397
wenzelm@63531
  1398
  The command @{command (HOL) "lifting_forget"} \<open>\<tau>.lifting\<close> deletes set-up of
wenzelm@63531
  1399
  the Lifting package for \<open>\<tau>\<close> and deletes all the transfer rules that were
wenzelm@63531
  1400
  introduced by @{command (HOL) "lift_definition"} using \<open>\<tau>\<close> as an abstract
wenzelm@63531
  1401
  type.
wenzelm@60660
  1402
wenzelm@60660
  1403
  The stored set-up in a bundle can be reintroduced by the Isar commands for
wenzelm@60660
  1404
  including a bundle (@{command "include"}, @{keyword "includes"} and
wenzelm@60660
  1405
  @{command "including"}).
kuncar@54334
  1406
wenzelm@63531
  1407
  \<^descr> @{command (HOL) "print_quot_maps"} prints stored quotient map theorems.
wenzelm@60660
  1408
wenzelm@61439
  1409
  \<^descr> @{command (HOL) "print_quotients"} prints stored quotient theorems.
wenzelm@61439
  1410
wenzelm@63531
  1411
  \<^descr> @{attribute (HOL) quot_map} registers a quotient map theorem, a theorem
wenzelm@63531
  1412
  showing how to ``lift'' quotients over type constructors. E.g.\ @{term
wenzelm@63531
  1413
  "Quotient R Abs Rep T \<Longrightarrow> Quotient (rel_set R) (image Abs) (image Rep)
wenzelm@63680
  1414
  (rel_set T)"}. For examples see \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or
wenzelm@63680
  1415
  \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property is proved automatically if the
wenzelm@63680
  1416
  involved type is BNF without dead variables.
wenzelm@63531
  1417
wenzelm@63531
  1418
  \<^descr> @{attribute (HOL) relator_eq_onp} registers a theorem that shows that a
wenzelm@63531
  1419
  relator applied to an equality restricted by a predicate @{term P} (i.e.\
wenzelm@63531
  1420
  @{term "eq_onp P"}) is equal to a predicator applied to the @{term P}. The
wenzelm@63531
  1421
  combinator @{const eq_onp} is used for internal encoding of proper subtypes.
wenzelm@63531
  1422
  Such theorems allows the package to hide \<open>eq_onp\<close> from a user in a
wenzelm@63680
  1423
  user-readable form of a respectfulness theorem. For examples see
wenzelm@63680
  1424
  \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
wenzelm@63680
  1425
  is proved automatically if the involved type is BNF without dead variables.
wenzelm@60660
  1426
wenzelm@61439
  1427
  \<^descr> @{attribute (HOL) "relator_mono"} registers a property describing a
wenzelm@60670
  1428
  monotonicity of a relator. E.g.\ @{prop "A \<le> B \<Longrightarrow> rel_set A \<le> rel_set B"}.
wenzelm@60660
  1429
  This property is needed for proving a stronger transfer rule in
wenzelm@63531
  1430
  @{command_def (HOL) "lift_definition"} when a parametricity theorem for the
wenzelm@63531
  1431
  raw term is specified and also for the reflexivity prover. For examples see
wenzelm@63680
  1432
  \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
wenzelm@63680
  1433
  is proved automatically if the involved type is BNF without dead variables.
wenzelm@60660
  1434
wenzelm@61439
  1435
  \<^descr> @{attribute (HOL) "relator_distr"} registers a property describing a
wenzelm@63531
  1436
  distributivity of the relation composition and a relator. E.g.\ \<open>rel_set R
wenzelm@63531
  1437
  \<circ>\<circ> rel_set S = rel_set (R \<circ>\<circ> S)\<close>. This property is needed for proving a
wenzelm@63531
  1438
  stronger transfer rule in @{command_def (HOL) "lift_definition"} when a
wenzelm@63531
  1439
  parametricity theorem for the raw term is specified. When this equality does
wenzelm@63531
  1440
  not hold unconditionally (e.g.\ for the function type), the user can
wenzelm@63531
  1441
  specified each direction separately and also register multiple theorems with
wenzelm@63531
  1442
  different set of assumptions. This attribute can be used only after the
wenzelm@63531
  1443
  monotonicity property was already registered by @{attribute (HOL)
wenzelm@63680
  1444
  "relator_mono"}. For examples see \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or
wenzelm@63680
  1445
  \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property is proved automatically if the
wenzelm@63680
  1446
  involved type is BNF without dead variables.
wenzelm@63531
  1447
wenzelm@63531
  1448
  \<^descr> @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem from
wenzelm@63531
  1449
  the Lifting infrastructure and thus de-register the corresponding quotient.
wenzelm@63531
  1450
  This effectively causes that @{command (HOL) lift_definition} will not do
wenzelm@63531
  1451
  any lifting for the corresponding type. This attribute is rather used for
wenzelm@63531
  1452
  low-level manipulation with set-up of the Lifting package because @{command
wenzelm@63531
  1453
  (HOL) lifting_forget} is preferred for normal usage.
wenzelm@63531
  1454
wenzelm@63531
  1455
  \<^descr> @{attribute (HOL) lifting_restore} \<open>Quotient_thm pcr_def pcr_cr_eq_thm\<close>
wenzelm@63531
  1456
  registers the Quotient theorem \<open>Quotient_thm\<close> in the Lifting infrastructure
wenzelm@63531
  1457
  and thus sets up lifting for an abstract type \<open>\<tau>\<close> (that is defined by
wenzelm@63531
  1458
  \<open>Quotient_thm\<close>). Optional theorems \<open>pcr_def\<close> and \<open>pcr_cr_eq_thm\<close> can be
wenzelm@63531
  1459
  specified to register the parametrized correspondence relation for \<open>\<tau>\<close>.
wenzelm@63531
  1460
  E.g.\ for @{typ "'a dlist"}, \<open>pcr_def\<close> is \<open>pcr_dlist A \<equiv> list_all2 A \<circ>\<circ>
wenzelm@63531
  1461
  cr_dlist\<close> and \<open>pcr_cr_eq_thm\<close> is \<open>pcr_dlist (op =) = (op =)\<close>. This attribute
wenzelm@63531
  1462
  is rather used for low-level manipulation with set-up of the Lifting package
wenzelm@63531
  1463
  because using of the bundle \<open>\<tau>.lifting\<close> together with the commands @{command
wenzelm@63531
  1464
  (HOL) lifting_forget} and @{command (HOL) lifting_update} is preferred for
wenzelm@63531
  1465
  normal usage.
wenzelm@63531
  1466
wenzelm@63531
  1467
  \<^descr> Integration with the BNF package @{cite "isabelle-datatypes"}: As already
wenzelm@63531
  1468
  mentioned, the theorems that are registered by the following attributes are
wenzelm@63531
  1469
  proved and registered automatically if the involved type is BNF without dead
wenzelm@63531
  1470
  variables: @{attribute (HOL) quot_map}, @{attribute (HOL) relator_eq_onp},
wenzelm@63531
  1471
  @{attribute (HOL) "relator_mono"}, @{attribute (HOL) "relator_distr"}. Also
wenzelm@63531
  1472
  the definition of a relator and predicator is provided automatically.
wenzelm@63531
  1473
  Moreover, if the BNF represents a datatype, simplification rules for a
wenzelm@63531
  1474
  predicator are again proved automatically.
wenzelm@58618
  1475
\<close>
wenzelm@58618
  1476
wenzelm@58618
  1477
wenzelm@60671
  1478
subsection \<open>Transfer package \label{sec:transfer}\<close>
wenzelm@60660
  1479
wenzelm@60660
  1480
text \<open>
wenzelm@60660
  1481
  \begin{matharray}{rcl}
wenzelm@61493
  1482
    @{method_def (HOL) "transfer"} & : & \<open>method\<close> \\
wenzelm@61493
  1483
    @{method_def (HOL) "transfer'"} & : & \<open>method\<close> \\
wenzelm@61493
  1484
    @{method_def (HOL) "transfer_prover"} & : & \<open>method\<close> \\
wenzelm@61493
  1485
    @{attribute_def (HOL) "Transfer.transferred"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1486
    @{attribute_def (HOL) "untransferred"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1487
    @{method_def (HOL) "transfer_start"} & : & \<open>method\<close> \\
wenzelm@61493
  1488
    @{method_def (HOL) "transfer_prover_start"} & : & \<open>method\<close> \\
wenzelm@61493
  1489
    @{method_def (HOL) "transfer_step"} & : & \<open>method\<close> \\
wenzelm@61493
  1490
    @{method_def (HOL) "transfer_end"} & : & \<open>method\<close> \\
wenzelm@61493
  1491
    @{method_def (HOL) "transfer_prover_end"} & : & \<open>method\<close> \\
wenzelm@61493
  1492
    @{attribute_def (HOL) "transfer_rule"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1493
    @{attribute_def (HOL) "transfer_domain_rule"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1494
    @{attribute_def (HOL) "relator_eq"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1495
    @{attribute_def (HOL) "relator_domain"} & : & \<open>attribute\<close> \\
wenzelm@60660
  1496
  \end{matharray}
wenzelm@60660
  1497
wenzelm@63531
  1498
  \<^descr> @{method (HOL) "transfer"} method replaces the current subgoal with a
wenzelm@63531
  1499
  logically equivalent one that uses different types and constants. The
wenzelm@60660
  1500
  replacement of types and constants is guided by the database of transfer
wenzelm@60660
  1501
  rules. Goals are generalized over all free variables by default; this is
wenzelm@60660
  1502
  necessary for variables whose types change, but can be overridden for
wenzelm@61493
  1503
  specific variables with e.g. \<open>transfer fixing: x y z\<close>.
wenzelm@60660
  1504
wenzelm@63531
  1505
  \<^descr> @{method (HOL) "transfer'"} is a variant of @{method (HOL) transfer} that
wenzelm@63531
  1506
  allows replacing a subgoal with one that is logically stronger (rather than
wenzelm@63531
  1507
  equivalent). For example, a subgoal involving equality on a quotient type
wenzelm@63531
  1508
  could be replaced with a subgoal involving equality (instead of the
wenzelm@63531
  1509
  corresponding equivalence relation) on the underlying raw type.
wenzelm@63531
  1510
wenzelm@63531
  1511
  \<^descr> @{method (HOL) "transfer_prover"} method assists with proving a transfer
wenzelm@63531
  1512
  rule for a new constant, provided the constant is defined in terms of other
wenzelm@63531
  1513
  constants that already have transfer rules. It should be applied after
wenzelm@63531
  1514
  unfolding the constant definitions.
wenzelm@60660
  1515
wenzelm@61439
  1516
  \<^descr> @{method (HOL) "transfer_start"}, @{method (HOL) "transfer_step"},
wenzelm@63531
  1517
  @{method (HOL) "transfer_end"}, @{method (HOL) "transfer_prover_start"} and
wenzelm@63531
  1518
  @{method (HOL) "transfer_prover_end"} methods are meant to be used for
wenzelm@63531
  1519
  debugging of @{method (HOL) "transfer"} and @{method (HOL)
wenzelm@63531
  1520
  "transfer_prover"}, which we can decompose as follows: @{method (HOL)
wenzelm@63531
  1521
  "transfer"} = (@{method (HOL) "transfer_start"}, @{method (HOL)
wenzelm@63531
  1522
  "transfer_step"}+, @{method (HOL) "transfer_end"}) and @{method (HOL)
wenzelm@63531
  1523
  "transfer_prover"} = (@{method (HOL) "transfer_prover_start"}, @{method
wenzelm@63531
  1524
  (HOL) "transfer_step"}+, @{method (HOL) "transfer_prover_end"}). For usage
wenzelm@63680
  1525
  examples see \<^file>\<open>~~/src/HOL/ex/Transfer_Debug.thy\<close>.
wenzelm@63531
  1526
wenzelm@63531
  1527
  \<^descr> @{attribute (HOL) "untransferred"} proves the same equivalent theorem as
wenzelm@63531
  1528
  @{method (HOL) "transfer"} internally does.
wenzelm@63531
  1529
wenzelm@63531
  1530
  \<^descr> @{attribute (HOL) Transfer.transferred} works in the opposite direction
wenzelm@63531
  1531
  than @{method (HOL) "transfer'"}. E.g.\ given the transfer relation \<open>ZN x n
wenzelm@63531
  1532
  \<equiv> (x = int n)\<close>, corresponding transfer rules and the theorem \<open>\<forall>x::int \<in>
wenzelm@63531
  1533
  {0..}. x < x + 1\<close>, the attribute would prove \<open>\<forall>n::nat. n < n + 1\<close>. The
wenzelm@63531
  1534
  attribute is still in experimental phase of development.
wenzelm@63531
  1535
wenzelm@63531
  1536
  \<^descr> @{attribute (HOL) "transfer_rule"} attribute maintains a collection of
wenzelm@63531
  1537
  transfer rules, which relate constants at two different types. Typical
wenzelm@60660
  1538
  transfer rules may relate different type instances of the same polymorphic
wenzelm@60660
  1539
  constant, or they may relate an operation on a raw type to a corresponding
wenzelm@60660
  1540
  operation on an abstract type (quotient or subtype). For example:
wenzelm@60660
  1541
wenzelm@61493
  1542
    \<open>((A ===> B) ===> list_all2 A ===> list_all2 B) map map\<close> \\
wenzelm@61493
  1543
    \<open>(cr_int ===> cr_int ===> cr_int) (\<lambda>(x,y) (u,v). (x+u, y+v)) plus\<close>
wenzelm@60660
  1544
wenzelm@60660
  1545
  Lemmas involving predicates on relations can also be registered using the
wenzelm@60660
  1546
  same attribute. For example:
wenzelm@60660
  1547
wenzelm@61493
  1548
    \<open>bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct\<close> \\
wenzelm@61493
  1549
    \<open>\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)\<close>
wenzelm@61493
  1550
wenzelm@63531
  1551
  Preservation of predicates on relations (\<open>bi_unique, bi_total, right_unique,
wenzelm@63531
  1552
  right_total, left_unique, left_total\<close>) with the respect to a relator is
wenzelm@63531
  1553
  proved automatically if the involved type is BNF @{cite
wenzelm@60660
  1554
  "isabelle-datatypes"} without dead variables.
wenzelm@60660
  1555
wenzelm@63531
  1556
  \<^descr> @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
wenzelm@63531
  1557
  of rules, which specify a domain of a transfer relation by a predicate.
wenzelm@63531
  1558
  E.g.\ given the transfer relation \<open>ZN x n \<equiv> (x = int n)\<close>, one can register
wenzelm@63531
  1559
  the following transfer domain rule: \<open>Domainp ZN = (\<lambda>x. x \<ge> 0)\<close>. The rules
wenzelm@63531
  1560
  allow the package to produce more readable transferred goals, e.g.\ when
wenzelm@63531
  1561
  quantifiers are transferred.
wenzelm@60660
  1562
wenzelm@61439
  1563
  \<^descr> @{attribute (HOL) relator_eq} attribute collects identity laws for
wenzelm@60660
  1564
  relators of various type constructors, e.g. @{term "rel_set (op =) = (op
wenzelm@60660
  1565
  =)"}. The @{method (HOL) transfer} method uses these lemmas to infer
wenzelm@60660
  1566
  transfer rules for non-polymorphic constants on the fly. For examples see
wenzelm@63680
  1567
  \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
wenzelm@63680
  1568
  is proved automatically if the involved type is BNF without dead variables.
wenzelm@60660
  1569
wenzelm@61439
  1570
  \<^descr> @{attribute_def (HOL) "relator_domain"} attribute collects rules
wenzelm@60670
  1571
  describing domains of relators by predicators. E.g.\ @{term "Domainp
wenzelm@60660
  1572
  (rel_set T) = (\<lambda>A. Ball A (Domainp T))"}. This allows the package to lift
wenzelm@63680
  1573
  transfer domain rules through type constructors. For examples see
wenzelm@63680
  1574
  \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
wenzelm@63680
  1575
  is proved automatically if the involved type is BNF without dead variables.
wenzelm@60660
  1576
wenzelm@60660
  1577
wenzelm@60660
  1578
  Theoretical background can be found in @{cite
wenzelm@60660
  1579
  "Huffman-Kuncar:2013:lifting_transfer"}.
wenzelm@60660
  1580
\<close>
wenzelm@60660
  1581
wenzelm@60660
  1582
wenzelm@60671
  1583
subsection \<open>Old-style definitions for quotient types \label{sec:old-quotient}\<close>
wenzelm@60671
  1584
wenzelm@60671
  1585
text \<open>
wenzelm@60671
  1586
  \begin{matharray}{rcl}
wenzelm@61493
  1587
    @{command_def (HOL) "quotient_definition"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close>\\
wenzelm@61493
  1588
    @{command_def (HOL) "print_quotmapsQ3"} & : & \<open>context \<rightarrow>\<close>\\
wenzelm@61493
  1589
    @{command_def (HOL) "print_quotientsQ3"} & : & \<open>context \<rightarrow>\<close>\\
wenzelm@61493
  1590
    @{command_def (HOL) "print_quotconsts"} & : & \<open>context \<rightarrow>\<close>\\
wenzelm@61493
  1591
    @{method_def (HOL) "lifting"} & : & \<open>method\<close> \\
wenzelm@61493
  1592
    @{method_def (HOL) "lifting_setup"} & : & \<open>method\<close> \\
wenzelm@61493
  1593
    @{method_def (HOL) "descending"} & : & \<open>method\<close> \\
wenzelm@61493
  1594
    @{method_def (HOL) "descending_setup"} & : & \<open>method\<close> \\
wenzelm@61493
  1595
    @{method_def (HOL) "partiality_descending"} & : & \<open>method\<close> \\
wenzelm@61493
  1596
    @{method_def (HOL) "partiality_descending_setup"} & : & \<open>method\<close> \\
wenzelm@61493
  1597
    @{method_def (HOL) "regularize"} & : & \<open>method\<close> \\
wenzelm@61493
  1598
    @{method_def (HOL) "injection"} & : & \<open>method\<close> \\
wenzelm@61493
  1599
    @{method_def (HOL) "cleaning"} & : & \<open>method\<close> \\
wenzelm@61493
  1600
    @{attribute_def (HOL) "quot_thm"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1601
    @{attribute_def (HOL) "quot_lifted"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1602
    @{attribute_def (HOL) "quot_respect"} & : & \<open>attribute\<close> \\
wenzelm@61493
  1603
    @{attribute_def (HOL) "quot_preserve"} & : & \<open>attribute\<close> \\
wenzelm@60671
  1604
  \end{matharray}
wenzelm@60671
  1605
wenzelm@60671
  1606
  @{rail \<open>
wenzelm@60671
  1607
    @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \<newline>
wenzelm@60671
  1608
    @{syntax term} 'is' @{syntax term}
wenzelm@60671
  1609
    ;
wenzelm@60671
  1610
    constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
wenzelm@60671
  1611
    ;
wenzelm@62969
  1612
    @@{method (HOL) lifting} @{syntax thms}?
wenzelm@60671
  1613
    ;
wenzelm@62969
  1614
    @@{method (HOL) lifting_setup} @{syntax thms}?
wenzelm@60671
  1615
  \<close>}
wenzelm@60671
  1616
wenzelm@63531
  1617
  \<^descr> @{command (HOL) "quotient_definition"} defines a constant on the quotient
wenzelm@63531
  1618
  type.
wenzelm@60671
  1619
wenzelm@61439
  1620
  \<^descr> @{command (HOL) "print_quotmapsQ3"} prints quotient map functions.
wenzelm@61439
  1621
wenzelm@61439
  1622
  \<^descr> @{command (HOL) "print_quotientsQ3"} prints quotients.
wenzelm@61439
  1623
wenzelm@61439
  1624
  \<^descr> @{command (HOL) "print_quotconsts"} prints quotient constants.
wenzelm@61439
  1625
wenzelm@63531
  1626
  \<^descr> @{method (HOL) "lifting"} and @{method (HOL) "lifting_setup"} methods
wenzelm@63531
  1627
  match the current goal with the given raw theorem to be lifted producing
wenzelm@63531
  1628
  three new subgoals: regularization, injection and cleaning subgoals.
wenzelm@63531
  1629
  @{method (HOL) "lifting"} tries to apply the heuristics for automatically
wenzelm@63531
  1630
  solving these three subgoals and leaves only the subgoals unsolved by the
wenzelm@63531
  1631
  heuristics to the user as opposed to @{method (HOL) "lifting_setup"} which
wenzelm@63531
  1632
  leaves the three subgoals unsolved.
wenzelm@63531
  1633
wenzelm@63531
  1634
  \<^descr> @{method (HOL) "descending"} and @{method (HOL) "descending_setup"} try to
wenzelm@63531
  1635
  guess a raw statement that would lift to the current subgoal. Such statement
wenzelm@63531
  1636
  is assumed as a new subgoal and @{method (HOL) "descending"} continues in
wenzelm@63531
  1637
  the same way as @{method (HOL) "lifting"} does. @{method (HOL) "descending"}
wenzelm@63531
  1638
  tries to solve the arising regularization, injection and cleaning subgoals
wenzelm@63531
  1639
  with the analogous method @{method (HOL) "descending_setup"} which leaves
wenzelm@63531
  1640
  the four unsolved subgoals.
wenzelm@63531
  1641
wenzelm@63531
  1642
  \<^descr> @{method (HOL) "partiality_descending"} finds the regularized theorem that
wenzelm@63531
  1643
  would lift to the current subgoal, lifts it and leaves as a subgoal. This
wenzelm@63531
  1644
  method can be used with partial equivalence quotients where the non
wenzelm@63531
  1645
  regularized statements would not be true. @{method (HOL)
wenzelm@60671
  1646
  "partiality_descending_setup"} leaves the injection and cleaning subgoals
wenzelm@60671
  1647
  unchanged.
wenzelm@60671
  1648
wenzelm@63531
  1649
  \<^descr> @{method (HOL) "regularize"} applies the regularization heuristics to the
wenzelm@63531
  1650
  current subgoal.
wenzelm@60671
  1651
wenzelm@61439
  1652
  \<^descr> @{method (HOL) "injection"} applies the injection heuristics to the
wenzelm@60671
  1653
  current goal using the stored quotient respectfulness theorems.
wenzelm@60671
  1654
wenzelm@63531
  1655
  \<^descr> @{method (HOL) "cleaning"} applies the injection cleaning heuristics to
wenzelm@63531
  1656
  the current subgoal using the stored quotient preservation theorems.
wenzelm@63531
  1657
wenzelm@63531
  1658
  \<^descr> @{attribute (HOL) quot_lifted} attribute tries to automatically transport
wenzelm@63531
  1659
  the theorem to the quotient type. The attribute uses all the defined
wenzelm@63531
  1660
  quotients types and quotient constants often producing undesired results or
wenzelm@63531
  1661
  theorems that cannot be lifted.
wenzelm@60671
  1662
wenzelm@61439
  1663
  \<^descr> @{attribute (HOL) quot_respect} and @{attribute (HOL) quot_preserve}
wenzelm@60671
  1664
  attributes declare a theorem as a respectfulness and preservation theorem
wenzelm@60671
  1665
  respectively. These are stored in the local theory store and used by the
wenzelm@60671
  1666
  @{method (HOL) "injection"} and @{method (HOL) "cleaning"} methods
wenzelm@60671
  1667
  respectively.
wenzelm@60671
  1668
wenzelm@63531
  1669
  \<^descr> @{attribute (HOL) quot_thm} declares that a certain theorem is a quotient
wenzelm@63531
  1670
  extension theorem. Quotient extension theorems allow for quotienting inside
wenzelm@63531
  1671
  container types. Given a polymorphic type that serves as a container, a map
wenzelm@63531
  1672
  function defined for this container using @{command (HOL) "functor"} and a
wenzelm@63531
  1673
  relation map defined for for the container type, the quotient extension
wenzelm@63531
  1674
  theorem should be @{term "Quotient3 R Abs Rep \<Longrightarrow> Quotient3 (rel_map R) (map
wenzelm@63531
  1675
  Abs) (map Rep)"}. Quotient extension theorems are stored in a database and
wenzelm@63531
  1676
  are used all the steps of lifting theorems.
wenzelm@60671
  1677
\<close>
wenzelm@60671
  1678
wenzelm@60671
  1679
wenzelm@60671
  1680
chapter \<open>Proof tools\<close>
wenzelm@60671
  1681
wenzelm@58618
  1682
section \<open>Proving propositions\<close>
wenzelm@58618
  1683
wenzelm@58618
  1684
text \<open>
wenzelm@63531
  1685
  In addition to the standard proof methods, a number of diagnosis tools
wenzelm@63531
  1686
  search for proofs and provide an Isar proof snippet on success. These tools
wenzelm@63531
  1687
  are available via the following commands.
blanchet@42215
  1688
blanchet@42215
  1689
  \begin{matharray}{rcl}
wenzelm@61493
  1690
    @{command_def (HOL) "solve_direct"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
wenzelm@61493
  1691
    @{command_def (HOL) "try"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
wenzelm@61493
  1692
    @{command_def (HOL) "try0"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
wenzelm@61493
  1693
    @{command_def (HOL) "sledgehammer"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
wenzelm@61493
  1694
    @{command_def (HOL) "sledgehammer_params"} & : & \<open>theory \<rightarrow> theory\<close>
blanchet@42215
  1695
  \end{matharray}
blanchet@42215
  1696
wenzelm@55112
  1697
  @{rail \<open>
blanchet@43040
  1698
    @@{command (HOL) try}
blanchet@43040
  1699
    ;
blanchet@43040
  1700
wenzelm@62969
  1701
    @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thms} ) + ) ?
wenzelm@42596
  1702
      @{syntax nat}?
blanchet@42215
  1703
    ;
blanchet@43040
  1704
wenzelm@42596
  1705
    @@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?
blanchet@42215
  1706
    ;
blanchet@42215
  1707
wenzelm@42596
  1708
    @@{command (HOL) sledgehammer_params} ( ( '[' args ']' ) ? )
blanchet@42215
  1709
    ;
wenzelm@42596
  1710
    args: ( @{syntax name} '=' value + ',' )
blanchet@42215
  1711
    ;
wenzelm@62969
  1712
    facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thms} ) + ) ? ')'
wenzelm@55112
  1713
  \<close>} % FIXME check args "value"
blanchet@42215
  1714
wenzelm@63531
  1715
  \<^descr> @{command (HOL) "solve_direct"} checks whether the current subgoals can be
wenzelm@63531
  1716
  solved directly by an existing theorem. Duplicate lemmas can be detected in
wenzelm@63531
  1717
  this way.
wenzelm@63531
  1718
wenzelm@63531
  1719
  \<^descr> @{command (HOL) "try0"} attempts to prove a subgoal using a combination of
wenzelm@63531
  1720
  standard proof methods (@{method auto}, @{method simp}, @{method blast},
wenzelm@63531
  1721
  etc.). Additional facts supplied via \<open>simp:\<close>, \<open>intro:\<close>, \<open>elim:\<close>, and \<open>dest:\<close>
wenzelm@63531
  1722
  are passed to the appropriate proof methods.
wenzelm@63531
  1723
wenzelm@63531
  1724
  \<^descr> @{command (HOL) "try"} attempts to prove or disprove a subgoal using a
wenzelm@63531
  1725
  combination of provers and disprovers (@{command (HOL) "solve_direct"},
wenzelm@63531
  1726
  @{command (HOL) "quickcheck"}, @{command (HOL) "try0"}, @{command (HOL)
wenzelm@63531
  1727
  "sledgehammer"}, @{command (HOL) "nitpick"}).
wenzelm@63531
  1728
wenzelm@63531
  1729
  \<^descr> @{command (HOL) "sledgehammer"} attempts to prove a subgoal using external
wenzelm@63531
  1730
  automatic provers (resolution provers and SMT solvers). See the Sledgehammer
wenzelm@63531
  1731
  manual @{cite "isabelle-sledgehammer"} for details.
blanchet@42215
  1732
wenzelm@61439
  1733
  \<^descr> @{command (HOL) "sledgehammer_params"} changes @{command (HOL)
wenzelm@46283
  1734
  "sledgehammer"} configuration options persistently.
wenzelm@58618
  1735
\<close>
wenzelm@58618
  1736
wenzelm@58618
  1737
wenzelm@58618
  1738
section \<open>Checking and refuting propositions\<close>
wenzelm@58618
  1739
wenzelm@58618
  1740
text \<open>
wenzelm@63531
  1741
  Identifying incorrect propositions usually involves evaluation of particular
wenzelm@63531
  1742
  assignments and systematic counterexample search. This is supported by the
wenzelm@63531
  1743
  following commands.
haftmann@31912
  1744
haftmann@31912
  1745
  \begin{matharray}{rcl}
wenzelm@61493
  1746
    @{command_def (HOL) "value"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
  1747
    @{command_def (HOL) "values"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
  1748
    @{command_def (HOL) "quickcheck"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
wenzelm@61493
  1749
    @{command_def (HOL) "nitpick"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
wenzelm@61493
  1750
    @{command_def (HOL) "quickcheck_params"} & : & \<open>theory \<rightarrow> theory\<close> \\
wenzelm@61493
  1751
    @{command_def (HOL) "nitpick_params"} & : & \<open>theory \<rightarrow> theory\<close> \\
wenzelm@61493
  1752
    @{command_def (HOL) "quickcheck_generator"} & : & \<open>theory \<rightarrow> theory\<close> \\
wenzelm@61493
  1753
    @{command_def (HOL) "find_unused_assms"} & : & \<open>context \<rightarrow>\<close>
haftmann@31912
  1754
  \end{matharray}
haftmann@31912
  1755
wenzelm@55112
  1756
  @{rail \<open>
haftmann@58100
  1757
    @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
haftmann@31912
  1758
    ;
haftmann@31912
  1759
bulwahn@45409
  1760
    @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
bulwahn@45409
  1761
    ;
bulwahn@45409
  1762
blanchet@49993
  1763
    (@@{command (HOL) quickcheck} | @@{command (HOL) nitpick})
wenzelm@42596
  1764
      ( '[' args ']' )? @{syntax nat}?
haftmann@31912
  1765
    ;
haftmann@31912
  1766
blanchet@49993
  1767
    (@@{command (HOL) quickcheck_params} |
wenzelm@42596
  1768
      @@{command (HOL) nitpick_params}) ( '[' args ']' )?
haftmann@31912
  1769
    ;
bulwahn@46592
  1770
wenzelm@62969
  1771
    @@{command (HOL) quickcheck_generator} @{syntax name} \<newline>
bulwahn@45943
  1772
      'operations:' ( @{syntax term} +)
bulwahn@45943
  1773
    ;
haftmann@31912
  1774
wenzelm@46628
  1775
    @@{command (HOL) find_unused_assms} @{syntax name}?
bulwahn@46592
  1776
    ;
wenzelm@42596
  1777
    modes: '(' (@{syntax name} +) ')'
haftmann@31912
  1778
    ;
wenzelm@42596
  1779
    args: ( @{syntax name} '=' value + ',' )
wenzelm@55112
  1780
  \<close>} % FIXME check "value"
haftmann@31912
  1781
wenzelm@63531
  1782
  \<^descr> @{command (HOL) "value"}~\<open>t\<close> evaluates and prints a term; optionally
wenzelm@63531
  1783
  \<open>modes\<close> can be specified, which are appended to the current print mode; see
wenzelm@63531
  1784
  \secref{sec:print-modes}. Evaluation is tried first using ML, falling back
wenzelm@63531
  1785
  to normalization by evaluation if this fails. Alternatively a specific
wenzelm@63531
  1786
  evaluator can be selected using square brackets; typical evaluators use the
wenzelm@63531
  1787
  current set of code equations to normalize and include \<open>simp\<close> for fully
wenzelm@63531
  1788
  symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
wenzelm@61477
  1789
  evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
haftmann@31912
  1790
wenzelm@63531
  1791
  \<^descr> @{command (HOL) "values"}~\<open>t\<close> enumerates a set comprehension by evaluation
wenzelm@63531
  1792
  and prints its values up to the given number of solutions; optionally
wenzelm@63531
  1793
  \<open>modes\<close> can be specified, which are appended to the current print mode; see
wenzelm@46283
  1794
  \secref{sec:print-modes}.
bulwahn@45409
  1795
wenzelm@63531
  1796
  \<^descr> @{command (HOL) "quickcheck"} tests the current goal for counterexamples
wenzelm@63531
  1797
  using a series of assignments for its free variables; by default the first
wenzelm@63531
  1798
  subgoal is tested, an other can be selected explicitly using an optional
wenzelm@63531
  1799
  goal index. Assignments can be chosen exhausting the search space up to a
wenzelm@63531
  1800
  given size, or using a fixed number of random assignments in the search
wenzelm@63531
  1801
  space, or exploring the search space symbolically using narrowing. By
wenzelm@63531
  1802
  default, quickcheck uses exhaustive testing. A number of configuration
wenzelm@46283
  1803
  options are supported for @{command (HOL) "quickcheck"}, notably:
haftmann@31912
  1804
wenzelm@63531
  1805
    \<^descr>[\<open>tester\<close>] specifies which testing approach to apply. There are three
wenzelm@63531
  1806
    testers, \<open>exhaustive\<close>, \<open>random\<close>, and \<open>narrowing\<close>. An unknown configuration
wenzelm@63531
  1807
    option is treated as an argument to tester, making \<open>tester =\<close> optional.
wenzelm@63531
  1808
    When multiple testers are given, these are applied in parallel. If no
wenzelm@63531
  1809
    tester is specified, quickcheck uses the testers that are set active,
wenzelm@63531
  1810
    i.e.\ configurations @{attribute quickcheck_exhaustive_active},
wenzelm@63531
  1811
    @{attribute quickcheck_random_active}, @{attribute
wenzelm@46283
  1812
    quickcheck_narrowing_active} are set to true.
wenzelm@46283
  1813
wenzelm@63531
  1814
    \<^descr>[\<open>size\<close>] specifies the maximum size of the search space for assignment
wenzelm@63531
  1815
    values.
wenzelm@63531
  1816
wenzelm@63531
  1817
    \<^descr>[\<open>genuine_only\<close>] sets quickcheck only to return genuine counterexample,
wenzelm@63531
  1818
    but not potentially spurious counterexamples due to underspecified
wenzelm@63531
  1819
    functions.
wenzelm@63531
  1820
wenzelm@63531
  1821
    \<^descr>[\<open>abort_potential\<close>] sets quickcheck to abort once it found a potentially
wenzelm@63531
  1822
    spurious counterexample and to not continue to search for a further
wenzelm@63531
  1823
    genuine counterexample. For this option to be effective, the
wenzelm@63531
  1824
    \<open>genuine_only\<close> option must be set to false.
wenzelm@63531
  1825
wenzelm@63531
  1826
    \<^descr>[\<open>eval\<close>] takes a term or a list of terms and evaluates these terms under
wenzelm@63531
  1827
    the variable assignment found by quickcheck. This option is currently only
wenzelm@63531
  1828
    supported by the default (exhaustive) tester.
wenzelm@63531
  1829
wenzelm@63531
  1830
    \<^descr>[\<open>iterations\<close>] sets how many sets of assignments are generated for each
wenzelm@63531
  1831
    particular size.
wenzelm@63531
  1832
wenzelm@63531
  1833
    \<^descr>[\<open>no_assms\<close>] specifies whether assumptions in structured proofs should be
wenzelm@63531
  1834
    ignored.
wenzelm@63531
  1835
wenzelm@63531
  1836
    \<^descr>[\<open>locale\<close>] specifies how to process conjectures in a locale context,
wenzelm@63531
  1837
    i.e.\ they can be interpreted or expanded. The option is a
wenzelm@63531
  1838
    whitespace-separated list of the two words \<open>interpret\<close> and \<open>expand\<close>. The
wenzelm@63531
  1839
    list determines the order they are employed. The default setting is to
wenzelm@63531
  1840
    first use interpretations and then test the expanded conjecture. The
wenzelm@63531
  1841
    option is only provided as attribute declaration, but not as parameter to
wenzelm@63531
  1842
    the command.
bulwahn@47349
  1843
wenzelm@61493
  1844
    \<^descr>[\<open>timeout\<close>] sets the time limit in seconds.
wenzelm@61493
  1845
wenzelm@63531
  1846
    \<^descr>[\<open>default_type\<close>] sets the type(s) generally used to instantiate type
wenzelm@63531
  1847
    variables.
wenzelm@63531
  1848
wenzelm@63531
  1849
    \<^descr>[\<open>report\<close>] if set quickcheck reports how many tests fulfilled the
wenzelm@63531
  1850
    preconditions.
wenzelm@63531
  1851
wenzelm@63531
  1852
    \<^descr>[\<open>use_subtype\<close>] if set quickcheck automatically lifts conjectures to
wenzelm@63531
  1853
    registered subtypes if possible, and tests the lifted conjecture.
wenzelm@63531
  1854
wenzelm@63531
  1855
    \<^descr>[\<open>quiet\<close>] if set quickcheck does not output anything while testing.
wenzelm@63531
  1856
wenzelm@63531
  1857
    \<^descr>[\<open>verbose\<close>] if set quickcheck informs about the current size and
wenzelm@63531
  1858
    cardinality while testing.
wenzelm@63531
  1859
wenzelm@63531
  1860
    \<^descr>[\<open>expect\<close>] can be used to check if the user's expectation was met
wenzelm@63531
  1861
    (\<open>no_expectation\<close>, \<open>no_counterexample\<close>, or \<open>counterexample\<close>).
bulwahn@40245
  1862
wenzelm@46283
  1863
  These option can be given within square brackets.
haftmann@31912
  1864
Andreas@56363
  1865
  Using the following type classes, the testers generate values and convert
Andreas@56363
  1866
  them back into Isabelle terms for displaying counterexamples.
wenzelm@61439
  1867
wenzelm@63531
  1868
    \<^descr>[\<open>exhaustive\<close>] The parameters of the type classes @{class exhaustive} and
wenzelm@63531
  1869
    @{class full_exhaustive} implement the testing. They take a testing
wenzelm@63531
  1870
    function as a parameter, which takes a value of type @{typ "'a"} and
wenzelm@63531
  1871
    optionally produces a counterexample, and a size parameter for the test
wenzelm@63531
  1872
    values. In @{class full_exhaustive}, the testing function parameter
wenzelm@63531
  1873
    additionally expects a lazy term reconstruction in the type @{typ
wenzelm@63531
  1874
    Code_Evaluation.term} of the tested value.
wenzelm@61459
  1875
wenzelm@61493
  1876
    The canonical implementation for \<open>exhaustive\<close> testers calls the given
wenzelm@63531
  1877
    testing function on all values up to the given size and stops as soon as a
wenzelm@63531
  1878
    counterexample is found.
wenzelm@63531
  1879
wenzelm@63531
  1880
    \<^descr>[\<open>random\<close>] The operation @{const Quickcheck_Random.random} of the type
wenzelm@63531
  1881
    class @{class random} generates a pseudo-random value of the given size
wenzelm@63531
  1882
    and a lazy term reconstruction of the value in the type @{typ
wenzelm@63531
  1883
    Code_Evaluation.term}. A pseudo-randomness generator is defined in theory
wenzelm@63531
  1884
    @{theory Random}.
wenzelm@63531
  1885
wenzelm@63531
  1886
    \<^descr>[\<open>narrowing\<close>] implements Haskell's Lazy Smallcheck @{cite
wenzelm@63531
  1887
    "runciman-naylor-lindblad"} using the type classes @{class narrowing} and
wenzelm@63531
  1888
    @{class partial_term_of}. Variables in the current goal are initially
wenzelm@63531
  1889
    represented as symbolic variables. If the execution of the goal tries to
wenzelm@63531
  1890
    evaluate one of them, the test engine replaces it with refinements
wenzelm@63531
  1891
    provided by @{const narrowing}. Narrowing views every value as a
wenzelm@63531
  1892
    sum-of-products which is expressed using the operations @{const
wenzelm@63531
  1893
    Quickcheck_Narrowing.cons} (embedding a value), @{const
wenzelm@63531
  1894
    Quickcheck_Narrowing.apply} (product) and @{const
wenzelm@63531
  1895
    Quickcheck_Narrowing.sum} (sum). The refinement should enable further
wenzelm@63531
  1896
    evaluation of the goal.
wenzelm@61459
  1897
wenzelm@61459
  1898
    For example, @{const narrowing} for the list type @{typ "'a :: narrowing list"}
wenzelm@61459
  1899
    can be recursively defined as
wenzelm@61459
  1900
    @{term "Quickcheck_Narrowing.sum (Quickcheck_Narrowing.cons [])
wenzelm@61459
  1901
              (Quickcheck_Narrowing.apply
Andreas@56363
  1902
                (Quickcheck_Narrowing.apply
wenzelm@61459
  1903
                  (Quickcheck_Narrowing.cons (op #))
wenzelm@61459
  1904
                  narrowing)
wenzelm@61459
  1905
                narrowing)"}.
wenzelm@63531
  1906
    If a symbolic variable of type @{typ "_ list"} is evaluated, it is
wenzelm@63531
  1907
    replaced by (i)~the empty list @{term "[]"} and (ii)~by a non-empty list
wenzelm@63531
  1908
    whose head and tail can then be recursively refined if needed.
wenzelm@63531
  1909
wenzelm@63531
  1910
    To reconstruct counterexamples, the operation @{const partial_term_of}
wenzelm@63531
  1911
    transforms \<open>narrowing\<close>'s deep representation of terms to the type @{typ
wenzelm@63531
  1912
    Code_Evaluation.term}. The deep representation models symbolic variables
wenzelm@63531
  1913
    as @{const Quickcheck_Narrowing.Narrowing_variable}, which are normally
wenzelm@63531
  1914
    converted to @{const Code_Evaluation.Free}, and refined values as @{term
wenzelm@63531
  1915
    "Quickcheck_Narrowing.Narrowing_constructor i args"}, where @{term "i ::
wenzelm@63531
  1916
    integer"} denotes the index in the sum of refinements. In the above
wenzelm@63531
  1917
    example for lists, @{term "0"} corresponds to @{term "[]"} and @{term "1"}
wenzelm@61459
  1918
    to @{term "op #"}.
wenzelm@61459
  1919
wenzelm@63531
  1920
    The command @{command (HOL) "code_datatype"} sets up @{const
wenzelm@63531
  1921
    partial_term_of} such that the @{term "i"}-th refinement is interpreted as
wenzelm@63531
  1922
    the @{term "i"}-th constructor, but it does not ensures consistency with
wenzelm@63531
  1923
    @{const narrowing}.
wenzelm@63531
  1924
wenzelm@63531
  1925
  \<^descr> @{command (HOL) "quickcheck_params"} changes @{command (HOL) "quickcheck"}
wenzelm@63531
  1926
  configuration options persistently.
wenzelm@63531
  1927
wenzelm@63531
  1928
  \<^descr> @{command (HOL) "quickcheck_generator"} creates random and exhaustive
wenzelm@63531
  1929
  value generators for a given type and operations. It generates values by
wenzelm@63531
  1930
  using the operations as if they were constructors of that type.
wenzelm@63531
  1931
wenzelm@63531
  1932
  \<^descr> @{command (HOL) "nitpick"} tests the current goal for counterexamples
wenzelm@63531
  1933
  using a reduction to first-order relational logic. See the Nitpick manual
wenzelm@63531
  1934
  @{cite "isabelle-nitpick"} for details.
wenzelm@63531
  1935
wenzelm@63531
  1936
  \<^descr> @{command (HOL) "nitpick_params"} changes @{command (HOL) "nitpick"}
wenzelm@63531
  1937
  configuration options persistently.
haftmann@31912
  1938
wenzelm@61439
  1939
  \<^descr> @{command (HOL) "find_unused_assms"} finds potentially superfluous
wenzelm@63531
  1940
  assumptions in theorems using quickcheck. It takes the theory name to be
wenzelm@63531
  1941
  checked for superfluous assumptions as optional argument. If not provided,
wenzelm@63531
  1942
  it checks the current theory. Options to the internal quickcheck invocations
wenzelm@63531
  1943
  can be changed with common configuration declarations.
wenzelm@58618
  1944
\<close>
wenzelm@58618
  1945
wenzelm@58618
  1946
wenzelm@60673
  1947
section \<open>Coercive subtyping\<close>
wenzelm@60673
  1948
wenzelm@60673
  1949
text \<open>
wenzelm@60673
  1950
  \begin{matharray}{rcl}
wenzelm@61493
  1951
    @{attribute_def (HOL) coercion} & : & \<open>attribute\<close> \\
wenzelm@61493
  1952
    @{attribute_def (HOL) coercion_delete} & : & \<open>attribute\<close> \\
wenzelm@61493
  1953
    @{attribute_def (HOL) coercion_enabled} & : & \<open>attribute\<close> \\
wenzelm@61493
  1954
    @{attribute_def (HOL) coercion_map} & : & \<open>attribute\<close> \\
wenzelm@61493
  1955
    @{attribute_def (HOL) coercion_args} & : & \<open>attribute\<close> \\
wenzelm@60673
  1956
  \end{matharray}
wenzelm@60673
  1957
wenzelm@63531
  1958
  Coercive subtyping allows the user to omit explicit type conversions, also
wenzelm@63531
  1959
  called \<^emph>\<open>coercions\<close>. Type inference will add them as necessary when parsing
wenzelm@63531
  1960
  a term. See @{cite "traytel-berghofer-nipkow-2011"} for details.
wenzelm@60673
  1961
wenzelm@60673
  1962
  @{rail \<open>
traytel@60837
  1963
    @@{attribute (HOL) coercion} (@{syntax term})
traytel@60837
  1964
    ;
traytel@60837
  1965
    @@{attribute (HOL) coercion_delete} (@{syntax term})
wenzelm@60673
  1966
    ;
traytel@60837
  1967
    @@{attribute (HOL) coercion_map} (@{syntax term})
traytel@60837
  1968
    ;
traytel@60837
  1969
    @@{attribute (HOL) coercion_args} (@{syntax const}) (('+' | '0' | '-')+)
wenzelm@60673
  1970
  \<close>}
wenzelm@60673
  1971
wenzelm@63531
  1972
  \<^descr> @{attribute (HOL) "coercion"}~\<open>f\<close> registers a new coercion function \<open>f ::
wenzelm@63531
  1973
  \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2\<close> where \<open>\<sigma>\<^sub>1\<close> and \<open>\<sigma>\<^sub>2\<close> are type constructors without arguments.
wenzelm@63531
  1974
  Coercions are composed by the inference algorithm if needed. Note that the
wenzelm@63531
  1975
  type inference algorithm is complete only if the registered coercions form a
wenzelm@63531
  1976
  lattice.
wenzelm@63531
  1977
wenzelm@63531
  1978
  \<^descr> @{attribute (HOL) "coercion_delete"}~\<open>f\<close> deletes a preceding declaration
wenzelm@63531
  1979
  (using @{attribute (HOL) "coercion"}) of the function \<open>f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2\<close> as a
wenzelm@63531
  1980
  coercion.
wenzelm@63531
  1981
wenzelm@63531
  1982
  \<^descr> @{attribute (HOL) "coercion_map"}~\<open>map\<close> registers a new map function to
wenzelm@63531
  1983
  lift coercions through type constructors. The function \<open>map\<close> must conform to
wenzelm@63531
  1984
  the following type pattern
wenzelm@60673
  1985
wenzelm@60673
  1986
  \begin{matharray}{lll}
wenzelm@61493
  1987
    \<open>map\<close> & \<open>::\<close> &
wenzelm@61493
  1988
      \<open>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\<close> \\
wenzelm@60673
  1989
  \end{matharray}
wenzelm@60673
  1990
wenzelm@63531
  1991
  where \<open>t\<close> is a type constructor and \<open>f\<^sub>i\<close> is of type \<open>\<alpha>\<^sub>i \<Rightarrow> \<beta>\<^sub>i\<close> or \<open>\<beta>\<^sub>i \<Rightarrow>
wenzelm@63531
  1992
  \<alpha>\<^sub>i\<close>. Registering a map function overwrites any existing map function for
wenzelm@63531
  1993
  this particular type constructor.
wenzelm@63531
  1994
wenzelm@63531
  1995
  \<^descr> @{attribute (HOL) "coercion_args"} can be used to disallow coercions to be
wenzelm@63531
  1996
  inserted in certain positions in a term. For example, given the constant \<open>c
wenzelm@63531
  1997
  :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2 \<Rightarrow> \<sigma>\<^sub>3 \<Rightarrow> \<sigma>\<^sub>4\<close> and the list of policies \<open>- + 0\<close> as arguments,
wenzelm@63531
  1998
  coercions will not be inserted in the first argument of \<open>c\<close> (policy \<open>-\<close>);
wenzelm@63531
  1999
  they may be inserted in the second argument (policy \<open>+\<close>) even if the
wenzelm@63531
  2000
  constant \<open>c\<close> itself is in a position where coercions are disallowed; the
wenzelm@63531
  2001
  third argument inherits the allowance of coercsion insertion from the
wenzelm@63531
  2002
  position of the constant \<open>c\<close> (policy \<open>0\<close>). The standard usage of policies is
wenzelm@63531
  2003
  the definition of syntatic constructs (usually extralogical, i.e., processed
wenzelm@63531
  2004
  and stripped during type inference), that should not be destroyed by the
wenzelm@63531
  2005
  insertion of coercions (see, for example, the setup for the case syntax in
wenzelm@63531
  2006
  @{theory Ctr_Sugar}).
wenzelm@63531
  2007
wenzelm@63531
  2008
  \<^descr> @{attribute (HOL) "coercion_enabled"} enables the coercion inference
wenzelm@63531
  2009
  algorithm.
wenzelm@60673
  2010
\<close>
wenzelm@60673
  2011
wenzelm@60673
  2012
wenzelm@60673
  2013
section \<open>Arithmetic proof support\<close>
wenzelm@60673
  2014
wenzelm@60673
  2015
text \<open>
wenzelm@60673
  2016
  \begin{matharray}{rcl}
wenzelm@61493
  2017
    @{method_def (HOL) arith} & : & \<open>method\<close> \\
wenzelm@61493
  2018
    @{attribute_def (HOL) arith} & : & \<open>attribute\<close> \\
wenzelm@61493
  2019
    @{attribute_def (HOL) arith_split} & : & \<open>attribute\<close> \\
wenzelm@60673
  2020
  \end{matharray}
wenzelm@60673
  2021
wenzelm@63531
  2022
  \<^descr> @{method (HOL) arith} decides linear arithmetic problems (on types \<open>nat\<close>,
wenzelm@63531
  2023
  \<open>int\<close>, \<open>real\<close>). Any current facts are inserted into the goal before running
wenzelm@63531
  2024
  the procedure.
wenzelm@63531
  2025
wenzelm@63531
  2026
  \<^descr> @{attribute (HOL) arith} declares facts that are supplied to the
wenzelm@63531
  2027
  arithmetic provers implicitly.
wenzelm@63531
  2028
wenzelm@63531
  2029
  \<^descr> @{attribute (HOL) arith_split} attribute declares case split rules to be
wenzelm@63531
  2030
  expanded before @{method (HOL) arith} is invoked.
wenzelm@63531
  2031
wenzelm@63531
  2032
wenzelm@63531
  2033
  Note that a simpler (but faster) arithmetic prover is already invoked by the
wenzelm@63531
  2034
  Simplifier.
wenzelm@60673
  2035
\<close>
wenzelm@60673
  2036
wenzelm@60673
  2037
wenzelm@60673
  2038
section \<open>Intuitionistic proof search\<close>
wenzelm@60673
  2039
wenzelm@60673
  2040
text \<open>
wenzelm@60673
  2041
  \begin{matharray}{rcl}
wenzelm@61493
  2042
    @{method_def (HOL) iprover} & : & \<open>method\<close> \\
wenzelm@60673
  2043
  \end{matharray}
wenzelm@60673
  2044
wenzelm@60673
  2045
  @{rail \<open>
wenzelm@60673
  2046
    @@{method (HOL) iprover} (@{syntax rulemod} *)
wenzelm@60673
  2047
  \<close>}
wenzelm@60673
  2048
wenzelm@63531
  2049
  \<^descr> @{method (HOL) iprover} performs intuitionistic proof search, depending on
wenzelm@63531
  2050
  specifically declared rules from the context, or given as explicit
wenzelm@63531
  2051
  arguments. Chained facts are inserted into the goal before commencing proof
wenzelm@63531
  2052
  search.
wenzelm@63531
  2053
wenzelm@63531
  2054
  Rules need to be classified as @{attribute (Pure) intro}, @{attribute (Pure)
wenzelm@63531
  2055
  elim}, or @{attribute (Pure) dest}; here the ``\<open>!\<close>'' indicator refers to
wenzelm@63531
  2056
  ``safe'' rules, which may be applied aggressively (without considering
wenzelm@63531
  2057
  back-tracking later). Rules declared with ``\<open>?\<close>'' are ignored in proof
wenzelm@63531
  2058
  search (the single-step @{method (Pure) rule} method still observes these).
wenzelm@63531
  2059
  An explicit weight annotation may be given as well; otherwise the number of
wenzelm@63531
  2060
  rule premises will be taken into account here.
wenzelm@60673
  2061
\<close>
wenzelm@60673
  2062
wenzelm@60673
  2063
wenzelm@60673
  2064
section \<open>Model Elimination and Resolution\<close>
wenzelm@60673
  2065
wenzelm@60673
  2066
text \<open>
wenzelm@60673
  2067
  \begin{matharray}{rcl}
wenzelm@61493
  2068
    @{method_def (HOL) "meson"} & : & \<open>method\<close> \\
wenzelm@61493
  2069
    @{method_def (HOL) "metis"} & : & \<open>method\<close> \\
wenzelm@60673
  2070
  \end{matharray}
wenzelm@60673
  2071
wenzelm@60673
  2072
  @{rail \<open>
wenzelm@62969
  2073
    @@{method (HOL) meson} @{syntax thms}?
wenzelm@60673
  2074
    ;
wenzelm@60673
  2075
    @@{method (HOL) metis}
wenzelm@60673
  2076
      ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
wenzelm@62969
  2077
      @{syntax thms}?
wenzelm@60673
  2078
  \<close>}
wenzelm@60673
  2079
wenzelm@63531
  2080
  \<^descr> @{method (HOL) meson} implements Loveland's model elimination procedure
wenzelm@63680
  2081
  @{cite "loveland-78"}. See \<^file>\<open>~~/src/HOL/ex/Meson_Test.thy\<close> for examples.
wenzelm@60673
  2082
wenzelm@61439
  2083
  \<^descr> @{method (HOL) metis} combines ordered resolution and ordered
wenzelm@63531
  2084
  paramodulation to find first-order (or mildly higher-order) proofs. The
wenzelm@63531
  2085
  first optional argument specifies a type encoding; see the Sledgehammer
wenzelm@63680
  2086
  manual @{cite "isabelle-sledgehammer"} for details. The directory
wenzelm@63680
  2087
  \<^dir>\<open>~~/src/HOL/Metis_Examples\<close> contains several small theories developed to a
wenzelm@63531
  2088
  large extent using @{method (HOL) metis}.
wenzelm@60673
  2089
\<close>
wenzelm@60673
  2090
wenzelm@60673
  2091
wenzelm@60673
  2092
section \<open>Algebraic reasoning via Gr\"obner bases\<close>
wenzelm@60673
  2093
wenzelm@60673
  2094
text \<open>
wenzelm@60673
  2095
  \begin{matharray}{rcl}
wenzelm@61493
  2096
    @{method_def (HOL) "algebra"} & : & \<open>method\<close> \\
wenzelm@61493
  2097
    @{attribute_def (HOL) algebra} & : & \<open>attribute\<close> \\
wenzelm@60673
  2098
  \end{matharray}
wenzelm@60673
  2099
wenzelm@60673
  2100
  @{rail \<open>
wenzelm@60673
  2101
    @@{method (HOL) algebra}
wenzelm@62969
  2102
      ('add' ':' @{syntax thms})?
wenzelm@62969
  2103
      ('del' ':' @{syntax thms})?
wenzelm@60673
  2104
    ;
wenzelm@60673
  2105
    @@{attribute (HOL) algebra} (() | 'add' | 'del')
wenzelm@60673
  2106
  \<close>}
wenzelm@60673
  2107
wenzelm@63531
  2108
  \<^descr> @{method (HOL) algebra} performs algebraic reasoning via Gr\"obner bases,
wenzelm@63531
  2109
  see also @{cite "Chaieb-Wenzel:2007"} and @{cite \<open>\S3.2\<close> "Chaieb-thesis"}.
wenzelm@63531
  2110
  The method handles deals with two main classes of problems:
wenzelm@60673
  2111
wenzelm@61459
  2112
    \<^enum> Universal problems over multivariate polynomials in a
wenzelm@61458
  2113
    (semi)-ring/field/idom; the capabilities of the method are augmented
wenzelm@63531
  2114
    according to properties of these structures. For this problem class the
wenzelm@63531
  2115
    method is only complete for algebraically closed fields, since the
wenzelm@63531
  2116
    underlying method is based on Hilbert's Nullstellensatz, where the
wenzelm@63531
  2117
    equivalence only holds for algebraically closed fields.
wenzelm@63531
  2118
wenzelm@63531
  2119
    The problems can contain equations \<open>p = 0\<close> or inequations \<open>q \<noteq> 0\<close> anywhere
wenzelm@63531
  2120
    within a universal problem statement.
wenzelm@63531
  2121
wenzelm@63531
  2122
    \<^enum> All-exists problems of the following restricted (but useful) form:
wenzelm@61458
  2123
wenzelm@61458
  2124
    @{text [display] "\<forall>x\<^sub>1 \<dots> x\<^sub>n.
wenzelm@61458
  2125
      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>
wenzelm@61458
  2126
      (\<exists>y\<^sub>1 \<dots> y\<^sub>k.
wenzelm@61458
  2127
        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>
wenzelm@61458
  2128
        \<dots> \<and>
wenzelm@61458
  2129
        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)"}
wenzelm@61458
  2130
wenzelm@63531
  2131
    Here \<open>e\<^sub>1, \<dots>, e\<^sub>n\<close> and the \<open>p\<^sub>i\<^sub>j\<close> are multivariate polynomials only in
wenzelm@63531
  2132
    the variables mentioned as arguments.
wenzelm@63531
  2133
wenzelm@63531
  2134
  The proof method is preceded by a simplification step, which may be modified
wenzelm@63531
  2135
  by using the form \<open>(algebra add: ths\<^sub>1 del: ths\<^sub>2)\<close>. This acts like
wenzelm@63531
  2136
  declarations for the Simplifier (\secref{sec:simplifier}) on a private
wenzelm@63531
  2137
  simpset for this tool.
wenzelm@63531
  2138
wenzelm@63531
  2139
  \<^descr> @{attribute algebra} (as attribute) manages the default collection of
wenzelm@63531
  2140
  pre-simplification rules of the above proof method.
wenzelm@60673
  2141
\<close>
wenzelm@60673
  2142
wenzelm@60673
  2143
wenzelm@60673
  2144
subsubsection \<open>Example\<close>
wenzelm@60673
  2145
wenzelm@63531
  2146
text \<open>
wenzelm@63531
  2147
  The subsequent example is from geometry: collinearity is invariant by
wenzelm@63531
  2148
  rotation.
wenzelm@63531
  2149
\<close>
wenzelm@60673
  2150
wenzelm@60673
  2151
(*<*)experiment begin(*>*)
wenzelm@60673
  2152
type_synonym point = "int \<times> int"
wenzelm@60673
  2153
wenzelm@60673
  2154
fun collinear :: "point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
wenzelm@60673
  2155
  "collinear (Ax, Ay) (Bx, By) (Cx, Cy) \<longleftrightarrow>
wenzelm@60673
  2156
    (Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx)"
wenzelm@60673
  2157
wenzelm@60673
  2158
lemma collinear_inv_rotation:
wenzelm@60673
  2159
  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"
wenzelm@60673
  2160
  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
wenzelm@60673
  2161
    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
wenzelm@60673
  2162
  using assms by (algebra add: collinear.simps)
wenzelm@60673
  2163
(*<*)end(*>*)
wenzelm@60673
  2164
wenzelm@60673
  2165
text \<open>
wenzelm@63680
  2166
  See also \<^file>\<open>~~/src/HOL/ex/Groebner_Examples.thy\<close>.
wenzelm@60673
  2167
\<close>
wenzelm@60673
  2168
wenzelm@60673
  2169
wenzelm@60673
  2170
section \<open>Coherent Logic\<close>
wenzelm@60673
  2171
wenzelm@60673
  2172
text \<open>
wenzelm@60673
  2173
  \begin{matharray}{rcl}
wenzelm@61493
  2174
    @{method_def (HOL) "coherent"} & : & \<open>method\<close> \\
wenzelm@60673
  2175
  \end{matharray}
wenzelm@60673
  2176
wenzelm@60673
  2177
  @{rail \<open>
wenzelm@62969
  2178
    @@{method (HOL) coherent} @{syntax thms}?
wenzelm@60673
  2179
  \<close>}
wenzelm@60673
  2180
wenzelm@63531
  2181
  \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> @{cite
wenzelm@63531
  2182
  "Bezem-Coquand:2005"}, which covers applications in confluence theory,
wenzelm@63680
  2183
  lattice theory and projective geometry. See \<^file>\<open>~~/src/HOL/ex/Coherent.thy\<close>
wenzelm@63680
  2184
  for some examples.
wenzelm@60673
  2185
\<close>
wenzelm@60673
  2186
wenzelm@60673
  2187
wenzelm@58618
  2188
section \<open>Unstructured case analysis and induction \label{sec:hol-induct-tac}\<close>
wenzelm@58618
  2189
wenzelm@58618
  2190
text \<open>
wenzelm@63531
  2191
  The following tools of Isabelle/HOL support cases analysis and induction in
wenzelm@63531
  2192
  unstructured tactic scripts; see also \secref{sec:cases-induct} for proper
wenzelm@63531
  2193
  Isar versions of similar ideas.
wenzelm@26849
  2194
wenzelm@26849
  2195
  \begin{matharray}{rcl}
wenzelm@61493
  2196
    @{method_def (HOL) case_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
  2197
    @{method_def (HOL) induct_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
  2198
    @{method_def (HOL) ind_cases}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
  2199
    @{command_def (HOL) "inductive_cases"}\<open>\<^sup>*\<close> & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@26849
  2200
  \end{matharray}
wenzelm@26849
  2201
wenzelm@55112
  2202
  @{rail \<open>
wenzelm@42705
  2203
    @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?
wenzelm@26849
  2204
    ;
wenzelm@42705
  2205
    @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
wenzelm@26849
  2206
    ;
wenzelm@59845
  2207
    @@{method (HOL) ind_cases} (@{syntax prop}+) @{syntax for_fixes}
wenzelm@26849
  2208
    ;
wenzelm@42596
  2209
    @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
wenzelm@26849
  2210
    ;
wenzelm@62969
  2211
    rule: 'rule' ':' @{syntax thm}
wenzelm@55112
  2212
  \<close>}
wenzelm@26849
  2213
wenzelm@63531
  2214
  \<^descr> @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit to reason
wenzelm@63531
  2215
  about inductive types. Rules are selected according to the declarations by
wenzelm@63531
  2216
  the @{attribute cases} and @{attribute induct} attributes, cf.\
wenzelm@63531
  2217
  \secref{sec:cases-induct}. The @{command (HOL) datatype} package already
wenzelm@63531
  2218
  takes care of this.
wenzelm@27123
  2219
wenzelm@27123
  2220
  These unstructured tactics feature both goal addressing and dynamic
wenzelm@63531
  2221
  instantiation. Note that named rule cases are \<^emph>\<open>not\<close> provided as would be by
wenzelm@63531
  2222
  the proper @{method cases} and @{method induct} proof methods (see
wenzelm@63531
  2223
  \secref{sec:cases-induct}). Unlike the @{method induct} method, @{method
wenzelm@63531
  2224
  induct_tac} does not handle structured rule statements, only the compact
wenzelm@63531
  2225
  object-logic conclusion of the subgoal being addressed.
wenzelm@63531
  2226
wenzelm@63531
  2227
  \<^descr> @{method (HOL) ind_cases} and @{command (HOL) "inductive_cases"} provide
wenzelm@63531
  2228
  an interface to the internal @{ML_text mk_cases} operation. Rules are
wenzelm@63531
  2229
  simplified in an unrestricted forward manner.
wenzelm@63531
  2230
wenzelm@63531
  2231
  While @{method (HOL) ind_cases} is a proof method to apply the result
wenzelm@63531
  2232
  immediately as elimination rules, @{command (HOL) "inductive_cases"}
wenzelm@63531
  2233
  provides case split theorems at the theory level for later use. The
wenzelm@63531
  2234
  @{keyword "for"} argument of the @{method (HOL) ind_cases} method allows to
wenzelm@63531
  2235
  specify a list of variables that should be generalized before applying the
wenzelm@63531
  2236
  resulting rule.
wenzelm@58618
  2237
\<close>
wenzelm@58618
  2238
wenzelm@58618
  2239
wenzelm@60657
  2240
section \<open>Adhoc tuples\<close>
wenzelm@60657
  2241
wenzelm@60657
  2242
text \<open>
wenzelm@60657
  2243
  \begin{matharray}{rcl}
wenzelm@61493
  2244
    @{attribute_def (HOL) split_format}\<open>\<^sup>*\<close> & : & \<open>attribute\<close> \\
wenzelm@60657
  2245
  \end{matharray}
wenzelm@60657
  2246
wenzelm@60657
  2247
  @{rail \<open>
wenzelm@60657
  2248
    @@{attribute (HOL) split_format} ('(' 'complete' ')')?
wenzelm@60657
  2249
  \<close>}
wenzelm@60657
  2250
wenzelm@63531
  2251
  \<^descr> @{attribute (HOL) split_format}\ \<open>(complete)\<close> causes arguments in function
wenzelm@63531
  2252
  applications to be represented canonically according to their tuple type
wenzelm@63531
  2253
  structure.
wenzelm@60657
  2254
wenzelm@60657
  2255
  Note that this operation tends to invent funny names for new local
wenzelm@60657
  2256
  parameters introduced.
wenzelm@60657
  2257
\<close>
wenzelm@60657
  2258
wenzelm@60657
  2259
wenzelm@58618
  2260
chapter \<open>Executable code\<close>
wenzelm@58618
  2261
wenzelm@63531
  2262
text \<open>
wenzelm@63531
  2263
  For validation purposes, it is often useful to \<^emph>\<open>execute\<close> specifications. In
wenzelm@63531
  2264
  principle, execution could be simulated by Isabelle's inference kernel, i.e.
wenzelm@63531
  2265
  by a combination of resolution and simplification. Unfortunately, this
wenzelm@63531
  2266
  approach is rather inefficient. A more efficient way of executing
wenzelm@63531
  2267
  specifications is to translate them into a functional programming language
wenzelm@63531
  2268
  such as ML.
wenzelm@60675
  2269
wenzelm@60675
  2270
  Isabelle provides a generic framework to support code generation from
wenzelm@60675
  2271
  executable specifications. Isabelle/HOL instantiates these mechanisms in a
wenzelm@60675
  2272
  way that is amenable to end-user applications. Code can be generated for
wenzelm@63531
  2273
  functional programs (including overloading using type classes) targeting SML
wenzelm@63531
  2274
  @{cite SML}, OCaml @{cite OCaml}, Haskell @{cite "haskell-revised-report"}
wenzelm@63531
  2275
  and Scala @{cite "scala-overview-tech-report"}. Conceptually, code
wenzelm@63531
  2276
  generation is split up in three steps: \<^emph>\<open>selection\<close> of code theorems,
wenzelm@63531
  2277
  \<^emph>\<open>translation\<close> into an abstract executable view and \<^emph>\<open>serialization\<close> to a
wenzelm@63531
  2278
  specific \<^emph>\<open>target language\<close>. Inductive specifications can be executed using
wenzelm@63531
  2279
  the predicate compiler which operates within HOL. See @{cite
wenzelm@63531
  2280
  "isabelle-codegen"} for an introduction.
haftmann@37422
  2281
haftmann@37422
  2282
  \begin{matharray}{rcl}
wenzelm@61493
  2283
    @{command_def (HOL) "export_code"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
  2284
    @{attribute_def (HOL) code} & : & \<open>attribute\<close> \\
wenzelm@61493
  2285
    @{command_def (HOL) "code_datatype"} & : & \<open>theory \<rightarrow> theory\<close> \\
wenzelm@61493
  2286
    @{command_def (HOL) "print_codesetup"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
  2287
    @{attribute_def (HOL) code_unfold} & : & \<open>attribute\<close> \\
wenzelm@61493
  2288
    @{attribute_def (HOL) code_post} & : & \<open>attribute\<close> \\
wenzelm@61493
  2289
    @{attribute_def (HOL) code_abbrev} & : & \<open>attribute\<close> \\
wenzelm@61493
  2290
    @{command_def (HOL) "print_codeproc"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
  2291
    @{command_def (HOL) "code_thms"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
  2292
    @{command_def (HOL) "code_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
  2293
    @{command_def (HOL) "code_reserved"} & : & \<open>theory \<rightarrow> theory\<close> \\
wenzelm@61493
  2294
    @{command_def (HOL) "code_printing"} & : & \<open>theory \<rightarrow> theory\<close> \\
wenzelm@61493
  2295
    @{command_def (HOL) "code_identifier"} & : & \<open>theory \<rightarrow> theory\<close> \\
wenzelm@61493
  2296
    @{command_def (HOL) "code_monad"} & : & \<open>theory \<rightarrow> theory\<close> \\
wenzelm@61493
  2297
    @{command_def (HOL) "code_reflect"} & : & \<open>theory \<rightarrow> theory\<close> \\
wenzelm@61493
  2298
    @{command_def (HOL) "code_pred"} & : & \<open>theory \<rightarrow> proof(prove)\<close>
haftmann@37422
  2299
  \end{matharray}
haftmann@37422
  2300
wenzelm@55112
  2301
  @{rail \<open>
haftmann@55686
  2302
    @@{command (HOL) export_code} ( @'open' ) ? ( constexpr + ) \<newline>
wenzelm@55029
  2303
       ( ( @'in' target ( @'module_name' @{syntax string} ) ? \<newline>
haftmann@52435
  2304
        ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
haftmann@37422
  2305
    ;
wenzelm@42596
  2306
    const: @{syntax term}
haftmann@37422
  2307
    ;
haftmann@40711
  2308
    constexpr: ( const | 'name._' | '_' )
haftmann@37422
  2309
    ;
wenzelm@62969
  2310
    typeconstructor: @{syntax name}
haftmann@37422
  2311
    ;
wenzelm@62969
  2312
    class: @{syntax name}
haftmann@37422
  2313
    ;
haftmann@52378
  2314
    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
haftmann@37422
  2315
    ;
haftmann@54890
  2316
    @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract'
haftmann@54890
  2317
      | 'drop:' ( const + ) | 'abort:' ( const + ) )?
haftmann@37422
  2318
    ;
wenzelm@42596
  2319
    @@{command (HOL) code_datatype} ( const + )
haftmann@37422
  2320
    ;
bulwahn@45232
  2321
    @@{attribute (HOL) code_unfold} ( 'del' ) ?
haftmann@37422
  2322
    ;
wenzelm@42596
  2323
    @@{attribute (HOL) code_post} ( 'del' ) ?
haftmann@37422
  2324
    ;
haftmann@46028
  2325
    @@{attribute (HOL) code_abbrev}
bulwahn@45232
  2326
    ;
wenzelm@42596
  2327
    @@{command (HOL) code_thms} ( constexpr + ) ?
haftmann@37422
  2328
    ;
wenzelm@42596
  2329
    @@{command (HOL) code_deps} ( constexpr + ) ?
haftmann@37422
  2330
    ;
haftmann@52378
  2331
    @@{command (HOL) code_reserved} target ( @{syntax string} + )
haftmann@52378
  2332
    ;
haftmann@52378
  2333
    symbol_const: ( @'constant' const )
haftmann@52378
  2334
    ;
haftmann@52378
  2335
    symbol_typeconstructor: ( @'type_constructor' typeconstructor )
haftmann@52378
  2336
    ;
haftmann@52378
  2337
    symbol_class: ( @'type_class' class )
haftmann@52378
  2338
    ;
haftmann@52378
  2339
    symbol_class_relation: ( @'class_relation' class ( '<' | '\<subseteq>' ) class )
haftmann@52378
  2340
    ;
haftmann@52378
  2341
    symbol_class_instance: ( @'class_instance' typeconstructor @'::' class )
haftmann@52378
  2342
    ;
haftmann@52378
  2343
    symbol_module: ( @'code_module' name )
haftmann@52378
  2344
    ;
haftmann@52378
  2345
    syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
haftmann@52378
  2346
    ;
wenzelm@55029
  2347
    printing_const: symbol_const ( '\<rightharpoonup>' | '=>' ) \<newline>
haftmann@52378
  2348
      ( '(' target ')' syntax ? + @'and' )
haftmann@52378
  2349
    ;
wenzelm@55029
  2350
    printing_typeconstructor: symbol_typeconstructor ( '\<rightharpoonup>' | '=>' ) \<newline>
haftmann@52378
  2351
      ( '(' target ')' syntax ? + @'and' )
haftmann@52378
  2352
    ;
wenzelm@55029
  2353
    printing_class: symbol_class ( '\<rightharpoonup>' | '=>' ) \<newline>
haftmann@52378
  2354
      ( '(' target ')' @{syntax string} ? + @'and' )
haftmann@52378
  2355
    ;
wenzelm@55029
  2356
    printing_class_relation: symbol_class_relation ( '\<rightharpoonup>' | '=>' ) \<newline>
haftmann@52378
  2357
      ( '(' target ')' @{syntax string} ? + @'and' )
haftmann@52378
  2358
    ;
wenzelm@55029
  2359
    printing_class_instance: symbol_class_instance ( '\<rightharpoonup>' | '=>' ) \<newline>
haftmann@52378
  2360
      ( '(' target ')' '-' ? + @'and' )
haftmann@52378
  2361
    ;
wenzelm@55029
  2362
    printing_module: symbol_module ( '\<rightharpoonup>' | '=>' ) \<newline>
haftmann@52378
  2363
      ( '(' target ')' ( @{syntax string} ( @'attach' ( const + ) ) ? ) ? + @'and' )
haftmann@52378
  2364
    ;
haftmann@52378
  2365
    @@{command (HOL) code_printing} ( ( printing_const | printing_typeconstructor
haftmann@52378
  2366
      | printing_class | printing_class_relation | printing_class_instance
haftmann@52378
  2367
      | printing_module ) + '|' )
haftmann@52378
  2368
    ;
haftmann@52378
  2369
    @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
haftmann@52378
  2370
      | symbol_class | symbol_class_relation | symbol_class_instance
wenzelm@55029
  2371
      | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \<newline>
haftmann@52378
  2372
      ( '(' target ')' @{syntax string} ? + @'and' ) + '|' )
haftmann@52378
  2373
    ;
wenzelm@42596
  2374
    @@{command (HOL) code_monad} const const target
haftmann@37422
  2375
    ;
wenzelm@55029
  2376
    @@{command (HOL) code_reflect} @{syntax string} \<newline>
wenzelm@55029
  2377
      ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \<newline>
wenzelm@42596
  2378
      ( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?
haftmann@37422
  2379
    ;
wenzelm@55029
  2380
    @@{command (HOL) code_pred} \<newline> ('(' @'modes' ':' modedecl ')')? \<newline> const
bulwahn@45408
  2381
    ;
wenzelm@55029
  2382
    modedecl: (modes | ((const ':' modes) \<newline>
wenzelm@55029
  2383
        (@'and' ((const ':' modes @'and') +))?))
bulwahn@45408
  2384
    ;
bulwahn@45408
  2385
    modes: mode @'as' const
wenzelm@55112
  2386
  \<close>}
haftmann@37422
  2387
wenzelm@61439
  2388
  \<^descr> @{command (HOL) "export_code"} generates code for a given list of
wenzelm@60675
  2389
  constants in the specified target language(s). If no serialization
wenzelm@60675
  2390
  instruction is given, only abstract code is generated internally.
wenzelm@60675
  2391
wenzelm@60675
  2392
  Constants may be specified by giving them literally, referring to all
wenzelm@63531
  2393
  executable constants within a certain theory by giving \<open>name._\<close>, or
wenzelm@63531
  2394
  referring to \<^emph>\<open>all\<close> executable constants currently available by giving \<open>_\<close>.
wenzelm@60675
  2395
wenzelm@60675
  2396
  By default, exported identifiers are minimized per module. This can be
wenzelm@60675
  2397
  suppressed by prepending @{keyword "open"} before the list of constants.
wenzelm@60675
  2398
wenzelm@63531
  2399
  By default, for each involved theory one corresponding name space module is
wenzelm@63531
  2400
  generated. Alternatively, a module name may be specified after the @{keyword
wenzelm@63531
  2401
  "module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this module.
wenzelm@63531
  2402
wenzelm@63531
  2403
  For \<^emph>\<open>SML\<close>, \<^emph>\<open>OCaml\<close> and \<^emph>\<open>Scala\<close> the file specification refers to a single
wenzelm@63531
  2404
  file; for \<^emph>\<open>Haskell\<close>, it refers to a whole directory, where code is
wenzelm@63531
  2405
  generated in multiple files reflecting the module hierarchy. Omitting the
wenzelm@63531
  2406
  file specification denotes standard output.
wenzelm@60675
  2407
wenzelm@60675
  2408
  Serializers take an optional list of arguments in parentheses. For
wenzelm@61503
  2409
  \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>'' argument;
wenzelm@61503
  2410
  ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause to each
wenzelm@61503
  2411
  appropriate datatype declaration.
wenzelm@60675
  2412
wenzelm@61439
  2413
  \<^descr> @{attribute (HOL) code} declare code equations for code generation.
wenzelm@63531
  2414
  Variant \<open>code equation\<close> declares a conventional equation as code equation.
wenzelm@63531
  2415
  Variants \<open>code abstype\<close> and \<open>code abstract\<close> declare abstract datatype
wenzelm@63531
  2416
  certificates or code equations on abstract datatype representations
wenzelm@63531
  2417
  respectively. Vanilla \<open>code\<close> falls back to \<open>code equation\<close> or \<open>code abstype\<close>
wenzelm@63531
  2418
  depending on the syntactic shape of the underlying equation. Variant \<open>code
wenzelm@63531
  2419
  del\<close> deselects a code equation for code generation.
wenzelm@63531
  2420
wenzelm@63531
  2421
  Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constant as arguments
wenzelm@63531
  2422
  and drop all code equations declared for them. In the case of {text abort},
wenzelm@63531
  2423
  these constants then are are not required to have a definition by means of
wenzelm@63531
  2424
  code equations; if needed these are implemented by program abort (exception)
wenzelm@63531
  2425
  instead.
wenzelm@60675
  2426
wenzelm@60675
  2427
  Usually packages introducing code equations provide a reasonable default
wenzelm@60675
  2428
  setup for selection.
wenzelm@60675
  2429
wenzelm@63531
  2430
  \<^descr> @{command (HOL) "code_datatype"} specifies a constructor set for a logical
wenzelm@63531
  2431
  type.
wenzelm@63531
  2432
wenzelm@63531
  2433
  \<^descr> @{command (HOL) "print_codesetup"} gives an overview on selected code
wenzelm@63531
  2434
  equations and code generator datatypes.
wenzelm@63531
  2435
wenzelm@63531
  2436
  \<^descr> @{attribute (HOL) code_unfold} declares (or with option ``\<open>del\<close>'' removes)
wenzelm@63531
  2437
  theorems which during preprocessing are applied as rewrite rules to any code
wenzelm@60675
  2438
  equation or evaluation input.
haftmann@46028
  2439
wenzelm@63531
  2440
  \<^descr> @{attribute (HOL) code_post} declares (or with option ``\<open>del\<close>'' removes)
wenzelm@63531
  2441
  theorems which are applied as rewrite rules to any result of an evaluation.
wenzelm@63531
  2442
wenzelm@63531
  2443
  \<^descr> @{attribute (HOL) code_abbrev} declares (or with option ``\<open>del\<close>'' removes)
wenzelm@63531
  2444
  equations which are applied as rewrite rules to any result of an evaluation
wenzelm@63531
  2445
  and symmetrically during preprocessing to any code equation or evaluation
wenzelm@63531
  2446
  input.
wenzelm@63531
  2447
wenzelm@63531
  2448
  \<^descr> @{command (HOL) "print_codeproc"} prints the setup of the code generator
wenzelm@63531
  2449
  preprocessor.
wenzelm@63531
  2450
wenzelm@63531
  2451
  \<^descr> @{command (HOL) "code_thms"} prints a list of theorems representing the
wenzelm@63531
  2452
  corresponding program containing all given constants after preprocessing.
wenzelm@60675
  2453
wenzelm@61439
  2454
  \<^descr> @{command (HOL) "code_deps"} visualizes dependencies of theorems
wenzelm@63531
  2455
  representing the corresponding program containing all given constants after
wenzelm@63531
  2456
  preprocessing.
wenzelm@63531
  2457
wenzelm@63531
  2458
  \<^descr> @{command (HOL) "code_reserved"} declares a list of names as reserved for
wenzelm@63531
  2459
  a given target, preventing it to be shadowed by any generated code.
haftmann@37422
  2460
wenzelm@61439
  2461
  \<^descr> @{command (HOL) "code_printing"} associates a series of symbols
wenzelm@60675
  2462
  (constants, type constructors, classes, class relations, instances, module
wenzelm@63531
  2463
  names) with target-specific serializations; omitting a serialization deletes
wenzelm@63531
  2464
  an existing serialization.
wenzelm@63531
  2465