15 height :: "lam \<Rightarrow> int" |
15 height :: "lam \<Rightarrow> int" |
16 where |
16 where |
17 "height (Var x) = 1" |
17 "height (Var x) = 1" |
18 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
18 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
19 | "height (Lam [x].t) = height t + 1" |
19 | "height (Lam [x].t) = height t + 1" |
|
20 defer |
20 apply(rule_tac y="x" in lam.exhaust) |
21 apply(rule_tac y="x" in lam.exhaust) |
21 apply(auto simp add: lam.distinct lam.eq_iff) |
22 apply(auto simp add: lam.distinct lam.eq_iff) |
22 apply(simp add: Abs_eq_iff alphas) |
23 apply(simp add: Abs_eq_iff alphas) |
23 apply(clarify) |
24 apply(clarify) |
24 apply(subst (4) supp_perm_eq[where p="p", symmetric]) |
25 apply(subst (4) supp_perm_eq[where p="p", symmetric]) |
25 apply(simp add: pure_supp fresh_star_def) |
26 apply(simp add: pure_supp fresh_star_def) |
26 apply(simp add: eqvt_at_def) |
27 apply(simp add: eqvt_at_def) |
|
28 apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") |
|
29 unfolding eqvt_def |
|
30 apply(rule allI) |
|
31 apply(simp add: permute_fun_def) |
|
32 apply(rule ext) |
|
33 apply(rule ext) |
|
34 apply(simp add: permute_bool_def) |
|
35 apply(rule iffI) |
|
36 apply(drule_tac x="p" in meta_spec) |
|
37 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
38 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
39 apply(simp) |
|
40 apply(drule_tac x="-p" in meta_spec) |
|
41 apply(drule_tac x="x" in meta_spec) |
|
42 apply(drule_tac x="xa" in meta_spec) |
|
43 apply(simp) |
|
44 apply(erule height_graph.induct) |
|
45 apply(perm_simp) |
|
46 apply(rule height_graph.intros) |
|
47 apply(perm_simp) |
|
48 apply(rule height_graph.intros) |
|
49 apply(assumption) |
|
50 apply(assumption) |
|
51 apply(perm_simp) |
|
52 apply(rule height_graph.intros) |
|
53 apply(assumption) |
27 done |
54 done |
28 |
55 |
29 termination |
56 termination |
30 by (relation "measure size") (simp_all add: lam.size) |
57 by (relation "measure size") (simp_all add: lam.size) |
31 |
58 |
|
59 thm height.simps |
|
60 |
32 |
61 |
33 text {* free name function - returns atom lists *} |
62 text {* free name function - returns atom lists *} |
34 |
63 |
35 nominal_primrec |
64 nominal_primrec |
36 frees_lst :: "lam \<Rightarrow> atom list" |
65 frees_lst :: "lam \<Rightarrow> atom list" |
37 where |
66 where |
38 "frees_lst (Var x) = [atom x]" |
67 "frees_lst (Var x) = [atom x]" |
39 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
68 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
40 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
69 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
|
70 defer |
41 apply(rule_tac y="x" in lam.exhaust) |
71 apply(rule_tac y="x" in lam.exhaust) |
42 apply(simp_all)[3] |
72 apply(simp_all)[3] |
43 apply(simp_all only: lam.distinct) |
73 apply(simp_all only: lam.distinct) |
44 apply(simp add: lam.eq_iff) |
74 apply(simp add: lam.eq_iff) |
45 apply(simp add: lam.eq_iff) |
75 apply(simp add: lam.eq_iff) |
55 apply(drule supp_eqvt_at) |
85 apply(drule supp_eqvt_at) |
56 apply(simp add: finite_supp) |
86 apply(simp add: finite_supp) |
57 apply(auto simp add: fresh_star_def)[1] |
87 apply(auto simp add: fresh_star_def)[1] |
58 unfolding eqvt_at_def |
88 unfolding eqvt_at_def |
59 apply(simp only: removeAll_eqvt atom_eqvt) |
89 apply(simp only: removeAll_eqvt atom_eqvt) |
|
90 apply(subgoal_tac "\<And>p x r. frees_lst_graph x r \<Longrightarrow> frees_lst_graph (p \<bullet> x) (p \<bullet> r)") |
|
91 unfolding eqvt_def |
|
92 apply(rule allI) |
|
93 apply(simp add: permute_fun_def) |
|
94 apply(rule ext) |
|
95 apply(rule ext) |
|
96 apply(simp add: permute_bool_def) |
|
97 apply(rule iffI) |
|
98 apply(drule_tac x="p" in meta_spec) |
|
99 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
100 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
101 apply(simp) |
|
102 apply(drule_tac x="-p" in meta_spec) |
|
103 apply(drule_tac x="x" in meta_spec) |
|
104 apply(drule_tac x="xa" in meta_spec) |
|
105 apply(simp) |
|
106 apply(erule frees_lst_graph.induct) |
|
107 apply(perm_simp) |
|
108 apply(rule frees_lst_graph.intros) |
|
109 apply(perm_simp) |
|
110 apply(rule frees_lst_graph.intros) |
|
111 apply(assumption) |
|
112 apply(assumption) |
|
113 apply(perm_simp) |
|
114 apply(rule frees_lst_graph.intros) |
|
115 apply(assumption) |
60 done |
116 done |
61 |
117 |
62 termination |
118 termination |
63 apply(relation "measure size") |
119 apply(relation "measure size") |
64 apply(simp_all add: lam.size) |
120 apply(simp_all add: lam.size) |
77 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
133 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
78 where |
134 where |
79 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
135 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
80 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
136 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
81 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
137 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
|
138 defer |
82 apply(auto simp add: lam.distinct lam.eq_iff) |
139 apply(auto simp add: lam.distinct lam.eq_iff) |
83 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
140 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
84 apply(blast)+ |
141 apply(blast)+ |
85 apply(simp add: fresh_star_def) |
142 apply(simp add: fresh_star_def) |
86 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta") |
143 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta") |
113 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
170 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
114 apply(rule conjI) |
171 apply(rule conjI) |
115 apply(simp add: Abs_fresh_iff) |
172 apply(simp add: Abs_fresh_iff) |
116 apply(drule sym) |
173 apply(drule sym) |
117 apply(simp add: Abs_fresh_iff) |
174 apply(simp add: Abs_fresh_iff) |
|
175 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
|
176 unfolding eqvt_def |
|
177 apply(rule allI) |
|
178 apply(simp add: permute_fun_def) |
|
179 apply(rule ext) |
|
180 apply(rule ext) |
|
181 apply(simp add: permute_bool_def) |
|
182 apply(rule iffI) |
|
183 apply(drule_tac x="p" in meta_spec) |
|
184 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
185 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
186 apply(simp) |
|
187 apply(drule_tac x="-p" in meta_spec) |
|
188 apply(drule_tac x="x" in meta_spec) |
|
189 apply(drule_tac x="xa" in meta_spec) |
|
190 apply(simp) |
|
191 apply(erule subst_graph.induct) |
|
192 apply(perm_simp) |
|
193 apply(rule subst_graph.intros) |
|
194 apply(perm_simp) |
|
195 apply(rule subst_graph.intros) |
|
196 apply(assumption) |
|
197 apply(assumption) |
|
198 apply(perm_simp) |
|
199 apply(rule subst_graph.intros) |
|
200 apply(simp add: fresh_Pair) |
|
201 apply(assumption) |
118 done |
202 done |
119 |
203 |
120 termination |
204 termination |
121 by (relation "measure (\<lambda>(t,_,_). size t)") |
205 by (relation "measure (\<lambda>(t,_,_). size t)") |
122 (simp_all add: lam.size) |
206 (simp_all add: lam.size) |
247 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
331 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
248 where |
332 where |
249 "trans (Var x) xs = lookup xs 0 x" |
333 "trans (Var x) xs = lookup xs 0 x" |
250 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
334 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
251 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
335 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
|
336 defer |
252 apply(case_tac x) |
337 apply(case_tac x) |
253 apply(simp) |
338 apply(simp) |
254 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
339 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
255 apply(simp_all)[3] |
340 apply(simp_all)[3] |
256 apply(blast) |
341 apply(blast) |
333 shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
418 shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
334 apply(induct xs arbitrary: n) |
419 apply(induct xs arbitrary: n) |
335 apply(simp_all add: permute_pure) |
420 apply(simp_all add: permute_pure) |
336 done |
421 done |
337 |
422 |
338 ML {* |
|
339 Nominal_Function_Core.trace := true |
|
340 *} |
|
341 |
|
342 (* |
423 (* |
343 inductive |
|
344 trans_graph |
|
345 where |
|
346 "trans_graph (Var x, xs) (index xs 0 (atom x) \<guillemotright>= (\<lambda>v. Some (DBVar v)))" |
|
347 | "\<lbrakk>trans_graph (t1, xs) (trans_sum (t1, xs)); |
|
348 \<And>a. trans_sum (t1, xs) = Some a \<Longrightarrow> trans_graph (t2, xs) (trans_sum (t2, xs))\<rbrakk> |
|
349 \<Longrightarrow> trans_graph (App t1 t2, xs) |
|
350 (trans_sum (t1, xs) \<guillemotright>= (\<lambda>v. trans_sum (t2, xs) \<guillemotright>= (\<lambda>va. Some (DBApp v va))))" |
|
351 | "trans_graph (t, atom x # xs) (trans_sum (t, atom x # xs)) \<Longrightarrow> |
|
352 trans_graph (Lam x t, xs) (trans_sum (t, atom x # xs) \<guillemotright>= (\<lambda>v. Some (DBLam v)))" |
|
353 |
|
354 lemma |
|
355 assumes a: "trans_graph x t" |
|
356 shows "trans_graph (p \<bullet> x) (p \<bullet> t)" |
|
357 using a |
|
358 apply(induct) |
|
359 apply(perm_simp) |
|
360 apply(rule trans_graph.intros) |
|
361 apply(perm_simp) |
|
362 apply(rule trans_graph.intros) |
|
363 apply(simp) |
|
364 apply(simp) |
|
365 defer |
|
366 apply(perm_simp) |
|
367 apply(rule trans_graph.intros) |
|
368 apply(simp) |
|
369 apply(rotate_tac 3) |
|
370 apply(drule_tac x="FOO" in meta_spec) |
|
371 apply(drule meta_mp) |
|
372 prefer 2 |
|
373 apply(simp) |
|
374 |
|
375 equivariance trans_graph |
|
376 *) |
|
377 |
|
378 (* equivariance fails at the moment |
|
379 nominal_primrec |
424 nominal_primrec |
380 trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
425 trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
381 where |
426 where |
382 "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
427 "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
383 | "trans (App t1 t2) xs = (trans t1 xs \<guillemotright>= (\<lambda>db1. trans t2 xs \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
428 | "trans (App t1 t2) xs = ((trans t1 xs) \<guillemotright>= (\<lambda>db1. (trans t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
384 | "trans (Lam x t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
429 | "trans (Lam [x].t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
385 *) |
430 *) |
386 |
431 |
387 |
432 |
388 |
433 |
389 |
434 |