src/Doc/Tutorial/Inductive/Advanced.thy
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 48985 5386df44a037
child 56059 2390391584c2
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48895
4cd4ef1ef4a4 prefer ML_file over old uses;
wenzelm
parents: 43564
diff changeset
     1
(*<*)theory Advanced imports Even begin
4cd4ef1ef4a4 prefer ML_file over old uses;
wenzelm
parents: 43564
diff changeset
     2
ML_file "../../antiquote_setup.ML"
4cd4ef1ef4a4 prefer ML_file over old uses;
wenzelm
parents: 43564
diff changeset
     3
setup Antiquote_Setup.setup
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 39795
diff changeset
     4
(*>*)
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
     5
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
     6
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
     7
The premises of introduction rules may contain universal quantifiers and
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
     8
monotone functions.  A universal quantifier lets the rule 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
     9
refer to any number of instances of 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    10
the inductively defined set.  A monotone function lets the rule refer
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    11
to existing constructions (such as ``list of'') over the inductively defined
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    12
set.  The examples below show how to use the additional expressiveness
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    13
and how to reason from the resulting definitions.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    14
*}
10426
469f19c4bf97 rule inversion
nipkow
parents: 10370
diff changeset
    15
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    16
subsection{* Universal Quantifiers in Introduction Rules \label{sec:gterm-datatype} *}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    17
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    18
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    19
\index{ground terms example|(}%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    20
\index{quantifiers!and inductive definitions|(}%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    21
As a running example, this section develops the theory of \textbf{ground
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    22
terms}: terms constructed from constant and function 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    23
symbols but not variables. To simplify matters further, we regard a
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    24
constant as a function applied to the null argument  list.  Let us declare a
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    25
datatype @{text gterm} for the type of ground  terms. It is a type constructor
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    26
whose argument is a type of  function symbols. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    27
*}
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
    28
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
    29
datatype 'f gterm = Apply 'f "'f gterm list"
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
    30
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    31
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    32
To try it out, we declare a datatype of some integer operations: 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    33
integer constants, the unary minus operator and the addition 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    34
operator.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    35
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    36
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    37
datatype integer_op = Number int | UnaryMinus | Plus
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    38
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    39
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    40
Now the type @{typ "integer_op gterm"} denotes the ground 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    41
terms built over those symbols.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    42
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    43
The type constructor @{text gterm} can be generalized to a function 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    44
over sets.  It returns 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    45
the set of ground terms that can be formed over a set @{text F} of function symbols. For
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    46
example,  we could consider the set of ground terms formed from the finite 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    47
set @{text "{Number 2, UnaryMinus, Plus}"}.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    48
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    49
This concept is inductive. If we have a list @{text args} of ground terms 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    50
over~@{text F} and a function symbol @{text f} in @{text F}, then we 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    51
can apply @{text f} to @{text args} to obtain another ground term. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    52
The only difficulty is that the argument list may be of any length. Hitherto, 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    53
each rule in an inductive definition referred to the inductively 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    54
defined set a fixed number of times, typically once or twice. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    55
A universal quantifier in the premise of the introduction rule 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    56
expresses that every element of @{text args} belongs
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    57
to our inductively defined set: is a ground term 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    58
over~@{text F}.  The function @{term set} denotes the set of elements in a given 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    59
list. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    60
*}
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
    61
23733
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    62
inductive_set
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    63
  gterms :: "'f set \<Rightarrow> 'f gterm set"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    64
  for F :: "'f set"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    65
where
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
    66
step[intro!]: "\<lbrakk>\<forall>t \<in> set args. t \<in> gterms F;  f \<in> F\<rbrakk>
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
    67
               \<Longrightarrow> (Apply f args) \<in> gterms F"
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
    68
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    69
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    70
To demonstrate a proof from this definition, let us 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    71
show that the function @{term gterms}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    72
is \textbf{monotone}.  We shall need this concept shortly.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    73
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    74
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    75
lemma gterms_mono: "F\<subseteq>G \<Longrightarrow> gterms F \<subseteq> gterms G"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    76
apply clarify
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    77
apply (erule gterms.induct)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    78
apply blast
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    79
done
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    80
(*<*)
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
    81
