--- a/Nominal/Ex/AuxNoFCB.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/AuxNoFCB.thy Mon May 19 12:45:26 2014 +0100
@@ -7,7 +7,7 @@
| App "lam" "lam"
| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
-nominal_primrec lookup where
+nominal_function lookup where
"lookup (n :: name) m [] \<longleftrightarrow> (n = m)"
| "lookup n m ((hn, hm) # t) \<longleftrightarrow>
(n, m) = (hn, hm) \<or> (n \<noteq> hn \<and> m \<noteq> hm \<and> lookup n m t)"
@@ -17,7 +17,7 @@
termination (eqvt) by lexicographic_order
-nominal_primrec lam2_rec where
+nominal_function lam2_rec where
"lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs"
| "lam2_rec faa fll xs (Var n) (App l r) = False"
| "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False"
@@ -97,7 +97,7 @@
apply (subst lam2_rec.simps(10)) apply (simp_all add: fresh_star_def)
done
-nominal_primrec aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
+nominal_function aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
where
[simp del]: "aux l r xs = lam2_rec
(%t1 t2 t3 t4. (aux t1 t3 xs) \<and> (aux t2 t4 xs))
@@ -204,7 +204,7 @@
apply lexicographic_order
done
-nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where
+nominal_function swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where
"swapequal l r [] \<longleftrightarrow> l = r"
| "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow>
swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t"
--- a/Nominal/Ex/Beta.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Beta.thy Mon May 19 12:45:26 2014 +0100
@@ -14,7 +14,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))"
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy Mon May 19 12:45:26 2014 +0100
@@ -3,7 +3,7 @@
imports Lt
begin
-nominal_primrec
+nominal_function
CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250)
where
"atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $$ (x~)))"
@@ -74,7 +74,7 @@
lemma [simp]: "x \<sharp> M* = x \<sharp> M"
unfolding fresh_def by simp
-nominal_primrec
+nominal_function
convert:: "lt => lt" ("_+" [250] 250)
where
"(Var x)+ = Var x"
@@ -104,7 +104,7 @@
shows "isValue (p \<bullet> (M::lt)) = isValue M"
by (nominal_induct M rule: lt.strong_induct) auto
-nominal_primrec
+nominal_function
Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt" (infixl ";" 100)
where
"Kapply (Lam x M) K = K $$ (Lam x M)+"
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Mon May 19 12:45:26 2014 +0100
@@ -9,7 +9,7 @@
| CArg lt cpsctxt
| CAbs x::name c::cpsctxt binds x in c
-nominal_primrec
+nominal_function
fill :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt" ("_<_>" [200, 200] 100)
where
fill_hole : "Hole<M> = M"
@@ -34,7 +34,7 @@
termination (eqvt) by lexicographic_order
-nominal_primrec
+nominal_function
ccomp :: "cpsctxt => cpsctxt => cpsctxt"
where
"ccomp Hole C = C"
@@ -59,7 +59,7 @@
termination (eqvt) by lexicographic_order
-nominal_primrec
+nominal_function
CPSv :: "lt => lt"
and CPS :: "lt => cpsctxt" where
"CPSv (Var x) = x~"
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Mon May 19 12:45:26 2014 +0100
@@ -1,7 +1,7 @@
header {* CPS transformation of Danvy and Filinski *}
theory CPS3_DanvyFilinski imports Lt begin
-nominal_primrec
+nominal_function
CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100)
and
CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy Mon May 19 12:45:26 2014 +0100
@@ -3,7 +3,7 @@
imports Lt
begin
-nominal_primrec
+nominal_function
CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100)
and
CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
--- a/Nominal/Ex/CPS/Lt.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/Lt.thy Mon May 19 12:45:26 2014 +0100
@@ -10,7 +10,7 @@
| App lt lt (infixl "$$" 100)
| Lam x::"name" t::"lt" binds x in t
-nominal_primrec
+nominal_function
subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt" ("_ [_ ::= _]" [90, 90, 90] 90)
where
"(Var x)[y ::= s] = (if x = y then s else (Var x))"
@@ -44,7 +44,7 @@
by (nominal_induct M avoiding: x V rule: lt.strong_induct)
(auto simp add: lt.supp supp_at_base, blast, blast)
-nominal_primrec
+nominal_function
isValue:: "lt => bool"
where
"isValue (Var x) = True"
--- a/Nominal/Ex/CR.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CR.thy Mon May 19 12:45:26 2014 +0100
@@ -10,7 +10,7 @@
| App "lam" "lam"
| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
-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))"
--- a/Nominal/Ex/Classical.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Classical.thy Mon May 19 12:45:26 2014 +0100
@@ -47,7 +47,7 @@
thm trm.supp
thm trm.supp[simplified]
-nominal_primrec
+nominal_function
crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100)
where
"(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)"
@@ -252,7 +252,7 @@
termination (eqvt)
by lexicographic_order
-nominal_primrec
+nominal_function
nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm" ("_[_\<turnstile>n>_]" [100,100,100] 100)
where
"(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)"
@@ -449,7 +449,7 @@
thm crename.eqvt nrename.eqvt
-nominal_primrec
+nominal_function
substn :: "trm \<Rightarrow> name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100)
where
"(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)"
--- a/Nominal/Ex/Exec/Lambda_Exec.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Exec/Lambda_Exec.thy Mon May 19 12:45:26 2014 +0100
@@ -7,7 +7,7 @@
| App "lam" "lam"
| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
-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))"
@@ -122,7 +122,7 @@
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)
-nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
+nominal_function (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
lam_ln_aux :: "lam \<Rightarrow> name list \<Rightarrow> ln"
where
"lam_ln_aux (Var x) xs = lookup xs 0 x"
@@ -164,7 +164,7 @@
apply simp_all
done
-nominal_primrec
+nominal_function
ln_lam_aux :: "ln \<Rightarrow> name list \<Rightarrow> lam"
where
"ln_lam_aux (LNBnd n) ns = (nth_or_def (map Var ns) n (Lam [x]. Var x))"
@@ -321,7 +321,7 @@
"atom y \<sharp> subst_ln_nat t x n \<longleftrightarrow> y = x \<or> atom y \<sharp> t"
unfolding fresh_def supp_subst_ln_nat by auto
-nominal_primrec
+nominal_function
lam_ln_ex :: "lam \<Rightarrow> ln"
where
"lam_ln_ex (Var x) = LNVar x"
--- a/Nominal/Ex/FiniteType.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/FiniteType.thy Mon May 19 12:45:26 2014 +0100
@@ -16,4 +16,4 @@
-end
\ No newline at end of file
+end
--- a/Nominal/Ex/LamTest.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LamTest.thy Mon May 19 12:45:26 2014 +0100
@@ -1507,7 +1507,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof "nominal_primrec" "define recursive functions for nominal types"
+ Outer_Syntax.local_theory_to_proof "nominal_function" "define recursive functions for nominal types"
Keyword.thy_goal
(function_parser default_config
>> (fn ((config, fixes), statements) => function_cmd fixes statements config))
@@ -1545,7 +1545,7 @@
shows "(a \<rightleftharpoons> c) \<bullet> x = (b \<rightleftharpoons> c) \<bullet> y"
using assms by (simp add: swap_fresh_fresh)
-nominal_primrec
+nominal_function
depth :: "lam \<Rightarrow> nat"
where
"depth (Var x) = 1"
@@ -1566,7 +1566,7 @@
shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
by (induct xs) (auto)
-nominal_primrec
+nominal_function
frees_lst :: "lam \<Rightarrow> atom list"
where
"frees_lst (Var x) = [atom x]"
@@ -1585,7 +1585,7 @@
apply(clarify)
oops
-nominal_primrec
+nominal_function
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100)
where
"(Var x)[y ::= s] = (if x=y then s else (Var x))"
@@ -1608,7 +1608,7 @@
-nominal_primrec
+nominal_function
depth :: "lam \<Rightarrow> nat"
where
"depth (Var x) = 1"
@@ -1665,7 +1665,7 @@
shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
by (induct xs) (auto)
-nominal_primrec
+nominal_function
frees_lst :: "lam \<Rightarrow> atom list"
where
"frees_lst (Var x) = [atom x]"
@@ -1687,7 +1687,7 @@
apply(rule_tac p="p" in supp_perm_eq)
oops
-nominal_primrec
+nominal_function
frees :: "lam \<Rightarrow> name set"
where
"frees (Var x) = {x}"
@@ -1771,7 +1771,7 @@
apply(simp add: set_eqvt)
sorry
-nominal_primrec
+nominal_function
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100)
where
"(Var x)[y ::= s] = (if x=y then s else (Var x))"
@@ -1822,7 +1822,7 @@
-nominal_primrec
+nominal_function
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100)
where
"(Var x)[y ::= s] = (if x=y then s else (Var x))"
@@ -1874,7 +1874,7 @@
done
(* this should not work *)
-nominal_primrec
+nominal_function
bnds :: "lam \<Rightarrow> name set"
where
"bnds (Var x) = {}"
--- 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)"
--- a/Nominal/Ex/Lambda_F_T.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Lambda_F_T.thy Mon May 19 12:45:26 2014 +0100
@@ -47,7 +47,7 @@
and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"
begin
-nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
+nominal_function (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
f
where
"f (Var x) l = f1 x l"
@@ -157,7 +157,7 @@
\<Longrightarrow> P"
sorry
-nominal_primrec
+nominal_function
g
where
"(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t"
--- a/Nominal/Ex/Lambda_F_T_FCB2.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Lambda_F_T_FCB2.thy Mon May 19 12:45:26 2014 +0100
@@ -133,7 +133,7 @@
and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"
begin
-nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
+nominal_function (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
f
where
"f (Var x) l = f1 x l"
@@ -244,7 +244,7 @@
\<Longrightarrow> P"
sorry
-nominal_primrec
+nominal_function
g
where
"(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t"
--- a/Nominal/Ex/Let.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Let.thy Mon May 19 12:45:26 2014 +0100
@@ -107,7 +107,7 @@
apply simp_all
done
-nominal_primrec
+nominal_function
height_trm :: "trm \<Rightarrow> nat"
where
"height_trm (Var x) = 1"
@@ -160,7 +160,7 @@
apply (simp_all add: trm_assn.bn_defs)
done
-nominal_primrec
+nominal_function
subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
where
"subst s t (Var x) = (if (s = x) then t else (Var x))"
--- a/Nominal/Ex/LetFun.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetFun.thy Mon May 19 12:45:26 2014 +0100
@@ -40,4 +40,4 @@
thm exp_pat.supp
-end
\ No newline at end of file
+end
--- a/Nominal/Ex/LetInv.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetInv.thy Mon May 19 12:45:26 2014 +0100
@@ -223,7 +223,7 @@
apply (simp add: Abs_eq_iff alphas supp_atom fresh_star_def neq)
done
-nominal_primrec
+nominal_function
subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
where
"subst s t (Var x) = (if (s = x) then t else (Var x))"
--- a/Nominal/Ex/LetRec.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetRec.thy Mon May 19 12:45:26 2014 +0100
@@ -28,7 +28,7 @@
thm let_rec.size_eqvt
-nominal_primrec
+nominal_function
height_trm :: "trm \<Rightarrow> nat"
and height_bp :: "bp \<Rightarrow> nat"
where
--- a/Nominal/Ex/LetRecFunNo.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetRecFunNo.thy Mon May 19 12:45:26 2014 +0100
@@ -17,7 +17,7 @@
"bn ANil = []"
| "bn (ACons x t as) = (atom x) # (bn as)"
-nominal_primrec substrec where
+nominal_function substrec where
"substrec fa fl fd y z (Var x) = (if (y = x) then z else (Var x))"
| "substrec fa fl fd y z (App l r) = fa l r"
| "(set (bn as) \<sharp>* (Let as t, y, z) \<and> (\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow>
@@ -55,7 +55,7 @@
done
termination (eqvt) by lexicographic_order
-nominal_primrec substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where
+nominal_function substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where
"substarec fac ANil = ANil"
| "substarec fac (ACons x t as) = fac x t as"
unfolding eqvt_def substarec_graph_def
--- a/Nominal/Ex/LetSimple1.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetSimple1.thy Mon May 19 12:45:26 2014 +0100
@@ -25,7 +25,7 @@
thm trm.strong_exhaust
thm trm.perm_bn_simps
-nominal_primrec
+nominal_function
height_trm :: "trm \<Rightarrow> nat"
where
"height_trm (Var x) = 1"
@@ -51,7 +51,7 @@
by lexicographic_order
-nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
+nominal_function (invariant "\<lambda>x (y::atom set). finite y")
frees_set :: "trm \<Rightarrow> atom set"
where
"frees_set (Var x) = {atom x}"
@@ -79,7 +79,7 @@
by lexicographic_order
-nominal_primrec
+nominal_function
subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90)
where
"(Var x)[y ::= s] = (if x = y then s else (Var x))"
@@ -108,4 +108,4 @@
by lexicographic_order
-end
\ No newline at end of file
+end
--- a/Nominal/Ex/LetSimple2.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetSimple2.thy Mon May 19 12:45:26 2014 +0100
@@ -111,7 +111,7 @@
done
-nominal_primrec
+nominal_function
height_trm :: "trm \<Rightarrow> nat"
where
"height_trm (Var x) = 1"
@@ -143,7 +143,7 @@
termination by lexicographic_order
*)
-nominal_primrec
+nominal_function
subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90)
where
"(Var x)[y ::= s] = (if x = y then s else (Var x))"
@@ -197,7 +197,7 @@
-nominal_primrec
+nominal_function
<<<<<<< variant A
(invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> alpha_bn_preserve (height_assn2::assn \<Rightarrow> nat) x2")
>>>>>>> variant B
@@ -334,7 +334,7 @@
text {* works, but only because no recursion in as *}
-nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
+nominal_function (invariant "\<lambda>x (y::atom set). finite y")
frees_set :: "trm \<Rightarrow> atom set"
where
"frees_set (Var x) = {atom x}"
@@ -381,7 +381,7 @@
done
-nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
+nominal_function (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
subst_trm2 :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::trm2= _]" [90, 90, 90] 90) and
subst_assn2 :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn" ("_ [_ ::assn2= _]" [90, 90, 90] 90)
where
@@ -488,4 +488,4 @@
done
-end
\ No newline at end of file
+end
--- a/Nominal/Ex/Let_ExhaustIssue.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Let_ExhaustIssue.thy Mon May 19 12:45:26 2014 +0100
@@ -64,7 +64,7 @@
shows "f as x c = f bs y c"
sorry
-nominal_primrec
+nominal_function
height_trm :: "trm \<Rightarrow> nat"
and height_assn :: "assn \<Rightarrow> nat"
where
--- a/Nominal/Ex/Local_Contexts.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Local_Contexts.thy Mon May 19 12:45:26 2014 +0100
@@ -29,7 +29,7 @@
lemma atom_image_set_eq_supp: "atom ` set xs = supp xs"
by (metis image_set set_map_atom_eq_supp)
-nominal_primrec (in name_subst)
+nominal_function (in name_subst)
subst :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [120,120,120] 120)
where
"(Var x)[xs::=t] = name_subst x xs t"
--- a/Nominal/Ex/NBE.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/NBE.thy Mon May 19 12:45:26 2014 +0100
@@ -88,7 +88,7 @@
using assms by (auto simp add: fresh_star_def)
-nominal_primrec (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow>
+nominal_function (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow>
supp y \<subseteq> (supp y1 - set (bn x1)) \<union> (fv_bn x1) | Inr (x2, y2) \<Rightarrow> supp y \<subseteq> supp x2 \<union> supp y2")
evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem"
@@ -346,7 +346,7 @@
done
-nominal_primrec
+nominal_function
reify :: "sem \<Rightarrow> lam" and
reifyn :: "neu \<Rightarrow> lam"
where
@@ -543,4 +543,4 @@
where
"normalize t = reify (eval t)"
-end
\ No newline at end of file
+end
--- a/Nominal/Ex/PaperTest.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/PaperTest.thy Mon May 19 12:45:26 2014 +0100
@@ -300,4 +300,4 @@
apply(relation "measure (\<lambda>(_, t). size t)")
apply(simp_all)
-end
\ No newline at end of file
+end
--- a/Nominal/Ex/Pi.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Pi.thy Mon May 19 12:45:26 2014 +0100
@@ -27,7 +27,7 @@
by(auto)
qed
-nominal_primrec
+nominal_function
subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name"
where
"subst_name_list a [] = a"
@@ -143,7 +143,7 @@
shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))"
using a by auto
-nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
+nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix" ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and
subsList_mix :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix" ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and
subs_mix :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix" ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)
@@ -568,4 +568,4 @@
nominal_inductive fresh_list_mix
done
-end
\ No newline at end of file
+end
--- a/Nominal/Ex/SFT/Consts.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/SFT/Consts.thy Mon May 19 12:45:26 2014 +0100
@@ -71,7 +71,7 @@
"p \<bullet> VAR = VAR" "p \<bullet> APP = APP" "p \<bullet> Abs = Abs"
by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
-nominal_primrec
+nominal_function
Numeral :: "lam \<Rightarrow> lam" ("\<lbrace>_\<rbrace>" 1000)
where
"\<lbrace>Var x\<rbrace> = VAR \<cdot> (Var x)"
@@ -128,7 +128,7 @@
lemma app_lst_rev_eq_iff: "app_lst n (rev M) = app_lst n (rev N) \<Longrightarrow> M = N"
by (drule app_lst_eq_iff) simp
-nominal_primrec
+nominal_function
Ltgt :: "lam list \<Rightarrow> lam" ("\<guillemotleft>_\<guillemotright>" 1000)
where
[simp del]: "atom x \<sharp> l \<Longrightarrow> \<guillemotleft>l\<guillemotright> = \<integral>x. (app_lst x (rev l))"
--- a/Nominal/Ex/SFT/LambdaTerms.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/SFT/LambdaTerms.thy Mon May 19 12:45:26 2014 +0100
@@ -16,7 +16,7 @@
App (infixl "\<cdot>" 98) and
Lam ("\<integral> _. _" [97, 97] 99)
-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))"
--- a/Nominal/Ex/SubstNoFcb.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/SubstNoFcb.thy Mon May 19 12:45:26 2014 +0100
@@ -7,7 +7,7 @@
| App "lam" "lam"
| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
-nominal_primrec lam_rec ::
+nominal_function lam_rec ::
"(name \<Rightarrow> 'a :: pt) \<Rightarrow> (lam \<Rightarrow> lam \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> lam \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b :: fs \<Rightarrow> lam \<Rightarrow> 'a"
where
"lam_rec fv fa fl fd P (Var n) = fv n"
@@ -49,7 +49,7 @@
using Abs1_eq_iff lam.eq_iff apply metis
done
-nominal_primrec substr where
+nominal_function substr where
[simp del]: "substr l y s = lam_rec
(%x. if x = y then s else (Var x))
(%t1 t2. App (substr t1 y s) (substr t2 y s))
--- a/Nominal/Ex/TypeSchemes1.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/TypeSchemes1.thy Mon May 19 12:45:26 2014 +0100
@@ -75,7 +75,7 @@
shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
by (induct Ts T rule: lookup.induct) (simp_all)
-nominal_primrec
+nominal_function
subst :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)
where
"\<theta><Var X> = lookup \<theta> X"
@@ -114,7 +114,7 @@
unfolding eqvt_def
by (simp add: permute_fun_def subst.eqvt)
-nominal_primrec
+nominal_function
substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
where
"fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
@@ -272,7 +272,7 @@
apply(simp add: fresh_def supp_perm)
done
-nominal_primrec
+nominal_function
generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")
where
"atom ` (fset Xs) \<sharp>* T \<Longrightarrow>
@@ -399,7 +399,7 @@
apply(simp add: compose_ty[symmetric] subst_id2 compose_Dom)
done
-nominal_primrec
+nominal_function
ftv :: "ty \<Rightarrow> name fset"
where
"ftv (Var X) = {|X|}"
--- a/Nominal/Ex/TypeSchemes2.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/TypeSchemes2.thy Mon May 19 12:45:26 2014 +0100
@@ -61,7 +61,7 @@
using a
by clarsimp
-nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
+nominal_function (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
where
--- a/Nominal/Nominal2.thy Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Nominal2.thy Mon May 19 12:45:26 2014 +0100
@@ -3,7 +3,7 @@
Nominal2_Base Nominal2_Abs Nominal2_FCB
keywords
"nominal_datatype" :: thy_decl and
- "nominal_primrec" "nominal_inductive" :: thy_goal and
+ "nominal_function" "nominal_inductive" :: thy_goal and
"avoids" "binds"
begin
--- a/Nominal/nominal_function.ML Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/nominal_function.ML Mon May 19 12:45:26 2014 +0100
@@ -275,7 +275,7 @@
(* nominal *)
val _ =
- Outer_Syntax.local_theory_to_proof' @{command_spec "nominal_primrec"}
+ Outer_Syntax.local_theory_to_proof' @{command_spec "nominal_function"}
"define general recursive nominal functions"
(nominal_function_parser nominal_default_config
>> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
--- a/README Mon May 19 11:19:48 2014 +0100
+++ b/README Mon May 19 12:45:26 2014 +0100
@@ -6,6 +6,12 @@
isabelle build -d . -g Tests
+The version of Nominal2 in the AFP can be tested with
+
+isabelle build -d . Nominal2
+isabelle build -d . Launchbury
+
+
Subdirectories:
===============
--- a/Tutorial/Lambda.thy Mon May 19 11:19:48 2014 +0100
+++ b/Tutorial/Lambda.thy Mon May 19 12:45:26 2014 +0100
@@ -32,7 +32,7 @@
subsection {* Height Function *}
-nominal_primrec
+nominal_function
height :: "lam \<Rightarrow> int"
where
"height (Var x) = 1"
@@ -53,7 +53,7 @@
subsection {* 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))"
--- a/Tutorial/Minimal.thy Mon May 19 11:19:48 2014 +0100
+++ b/Tutorial/Minimal.thy Mon May 19 12:45:26 2014 +0100
@@ -15,4 +15,4 @@
shows "Lam [x]. (Var x) = Lam [y]. (Var y)"
by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)
-end
\ No newline at end of file
+end
--- a/Tutorial/Tutorial6.thy Mon May 19 11:19:48 2014 +0100
+++ b/Tutorial/Tutorial6.thy Mon May 19 12:45:26 2014 +0100
@@ -46,4 +46,4 @@
by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def)
-end
\ No newline at end of file
+end