40 thm foo.supports |
40 thm foo.supports |
41 thm foo.fsupp |
41 thm foo.fsupp |
42 thm foo.supp |
42 thm foo.supp |
43 thm foo.fresh |
43 thm foo.fresh |
44 |
44 |
|
45 primrec |
|
46 permute_bn1_raw |
|
47 where |
|
48 "permute_bn1_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t" |
|
49 |
|
50 primrec |
|
51 permute_bn2_raw |
|
52 where |
|
53 "permute_bn2_raw p (As_raw x y t) = As_raw x (p \<bullet> y) t" |
|
54 |
|
55 primrec |
|
56 permute_bn3_raw |
|
57 where |
|
58 "permute_bn3_raw p (As_raw x y t) = As_raw (p \<bullet> x) (p \<bullet> y) t" |
|
59 |
|
60 quotient_definition |
|
61 "permute_bn1 :: perm \<Rightarrow> assg \<Rightarrow> assg" |
|
62 is |
|
63 "permute_bn1_raw" |
|
64 |
|
65 quotient_definition |
|
66 "permute_bn2 :: perm \<Rightarrow> assg \<Rightarrow> assg" |
|
67 is |
|
68 "permute_bn2_raw" |
|
69 |
|
70 quotient_definition |
|
71 "permute_bn3 :: perm \<Rightarrow> assg \<Rightarrow> assg" |
|
72 is |
|
73 "permute_bn3_raw" |
|
74 |
|
75 lemma [quot_respect]: |
|
76 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw" |
|
77 apply simp |
|
78 apply clarify |
|
79 apply (erule alpha_assg_raw.cases) |
|
80 apply simp_all |
|
81 apply (rule foo.raw_alpha) |
|
82 apply simp_all |
|
83 done |
|
84 |
|
85 lemma [quot_respect]: |
|
86 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw" |
|
87 apply simp |
|
88 apply clarify |
|
89 apply (erule alpha_assg_raw.cases) |
|
90 apply simp_all |
|
91 apply (rule foo.raw_alpha) |
|
92 apply simp_all |
|
93 done |
|
94 |
|
95 lemma [quot_respect]: |
|
96 shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw" |
|
97 apply simp |
|
98 apply clarify |
|
99 apply (erule alpha_assg_raw.cases) |
|
100 apply simp_all |
|
101 apply (rule foo.raw_alpha) |
|
102 apply simp_all |
|
103 done |
|
104 |
|
105 lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted] |
|
106 lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted] |
|
107 lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted] |
|
108 |
|
109 lemma uu1: |
|
110 shows "alpha_bn1 as (permute_bn1 p as)" |
|
111 apply(induct as rule: foo.inducts(2)) |
|
112 apply(auto)[6] |
|
113 apply(simp add: permute_bn1) |
|
114 apply(simp add: foo.eq_iff) |
|
115 done |
|
116 |
|
117 lemma uu2: |
|
118 shows "alpha_bn2 as (permute_bn2 p as)" |
|
119 apply(induct as rule: foo.inducts(2)) |
|
120 apply(auto)[6] |
|
121 apply(simp add: permute_bn2) |
|
122 apply(simp add: foo.eq_iff) |
|
123 done |
|
124 |
|
125 lemma uu3: |
|
126 shows "alpha_bn3 as (permute_bn3 p as)" |
|
127 apply(induct as rule: foo.inducts(2)) |
|
128 apply(auto)[6] |
|
129 apply(simp add: permute_bn3) |
|
130 apply(simp add: foo.eq_iff) |
|
131 done |
|
132 |
|
133 lemma tt1: |
|
134 shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)" |
|
135 apply(induct as rule: foo.inducts(2)) |
|
136 apply(auto)[6] |
|
137 apply(simp add: permute_bn1 foo.bn_defs) |
|
138 apply(simp add: atom_eqvt) |
|
139 done |
|
140 |
|
141 lemma tt2: |
|
142 shows "(p \<bullet> bn2 as) = bn2 (permute_bn2 p as)" |
|
143 apply(induct as rule: foo.inducts(2)) |
|
144 apply(auto)[6] |
|
145 apply(simp add: permute_bn2 foo.bn_defs) |
|
146 apply(simp add: atom_eqvt) |
|
147 done |
|
148 |
|
149 lemma tt3: |
|
150 shows "(p \<bullet> bn3 as) = bn3 (permute_bn3 p as)" |
|
151 apply(induct as rule: foo.inducts(2)) |
|
152 apply(auto)[6] |
|
153 apply(simp add: permute_bn3 foo.bn_defs) |
|
154 apply(simp add: atom_eqvt) |
|
155 done |
|
156 |
|
157 |
|
158 lemma strong_exhaust1: |
|
159 fixes c::"'a::fs" |
|
160 assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P" |
|
161 and "\<And>trm1 trm2 ca. \<lbrakk>c = ca; y = App trm1 trm2\<rbrakk> \<Longrightarrow> P" |
|
162 and "\<And>name trm ca. \<lbrakk>{atom name} \<sharp>* ca; c = ca; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
163 and "\<And>assn trm ca. \<lbrakk>set (bn1 assn) \<sharp>* ca; c = ca; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
|
164 and "\<And>assn trm ca. \<lbrakk>set (bn2 assn) \<sharp>* ca; c = ca; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
|
165 and "\<And>assn trm ca. \<lbrakk>set (bn3 assn) \<sharp>* ca; c = ca; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
|
166 shows "P" |
|
167 apply(rule_tac y="y" in foo.exhaust(1)) |
|
168 apply(rule assms(1)) |
|
169 apply(auto)[2] |
|
170 apply(rule assms(2)) |
|
171 apply(auto)[2] |
|
172 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
|
173 apply(erule exE) |
|
174 apply(erule conjE) |
|
175 apply(rule assms(3)) |
|
176 apply(perm_simp) |
|
177 apply(assumption) |
|
178 apply(rule refl) |
|
179 apply(drule supp_perm_eq[symmetric]) |
|
180 apply(simp) |
|
181 apply(rule at_set_avoiding2) |
|
182 apply(simp add: finite_supp) |
|
183 apply(simp add: finite_supp) |
|
184 apply(simp add: finite_supp) |
|
185 apply(simp add: foo.fresh fresh_star_def) |
|
186 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn1 assg))) \<sharp>* c \<and> supp ([bn1 assg]lst.trm) \<sharp>* q") |
|
187 apply(erule exE) |
|
188 apply(erule conjE) |
|
189 apply(rule assms(4)) |
|
190 apply(simp add: set_eqvt) |
|
191 apply(simp add: tt1) |
|
192 apply(rule refl) |
|
193 apply(simp) |
|
194 apply(simp add: foo.eq_iff) |
|
195 apply(drule supp_perm_eq[symmetric]) |
|
196 apply(simp) |
|
197 apply(simp add: tt1 uu1) |
|
198 apply(rule at_set_avoiding2) |
|
199 apply(simp add: finite_supp) |
|
200 apply(simp add: finite_supp) |
|
201 apply(simp add: finite_supp) |
|
202 apply(simp add: Abs_fresh_star) |
|
203 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q") |
|
204 apply(erule exE) |
|
205 apply(erule conjE) |
|
206 apply(rule assms(5)) |
|
207 apply(simp add: set_eqvt) |
|
208 apply(simp add: tt2) |
|
209 apply(rule refl) |
|
210 apply(simp) |
|
211 apply(simp add: foo.eq_iff) |
|
212 apply(drule supp_perm_eq[symmetric]) |
|
213 apply(simp) |
|
214 apply(simp add: tt2 uu2) |
|
215 apply(rule at_set_avoiding2) |
|
216 apply(simp add: finite_supp) |
|
217 apply(simp add: finite_supp) |
|
218 apply(simp add: finite_supp) |
|
219 apply(simp add: Abs_fresh_star) |
|
220 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn3 assg))) \<sharp>* c \<and> supp ([bn3 assg]lst.trm) \<sharp>* q") |
|
221 apply(erule exE) |
|
222 apply(erule conjE) |
|
223 apply(rule assms(6)) |
|
224 apply(simp add: set_eqvt) |
|
225 apply(simp add: tt3) |
|
226 apply(rule refl) |
|
227 apply(simp) |
|
228 apply(simp add: foo.eq_iff) |
|
229 apply(drule supp_perm_eq[symmetric]) |
|
230 apply(simp) |
|
231 apply(simp add: tt3 uu3) |
|
232 apply(rule at_set_avoiding2) |
|
233 apply(simp add: finite_supp) |
|
234 apply(simp add: finite_supp) |
|
235 apply(simp add: finite_supp) |
|
236 apply(simp add: Abs_fresh_star) |
|
237 done |
|
238 |
|
239 thm foo.exhaust |
|
240 |
|
241 lemma strong_exhaust2: |
|
242 assumes "\<And>x y t ca. \<lbrakk>c = ca; as = As x y t\<rbrakk> \<Longrightarrow> P" |
|
243 shows "P" |
|
244 apply(rule_tac y="as" in foo.exhaust(2)) |
|
245 apply(rule assms(1)) |
|
246 apply(auto)[2] |
|
247 done |
|
248 |
|
249 |
|
250 lemma |
|
251 fixes t::trm |
|
252 and as::assg |
|
253 and c::"'a::fs" |
|
254 assumes a1: "\<And>x c. P1 c (Var x)" |
|
255 and a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)" |
|
256 and a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)" |
|
257 and a4: "\<And>as t c. \<lbrakk>set (bn1 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let1 as t)" |
|
258 and a5: "\<And>as t c. \<lbrakk>set (bn2 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let2 as t)" |
|
259 and a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)" |
|
260 and a7: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" |
|
261 shows "P1 c t" "P2 c as" |
|
262 using assms |
|
263 apply(induction_schema) |
|
264 apply(rule_tac y="t" in strong_exhaust1) |
|
265 apply(blast) |
|
266 apply(blast) |
|
267 apply(blast) |
|
268 apply(blast) |
|
269 apply(blast) |
|
270 apply(blast) |
|
271 apply(rule_tac as="as" in strong_exhaust2) |
|
272 apply(blast) |
|
273 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))") |
|
274 apply(auto)[1] |
|
275 apply(simp_all add: foo.size) |
|
276 done |
45 |
277 |
46 end |
278 end |
47 |
279 |
48 |
280 |
49 |
281 |