|
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 |
|
10 theory QuoNestedDataType = Main: |
|
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 |
|
23 syntax |
|
24 "_exprel" :: "[freeExp, freeExp] => bool" (infixl "~~" 50) |
|
25 syntax (xsymbols) |
|
26 "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50) |
|
27 syntax (HTML output) |
|
28 "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50) |
|
29 translations |
|
30 "X \<sim> Y" == "(X,Y) \<in> exprel" |
|
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 |
|
48 lemma exprel_refl_conj: "X \<sim> X & (Xs,Xs) \<in> listrel(exprel)" |
|
49 apply (induct X and Xs) |
|
50 apply (blast intro: exprel.intros listrel.intros)+ |
|
51 done |
|
52 |
|
53 lemmas exprel_refl = exprel_refl_conj [THEN conjunct1] |
|
54 lemmas list_exprel_refl = exprel_refl_conj [THEN conjunct2] |
|
55 |
|
56 theorem equiv_exprel: "equiv UNIV exprel" |
|
57 proof (simp add: equiv_def, intro conjI) |
|
58 show "reflexive exprel" by (simp add: refl_def exprel_refl) |
|
59 show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM) |
|
60 show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS) |
|
61 qed |
|
62 |
|
63 theorem equiv_list_exprel: "equiv UNIV (listrel exprel)" |
|
64 by (insert equiv_listrel [OF equiv_exprel], simp) |
|
65 |
|
66 |
|
67 lemma FNCALL_Nil: "FNCALL F [] \<sim> FNCALL F []" |
|
68 apply (rule exprel.intros) |
|
69 apply (rule listrel.intros) |
|
70 done |
|
71 |
|
72 lemma FNCALL_Cons: |
|
73 "\<lbrakk>X \<sim> X'; (Xs,Xs') \<in> listrel(exprel)\<rbrakk> |
|
74 \<Longrightarrow> FNCALL F (X#Xs) \<sim> FNCALL F (X'#Xs')" |
|
75 by (blast intro: exprel.intros listrel.intros) |
|
76 |
|
77 |
|
78 |
|
79 subsection{*Some Functions on the Free Algebra*} |
|
80 |
|
81 subsubsection{*The Set of Variables*} |
|
82 |
|
83 text{*A function to return the set of variables present in a message. It will |
|
84 be lifted to the initial algrebra, to serve as an example of that process. |
|
85 Note that the "free" refers to the free datatype rather than to the concept |
|
86 of a free variable.*} |
|
87 consts |
|
88 freevars :: "freeExp \<Rightarrow> nat set" |
|
89 freevars_list :: "freeExp list \<Rightarrow> nat set" |
|
90 |
|
91 primrec |
|
92 "freevars (VAR N) = {N}" |
|
93 "freevars (PLUS X Y) = freevars X \<union> freevars Y" |
|
94 "freevars (FNCALL F Xs) = freevars_list Xs" |
|
95 |
|
96 "freevars_list [] = {}" |
|
97 "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs" |
|
98 |
|
99 text{*This theorem lets us prove that the vars function respects the |
|
100 equivalence relation. It also helps us prove that Variable |
|
101 (the abstract constructor) is injective*} |
|
102 theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V" |
|
103 apply (erule exprel.induct) |
|
104 apply (erule_tac [4] listrel.induct) |
|
105 apply (simp_all add: Un_assoc) |
|
106 done |
|
107 |
|
108 |
|
109 |
|
110 subsubsection{*Functions for Freeness*} |
|
111 |
|
112 text{*A discriminator function to distinguish vars, sums and function calls*} |
|
113 consts freediscrim :: "freeExp \<Rightarrow> int" |
|
114 primrec |
|
115 "freediscrim (VAR N) = 0" |
|
116 "freediscrim (PLUS X Y) = 1" |
|
117 "freediscrim (FNCALL F Xs) = 2" |
|
118 |
|
119 theorem exprel_imp_eq_freediscrim: |
|
120 "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V" |
|
121 by (erule exprel.induct, auto) |
|
122 |
|
123 |
|
124 text{*This function, which returns the function name, is used to |
|
125 prove part of the injectivity property for FnCall.*} |
|
126 consts freefun :: "freeExp \<Rightarrow> nat" |
|
127 |
|
128 primrec |
|
129 "freefun (VAR N) = 0" |
|
130 "freefun (PLUS X Y) = 0" |
|
131 "freefun (FNCALL F Xs) = F" |
|
132 |
|
133 theorem exprel_imp_eq_freefun: |
|
134 "U \<sim> V \<Longrightarrow> freefun U = freefun V" |
|
135 by (erule exprel.induct, simp_all add: listrel.intros) |
|
136 |
|
137 |
|
138 text{*This function, which returns the list of function arguments, is used to |
|
139 prove part of the injectivity property for FnCall.*} |
|
140 consts freeargs :: "freeExp \<Rightarrow> freeExp list" |
|
141 primrec |
|
142 "freeargs (VAR N) = []" |
|
143 "freeargs (PLUS X Y) = []" |
|
144 "freeargs (FNCALL F Xs) = Xs" |
|
145 |
|
146 theorem exprel_imp_eqv_freeargs: |
|
147 "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel" |
|
148 apply (erule exprel.induct) |
|
149 apply (erule_tac [4] listrel.induct) |
|
150 apply (simp_all add: listrel.intros) |
|
151 apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]]) |
|
152 apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]]) |
|
153 done |
|
154 |
|
155 |
|
156 |
|
157 subsection{*The Initial Algebra: A Quotiented Message Type*} |
|
158 |
|
159 |
|
160 typedef (Exp) exp = "UNIV//exprel" |
|
161 by (auto simp add: quotient_def) |
|
162 |
|
163 text{*The abstract message constructors*} |
|
164 |
|
165 constdefs |
|
166 Var :: "nat \<Rightarrow> exp" |
|
167 "Var N == Abs_Exp(exprel``{VAR N})" |
|
168 |
|
169 Plus :: "[exp,exp] \<Rightarrow> exp" |
|
170 "Plus X Y == |
|
171 Abs_Exp (\<Union>U \<in> Rep_Exp X. \<Union>V \<in> Rep_Exp Y. exprel``{PLUS U V})" |
|
172 |
|
173 FnCall :: "[nat, exp list] \<Rightarrow> exp" |
|
174 "FnCall F Xs == |
|
175 Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})" |
|
176 |
|
177 |
|
178 text{*Reduces equality of equivalence classes to the @{term exprel} relation: |
|
179 @{term "(exprel `` {x} = exprel `` {y}) = ((x,y) \<in> exprel)"} *} |
|
180 lemmas equiv_exprel_iff = eq_equiv_class_iff [OF equiv_exprel UNIV_I UNIV_I] |
|
181 |
|
182 declare equiv_exprel_iff [simp] |
|
183 |
|
184 |
|
185 text{*All equivalence classes belong to set of representatives*} |
|
186 lemma [simp]: "exprel``{U} \<in> Exp" |
|
187 by (auto simp add: Exp_def quotient_def intro: exprel_refl) |
|
188 |
|
189 lemma inj_on_Abs_Exp: "inj_on Abs_Exp Exp" |
|
190 apply (rule inj_on_inverseI) |
|
191 apply (erule Abs_Exp_inverse) |
|
192 done |
|
193 |
|
194 text{*Reduces equality on abstractions to equality on representatives*} |
|
195 declare inj_on_Abs_Exp [THEN inj_on_iff, simp] |
|
196 |
|
197 declare Abs_Exp_inverse [simp] |
|
198 |
|
199 |
|
200 text{*Case analysis on the representation of a exp as an equivalence class.*} |
|
201 lemma eq_Abs_Exp [case_names Abs_Exp, cases type: exp]: |
|
202 "(!!U. z = Abs_Exp(exprel``{U}) ==> P) ==> P" |
|
203 apply (rule Rep_Exp [of z, unfolded Exp_def, THEN quotientE]) |
|
204 apply (drule arg_cong [where f=Abs_Exp]) |
|
205 apply (auto simp add: Rep_Exp_inverse intro: exprel_refl) |
|
206 done |
|
207 |
|
208 |
|
209 subsection{*Every list of abstract expressions can be expressed in terms of a |
|
210 list of concrete expressions*} |
|
211 |
|
212 constdefs Abs_ExpList :: "freeExp list => exp list" |
|
213 "Abs_ExpList Xs == map (%U. Abs_Exp(exprel``{U})) Xs" |
|
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) |
|
225 apply (auto simp add: Abs_ExpList_def intro: exprel_refl) |
|
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" |
|
261 by (simp add: congruent_def FNCALL_Cons listrel.intros) |
|
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}"; |
|
268 by (induct_tac Us, simp_all add: listrel_Cons Abs_ExpList_def) |
|
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 |
|
289 constdefs |
|
290 vars :: "exp \<Rightarrow> nat set" |
|
291 "vars X == \<Union>U \<in> Rep_Exp X. freevars U" |
|
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 |
|
355 constdefs |
|
356 fun :: "exp \<Rightarrow> nat" |
|
357 "fun X == contents (\<Union>U \<in> Rep_Exp X. {freefun U})" |
|
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 |
|
367 constdefs |
|
368 args :: "exp \<Rightarrow> exp list" |
|
369 "args X == contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})" |
|
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)" |
|
375 by (erule listrel.induct, simp_all) |
|
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 |
|
402 constdefs |
|
403 discrim :: "exp \<Rightarrow> int" |
|
404 "discrim X == contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})" |
|
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*} |
|
429 theorem exp_induct: |
|
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)" |
|
435 shows "P1 exp & P2 list" |
|
436 proof (cases exp, rule eq_Abs_ExpList [of list], clarify) |
|
437 fix U Us |
|
438 show "P1 (Abs_Exp (exprel `` {U})) \<and> |
|
439 P2 (Abs_ExpList Us)" |
|
440 proof (induct U and Us) |
|
441 case (VAR nat) |
|
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 |
|
456 with Cons |
|
457 show ?case by simp |
|
458 qed |
|
459 qed |
|
460 |
|
461 end |
|
462 |