nominal2: comparison Nominal/Test.thy

equal deleted inserted replaced

-:4de35639fef0
+:d18defacda25
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 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) \<union> fv_bi bp_raw" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
 apply(simp only: permute_ABS)
 apply(simp only: lam_bp_inject)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
 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]]
 ML {* val _ = recursive := true *}
 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
+| 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 \<Rightarrow> atom set"
+bp'' :: "pat3 \<Rightarrow> atom set"
 where
-"bp' (PVar x) = {atom x}"
+"bp'' (PVar x) = {atom x}"
-| "bp' (PUnit) = {}"
+| "bp'' (PUnit) = {}"
-| "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2"
+| "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
 thm exp_pat3_fv
 thm exp_pat3_inject
 thm exp_pat3_bn
 thm exp_pat3_perm
 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 =
-EVar name
+EVar' name
-| EUnit
+| EUnit'
-| EPair exp7 exp7
+| EPair' exp7 exp7
-| ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l
+| 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
+Single' lrb
-| More lrb lrbs
+| More' lrb lrbs
 binder
 b7 :: "lrb \<Rightarrow> atom set" and
 b7s :: "lrbs \<Rightarrow> atom set"
 where
 "b7 (Assign x e) = {atom x}"
 | "b7s (Single a) = b7 a"
 | "b7s (More a as) = (b7 a) \<union> (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
+EVar' name
-| EUnit
+| EUnit'
-| EPair exp8 exp8
+| EPair' exp8 exp8
-| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l
+| 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
+S' fnclause
-| ORs fnclause fnclauses
+| ORs' fnclause fnclauses
 and lrb8 =
-Clause fnclauses
+Clause' fnclauses
 and lrbs8 =
-Single lrb8
+Single' lrb8
-| More lrb8 lrbs8
+| More' lrb8 lrbs8
 and pat8 =
-PVar name
+PVar'' name
-| PUnit
+| PUnit''
-| PPair pat8 pat8
+| PPair'' pat8 pat8
 binder
 b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
 b_pat :: "pat8 \<Rightarrow> atom set" and
 b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
 b_fnclause :: "fnclause \<Rightarrow> atom set" and
 b_lrb8 :: "lrb8 \<Rightarrow> atom set"
 where
-"b_lrbs8 (Single l) = b_lrb8 l"
+"b_lrbs8 (Single' l) = b_lrb8 l"
-| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
+| "b_lrbs8 (More' l ls) = b_lrb8 l \<union> b_lrbs8 ls"
-| "b_pat (PVar x) = {atom x}"
+| "b_pat (PVar'' x) = {atom x}"
-| "b_pat (PUnit) = {}"
+| "b_pat (PUnit'') = {}"
-| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
+| "b_pat (PPair'' p1 p2) = b_pat p1 \<union> b_pat p2"
-| "b_fnclauses (S fc) = (b_fnclause fc)"
+| "b_fnclauses (S' fc) = (b_fnclause fc)"
-| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
+| "b_fnclauses (ORs' fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
-| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
+| "b_lrb8 (Clause' fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp8) = {atom x}"
+| "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"
 | 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]
+*)
 (* 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"
 | CSim "co"
 | CRightc "co"
 | 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 \<equiv> atom ` A"
 nominal_datatype trm =
 Var "var"
 K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
 binder
 bv :: "pat \<Rightarrow> atom set"
 where
 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (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 =
 WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
 thm fv_weird_raw.simps[no_vars]
 (* 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} \<union> bv6 t"
 | "bv6 (Lt6 l r) = bv6 l \<union> 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 \<union> 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"
 and bar8 =
 Bar0 "name"
 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}"
+*)
 (* Type schemes with separate datatypes *)
-nominal_datatype t =
+nominal_datatype T =
-Var "name"
+TVar "name"
-| Fun "t" "t"
+| TFun "T" "T"
-nominal_datatype tyS =
+(* PROBLEM:
-All xs::"name list" ty::"t_raw" bind xs in ty
+*** 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 *)
 end

changeset 1466	d18defacda25
parent 1465	4de35639fef0
child 1471	7fe643ad19e4