16 bn |
16 bn |
17 where |
17 where |
18 "bn ANil = []" |
18 "bn ANil = []" |
19 | "bn (ACons x t as) = (atom x) # (bn as)" |
19 | "bn (ACons x t as) = (atom x) # (bn as)" |
20 |
20 |
|
21 |
21 thm trm_assn.fv_defs |
22 thm trm_assn.fv_defs |
22 thm trm_assn.eq_iff trm_assn.bn_defs |
23 thm trm_assn.eq_iff |
23 thm trm_assn.bn_defs |
24 thm trm_assn.bn_defs |
24 thm trm_assn.perm_simps |
25 thm trm_assn.perm_simps |
25 thm trm_assn.induct[no_vars] |
26 thm trm_assn.induct |
26 thm trm_assn.inducts[no_vars] |
27 thm trm_assn.inducts |
27 thm trm_assn.distinct |
28 thm trm_assn.distinct |
28 thm trm_assn.supp |
29 thm trm_assn.supp |
29 thm trm_assn.fv_defs[simplified trm_assn.supp(1-2)] |
30 |
30 |
|
31 |
|
32 |
|
33 lemma fv_supp: |
|
34 shows "fv_trm = supp" |
|
35 and "fv_assn = supp" |
|
36 apply(rule ext) |
|
37 apply(rule trm_assn.supp) |
|
38 apply(rule ext) |
|
39 apply(rule trm_assn.supp) |
|
40 done |
|
41 |
|
42 lemmas eq_iffs = trm_assn.eq_iff[folded fv_supp[symmetric], folded Abs_eq_iff] |
|
43 |
|
44 lemmas supps = trm_assn.fv_defs[simplified trm_assn.supp(1-2)] |
|
45 |
31 |
46 lemma supp_fresh_eq: |
32 lemma supp_fresh_eq: |
47 assumes "supp x = supp y" |
33 assumes "supp x = supp y" |
48 shows "a \<sharp> x \<longleftrightarrow> a \<sharp> y" |
34 shows "a \<sharp> x \<longleftrightarrow> a \<sharp> y" |
49 using assms |
35 using assms by (simp add: fresh_def) |
50 by (simp add: fresh_def) |
|
51 |
36 |
52 lemma supp_not_in: |
37 lemma supp_not_in: |
53 assumes "x = y" |
38 assumes "x = y" |
54 shows "a \<notin> x \<longleftrightarrow> a \<notin> y" |
39 shows "a \<notin> x \<longleftrightarrow> a \<notin> y" |
55 using assms |
40 using assms |
56 by (simp add: fresh_def) |
41 by (simp add: fresh_def) |
57 |
42 |
58 lemmas freshs = |
43 lemmas freshs = |
59 supps(1)[THEN supp_not_in, folded fresh_def] |
44 trm_assn.supp(1)[THEN supp_not_in, folded fresh_def] |
60 supps(2)[THEN supp_not_in, simplified, folded fresh_def] |
45 trm_assn.supp(2)[THEN supp_not_in, simplified, folded fresh_def] |
61 supps(3)[THEN supp_not_in, folded fresh_def] |
46 trm_assn.supp(3)[THEN supp_not_in, folded fresh_def] |
62 supps(4)[THEN supp_not_in, folded fresh_def] |
47 trm_assn.supp(4)[THEN supp_not_in, folded fresh_def] |
63 supps(5)[THEN supp_not_in, simplified, folded fresh_def] |
48 trm_assn.supp(5)[THEN supp_not_in, simplified, folded fresh_def] |
64 supps(6)[THEN supp_not_in, simplified, folded fresh_def] |
49 trm_assn.supp(6)[THEN supp_not_in, simplified, folded fresh_def] |
65 |
50 |
66 lemma fin_bn: |
51 lemma fin_bn: |
67 shows "finite (set (bn l))" |
52 shows "finite (set (bn l))" |
68 apply(induct l rule: trm_assn.inducts(2)) |
53 apply(induct l rule: trm_assn.inducts(2)) |
69 apply(simp_all) |
54 apply(simp_all) |