--- a/Nominal/LFex.thy Tue Mar 23 08:22:48 2010 +0100
+++ b/Nominal/LFex.thy Tue Mar 23 08:33:48 2010 +0100
@@ -5,8 +5,6 @@
atom_decl name
atom_decl ident
-ML {* val _ = cheat_equivp := false *}
-
nominal_datatype kind =
Type
| KPi "ty" n::"name" k::"kind" bind n in k
--- a/Nominal/Parser.thy Tue Mar 23 08:22:48 2010 +0100
+++ b/Nominal/Parser.thy Tue Mar 23 08:33:48 2010 +0100
@@ -265,7 +265,8 @@
end
*}
-ML {* val cheat_equivp = Unsynchronized.ref true *}
+(* This one is not needed for the proper examples *)
+ML {* val cheat_equivp = Unsynchronized.ref false *}
(* These 4 are not needed any more *)
ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
--- a/Nominal/Test.thy Tue Mar 23 08:22:48 2010 +0100
+++ b/Nominal/Test.thy Tue Mar 23 08:33:48 2010 +0100
@@ -108,30 +108,8 @@
thm trm0_pat0.distinct
thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]
-text {* example type schemes *}
-
-nominal_datatype t =
- VarTS "name"
-| FunTS "t" "t"
-and tyS =
- All xs::"name fset" ty::"t" bind xs in ty
-
-thm t_tyS.fv
-thm t_tyS.eq_iff
-thm t_tyS.bn
-thm t_tyS.perm
-thm t_tyS.induct
-thm t_tyS.distinct
-thm t_tyS.fv[simplified t_tyS.supp]
-
-ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
-ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
-
-
-
(* example 1 from Terms.thy *)
-
nominal_datatype trm1 =
Vr1 "name"
| Ap1 "trm1" "trm1"
@@ -266,28 +244,6 @@
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
-
-(* 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 phd.fv
-thm phd.eq_iff
-thm phd.bn
-thm phd.perm
-thm phd.induct
-thm phd.distinct
-thm phd.fv[simplified phd.supp]
-
(* example 3 from Peter Sewell's bestiary *)
nominal_datatype exp =
@@ -471,18 +427,6 @@
"bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
*)
-text {* weirdo example from Peter Sewell's bestiary *}
-
-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 permute_weird_raw.simps[no_vars]
-thm alpha_weird_raw.intros[no_vars]
-thm fv_weird_raw.simps[no_vars]
-
(* example 8 from Terms.thy *)
(* Binding in a term under a bn, needs to fail *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/TestMorePerm.thy Tue Mar 23 08:33:48 2010 +0100
@@ -0,0 +1,49 @@
+theory TestMorePerm
+imports "Parser"
+begin
+
+(* Since there are more permutations, we do not know how to prove equivalence
+ (it is probably not true with the way alpha is defined now) so *)
+ML {* val _ = cheat_equivp := true *}
+
+
+atom_decl name
+
+(* 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 phd.fv
+thm phd.eq_iff
+thm phd.bn
+thm phd.perm
+thm phd.induct
+thm phd.distinct
+thm phd.fv[simplified phd.supp]
+
+text {* weirdo example from Peter Sewell's bestiary *}
+
+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 permute_weird_raw.simps[no_vars]
+thm alpha_weird_raw.intros[no_vars]
+thm fv_weird_raw.simps[no_vars]
+
+
+end
+
+
+
--- a/Nominal/TySch.thy Tue Mar 23 08:22:48 2010 +0100
+++ b/Nominal/TySch.thy Tue Mar 23 08:33:48 2010 +0100
@@ -4,8 +4,6 @@
atom_decl name
-ML {* val _ = cheat_equivp := false *}
-
nominal_datatype t =
Var "name"
| Fun "t" "t"