|
1 theory Lambda |
|
2 imports "../Parser" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 nominal_datatype lm = |
|
8 Vr "name" |
|
9 | Ap "lm" "lm" |
|
10 | Lm x::"name" l::"lm" bind x in l |
|
11 |
|
12 lemmas supp_fn' = lm.fv[simplified lm.supp] |
|
13 |
|
14 (* |
|
15 Old way of establishing strong induction |
|
16 principles by chosing a fresh name. |
|
17 *) |
|
18 lemma |
|
19 fixes c::"'a::fs" |
|
20 assumes a1: "\<And>name c. P c (Vr name)" |
|
21 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
|
22 and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
|
23 shows "P c lm" |
|
24 proof - |
|
25 have "\<And>p. P c (p \<bullet> lm)" |
|
26 apply(induct lm arbitrary: c rule: lm.induct) |
|
27 apply(simp only: lm.perm) |
|
28 apply(rule a1) |
|
29 apply(simp only: lm.perm) |
|
30 apply(rule a2) |
|
31 apply(assumption) |
|
32 apply(assumption) |
|
33 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))") |
|
34 defer |
|
35 apply(simp add: fresh_def) |
|
36 apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base) |
|
37 apply(simp add: supp_Pair finite_supp) |
|
38 apply(blast) |
|
39 apply(erule exE) |
|
40 apply(rule_tac t="p \<bullet> Lm name lm" and |
|
41 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst) |
|
42 apply(simp del: lm.perm) |
|
43 apply(subst lm.perm) |
|
44 apply(subst (2) lm.perm) |
|
45 apply(rule flip_fresh_fresh) |
|
46 apply(simp add: fresh_def) |
|
47 apply(simp only: supp_fn') |
|
48 apply(simp) |
|
49 apply(simp add: fresh_Pair) |
|
50 apply(simp) |
|
51 apply(rule a3) |
|
52 apply(simp add: fresh_Pair) |
|
53 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
|
54 apply(simp) |
|
55 done |
|
56 then have "P c (0 \<bullet> lm)" by blast |
|
57 then show "P c lm" by simp |
|
58 qed |
|
59 |
|
60 (* |
|
61 New way of establishing strong induction |
|
62 principles by using a appropriate permutation. |
|
63 *) |
|
64 lemma |
|
65 fixes c::"'a::fs" |
|
66 assumes a1: "\<And>name c. P c (Vr name)" |
|
67 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
|
68 and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
|
69 shows "P c lm" |
|
70 proof - |
|
71 have "\<And>p. P c (p \<bullet> lm)" |
|
72 apply(induct lm arbitrary: c rule: lm.induct) |
|
73 apply(simp only: lm.perm) |
|
74 apply(rule a1) |
|
75 apply(simp only: lm.perm) |
|
76 apply(rule a2) |
|
77 apply(assumption) |
|
78 apply(assumption) |
|
79 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q") |
|
80 apply(erule exE) |
|
81 apply(rule_tac t="p \<bullet> Lm name lm" and |
|
82 s="q \<bullet> p \<bullet> Lm name lm" in subst) |
|
83 defer |
|
84 apply(simp add: lm.perm) |
|
85 apply(rule a3) |
|
86 apply(simp add: eqvts fresh_star_def) |
|
87 apply(drule_tac x="q + p" in meta_spec) |
|
88 apply(simp) |
|
89 apply(rule at_set_avoiding2) |
|
90 apply(simp add: finite_supp) |
|
91 apply(simp add: finite_supp) |
|
92 apply(simp add: finite_supp) |
|
93 apply(simp only: lm.perm atom_eqvt) |
|
94 apply(simp add: fresh_star_def fresh_def supp_fn') |
|
95 apply(rule supp_perm_eq) |
|
96 apply(simp) |
|
97 done |
|
98 then have "P c (0 \<bullet> lm)" by blast |
|
99 then show "P c lm" by simp |
|
100 qed |
|
101 |
|
102 end |
|
103 |
|
104 |
|
105 |