author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45694  4a8743618257 
child 49834  b27bbb021df1 
permissions  rwrr 
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.*} 

13 
datatype 

14 
freeExp = VAR nat 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30198
diff
changeset

15 
 PLUS freeExp freeExp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30198
diff
changeset

16 
 FNCALL nat "freeExp list" 
15172  17 

18 
text{*The equivalence relation, which makes PLUS associative.*} 

19 

20 
text{*The first rule is the desired equation. The next three rules 

21 
make the equations applicable to subterms. The last two rules are symmetry 

22 
and transitivity.*} 

23746  23 
inductive_set 
24 
exprel :: "(freeExp * freeExp) set" 

25 
and exp_rel :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50) 

26 
where 

27 
"X \<sim> Y == (X,Y) \<in> exprel" 

28 
 ASSOC: "PLUS X (PLUS Y Z) \<sim> PLUS (PLUS X Y) Z" 

29 
 VAR: "VAR N \<sim> VAR N" 

30 
 PLUS: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> PLUS X Y \<sim> PLUS X' Y'" 

31 
 FNCALL: "(Xs,Xs') \<in> listrel exprel \<Longrightarrow> FNCALL F Xs \<sim> FNCALL F Xs'" 

32 
 SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X" 

33 
 TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z" 

15172  34 
monos listrel_mono 
35 

36 

37 
text{*Proving that it is an equivalence relation*} 

38 

18460  39 
lemma exprel_refl: "X \<sim> X" 
40 
and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)" 

23746  41 
by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+ 
15172  42 

43 
theorem equiv_exprel: "equiv UNIV exprel" 

18460  44 
proof  
30198  45 
have "refl exprel" by (simp add: refl_on_def exprel_refl) 
18460  46 
moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM) 
47 
moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS) 

48 
ultimately show ?thesis by (simp add: equiv_def) 

15172  49 
qed 
50 

51 
theorem equiv_list_exprel: "equiv UNIV (listrel exprel)" 

18460  52 
using equiv_listrel [OF equiv_exprel] by simp 
15172  53 

54 

55 
lemma FNCALL_Nil: "FNCALL F [] \<sim> FNCALL F []" 

56 
apply (rule exprel.intros) 

23746  57 
apply (rule listrel.intros) 
15172  58 
done 
59 

60 
lemma FNCALL_Cons: 

61 
"\<lbrakk>X \<sim> X'; (Xs,Xs') \<in> listrel(exprel)\<rbrakk> 

