author | wenzelm |
Fri, 02 Oct 2009 22:15:08 +0200 | |
changeset 32861 | 105f40051387 |
parent 30198 | 922f944f03b2 |
child 32960 | 69916a850301 |
permissions | -rw-r--r-- |
15172 | 1 |
(* Title: HOL/Induct/QuoNestedDataType |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 2004 University of Cambridge |
|
5 |
||
6 |
*) |
|
7 |
||
8 |
header{*Quotienting a Free Algebra Involving Nested Recursion*} |
|
9 |
||
16417 | 10 |
theory QuoNestedDataType imports Main begin |
15172 | 11 |
|
12 |
subsection{*Defining the Free Algebra*} |
|
13 |
||
14 |
text{*Messages with encryption and decryption as free constructors.*} |
|
15 |
datatype |
|
16 |
freeExp = VAR nat |
|
17 |
| PLUS freeExp freeExp |
|
18 |
| FNCALL nat "freeExp list" |
|
19 |
||
20 |
text{*The equivalence relation, which makes PLUS associative.*} |
|
21 |
||
22 |
text{*The first rule is the desired equation. The next three rules |
|
23 |
make the equations applicable to subterms. The last two rules are symmetry |
|
24 |
and transitivity.*} |
|
23746 | 25 |
inductive_set |
26 |
exprel :: "(freeExp * freeExp) set" |
|
27 |
and exp_rel :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50) |
|
28 |
where |
|
29 |
"X \<sim> Y == (X,Y) \<in> exprel" |
|
30 |
| ASSOC: "PLUS X (PLUS Y Z) \<sim> PLUS (PLUS X Y) Z" |
|
31 |
| VAR: "VAR N \<sim> VAR N" |
|
32 |
| PLUS: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> PLUS X Y \<sim> PLUS X' Y'" |
|
33 |
| FNCALL: "(Xs,Xs') \<in> listrel exprel \<Longrightarrow> FNCALL F Xs \<sim> FNCALL F Xs'" |
|
34 |
| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X" |
|
35 |
| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z" |
|
15172 | 36 |
monos listrel_mono |
37 |
||
38 |
||
39 |
text{*Proving that it is an equivalence relation*} |
|
40 |
||
18460 | 41 |
lemma exprel_refl: "X \<sim> X" |
42 |
and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)" |
|
23746 | 43 |
by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+ |
15172 | 44 |
|
45 |
theorem equiv_exprel: "equiv UNIV exprel" |
|
18460 | 46 |
proof - |
30198 | 47 |
have "refl exprel" by (simp add: refl_on_def exprel_refl) |
18460 | 48 |
moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM) |
49 |
moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS) |
|
50 |
ultimately show ?thesis by (simp add: equiv_def) |
|
15172 | 51 |
qed |
52 |
||
53 |
theorem equiv_list_exprel: "equiv UNIV (listrel exprel)" |
|
18460 | 54 |
using equiv_listrel [OF equiv_exprel] by simp |
15172 | 55 |
|
56 |
||
57 |
lemma FNCALL_Nil: "FNCALL F [] \<sim> FNCALL F []" |
|
58 |
apply (rule exprel.intros) |
|
23746 | 59 |
apply (rule listrel.intros) |
15172 | 60 |
done |
61 |
||
62 |
lemma FNCALL_Cons: |
|
63 |
"\<lbrakk>X \<sim> X'; (Xs,Xs') \<in> listrel(exprel)\<rbrakk> |
|
64 |
\<Longrightarrow> FNCALL F (X#Xs) \<sim> FNCALL F (X'#Xs')" |
|
23746 | 65 |
by (blast intro: exprel.intros listrel.intros) |
15172 | 66 |
|
67 |
||
68 |
||
69 |
subsection{*Some Functions on the Free Algebra*} |
|
70 |
||
71 |
subsubsection{*The Set of Variables*} |
|
72 |
||
73 |
text{*A function to return the set of variables present in a message. It will |
|
74 |
be lifted to the initial algrebra, to serve as an example of that process. |
|
75 |
Note that the "free" refers to the free datatype rather than to the concept |
|
76 |
of a free variable.*} |
|
77 |
consts |
|
78 |
freevars :: "freeExp \<Rightarrow> nat set" |
|
79 |
freevars_list :: "freeExp list \<Rightarrow> nat set" |
|
80 |
||
81 |
primrec |
|
82 |
"freevars (VAR N) = {N}" |
|
83 |
"freevars (PLUS X Y) = freevars X \<union> freevars Y" |
|
84 |
"freevars (FNCALL F Xs) = freevars_list Xs" |
|
85 |
||
86 |
"freevars_list [] = {}" |
|
87 |
"freevars_list (X # Xs) = freevars X \<union> freevars_list Xs" |
|
88 |
||
89 |
text{*This theorem lets us prove that the vars function respects the |
|
90 |
equivalence relation. It also helps us prove that Variable |
|
91 |
(the abstract constructor) is injective*} |
|
92 |
theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V" |
|
18460 | 93 |
apply (induct set: exprel) |
23746 | 94 |
apply (erule_tac [4] listrel.induct) |
15172 | 95 |
apply (simp_all add: Un_assoc) |
96 |
done |
|
97 |
||
98 |
||
99 |
||
100 |
subsubsection{*Functions for Freeness*} |
|
101 |
||
102 |
text{*A discriminator function to distinguish vars, sums and function calls*} |
|
103 |
consts freediscrim :: "freeExp \<Rightarrow> int" |
|
104 |
primrec |
|
105 |
"freediscrim (VAR N) = 0" |
|
106 |
"freediscrim (PLUS X Y) = 1" |
|
107 |
"freediscrim (FNCALL F Xs) = 2" |
|
108 |
||
109 |
theorem exprel_imp_eq_freediscrim: |
|
110 |
"U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V" |
|
18460 | 111 |
by (induct set: exprel) auto |
15172 | 112 |
|
113 |
||
114 |
text{*This function, which returns the function name, is used to |
|
115 |
prove part of the injectivity property for FnCall.*} |
|
116 |
consts freefun :: "freeExp \<Rightarrow> nat" |
|
117 |
||
118 |
primrec |
|
119 |
"freefun (VAR N) = 0" |
|
120 |
"freefun (PLUS X Y) = 0" |
|
121 |
"freefun (FNCALL F Xs) = F" |
|
122 |
||
123 |
theorem exprel_imp_eq_freefun: |
|
124 |
"U \<sim> V \<Longrightarrow> freefun U = freefun V" |
|
23746 | 125 |
by (induct set: exprel) (simp_all add: listrel.intros) |
15172 | 126 |
|
127 |
||
128 |
text{*This function, which returns the list of function arguments, is used to |
|
129 |
prove part of the injectivity property for FnCall.*} |
|
130 |
consts freeargs :: "freeExp \<Rightarrow> freeExp list" |
|
131 |
primrec |
|
132 |
"freeargs (VAR N) = []" |
|
133 |
"freeargs (PLUS X Y) = []" |
|
134 |
"freeargs (FNCALL F Xs) = Xs" |
|
135 |
||
136 |
theorem exprel_imp_eqv_freeargs: |
|
137 |
"U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel" |
|
18460 | 138 |
apply (induct set: exprel) |
23746 | 139 |
apply (erule_tac [4] listrel.induct) |
140 |
apply (simp_all add: listrel.intros) |
|
15172 | 141 |
apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]]) |
142 |
apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]]) |
|
143 |
done |
|
144 |
||
145 |
||
146 |
||
147 |
subsection{*The Initial Algebra: A Quotiented Message Type*} |
|
148 |
||
149 |
||
150 |
typedef (Exp) exp = "UNIV//exprel" |
|
151 |
by (auto simp add: quotient_def) |
|
152 |
||
153 |
text{*The abstract message constructors*} |
|
154 |
||
19736 | 155 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
156 |
Var :: "nat \<Rightarrow> exp" where |
19736 | 157 |
"Var N = Abs_Exp(exprel``{VAR N})" |
15172 | 158 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
159 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
160 |
Plus :: "[exp,exp] \<Rightarrow> exp" where |
19736 | 161 |
"Plus X Y = |
15172 | 162 |
Abs_Exp (\<Union>U \<in> Rep_Exp X. \<Union>V \<in> Rep_Exp Y. exprel``{PLUS U V})" |
163 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
164 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
165 |
FnCall :: "[nat, exp list] \<Rightarrow> exp" where |
19736 | 166 |
"FnCall F Xs = |
15172 | 167 |
Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})" |
168 |
||
169 |
||
170 |
text{*Reduces equality of equivalence classes to the @{term exprel} relation: |
|
171 |
@{term "(exprel `` {x} = exprel `` {y}) = ((x,y) \<in> exprel)"} *} |
|
172 |
lemmas equiv_exprel_iff = eq_equiv_class_iff [OF equiv_exprel UNIV_I UNIV_I] |
|
173 |
||
174 |
declare equiv_exprel_iff [simp] |
|
175 |
||
176 |
||
177 |
text{*All equivalence classes belong to set of representatives*} |
|
178 |
lemma [simp]: "exprel``{U} \<in> Exp" |
|
179 |
by (auto simp add: Exp_def quotient_def intro: exprel_refl) |
|
180 |
||
181 |
lemma inj_on_Abs_Exp: "inj_on Abs_Exp Exp" |
|
182 |
apply (rule inj_on_inverseI) |
|
183 |
apply (erule Abs_Exp_inverse) |
|
184 |
done |
|
185 |
||
186 |
text{*Reduces equality on abstractions to equality on representatives*} |
|
187 |
declare inj_on_Abs_Exp [THEN inj_on_iff, simp] |
|
188 |
||
189 |
declare Abs_Exp_inverse [simp] |
|
190 |
||
191 |
||
192 |
text{*Case analysis on the representation of a exp as an equivalence class.*} |
|
193 |
lemma eq_Abs_Exp [case_names Abs_Exp, cases type: exp]: |
|
194 |
"(!!U. z = Abs_Exp(exprel``{U}) ==> P) ==> P" |
|
195 |
apply (rule Rep_Exp [of z, unfolded Exp_def, THEN quotientE]) |
|
196 |
apply (drule arg_cong [where f=Abs_Exp]) |
|
197 |
apply (auto simp add: Rep_Exp_inverse intro: exprel_refl) |
|
198 |
done |
|
199 |
||
200 |
||
201 |
subsection{*Every list of abstract expressions can be expressed in terms of a |
|
202 |
list of concrete expressions*} |
|
203 |
||
19736 | 204 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
205 |
Abs_ExpList :: "freeExp list => exp list" where |
19736 | 206 |
"Abs_ExpList Xs = map (%U. Abs_Exp(exprel``{U})) Xs" |
15172 | 207 |
|
208 |
lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] == []" |
|
209 |
by (simp add: Abs_ExpList_def) |
|
210 |
||
211 |
lemma Abs_ExpList_Cons [simp]: |
|
212 |
"Abs_ExpList (X#Xs) == Abs_Exp (exprel``{X}) # Abs_ExpList Xs" |
|
213 |
by (simp add: Abs_ExpList_def) |
|
214 |
||
215 |
lemma ExpList_rep: "\<exists>Us. z = Abs_ExpList Us" |
|
216 |
apply (induct z) |
|
217 |
apply (rule_tac [2] z=a in eq_Abs_Exp) |
|
18447 | 218 |
apply (auto simp add: Abs_ExpList_def Cons_eq_map_conv intro: exprel_refl) |
15172 | 219 |
done |
220 |
||
221 |
lemma eq_Abs_ExpList [case_names Abs_ExpList]: |
|
222 |
"(!!Us. z = Abs_ExpList Us ==> P) ==> P" |
|
223 |
by (rule exE [OF ExpList_rep], blast) |
|
224 |
||
225 |
||
226 |
subsubsection{*Characteristic Equations for the Abstract Constructors*} |
|
227 |
||
228 |
lemma Plus: "Plus (Abs_Exp(exprel``{U})) (Abs_Exp(exprel``{V})) = |
|
229 |
Abs_Exp (exprel``{PLUS U V})" |
|
230 |
proof - |
|
231 |
have "(\<lambda>U V. exprel `` {PLUS U V}) respects2 exprel" |
|
232 |
by (simp add: congruent2_def exprel.PLUS) |
|
233 |
thus ?thesis |
|
234 |
by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel]) |
|
235 |
qed |
|
236 |
||
237 |
text{*It is not clear what to do with FnCall: it's argument is an abstraction |
|
238 |
of an @{typ "exp list"}. Is it just Nil or Cons? What seems to work best is to |
|
239 |
regard an @{typ "exp list"} as a @{term "listrel exprel"} equivalence class*} |
|
240 |
||
241 |
text{*This theorem is easily proved but never used. There's no obvious way |
|
242 |
even to state the analogous result, @{text FnCall_Cons}.*} |
|
243 |
lemma FnCall_Nil: "FnCall F [] = Abs_Exp (exprel``{FNCALL F []})" |
|
244 |
by (simp add: FnCall_def) |
|
245 |
||
246 |
lemma FnCall_respects: |
|
247 |
"(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)" |
|
248 |
by (simp add: congruent_def exprel.FNCALL) |
|
249 |
||
250 |
lemma FnCall_sing: |
|
251 |
"FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})" |
|
252 |
proof - |
|
253 |
have "(\<lambda>U. exprel `` {FNCALL F [U]}) respects exprel" |
|
23746 | 254 |
by (simp add: congruent_def FNCALL_Cons listrel.intros) |
15172 | 255 |
thus ?thesis |
256 |
by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel]) |
|
257 |
qed |
|
258 |
||
259 |
lemma listset_Rep_Exp_Abs_Exp: |
|
260 |
"listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}"; |
|
18460 | 261 |
by (induct Us) (simp_all add: listrel_Cons Abs_ExpList_def) |
15172 | 262 |
|
263 |
lemma FnCall: |
|
264 |
"FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})" |
|
265 |
proof - |
|
266 |
have "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)" |
|
267 |
by (simp add: congruent_def exprel.FNCALL) |
|
268 |
thus ?thesis |
|
269 |
by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel] |
|
270 |
listset_Rep_Exp_Abs_Exp) |
|
271 |
qed |
|
272 |
||
273 |
||
274 |
text{*Establishing this equation is the point of the whole exercise*} |
|
275 |
theorem Plus_assoc: "Plus X (Plus Y Z) = Plus (Plus X Y) Z" |
|
276 |
by (cases X, cases Y, cases Z, simp add: Plus exprel.ASSOC) |
|
277 |
||
278 |
||
279 |
||
280 |
subsection{*The Abstract Function to Return the Set of Variables*} |
|
281 |
||
19736 | 282 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
283 |
vars :: "exp \<Rightarrow> nat set" where |
19736 | 284 |
"vars X = (\<Union>U \<in> Rep_Exp X. freevars U)" |
15172 | 285 |
|
286 |
lemma vars_respects: "freevars respects exprel" |
|
287 |
by (simp add: congruent_def exprel_imp_eq_freevars) |
|
288 |
||
289 |
text{*The extension of the function @{term vars} to lists*} |
|
290 |
consts vars_list :: "exp list \<Rightarrow> nat set" |
|
291 |
primrec |
|
292 |
"vars_list [] = {}" |
|
293 |
"vars_list(E#Es) = vars E \<union> vars_list Es" |
|
294 |
||
295 |
||
296 |
text{*Now prove the three equations for @{term vars}*} |
|
297 |
||
298 |
lemma vars_Variable [simp]: "vars (Var N) = {N}" |
|
299 |
by (simp add: vars_def Var_def |
|
300 |
UN_equiv_class [OF equiv_exprel vars_respects]) |
|
301 |
||
302 |
lemma vars_Plus [simp]: "vars (Plus X Y) = vars X \<union> vars Y" |
|
303 |
apply (cases X, cases Y) |
|
304 |
apply (simp add: vars_def Plus |
|
305 |
UN_equiv_class [OF equiv_exprel vars_respects]) |
|
306 |
done |
|
307 |
||
308 |
lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs" |
|
309 |
apply (cases Xs rule: eq_Abs_ExpList) |
|
310 |
apply (simp add: FnCall) |
|
311 |
apply (induct_tac Us) |
|
312 |
apply (simp_all add: vars_def UN_equiv_class [OF equiv_exprel vars_respects]) |
|
313 |
done |
|
314 |
||
315 |
lemma vars_FnCall_Nil: "vars (FnCall F Nil) = {}" |
|
316 |
by simp |
|
317 |
||
318 |
lemma vars_FnCall_Cons: "vars (FnCall F (X#Xs)) = vars X \<union> vars_list Xs" |
|
319 |
by simp |
|
320 |
||
321 |
||
322 |
subsection{*Injectivity Properties of Some Constructors*} |
|
323 |
||
324 |
lemma VAR_imp_eq: "VAR m \<sim> VAR n \<Longrightarrow> m = n" |
|
325 |
by (drule exprel_imp_eq_freevars, simp) |
|
326 |
||
327 |
text{*Can also be proved using the function @{term vars}*} |
|
328 |
lemma Var_Var_eq [iff]: "(Var m = Var n) = (m = n)" |
|
329 |
by (auto simp add: Var_def exprel_refl dest: VAR_imp_eq) |
|
330 |
||
331 |
lemma VAR_neqv_PLUS: "VAR m \<sim> PLUS X Y \<Longrightarrow> False" |
|
332 |
by (drule exprel_imp_eq_freediscrim, simp) |
|
333 |
||
334 |
theorem Var_neq_Plus [iff]: "Var N \<noteq> Plus X Y" |
|
335 |
apply (cases X, cases Y) |
|
336 |
apply (simp add: Var_def Plus) |
|
337 |
apply (blast dest: VAR_neqv_PLUS) |
|
338 |
done |
|
339 |
||
340 |
theorem Var_neq_FnCall [iff]: "Var N \<noteq> FnCall F Xs" |
|
341 |
apply (cases Xs rule: eq_Abs_ExpList) |
|
342 |
apply (auto simp add: FnCall Var_def) |
|
343 |
apply (drule exprel_imp_eq_freediscrim, simp) |
|
344 |
done |
|
345 |
||
346 |
subsection{*Injectivity of @{term FnCall}*} |
|
347 |
||
19736 | 348 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
349 |
"fun" :: "exp \<Rightarrow> nat" where |
19736 | 350 |
"fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})" |
15172 | 351 |
|
352 |
lemma fun_respects: "(%U. {freefun U}) respects exprel" |
|
353 |
by (simp add: congruent_def exprel_imp_eq_freefun) |
|
354 |
||
355 |
lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F" |
|
356 |
apply (cases Xs rule: eq_Abs_ExpList) |
|
357 |
apply (simp add: FnCall fun_def UN_equiv_class [OF equiv_exprel fun_respects]) |
|
358 |
done |
|
359 |
||
19736 | 360 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
361 |
args :: "exp \<Rightarrow> exp list" where |
19736 | 362 |
"args X = contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})" |
15172 | 363 |
|
364 |
text{*This result can probably be generalized to arbitrary equivalence |
|
365 |
relations, but with little benefit here.*} |
|
366 |
lemma Abs_ExpList_eq: |
|
367 |
"(y, z) \<in> listrel exprel \<Longrightarrow> Abs_ExpList (y) = Abs_ExpList (z)" |
|
18460 | 368 |
by (induct set: listrel) simp_all |
15172 | 369 |
|
370 |
lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel" |
|
371 |
by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) |
|
372 |
||
373 |
lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs" |
|
374 |
apply (cases Xs rule: eq_Abs_ExpList) |
|
375 |
apply (simp add: FnCall args_def UN_equiv_class [OF equiv_exprel args_respects]) |
|
376 |
done |
|
377 |
||
378 |
||
379 |
lemma FnCall_FnCall_eq [iff]: |
|
380 |
"(FnCall F Xs = FnCall F' Xs') = (F=F' & Xs=Xs')" |
|
381 |
proof |
|
382 |
assume "FnCall F Xs = FnCall F' Xs'" |
|
383 |
hence "fun (FnCall F Xs) = fun (FnCall F' Xs')" |
|
384 |
and "args (FnCall F Xs) = args (FnCall F' Xs')" by auto |
|
385 |
thus "F=F' & Xs=Xs'" by simp |
|
386 |
next |
|
387 |
assume "F=F' & Xs=Xs'" thus "FnCall F Xs = FnCall F' Xs'" by simp |
|
388 |
qed |
|
389 |
||
390 |
||
391 |
subsection{*The Abstract Discriminator*} |
|
392 |
text{*However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this |
|
393 |
function in order to prove discrimination theorems.*} |
|
394 |
||
19736 | 395 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
396 |
discrim :: "exp \<Rightarrow> int" where |
19736 | 397 |
"discrim X = contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})" |
15172 | 398 |
|
399 |
lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel" |
|
400 |
by (simp add: congruent_def exprel_imp_eq_freediscrim) |
|
401 |
||
402 |
text{*Now prove the four equations for @{term discrim}*} |
|
403 |
||
404 |
lemma discrim_Var [simp]: "discrim (Var N) = 0" |
|
405 |
by (simp add: discrim_def Var_def |
|
406 |
UN_equiv_class [OF equiv_exprel discrim_respects]) |
|
407 |
||
408 |
lemma discrim_Plus [simp]: "discrim (Plus X Y) = 1" |
|
409 |
apply (cases X, cases Y) |
|
410 |
apply (simp add: discrim_def Plus |
|
411 |
UN_equiv_class [OF equiv_exprel discrim_respects]) |
|
412 |
done |
|
413 |
||
414 |
lemma discrim_FnCall [simp]: "discrim (FnCall F Xs) = 2" |
|
415 |
apply (rule_tac z=Xs in eq_Abs_ExpList) |
|
416 |
apply (simp add: discrim_def FnCall |
|
417 |
UN_equiv_class [OF equiv_exprel discrim_respects]) |
|
418 |
done |
|
419 |
||
420 |
||
421 |
text{*The structural induction rule for the abstract type*} |
|
18460 | 422 |
theorem exp_inducts: |
15172 | 423 |
assumes V: "\<And>nat. P1 (Var nat)" |
424 |
and P: "\<And>exp1 exp2. \<lbrakk>P1 exp1; P1 exp2\<rbrakk> \<Longrightarrow> P1 (Plus exp1 exp2)" |
|
425 |
and F: "\<And>nat list. P2 list \<Longrightarrow> P1 (FnCall nat list)" |
|
426 |
and Nil: "P2 []" |
|
427 |
and Cons: "\<And>exp list. \<lbrakk>P1 exp; P2 list\<rbrakk> \<Longrightarrow> P2 (exp # list)" |
|
18460 | 428 |
shows "P1 exp" and "P2 list" |
429 |
proof - |
|
430 |
obtain U where exp: "exp = (Abs_Exp (exprel `` {U}))" by (cases exp) |
|
431 |
obtain Us where list: "list = Abs_ExpList Us" by (rule eq_Abs_ExpList) |
|
432 |
have "P1 (Abs_Exp (exprel `` {U}))" and "P2 (Abs_ExpList Us)" |
|
15172 | 433 |
proof (induct U and Us) |
18460 | 434 |
case (VAR nat) |
15172 | 435 |
with V show ?case by (simp add: Var_def) |
436 |
next |
|
437 |
case (PLUS X Y) |
|
438 |
with P [of "Abs_Exp (exprel `` {X})" "Abs_Exp (exprel `` {Y})"] |
|
439 |
show ?case by (simp add: Plus) |
|
440 |
next |
|
441 |
case (FNCALL nat list) |
|
442 |
with F [of "Abs_ExpList list"] |
|
443 |
show ?case by (simp add: FnCall) |
|
444 |
next |
|
445 |
case Nil_freeExp |
|
446 |
with Nil show ?case by simp |
|
447 |
next |
|
448 |
case Cons_freeExp |
|
18460 | 449 |
with Cons show ?case by simp |
15172 | 450 |
qed |
18460 | 451 |
with exp and list show "P1 exp" and "P2 list" by (simp_all only:) |
15172 | 452 |
qed |
453 |
||
454 |
end |