1 theory Lambda |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 nominal_datatype lam = |
|
8 Var "name" |
|
9 | App "lam" "lam" |
|
10 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
|
11 |
|
12 lemma fresh_fun_eqvt_app3: |
|
13 assumes a: "eqvt f" |
|
14 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
|
15 shows "a \<sharp> f x y z" |
|
16 using fresh_fun_eqvt_app[OF a b(1)] a b |
|
17 by (metis fresh_fun_app) |
|
18 |
|
19 lemma fresh_fun_eqvt_app4: |
|
20 assumes a: "eqvt f" |
|
21 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" "a \<sharp> w" |
|
22 shows "a \<sharp> f x y z w" |
|
23 using fresh_fun_eqvt_app[OF a b(1)] a b |
|
24 by (metis fresh_fun_app) |
|
25 |
|
26 lemma the_default_pty: |
|
27 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
|
28 and unique: "\<exists>!y. G x y" |
|
29 and pty: "\<And>x y. G x y \<Longrightarrow> P x y" |
|
30 shows "P x (f x)" |
|
31 apply(subst f_def) |
|
32 apply (rule ex1E[OF unique]) |
|
33 apply (subst THE_default1_equality[OF unique]) |
|
34 apply assumption |
|
35 apply (rule pty) |
|
36 apply assumption |
|
37 done |
|
38 |
|
39 lemma Abs_lst1_fcb2: |
|
40 fixes a b :: "'a :: at" |
|
41 and S T :: "'b :: fs" |
|
42 and c::"'c::fs" |
|
43 assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)" |
|
44 and fcb: "\<And>a T. atom a \<sharp> f a T c" |
|
45 and fresh: "{atom a, atom b} \<sharp>* c" |
|
46 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c" |
|
47 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c" |
|
48 shows "f a T c = f b S c" |
|
49 proof - |
|
50 have fin1: "finite (supp (f a T c))" |
|
51 apply(rule_tac S="supp (a, T, c)" in supports_finite) |
|
52 apply(simp add: supports_def) |
|
53 apply(simp add: fresh_def[symmetric]) |
|
54 apply(clarify) |
|
55 apply(subst perm1) |
|
56 apply(simp add: supp_swap fresh_star_def) |
|
57 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
58 apply(simp add: finite_supp) |
|
59 done |
|
60 have fin2: "finite (supp (f b S c))" |
|
61 apply(rule_tac S="supp (b, S, c)" in supports_finite) |
|
62 apply(simp add: supports_def) |
|
63 apply(simp add: fresh_def[symmetric]) |
|
64 apply(clarify) |
|
65 apply(subst perm2) |
|
66 apply(simp add: supp_swap fresh_star_def) |
|
67 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
68 apply(simp add: finite_supp) |
|
69 done |
|
70 obtain d::"'a::at" where fr: "atom d \<sharp> (a, b, S, T, c, f a T c, f b S c)" |
|
71 using obtain_fresh'[where x="(a, b, S, T, c, f a T c, f b S c)"] |
|
72 apply(auto simp add: finite_supp supp_Pair fin1 fin2) |
|
73 done |
|
74 have "(a \<leftrightarrow> d) \<bullet> (Abs_lst [atom a] T) = (b \<leftrightarrow> d) \<bullet> (Abs_lst [atom b] S)" |
|
75 apply(simp (no_asm_use) only: flip_def) |
|
76 apply(subst swap_fresh_fresh) |
|
77 apply(simp add: Abs_fresh_iff) |
|
78 using fr |
|
79 apply(simp add: Abs_fresh_iff) |
|
80 apply(subst swap_fresh_fresh) |
|
81 apply(simp add: Abs_fresh_iff) |
|
82 using fr |
|
83 apply(simp add: Abs_fresh_iff) |
|
84 apply(rule e) |
|
85 done |
|
86 then have "Abs_lst [atom d] ((a \<leftrightarrow> d) \<bullet> T) = Abs_lst [atom d] ((b \<leftrightarrow> d) \<bullet> S)" |
|
87 apply (simp add: swap_atom flip_def) |
|
88 done |
|
89 then have eq: "(a \<leftrightarrow> d) \<bullet> T = (b \<leftrightarrow> d) \<bullet> S" |
|
90 by (simp add: Abs1_eq_iff) |
|
91 have "f a T c = (a \<leftrightarrow> d) \<bullet> f a T c" |
|
92 unfolding flip_def |
|
93 apply(rule sym) |
|
94 apply(rule swap_fresh_fresh) |
|
95 using fcb[where a="a"] |
|
96 apply(simp) |
|
97 using fr |
|
98 apply(simp add: fresh_Pair) |
|
99 done |
|
100 also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c" |
|
101 unfolding flip_def |
|
102 apply(subst perm1) |
|
103 using fresh fr |
|
104 apply(simp add: supp_swap fresh_star_def fresh_Pair) |
|
105 apply(simp) |
|
106 done |
|
107 also have "... = f d ((b \<leftrightarrow> d) \<bullet> S) c" using eq by simp |
|
108 also have "... = (b \<leftrightarrow> d) \<bullet> f b S c" |
|
109 unfolding flip_def |
|
110 apply(subst perm2) |
|
111 using fresh fr |
|
112 apply(simp add: supp_swap fresh_star_def fresh_Pair) |
|
113 apply(simp) |
|
114 done |
|
115 also have "... = f b S c" |
|
116 apply(rule flip_fresh_fresh) |
|
117 using fcb[where a="b"] |
|
118 apply(simp) |
|
119 using fr |
|
120 apply(simp add: fresh_Pair) |
|
121 done |
|
122 finally show ?thesis by simp |
|
123 qed |
|
124 |
|
125 locale test = |
|
126 fixes f1::"name \<Rightarrow> name list \<Rightarrow> ('a::pt)" |
|
127 and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)" |
|
128 and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)" |
|
129 assumes fs: "finite (supp (f1, f2, f3))" |
|
130 and eq: "eqvt f1" "eqvt f2" "eqvt f3" |
|
131 and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l" |
|
132 and fcb2: "\<And>l t1 t2 r1 r2. atom ` set l \<sharp>* (r1, r2) \<Longrightarrow> atom ` set l \<sharp>* f2 t1 t2 r1 r2 l" |
|
133 and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l" |
|
134 begin |
|
135 |
|
136 nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y") |
|
137 f |
|
138 where |
|
139 "f (Var x) l = f1 x l" |
|
140 | "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l" |
|
141 | "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l" |
|
142 apply (simp add: eqvt_def f_graph_def) |
|
143 apply (rule, perm_simp) |
|
144 apply (simp only: eq[unfolded eqvt_def]) |
|
145 apply (erule f_graph.induct) |
|
146 apply (simp add: fcb1) |
|
147 apply (simp add: fcb2 fresh_star_Pair) |
|
148 apply simp |
|
149 apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l") |
|
150 apply (simp add: fresh_star_def) |
|
151 apply (rule fcb3) |
|
152 apply (simp add: fresh_star_def fresh_def) |
|
153 apply simp_all |
|
154 apply(case_tac x) |
|
155 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
|
156 apply(auto simp add: fresh_star_def) |
|
157 apply(erule_tac Abs_lst1_fcb2) |
|
158 --"?" |
|
159 apply (subgoal_tac "atom ` set (a # la) \<sharp>* f3 a T (f_sumC (T, a # la)) la") |
|
160 apply (simp add: fresh_star_def) |
|
161 apply (rule fcb3) |
|
162 apply (simp add: fresh_star_def) |
|
163 apply (rule fresh_fun_eqvt_app4[OF eq(3)]) |
|
164 apply (simp add: fresh_at_base) |
|
165 apply assumption |
|
166 apply (erule fresh_eqvt_at) |
|
167 apply (simp add: finite_supp) |
|
168 apply (simp add: fresh_Pair fresh_Cons fresh_at_base) |
|
169 apply assumption |
|
170 apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 x y r l) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)") |
|
171 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la") |
|
172 apply (simp add: eqvt_at_def) |
|
173 apply (simp add: swap_fresh_fresh) |
|
174 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
|
175 apply simp |
|
176 done |
|
177 |
|
178 termination |
|
179 by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size) |
|
180 |
|
181 end |
|
182 |
|
183 section {* Locally Nameless Terms *} |
|
184 |
|
185 nominal_datatype ln = |
|
186 LNBnd nat |
|
187 | LNVar name |
|
188 | LNApp ln ln |
|
189 | LNLam ln |
|
190 |
|
191 fun |
|
192 lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" |
|
193 where |
|
194 "lookup [] n x = LNVar x" |
|
195 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
|
196 |
|
197 lemma lookup_eqvt[eqvt]: |
|
198 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
|
199 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
|
200 |
|
201 lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs" |
|
202 unfolding fresh_def supp_set[symmetric] |
|
203 apply (induct xs) |
|
204 apply (simp add: supp_set_empty) |
|
205 apply simp |
|
206 apply auto |
|
207 apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base) |
|
208 done |
|
209 |
|
210 interpretation trans: test |
|
211 "%x l. lookup l 0 x" |
|
212 "%t1 t2 r1 r2 l. LNApp r1 r2" |
|
213 "%n t r l. LNLam r" |
|
214 apply default |
|
215 apply (auto simp add: pure_fresh supp_Pair) |
|
216 apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure lookup_eqvt)[3] |
|
217 apply (simp_all add: eqvt_def permute_fun_def permute_pure lookup_eqvt) |
|
218 apply (simp add: fresh_star_def) |
|
219 apply (rule_tac x="0 :: nat" in spec) |
|
220 apply (induct_tac l) |
|
221 apply (simp add: ln.fresh pure_fresh) |
|
222 apply (auto simp add: ln.fresh pure_fresh)[1] |
|
223 apply (case_tac "a \<in> set list") |
|
224 apply simp |
|
225 apply (rule_tac f="lookup" in fresh_fun_eqvt_app3) |
|
226 unfolding eqvt_def |
|
227 apply rule |
|
228 using eqvts_raw(35) |
|
229 apply auto[1] |
|
230 apply (simp add: fresh_at_list) |
|
231 apply (simp add: pure_fresh) |
|
232 apply (simp add: fresh_at_base) |
|
233 apply (simp add: fresh_star_Pair fresh_star_def ln.fresh) |
|
234 apply (simp add: fresh_star_def ln.fresh) |
|
235 done |
|
236 |
|
237 thm trans.f.simps |
|
238 |
|
239 lemma lam_strong_exhaust2: |
|
240 "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; |
|
241 \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P; |
|
242 \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P; |
|
243 finite (supp c)\<rbrakk> |
|
244 \<Longrightarrow> P" |
|
245 sorry |
|
246 |
|
247 nominal_primrec |
|
248 g |
|
249 where |
|
250 "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t" |
|
251 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x" |
|
252 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (App t1 t2) = g2 t1 t2 (g g1 g2 g3 t1) (g g1 g2 g3 t2)" |
|
253 | "finite (supp (g1, g2, g3)) \<Longrightarrow> atom x \<sharp> (g1,g2,g3) \<Longrightarrow> (g g1 g2 g3 (Lam [x].t)) = g3 x t (g g1 g2 g3 t)" |
|
254 apply (simp add: eqvt_def g_graph_def) |
|
255 apply (rule, perm_simp, rule) |
|
256 apply simp_all |
|
257 apply (case_tac x) |
|
258 apply (case_tac "finite (supp (a, b, c))") |
|
259 prefer 2 |
|
260 apply simp |
|
261 apply(rule_tac y="d" and c="(a,b,c)" in lam_strong_exhaust2) |
|
262 apply auto |
|
263 apply blast |
|
264 apply (simp add: Abs1_eq_iff fresh_star_def) |
|
265 sorry |
|
266 |
|
267 termination |
|
268 by (relation "measure (\<lambda>(_,_,_,t). size t)") (simp_all add: lam.size) |
|
269 |
|
270 end |
|