diff -r c79d40b2128e -r 2f1b00d83925 Nominal/Test_compat.thy --- a/Nominal/Test_compat.thy Tue Mar 23 08:11:39 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,653 +0,0 @@ -theory Test_compat -imports "Parser" "../Attic/Prove" -begin - -text {* - example 1 - - single let binding -*} - -nominal_datatype lam = - VAR "name" -| APP "lam" "lam" -| LET bp::"bp" t::"lam" bind "bi bp" in t -and bp = - BP "name" "lam" -binder - bi::"bp \ atom set" -where - "bi (BP x t) = {atom x}" - -thm alpha_lam_raw_alpha_bp_raw.intros[no_vars] -thm fv_lam_raw_fv_bp_raw.simps[no_vars] - -abbreviation "VAR \ VAR_raw" -abbreviation "APP \ APP_raw" -abbreviation "LET \ LET_raw" -abbreviation "BP \ BP_raw" -abbreviation "bi \ bi_raw" - -(* non-recursive case *) -primrec - fv_lam :: "lam_raw \ atom set" -and fv_compat :: "bp_raw \ atom set" -where - "fv_lam (VAR name) = {atom name}" -| "fv_lam (APP lam1 lam2) = fv_lam lam1 \ fv_lam lam2" -| "fv_lam (LET bp lam) = (fv_compat bp) \ (fv_lam lam - bi bp)" -| "fv_compat (BP name lam) = fv_lam lam" - -primrec - fv_bp :: "bp_raw \ atom set" -where - "fv_bp (BP name lam) = {atom name} \ fv_lam lam" - - -inductive - alpha_lam :: "lam_raw \ lam_raw \ bool" and - alpha_bp :: "bp_raw \ bp_raw \ bool" and - compat_bp :: "bp_raw \ perm \ bp_raw \ bool" -where - "x = y \ alpha_lam (VAR x) (VAR y)" -| "alpha_lam l1 s1 \ alpha_lam l2 s2 \ alpha_lam (APP l1 l2) (APP s1 s2)" -| "\pi. (bi bp, lam) \gen alpha_lam fv_lam_raw pi (bi bp', lam') \ compat_bp bp pi bp' - \ alpha_lam (LET bp lam) (LET bp' lam')" -| "alpha_lam lam lam' \ name = name' \ alpha_bp (BP name lam) (BP name' lam')" -| "alpha_lam t t' \ pi \ x = x' \ compat_bp (BP x t) pi (BP x' t')" - -lemma test1: - shows "alpha_lam (LET (BP x (VAR x)) (VAR x)) - (LET (BP y (VAR x)) (VAR y))" -apply(rule alpha_lam_alpha_bp_compat_bp.intros) -apply(rule_tac x="(x \ y)" in exI) -apply(simp add: alpha_gen fresh_star_def) -apply(simp add: alpha_lam_alpha_bp_compat_bp.intros(1)) -apply(rule alpha_lam_alpha_bp_compat_bp.intros) -apply(simp add: alpha_lam_alpha_bp_compat_bp.intros(1)) -done - -lemma test2: - assumes asm: "distinct [x, y]" - shows "\ alpha_lam (LET (BP x (VAR x)) (VAR x)) - (LET (BP y (VAR y)) (VAR y))" -using asm -apply(clarify) -apply(erule alpha_lam.cases) -apply(simp_all) -apply(erule exE) -apply(clarify) -apply(simp add: alpha_gen fresh_star_def) -apply(erule alpha_lam.cases) -apply(simp_all) -apply(clarify) -apply(erule compat_bp.cases) -apply(simp_all) -apply(clarify) -apply(erule alpha_lam.cases) -apply(simp_all) -done - -(* recursive case where we have also bind "bi bp" in bp *) - -inductive - Alpha_lam :: "lam_raw \ lam_raw \ bool" and - Alpha_bp :: "bp_raw \ bp_raw \ bool" and - Compat_bp :: "bp_raw \ perm \ bp_raw \ bool" -where - "x = y \ Alpha_lam (VAR x) (VAR y)" -| "Alpha_lam l1 s1 \ Alpha_lam l2 s2 \ Alpha_lam (APP l1 l2) (APP s1 s2)" -| "\pi. (bi bp, lam) \gen Alpha_lam fv_lam_raw pi (bi bp', lam') \ Compat_bp bp pi bp' - \ Alpha_lam (LET bp lam) (LET bp' lam')" -| "Alpha_lam lam lam' \ name = name' \ Alpha_bp (BP name lam) (BP name' lam')" -| "Alpha_lam (pi \ t) t' \ pi \ x = x' \ Compat_bp (BP x t) pi (BP x' t')" - -lemma Test1: - assumes "distinct [x, y]" - shows "Alpha_lam (LET (BP x (VAR x)) (VAR x)) - (LET (BP y (VAR y)) (VAR y))" -apply(rule Alpha_lam_Alpha_bp_Compat_bp.intros) -apply(rule_tac x="(x \ y)" in exI) -apply(simp add: alpha_gen fresh_star_def) -apply(simp add: Alpha_lam_Alpha_bp_Compat_bp.intros(1)) -apply(rule Alpha_lam_Alpha_bp_Compat_bp.intros) -apply(simp add: Alpha_lam_Alpha_bp_Compat_bp.intros(1)) -done - -lemma Test2: - assumes asm: "distinct [x, y]" - shows "\ Alpha_lam (LET (BP x (VAR x)) (VAR x)) - (LET (BP y (VAR x)) (VAR y))" -using asm -apply(clarify) -apply(erule Alpha_lam.cases) -apply(simp_all) -apply(erule exE) -apply(clarify) -apply(simp add: alpha_gen fresh_star_def) -apply(erule Alpha_lam.cases) -apply(simp_all) -apply(clarify) -apply(erule Compat_bp.cases) -apply(simp_all) -apply(clarify) -apply(erule Alpha_lam.cases) -apply(simp_all) -done - - -text {* example 2 *} - -nominal_datatype trm' = - Var "name" -| App "trm'" "trm'" -| Lam x::"name" t::"trm'" bind x in t -| Let p::"pat'" "trm'" t::"trm'" bind "f p" in t -and pat' = - PN -| PS "name" -| PD "name" "name" -binder - f::"pat' \ atom set" -where - "f PN = {}" -| "f (PS x) = {atom x}" -| "f (PD x y) = {atom x} \ {atom y}" - -thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars] - -abbreviation "Var \ Var_raw" -abbreviation "App \ App_raw" -abbreviation "Lam \ Lam_raw" -abbreviation "Lett \ Let_raw" -abbreviation "PN \ PN_raw" -abbreviation "PS \ PS_raw" -abbreviation "PD \ PD_raw" -abbreviation "f \ f_raw" - -(* not_yet_done *) -inductive - alpha_trm' :: "trm'_raw \ trm'_raw \ bool" and - alpha_pat' :: "pat'_raw \ pat'_raw \ bool" and - compat_pat' :: "pat'_raw \ perm \ pat'_raw \ bool" -where - "name = name' \ alpha_trm' (Var name) (Var name')" -| "alpha_trm' t2 t2' \ alpha_trm' t1 t1' \ alpha_trm' (App t1 t2) (App t1' t2')" -| "\pi. ({atom x}, t) \gen alpha_trm' fv_trm'_raw pi ({atom x'}, t') \ alpha_trm' (Lam x t) (Lam x' t')" -| "\pi. (f p, t) \gen alpha_trm' fv_trm'_raw pi (f p', t') \ alpha_trm' s s' \ - compat_pat' p pi p' \ alpha_trm' (Lett p s t) (Lett p' s' t')" -| "alpha_pat' PN PN" -| "name = name' \ alpha_pat' (PS name) (PS name')" -| "name2 = name2' \ name1 = name1' \ alpha_pat' (PD name1 name2) (PD name1' name2')" -| "compat_pat' PN pi PN" -| "pi \ x = x' \ compat_pat' (PS x) pi (PS x')" -| "pi \ p1 = p1' \ pi \ p2 = p2' \ compat_pat' (PD p1 p2) pi (PD p1' p2')" - -lemma - assumes a: "distinct [x, y, z, u]" - shows "alpha_trm' (Lett (PD x u) t (App (Var x) (Var y))) - (Lett (PD z u) t (App (Var z) (Var y)))" -using a -apply - -apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros) -apply(auto simp add: alpha_gen) -apply(rule_tac x="(x \ z)" in exI) -apply(auto simp add: fresh_star_def) -defer -apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros) -apply(simp add: alpha_trm'_alpha_pat'_compat_pat'.intros) -defer -apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros) -apply(simp) -(* they can be proved *) -oops - -lemma - assumes a: "distinct [x, y, z, u]" - shows "\ alpha_trm' (Lett (PD x u) t (App (Var x) (Var y))) - (Lett (PD z z) t (App (Var z) (Var y)))" -using a -apply(clarify) -apply(erule alpha_trm'.cases) -apply(simp_all) -apply(auto simp add: alpha_gen) -apply(erule alpha_trm'.cases) -apply(simp_all) -apply(clarify) -apply(erule compat_pat'.cases) -apply(simp_all) -apply(clarify) -apply(erule alpha_trm'.cases) -apply(simp_all) -done - -nominal_datatype trm0 = - Var0 "name" -| App0 "trm0" "trm0" -| Lam0 x::"name" t::"trm0" bind x in t -| Let0 p::"pat0" "trm0" t::"trm0" bind "f0 p" in t -and pat0 = - PN0 -| PS0 "name" -| PD0 "pat0" "pat0" -binder - f0::"pat0 \ atom set" -where - "f0 PN0 = {}" -| "f0 (PS0 x) = {atom x}" -| "f0 (PD0 p1 p2) = (f0 p1) \ (f0 p2)" - -thm f0_raw.simps -(*thm trm0_pat0_induct -thm trm0_pat0_perm -thm trm0_pat0_fv -thm trm0_pat0_bn*) - -text {* example type schemes *} - -(* does not work yet -nominal_datatype t = - Var "name" -| Fun "t" "t" - -nominal_datatype tyS = - All xs::"name list" ty::"t_raw" bind xs in ty -*) - - -nominal_datatype t = - Var "name" -| Fun "t" "t" -and tyS = - All xs::"name set" ty::"t" bind xs in ty - -(* example 1 from Terms.thy *) - -nominal_datatype trm1 = - Vr1 "name" -| Ap1 "trm1" "trm1" -| Lm1 x::"name" t::"trm1" bind x in t -| Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t -and bp1 = - BUnit1 -| BV1 "name" -| BP1 "bp1" "bp1" -binder - bv1 -where - "bv1 (BUnit1) = {}" -| "bv1 (BV1 x) = {atom x}" -| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \ (bv1 bp2)" - -thm bv1_raw.simps - -(* example 2 from Terms.thy *) - -nominal_datatype trm2 = - Vr2 "name" -| Ap2 "trm2" "trm2" -| Lm2 x::"name" t::"trm2" bind x in t -| Lt2 r::"assign" t::"trm2" bind "bv2 r" in t -and assign = - As "name" "trm2" -binder - bv2 -where - "bv2 (As x t) = {atom x}" - -(* compat should be -compat (As x t) pi (As x' t') == pi o x = x' & alpha t t' -*) - - -thm fv_trm2_raw_fv_assign_raw.simps[no_vars] -thm alpha_trm2_raw_alpha_assign_raw.intros[no_vars] - - - -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)" - - -(* compat should be -compat (ANil) pi (PNil) \ TRue -compat (ACons x t ts) pi (ACons x' t' ts') \ pi o x = x' \ alpha t t' \ compat ts pi ts' -*) - -(* example 4 from Terms.thy *) - -(* fv_eqvt does not work, we need to repaire defined permute functions - defined fv and defined alpha... *) -nominal_datatype trm4 = - Vr4 "name" -| Ap4 "trm4" "trm4 list" -| Lm4 x::"name" t::"trm4" bind x in t - -thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] -thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] - -(* 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)" - -(* example 6 from Terms.thy *) - -(* BV is not respectful, needs to fail*) -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 *) - -(* BV is not respectful, needs to fail*) -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 8 from Terms.thy *) - -nominal_datatype foo8 = - Foo0 "name" -| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo" -and bar8 = - Bar0 "name" -| Bar1 "name" s::"name" b::"bar8" bind s in b -binder - bv8 -where - "bv8 (Bar0 x) = {}" -| "bv8 (Bar1 v x b) = {atom v}" - -(* example 9 from Terms.thy *) - -(* BV is not respectful, needs to fail*) -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}" - -(* example from my PHD *) - -atom_decl coname - -nominal_datatype phd = - Ax "name" "coname" -| Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 -| AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 -| AndL1 n::"name" t::"phd" "name" bind n in t -| AndL2 n::"name" t::"phd" "name" bind n in t -| ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 -| ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t - -thm alpha_phd_raw.intros[no_vars] -thm fv_phd_raw.simps[no_vars] - - -(* example form Leroy 96 about modules; OTT *) - -nominal_datatype mexp = - Acc "path" -| Stru "body" -| Funct x::"name" "sexp" m::"mexp" bind x in m -| FApp "mexp" "path" -| Ascr "mexp" "sexp" -and body = - Empty -| Seq c::defn d::"body" bind "cbinders c" in d -and defn = - Type "name" "tyty" -| Dty "name" -| DStru "name" "mexp" -| Val "name" "trmtrm" -and sexp = - Sig sbody -| SFunc "name" "sexp" "sexp" -and sbody = - SEmpty -| SSeq C::spec D::sbody bind "Cbinders C" in D -and spec = - Type1 "name" -| Type2 "name" "tyty" -| SStru "name" "sexp" -| SVal "name" "tyty" -and tyty = - Tyref1 "name" -| Tyref2 "path" "tyty" -| Fun "tyty" "tyty" -and path = - Sref1 "name" -| Sref2 "path" "name" -and trmtrm = - Tref1 "name" -| Tref2 "path" "name" -| Lam' v::"name" "tyty" M::"trmtrm" bind v in M -| App' "trmtrm" "trmtrm" -| Let' "body" "trmtrm" -binder - cbinders :: "defn \ atom set" -and Cbinders :: "spec \ atom set" -where - "cbinders (Type t T) = {atom t}" -| "cbinders (Dty t) = {atom t}" -| "cbinders (DStru x s) = {atom x}" -| "cbinders (Val v M) = {atom v}" -| "Cbinders (Type1 t) = {atom t}" -| "Cbinders (Type2 t T) = {atom t}" -| "Cbinders (SStru x S) = {atom x}" -| "Cbinders (SVal v T) = {atom v}" - -(* core haskell *) -print_theorems - -atom_decl var -atom_decl tvar - - -(* there are types, coercion types and regular types *) -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" - - -typedecl ty --"hack since ty is not yet defined" - -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)))" - -(* -compat (K s ts vs) pi (K s' ts' vs') == - s = s' & - -*) - - -(*thm bv_raw.simps*) - -(* 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::"pat" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1 -and pat = - PVar "name" -| PUnit -| PPair "pat" "pat" -binder - bp :: "pat \ atom set" -where - "bp (PVar x) = {atom x}" -| "bp (PUnit) = {}" -| "bp (PPair p1 p2) = bp p1 \ bp p2" -thm alpha_exp_raw_alpha_pat_raw.intros - -(* 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 alpha_exp6_raw_alpha_pat6_raw.intros - -(* example 7 from Peter Sewell's bestiary *) -nominal_datatype exp7 = - EVar name -| EUnit -| EPair exp7 exp7 -| ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l -and lrb = - Assign name exp7 -and lrbs = - Single lrb -| More lrb lrbs -binder - b7 :: "lrb \ atom set" and - b7s :: "lrbs \ atom set" -where - "b7 (Assign x e) = {atom x}" -| "b7s (Single a) = b7 a" -| "b7s (More a as) = (b7 a) \ (b7s as)" -thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros - -(* example 8 from Peter Sewell's bestiary *) -nominal_datatype exp8 = - EVar name -| EUnit -| EPair exp8 exp8 -| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l -and fnclause = - K x::name p::pat8 e::exp8 bind "b_pat p" in e -and fnclauses = - S fnclause -| ORs fnclause fnclauses -and lrb8 = - Clause fnclauses -and lrbs8 = - Single lrb8 -| More lrb8 lrbs8 -and pat8 = - PVar name -| PUnit -| PPair pat8 pat8 -binder - b_lrbs8 :: "lrbs8 \ atom set" and - b_pat :: "pat8 \ atom set" and - b_fnclauses :: "fnclauses \ atom set" and - b_fnclause :: "fnclause \ atom set" and - b_lrb8 :: "lrb8 \ atom set" -where - "b_lrbs8 (Single l) = b_lrb8 l" -| "b_lrbs8 (More l ls) = b_lrb8 l \ b_lrbs8 ls" -| "b_pat (PVar x) = {atom x}" -| "b_pat (PUnit) = {}" -| "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" -| "b_fnclauses (S fc) = (b_fnclause fc)" -| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \ (b_fnclauses fcs)" -| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)" -| "b_fnclause (K x pat exp8) = {atom x}" -thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros - - - - -(* example 9 from Peter Sewell's bestiary *) -(* run out of steam at the moment *) - -end - - -