# HG changeset patch # User Cezary Kaliszyk # Date 1269331523 -3600 # Node ID e33e37fd4c7ddb7a3a1b5c34f0cfd0784495f7da # Parent 8b5a1ad6048764e2cc5c589a3a5d253688212e80 More reorganization. diff -r 8b5a1ad60487 -r e33e37fd4c7d Nominal/ExLeroy.thy --- a/Nominal/ExLeroy.thy Tue Mar 23 08:51:43 2010 +0100 +++ b/Nominal/ExLeroy.thy Tue Mar 23 09:05:23 2010 +0100 @@ -1,4 +1,4 @@ -theory Test +theory ExLeroy imports "Parser" begin diff -r 8b5a1ad60487 -r e33e37fd4c7d Nominal/ExLet.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/ExLet.thy Tue Mar 23 09:05:23 2010 +0100 @@ -0,0 +1,35 @@ +theory ExLet +imports "Parser" +begin + +text {* example 3 or example 5 from Terms.thy *} + +atom_decl name + +ML {* val _ = recursive := false *} +nominal_datatype trm = + Vr "name" +| Ap "trm" "trm" +| Lm x::"name" t::"trm" bind x in t +| Lt a::"lts" t::"trm" bind "bv a" in t +and lts = + Nil +| Cons "name" "trm" "lts" +binder + bn +where + "bn Nil = {}" +| "bn (Cons x t l) = {atom x} \ (bn l)" + +thm trm_lts.fv +thm trm_lts.eq_iff +thm trm_lts.bn +thm trm_lts.perm +thm trm_lts.induct +thm trm_lts.distinct +thm trm_lts.fv[simplified trm_lts.supp] + +end + + + diff -r 8b5a1ad60487 -r e33e37fd4c7d Nominal/ExNotRsp.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/ExNotRsp.thy Tue Mar 23 09:05:23 2010 +0100 @@ -0,0 +1,48 @@ +theory ExNotRsp +imports "Parser" +begin + +atom_decl name + +(* example 6 from Terms.thy *) + +nominal_datatype trm6 = + Vr6 "name" +| Lm6 x::"name" t::"trm6" bind x in t +| Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right +binder + bv6 +where + "bv6 (Vr6 n) = {}" +| "bv6 (Lm6 n t) = {atom n} \ bv6 t" +| "bv6 (Lt6 l r) = bv6 l \ bv6 r" + +(* example 7 from Terms.thy *) +nominal_datatype trm7 = + Vr7 "name" +| Lm7 l::"name" r::"trm7" bind l in r +| Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r +binder + bv7 +where + "bv7 (Vr7 n) = {atom n}" +| "bv7 (Lm7 n t) = bv7 t - {atom n}" +| "bv7 (Lt7 l r) = bv7 l \ bv7 r" +*) + +(* example 9 from Terms.thy *) +nominal_datatype lam9 = + Var9 "name" +| Lam9 n::"name" l::"lam9" bind n in l +and bla9 = + Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s +binder + bv9 +where + "bv9 (Var9 x) = {}" +| "bv9 (Lam9 x b) = {atom x}" + +end + + + diff -r 8b5a1ad60487 -r e33e37fd4c7d Nominal/ExPS3.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/ExPS3.thy Tue Mar 23 09:05:23 2010 +0100 @@ -0,0 +1,37 @@ +theory ExPS3 +imports "Parser" +begin + +(* example 3 from Peter Sewell's bestiary *) + +atom_decl name + +ML {* val _ = recursive := false *} +nominal_datatype exp = + VarP "name" +| AppP "exp" "exp" +| LamP x::"name" e::"exp" bind x in e +| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1 +and pat3 = + PVar "name" +| PUnit +| PPair "pat3" "pat3" +binder + bp'' :: "pat3 \ atom set" +where + "bp'' (PVar x) = {atom x}" +| "bp'' (PUnit) = {}" +| "bp'' (PPair p1 p2) = bp'' p1 \ bp'' p2" + +thm exp_pat3.fv +thm exp_pat3.eq_iff +thm exp_pat3.bn +thm exp_pat3.perm +thm exp_pat3.induct +thm exp_pat3.distinct +thm exp_pat3.fv[simplified exp_pat3.supp] + +end + + + diff -r 8b5a1ad60487 -r e33e37fd4c7d Nominal/ExPS6.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/ExPS6.thy Tue Mar 23 09:05:23 2010 +0100 @@ -0,0 +1,35 @@ +theory ExPS6 +imports "Parser" +begin + +(* example 6 from Peter Sewell's bestiary *) + +atom_decl name + +ML {* val _ = recursive := false *} +nominal_datatype exp6 = + EVar name +| EPair exp6 exp6 +| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1 +and pat6 = + PVar' name +| PUnit' +| PPair' pat6 pat6 +binder + bp6 :: "pat6 \ atom set" +where + "bp6 (PVar' x) = {atom x}" +| "bp6 (PUnit') = {}" +| "bp6 (PPair' p1 p2) = bp6 p1 \ bp6 p2" + +thm exp6_pat6.fv +thm exp6_pat6.eq_iff +thm exp6_pat6.bn +thm exp6_pat6.perm +thm exp6_pat6.induct +thm exp6_pat6.distinct + +end + + + diff -r 8b5a1ad60487 -r e33e37fd4c7d Nominal/NotRsp.thy --- a/Nominal/NotRsp.thy Tue Mar 23 08:51:43 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -theory NotRsp -imports "Parser" "../Attic/Prove" -begin - -atom_decl name - -(* example 6 from Terms.thy *) - -nominal_datatype trm6 = - Vr6 "name" -| Lm6 x::"name" t::"trm6" bind x in t -| Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right -binder - bv6 -where - "bv6 (Vr6 n) = {}" -| "bv6 (Lm6 n t) = {atom n} \ bv6 t" -| "bv6 (Lt6 l r) = bv6 l \ bv6 r" - -(* example 7 from Terms.thy *) -nominal_datatype trm7 = - Vr7 "name" -| Lm7 l::"name" r::"trm7" bind l in r -| Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r -binder - bv7 -where - "bv7 (Vr7 n) = {atom n}" -| "bv7 (Lm7 n t) = bv7 t - {atom n}" -| "bv7 (Lt7 l r) = bv7 l \ bv7 r" -*) - -(* example 9 from Terms.thy *) -nominal_datatype lam9 = - Var9 "name" -| Lam9 n::"name" l::"lam9" bind n in l -and bla9 = - Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s -binder - bv9 -where - "bv9 (Var9 x) = {}" -| "bv9 (Lam9 x b) = {atom x}" - -end - - - diff -r 8b5a1ad60487 -r e33e37fd4c7d Nominal/Test.thy --- a/Nominal/Test.thy Tue Mar 23 08:51:43 2010 +0100 +++ b/Nominal/Test.thy Tue Mar 23 09:05:23 2010 +0100 @@ -2,109 +2,13 @@ imports "Parser" begin +(* This file contains only the examples that are not supposed to work yet. *) + + atom_decl name ML {* val _ = recursive := false *} -text {* example 3 from Terms.thy *} - -nominal_datatype trm3 = - Vr3 "name" -| Ap3 "trm3" "trm3" -| Lm3 x::"name" t::"trm3" bind x in t -| Lt3 r::"rassigns3" t::"trm3" bind "bv3 r" in t -and rassigns3 = - ANil -| ACons "name" "trm3" "rassigns3" -binder - bv3 -where - "bv3 ANil = {}" -| "bv3 (ACons x t as) = {atom x} \ (bv3 as)" - -thm trm3_rassigns3.fv -thm trm3_rassigns3.eq_iff -thm trm3_rassigns3.bn -thm trm3_rassigns3.perm -thm trm3_rassigns3.induct -thm trm3_rassigns3.distinct -thm trm3_rassigns3.fv[simplified trm3_rassigns3.supp] - -(* example 5 from Terms.thy *) - -nominal_datatype trm5 = - Vr5 "name" -| Ap5 "trm5" "trm5" -| Lt5 l::"lts" t::"trm5" bind "bv5 l" in t -and lts = - Lnil -| Lcons "name" "trm5" "lts" -binder - bv5 -where - "bv5 Lnil = {}" -| "bv5 (Lcons n t ltl) = {atom n} \ (bv5 ltl)" - -thm trm5_lts.fv -thm trm5_lts.eq_iff -thm trm5_lts.bn -thm trm5_lts.perm -thm trm5_lts.induct -thm trm5_lts.distinct -thm trm5_lts.fv[simplified trm5_lts.supp] - -(* example 3 from Peter Sewell's bestiary *) - -nominal_datatype exp = - VarP "name" -| AppP "exp" "exp" -| LamP x::"name" e::"exp" bind x in e -| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1 -and pat3 = - PVar "name" -| PUnit -| PPair "pat3" "pat3" -binder - bp'' :: "pat3 \ atom set" -where - "bp'' (PVar x) = {atom x}" -| "bp'' (PUnit) = {}" -| "bp'' (PPair p1 p2) = bp'' p1 \ bp'' p2" - -thm exp_pat3.fv -thm exp_pat3.eq_iff -thm exp_pat3.bn -thm exp_pat3.perm -thm exp_pat3.induct -thm exp_pat3.distinct -thm exp_pat3.fv[simplified exp_pat3.supp] - -(* example 6 from Peter Sewell's bestiary *) -nominal_datatype exp6 = - EVar name -| EPair exp6 exp6 -| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1 -and pat6 = - PVar' name -| PUnit' -| PPair' pat6 pat6 -binder - bp6 :: "pat6 \ atom set" -where - "bp6 (PVar' x) = {atom x}" -| "bp6 (PUnit') = {}" -| "bp6 (PPair' p1 p2) = bp6 p1 \ bp6 p2" - -thm exp6_pat6.fv -thm exp6_pat6.eq_iff -thm exp6_pat6.bn -thm exp6_pat6.perm -thm exp6_pat6.induct -thm exp6_pat6.distinct - - -(* THE REST ARE NOT SUPPOSED TO WORK YET *) - (* example 7 from Peter Sewell's bestiary *) (* dest_Const raised nominal_datatype exp7 = @@ -180,61 +84,6 @@ thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] *) -(* core haskell *) -atom_decl var -atom_decl tvar - -(* there are types, coercion types and regular types *) -(* list-data-structure -nominal_datatype tkind = - KStar -| KFun "tkind" "tkind" -and ckind = - CKEq "ty" "ty" -and ty = - TVar "tvar" -| TC "string" -| TApp "ty" "ty" -| TFun "string" "ty list" -| TAll tv::"tvar" "tkind" T::"ty" bind tv in T -| TEq "ty" "ty" "ty" -and co = - CC "string" -| CApp "co" "co" -| CFun "string" "co list" -| CAll tv::"tvar" "ckind" C::"co" bind tv in C -| CEq "co" "co" "co" -| CSym "co" -| CCir "co" "co" -| CLeft "co" -| CRight "co" -| CSim "co" -| CRightc "co" -| CLeftc "co" -| CCoe "co" "co" - -abbreviation - "atoms A \ atom ` A" - -nominal_datatype trm = - Var "var" -| C "string" -| LAM tv::"tvar" "kind" t::"trm" bind tv in t -| APP "trm" "ty" -| Lam v::"var" "ty" t::"trm" bind v in t -| App "trm" "trm" -| Let x::"var" "ty" "trm" t::"trm" bind x in t -| Case "trm" "assoc list" -| Cast "trm" "ty" --"ty is supposed to be a coercion type only" -and assoc = - A p::"pat" t::"trm" bind "bv p" in t -and pat = - K "string" "(tvar \ kind) list" "(var \ ty) list" -binder - bv :: "pat \ atom set" -where - "bv (K s ts vs) = (atoms (set (map fst ts))) \ (atoms (set (map fst vs)))" -*) (* example 8 from Terms.thy *)