93 termination |
93 termination |
94 apply(relation "measure size") |
94 apply(relation "measure size") |
95 apply(simp_all add: lam.size) |
95 apply(simp_all add: lam.size) |
96 done |
96 done |
97 |
97 |
98 (* a small lemma *) |
98 text {* a small lemma *} |
99 lemma |
99 lemma |
100 "supp t = set (frees_lst t)" |
100 "supp t = set (frees_lst t)" |
101 apply(induct t rule: lam.induct) |
101 apply(induct t rule: lam.induct) |
102 apply(simp_all add: lam.supp supp_at_base) |
102 apply(simp_all add: lam.supp supp_at_base) |
|
103 done |
|
104 |
|
105 nominal_primrec |
|
106 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
|
107 where |
|
108 "(Var x)[y ::= s] = (if x=y then s else (Var x))" |
|
109 | "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])" |
|
110 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
|
111 apply(case_tac x) |
|
112 apply(simp) |
|
113 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) |
|
114 apply(simp add: lam.eq_iff lam.distinct) |
|
115 apply(auto)[1] |
|
116 apply(simp add: lam.eq_iff lam.distinct) |
|
117 apply(auto)[1] |
|
118 apply(simp add: fresh_star_def lam.eq_iff lam.distinct) |
|
119 apply(simp_all add: lam.distinct)[5] |
|
120 apply(simp add: lam.eq_iff) |
|
121 apply(simp add: lam.eq_iff) |
|
122 apply(simp add: lam.eq_iff) |
|
123 apply(erule conjE)+ |
|
124 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta") |
|
125 prefer 2 |
|
126 apply(rule conjI) |
|
127 apply(simp add: Abs_fresh_iff) |
|
128 apply(drule sym) |
|
129 apply(simp add: Abs_fresh_iff) |
|
130 apply(subst (asm) Abs_eq_iff2) |
|
131 apply(auto) |
|
132 apply(simp add: alphas) |
|
133 apply(simp add: atom_eqvt) |
|
134 apply(clarify) |
|
135 apply(rule trans) |
|
136 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
137 apply(rule fresh_star_supp_conv) |
|
138 apply(drule fresh_star_perm_set_conv) |
|
139 apply(simp add: finite_supp) |
|
140 apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))") |
|
141 apply(auto simp add: fresh_star_def)[1] |
|
142 apply(simp (no_asm) add: fresh_star_def) |
|
143 apply(rule conjI) |
|
144 apply(simp (no_asm) add: Abs_fresh_iff) |
|
145 apply(clarify) |
|
146 apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at) |
|
147 apply(simp add: finite_supp) |
|
148 apply(simp (no_asm_use) add: fresh_Pair) |
|
149 apply(simp add: Abs_fresh_iff) |
|
150 apply(simp) |
|
151 apply(simp add: Abs_fresh_iff) |
|
152 apply(subgoal_tac "p \<bullet> ya = ya") |
|
153 apply(subgoal_tac "p \<bullet> sa = sa") |
|
154 unfolding eqvt_at_def |
|
155 apply(simp add: atom_eqvt fresh_Pair) |
|
156 apply(rule perm_supp_eq) |
|
157 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
|
158 apply(rule perm_supp_eq) |
|
159 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
103 done |
160 done |
104 |
161 |
105 nominal_datatype ln = |
162 nominal_datatype ln = |
106 LNBnd nat |
163 LNBnd nat |
107 | LNVar name |
164 | LNVar name |
135 apply(simp add: fresh_star_def) |
192 apply(simp add: fresh_star_def) |
136 apply(simp_all add: lam.distinct) |
193 apply(simp_all add: lam.distinct) |
137 apply(simp add: lam.eq_iff) |
194 apply(simp add: lam.eq_iff) |
138 apply(simp add: lam.eq_iff) |
195 apply(simp add: lam.eq_iff) |
139 apply(simp add: lam.eq_iff) |
196 apply(simp add: lam.eq_iff) |
140 apply(simp add: Abs_eq_iff) |
|
141 apply(erule conjE) |
197 apply(erule conjE) |
142 apply(erule exE) |
198 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta") |
|
199 prefer 2 |
|
200 apply(rule conjI) |
|
201 apply(simp add: Abs_fresh_iff) |
|
202 apply(drule sym) |
|
203 apply(simp add: Abs_fresh_iff) |
|
204 apply(subst (asm) Abs_eq_iff2) |
|
205 apply(auto) |
143 apply(simp add: alphas) |
206 apply(simp add: alphas) |
144 apply(simp add: atom_eqvt) |
207 apply(simp add: atom_eqvt) |
145 apply(clarify) |
208 apply(clarify) |
146 apply(rule trans) |
209 apply(rule trans) |
147 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
210 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
148 apply(simp (no_asm) add: ln.supp) |
211 apply(rule fresh_star_supp_conv) |
149 apply(drule supp_eqvt_at) |
212 apply(drule fresh_star_perm_set_conv) |
150 apply(simp add: finite_supp) |
213 apply(simp add: finite_supp) |
|
214 apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* LNLam (trans_sumC (t, x # xsa))") |
|
215 apply(auto simp add: fresh_star_def)[1] |
|
216 apply(simp (no_asm) add: fresh_star_def ln.fresh) |
|
217 apply(rule conjI) |
|
218 apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at) |
|
219 apply(simp add: finite_supp) |
|
220 apply(simp (no_asm_use) add: fresh_Pair) |
|
221 apply(simp add: Abs_fresh_iff fresh_Cons)[1] |
|
222 apply(erule disjE) |
|
223 apply(erule disjE) |
|
224 apply(simp) |
151 oops |
225 oops |
152 |
|
153 |
|
154 |
|
155 |
|
156 |
226 |
157 nominal_datatype db = |
227 nominal_datatype db = |
158 DBVar nat |
228 DBVar nat |
159 | DBApp db db |
229 | DBApp db db |
160 | DBLam db |
230 | DBLam db |
246 "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
316 "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
247 | "trans (App t1 t2) xs = (trans t1 xs \<guillemotright>= (\<lambda>db1. trans t2 xs \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
317 | "trans (App t1 t2) xs = (trans t1 xs \<guillemotright>= (\<lambda>db1. trans t2 xs \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
248 | "trans (Lam x t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
318 | "trans (Lam x t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
249 *) |
319 *) |
250 |
320 |
251 nominal_primrec |
321 |
252 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
|
253 where |
|
254 "(Var x)[y ::= s] = (if x=y then s else (Var x))" |
|
255 | "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])" |
|
256 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
|
257 apply(case_tac x) |
|
258 apply(simp) |
|
259 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) |
|
260 apply(simp add: lam.eq_iff lam.distinct) |
|
261 apply(auto)[1] |
|
262 apply(simp add: lam.eq_iff lam.distinct) |
|
263 apply(auto)[1] |
|
264 apply(simp add: fresh_star_def lam.eq_iff lam.distinct) |
|
265 apply(simp_all add: lam.distinct)[5] |
|
266 apply(simp add: lam.eq_iff) |
|
267 apply(simp add: lam.eq_iff) |
|
268 apply(simp add: lam.eq_iff) |
|
269 apply(erule conjE)+ |
|
270 oops |
|
271 |
322 |
272 |
323 |
273 end |
324 end |
274 |
325 |
275 |
326 |