lemma gterms_mono: "F\<subseteq>G \<Longrightarrow> gterms F \<subseteq> gterms G"
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
    82
apply clarify
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
    83
apply (erule gterms.induct)
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    84
(*>*)
10882
ca41ba5fb8e2 updated for new version of advanced-examples.tex
paulson
parents: 10468
diff changeset
    85
txt{*
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    86
Intuitively, this theorem says that
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    87
enlarging the set of function symbols enlarges the set of ground 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    88
terms. The proof is a trivial rule induction.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    89
First we use the @{text clarify} method to assume the existence of an element of
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    90
@{term "gterms F"}.  (We could have used @{text "intro subsetI"}.)  We then
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    91
apply rule induction. Here is the resulting subgoal:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    92
@{subgoals[display,indent=0]}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    93
The assumptions state that @{text f} belongs 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    94
to~@{text F}, which is included in~@{text G}, and that every element of the list @{text args} is
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    95
a ground term over~@{text G}.  The @{text blast} method finds this chain of reasoning easily.  
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
    96
*}
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    97
(*<*)oops(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    98
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
    99
\begin{warn}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   100
Why do we call this function @{text gterms} instead 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   101
of @{text gterm}?  A constant may have the same name as a type.  However,
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   102
name  clashes could arise in the theorems that Isabelle generates. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   103
Our choice of names keeps @{text gterms.induct} separate from 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   104
@{text gterm.induct}.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   105
\end{warn}
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   106
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   107
Call a term \textbf{well-formed} if each symbol occurring in it is applied
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   108
to the correct number of arguments.  (This number is called the symbol's
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   109
\textbf{arity}.)  We can express well-formedness by
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   110
generalizing the inductive definition of
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   111
\isa{gterms}.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   112
Suppose we are given a function called @{text arity}, specifying the arities
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   113
of all symbols.  In the inductive step, we have a list @{text args} of such
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   114
terms and a function  symbol~@{text f}. If the length of the list matches the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   115
function's arity  then applying @{text f} to @{text args} yields a well-formed
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   116
term.
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   117
*}
10426
469f19c4bf97 rule inversion
nipkow
parents: 10370
diff changeset
   118
23733
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   119
inductive_set
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   120
  well_formed_gterm :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   121
  for arity :: "'f \<Rightarrow> nat"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   122
where
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   123
step[intro!]: "\<lbrakk>\<forall>t \<in> set args. t \<in> well_formed_gterm arity;  
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   124
                length args = arity f\<rbrakk>
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   125
               \<Longrightarrow> (Apply f args) \<in> well_formed_gterm arity"
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   126
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   127
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   128
The inductive definition neatly captures the reasoning above.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   129
The universal quantification over the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   130
@{text set} of arguments expresses that all of them are well-formed.%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   131
\index{quantifiers!and inductive definitions|)}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   132
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   133
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   134
subsection{* Alternative Definition Using a Monotone Function *}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   135
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   136
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   137
\index{monotone functions!and inductive definitions|(}% 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   138
An inductive definition may refer to the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   139
inductively defined  set through an arbitrary monotone function.  To
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   140
demonstrate this powerful feature, let us
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   141
change the  inductive definition above, replacing the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   142
quantifier by a use of the function @{term lists}. This
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   143
function, from the Isabelle theory of lists, is analogous to the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   144
function @{term gterms} declared above: if @{text A} is a set then
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   145
@{term "lists A"} is the set of lists whose elements belong to
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   146
@{term A}.  
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   147
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   148
In the inductive definition of well-formed terms, examine the one
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   149
introduction rule.  The first premise states that @{text args} belongs to
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   150
the @{text lists} of well-formed terms.  This formulation is more
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   151
direct, if more obscure, than using a universal quantifier.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   152
*}
10426
469f19c4bf97 rule inversion
nipkow
parents: 10370
diff changeset
   153
23733
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   154
inductive_set
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   155
  well_formed_gterm' :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   156
  for arity :: "'f \<Rightarrow> nat"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   157
