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