1 theory Lambda |
1 theory Lambda |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 declare [[STEPS = 100]] |
|
7 |
6 |
8 nominal_datatype lam = |
7 nominal_datatype lam = |
9 Var "name" |
8 Var "name" |
10 | App "lam" "lam" |
9 | App "lam" "lam" |
11 | Lam x::"name" l::"lam" bind x in l |
10 | Lam x::"name" l::"lam" bind x in l |
12 |
11 |
13 thm lam.distinct |
12 thm lam.distinct |
14 thm lam.induct |
13 thm lam.induct |
15 thm lam.exhaust |
14 thm lam.exhaust lam.strong_exhaust |
16 thm lam.fv_defs |
15 thm lam.fv_defs |
17 thm lam.bn_defs |
16 thm lam.bn_defs |
18 thm lam.perm_simps |
17 thm lam.perm_simps |
19 thm lam.eq_iff |
18 thm lam.eq_iff |
20 thm lam.eq_iff[folded alphas] |
|
21 thm lam.fv_bn_eqvt |
19 thm lam.fv_bn_eqvt |
22 thm lam.size_eqvt |
20 thm lam.size_eqvt |
23 |
21 |
24 |
22 |
25 section {* Strong Exhausts Lemma and Strong Induction Lemma via Induct_schema *} |
23 section {* Strong Induction Lemma via Induct_schema *} |
26 |
|
27 lemma strong_exhaust: |
|
28 fixes c::"'a::fs" |
|
29 assumes "\<And>name. \<lbrakk>y = Var name\<rbrakk> \<Longrightarrow> P" |
|
30 and "\<And>lam1 lam2. \<lbrakk>y = App lam1 lam2\<rbrakk> \<Longrightarrow> P" |
|
31 and "\<And>name lam. \<lbrakk>atom name \<sharp> c; y = Lam name lam\<rbrakk> \<Longrightarrow> P" |
|
32 shows "P" |
|
33 apply(rule_tac y="y" in lam.exhaust) |
|
34 apply(rule assms(1)) |
|
35 apply(assumption) |
|
36 apply(rule assms(2)) |
|
37 apply(assumption) |
|
38 apply(subgoal_tac "\<exists>q. (q \<bullet> (atom name)) \<sharp> c \<and> supp (Lam name lam) \<sharp>* q") |
|
39 apply(erule exE) |
|
40 apply(erule conjE) |
|
41 apply(rule assms(3)) |
|
42 apply(simp add: atom_eqvt) |
|
43 apply(clarify) |
|
44 apply(drule supp_perm_eq[symmetric]) |
|
45 apply(simp) |
|
46 apply(rule at_set_avoiding2_atom) |
|
47 apply(simp add: finite_supp) |
|
48 apply(simp add: finite_supp) |
|
49 apply(simp add: lam.fresh) |
|
50 done |
|
51 |
24 |
52 |
25 |
53 lemma strong_induct: |
26 lemma strong_induct: |
54 fixes c::"'a::fs" |
27 fixes c::"'a::fs" |
55 assumes a1: "\<And>name c. P c (Var name)" |
28 assumes a1: "\<And>name c. P c (Var name)" |
56 and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)" |
29 and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)" |
57 and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
30 and a3: "\<And>name lam c. \<lbrakk>{atom name} \<sharp>* c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
58 shows "P c lam" |
31 shows "P c lam" |
59 using assms |
32 using assms |
60 apply(induction_schema) |
33 apply(induction_schema) |
61 apply(rule_tac y="lam" in strong_exhaust) |
34 apply(rule_tac y="lam" in lam.strong_exhaust) |
62 apply(blast) |
35 apply(blast) |
63 apply(blast) |
36 apply(blast) |
64 apply(blast) |
37 apply(blast) |
65 apply(relation "measure (\<lambda>(x,y). size y)") |
38 apply(relation "measure (\<lambda>(x,y). size y)") |
66 apply(simp_all add: lam.size) |
39 apply(simp_all add: lam.size) |
67 done |
40 done |
68 |
|
69 section {* Strong Induction Principles*} |
|
70 |
|
71 (* |
|
72 Old way of establishing strong induction |
|
73 principles by chosing a fresh name. |
|
74 *) |
|
75 (* |
|
76 lemma |
|
77 fixes c::"'a::fs" |
|
78 assumes a1: "\<And>name c. P c (Var name)" |
|
79 and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)" |
|
80 and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
|
81 shows "P c lam" |
|
82 proof - |
|
83 have "\<And>p. P c (p \<bullet> lam)" |
|
84 apply(induct lam arbitrary: c rule: lam.induct) |
|
85 apply(perm_simp) |
|
86 apply(rule a1) |
|
87 apply(perm_simp) |
|
88 apply(rule a2) |
|
89 apply(assumption) |
|
90 apply(assumption) |
|
91 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lam (p \<bullet> name) (p \<bullet> lam))") |
|
92 defer |
|
93 apply(simp add: fresh_def) |
|
94 apply(rule_tac X="supp (c, Lam (p \<bullet> name) (p \<bullet> lam))" in obtain_at_base) |
|
95 apply(simp add: supp_Pair finite_supp) |
|
96 apply(blast) |
|
97 apply(erule exE) |
|
98 apply(rule_tac t="p \<bullet> Lam name lam" and |
|
99 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lam name lam" in subst) |
|
100 apply(simp del: lam.perm) |
|
101 apply(subst lam.perm) |
|
102 apply(subst (2) lam.perm) |
|
103 apply(rule flip_fresh_fresh) |
|
104 apply(simp add: fresh_def) |
|
105 apply(simp only: supp_fn') |
|
106 apply(simp) |
|
107 apply(simp add: fresh_Pair) |
|
108 apply(simp) |
|
109 apply(rule a3) |
|
110 apply(simp add: fresh_Pair) |
|
111 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
|
112 apply(simp) |
|
113 done |
|
114 then have "P c (0 \<bullet> lam)" by blast |
|
115 then show "P c lam" by simp |
|
116 qed |
|
117 *) |
|
118 (* |
|
119 New way of establishing strong induction |
|
120 principles by using a appropriate permutation. |
|
121 *) |
|
122 (* |
|
123 lemma |
|
124 fixes c::"'a::fs" |
|
125 assumes a1: "\<And>name c. P c (Var name)" |
|
126 and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)" |
|
127 and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
|
128 shows "P c lam" |
|
129 proof - |
|
130 have "\<And>p. P c (p \<bullet> lam)" |
|
131 apply(induct lam arbitrary: c rule: lam.induct) |
|
132 apply(perm_simp) |
|
133 apply(rule a1) |
|
134 apply(perm_simp) |
|
135 apply(rule a2) |
|
136 apply(assumption) |
|
137 apply(assumption) |
|
138 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q") |
|
139 apply(erule exE) |
|
140 apply(rule_tac t="p \<bullet> Lam name lam" and |
|
141 s="q \<bullet> p \<bullet> Lam name lam" in subst) |
|
142 defer |
|
143 apply(simp) |
|
144 apply(rule a3) |
|
145 apply(simp add: eqvts fresh_star_def) |
|
146 apply(drule_tac x="q + p" in meta_spec) |
|
147 apply(simp) |
|
148 apply(rule at_set_avoiding2) |
|
149 apply(simp add: finite_supp) |
|
150 apply(simp add: finite_supp) |
|
151 apply(simp add: finite_supp) |
|
152 apply(perm_simp) |
|
153 apply(simp add: fresh_star_def fresh_def supp_fn') |
|
154 apply(rule supp_perm_eq) |
|
155 apply(simp) |
|
156 done |
|
157 then have "P c (0 \<bullet> lam)" by blast |
|
158 then show "P c lam" by simp |
|
159 qed |
|
160 *) |
|
161 |
41 |
162 section {* Typing *} |
42 section {* Typing *} |
163 |
43 |
164 nominal_datatype ty = |
44 nominal_datatype ty = |
165 TVar string |
45 TVar string |