62 
\<Longrightarrow> FNCALL F (X#Xs) \<sim> FNCALL F (X'#Xs')" 

23746  63 
by (blast intro: exprel.intros listrel.intros) 
15172  64 

65 

66 

67 
subsection{*Some Functions on the Free Algebra*} 

68 

69 
subsubsection{*The Set of Variables*} 

70 

71 
text{*A function to return the set of variables present in a message. It will 

72 
be lifted to the initial algrebra, to serve as an example of that process. 

73 
Note that the "free" refers to the free datatype rather than to the concept 

74 
of a free variable.*} 

39246  75 
primrec freevars :: "freeExp \<Rightarrow> nat set" 
76 
and freevars_list :: "freeExp list \<Rightarrow> nat set" where 

77 
"freevars (VAR N) = {N}" 

78 
 "freevars (PLUS X Y) = freevars X \<union> freevars Y" 

79 
 "freevars (FNCALL F Xs) = freevars_list Xs" 

15172  80 

39246  81 
 "freevars_list [] = {}" 
82 
 "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs" 

15172  83 

84 
text{*This theorem lets us prove that the vars function respects the 

85 
equivalence relation. It also helps us prove that Variable 

86 
(the abstract constructor) is injective*} 

87 
theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V" 

18460  88 
apply (induct set: exprel) 
23746  89 
apply (erule_tac [4] listrel.induct) 
15172  90 
apply (simp_all add: Un_assoc) 
91 
done 

92 

93 

94 

95 
subsubsection{*Functions for Freeness*} 

96 

97 
text{*A discriminator function to distinguish vars, sums and function calls*} 

39246  98 
primrec freediscrim :: "freeExp \<Rightarrow> int" where 
99 
"freediscrim (VAR N) = 0" 

100 
 "freediscrim (PLUS X Y) = 1" 

101 
 "freediscrim (FNCALL F Xs) = 2" 

15172  102 

103 
theorem exprel_imp_eq_freediscrim: 

104 
"U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V" 

18460  105 
by (induct set: exprel) auto 
15172  106 

107 

108 
text{*This function, which returns the function name, is used to 

109 
prove part of the injectivity property for FnCall.*} 

39246  110 
primrec freefun :: "freeExp \<Rightarrow> nat" where 
111 
"freefun (VAR N) = 0" 

112 
 "freefun (PLUS X Y) = 0" 

113 
 "freefun (FNCALL F Xs) = F" 

15172  114 

115 
theorem exprel_imp_eq_freefun: 

116 
"U \<sim> V \<Longrightarrow> freefun U = freefun V" 

23746  117 
by (induct set: exprel) (simp_all add: listrel.intros) 
15172  118 

119 

120 
text{*This function, which returns the list of function arguments, is used to 

121 
prove part of the injectivity property for FnCall.*} 

39246  122 
primrec freeargs :: "freeExp \<Rightarrow> freeExp list" where 
123 
"freeargs (VAR N) = []" 

124 
 "freeargs (PLUS X Y) = []" 

125 
 "freeargs (FNCALL F Xs) = Xs" 

15172  126 

127 
theorem exprel_imp_eqv_freeargs: 

40822  128 
assumes "U \<sim> V" 
129 
shows "(freeargs U, freeargs V) \<in> listrel exprel" 

130 
proof  

131 
from equiv_list_exprel have sym: "sym (listrel exprel)" by (rule equivE) 

132 
from equiv_list_exprel have trans: "trans (listrel exprel)" by (rule equivE) 

133 
from assms show ?thesis 

134 
apply induct 

135 
apply (erule_tac [4] listrel.induct) 

136 
apply (simp_all add: listrel.intros) 

137 
apply (blast intro: symD [OF sym]) 

138 
apply (blast intro: transD [OF trans]) 

139 
done 

140 
qed 

15172  141 

142 

143 
subsection{*The Initial Algebra: A Quotiented Message Type*} 

144 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
41959
diff
changeset

145 
definition "Exp = UNIV//exprel" 
15172  146 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
41959
diff
changeset

147 
typedef (open) exp = Exp 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
41959
diff
changeset

148 
morphisms Rep_Exp Abs_Exp 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
41959
diff
changeset

149 
unfolding Exp_def by (auto simp add: quotient_def) 
15172  150 

151 
text{*The abstract message constructors*} 

152 

19736  153 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

154 
Var :: "nat \<Rightarrow> exp" where 
19736  155 
"Var N = Abs_Exp(exprel``{VAR N})" 
15172  156 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

157 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

158 
Plus :: "[exp,exp] \<Rightarrow> exp" where 
19736  159 
"Plus X Y = 
15172  160 
Abs_Exp (\<Union>U \<in> Rep_Exp X. \<Union>V \<in> Rep_Exp Y. exprel``{PLUS U V})" 
161 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

162 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

163 
FnCall :: "[nat, exp list] \<Rightarrow> exp" where 
19736  164 
"FnCall F Xs = 
15172  165 
Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})" 
166 

167 

168 
text{*Reduces equality of equivalence classes to the @{term exprel} relation: 

169 
@{term "(exprel `` {x} = exprel `` {y}) = ((x,y) \<in> exprel)"} *} 

170 
lemmas equiv_exprel_iff = eq_equiv_class_iff [OF equiv_exprel UNIV_I UNIV_I] 

171 

172 
declare equiv_exprel_iff [simp] 

173 

174 

175 
text{*All equivalence classes belong to set of representatives*} 

176 
lemma [simp]: "exprel``{U} \<in> Exp" 

177 
by (auto simp add: Exp_def quotient_def intro: exprel_refl) 

178 

179 
lemma inj_on_Abs_Exp: "inj_on Abs_Exp Exp" 

180 
apply (rule inj_on_inverseI) 

181 
apply (erule Abs_Exp_inverse) 

182 
done 

183 

184 
text{*Reduces equality on abstractions to equality on representatives*} 

185 
declare inj_on_Abs_Exp [THEN inj_on_iff, simp] 

186 

187 
declare Abs_Exp_inverse [simp] 

188 

189 

190 
text{*Case analysis on the representation of a exp as an equivalence class.*} 

191 
lemma eq_Abs_Exp [case_names Abs_Exp, cases type: exp]: 

