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" binds 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 locale test = |
|
40 fixes f1::"name \<Rightarrow> name list \<Rightarrow> ('a::pt)" |
|
41 and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)" |
|
42 and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)" |
|
43 assumes fs: "finite (supp (f1, f2, f3))" |
|
44 and eq: "eqvt f1" "eqvt f2" "eqvt f3" |
|
45 and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l" |
|
46 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" |
|
47 and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l" |
|
48 begin |
|
49 |
|
50 nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y") |
|
51 f |
|
52 where |
|
53 "f (Var x) l = f1 x l" |
|
54 | "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l" |
|
55 | "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l" |
|
56 apply (simp add: eqvt_def f_graph_def) |
|
57 apply (rule, perm_simp) |
|
58 apply (simp only: eq[unfolded eqvt_def]) |
|
59 apply (erule f_graph.induct) |
|
60 apply (simp add: fcb1) |
|
61 apply (simp add: fcb2 fresh_star_Pair) |
|
62 apply simp |
|
63 apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l") |
|
64 apply (simp add: fresh_star_def) |
|
65 apply (rule fcb3) |
|
66 apply (simp add: fresh_star_def fresh_def) |
|
67 apply simp_all |
|
68 apply(case_tac x) |
|
69 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
|
70 apply(auto simp add: fresh_star_def) |
|
71 apply(erule Abs_lst1_fcb) |
|
72 apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la") |
|
73 apply (simp add: fresh_star_def) |
|
74 apply (rule fcb3) |
|
75 apply (simp add: fresh_star_def) |
|
76 apply (rule fresh_fun_eqvt_app4[OF eq(3)]) |
|
77 apply (simp add: fresh_at_base) |
|
78 apply assumption |
|
79 apply (erule fresh_eqvt_at) |
|
80 apply (simp add: finite_supp) |
|
81 apply (simp add: fresh_Pair fresh_Cons fresh_at_base) |
|
82 apply assumption |
|
83 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)") |
|
84 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la") |
|
85 apply (simp add: eqvt_at_def) |
|
86 apply (simp add: swap_fresh_fresh) |
|
87 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
|
88 apply simp |
|
89 done |
|
90 |
|
91 termination |
|
92 by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size) |
|
93 |
|
94 end |
|
95 |
|
96 section {* Locally Nameless Terms *} |
|
97 |
|
98 nominal_datatype ln = |
|
99 LNBnd nat |
|
100 | LNVar name |
|
101 | LNApp ln ln |
|
102 | LNLam ln |
|
103 |
|
104 fun |
|
105 lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" |
|
106 where |
|
107 "lookup [] n x = LNVar x" |
|
108 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
|
109 |
|
110 lemma lookup_eqvt[eqvt]: |
|
111 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
|
112 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
|
113 |
|
114 lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs" |
|
115 unfolding fresh_def supp_set[symmetric] |
|
116 apply (induct xs) |
|
117 apply (simp add: supp_set_empty) |
|
118 apply simp |
|
119 apply auto |
|
120 apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base) |
|
121 done |
|
122 |
|
123 interpretation trans: test |
|
124 "%x l. lookup l 0 x" |
|
125 "%t1 t2 r1 r2 l. LNApp r1 r2" |
|
126 "%n t r l. LNLam r" |
|
127 apply default |
|
128 apply (auto simp add: pure_fresh supp_Pair) |
|
129 apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure lookup_eqvt)[3] |
|
130 apply (simp_all add: eqvt_def permute_fun_def permute_pure lookup_eqvt) |
|
131 apply (simp add: fresh_star_def) |
|
132 apply (rule_tac x="0 :: nat" in spec) |
|
133 apply (induct_tac l) |
|
134 apply (simp add: ln.fresh pure_fresh) |
|
135 apply (auto simp add: ln.fresh pure_fresh)[1] |
|
136 apply (case_tac "a \<in> set list") |
|
137 apply simp |
|
138 apply (rule_tac f="lookup" in fresh_fun_eqvt_app3) |
|
139 unfolding eqvt_def |
|
140 apply rule |
|
141 using eqvts_raw(35) |
|
142 apply auto[1] |
|
143 apply (simp add: fresh_at_list) |
|
144 apply (simp add: pure_fresh) |
|
145 apply (simp add: fresh_at_base) |
|
146 apply (simp add: fresh_star_Pair fresh_star_def ln.fresh) |
|
147 apply (simp add: fresh_star_def ln.fresh) |
|
148 done |
|
149 |
|
150 thm trans.f.simps |
|
151 |
|
152 lemma lam_strong_exhaust2: |
|
153 "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; |
|
154 \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P; |
|
155 \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P; |
|
156 finite (supp c)\<rbrakk> |
|
157 \<Longrightarrow> P" |
|
158 sorry |
|
159 |
|
160 nominal_primrec |
|
161 g |
|
162 where |
|
163 "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t" |
|
164 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x" |
|
165 | "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)" |
|
166 | "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)" |
|
167 apply (simp add: eqvt_def g_graph_def) |
|
168 apply (rule, perm_simp, rule) |
|
169 apply simp_all |
|
170 apply (case_tac x) |
|
171 apply (case_tac "finite (supp (a, b, c))") |
|
172 prefer 2 |
|
173 apply simp |
|
174 apply(rule_tac y="d" and c="(a,b,c)" in lam_strong_exhaust2) |
|
175 apply auto |
|
176 apply blast |
|
177 apply (simp add: Abs1_eq_iff fresh_star_def) |
|
178 sorry |
|
179 |
|
180 termination |
|
181 by (relation "measure (\<lambda>(_,_,_,t). size t)") (simp_all add: lam.size) |
|
182 |
|
183 end |
|