--- a/Nominal/Ex/Lambda.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Lambda.thy Mon May 19 12:45:26 2014 +0100
@@ -72,7 +72,7 @@
section {* Simple examples from Norrish 2004 *}
-nominal_primrec
+nominal_function
is_app :: "lam \<Rightarrow> bool"
where
"is_app (Var x) = False"
@@ -93,7 +93,7 @@
thm eqvts
-nominal_primrec
+nominal_function
rator :: "lam \<Rightarrow> lam option"
where
"rator (Var x) = None"
@@ -108,7 +108,7 @@
termination (eqvt) by lexicographic_order
-nominal_primrec
+nominal_function
rand :: "lam \<Rightarrow> lam option"
where
"rand (Var x) = None"
@@ -123,7 +123,7 @@
termination (eqvt) by lexicographic_order
-nominal_primrec
+nominal_function
is_eta_nf :: "lam \<Rightarrow> bool"
where
"is_eta_nf (Var x) = True"
@@ -154,7 +154,7 @@
apply(simp_all)
done
-nominal_primrec
+nominal_function
var_pos :: "name \<Rightarrow> lam \<Rightarrow> (path list) set"
where
"var_pos y (Var x) = (if y = x then {[]} else {})"
@@ -200,7 +200,7 @@
text {* strange substitution operation *}
-nominal_primrec
+nominal_function
subst' :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::== _]" [90, 90, 90] 90)
where
"(Var x)[y ::== s] = (if x = y then s else (Var x))"
@@ -234,7 +234,7 @@
text {* first returns an atom list *}
-nominal_primrec
+nominal_function
frees_lst :: "lam \<Rightarrow> atom list"
where
"frees_lst (Var x) = [atom x]"
@@ -260,7 +260,7 @@
text {* second returns an atom set - therefore needs an invariant *}
-nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
+nominal_function (invariant "\<lambda>x (y::atom set). finite y")
frees_set :: "lam \<Rightarrow> atom set"
where
"frees_set (Var x) = {atom x}"
@@ -288,7 +288,7 @@
section {* height function *}
-nominal_primrec
+nominal_function
height :: "lam \<Rightarrow> int"
where
"height (Var x) = 1"
@@ -311,7 +311,7 @@
section {* capture-avoiding substitution *}
-nominal_primrec
+nominal_function
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90)
where
"(Var x)[y ::= s] = (if x = y then s else (Var x))"
@@ -501,7 +501,7 @@
text {* Function that translates lambda-terms into locally nameless terms *}
-nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
+nominal_function (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
where
"trans (Var x) xs = lookup xs 0 x"
@@ -536,7 +536,7 @@
text {* count the occurences of lambdas in a term *}
-nominal_primrec
+nominal_function
cntlams :: "lam \<Rightarrow> nat"
where
"cntlams (Var x) = 0"
@@ -563,7 +563,7 @@
text {* count the bound-variable occurences in a lambda-term *}
-nominal_primrec
+nominal_function
cntbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
where
"cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
@@ -621,7 +621,7 @@
"(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)"
by (induct l arbitrary: n) (simp_all add: permute_pure)
-nominal_primrec
+nominal_function
transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option"
where
"transdb (Var x) l = vindex l x 0"
@@ -679,7 +679,7 @@
by (induct t x s rule: subst.induct) (auto simp add: lam.supp fresh_at_base)
(* function that evaluates a lambda term *)
-nominal_primrec
+nominal_function
eval :: "lam \<Rightarrow> lam" and
apply_subst :: "lam \<Rightarrow> lam \<Rightarrow> lam"
where
@@ -734,7 +734,7 @@
text {* TODO: eqvt_at for the other side *}
-nominal_primrec q where
+nominal_function q where
"atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))"
| "q (Var x) N = Var x"
| "q (App l r) N = App l r"
@@ -757,7 +757,7 @@
text {* Working Examples *}
-nominal_primrec
+nominal_function
map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam"
where
"eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)"
@@ -821,7 +821,7 @@
*)
(*
-nominal_primrec
+nominal_function
trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
where
"trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n::nat. Some (DBVar n)))"
@@ -831,7 +831,7 @@
oops
*)
-nominal_primrec
+nominal_function
CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
where
"CPS (Var x) k = Var x"
@@ -839,7 +839,7 @@
oops
consts b :: name
-nominal_primrec
+nominal_function
Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
where
"Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
@@ -871,7 +871,7 @@
-nominal_primrec (invariant "\<lambda>(_, _, xs) y. atom ` fst ` set xs \<sharp>* y \<and> atom ` snd ` set xs \<sharp>* y")
+nominal_function (invariant "\<lambda>(_, _, xs) y. atom ` fst ` set xs \<sharp>* y \<and> atom ` snd ` set xs \<sharp>* y")
aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
where
"aux (Var x) (Var y) xs = ((x, y) \<in> set xs)"
@@ -919,7 +919,7 @@
\<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)"
by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair)
-nominal_primrec
+nominal_function
aux2 :: "lam \<Rightarrow> lam \<Rightarrow> bool"
where
"aux2 (Var x) (Var y) = (x = y)"
@@ -961,7 +961,7 @@
consts P :: "lam \<Rightarrow> bool"
(*
-nominal_primrec
+nominal_function
A :: "lam => lam"
where
"A (App M N) = (if (True \<or> P M) then (A M) else (A N))"
@@ -969,7 +969,7 @@
| "A (App M N) = (if True then M else A N)"
oops
-nominal_primrec
+nominal_function
C :: "lam => lam"
where
"C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))"
@@ -977,7 +977,7 @@
| "C (App M N) = (if True then M else C N)"
oops
-nominal_primrec
+nominal_function
A :: "lam => lam"
where
"A (Lam [x].M) = (Lam [x].M)"
@@ -985,7 +985,7 @@
| "A (App M N) = (if True then M else A N)"
oops
-nominal_primrec
+nominal_function
B :: "lam => lam"
where
"B (Lam [x].M) = (Lam [x].M)"