192 
"(!!U. z = Abs_Exp(exprel``{U}) ==> P) ==> P" 

193 
apply (rule Rep_Exp [of z, unfolded Exp_def, THEN quotientE]) 

194 
apply (drule arg_cong [where f=Abs_Exp]) 

195 
apply (auto simp add: Rep_Exp_inverse intro: exprel_refl) 

196 
done 

197 

198 

199 
subsection{*Every list of abstract expressions can be expressed in terms of a 

200 
list of concrete expressions*} 

201 

19736  202 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

203 
Abs_ExpList :: "freeExp list => exp list" where 
19736  204 
"Abs_ExpList Xs = map (%U. Abs_Exp(exprel``{U})) Xs" 
15172  205 

206 
lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] == []" 

207 
by (simp add: Abs_ExpList_def) 

208 

209 
lemma Abs_ExpList_Cons [simp]: 

210 
"Abs_ExpList (X#Xs) == Abs_Exp (exprel``{X}) # Abs_ExpList Xs" 

211 
by (simp add: Abs_ExpList_def) 

212 

213 
lemma ExpList_rep: "\<exists>Us. z = Abs_ExpList Us" 

214 
apply (induct z) 

215 
apply (rule_tac [2] z=a in eq_Abs_Exp) 

18447  216 
apply (auto simp add: Abs_ExpList_def Cons_eq_map_conv intro: exprel_refl) 
15172  217 
done 
218 

219 
lemma eq_Abs_ExpList [case_names Abs_ExpList]: 

220 
"(!!Us. z = Abs_ExpList Us ==> P) ==> P" 

221 
by (rule exE [OF ExpList_rep], blast) 

222 

223 

224 
subsubsection{*Characteristic Equations for the Abstract Constructors*} 

225 

226 
lemma Plus: "Plus (Abs_Exp(exprel``{U})) (Abs_Exp(exprel``{V})) = 

227 
Abs_Exp (exprel``{PLUS U V})" 

228 
proof  

229 
have "(\<lambda>U V. exprel `` {PLUS U V}) respects2 exprel" 

40822  230 
by (auto simp add: congruent2_def exprel.PLUS) 
15172  231 
thus ?thesis 
232 
by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel]) 

233 
qed 

234 

235 
text{*It is not clear what to do with FnCall: it's argument is an abstraction 

236 
of an @{typ "exp list"}. Is it just Nil or Cons? What seems to work best is to 

237 
regard an @{typ "exp list"} as a @{term "listrel exprel"} equivalence class*} 

238 

239 
text{*This theorem is easily proved but never used. There's no obvious way 

240 
even to state the analogous result, @{text FnCall_Cons}.*} 

241 
lemma FnCall_Nil: "FnCall F [] = Abs_Exp (exprel``{FNCALL F []})" 

242 
by (simp add: FnCall_def) 

243 

244 
lemma FnCall_respects: 

245 
"(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)" 

40822  246 
by (auto simp add: congruent_def exprel.FNCALL) 
15172  247 

248 
lemma FnCall_sing: 

249 
"FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})" 

250 
proof  

251 
have "(\<lambda>U. exprel `` {FNCALL F [U]}) respects exprel" 

40822  252 
by (auto simp add: congruent_def FNCALL_Cons listrel.intros) 
15172  253 
thus ?thesis 
254 
by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel]) 

255 
qed 

256 

257 
lemma listset_Rep_Exp_Abs_Exp: 

258 
"listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}"; 

18460  259 
by (induct Us) (simp_all add: listrel_Cons Abs_ExpList_def) 
15172  260 

261 
lemma FnCall: 

262 
"FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})" 

263 
proof  

264 
have "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)" 

40822  265 
by (auto simp add: congruent_def exprel.FNCALL) 
15172  266 
thus ?thesis 
267 
by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel] 

268 
listset_Rep_Exp_Abs_Exp) 

269 
qed 

270 

271 

272 
text{*Establishing this equation is the point of the whole exercise*} 

273 
theorem Plus_assoc: "Plus X (Plus Y Z) = Plus (Plus X Y) Z" 

274 
by (cases X, cases Y, cases Z, simp add: Plus exprel.ASSOC) 

275 

276 

277 

278 
subsection{*The Abstract Function to Return the Set of Variables*} 

279 

19736  280 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

