211 |
211 |
212 lemma better_o4_intro: |
212 lemma better_o4_intro: |
213 assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2" |
213 assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2" |
214 shows "App (Lam [x]. t1) s1 \<longrightarrow>1 t2[ x ::= s2]" |
214 shows "App (Lam [x]. t1) s1 \<longrightarrow>1 t2[ x ::= s2]" |
215 proof - |
215 proof - |
216 obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" sorry |
216 obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" by (rule obtain_fresh) |
217 have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs |
217 have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs |
218 by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base) |
218 by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base) |
219 also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt) |
219 also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt) |
220 also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric]) |
220 also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric]) |
221 finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp |
221 finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp |
222 qed |
222 qed |
223 |
223 |
224 |
224 |
225 |
225 |
226 |
|
227 |
|
228 section {* Locally Nameless Terms *} |
226 section {* Locally Nameless Terms *} |
229 |
227 |
230 nominal_datatype ln = |
228 nominal_datatype ln = |
231 LNBnd nat |
229 LNBnd nat |
232 | LNVar name |
230 | LNVar name |
248 nominal_primrec |
246 nominal_primrec |
249 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
247 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
250 where |
248 where |
251 "trans (Var x) xs = lookup xs 0 x" |
249 "trans (Var x) xs = lookup xs 0 x" |
252 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
250 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
253 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam x t) xs = LNLam (trans t (x # xs))" |
251 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
254 apply(case_tac x) |
252 apply(case_tac x) |
255 apply(simp) |
253 apply(simp) |
256 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
254 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
257 apply(simp_all)[3] |
255 apply(simp_all)[3] |
258 apply(blast) |
256 apply(blast) |