nominal2: comparison Nominal/Ex/Lambda.thy

equal deleted inserted replaced

-:08c3ef07cef7
+:5ebd327ffb96
 qed
 section {* Simple examples from Norrish 2004 *}
-nominal_primrec
+nominal_function
 is_app :: "lam \<Rightarrow> bool"
 where
 "is_app (Var x) = False"
 | "is_app (App t1 t2) = True"
 | "is_app (Lam [x]. t) = False"
 thm is_app_def
 thm is_app.eqvt
 thm eqvts
-nominal_primrec
+nominal_function
 rator :: "lam \<Rightarrow> lam option"
 where
 "rator (Var x) = None"
 | "rator (App t1 t2) = Some t1"
 | "rator (Lam [x]. t) = None"
 apply(simp_all)
 done
 termination (eqvt) by lexicographic_order
-nominal_primrec
+nominal_function
 rand :: "lam \<Rightarrow> lam option"
 where
 "rand (Var x) = None"
 | "rand (App t1 t2) = Some t2"
 | "rand (Lam [x]. t) = None"
 apply(simp_all)
 done
 termination (eqvt) by lexicographic_order
-nominal_primrec
+nominal_function
 is_eta_nf :: "lam \<Rightarrow> bool"
 where
 "is_eta_nf (Var x) = True"
 | "is_eta_nf (App t1 t2) = (is_eta_nf t1 \<and> is_eta_nf t2)"
 | "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and>
 apply(default)
 apply(induct_tac "x::path" rule: path.induct)
 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 {})"
 | "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))"
 | "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))"
 done
 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))"
 | "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])"
 section {* free name function *}
 text {* first returns an atom list *}
-nominal_primrec
+nominal_function
 frees_lst :: "lam \<Rightarrow> atom list"
 where
 "frees_lst (Var x) = [atom x]"
 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
 lemma shows "supp t = set (frees_lst t)"
 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base)
 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}"
 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}"
 lemma "frees_set t = supp t"
 by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base)
 section {* height function *}
-nominal_primrec
+nominal_function
 height :: "lam \<Rightarrow> int"
 where
 "height (Var x) = 1"
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
 thm height.simps
 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))"
 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
 by (induct xs arbitrary: n) (simp_all add: permute_pure)
 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"
 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
 by lexicographic_order
 text {* count the occurences of lambdas in a term *}
-nominal_primrec
+nominal_function
 cntlams :: "lam  \<Rightarrow> nat"
 where
 "cntlams (Var x) = 0"
 | "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)"
 | "cntlams (Lam [x]. t) = Suc (cntlams t)"
 by lexicographic_order
 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)"
 | "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)"
 lemma vindex_eqvt[eqvt]:
 "(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"
 | "transdb (App t1 t2) xs =
 Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
 lemma var_fresh_subst:
 "atom x \<sharp> s \<Longrightarrow> atom x \<sharp> (t[x ::= s])"
 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
 "eval (Var x) = Var x"
 | "eval (Lam [x].t) = Lam [x].(eval t)"
 done
 *)
 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"
 apply(simp add: eqvt_def q_graph_aux_def)
 apply (rule TrueI)
 apply (erule Abs_lst1_fcb)
 oops
 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)"
 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)"
 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
 apply(simp_all add: permute_pure)
 done
 *)
 (*
-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)))"
 | "trans2 (App t1 t2) xs =
 ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1::db. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2::db. Some (DBApp db1 db2))))"
 | "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db::db. Some (DBLam db)))"
 oops
 *)
-nominal_primrec
+nominal_function
 CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
 where
 "CPS (Var x) k = Var x"
 | "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))"
 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))))"
 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
 apply(simp add: eqvt_def Z_graph_aux_def)
 using assms
 by (auto simp add: fresh_star_def)
-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)"
 | "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)"
 | "aux (Var x) (App t1 t2) xs = False"
 and x y::"'a::at"
 shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa
 \<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)"
 | "aux2 (App t1 t2) (App s1 s2) = (aux2 t1 s1 \<and> aux2 t2 s2)"
 | "aux2 (Var x) (App t1 t2) = False"
 text {* tests of functions containing if and case *}
 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))"
 | "A (Var x) = (Var x)"
 | "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))"
 | "C (Var x) = (Var x)"
 | "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)"
 | "A (Var x) = (Var x)"
 | "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)"
 | "B (Var x) = (Var x)"
 | "B (App M N) = (if True then M else (B N))"

changeset 3235	5ebd327ffb96
parent 3232	7bc38b93a1fc
child 3236	e2da10806a34