42 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" "a \<sharp> w" |
42 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" "a \<sharp> w" |
43 shows "a \<sharp> f x y z w" |
43 shows "a \<sharp> f x y z w" |
44 using fresh_fun_eqvt_app[OF a b(1)] a b |
44 using fresh_fun_eqvt_app[OF a b(1)] a b |
45 by (metis fresh_fun_app) |
45 by (metis fresh_fun_app) |
46 |
46 |
|
47 lemma the_default_pty: |
|
48 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
|
49 and unique: "\<exists>!y. G x y" |
|
50 and pty: "\<And>x y. G x y \<Longrightarrow> P x y" |
|
51 shows "P x (f x)" |
|
52 apply(subst f_def) |
|
53 apply (rule ex1E[OF unique]) |
|
54 apply (subst THE_default1_equality[OF unique]) |
|
55 apply assumption |
|
56 apply (rule pty) |
|
57 apply assumption |
|
58 done |
|
59 |
|
60 locale test = |
|
61 fixes f1::"name \<Rightarrow> name list \<Rightarrow> ('a::pt)" |
|
62 and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)" |
|
63 and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)" |
|
64 assumes fs: "finite (supp (f1, f2, f3))" |
|
65 and eq: "eqvt f1" "eqvt f2" "eqvt f3" |
|
66 and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l" |
|
67 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" |
|
68 and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l" |
|
69 begin |
|
70 |
47 nominal_primrec |
71 nominal_primrec |
48 f |
72 f |
49 where |
73 where |
50 "f f1 f2 f3 (Var x) l = f1 x l" |
74 "f (Var x) l = f1 x l" |
51 | "f f1 f2 f3 (App t1 t2) l = f2 t1 t2 (f f1 f2 f3 t1 l) (f f1 f2 f3 t2 l) l" |
75 | "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l" |
52 | "(\<And>t l r. atom x \<sharp> r \<Longrightarrow> atom x \<sharp> f3 x t r l) \<Longrightarrow> (eqvt f1 \<and> eqvt f2 \<and> eqvt f3) \<Longrightarrow> atom x \<sharp> (f1,f2,f3,l) \<Longrightarrow> (f f1 f2 f3 (Lam [x].t) l) = f3 x t (f f1 f2 f3 t (x # l)) l" |
76 | "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l" |
53 apply (simp add: eqvt_def f_graph_def) |
77 apply (simp add: eqvt_def f_graph_def) |
54 apply (rule, perm_simp, rule) |
78 apply (rule, perm_simp) |
|
79 apply (simp only: eq[unfolded eqvt_def]) |
55 apply(case_tac x) |
80 apply(case_tac x) |
56 apply(rule_tac y="d" and c="z" in lam.strong_exhaust) |
81 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
57 apply(auto simp add: fresh_star_def) |
82 apply(auto simp add: fresh_star_def) |
58 apply(blast) |
|
59 apply blast |
|
60 defer |
|
61 apply(simp add: fresh_Pair_elim) |
|
62 apply(erule Abs1_eq_fdest) |
83 apply(erule Abs1_eq_fdest) |
63 defer |
84 defer |
64 apply simp_all |
85 apply simp_all |
65 apply (rule_tac f="f3a" in fresh_fun_eqvt_app4) |
86 apply (rule fresh_fun_eqvt_app4[OF eq(3)]) |
66 apply assumption |
|
67 apply (simp add: fresh_at_base) |
87 apply (simp add: fresh_at_base) |
68 apply assumption |
88 apply assumption |
69 apply (erule fresh_eqvt_at) |
89 apply (erule fresh_eqvt_at) |
70 apply (simp add: supp_Pair supp_fun_eqvt finite_supp) |
90 apply (simp add: finite_supp) |
71 apply (simp add: fresh_Pair) |
91 apply (simp add: fresh_Pair fresh_Cons fresh_at_base) |
72 apply (simp add: fresh_Cons) |
92 apply assumption |
73 apply (simp add: fresh_Cons fresh_at_base) |
93 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)") |
74 apply (assumption) |
|
75 apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3a x y r l) = f3a (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)") |
|
76 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la") |
94 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la") |
77 apply (simp add: eqvt_at_def eqvt_def) |
95 apply (simp add: eqvt_at_def) |
78 apply (simp add: swap_fresh_fresh) |
96 apply (simp add: swap_fresh_fresh) |
79 apply (simp add: permute_fun_app_eq) |
97 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
80 apply (simp add: eqvt_def) |
98 apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la") |
81 prefer 2 |
99 apply (simp add: fresh_star_def) |
82 apply (subgoal_tac "atom x \<sharp> f_sumC (f1a, f2a, f3a, t, x # la)") |
100 apply (rule fcb3) |
83 apply simp |
101 apply (rule_tac x="x # la" in meta_spec) |
84 --"I believe this holds by induction on the graph..." |
102 apply (thin_tac "eqvt_at f_sumC (t, x # la)") |
85 unfolding f_sumC_def |
103 apply (thin_tac "atom x \<sharp> la") |
86 apply (rule_tac y="t" in lam.exhaust) |
104 apply (thin_tac "atom xa \<sharp> la") |
87 apply (subgoal_tac "THE_default undefined (f_graph (f1a, f2a, f3a, t, x # la)) = f1a name (x # la)") |
105 apply (thin_tac "x \<noteq> xa") |
88 apply simp |
106 apply (thin_tac "atom xa \<sharp> t") |
89 defer |
107 apply (subgoal_tac "atom ` set (snd (t, xb)) \<sharp>* f_sumC (t, xb)") |
90 apply (rule THE_default1_equality) |
108 apply simp |
91 apply simp |
109 apply (rule_tac x="(t, xb)" in meta_spec) |
92 defer |
110 apply (simp only: triv_forall_equality) |
93 apply simp |
111 --"We start induction on the graph. We need the 2nd subgoal in the first one" |
94 apply (rule_tac ?f1.0="f1a" in f_graph.intros(1)) |
112 apply (subgoal_tac "\<And>x y. f_graph x y \<Longrightarrow> atom ` set (snd x) \<sharp>* y") |
95 sorry (*this could be defined? *) |
113 apply (rule the_default_pty[OF f_sumC_def]) |
|
114 prefer 2 |
|
115 apply blast |
|
116 prefer 2 |
|
117 apply (erule f_graph.induct) |
|
118 apply (simp add: fcb1) |
|
119 apply (simp add: fcb2 fresh_star_Pair) |
|
120 apply (simp only: snd_conv) |
|
121 apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l") |
|
122 apply (simp add: fresh_star_def) |
|
123 apply (rule fcb3) |
|
124 apply assumption |
|
125 --"We'd like to do the proof with this property" |
|
126 apply (case_tac xc) |
|
127 apply simp |
|
128 apply (rule_tac lam="a" and c="b" in lam.strong_induct) |
|
129 apply (rule_tac a="f1 name c" in ex1I) |
|
130 apply (rule f_graph.intros) |
|
131 apply (erule f_graph.cases) |
|
132 apply simp_all[3] |
|
133 apply (drule_tac x="c" in meta_spec)+ |
|
134 apply (erule ex1E)+ |
|
135 apply (subgoal_tac "f_graph (lam1, c) (f_sumC (lam1, c))") |
|
136 apply (subgoal_tac "f_graph (lam2, c) (f_sumC (lam2, c))") |
|
137 apply (rule_tac a="f2 lam1 lam2 (f_sumC (lam1, c)) (f_sumC (lam2, c)) c" in ex1I) |
|
138 apply (rule_tac f_graph.intros(2)) |
|
139 apply assumption+ |
|
140 apply (rotate_tac 8) |
|
141 apply (erule f_graph.cases) |
|
142 apply simp |
|
143 apply auto[1] |
|
144 apply metis |
|
145 apply simp |
|
146 apply (simp add: f_sumC_def) |
|
147 apply (rule THE_defaultI') |
|
148 apply metis |
|
149 apply (simp add: f_sumC_def) |
|
150 apply (rule THE_defaultI') |
|
151 apply metis |
|
152 --"Only the Lambda case left" |
|
153 apply (subgoal_tac "f_graph (lam, (name # c)) (f_sumC (lam, (name # c)))") |
|
154 prefer 2 |
|
155 apply (simp add: f_sumC_def) |
|
156 apply (rule THE_defaultI') |
|
157 apply assumption |
|
158 apply (rule_tac a="f3 name lam (f_sumC (lam, name # c)) c" in ex1I) |
|
159 apply (rule f_graph.intros(3)) |
|
160 apply (simp add: fresh_star_def) |
|
161 apply assumption |
|
162 apply (rotate_tac -1) |
|
163 apply (erule f_graph.cases) |
|
164 apply simp_all[2] |
|
165 apply simp |
|
166 apply auto[1] |
|
167 apply (subgoal_tac "f_sumC (lam, name # l) = f_sum (lam, name # l)") |
|
168 apply simp |
|
169 apply (rule sym) |
|
170 apply (erule Abs1_eq_fdest) |
|
171 apply (subgoal_tac "atom ` set (name # l) \<sharp>* f3 name lam (f_sum (lam, name # l)) l") |
|
172 apply (simp add: fresh_star_def) |
|
173 apply (rule fcb3) |
|
174 apply metis |
|
175 apply (rule fresh_fun_eqvt_app4[OF eq(3)]) |
|
176 apply (simp add: fresh_at_base) |
|
177 apply assumption |
|
178 defer --"eqvt_at f_sumC" |
|
179 apply assumption |
|
180 apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 name y r l) = f3 (p \<bullet> name) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)") |
|
181 apply (subgoal_tac "(atom name \<rightleftharpoons> atom xa) \<bullet> l = l") |
|
182 apply (simp add: eq[unfolded eqvt_def]) |
|
183 defer --"eqvt_at f_sumC" |
|
184 apply (metis fresh_star_insert swap_fresh_fresh) |
|
185 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
|
186 apply simp |
|
187 sorry |
96 |
188 |
97 termination |
189 termination |
98 by (relation "measure (\<lambda>(_,_,_,x,_). size x)") (auto simp add: lam.size) |
190 by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size) |
|
191 |
|
192 end |
99 |
193 |
100 section {* Locally Nameless Terms *} |
194 section {* Locally Nameless Terms *} |
101 |
195 |
102 nominal_datatype ln = |
196 nominal_datatype ln = |
103 LNBnd nat |
197 LNBnd nat |
109 lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" |
203 lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" |
110 where |
204 where |
111 "lookup [] n x = LNVar x" |
205 "lookup [] n x = LNVar x" |
112 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
206 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
113 |
207 |
114 lemma [eqvt]: |
208 lemma lookup_eqvt[eqvt]: |
115 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
209 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
116 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
210 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
117 |
211 |
118 definition |
212 lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs" |
119 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
213 unfolding fresh_def supp_set[symmetric] |
120 where |
214 apply (induct xs) |
121 "trans t l = f (%x l. lookup l 0 x) (%t1 t2 r1 r2 l. LNApp r1 r2) (%n t r l. LNLam r) t l" |
215 apply (simp add: supp_set_empty) |
122 |
216 apply simp |
123 lemma |
217 apply auto |
124 "trans (Var x) xs = lookup xs 0 x" |
218 apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base) |
125 "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
219 done |
126 "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
220 |
127 apply (simp_all add: trans_def) |
221 interpretation trans: test |
128 apply (subst f.simps) |
222 "%x l. lookup l 0 x" |
129 apply (simp add: ln.fresh) |
223 "%t1 t2 r1 r2 l. LNApp r1 r2" |
130 apply (simp add: eqvt_def) |
224 "%n t r l. LNLam r" |
131 apply auto |
225 apply default |
132 apply (perm_simp, rule) |
226 apply (auto simp add: pure_fresh supp_Pair) |
133 apply (perm_simp, rule) |
227 apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure lookup_eqvt)[3] |
134 apply (perm_simp, rule) |
228 apply (simp_all add: eqvt_def permute_fun_def permute_pure lookup_eqvt) |
135 apply (auto simp add: fresh_Pair)[1] |
229 apply (simp add: fresh_star_def) |
136 apply (simp_all add: fresh_def supp_def permute_fun_def)[3] |
230 apply (rule_tac x="0 :: nat" in spec) |
137 apply (simp add: eqvts permute_pure) |
231 apply (induct_tac l) |
138 done |
232 apply (simp add: ln.fresh pure_fresh) |
|
233 apply (auto simp add: ln.fresh pure_fresh)[1] |
|
234 apply (case_tac "a \<in> set list") |
|
235 apply simp |
|
236 apply (rule_tac f="lookup" in fresh_fun_eqvt_app3) |
|
237 unfolding eqvt_def |
|
238 apply rule |
|
239 using eqvts_raw(35) |
|
240 apply auto[1] |
|
241 apply (simp add: fresh_at_list) |
|
242 apply (simp add: pure_fresh) |
|
243 apply (simp add: fresh_at_base) |
|
244 apply (simp add: fresh_star_Pair fresh_star_def ln.fresh) |
|
245 apply (simp add: fresh_star_def ln.fresh) |
|
246 done |
|
247 |
|
248 thm trans.f.simps |
139 |
249 |
140 lemma lam_strong_exhaust2: |
250 lemma lam_strong_exhaust2: |
141 "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; |
251 "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; |
142 \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P; |
252 \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P; |
143 \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P; |
253 \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P; |