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 thm at_set_avoiding2 |
|
22 thm trm_assn.fv_defs |
21 thm trm_assn.fv_defs |
23 thm trm_assn.eq_iff |
22 thm trm_assn.eq_iff |
24 thm trm_assn.bn_defs |
23 thm trm_assn.bn_defs |
25 thm trm_assn.perm_simps |
24 thm trm_assn.perm_simps |
26 thm trm_assn.induct |
25 thm trm_assn.induct |
27 thm trm_assn.inducts |
26 thm trm_assn.inducts |
28 thm trm_assn.distinct |
27 thm trm_assn.distinct |
29 thm trm_assn.supp |
28 thm trm_assn.supp |
30 thm trm_assn.fresh |
29 thm trm_assn.fresh |
31 thm trm_assn.exhaust[where y="t", no_vars] |
30 thm trm_assn.exhaust |
32 |
31 thm trm_assn.strong_exhaust |
33 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
|
34 |
|
35 lemma uu: |
|
36 shows "alpha_bn as (permute_bn p as)" |
|
37 apply(induct as rule: trm_assn.inducts(2)) |
|
38 apply(auto)[4] |
|
39 apply(simp add: permute_bn) |
|
40 apply(simp add: trm_assn.eq_iff) |
|
41 apply(simp add: permute_bn) |
|
42 apply(simp add: trm_assn.eq_iff) |
|
43 done |
|
44 |
|
45 lemma tt: |
|
46 shows "(p \<bullet> bn as) = bn (permute_bn p as)" |
|
47 apply(induct as rule: trm_assn.inducts(2)) |
|
48 apply(auto)[4] |
|
49 apply(simp add: permute_bn trm_assn.bn_defs) |
|
50 apply(simp add: permute_bn trm_assn.bn_defs) |
|
51 apply(simp add: atom_eqvt) |
|
52 done |
|
53 |
32 |
54 lemma strong_exhaust1: |
33 lemma strong_exhaust1: |
55 fixes c::"'a::fs" |
34 fixes c::"'a::fs" |
56 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
35 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
57 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
36 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
58 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
37 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
59 and "\<And>assn trm. \<lbrakk>set (bn assn) \<sharp>* c; y = Let assn trm\<rbrakk> \<Longrightarrow> P" |
38 and "\<And>assn trm. \<lbrakk>set (bn assn) \<sharp>* c; y = Let assn trm\<rbrakk> \<Longrightarrow> P" |
60 shows "P" |
39 shows "P" |
61 apply(rule_tac y="y" in trm_assn.exhaust(1)) |
40 apply(rule_tac y="y" in trm_assn.strong_exhaust(1)) |
62 apply(rule assms(1)) |
41 apply(rule assms(1)) |
63 apply(assumption) |
42 apply(assumption) |
64 apply(rule assms(2)) |
43 apply(rule assms(2)) |
65 apply(assumption) |
44 apply(assumption) |
66 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
|
67 apply(erule exE) |
|
68 apply(erule conjE) |
|
69 apply(rule assms(3)) |
45 apply(rule assms(3)) |
70 apply(perm_simp) |
46 apply(assumption) |
71 apply(assumption) |
47 apply(assumption) |
72 apply(drule supp_perm_eq[symmetric]) |
48 apply(rule assms(4)) |
73 apply(simp) |
49 apply(assumption) |
74 apply(rule at_set_avoiding2) |
50 apply(assumption) |
75 apply(simp add: finite_supp) |
51 sorry |
76 apply(simp add: finite_supp) |
|
77 apply(simp add: finite_supp) |
|
78 apply(simp add: trm_assn.fresh fresh_star_def) |
|
79 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q") |
|
80 apply(erule exE) |
|
81 apply(erule conjE) |
|
82 apply(simp add: set_eqvt) |
|
83 apply(subst (asm) tt) |
|
84 apply(rule_tac assms(4)) |
|
85 apply(simp) |
|
86 apply(simp add: trm_assn.eq_iff) |
|
87 apply(drule supp_perm_eq[symmetric]) |
|
88 apply(simp) |
|
89 apply(simp add: tt uu) |
|
90 apply(rule at_set_avoiding2) |
|
91 apply(simp add: finite_supp) |
|
92 apply(simp add: finite_supp) |
|
93 apply(simp add: finite_supp) |
|
94 apply(simp add: Abs_fresh_star) |
|
95 done |
|
96 |
52 |
97 |
53 |
98 lemma strong_exhaust2: |
54 lemma strong_exhaust2: |
99 assumes "as = ANil \<Longrightarrow> P" |
55 assumes "as = ANil \<Longrightarrow> P" |
100 and "\<And>x t assn. \<lbrakk>as = ACons x t assn\<rbrakk> \<Longrightarrow> P" |
56 and "\<And>x t assn. \<lbrakk>as = ACons x t assn\<rbrakk> \<Longrightarrow> P" |