1 theory Lambda imports "../Nominal2" begin |
|
2 |
|
3 atom_decl name |
|
4 |
|
5 nominal_datatype lam = |
|
6 Var "name" |
|
7 | App "lam" "lam" |
|
8 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
|
9 |
|
10 nominal_primrec lookup where |
|
11 "lookup (n :: name) m [] \<longleftrightarrow> (n = m)" |
|
12 | "lookup n m ((hn, hm) # t) \<longleftrightarrow> |
|
13 (n, m) = (hn, hm) \<or> (n \<noteq> hn \<and> m \<noteq> hm \<and> lookup n m t)" |
|
14 apply (simp add: eqvt_def lookup_graph_def) |
|
15 apply (rule, perm_simp, rule, rule) |
|
16 by pat_completeness auto |
|
17 |
|
18 termination (eqvt) by lexicographic_order |
|
19 |
|
20 nominal_primrec lam2_rec where |
|
21 "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs" |
|
22 | "lam2_rec faa fll xs (Var n) (App l r) = False" |
|
23 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False" |
|
24 | "lam2_rec faa fll xs (App l r) (Var n) = False" |
|
25 | "lam2_rec faa fll xs (App l1 r1) (App l2 r2) = faa l1 r1 l2 r2" |
|
26 | "lam2_rec faa fll xs (App l r) (Lam [x]. t) = False" |
|
27 | "lam2_rec faa fll xs (Lam [x]. t) (Var n) = False" |
|
28 | "lam2_rec faa fll xs (Lam [x]. t) (App l1 r1) = False" |
|
29 | "(atom x \<sharp> (xs, Lam [y]. s) \<and> atom y \<sharp> (x, xs, Lam [x]. t) \<and> |
|
30 (\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s' |
|
31 \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow> |
|
32 lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = fll x t y s" |
|
33 | "(atom x \<sharp> (xs, Lam [y]. s) \<and> atom y \<sharp> (x, xs, Lam [x]. t) \<and> |
|
34 \<not>(\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s' |
|
35 \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow> |
|
36 lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = False" |
|
37 apply (simp add: eqvt_def lam2_rec_graph_def) |
|
38 apply (rule, perm_simp, rule, rule) |
|
39 apply (case_tac x) |
|
40 apply (rule_tac y="d" and c="(c, e)" in lam.strong_exhaust) |
|
41 apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust) |
|
42 apply simp_all[3] apply (metis, metis, metis) |
|
43 apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust) |
|
44 apply simp_all[3] apply (metis, metis, metis) |
|
45 apply (rule_tac y="e" and c="(name, c, d)" in lam.strong_exhaust) |
|
46 apply simp_all[2] apply (metis, metis) |
|
47 unfolding fresh_star_def |
|
48 apply (thin_tac "\<And>faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \<Longrightarrow> P") |
|
49 apply (thin_tac "\<And>faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \<Longrightarrow> P") |
|
50 apply (thin_tac "\<And>faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \<Longrightarrow> P") |
|
51 apply (thin_tac "\<And>faa fll xs l1 r1 l2 r2. x = (faa, fll, xs, App l1 r1, App l2 r2) \<Longrightarrow> P") |
|
52 apply (thin_tac "\<And>faa fll xs l r n. x = (faa, fll, xs, App l r, Var n) \<Longrightarrow> P") |
|
53 apply (thin_tac "\<And>faa fll xs l r xa t. x = (faa, fll, xs, App l r, Lam [xa]. t) \<Longrightarrow> P") |
|
54 apply (thin_tac "\<And>faa fll xs xa t n. x = (faa, fll, xs, Lam [xa]. t, Var n) \<Longrightarrow> P") |
|
55 apply (thin_tac "\<And>faa fll xs xa t l1 r1. x = (faa, fll, xs, Lam [xa]. t, App l1 r1) \<Longrightarrow> P") |
|
56 apply (drule_tac x="name" in meta_spec)+ |
|
57 apply (drule_tac x="c" in meta_spec)+ |
|
58 apply (drule_tac x="namea" in meta_spec)+ |
|
59 apply (drule_tac x="lama" in meta_spec) |
|
60 apply (drule_tac x="lama" in meta_spec) |
|
61 apply (drule_tac x="lam" in meta_spec)+ |
|
62 apply (drule_tac x="b" in meta_spec)+ |
|
63 apply (drule_tac x="a" in meta_spec)+ |
|
64 apply (case_tac "(\<forall>x' y' t' s'. atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow> |
|
65 atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
|
66 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s')") |
|
67 apply clarify |
|
68 apply (simp) |
|
69 apply (simp only: fresh_Pair_elim) |
|
70 apply blast |
|
71 apply (simp_all)[53] |
|
72 apply clarify |
|
73 apply metis |
|
74 apply simp |
|
75 done |
|
76 |
|
77 termination (eqvt) by lexicographic_order |
|
78 |
|
79 lemma lam_rec2_cong[fundef_cong]: |
|
80 "(\<And>s1 s2 s3 s4. l = App s1 s2 \<Longrightarrow> l2 = App s3 s4 \<Longrightarrow> faa s1 s2 s3 s4 = faa' s1 s2 s3 s4) \<Longrightarrow> |
|
81 (\<And>n t n' t'. l = Lam [n]. t \<Longrightarrow> l2 = Lam [n']. t' \<Longrightarrow> fll n t n' t' = fll' n t n' t') \<Longrightarrow> |
|
82 lam2_rec faa fll xs l l2 = lam2_rec faa' fll' xs l l2" |
|
83 apply (rule_tac y="l" and c="(xs, l2)" in lam.strong_exhaust) |
|
84 apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3] |
|
85 apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3] |
|
86 apply (rule_tac y="l2" and c="(name, xs, l)" in lam.strong_exhaust) |
|
87 apply auto[2] |
|
88 apply clarify |
|
89 apply (case_tac "(\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> |
|
90 atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
|
91 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> fll name lam namea lama = fll x' t' y' s')") |
|
92 unfolding fresh_star_def |
|
93 apply (subst lam2_rec.simps) apply simp |
|
94 apply (subst lam2_rec.simps) apply simp |
|
95 apply metis |
|
96 apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def) |
|
97 apply (subst lam2_rec.simps(10)) apply (simp_all add: fresh_star_def) |
|
98 done |
|
99 |
|
100 nominal_primrec aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" |
|
101 where |
|
102 [simp del]: "aux l r xs = lam2_rec |
|
103 (%t1 t2 t3 t4. (aux t1 t3 xs) \<and> (aux t2 t4 xs)) |
|
104 (%x t y s. aux t s ((x, y) # xs)) xs l r" |
|
105 unfolding eqvt_def aux_graph_def |
|
106 apply (rule, perm_simp, rule, rule) |
|
107 by pat_completeness auto |
|
108 |
|
109 termination (eqvt) |
|
110 by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all |
|
111 |
|
112 lemma aux_simps[simp]: |
|
113 "aux (Var x) (Var y) xs = lookup x y xs" |
|
114 "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)" |
|
115 "aux (Var x) (App t1 t2) xs = False" |
|
116 "aux (Var x) (Lam [y].t) xs = False" |
|
117 "aux (App t1 t2) (Var x) xs = False" |
|
118 "aux (App t1 t2) (Lam [x].t) xs = False" |
|
119 "aux (Lam [x].t) (Var y) xs = False" |
|
120 "aux (Lam [x].t) (App t1 t2) xs = False" |
|
121 "\<lbrakk>atom x \<sharp> (s, xs); atom y \<sharp> (x, t, xs)\<rbrakk> \<Longrightarrow> aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)" |
|
122 apply (subst aux.simps, simp) |
|
123 apply (subst aux.simps, simp) |
|
124 apply (subst aux.simps, simp) |
|
125 apply (subst aux.simps, simp) |
|
126 apply (subst aux.simps, simp) |
|
127 apply (subst aux.simps, simp) |
|
128 apply (subst aux.simps, simp) |
|
129 apply (subst aux.simps, simp) |
|
130 apply (subst aux.simps) |
|
131 apply (subst lam2_rec.simps) |
|
132 apply (rule, simp add: lam.fresh) |
|
133 apply (rule, simp add: lam.fresh) |
|
134 apply (intro allI impI) |
|
135 apply (rule_tac x="(x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh) |
|
136 apply (rule_tac x="(a, x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh) |
|
137 apply (rule_tac s="aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) s ((a, y) # xs)" in trans) |
|
138 apply (rule_tac s="(atom x \<rightleftharpoons> atom a) \<bullet> aux t s ((x, y) # xs)" in trans) |
|
139 apply (rule permute_pure[symmetric]) |
|
140 apply (simp add: eqvts swap_fresh_fresh) |
|
141 apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim) |
|
142 apply (rename_tac b) |
|
143 apply (rule_tac s="aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) ((atom y \<rightleftharpoons> atom b) \<bullet> s) ((a, b) # xs)" in trans) |
|
144 apply (rule_tac s="(atom y \<rightleftharpoons> atom b) \<bullet> aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) s ((a, y) # xs)" in trans) |
|
145 apply (rule permute_pure[symmetric]) |
|
146 apply (simp add: eqvts swap_fresh_fresh) |
|
147 apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim) |
|
148 apply (subst permute_eqvt) |
|
149 apply (simp add: eqvts swap_fresh_fresh) |
|
150 apply (rule sym) |
|
151 apply (rule_tac s="aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') s' ((a, y') # xs)" in trans) |
|
152 apply (rule_tac s="(atom x' \<rightleftharpoons> atom a) \<bullet> aux t' s' ((x', y') # xs)" in trans) |
|
153 apply (rule permute_pure[symmetric]) |
|
154 apply (simp add: eqvts swap_fresh_fresh) |
|
155 apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim swap_fresh_fresh) |
|
156 apply (rule_tac s="aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') ((atom y' \<rightleftharpoons> atom b) \<bullet> s') ((a, b) # xs)" in trans) |
|
157 apply (rule_tac s="(atom y' \<rightleftharpoons> atom b) \<bullet> aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') s' ((a, y') # xs)" in trans) |
|
158 apply (rule permute_pure[symmetric]) |
|
159 apply (simp add: eqvts swap_fresh_fresh) |
|
160 apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim swap_fresh_fresh) |
|
161 apply (subst permute_eqvt) |
|
162 apply (simp add: eqvts swap_fresh_fresh) |
|
163 apply (subgoal_tac "(atom x' \<rightleftharpoons> atom a) \<bullet> t' = (atom x \<rightleftharpoons> atom a) \<bullet> t") |
|
164 apply (subgoal_tac "(atom y' \<rightleftharpoons> atom b) \<bullet> s' = (atom y \<rightleftharpoons> atom b) \<bullet> s") |
|
165 apply simp |
|
166 apply (subgoal_tac "Lam [y]. s = Lam [b]. ((atom y \<rightleftharpoons> atom b) \<bullet> s)") |
|
167 apply (subgoal_tac "Lam [y']. s' = Lam [b]. ((atom y' \<rightleftharpoons> atom b) \<bullet> s')") |
|
168 apply (auto simp add: fresh_Pair_elim Abs1_eq_iff)[1] |
|
169 apply (rule sym) |
|
170 apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute) |
|
171 apply (rule sym) |
|
172 apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute) |
|
173 apply (subgoal_tac "Lam [x]. t = Lam [a]. ((atom x \<rightleftharpoons> atom a) \<bullet> t)") |
|
174 apply (subgoal_tac "Lam [x']. t' = Lam [a]. ((atom x' \<rightleftharpoons> atom a) \<bullet> t')") |
|
175 apply (auto simp add: fresh_Pair_elim Abs1_eq_iff)[1] |
|
176 apply (rule sym) |
|
177 apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute) |
|
178 apply (rule sym) |
|
179 apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute) |
|
180 apply (rule refl) |
|
181 done |
|
182 |
|
183 lemma aux_induct: "\<lbrakk>\<And>xs n m. P xs (Var n) (Var m); \<And>xs n l r. P xs (Var n) (App l r); |
|
184 \<And>xs n x t. P xs (Var n) (Lam [x]. t); |
|
185 \<And>xs l r n. P xs (App l r) (Var n); |
|
186 (\<And>xs l1 r1 l2 r2. P xs l1 l2 \<Longrightarrow> P xs r1 r2 \<Longrightarrow> P xs (App l1 r1) (App l2 r2)); |
|
187 \<And>xs l r x t. P xs (App l r) (Lam [x]. t); |
|
188 \<And>xs x t n. P xs (Lam [x]. t) (Var n); |
|
189 \<And>xs x t l1 r1. P xs (Lam [x]. t) (App l1 r1); |
|
190 \<And>x xs y s t. |
|
191 atom x \<sharp> (xs, Lam [y]. s) \<and> |
|
192 atom y \<sharp> (x, xs, Lam [x]. t) \<Longrightarrow> P ((x, y) # xs) t s \<Longrightarrow> P xs (Lam [x]. t) (Lam [y]. s)\<rbrakk> |
|
193 \<Longrightarrow> P (a :: (name \<times> name) list) b c" |
|
194 apply (induction_schema) |
|
195 apply (rule_tac y="b" and c="(a, c)" in lam.strong_exhaust) |
|
196 apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust) |
|
197 apply simp_all[3] apply (metis) |
|
198 apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust) |
|
199 apply simp_all[3] apply (metis, metis, metis) |
|
200 apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust) |
|
201 apply simp_all[3] apply (metis) |
|
202 apply (simp add: fresh_star_def) |
|
203 apply metis |
|
204 apply lexicographic_order |
|
205 done |
|
206 |
|
207 nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where |
|
208 "swapequal l r [] \<longleftrightarrow> l = r" |
|
209 | "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow> |
|
210 swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t" |
|
211 unfolding eqvt_def swapequal_graph_def |
|
212 apply (rule, perm_simp, rule, rule TrueI) |
|
213 apply (case_tac x) |
|
214 apply (case_tac c) |
|
215 apply metis |
|
216 apply (case_tac aa) |
|
217 apply (rename_tac l r lst h t hl hr) |
|
218 apply (rule_tac x="(l, r, hl, hr, t)" and ?'a="name" in obtain_fresh) |
|
219 apply simp |
|
220 apply simp |
|
221 apply simp |
|
222 apply clarify |
|
223 apply (rule_tac s="(x \<leftrightarrow> xa) \<bullet> swapequal_sumC ((hla \<leftrightarrow> x) \<bullet> la, (hra \<leftrightarrow> x) \<bullet> ra, ta)" in trans) |
|
224 apply (simp only: permute_pure) |
|
225 apply (simp add: eqvt_at_def fresh_Pair_elim) |
|
226 apply (simp add: flip_fresh_fresh) |
|
227 apply (subgoal_tac "(x \<leftrightarrow> xa) \<bullet> (hla \<leftrightarrow> x) \<bullet> la = (hla \<leftrightarrow> xa) \<bullet> la") |
|
228 apply (subgoal_tac "(x \<leftrightarrow> xa) \<bullet> (hra \<leftrightarrow> x) \<bullet> ra = (hra \<leftrightarrow> xa) \<bullet> ra") |
|
229 apply simp |
|
230 apply (subst permute_eqvt) |
|
231 apply (simp add: flip_fresh_fresh flip_eqvt) |
|
232 apply (subst permute_eqvt) |
|
233 apply (simp add: flip_fresh_fresh flip_eqvt) |
|
234 done |
|
235 |
|
236 termination (eqvt) by lexicographic_order |
|
237 |
|
238 lemma var_eq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> swapequal (Var ab) (Var ab) xs" |
|
239 apply (induct xs) |
|
240 apply simp |
|
241 apply (case_tac a) |
|
242 apply (simp add: fresh_Cons) |
|
243 apply (rule_tac x="(ab, aa, b, xs)" and ?'a="name" in obtain_fresh) |
|
244 apply (subst swapequal.simps) |
|
245 apply (simp add: fresh_Pair lam.fresh) |
|
246 apply (simp add: fresh_Pair_elim) |
|
247 by (metis flip_at_base_simps(3) fresh_Pair fresh_at_base(2)) |
|
248 |
|
249 lemma var_neq_swapequal: |
|
250 "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var ab) (Var m) xs" |
|
251 "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs" |
|
252 apply (induct xs arbitrary: m) |
|
253 apply simp_all[2] |
|
254 apply (case_tac [!] a) |
|
255 apply (simp_all add: fresh_Cons) |
|
256 apply (rule_tac [!] x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh) |
|
257 apply (subst swapequal.simps) |
|
258 apply (auto simp add: fresh_Pair lam.fresh)[1] |
|
259 apply (elim conjE) |
|
260 apply (simp add: fresh_Pair_elim fresh_at_base permute_flip_at) |
|
261 apply (subst swapequal.simps) |
|
262 apply (auto simp add: fresh_Pair lam.fresh)[1] |
|
263 apply (elim conjE) |
|
264 apply (simp add: fresh_Pair_elim fresh_at_base permute_flip_at) |
|
265 done |
|
266 |
|
267 lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs" |
|
268 apply (induct xs arbitrary: m n) |
|
269 apply simp |
|
270 apply (case_tac a) |
|
271 apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh) |
|
272 apply simp |
|
273 apply (subst swapequal.simps) |
|
274 apply (simp add: fresh_Pair lam.fresh fresh_Nil) |
|
275 by (metis (hide_lams, mono_tags) flip_at_base_simps(3) flip_at_simps(1) fresh_Pair fresh_at_base(2) lam.perm_simps(1) var_eq_swapequal var_neq_swapequal(1) var_neq_swapequal(2)) |
|
276 |
|
277 lemma swapequal_reorder: " |
|
278 a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow> |
|
279 swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)" |
|
280 apply (rule_tac x="(a, b, x, y, t, s, xs)" and ?'a="name" in obtain_fresh) |
|
281 apply (rule_tac x="(a, b, x, y, t, s, xs, aa)" and ?'a="name" in obtain_fresh) |
|
282 apply (rename_tac f g) |
|
283 apply (simp add: fresh_Pair_elim fresh_at_base) |
|
284 apply (subst swapequal.simps) |
|
285 apply (auto simp add: fresh_Pair fresh_Cons fresh_at_base)[1] |
|
286 apply (subgoal_tac "(x \<leftrightarrow> f) \<bullet> atom g \<sharp> t") |
|
287 apply (subst swapequal.simps) |
|
288 apply (simp add: fresh_Pair fresh_Cons fresh_permute_left) |
|
289 apply rule apply assumption |
|
290 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
|
291 apply (subst swapequal.simps) |
|
292 apply (simp add: fresh_Pair fresh_Cons fresh_at_base) |
|
293 apply rule apply (rotate_tac 12) |
|
294 apply assumption |
|
295 apply (simp add: fresh_Pair fresh_Cons fresh_at_base) |
|
296 apply (subst swapequal.simps) |
|
297 apply (simp add: fresh_Pair fresh_Cons fresh_at_base fresh_permute_left) |
|
298 apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> atom f \<sharp> t") |
|
299 apply rule apply assumption |
|
300 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
|
301 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
|
302 apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> (x \<leftrightarrow> f) \<bullet> t = (x \<leftrightarrow> f) \<bullet> (a \<leftrightarrow> g) \<bullet> t") |
|
303 apply (subgoal_tac "(b \<leftrightarrow> g) \<bullet> (y \<leftrightarrow> f) \<bullet> s = (y \<leftrightarrow> f) \<bullet> (b \<leftrightarrow> g) \<bullet> s") |
|
304 apply simp |
|
305 apply (subst permute_eqvt) apply (simp add: flip_eqvt) |
|
306 apply (subst permute_eqvt) apply (simp add: flip_eqvt) |
|
307 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
|
308 done |
|
309 |
|
310 lemma swapequal_lambda: |
|
311 assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs" |
|
312 shows "swapequal (Lam [x]. t) (Lam [y]. s) xs = swapequal t s ((x, y) # xs)" |
|
313 using assms |
|
314 apply (induct xs arbitrary: t s x y) |
|
315 apply (rule_tac x="(x, y, t, s)" and ?'a="name" in obtain_fresh) |
|
316 apply (simp add: fresh_Pair_elim fresh_Nil) |
|
317 apply (subst swapequal.simps) |
|
318 apply (simp add: fresh_Pair fresh_Nil) |
|
319 apply auto[1] |
|
320 apply simp |
|
321 apply (subgoal_tac "[[atom x]]lst. t = [[atom a]]lst. ((x \<leftrightarrow> a) \<bullet> t)") |
|
322 apply (subgoal_tac "[[atom y]]lst. s = [[atom a]]lst. ((y \<leftrightarrow> a) \<bullet> s)") |
|
323 apply simp |
|
324 apply (simp add: Abs1_eq_iff) |
|
325 apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[2] |
|
326 apply (simp add: fresh_permute_left) |
|
327 apply (simp add: fresh_permute_left) |
|
328 apply clarify |
|
329 apply (simp add: fresh_Cons fresh_Pair fresh_at_base) |
|
330 apply clarify |
|
331 apply (simp add: swapequal_reorder) |
|
332 apply (rule_tac x="(x, y, t, s, a, b, xs)" and ?'a="name" in obtain_fresh) |
|
333 apply (rename_tac f) |
|
334 apply (subst (2) swapequal.simps) |
|
335 apply (auto simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)[1] |
|
336 apply (subst swapequal.simps) |
|
337 apply (auto simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)[1] |
|
338 apply (simp add: flip_def fresh_Pair_elim fresh_at_base) |
|
339 done |
|
340 |
|
341 lemma distinct_swapequal: "\<forall>p q. p \<bullet> l \<noteq> q \<bullet> r \<Longrightarrow> \<not>swapequal l r xs" |
|
342 apply (induct xs rule:swapequal.induct) |
|
343 apply auto[1] |
|
344 apply (simp add: fresh_Pair_elim) |
|
345 apply (subgoal_tac "\<forall>(p\<Colon>perm) q\<Colon>perm. p \<bullet> (hl \<leftrightarrow> x) \<bullet> l \<noteq> q \<bullet> (hr \<leftrightarrow> x) \<bullet> r") |
|
346 apply simp |
|
347 apply (intro allI) |
|
348 apply (drule_tac x="p + (hl \<leftrightarrow> x)" in spec) |
|
349 apply (drule_tac x="q + (hr \<leftrightarrow> x)" in spec) |
|
350 apply simp |
|
351 done |
|
352 |
|
353 lemma swapequal_app: "(swapequal l1 l2 xs \<and> swapequal r1 r2 xs) = swapequal (App l1 r1) (App l2 r2) xs" |
|
354 apply (induct xs arbitrary: l1 l2 r1 r2) |
|
355 apply simp |
|
356 apply (case_tac a) |
|
357 apply simp |
|
358 apply (rule_tac x="(l1, l2, r1, r2, aa, b, xs)" and ?'a="name" in obtain_fresh) |
|
359 apply (simp add: fresh_Pair_elim) |
|
360 apply (subst swapequal.simps) apply (auto simp add: fresh_Pair)[1] |
|
361 apply (subst swapequal.simps) apply (auto simp add: fresh_Pair lam.fresh) |
|
362 done |
|
363 |
|
364 lemma [simp]: "distinct (map fst xs) \<Longrightarrow> distinct xs" |
|
365 by (induct xs) auto |
|
366 |
|
367 lemma [simp]: |
|
368 "atom x \<sharp> xs \<Longrightarrow> x \<notin> fst ` set xs" |
|
369 "atom x \<sharp> xs \<Longrightarrow> x \<notin> snd ` set xs" |
|
370 apply (induct xs) |
|
371 apply simp_all |
|
372 apply (case_tac [!] a) |
|
373 apply (simp_all add: fresh_Cons fresh_Pair fresh_at_base) |
|
374 done |
|
375 |
|
376 lemma aux_alphaish: |
|
377 assumes "distinct (map fst xs @ map snd xs)" |
|
378 shows "aux x y xs \<longleftrightarrow> swapequal x y xs" |
|
379 using assms |
|
380 apply (induct xs x y rule: aux_induct) |
|
381 apply (simp add: lookup_swapequal) |
|
382 apply (simp, rule distinct_swapequal, simp)+ |
|
383 apply (simp add: swapequal_app) |
|
384 apply (simp, rule distinct_swapequal, simp)+ |
|
385 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base conjE) |
|
386 apply (elim conjE) |
|
387 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base) |
|
388 apply (subgoal_tac "x \<notin> fst ` set xs \<and> |
|
389 x \<notin> snd ` set xs \<and> y \<notin> snd ` set xs \<and> y \<notin> fst ` set xs") |
|
390 apply (subst swapequal_lambda) |
|
391 apply auto[2] |
|
392 apply simp |
|
393 done |
|
394 |
|
395 lemma aux_is_alpha: |
|
396 "aux x y [] \<longleftrightarrow> (x = y)" |
|
397 by (simp_all add: supp_Nil aux_alphaish) |
|
398 |
|
399 end |
|
400 |
|
401 |
|
402 |
|