where
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   158
step[intro!]: "\<lbrakk>args \<in> lists (well_formed_gterm' arity);  
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   159
                length args = arity f\<rbrakk>
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   160
               \<Longrightarrow> (Apply f args) \<in> well_formed_gterm' arity"
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   161
monos lists_mono
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   162
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   163
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   164
We cite the theorem @{text lists_mono} to justify 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   165
using the function @{term lists}.%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   166
\footnote{This particular theorem is installed by default already, but we
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   167
include the \isakeyword{monos} declaration in order to illustrate its syntax.}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   168
@{named_thms [display,indent=0] lists_mono [no_vars] (lists_mono)}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   169
Why must the function be monotone?  An inductive definition describes
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   170
an iterative construction: each element of the set is constructed by a
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   171
finite number of introduction rule applications.  For example, the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   172
elements of \isa{even} are constructed by finitely many applications of
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   173
the rules
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   174
@{thm [display,indent=0] even.intros [no_vars]}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   175
All references to a set in its
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   176
inductive definition must be positive.  Applications of an
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   177
introduction rule cannot invalidate previous applications, allowing the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   178
construction process to converge.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   179
The following pair of rules do not constitute an inductive definition:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   180
\begin{trivlist}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   181
\item @{term "0 \<in> even"}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   182
\item @{term "n \<notin> even \<Longrightarrow> (Suc n) \<in> even"}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   183
\end{trivlist}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   184
Showing that 4 is even using these rules requires showing that 3 is not
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   185
even.  It is far from trivial to show that this set of rules
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   186
characterizes the even numbers.  
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   187
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   188
Even with its use of the function \isa{lists}, the premise of our
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   189
introduction rule is positive:
32891
d403b99287ff new generalized concept for term styles
haftmann
parents: 27167
diff changeset
   190
