equal
deleted
inserted
replaced
45 fixes p q::perm |
45 fixes p q::perm |
46 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
46 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
47 unfolding fresh_star_def |
47 unfolding fresh_star_def |
48 by (simp add: fresh_plus) |
48 by (simp add: fresh_plus) |
49 |
49 |
50 |
50 lemma supp_finite_set: |
|
51 fixes S::"atom set" |
|
52 assumes "finite S" |
|
53 shows "supp S = S" |
|
54 apply(rule finite_supp_unique) |
|
55 apply(simp add: supports_def) |
|
56 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
57 apply(metis) |
|
58 apply(rule assms) |
|
59 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
60 done |
|
61 |
51 |
62 |
52 atom_decl name |
63 atom_decl name |
53 |
64 |
54 datatype rlam = |
65 datatype rlam = |
55 rVar "name" |
66 rVar "name" |
242 done |
253 done |
243 |
254 |
244 inductive |
255 inductive |
245 alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
256 alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
246 where |
257 where |
247 a1: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)" |
258 a21: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)" |
248 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2" |
259 | a22: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2" |
249 | a3: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s" |
260 | a23: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s" |
|
261 |
|
262 lemma fv_vars: |
|
263 fixes a::name |
|
264 assumes a1: "\<forall>x \<in> rfv t - {atom a}. pi \<bullet> x = x" |
|
265 shows "(pi \<bullet> t) \<approx>2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)" |
|
266 using a1 |
|
267 apply(induct t) |
|
268 apply(auto) |
|
269 apply(rule a21) |
|
270 apply(case_tac "name = a") |
|
271 apply(simp) |
|
272 apply(simp) |
|
273 defer |
|
274 apply(rule a22) |
|
275 apply(simp) |
|
276 apply(simp) |
|
277 apply(rule a23) |
|
278 apply(case_tac "a = name") |
|
279 apply(simp) |
|
280 oops |
|
281 |
250 |
282 |
251 lemma |
283 lemma |
252 assumes a1: "t \<approx>2 s" |
284 assumes a1: "t \<approx>2 s" |
253 shows "t \<approx> s" |
285 shows "t \<approx> s" |
254 using a1 |
286 using a1 |
270 apply(erule conjE)+ |
302 apply(erule conjE)+ |
271 apply(rule conjI) |
303 apply(rule conjI) |
272 apply(drule alpha_rfv) |
304 apply(drule alpha_rfv) |
273 apply(drule sym) |
305 apply(drule sym) |
274 apply(simp) |
306 apply(simp) |
|
307 apply(simp add: rfv_eqvt[symmetric]) |
275 defer |
308 defer |
276 apply(subgoal_tac "atom a \<sharp> (rfv t - {atom a})") |
309 apply(subgoal_tac "atom a \<sharp> (rfv t - {atom a})") |
277 apply(subgoal_tac "atom b \<sharp> (rfv t - {atom a})") |
310 apply(subgoal_tac "atom b \<sharp> (rfv t - {atom a})") |
|
311 |
278 defer |
312 defer |
279 sorry |
313 sorry |
280 |
314 |
281 lemma |
315 lemma |
282 assumes a1: "t \<approx> s" |
316 assumes a1: "t \<approx> s" |
298 apply(simp) |
332 apply(simp) |
299 apply(case_tac "a = pi \<bullet> a") |
333 apply(case_tac "a = pi \<bullet> a") |
300 apply(simp) |
334 apply(simp) |
301 defer |
335 defer |
302 apply(simp) |
336 apply(simp) |
|
337 apply(simp add: fresh_star_def) |
303 sorry |
338 sorry |
304 |
339 |
305 quotient_type lam = rlam / alpha |
340 quotient_type lam = rlam / alpha |
306 by (rule alpha_equivp) |
341 by (rule alpha_equivp) |
307 |
342 |