20 "bn (As x y t) = [atom x]" |
20 "bn (As x y t) = [atom x]" |
21 |
21 |
22 thm single_let.distinct |
22 thm single_let.distinct |
23 thm single_let.induct |
23 thm single_let.induct |
24 thm single_let.inducts |
24 thm single_let.inducts |
25 thm single_let.exhaust[no_vars] |
25 thm single_let.exhaust |
|
26 thm single_let.strong_exhaust |
26 thm single_let.fv_defs |
27 thm single_let.fv_defs |
27 thm single_let.bn_defs |
28 thm single_let.bn_defs |
28 thm single_let.perm_simps |
29 thm single_let.perm_simps |
29 thm single_let.eq_iff |
30 thm single_let.eq_iff |
30 thm single_let.fv_bn_eqvt |
31 thm single_let.fv_bn_eqvt |
32 thm single_let.supports |
33 thm single_let.supports |
33 thm single_let.fsupp |
34 thm single_let.fsupp |
34 thm single_let.supp |
35 thm single_let.supp |
35 thm single_let.fresh |
36 thm single_let.fresh |
36 |
37 |
37 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
|
38 |
|
39 lemma uu: |
|
40 shows "alpha_bn as (permute_bn p as)" |
|
41 apply(induct as rule: single_let.inducts(2)) |
|
42 apply(auto)[7] |
|
43 apply(simp add: permute_bn) |
|
44 apply(simp add: single_let.eq_iff) |
|
45 done |
|
46 |
|
47 lemma tt: |
|
48 shows "(p \<bullet> bn as) = bn (permute_bn p as)" |
|
49 apply(induct as rule: single_let.inducts(2)) |
|
50 apply(auto)[7] |
|
51 apply(simp add: permute_bn single_let.bn_defs) |
|
52 apply(simp add: atom_eqvt) |
|
53 done |
|
54 |
|
55 lemma Abs_fresh_star': |
|
56 fixes x::"'a::fs" |
|
57 shows "set bs = as \<Longrightarrow> as \<sharp>* Abs_lst bs x" |
|
58 unfolding fresh_star_def |
|
59 by(simp_all add: Abs_fresh_iff) |
|
60 |
|
61 lemma strong_exhaust: |
|
62 fixes c::"'a::fs" |
|
63 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
64 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
65 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
66 and "\<And>assg trm. \<lbrakk>set (bn assg) \<sharp>* c; y = Let assg trm\<rbrakk> \<Longrightarrow> P" |
|
67 and "\<And>name1 name2 trm1 trm2 trm3. \<lbrakk>{atom name1} \<sharp>* c; y = Foo name1 name2 trm1 trm2 trm3\<rbrakk> \<Longrightarrow> P" |
|
68 and "\<And>name1 name2 trm. \<lbrakk>{atom name1, atom name2} \<sharp>* c; y = Bar name1 name2 trm\<rbrakk> \<Longrightarrow> P" |
|
69 and "\<And>name trm1 trm2. \<lbrakk>{atom name} \<sharp>* c; y = Baz name trm1 trm2\<rbrakk> \<Longrightarrow> P" |
|
70 shows "P" |
|
71 apply(rule_tac y="y" in single_let.exhaust(1)) |
|
72 apply(rule assms(1)) |
|
73 apply(assumption) |
|
74 apply(rule assms(2)) |
|
75 apply(assumption) |
|
76 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp ([[atom name]]lst.trm) \<sharp>* q") |
|
77 apply(erule exE) |
|
78 apply(erule conjE) |
|
79 apply(perm_simp) |
|
80 apply(rule assms(3)) |
|
81 apply(assumption) |
|
82 apply(drule supp_perm_eq[symmetric]) |
|
83 apply(simp add: single_let.eq_iff) |
|
84 apply(perm_simp) |
|
85 apply(rule refl) |
|
86 apply(rule at_set_avoiding2) |
|
87 apply(simp add: finite_supp) |
|
88 apply(simp add: finite_supp) |
|
89 apply(simp add: finite_supp) |
|
90 apply(simp add: Abs_fresh_star') |
|
91 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg))) \<sharp>* (c::'a::fs) \<and> supp ([bn assg]lst.trm) \<sharp>* q") |
|
92 apply(erule exE) |
|
93 apply(erule conjE) |
|
94 apply(perm_simp add: tt) |
|
95 apply(rule_tac assms(4)) |
|
96 apply(assumption) |
|
97 apply(drule supp_perm_eq[symmetric]) |
|
98 apply(simp add: single_let.eq_iff) |
|
99 apply(simp add: tt uu) |
|
100 apply(rule at_set_avoiding2) |
|
101 apply(simp add: finite_supp) |
|
102 apply(simp add: finite_supp) |
|
103 apply(simp add: finite_supp) |
|
104 apply(simp add: Abs_fresh_star) |
|
105 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* (c::'a::fs) \<and> |
|
106 supp ([{atom name1}]set.(((name2, trm1), trm2), trm3)) \<sharp>* q") |
|
107 apply(erule exE) |
|
108 apply(erule conjE) |
|
109 apply(perm_simp add: tt) |
|
110 apply(rule_tac assms(5)) |
|
111 apply(assumption) |
|
112 apply(drule supp_perm_eq[symmetric]) |
|
113 apply(simp add: single_let.eq_iff) |
|
114 apply(perm_simp) |
|
115 apply(rule refl) |
|
116 apply(rule at_set_avoiding2) |
|
117 apply(simp add: finite_supp) |
|
118 apply(simp add: finite_supp) |
|
119 apply(simp add: finite_supp) |
|
120 apply(simp add: Abs_fresh_star) |
|
121 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name1, atom name2}) \<sharp>* (c::'a::fs) \<and> |
|
122 supp ([[atom name2, atom name1]]lst.((trm, name1), name2)) \<sharp>* q") |
|
123 apply(erule exE) |
|
124 apply(erule conjE) |
|
125 apply(perm_simp add: tt) |
|
126 apply(rule_tac assms(6)) |
|
127 apply(assumption) |
|
128 apply(drule supp_perm_eq[symmetric]) |
|
129 apply(simp add: single_let.eq_iff) |
|
130 apply(perm_simp) |
|
131 apply(rule refl) |
|
132 apply(rule at_set_avoiding2) |
|
133 apply(simp add: finite_supp) |
|
134 apply(simp add: finite_supp) |
|
135 apply(simp add: finite_supp) |
|
136 oops |
|
137 |
|
138 |
38 |
139 end |
39 end |
140 |
40 |
141 |
41 |
142 |
42 |