@{thm [display,indent=0] (prem 1) step [no_vars]}
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   191
To apply the rule we construct a list @{term args} of previously
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   192
constructed well-formed terms.  We obtain a
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   193
new term, @{term "Apply f args"}.  Because @{term lists} is monotone,
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   194
applications of the rule remain valid as new terms are constructed.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   195
Further lists of well-formed
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   196
terms become available and none are taken away.%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   197
\index{monotone functions!and inductive definitions|)} 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   198
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   199
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   200
subsection{* A Proof of Equivalence *}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   201
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   202
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   203
We naturally hope that these two inductive definitions of ``well-formed'' 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   204
coincide.  The equality can be proved by separate inclusions in 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   205
each direction.  Each is a trivial rule induction. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   206
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   207
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   208
lemma "well_formed_gterm arity \<subseteq> well_formed_gterm' arity"
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   209
apply clarify
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   210
apply (erule well_formed_gterm.induct)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   211
apply auto
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   212
done
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   213
(*<*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   214
lemma "well_formed_gterm arity \<subseteq> well_formed_gterm' arity"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   215
apply clarify
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   216
apply (erule well_formed_gterm.induct)
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   217
(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   218
txt {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   219
The @{text clarify} method gives
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   220
us an element of @{term "well_formed_gterm arity"} on which to perform 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   221
induction.  The resulting subgoal can be proved automatically:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   222
@{subgoals[display,indent=0]}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   223
This proof resembles the one given in
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   224
{\S}\ref{sec:gterm-datatype} above, especially in the form of the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   225
induction hypothesis.  Next, we consider the opposite inclusion:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   226
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   227
(*<*)oops(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   228
lemma "well_formed_gterm' arity \<subseteq> well_formed_gterm arity"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   229
apply clarify
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   230
apply (erule well_formed_gterm'.induct)
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   231
apply auto
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   232
done
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   233
(*<*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   234
lemma "well_formed_gterm' arity \<subseteq> well_formed_gterm arity"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   235
apply clarify
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   236
apply (erule well_formed_gterm'.induct)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   237
(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   238
txt {*
27167
nipkow
parents: 23842
diff changeset
   239
The proof script is virtually identical,
nipkow
parents: 23842
diff changeset
   240
but the subgoal after applying induction may be surprising:
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   241
@{subgoals[display,indent=0,margin=65]}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   242
The induction hypothesis contains an application of @{term lists}.  Using a
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   243
monotone function in the inductive definition always has this effect.  The
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   244
subgoal may look uninviting, but fortunately 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   245
@{term lists} distributes over intersection:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   246
@{named_thms [display,indent=0] lists_Int_eq [no_vars] (lists_Int_eq)}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   247
Thanks to this default simplification rule, the induction hypothesis 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   248
is quickly replaced by its two parts:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   249
\begin{trivlist}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   250
\item @{term "args \<in> lists (well_formed_gterm' arity)"}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   251
\item @{term "args \<in> lists (well_formed_gterm arity)"}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   252
\end{trivlist}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   253
Invoking the rule @{text well_formed_gterm.step} completes the proof.  The
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   254
call to @{text auto} does all this work.
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   255
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   256
This example is typical of how monotone functions
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   257
\index{monotone functions} can be used.  In particular, many of them
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   258
distribute over intersection.  Monotonicity implies one direction of
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   259
this set equality; we have this theorem:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   260
@{named_thms [display,indent=0] mono_Int [no_vars] (mono_Int)}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   261
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   262
(*<*)oops(*>*)
10426
469f19c4bf97 rule inversion
nipkow
parents: 10370
diff changeset
   263
10370
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   264
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   265
subsection{* Another Example of Rule Inversion *}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   266
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   267
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   268
\index{rule inversion|(}%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   269
Does @{term gterms} distribute over intersection?  We have proved that this
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   270
function is monotone, so @{text mono_Int} gives one of the inclusions.  The
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   271
opposite inclusion asserts that if @{term t} is a ground term over both of the
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   272
sets
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   273
@{term F} and~@{term G} then it is also a ground term over their intersection,
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   274
@{term "F \<inter> G"}.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   275
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   276
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   277
lemma gterms_IntI:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   278
     "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   279
(*<*)oops(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   280
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   281
Attempting this proof, we get the assumption 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   282
@{term "Apply f args \<in> gterms G"}, which cannot be broken down. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   283
It looks like a job for rule inversion:\cmmdx{inductive\protect\_cases}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   284
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   285
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   286
inductive_cases gterm_Apply_elim [elim!]: "Apply f args \<in> gterms F"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   287
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   288
text {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   289
Here is the result.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   290
@{named_thms [display,indent=0,margin=50] gterm_Apply_elim [no_vars] (gterm_Apply_elim)}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   291
This rule replaces an assumption about @{term "Apply f args"} by 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   292
assumptions about @{term f} and~@{term args}.  
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   293
No cases are discarded (there was only one to begin
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   294
with) but the rule applies specifically to the pattern @{term "Apply f args"}.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   295
It can be applied repeatedly as an elimination rule without looping, so we
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   296
have given the @{text "elim!"} attribute. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   297
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   298
Now we can prove the other half of that distributive law.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   299
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   300
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   301
lemma gterms_IntI [rule_format, intro!]:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   302
     "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   303
apply (erule gterms.induct)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   304
apply blast
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   305
done
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   306
(*<*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   307
lemma "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   308
apply (erule gterms.induct)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   309
(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   310
txt {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   311
The proof begins with rule induction over the definition of
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   312
@{term gterms}, which leaves a single subgoal:  
10882
ca41ba5fb8e2 updated for new version of advanced-examples.tex
paulson
parents: 10468
diff changeset
   313
@{subgoals[display,indent=0,margin=65]}
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   314
To prove this, we assume @{term "Apply f args \<in> gterms G"}.  Rule inversion,
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   315
in the form of @{text gterm_Apply_elim}, infers
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   316
that every element of @{term args} belongs to 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   317
@{term "gterms G"}; hence (by the induction hypothesis) it belongs
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   318
to @{term "gterms (F \<inter> G)"}.  Rule inversion also yields
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   319
@{term "f \<in> G"} and hence @{term "f \<in> F \<inter> G"}. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   320
All of this reasoning is done by @{text blast}.
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   321
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   322
\smallskip
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   323
Our distributive law is a trivial consequence of previously-proved results:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   324
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   325
(*<*)oops(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   326
lemma gterms_Int_eq [simp]:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   327
     "gterms (F \<inter> G) = gterms F \<inter> gterms G"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   328
by (blast intro!: mono_Int monoI gterms_mono)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   329
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   330
text_raw {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   331
\index{rule inversion|)}%
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   332
\index{ground terms example|)}
10370
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   333
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   334
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   335
\begin{isamarkuptext}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   336
\begin{exercise}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   337
A function mapping function symbols to their 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   338
types is called a \textbf{signature}.  Given a type 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   339
ranging over type symbols, we can represent a function's type by a
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   340
list of argument types paired with the result type. 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   341
Complete this inductive definition:
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   342
\begin{isabelle}
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   343
*}
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   344
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   345
inductive_set
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   346
  well_typed_gterm :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   347
  for sig :: "'f \<Rightarrow> 't list * 't"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   348
(*<*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   349
where
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   350
step[intro!]: 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   351
    "\<lbrakk>\<forall>pair \<in> set args. pair \<in> well_typed_gterm sig; 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   352
      sig f = (map snd args, rtype)\<rbrakk>
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   353
     \<Longrightarrow> (Apply f (map fst args), rtype) 
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   354
         \<in> well_typed_gterm sig"
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   355
(*>*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   356
text_raw {*
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   357
\end{isabelle}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   358
\end{exercise}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   359
\end{isamarkuptext}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   360
*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   361
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   362
(*<*)
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   363
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   364
text{*the following declaration isn't actually used*}
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   365
primrec
39795
9e59b4c11039 updated files to recent changes
haftmann
parents: 32891
diff changeset
   366
  integer_arity :: "integer_op \<Rightarrow> nat"
9e59b4c11039 updated files to recent changes
haftmann
parents: 32891
diff changeset
   367
where
9e59b4c11039 updated files to recent changes
haftmann
parents: 32891
diff changeset
   368
  "integer_arity (Number n)        = 0"
9e59b4c11039 updated files to recent changes
haftmann
parents: 32891
diff changeset
   369
| "integer_arity UnaryMinus        = 1"
9e59b4c11039 updated files to recent changes
haftmann
parents: 32891
diff changeset
   370
| "integer_arity Plus              = 2"
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   371
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   372
text{* the rest isn't used: too complicated.  OK for an exercise though.*}
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   373
23733
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   374
inductive_set
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   375
  integer_signature :: "(integer_op * (unit list * unit)) set"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   376
where
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   377
  Number:     "(Number n,   ([], ())) \<in> integer_signature"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   378
| UnaryMinus: "(UnaryMinus, ([()], ())) \<in> integer_signature"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   379
| Plus:       "(Plus,       ([(),()], ())) \<in> integer_signature"
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   380
23733
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   381
inductive_set
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   382
  well_typed_gterm' :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   383
  for sig :: "'f \<Rightarrow> 't list * 't"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   384
where
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   385
step[intro!]: 
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   386
    "\<lbrakk>args \<in> lists(well_typed_gterm' sig); 
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   387
      sig f = (map snd args, rtype)\<rbrakk>
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   388
     \<Longrightarrow> (Apply f (map fst args), rtype) 
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   389
         \<in> well_typed_gterm' sig"
10370
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   390
monos lists_mono
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   391
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   392
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   393
lemma "well_typed_gterm sig \<subseteq> well_typed_gterm' sig"
10370
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   394
apply clarify
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   395
apply (erule well_typed_gterm.induct)
10370
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   396
apply auto
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   397
done
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   398
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   399
lemma "well_typed_gterm' sig \<subseteq> well_typed_gterm sig"
10370
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   400
apply clarify
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   401
apply (erule well_typed_gterm'.induct)
10370
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   402
apply auto
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   403
done
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   404
10468
87dda999deca first version of Advanced Inductive Defs section
paulson
parents: 10426
diff changeset
   405
10370
99bd3e902979 advanced induction examples
paulson
parents:
diff changeset
   406
end
23842
9d87177f1f89 LaTeX code is now generated directly from theory file.
berghofe
parents: 23733
diff changeset
   407
(*>*)