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