author  berghofe 
Wed, 11 Jul 2007 11:14:51 +0200  
changeset 23746  a455e69c31cc 
parent 22269  7c1e65897693 
child 30198  922f944f03b2 
permissions  rwrr 
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  
47 
have "reflexive exprel" by (simp add: refl_def exprel_refl) 

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 