281 
vars :: "exp \<Rightarrow> nat set" where 
19736  282 
"vars X = (\<Union>U \<in> Rep_Exp X. freevars U)" 
15172  283 

284 
lemma vars_respects: "freevars respects exprel" 

40822  285 
by (auto simp add: congruent_def exprel_imp_eq_freevars) 
15172  286 

287 
text{*The extension of the function @{term vars} to lists*} 

39246  288 
primrec vars_list :: "exp list \<Rightarrow> nat set" where 
289 
"vars_list [] = {}" 

290 
 "vars_list(E#Es) = vars E \<union> vars_list Es" 

15172  291 

292 

293 
text{*Now prove the three equations for @{term vars}*} 

294 

295 
lemma vars_Variable [simp]: "vars (Var N) = {N}" 

296 
by (simp add: vars_def Var_def 

297 
UN_equiv_class [OF equiv_exprel vars_respects]) 

298 

299 
lemma vars_Plus [simp]: "vars (Plus X Y) = vars X \<union> vars Y" 

300 
apply (cases X, cases Y) 

301 
apply (simp add: vars_def Plus 

302 
UN_equiv_class [OF equiv_exprel vars_respects]) 

303 
done 

304 

305 
lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs" 

306 
apply (cases Xs rule: eq_Abs_ExpList) 

307 
apply (simp add: FnCall) 

308 
apply (induct_tac Us) 

309 
apply (simp_all add: vars_def UN_equiv_class [OF equiv_exprel vars_respects]) 

310 
done 

311 

312 
lemma vars_FnCall_Nil: "vars (FnCall F Nil) = {}" 

313 
by simp 

314 

315 
lemma vars_FnCall_Cons: "vars (FnCall F (X#Xs)) = vars X \<union> vars_list Xs" 

316 
by simp 

317 

318 

319 
subsection{*Injectivity Properties of Some Constructors*} 

320 

321 
lemma VAR_imp_eq: "VAR m \<sim> VAR n \<Longrightarrow> m = n" 

322 
by (drule exprel_imp_eq_freevars, simp) 

323 

324 
text{*Can also be proved using the function @{term vars}*} 

325 
lemma Var_Var_eq [iff]: "(Var m = Var n) = (m = n)" 

326 
by (auto simp add: Var_def exprel_refl dest: VAR_imp_eq) 

327 

328 
lemma VAR_neqv_PLUS: "VAR m \<sim> PLUS X Y \<Longrightarrow> False" 

329 
by (drule exprel_imp_eq_freediscrim, simp) 

330 

331 
theorem Var_neq_Plus [iff]: "Var N \<noteq> Plus X Y" 

332 
apply (cases X, cases Y) 

333 
apply (simp add: Var_def Plus) 

334 
apply (blast dest: VAR_neqv_PLUS) 

335 
done 

336 

337 
theorem Var_neq_FnCall [iff]: "Var N \<noteq> FnCall F Xs" 

338 
apply (cases Xs rule: eq_Abs_ExpList) 

339 
apply (auto simp add: FnCall Var_def) 

340 
apply (drule exprel_imp_eq_freediscrim, simp) 

341 
done 

342 

343 
subsection{*Injectivity of @{term FnCall}*} 

344 

19736  345 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

346 
"fun" :: "exp \<Rightarrow> nat" where 
39910  347 
"fun X = the_elem (\<Union>U \<in> Rep_Exp X. {freefun U})" 
15172  348 

349 
lemma fun_respects: "(%U. {freefun U}) respects exprel" 

40822  350 
by (auto simp add: congruent_def exprel_imp_eq_freefun) 
15172  351 

352 
lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F" 

353 
apply (cases Xs rule: eq_Abs_ExpList) 

354 
apply (simp add: FnCall fun_def UN_equiv_class [OF equiv_exprel fun_respects]) 

355 
done 

356 

19736  357 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

358 
args :: "exp \<Rightarrow> exp list" where 
39910  359 
"args X = the_elem (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})" 
15172  360 

361 
text{*This result can probably be generalized to arbitrary equivalence 

362 
relations, but with little benefit here.*} 

363 
lemma Abs_ExpList_eq: 

364 
"(y, z) \<in> listrel exprel \<Longrightarrow> Abs_ExpList (y) = Abs_ExpList (z)" 

18460  365 
by (induct set: listrel) simp_all 
15172  366 

