diff -r 4de35639fef0 -r d18defacda25 Nominal/Test.thy --- a/Nominal/Test.thy Wed Mar 17 06:49:33 2010 +0100 +++ b/Nominal/Test.thy Wed Mar 17 08:07:25 2010 +0100 @@ -74,19 +74,6 @@ apply(simp only: eqvts) apply(simp only: supp_Abs) (* LET case *) -defer -(* BP case *) -apply(simp only: supp_def) -apply(simp only: lam_bp_perm) -apply(simp only: lam_bp_inject) -apply(simp only: de_Morgan_conj) -apply(simp only: Collect_disj_eq) -apply(simp only: infinite_Un) -apply(simp only: Collect_disj_eq) -apply(simp only: supp_def[symmetric]) -apply(simp only: supp_at_base) -apply(simp) -(* LET case *) apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \ fv_bi bp_raw" in subst) apply(simp (no_asm) only: supp_def) apply(simp only: lam_bp_perm) @@ -105,6 +92,17 @@ apply(blast) apply(simp add: supp_Abs) apply(blast) +(* BP case *) +apply(simp only: supp_def) +apply(simp only: lam_bp_perm) +apply(simp only: lam_bp_inject) +apply(simp only: de_Morgan_conj) +apply(simp only: Collect_disj_eq) +apply(simp only: infinite_Un) +apply(simp only: Collect_disj_eq) +apply(simp only: supp_def[symmetric]) +apply(simp only: supp_at_base) +apply(simp) done thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] @@ -498,17 +496,17 @@ 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 +| 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" + bp'' :: "pat3 \ atom set" where - "bp' (PVar x) = {atom x}" -| "bp' (PUnit) = {}" -| "bp' (PPair p1 p2) = bp' p1 \ bp' p2" + "bp'' (PVar x) = {atom x}" +| "bp'' (PUnit) = {}" +| "bp'' (PPair p1 p2) = bp'' p1 \ bp'' p2" thm exp_pat3_fv thm exp_pat3_inject @@ -543,16 +541,17 @@ (* THE REST ARE NOT SUPPOSED TO WORK YET *) (* example 7 from Peter Sewell's bestiary *) +(* dest_Const raised nominal_datatype exp7 = - EVar name -| EUnit -| EPair exp7 exp7 -| ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l + 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 + Assign' name exp7 and lrbs = - Single lrb -| More lrb lrbs + Single' lrb +| More' lrb lrbs binder b7 :: "lrb \ atom set" and b7s :: "lrbs \ atom set" @@ -561,27 +560,31 @@ | "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 *) +(* +*** fv_bn: recursive argument, but wrong datatype. +*** At command "nominal_datatype". 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 + 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 + K' x::name p::pat8 e::exp8 bind "b_pat p" in e and fnclauses = - S fnclause -| ORs fnclause fnclauses + S' fnclause +| ORs' fnclause fnclauses and lrb8 = - Clause fnclauses + Clause' fnclauses and lrbs8 = - Single lrb8 -| More lrb8 lrbs8 + Single' lrb8 +| More' lrb8 lrbs8 and pat8 = - PVar name -| PUnit -| PPair pat8 pat8 + PVar'' name +| PUnit'' +| PPair'' pat8 pat8 binder b_lrbs8 :: "lrbs8 \ atom set" and b_pat :: "pat8 \ atom set" and @@ -589,20 +592,21 @@ 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}" + "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 4 from Terms.thy *) (* fv_eqvt does not work, we need to repaire defined permute functions defined fv and defined alpha... *) +(* lists-datastructure does not work yet nominal_datatype trm4 = Vr4 "name" | Ap4 "trm4" "trm4 list" @@ -610,12 +614,13 @@ 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" @@ -643,13 +648,6 @@ | CLeftc "co" | CCoe "co" "co" - -typedecl ty --"hack since ty is not yet defined" -typedecl kind - -instance ty and kind:: pt -sorry - abbreviation "atoms A \ atom ` A" @@ -671,15 +669,8 @@ 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' & - *) - - text {* weirdo example from Peter Sewell's bestiary *} nominal_datatype weird = @@ -695,6 +686,7 @@ (* 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 @@ -705,9 +697,11 @@ "bv6 (Vr6 n) = {}" | "bv6 (Lm6 n t) = {atom n} \ bv6 t" | "bv6 (Lt6 l r) = bv6 l \ bv6 r" -(* example 7 from Terms.thy *) +*) +(* 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 @@ -718,10 +712,12 @@ "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 *) (* Binding in a term under a bn, needs to fail *) +(* nominal_datatype foo8 = Foo0 "name" | Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo" @@ -733,10 +729,11 @@ 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 @@ -747,18 +744,20 @@ where "bv9 (Var9 x) = {}" | "bv9 (Lam9 x b) = {atom x}" - +*) (* Type schemes with separate datatypes *) -nominal_datatype t = - Var "name" -| Fun "t" "t" +nominal_datatype T = + TVar "name" +| TFun "T" "T" -nominal_datatype tyS = - All xs::"name list" ty::"t_raw" bind xs in ty - - - +(* PROBLEM: +*** exception Datatype raised +*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML") +*** At command "nominal_datatype". +nominal_datatype TyS = + TAll xs::"name list" ty::"T" bind xs in ty +*) (* example 9 from Peter Sewell's bestiary *) (* run out of steam at the moment *)