1 theory Let |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 nominal_datatype trm = |
|
8 Var "name" |
|
9 | App "trm" "trm" |
|
10 | Lam x::"name" t::"trm" binds x in t |
|
11 | Let as::"assn" t::"trm" binds "bn as" in t |
|
12 and assn = |
|
13 ANil |
|
14 | ACons "name" "trm" "assn" |
|
15 binder |
|
16 bn |
|
17 where |
|
18 "bn ANil = []" |
|
19 | "bn (ACons x t as) = (atom x) # (bn as)" |
|
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 |
|
29 thm trm_assn.fv_defs |
|
30 thm trm_assn.eq_iff |
|
31 thm trm_assn.bn_defs |
|
32 thm trm_assn.bn_inducts |
|
33 thm trm_assn.perm_simps |
|
34 thm trm_assn.induct |
|
35 thm trm_assn.inducts |
|
36 thm trm_assn.distinct |
|
37 thm trm_assn.supp |
|
38 thm trm_assn.fresh |
|
39 thm trm_assn.exhaust |
|
40 thm trm_assn.strong_exhaust |
|
41 thm trm_assn.perm_bn_simps |
|
42 |
|
43 lemma alpha_bn_inducts_raw[consumes 1]: |
|
44 "\<lbrakk>alpha_bn_raw a b; P3 ANil_raw ANil_raw; |
|
45 \<And>trm_raw trm_rawa assn_raw assn_rawa name namea. |
|
46 \<lbrakk>alpha_trm_raw trm_raw trm_rawa; alpha_bn_raw assn_raw assn_rawa; |
|
47 P3 assn_raw assn_rawa\<rbrakk> |
|
48 \<Longrightarrow> P3 (ACons_raw name trm_raw assn_raw) |
|
49 (ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b" |
|
50 by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto |
|
51 |
|
52 lemmas alpha_bn_inducts[consumes 1] = alpha_bn_inducts_raw[quot_lifted] |
|
53 |
|
54 |
|
55 |
|
56 lemma alpha_bn_refl: "alpha_bn x x" |
|
57 by (induct x rule: trm_assn.inducts(2)) |
|
58 (rule TrueI, auto simp add: trm_assn.eq_iff) |
|
59 lemma alpha_bn_sym: "alpha_bn x y \<Longrightarrow> alpha_bn y x" |
|
60 sorry |
|
61 lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z" |
|
62 sorry |
|
63 |
|
64 lemma bn_inj[rule_format]: |
|
65 assumes a: "alpha_bn x y" |
|
66 shows "bn x = bn y \<longrightarrow> x = y" |
|
67 by (rule alpha_bn_inducts[OF a]) (simp_all add: trm_assn.bn_defs) |
|
68 |
|
69 lemma bn_inj2: |
|
70 assumes a: "alpha_bn x y" |
|
71 shows "\<And>q r. (q \<bullet> bn x) = (r \<bullet> bn y) \<Longrightarrow> permute_bn q x = permute_bn r y" |
|
72 using a |
|
73 apply(induct rule: alpha_bn_inducts) |
|
74 apply(simp add: trm_assn.perm_bn_simps) |
|
75 apply(simp add: trm_assn.perm_bn_simps) |
|
76 apply(simp add: trm_assn.bn_defs) |
|
77 apply(simp add: atom_eqvt) |
|
78 done |
|
79 |
|
80 lemma Abs_lst_fcb2: |
|
81 fixes as bs :: "atom list" |
|
82 and x y :: "'b :: fs" |
|
83 and c::"'c::fs" |
|
84 assumes eq: "[as]lst. x = [bs]lst. y" |
|
85 and fcb1: "(set as) \<sharp>* c \<Longrightarrow> (set as) \<sharp>* f as x c" |
|
86 and fresh1: "set as \<sharp>* c" |
|
87 and fresh2: "set bs \<sharp>* c" |
|
88 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
|
89 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
|
90 shows "f as x c = f bs y c" |
|
91 proof - |
|
92 have "supp (as, x, c) supports (f as x c)" |
|
93 unfolding supports_def fresh_def[symmetric] |
|
94 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
|
95 then have fin1: "finite (supp (f as x c))" |
|
96 by (auto intro: supports_finite simp add: finite_supp) |
|
97 have "supp (bs, y, c) supports (f bs y c)" |
|
98 unfolding supports_def fresh_def[symmetric] |
|
99 by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh) |
|
100 then have fin2: "finite (supp (f bs y c))" |
|
101 by (auto intro: supports_finite simp add: finite_supp) |
|
102 obtain q::"perm" where |
|
103 fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and |
|
104 fr2: "supp q \<sharp>* Abs_lst as x" and |
|
105 inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)" |
|
106 using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"] |
|
107 fin1 fin2 |
|
108 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) |
|
109 have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp |
|
110 also have "\<dots> = Abs_lst as x" |
|
111 by (simp only: fr2 perm_supp_eq) |
|
112 finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp |
|
113 then obtain r::perm where |
|
114 qq1: "q \<bullet> x = r \<bullet> y" and |
|
115 qq2: "q \<bullet> as = r \<bullet> bs" and |
|
116 qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs" |
|
117 apply(drule_tac sym) |
|
118 apply(simp only: Abs_eq_iff2 alphas) |
|
119 apply(erule exE) |
|
120 apply(erule conjE)+ |
|
121 apply(drule_tac x="p" in meta_spec) |
|
122 apply(simp add: set_eqvt) |
|
123 apply(blast) |
|
124 done |
|
125 have "(set as) \<sharp>* f as x c" |
|
126 apply(rule fcb1) |
|
127 apply(rule fresh1) |
|
128 done |
|
129 then have "q \<bullet> ((set as) \<sharp>* f as x c)" |
|
130 by (simp add: permute_bool_def) |
|
131 then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
|
132 apply(simp add: fresh_star_eqvt set_eqvt) |
|
133 apply(subst (asm) perm1) |
|
134 using inc fresh1 fr1 |
|
135 apply(auto simp add: fresh_star_def fresh_Pair) |
|
136 done |
|
137 then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
138 then have "r \<bullet> ((set bs) \<sharp>* f bs y c)" |
|
139 apply(simp add: fresh_star_eqvt set_eqvt) |
|
140 apply(subst (asm) perm2[symmetric]) |
|
141 using qq3 fresh2 fr1 |
|
142 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
|
143 done |
|
144 then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
|
145 have "f as x c = q \<bullet> (f as x c)" |
|
146 apply(rule perm_supp_eq[symmetric]) |
|
147 using inc fcb1[OF fresh1] fr1 by (auto simp add: fresh_star_def) |
|
148 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
|
149 apply(rule perm1) |
|
150 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
|
151 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
152 also have "\<dots> = r \<bullet> (f bs y c)" |
|
153 apply(rule perm2[symmetric]) |
|
154 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
|
155 also have "... = f bs y c" |
|
156 apply(rule perm_supp_eq) |
|
157 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
|
158 finally show ?thesis by simp |
|
159 qed |
|
160 |
|
161 lemma Abs_lst1_fcb2: |
|
162 fixes a b :: "atom" |
|
163 and x y :: "'b :: fs" |
|
164 and c::"'c :: fs" |
|
165 assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)" |
|
166 and fcb1: "a \<sharp> c \<Longrightarrow> a \<sharp> f a x c" |
|
167 and fresh: "{a, b} \<sharp>* c" |
|
168 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
|
169 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
|
170 shows "f a x c = f b y c" |
|
171 using e |
|
172 apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"]) |
|
173 apply(simp_all) |
|
174 using fcb1 fresh perm1 perm2 |
|
175 apply(simp_all add: fresh_star_def) |
|
176 done |
|
177 |
|
178 |
|
179 function |
|
180 apply_assn2 :: "(trm \<Rightarrow> trm) \<Rightarrow> assn \<Rightarrow> assn" |
|
181 where |
|
182 "apply_assn2 f ANil = ANil" |
|
183 | "apply_assn2 f (ACons x t as) = ACons x (f t) (apply_assn2 f as)" |
|
184 apply(case_tac x) |
|
185 apply(case_tac b rule: trm_assn.exhaust(2)) |
|
186 apply(simp_all) |
|
187 apply(blast) |
|
188 done |
|
189 |
|
190 termination by lexicographic_order |
|
191 |
|
192 lemma apply_assn_eqvt[eqvt]: |
|
193 "p \<bullet> (apply_assn2 f a) = apply_assn2 (p \<bullet> f) (p \<bullet> a)" |
|
194 apply(induct f a rule: apply_assn2.induct) |
|
195 apply simp_all |
|
196 apply(perm_simp) |
|
197 apply rule |
|
198 done |
|
199 |
|
200 lemma |
|
201 fixes x y :: "'a :: fs" |
|
202 shows "[a # as]lst. x = [b # bs]lst. y \<Longrightarrow> [[a]]lst. [as]lst. x = [[b]]lst. [bs]lst. y" |
|
203 apply (simp add: Abs_eq_iff) |
|
204 apply (elim exE) |
|
205 apply (rule_tac x="p" in exI) |
|
206 apply (simp add: alphas) |
|
207 apply clarify |
|
208 apply rule |
|
209 apply (simp add: supp_Abs) |
|
210 apply blast |
|
211 apply (simp add: supp_Abs fresh_star_def) |
|
212 apply blast |
|
213 done |
|
214 |
|
215 lemma |
|
216 assumes neq: "a \<noteq> b" "sort_of a = sort_of b" |
|
217 shows "[[a]]lst. [[a]]lst. a = [[a]]lst. [[b]]lst. b \<and> [[a, a]]lst. a \<noteq> [[a, b]]lst. b" |
|
218 apply (simp add: Abs1_eq_iff) |
|
219 apply rule |
|
220 apply (simp add: Abs_eq_iff alphas supp_atom fresh_star_def) |
|
221 apply (rule_tac x="(a \<rightleftharpoons> b)" in exI) |
|
222 apply (simp add: neq) |
|
223 apply (simp add: Abs_eq_iff alphas supp_atom fresh_star_def neq) |
|
224 done |
|
225 |
|
226 nominal_primrec |
|
227 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
|
228 where |
|
229 "subst s t (Var x) = (if (s = x) then t else (Var x))" |
|
230 | "subst s t (App l r) = App (subst s t l) (subst s t r)" |
|
231 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)" |
|
232 | "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (apply_assn2 (subst s t) as) (subst s t b)" |
|
233 apply (simp only: eqvt_def subst_graph_def) |
|
234 apply (rule, perm_simp, rule) |
|
235 apply (rule TrueI) |
|
236 apply (case_tac x) |
|
237 apply (rule_tac y="c" and c="(a,b)" in trm_assn.strong_exhaust(1)) |
|
238 apply (auto simp add: fresh_star_def)[3] |
|
239 apply (drule_tac x="assn" in meta_spec) |
|
240 apply (simp add: Abs1_eq_iff alpha_bn_refl) |
|
241 apply auto[7] |
|
242 prefer 2 |
|
243 apply(simp) |
|
244 thm subst_sumC_def |
|
245 thm THE_default_def |
|
246 thm theI |
|
247 apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2) |
|
248 apply (simp add: Abs_fresh_iff) |
|
249 apply (simp add: fresh_star_def) |
|
250 apply (simp_all add: fresh_star_Pair_elim perm_supp_eq eqvt_at_def)[2] |
|
251 apply (subgoal_tac "apply_assn2 (\<lambda>x2\<Colon>trm. subst_sumC (sa, ta, x2)) asa |
|
252 = apply_assn2 (\<lambda>x2\<Colon>trm. subst_sumC (sa, ta, x2)) as") |
|
253 prefer 2 |
|
254 apply (erule alpha_bn_inducts) |
|
255 apply simp |
|
256 apply (simp only: apply_assn2.simps) |
|
257 apply simp |
|
258 --"We know nothing about names; not true; but we can apply fcb2" |
|
259 defer |
|
260 apply (simp only: ) |
|
261 apply (erule_tac c="(sa, ta)" in Abs_lst_fcb2) |
|
262 --"We again need induction for fcb assumption; this time true" |
|
263 apply (induct_tac as rule: trm_assn.inducts(2)) |
|
264 apply (rule TrueI)+ |
|
265 apply (simp_all add: trm_assn.bn_defs fresh_star_def)[2] |
|
266 apply (auto simp add: Abs_fresh_iff)[1] |
|
267 apply assumption+ |
|
268 --"But eqvt is not going to be true as well" |
|
269 apply (simp add: fresh_star_Pair_elim perm_supp_eq eqvt_at_def trm_assn.fv_bn_eqvt) |
|
270 apply (simp add: apply_assn_eqvt) |
|
271 apply (drule sym) |
|
272 apply (subgoal_tac "p \<bullet> (\<lambda>x2\<Colon>trm. subst_sumC (sa, ta, x2)) = (\<lambda>x2\<Colon>trm. subst_sumC (sa, ta, x2))") |
|
273 apply (simp) |
|
274 apply (erule alpha_bn_inducts) |
|
275 apply simp |
|
276 apply simp |
|
277 apply (simp add: trm_assn.bn_defs) |
|
278 --"Again we cannot relate 'namea' with 'p \<bullet> name'" |
|
279 prefer 4 |
|
280 apply (erule alpha_bn_inducts) |
|
281 apply simp_all[2] |
|
282 oops |
|
283 |
|
284 end |
|