367 
lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel" 

40822  368 
by (auto simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) 
15172  369 

370 
lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs" 

371 
apply (cases Xs rule: eq_Abs_ExpList) 

372 
apply (simp add: FnCall args_def UN_equiv_class [OF equiv_exprel args_respects]) 

373 
done 

374 

375 

376 
lemma FnCall_FnCall_eq [iff]: 

377 
"(FnCall F Xs = FnCall F' Xs') = (F=F' & Xs=Xs')" 

378 
proof 

379 
assume "FnCall F Xs = FnCall F' Xs'" 

380 
hence "fun (FnCall F Xs) = fun (FnCall F' Xs')" 

381 
and "args (FnCall F Xs) = args (FnCall F' Xs')" by auto 

382 
thus "F=F' & Xs=Xs'" by simp 

383 
next 

384 
assume "F=F' & Xs=Xs'" thus "FnCall F Xs = FnCall F' Xs'" by simp 

385 
qed 

386 

387 

388 
subsection{*The Abstract Discriminator*} 

389 
text{*However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this 

390 
function in order to prove discrimination theorems.*} 

391 

19736  392 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

393 
discrim :: "exp \<Rightarrow> int" where 
39910  394 
"discrim X = the_elem (\<Union>U \<in> Rep_Exp X. {freediscrim U})" 
15172  395 

396 
lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel" 

40822  397 
by (auto simp add: congruent_def exprel_imp_eq_freediscrim) 
15172  398 

399 
text{*Now prove the four equations for @{term discrim}*} 

400 

401 
lemma discrim_Var [simp]: "discrim (Var N) = 0" 

402 
by (simp add: discrim_def Var_def 

403 
UN_equiv_class [OF equiv_exprel discrim_respects]) 

404 

405 
lemma discrim_Plus [simp]: "discrim (Plus X Y) = 1" 

406 
apply (cases X, cases Y) 

407 
apply (simp add: discrim_def Plus 

408 
UN_equiv_class [OF equiv_exprel discrim_respects]) 

409 
done 

410 

411 
lemma discrim_FnCall [simp]: "discrim (FnCall F Xs) = 2" 

412 
apply (rule_tac z=Xs in eq_Abs_ExpList) 

413 
apply (simp add: discrim_def FnCall 

414 
UN_equiv_class [OF equiv_exprel discrim_respects]) 

415 
done 

416 

417 

418 
text{*The structural induction rule for the abstract type*} 

18460  419 
theorem exp_inducts: 
15172  420 
assumes V: "\<And>nat. P1 (Var nat)" 
421 
and P: "\<And>exp1 exp2. \<lbrakk>P1 exp1; P1 exp2\<rbrakk> \<Longrightarrow> P1 (Plus exp1 exp2)" 

422 
and F: "\<And>nat list. P2 list \<Longrightarrow> P1 (FnCall nat list)" 

423 
and Nil: "P2 []" 

424 
and Cons: "\<And>exp list. \<lbrakk>P1 exp; P2 list\<rbrakk> \<Longrightarrow> P2 (exp # list)" 

18460  425 
shows "P1 exp" and "P2 list" 
426 
proof  

427 
obtain U where exp: "exp = (Abs_Exp (exprel `` {U}))" by (cases exp) 

428 
obtain Us where list: "list = Abs_ExpList Us" by (rule eq_Abs_ExpList) 

429 
have "P1 (Abs_Exp (exprel `` {U}))" and "P2 (Abs_ExpList Us)" 

15172  430 
proof (induct U and Us) 
18460  431 
case (VAR nat) 
15172  432 
with V show ?case by (simp add: Var_def) 
433 
next 

434 
case (PLUS X Y) 

435 
with P [of "Abs_Exp (exprel `` {X})" "Abs_Exp (exprel `` {Y})"] 

436 
show ?case by (simp add: Plus) 

437 
next 

438 
case (FNCALL nat list) 

439 
with F [of "Abs_ExpList list"] 

440 
show ?case by (simp add: FnCall) 

441 
next 

442 
case Nil_freeExp 

443 
with Nil show ?case by simp 

444 
next 

445 
case Cons_freeExp 

18460  446 
with Cons show ?case by simp 
15172  447 
qed 
18460  448 
with exp and list show "P1 exp" and "P2 list" by (simp_all only:) 
15172  449 
qed 
450 

451 
end 