# HG changeset patch # User Christian Urban # Date 1309884154 -7200 # Node ID 0911cb7bf696b703ae8121e295b5cd83bed1802a # Parent adf22ee09738b8b1ca73e73d56f53660025a3fed changed bind to binds in specifications; bind will cause trouble with Monad_Syntax diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Classical.thy Tue Jul 05 18:42:34 2011 +0200 @@ -10,27 +10,27 @@ nominal_datatype trm = Ax "name" "coname" -| Cut c::"coname" t1::"trm" n::"name" t2::"trm" bind n in t1, bind c in t2 +| Cut c::"coname" t1::"trm" n::"name" t2::"trm" binds n in t1, binds c in t2 ("Cut <_>._ '(_')._" [100,100,100,100] 100) -| NotR n::"name" t::"trm" "coname" bind n in t +| NotR n::"name" t::"trm" "coname" binds n in t ("NotR '(_')._ _" [100,100,100] 100) -| NotL c::"coname" t::"trm" "name" bind c in t +| NotL c::"coname" t::"trm" "name" binds c in t ("NotL <_>._ _" [100,100,100] 100) -| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 +| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" binds c1 in t1, binds c2 in t2 ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100) -| AndL1 n::"name" t::"trm" "name" bind n in t +| AndL1 n::"name" t::"trm" "name" binds n in t ("AndL1 '(_')._ _" [100,100,100] 100) -| AndL2 n::"name" t::"trm" "name" bind n in t +| AndL2 n::"name" t::"trm" "name" binds n in t ("AndL2 '(_')._ _" [100,100,100] 100) -| OrR1 c::"coname" t::"trm" "coname" bind c in t +| OrR1 c::"coname" t::"trm" "coname" binds c in t ("OrR1 <_>._ _" [100,100,100] 100) -| OrR2 c::"coname" t::"trm" "coname" bind c in t +| OrR2 c::"coname" t::"trm" "coname" binds c in t ("OrR2 <_>._ _" [100,100,100] 100) -| OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name" bind n1 in t1, bind n2 in t2 +| OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name" binds n1 in t1, binds n2 in t2 ("OrL '(_')._ '(_')._ _" [100,100,100,100,100] 100) -| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 +| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" binds c in t1, binds n in t2 ("ImpL <_>._ '(_')._ _" [100,100,100,100,100] 100) -| ImpR n::"name" c::"coname" t::"trm" "coname" bind n c in t +| ImpR n::"name" c::"coname" t::"trm" "coname" binds n c in t ("ImpR '(_').<_>._ _" [100,100,100,100] 100) thm trm.distinct diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/CoreHaskell.thy Tue Jul 05 18:42:34 2011 +0200 @@ -19,7 +19,7 @@ | TC "string" | TApp "ty" "ty" | TFun "string" "ty_lst" -| TAll tv::"tvar" "tkind" T::"ty" bind (set) tv in T +| TAll tv::"tvar" "tkind" T::"ty" binds (set) tv in T | TEq "ckind" "ty" and ty_lst = TsNil @@ -29,7 +29,7 @@ | CConst "string" | CApp "co" "co" | CFun "string" "co_lst" -| CAll cv::"cvar" "ckind" C::"co" bind (set) cv in C +| CAll cv::"cvar" "ckind" C::"co" binds (set) cv in C | CEq "ckind" "co" | CRefl "ty" | CSym "co" @@ -47,18 +47,18 @@ and trm = Var "var" | K "string" -| LAMT tv::"tvar" "tkind" t::"trm" bind (set) tv in t -| LAMC cv::"cvar" "ckind" t::"trm" bind (set) cv in t +| LAMT tv::"tvar" "tkind" t::"trm" binds (set) tv in t +| LAMC cv::"cvar" "ckind" t::"trm" binds (set) cv in t | AppT "trm" "ty" | AppC "trm" "co" -| Lam v::"var" "ty" t::"trm" bind (set) v in t +| Lam v::"var" "ty" t::"trm" binds (set) v in t | App "trm" "trm" -| Let x::"var" "ty" "trm" t::"trm" bind (set) x in t +| Let x::"var" "ty" "trm" t::"trm" binds (set) x in t | Case "trm" "assoc_lst" | Cast "trm" "ty" --"ty is supposed to be a coercion type only" and assoc_lst = ANil -| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t +| ACons p::"pat" t::"trm" "assoc_lst" binds "bv p" in t and pat = Kpat "string" "tvars" "cvars" "vars" and vars = diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/CoreHaskell2.thy --- a/Nominal/Ex/CoreHaskell2.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/CoreHaskell2.thy Tue Jul 05 18:42:34 2011 +0200 @@ -20,7 +20,7 @@ Tvar tvar | Tcon string | Tapp Ty Ty - | Tforall pb::PBind ty::Ty bind "bind_pb pb" in ty + | Tforall pb::PBind ty::Ty binds "bind_pb pb" in ty and PBind = Pbind tvar Kind binder @@ -37,7 +37,7 @@ | Dcon string | App Exp Exp | Appt Exp Ty - | Lam b::Bind e::Exp bind "bind_b b" in e + | Lam b::Bind e::Exp binds "bind_b b" in e binder bind_b where diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Datatypes.thy --- a/Nominal/Ex/Datatypes.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Datatypes.thy Tue Jul 05 18:42:34 2011 +0200 @@ -53,7 +53,7 @@ nominal_datatype baz = - Baz x::name t::foo bind x in t + Baz x::name t::foo binds x in t @@ -78,7 +78,7 @@ Set_ty "nat set" | Fun "nat \ nat" | Var "name" -| Lam x::"name" t::"set_ty" bind x in t +| Lam x::"name" t::"set_ty" binds x in t thm meta_eq_to_obj_eq thm set_ty.distinct thm set_ty.induct diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Ex1.thy --- a/Nominal/Ex/Ex1.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Ex1.thy Tue Jul 05 18:42:34 2011 +0200 @@ -10,10 +10,10 @@ nominal_datatype foo = Foo0 "name" -| Foo1 b::"bar" f::"foo" bind (set) "bv b" in f +| Foo1 b::"bar" f::"foo" binds (set) "bv b" in f and bar = Bar0 "name" -| Bar1 "name" s::"name" b::"bar" bind (set) s in b +| Bar1 "name" s::"name" b::"bar" binds (set) s in b binder bv where diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/ExPS3.thy --- a/Nominal/Ex/ExPS3.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/ExPS3.thy Tue Jul 05 18:42:34 2011 +0200 @@ -9,8 +9,8 @@ nominal_datatype exp = Var "name" | App "exp" "exp" -| Lam x::"name" e::"exp" bind x in e -| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind (set) x in e2, bind (set) "bp p" in e1 +| Lam x::"name" e::"exp" binds x in e +| Let x::"name" p::"pat" e1::"exp" e2::"exp" binds (set) x in e2, binds (set) "bp p" in e1 and pat = PVar "name" | PUnit diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Foo1.thy --- a/Nominal/Ex/Foo1.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Foo1.thy Tue Jul 05 18:42:34 2011 +0200 @@ -13,11 +13,11 @@ nominal_datatype foo: trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind x in t -| Let1 a::"assg" t::"trm" bind "bn1 a" in t -| Let2 a::"assg" t::"trm" bind "bn2 a" in t -| Let3 a::"assg" t::"trm" bind "bn3 a" in t -| Let4 a::"assg'" t::"trm" bind (set) "bn4 a" in t +| Lam x::"name" t::"trm" binds x in t +| Let1 a::"assg" t::"trm" binds "bn1 a" in t +| Let2 a::"assg" t::"trm" binds "bn2 a" in t +| Let3 a::"assg" t::"trm" binds "bn3 a" in t +| Let4 a::"assg'" t::"trm" binds (set) "bn4 a" in t and assg = As "name" "name" "trm" and assg' = diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Foo2.thy Tue Jul 05 18:42:34 2011 +0200 @@ -13,9 +13,9 @@ nominal_datatype foo: trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind x in t -| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2 -| Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2 +| Lam x::"name" t::"trm" binds x in t +| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" binds "bn a1" in t1, binds "bn a2" in t2 +| Let2 x::"name" y::"name" t1::"trm" t2::"trm" binds x y in t1, binds y in t2 and assg = As_Nil | As "name" x::"name" t::"trm" "assg" diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/LF.thy --- a/Nominal/Ex/LF.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LF.thy Tue Jul 05 18:42:34 2011 +0200 @@ -8,16 +8,16 @@ nominal_datatype lf: kind = Type - | KPi "ty" n::"name" k::"kind" bind n in k + | KPi "ty" n::"name" k::"kind" binds n in k and ty = TConst "ident" | TApp "ty" "trm" - | TPi "ty" n::"name" ty::"ty" bind n in ty + | TPi "ty" n::"name" ty::"ty" binds n in ty and trm = Const "ident" | Var "name" | App "trm" "trm" - | Lam' "ty" n::"name" t::"trm" bind n in t + | Lam' "ty" n::"name" t::"trm" binds n in t abbreviation KPi_syn::"name \ ty \ kind \ kind" ("\[_:_]._" [100,100,100] 100) diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/LamFun.thy --- a/Nominal/Ex/LamFun.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LamFun.thy Tue Jul 05 18:42:34 2011 +0200 @@ -7,7 +7,7 @@ nominal_datatype lam = Var "name" | App "lam" "lam" -| Lam x::"name" l::"lam" bind x in l +| Lam x::"name" l::"lam" binds x in l thm lam.distinct thm lam.induct diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Lambda.thy Tue Jul 05 18:42:34 2011 +0200 @@ -1,5 +1,7 @@ theory Lambda -imports "../Nominal2" +imports + "../Nominal2" + "~~/src/HOL/Library/Monad_Syntax" begin @@ -8,7 +10,7 @@ nominal_datatype lam = Var "name" | App "lam" "lam" -| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) +| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) ML {* Method.SIMPLE_METHOD' *} ML {* Sign.intern_const *} @@ -320,24 +322,56 @@ termination by lexicographic_order + +text {* count the occurences of lambdas in a term *} + +nominal_primrec + cntlams :: "lam \ nat" +where + "cntlams (Var x) = 0" +| "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)" +| "cntlams (Lam [x]. t) = Suc (cntlams t)" + apply(simp add: eqvt_def cntlams_graph_def) + apply(rule, perm_simp, rule) + apply(rule TrueI) + apply(rule_tac y="x" in lam.exhaust) + apply(auto)[3] + apply(all_trivials) + apply(simp) + apply(simp) + apply(erule_tac c="()" in Abs_lst1_fcb2') + apply(simp add: pure_fresh) + apply(simp add: fresh_star_def pure_fresh) + apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + done + +termination + by lexicographic_order + + text {* count the bound-variable occurences in a lambda-term *} nominal_primrec - cbvs :: "lam \ name list \ nat" + cntbvs :: "lam \ name list \ nat" where - "cbvs (Var x) xs = (if x \ set xs then 1 else 0)" -| "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)" -| "atom x \ xs \ cbvs (Lam [x]. t) xs = cbvs t (x # xs)" - apply(simp add: eqvt_def cbvs_graph_def) + "cntbvs (Var x) xs = (if x \ set xs then 1 else 0)" +| "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)" +| "atom x \ xs \ cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)" + apply(simp add: eqvt_def cntbvs_graph_def) apply(rule, perm_simp, rule) - apply(simp_all) + apply(rule TrueI) apply(case_tac x) apply(rule_tac y="a" and c="b" in lam.strong_exhaust) apply(auto simp add: fresh_star_def)[3] + apply(all_trivials) + apply(simp) + apply(simp) + apply(simp) apply(erule conjE) apply(erule Abs_lst1_fcb2') apply(simp add: pure_fresh fresh_star_def) - apply(simp add: pure_fresh fresh_star_def) + apply(simp add: fresh_star_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) done @@ -380,11 +414,14 @@ "(p \ vindex l v n) = vindex (p \ l) (p \ v) (p \ n)" by (induct l arbitrary: n) (simp_all add: permute_pure) + + nominal_primrec transdb :: "lam \ name list \ db option" where "transdb (Var x) l = vindex l x 0" -| "transdb (App t1 t2) xs = Option.bind (transdb t1 xs) (\d1. Option.bind (transdb t2 xs) (\d2. Some (DBApp d1 d2)))" +| "transdb (App t1 t2) xs = + Option.bind (transdb t1 xs) (\d1. Option.bind (transdb t2 xs) (\d2. Some (DBApp d1 d2)))" | "x \ set xs \ transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))" unfolding eqvt_def transdb_graph_def apply (rule, perm_simp, rule) @@ -421,47 +458,6 @@ Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" using a by simp - -abbreviation - mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \= _" [65,65] 65) -where - "c \= f \ case c of None => None | (Some v) => f v" - -lemma mbind_eqvt: - fixes c::"'a::pt option" - shows "(p \ (c \= f)) = ((p \ c) \= (p \ f))" -apply(cases c) -apply(simp_all) -apply(perm_simp) -apply(rule refl) -done - -lemma mbind_eqvt_raw[eqvt_raw]: - shows "(p \ option_case) \ option_case" -apply(rule eq_reflection) -apply(rule ext)+ -apply(case_tac xb) -apply(simp_all) -apply(rule_tac p="-p" in permute_boolE) -apply(perm_simp add: permute_minus_cancel) -apply(simp) -apply(rule_tac p="-p" in permute_boolE) -apply(perm_simp add: permute_minus_cancel) -apply(simp) -done - -fun - index :: "atom list \ nat \ atom \ nat option" -where - "index [] n x = None" -| "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))" - -lemma [eqvt]: - shows "(p \ index xs n x) = index (p \ xs) (p \ n) (p \ x)" -apply(induct xs arbitrary: n) -apply(simp_all add: permute_pure) -done - lemma supp_subst: "supp (t[x ::= s]) \ supp t \ supp s" by (induct t x s rule: subst.induct) (auto simp add: lam.supp) @@ -569,13 +565,59 @@ termination by lexicographic_order + +(* +abbreviation + mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \= _" [65,65] 65) +where + "c \= f \ case c of None => None | (Some v) => f v" + +lemma mbind_eqvt: + fixes c::"'a::pt option" + shows "(p \ (c \= f)) = ((p \ c) \= (p \ f))" +apply(cases c) +apply(simp_all) +apply(perm_simp) +apply(rule refl) +done + +lemma mbind_eqvt_raw[eqvt_raw]: + shows "(p \ option_case) \ option_case" +apply(rule eq_reflection) +apply(rule ext)+ +apply(case_tac xb) +apply(simp_all) +apply(rule_tac p="-p" in permute_boolE) +apply(perm_simp add: permute_minus_cancel) +apply(simp) +apply(rule_tac p="-p" in permute_boolE) +apply(perm_simp add: permute_minus_cancel) +apply(simp) +done + +fun + index :: "atom list \ nat \ atom \ nat option" +where + "index [] n x = None" +| "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))" + +lemma [eqvt]: + shows "(p \ index xs n x) = index (p \ xs) (p \ n) (p \ x)" +apply(induct xs arbitrary: n) +apply(simp_all add: permute_pure) +done +*) + +(* nominal_primrec trans2 :: "lam \ atom list \ db option" where - "trans2 (Var x) xs = (index xs 0 (atom x) \= (\n. Some (DBVar n)))" -| "trans2 (App t1 t2) xs = ((trans2 t1 xs) \= (\db1. (trans2 t2 xs) \= (\db2. Some (DBApp db1 db2))))" -| "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \= (\db. Some (DBLam db)))" + "trans2 (Var x) xs = (index xs 0 (atom x) \= (\n::nat. Some (DBVar n)))" +| "trans2 (App t1 t2) xs = + ((trans2 t1 xs) \= (\db1::db. (trans2 t2 xs) \= (\db2::db. Some (DBApp db1 db2))))" +| "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \= (\db::db. Some (DBLam db)))" oops +*) nominal_primrec CPS :: "lam \ (lam \ lam) \ lam" diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Lambda_F_T.thy --- a/Nominal/Ex/Lambda_F_T.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Lambda_F_T.thy Tue Jul 05 18:42:34 2011 +0200 @@ -7,7 +7,7 @@ nominal_datatype lam = Var "name" | App "lam" "lam" -| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) +| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) lemma fresh_fun_eqvt_app3: assumes a: "eqvt f" diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Let.thy Tue Jul 05 18:42:34 2011 +0200 @@ -7,8 +7,8 @@ nominal_datatype trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind x in t -| Let as::"assn" t::"trm" bind "bn as" in t +| Lam x::"name" t::"trm" binds x in t +| Let as::"assn" t::"trm" binds "bn as" in t and assn = ANil | ACons "name" "trm" "assn" diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/LetFun.thy --- a/Nominal/Ex/LetFun.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LetFun.thy Tue Jul 05 18:42:34 2011 +0200 @@ -12,7 +12,7 @@ nominal_datatype exp = Var name | Pair exp exp -| LetRec x::name p::pat e1::exp e2::exp bind x in e2, bind x "bp p" in e1 +| LetRec x::name p::pat e1::exp e2::exp binds x in e2, binds x "bp p" in e1 and pat = PVar name | PUnit diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/LetInv.thy --- a/Nominal/Ex/LetInv.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LetInv.thy Tue Jul 05 18:42:34 2011 +0200 @@ -7,8 +7,8 @@ nominal_datatype trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind x in t -| Let as::"assn" t::"trm" bind "bn as" in t +| Lam x::"name" t::"trm" binds x in t +| Let as::"assn" t::"trm" binds "bn as" in t and assn = ANil | ACons "name" "trm" "assn" diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/LetPat.thy --- a/Nominal/Ex/LetPat.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LetPat.thy Tue Jul 05 18:42:34 2011 +0200 @@ -7,8 +7,8 @@ nominal_datatype trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind (set) x in t -| Let p::"pat" "trm" t::"trm" bind (set) "f p" in t +| Lam x::"name" t::"trm" binds (set) x in t +| Let p::"pat" "trm" t::"trm" binds (set) "f p" in t and pat = PN | PS "name" diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/LetRec.thy --- a/Nominal/Ex/LetRec.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LetRec.thy Tue Jul 05 18:42:34 2011 +0200 @@ -8,8 +8,8 @@ trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind (set) x in t -| Let_Rec bp::"bp" t::"trm" bind (set) "bn bp" in bp t +| Lam x::"name" t::"trm" binds (set) x in t +| Let_Rec bp::"bp" t::"trm" binds (set) "bn bp" in bp t and bp = Bp "name" "trm" binder diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/LetRec2.thy --- a/Nominal/Ex/LetRec2.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LetRec2.thy Tue Jul 05 18:42:34 2011 +0200 @@ -7,8 +7,8 @@ nominal_datatype trm = Vr "name" | Ap "trm" "trm" -| Lm x::"name" t::"trm" bind (set) x in t -| Lt a::"lts" t::"trm" bind "bn a" in a t +| Lm x::"name" t::"trm" binds (set) x in t +| Lt a::"lts" t::"trm" binds "bn a" in a t and lts = Lnil | Lcons "name" "trm" "lts" diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/LetRecB.thy --- a/Nominal/Ex/LetRecB.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LetRecB.thy Tue Jul 05 18:42:34 2011 +0200 @@ -8,8 +8,8 @@ trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind x in t -| Let_Rec bp::"bp" t::"trm" bind "bn bp" in bp t +| Lam x::"name" t::"trm" binds x in t +| Let_Rec bp::"bp" t::"trm" binds "bn bp" in bp t and bp = Bp "name" "trm" binder diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/LetSimple1.thy --- a/Nominal/Ex/LetSimple1.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LetSimple1.thy Tue Jul 05 18:42:34 2011 +0200 @@ -7,7 +7,7 @@ nominal_datatype trm = Var "name" | App "trm" "trm" -| Let x::"name" "trm" t::"trm" bind x in t +| Let x::"name" "trm" t::"trm" binds x in t print_theorems diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/LetSimple2.thy --- a/Nominal/Ex/LetSimple2.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LetSimple2.thy Tue Jul 05 18:42:34 2011 +0200 @@ -7,7 +7,7 @@ nominal_datatype trm = Var "name" | App "trm" "trm" -| Let as::"assn" t::"trm" bind "bn as" in t +| Let as::"assn" t::"trm" binds "bn as" in t and assn = Assn "name" "trm" binder diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Let_ExhaustIssue.thy --- a/Nominal/Ex/Let_ExhaustIssue.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Let_ExhaustIssue.thy Tue Jul 05 18:42:34 2011 +0200 @@ -8,8 +8,8 @@ nominal_datatype trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind x in t -| Let as::"assn" t::"trm" bind "bn as" in t +| Lam x::"name" t::"trm" binds x in t +| Let as::"assn" t::"trm" binds "bn as" in t and assn = ANil | ACons "name" "trm" "assn" diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Modules.thy --- a/Nominal/Ex/Modules.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Modules.thy Tue Jul 05 18:42:34 2011 +0200 @@ -14,12 +14,12 @@ mexp = Acc "path" | Stru "body" -| Funct x::"name" "sexp" m::"mexp" bind (set) x in m +| Funct x::"name" "sexp" m::"mexp" binds (set) x in m | FApp "mexp" "path" | Ascr "mexp" "sexp" and body = Empty -| Seq c::"defn" d::"body" bind (set) "cbinders c" in d +| Seq c::"defn" d::"body" binds (set) "cbinders c" in d and defn = Type "name" "ty" | Dty "name" @@ -30,7 +30,7 @@ | SFunc "name" "sexp" "sexp" and sbody = SEmpty -| SSeq C::"spec" D::"sbody" bind (set) "Cbinders C" in D +| SSeq C::"spec" D::"sbody" binds (set) "Cbinders C" in D and spec = Type1 "name" | Type2 "name" "ty" @@ -46,7 +46,7 @@ and trm = Tref1 "name" | Tref2 "path" "name" -| Lam' v::"name" "ty" M::"trm" bind (set) v in M +| Lam' v::"name" "ty" M::"trm" binds (set) v in M | App' "trm" "trm" | Let' "body" "trm" binder diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Multi_Recs.thy --- a/Nominal/Ex/Multi_Recs.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Multi_Recs.thy Tue Jul 05 18:42:34 2011 +0200 @@ -15,7 +15,7 @@ Var name | Unit | Pair exp exp -| LetRec l::"lrbs" e::"exp" bind (set) "bs l" in l e +| LetRec l::"lrbs" e::"exp" binds (set) "bs l" in l e and lrb = Assign name exp and lrbs = diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Multi_Recs2.thy --- a/Nominal/Ex/Multi_Recs2.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Multi_Recs2.thy Tue Jul 05 18:42:34 2011 +0200 @@ -17,9 +17,9 @@ Var name | Unit | Pair exp exp -| LetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e +| LetRec l::lrbs e::exp binds (set) "b_lrbs l" in l e and fnclause = - K x::name p::pat f::exp bind (set) "b_pat p" in f + K x::name p::pat f::exp binds (set) "b_pat p" in f and fnclauses = S fnclause | ORs fnclause fnclauses diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/NoneExamples.thy --- a/Nominal/Ex/NoneExamples.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/NoneExamples.thy Tue Jul 05 18:42:34 2011 +0200 @@ -20,8 +20,8 @@ Foo_var "name" | Foo_pair "weird" "weird" | Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" - bind x in p1 p2, - bind y in p2 p3 + binds x in p1 p2, + binds y in p2 p3 *) text {* @@ -32,8 +32,8 @@ (* nominal_datatype trm = Var "name" -| Lam x::"name" t::"trm" bind x in t -| Let left::"trm" right::"trm" bind (set) "bv left" in right +| Lam x::"name" t::"trm" binds x in t +| Let left::"trm" right::"trm" binds (set) "bv left" in right binder bv where @@ -50,8 +50,8 @@ (* nominal_datatype trm' = Var "name" -| Lam l::"name" r::"trm'" bind l in r -| Let l::"trm'" r::"trm'" bind (set) "bv' l" in r +| Lam l::"name" r::"trm'" binds l in r +| Let l::"trm'" r::"trm'" binds (set) "bv' l" in r binder bv' where @@ -67,9 +67,9 @@ (* nominal_datatype trm = Var "name" -| Lam n::"name" l::"trm" bind n in l +| Lam n::"name" l::"trm" binds n in l and bla = - Bla f::"trm" s::"trm" bind (set) "bv f" in s + Bla f::"trm" s::"trm" binds (set) "bv f" in s binder bv :: "trm \ atom set" where @@ -90,9 +90,9 @@ Var "name" and bla = App "trm" "trm" -| Bla1 f::"trm" s1::"trm" s2::"trm" bind "bv f" in s1 f, bind "bv f" in s2 f -| Bla2 f::"trm" s1::"trm" s2::"trm" bind "bv f" in s1, bind "bv f" in s2 f -| Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" bind "bv f" x in s1 f, bind y x in s2 +| Bla1 f::"trm" s1::"trm" s2::"trm" binds "bv f" in s1 f, binds "bv f" in s2 f +| Bla2 f::"trm" s1::"trm" s2::"trm" binds "bv f" in s1, binds "bv f" in s2 f +| Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" binds "bv f" x in s1 f, binds y x in s2 binder bv :: "trm \ atom list" where diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Shallow.thy --- a/Nominal/Ex/Shallow.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Shallow.thy Tue Jul 05 18:42:34 2011 +0200 @@ -13,7 +13,7 @@ nominal_datatype trm1 = Var1 "name" | App1 "trm1" "trm1" -| Lam1 xs::"name list" t::"trm1" bind xs in t +| Lam1 xs::"name list" t::"trm1" binds xs in t thm trm1.strong_exhaust @@ -23,7 +23,7 @@ nominal_datatype trm2 = Var2 "name" | App2 "trm2" "trm2" -| Lam2 xs::"name fset" t::"trm2" bind (set) xs in t +| Lam2 xs::"name fset" t::"trm2" binds (set) xs in t thm trm2.strong_exhaust @@ -32,7 +32,7 @@ nominal_datatype trm3 = Var3 "name" | App3 "trm3" "trm3" -| Lam3 xs::"name fset" t::"trm3" bind (set+) xs in t +| Lam3 xs::"name fset" t::"trm3" binds (set+) xs in t thm trm3.eq_iff diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/SingleLet.thy Tue Jul 05 18:42:34 2011 +0200 @@ -7,13 +7,13 @@ nominal_datatype single_let: trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind x in t -| Let a::"assg" t::"trm" bind "bn a" in t -| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2 -| Bar x::"name" y::"name" t::"trm" bind y x in t x y -| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set+) x in t2 +| Lam x::"name" t::"trm" binds x in t +| Let a::"assg" t::"trm" binds "bn a" in t +| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" binds (set) x in y t t1 t2 +| Bar x::"name" y::"name" t::"trm" binds y x in t x y +| Baz x::"name" t1::"trm" t2::"trm" binds (set) x in t1, binds (set+) x in t2 and assg = - As "name" x::"name" t::"trm" bind x in t + As "name" x::"name" t::"trm" binds x in t binder bn::"assg \ atom list" where diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/SystemFOmega.thy --- a/Nominal/Ex/SystemFOmega.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/SystemFOmega.thy Tue Jul 05 18:42:34 2011 +0200 @@ -19,9 +19,9 @@ nominal_datatype ty = TVar tvar | TFun ty ty -| TAll a::tvar kind t::ty bind a in t -| TEx a::tvar kind t::ty bind a in t -| TLam a::tvar kind t::ty bind a in t +| TAll a::tvar kind t::ty binds a in t +| TEx a::tvar kind t::ty binds a in t +| TLam a::tvar kind t::ty binds a in t | TApp ty ty | TRec trec and trec = @@ -30,13 +30,13 @@ nominal_datatype trm = Var var -| Lam x::var ty t::trm bind x in t +| Lam x::var ty t::trm binds x in t | App trm trm | Dot trm label -| LAM a::tvar kind t::trm bind a in t +| LAM a::tvar kind t::trm binds a in t | APP trm ty | Pack ty trm -| Unpack a::tvar x::var trm t::trm bind a x in t +| Unpack a::tvar x::var trm t::trm binds a x in t | Rec rec and rec = RNil diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/TypeSchemes.thy Tue Jul 05 18:42:34 2011 +0200 @@ -12,7 +12,7 @@ Var "name" | Fun "ty" "ty" and tys = - All xs::"name fset" ty::"ty" bind (set+) xs in ty + All xs::"name fset" ty::"ty" binds (set+) xs in ty ML {* get_all_info @{context} @@ -282,7 +282,7 @@ | Fun2 "ty2" "ty2" nominal_datatype tys2 = - All2 xs::"name fset" ty::"ty2" bind (set+) xs in ty + All2 xs::"name fset" ty::"ty2" binds (set+) xs in ty thm tys2.distinct thm tys2.induct tys2.strong_induct diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/TypeVarsTest.thy --- a/Nominal/Ex/TypeVarsTest.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/TypeVarsTest.thy Tue Jul 05 18:42:34 2011 +0200 @@ -20,9 +20,9 @@ nominal_datatype ('a, 'b, 'c) lam = Var "name" | App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam" -| Lam x::"name" l::"('a, 'b, 'c) lam" bind x in l +| Lam x::"name" l::"('a, 'b, 'c) lam" binds x in l | Foo "'a" "'b" -| Bar x::"'c" l::"('a, 'b, 'c) lam" bind x in l (* Bar binds a polymorphic atom *) +| Bar x::"'c" l::"('a, 'b, 'c) lam" binds x in l (* Bar binds a polymorphic atom *) term Foo term Bar diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Weakening.thy --- a/Nominal/Ex/Weakening.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Weakening.thy Tue Jul 05 18:42:34 2011 +0200 @@ -9,7 +9,7 @@ nominal_datatype lam = Var "name" | App "lam" "lam" -| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100,100] 100) +| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100,100] 100) text {* Typing *} diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Nominal2.thy Tue Jul 05 18:42:34 2011 +0200 @@ -679,13 +679,13 @@ fun tuple3 ((x, y), (z, u)) = (x, y, z, u) in -val _ = Keyword.keyword "bind" +val _ = Keyword.keyword "binds" val opt_name = Scan.option (P.binding --| Args.colon) val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ -val bind_mode = P.$$$ "bind" |-- +val bind_mode = P.$$$ "binds" |-- S.optional (Args.parens (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst