author  wenzelm 
Mon, 07 Oct 2013 21:24:44 +0200  
changeset 54313  da2e6282a4f5 
parent 48985  5386df44a037 
child 56059  2390391584c2 
permissions  rwrr 
48895  1 
(*<*)theory Advanced imports Even begin 
2 
ML_file "../../antiquote_setup.ML" 

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  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:gtermdatatype} *} 
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  28 

29 
datatype 'f gterm = Apply 'f "'f gterm list" 

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  61 

23733  62 
inductive_set 
63 
gterms :: "'f set \<Rightarrow> 'f gterm set" 

64 
for F :: "'f set" 

65 
where 

10468  66 
step[intro!]: "\<lbrakk>\<forall>t \<in> set args. t \<in> gterms F; f \<in> F\<rbrakk> 
67 
\<Longrightarrow> (Apply f args) \<in> gterms F" 

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  81 
lemma gterms_mono: "F\<subseteq>G \<Longrightarrow> gterms F \<subseteq> gterms G" 
82 
apply clarify 

83 
apply (erule gterms.induct) 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

84 
(*>*) 
10882  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  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  106 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

107 
Call a term \textbf{wellformed} 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 wellformedness 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 wellformed 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

116 
term. 
10468  117 
*} 
10426  118 

23733  119 
inductive_set 
120 
well_formed_gterm :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set" 

121 
for arity :: "'f \<Rightarrow> nat" 

122 
where 

10468  123 
step[intro!]: "\<lbrakk>\<forall>t \<in> set args. t \<in> well_formed_gterm arity; 
124 
length args = arity f\<rbrakk> 

125 
\<Longrightarrow> (Apply f args) \<in> well_formed_gterm arity" 

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 wellformed.% 
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 wellformed 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 wellformed 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  153 

23733  154 
inductive_set 
155 
well_formed_gterm' :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set" 

156 
for arity :: "'f \<Rightarrow> nat" 

157 
where 

10468  158 
step[intro!]: "\<lbrakk>args \<in> lists (well_formed_gterm' arity); 
159 
length args = arity f\<rbrakk> 

160 
\<Longrightarrow> (Apply f args) \<in> well_formed_gterm' arity" 

161 
monos lists_mono 

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  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 wellformed 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 wellformed 
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 ``wellformed'' 
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  208 
lemma "well_formed_gterm arity \<subseteq> well_formed_gterm' arity" 
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  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:gtermdatatype} 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  231 
apply auto 
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  239 
The proof script is virtually identical, 
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  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  263 

10370  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  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 previouslyproved 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  333 

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  343 
*} 
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  366 
integer_arity :: "integer_op \<Rightarrow> nat" 
367 
where 

368 
"integer_arity (Number n) = 0" 

369 
 "integer_arity UnaryMinus = 1" 

370 
 "integer_arity Plus = 2" 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

371 

10468  372 
text{* the rest isn't used: too complicated. OK for an exercise though.*} 
373 

23733  374 
inductive_set 
375 
integer_signature :: "(integer_op * (unit list * unit)) set" 

376 
where 

377 
Number: "(Number n, ([], ())) \<in> integer_signature" 

378 
 UnaryMinus: "(UnaryMinus, ([()], ())) \<in> integer_signature" 

379 
 Plus: "(Plus, ([(),()], ())) \<in> integer_signature" 

10468  380 

23733  381 
inductive_set 
382 
well_typed_gterm' :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set" 

383 
for sig :: "'f \<Rightarrow> 't list * 't" 

384 
where 

10468  385 
step[intro!]: 
386 
"\<lbrakk>args \<in> lists(well_typed_gterm' sig); 

387 
sig f = (map snd args, rtype)\<rbrakk> 

388 
\<Longrightarrow> (Apply f (map fst args), rtype) 

389 
\<in> well_typed_gterm' sig" 

10370  390 
monos lists_mono 
391 

392 

10468  393 
lemma "well_typed_gterm sig \<subseteq> well_typed_gterm' sig" 
10370  394 
apply clarify 
10468  395 
apply (erule well_typed_gterm.induct) 
10370  396 
apply auto 
397 
done 

398 

10468  399 
lemma "well_typed_gterm' sig \<subseteq> well_typed_gterm sig" 
10370  400 
apply clarify 
10468  401 
apply (erule well_typed_gterm'.induct) 
10370  402 
apply auto 
403 
done 

404 

10468  405 

10370  406 
end 
23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

407 
(*>*) 