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