equal
deleted
inserted
replaced
86 assumes "as \<subseteq> bs" "bs \<sharp>* x" |
86 assumes "as \<subseteq> bs" "bs \<sharp>* x" |
87 shows "as \<sharp>* x" |
87 shows "as \<sharp>* x" |
88 using assms by (auto simp add: fresh_star_def) |
88 using assms by (auto simp add: fresh_star_def) |
89 |
89 |
90 |
90 |
91 nominal_primrec (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow> |
91 nominal_function (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow> |
92 supp y \<subseteq> (supp y1 - set (bn x1)) \<union> (fv_bn x1) | Inr (x2, y2) \<Rightarrow> supp y \<subseteq> supp x2 \<union> supp y2") |
92 supp y \<subseteq> (supp y1 - set (bn x1)) \<union> (fv_bn x1) | Inr (x2, y2) \<Rightarrow> supp y \<subseteq> supp x2 \<union> supp y2") |
93 evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and |
93 evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and |
94 evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem" |
94 evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem" |
95 where |
95 where |
96 "evals ENil (Var x) = N (V x)" |
96 "evals ENil (Var x) = N (V x)" |
344 apply(blast) |
344 apply(blast) |
345 apply(simp add: sem_neu_env.supp) |
345 apply(simp add: sem_neu_env.supp) |
346 done |
346 done |
347 |
347 |
348 |
348 |
349 nominal_primrec |
349 nominal_function |
350 reify :: "sem \<Rightarrow> lam" and |
350 reify :: "sem \<Rightarrow> lam" and |
351 reifyn :: "neu \<Rightarrow> lam" |
351 reifyn :: "neu \<Rightarrow> lam" |
352 where |
352 where |
353 "atom x \<sharp> (env, y, t) \<Longrightarrow> reify (L env y t) = Lam [x]. (reify (evals (ECons env y (N (V x))) t))" |
353 "atom x \<sharp> (env, y, t) \<Longrightarrow> reify (L env y t) = Lam [x]. (reify (evals (ECons env y (N (V x))) t))" |
354 | "reify (N n) = reifyn n" |
354 | "reify (N n) = reifyn n" |