nominal2: comparison Nominal/Test.thy

equal deleted inserted replaced

-:cad5f3851569
+:3727e234fe6b
 imports "Parser" "../Attic/Prove"
 begin
 text {* weirdo example from Peter Sewell's bestiary *}
-(*nominal_datatype weird =
+nominal_datatype weird =
 WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
 bind x in p1, bind x in p2, bind y in p2, bind y in p3
 | WV "name"
 | WP "weird" "weird"
 thm eqvts
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding weird_inj}, []), (build_alpha_inj @{thms alpha_weird_raw.intros} @{thms weird_raw.distinct weird_raw.inject} @{thms alpha_weird_raw.cases} ctxt)) ctxt)) *}
 thm weird_inj
-local_setup {*
+(*local_setup {*
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha_eqvt}, []),
 build_alpha_eqvts [@{term alpha_weird_raw}] [@{term "permute :: perm \<Rightarrow> weird_raw \<Rightarrow> weird_raw"}] @{thms permute_weird_raw.simps weird_inj} @{thm alpha_weird_raw.induct} ctxt) ctxt)) *}
 (*prove {* (snd o snd) (build_alpha_refl_gl [@{term alpha_weird_raw}] ("x","y","z")) *}
 term Test.BP_raw
 thm bi_raw.simps
 thm permute_lam_raw_permute_bp_raw.simps
 thm alpha_lam_raw_alpha_bp_raw.intros[no_vars]
 thm fv_lam_raw_fv_bp_raw.simps[no_vars]
-thm lam_bp_induct
+(*thm lam_bp_induct
 thm lam_bp_perm
 thm lam_bp_fv
 thm lam_bp_bn
+thm lam_bp_inject*)
 text {* example 2 *}
 nominal_datatype trm' =
 Var "name"
 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]
 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
 thm f_raw.simps
-thm trm'_pat'_induct
+(*thm trm'_pat'_induct
 thm trm'_pat'_perm
 thm trm'_pat'_fv
 thm trm'_pat'_bn
+thm trm'_pat'_inject*)
 nominal_datatype trm0 =
 Var0 "name"
 | App0 "trm0" "trm0"
 | Lam0 x::"name" t::"trm0"          bind x in t
 "f0 PN0 = {}"
 | "f0 (PS0 x) = {atom x}"
 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
 thm f0_raw.simps
-thm trm0_pat0_induct
+(*thm trm0_pat0_induct
 thm trm0_pat0_perm
 thm trm0_pat0_fv
-thm trm0_pat0_bn
+thm trm0_pat0_bn*)
 text {* example type schemes *}
 (* does not work yet
 nominal_datatype t =
 nominal_datatype tyS =
 All xs::"name list" ty::"t_raw" bind xs in ty
 *)
-(* alpha_eqvt fails...
 nominal_datatype t =
 Var "name"
 | Fun "t" "t"
 and  tyS =
-All xs::"name set" ty::"t" bind xs in ty *)
+All xs::"name set" ty::"t" bind xs in ty
 (* example 1 from Terms.thy *)
 nominal_datatype trm1 =
 Vr1 "name"
 (* 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 =
+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]*)
+thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 (* example 5 from Terms.thy *)
 nominal_datatype trm5 =
 Vr5 "name"
 "bv5 Lnil = {}"
 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
 (* example 6 from Terms.thy *)
-(* BV is not respectful, needs to fail
+(* 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" *)
+| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
 (* example 7 from Terms.thy *)
-(* BV is not respectful, needs to fail
+(* 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" *)
+| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
 (* example 8 from Terms.thy *)
 nominal_datatype foo8 =
 Foo0 "name"
 "bv8 (Bar0 x) = {}"
 | "bv8 (Bar1 v x b) = {atom v}"
 (* example 9 from Terms.thy *)
-(* BV is not respectful, needs to fail
+(* 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}" *)
+| "bv9 (Lam9 x b) = {atom x}"
 (* example from my PHD *)
 atom_decl coname
-(*nominal_datatype phd =
+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"
 | "bp (PUnit) = {}"
 | "bp (PPair p1 p2) = bp p1 \<union> bp p2"
 thm quot_respect
 (* example 6 from Peter Sewell's bestiary *)
-(*nominal_datatype exp6 =
+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
 binder
 bp6 :: "pat6 \<Rightarrow> atom set"
 where
 "bp6 (PVar' x) = {atom x}"
 | "bp6 (PUnit') = {}"
-| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"*)
+| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
 (* example 7 from Peter Sewell's bestiary *)
-(*nominal_datatype exp7 =
+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 =
 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)"*)
+| "b7s (More a as) = (b7 a) \<union> (b7s as)"
 (* example 8 from Peter Sewell's bestiary *)
-(*nominal_datatype exp8 =
+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 =
 | "b_pat (PUnit) = {}"
 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
 | "b_fnclauses (S fc) = (b_fnclause fc)"
 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (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}"
 (* example 9 from Peter Sewell's bestiary *)

changeset 1353	3727e234fe6b
parent 1352	cad5f3851569
parent 1341	c25f797c7e6e
child 1355	7b0c6d07a24e