equal
deleted
inserted
replaced
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 print_theorems |
|
22 |
|
23 thm alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros |
|
24 thm bn_raw.simps |
|
25 thm permute_bn_raw.simps |
|
26 thm trm_assn.perm_bn_alpha |
|
27 thm trm_assn.permute_bn |
|
28 |
21 thm trm_assn.fv_defs |
29 thm trm_assn.fv_defs |
22 thm trm_assn.eq_iff |
30 thm trm_assn.eq_iff |
23 thm trm_assn.bn_defs |
31 thm trm_assn.bn_defs |
24 thm trm_assn.bn_inducts |
32 thm trm_assn.bn_inducts |
25 thm trm_assn.perm_simps |
33 thm trm_assn.perm_simps |
26 thm trm_assn.induct |
34 thm trm_assn.induct |
27 thm trm_assn.inducts |
35 thm trm_assn.inducts |
115 shows "\<exists>p.([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c)" |
123 shows "\<exists>p.([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c)" |
116 apply (rule_tac x="(a \<leftrightarrow> b)" in exI) |
124 apply (rule_tac x="(a \<leftrightarrow> b)" in exI) |
117 apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt) |
125 apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt) |
118 by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y) |
126 by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y) |
119 |
127 |
|
128 |
120 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
129 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
121 by (simp add: permute_pure) |
130 by (simp add: permute_pure) |
|
131 |
|
132 (* TODO: should be provided by nominal *) |
|
133 lemmas [eqvt] = trm_assn.fv_bn_eqvt |
|
134 thm trm_assn.fv_bn_eqvt |
|
135 |
|
136 |
|
137 thm Abs_lst_fcb |
122 |
138 |
123 lemma Abs_lst_fcb2: |
139 lemma Abs_lst_fcb2: |
124 fixes as bs :: "'a :: fs" |
140 fixes as bs :: "'a :: fs" |
125 and x y :: "'b :: fs" |
141 and x y :: "'b :: fs" |
126 and c::"'c::fs" |
142 and c::"'c::fs" |
129 and fresh1: "set (ba as) \<sharp>* c" |
145 and fresh1: "set (ba as) \<sharp>* c" |
130 and fresh2: "set (ba bs) \<sharp>* c" |
146 and fresh2: "set (ba bs) \<sharp>* c" |
131 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
147 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
132 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
148 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
133 (* What we would like in this proof, and lets this proof finish *) |
149 (* What we would like in this proof, and lets this proof finish *) |
134 and bainj: "\<And>q r. q \<bullet> ba as = r \<bullet> ba bs \<Longrightarrow> q \<bullet> as = r \<bullet> bs" |
150 and ba_inj: "\<And>q r. q \<bullet> ba as = r \<bullet> ba bs \<Longrightarrow> q \<bullet> as = r \<bullet> bs" |
135 (* What the user can supply with the help of alpha_bn *) |
151 (* What the user can supply with the help of alpha_bn *) |
136 (* and bainj: "ba as = ba bs \<Longrightarrow> as = bs"*) |
152 (* and bainj: "ba as = ba bs \<Longrightarrow> as = bs"*) |
137 shows "f as x c = f bs y c" |
153 shows "f as x c = f bs y c" |
138 proof - |
154 proof - |
139 have "supp (as, x, c) supports (f as x c)" |
155 have "supp (as, x, c) supports (f as x c)" |
176 apply(simp add: fresh_star_eqvt set_eqvt) |
192 apply(simp add: fresh_star_eqvt set_eqvt) |
177 apply(subst (asm) perm1) |
193 apply(subst (asm) perm1) |
178 using inc fresh1 fr1 |
194 using inc fresh1 fr1 |
179 apply(auto simp add: fresh_star_def fresh_Pair) |
195 apply(auto simp add: fresh_star_def fresh_Pair) |
180 done |
196 done |
181 then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 bainj |
197 then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 ba_inj |
182 by simp |
198 by simp |
183 then have "r \<bullet> ((set (ba bs)) \<sharp>* f bs y c)" |
199 then have "r \<bullet> ((set (ba bs)) \<sharp>* f bs y c)" |
184 apply(simp add: fresh_star_eqvt set_eqvt) |
200 apply(simp add: fresh_star_eqvt set_eqvt) |
185 apply(subst (asm) perm2[symmetric]) |
201 apply(subst (asm) perm2[symmetric]) |
186 using qq3 fresh2 fr1 |
202 using qq3 fresh2 fr1 |
191 apply(rule perm_supp_eq[symmetric]) |
207 apply(rule perm_supp_eq[symmetric]) |
192 using inc fcb1 fr1 by (auto simp add: fresh_star_def) |
208 using inc fcb1 fr1 by (auto simp add: fresh_star_def) |
193 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
209 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
194 apply(rule perm1) |
210 apply(rule perm1) |
195 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
211 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
196 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 bainj by simp |
212 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 ba_inj by simp |
197 also have "\<dots> = r \<bullet> (f bs y c)" |
213 also have "\<dots> = r \<bullet> (f bs y c)" |
198 apply(rule perm2[symmetric]) |
214 apply(rule perm2[symmetric]) |
199 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
215 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
200 also have "... = f bs y c" |
216 also have "... = f bs y c" |
201 apply(rule perm_supp_eq) |
217 apply(rule perm_supp_eq) |