Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Move Ex1 and Ex2 out of Test
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 23 Mar 2010 08:42:02 +0100
changeset 1596 c69d9fb16785
parent 1595 aeed597d2043
child 1597 af34dd3418fe
Move Ex1 and Ex2 out of Test
Nominal/Ex1.thy file | annotate | diff | comparison | revisions
Nominal/Ex1rec.thy file | annotate | diff | comparison | revisions
Nominal/Ex2.thy file | annotate | diff | comparison | revisions
Nominal/Test.thy file | annotate | diff | comparison | revisions
Nominal/TySch.thy file | annotate | diff | comparison | revisions 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex1.thy	Tue Mar 23 08:42:02 2010 +0100
@@ -0,0 +1,36 @@
+theory Ex1
+imports "Parser"
+begin
+
+text {* example 1, equivalent to example 2 from Terms *}
+
+atom_decl name
+
+ML {* val _ = recursive := false *}
+nominal_datatype lam =
+  VAR "name"
+| APP "lam" "lam"
+| LAM x::"name" t::"lam" bind x in t
+| LET bp::"bp" t::"lam"   bind "bi bp" in t
+and bp =
+  BP "name" "lam"
+binder
+  bi::"bp \<Rightarrow> atom set"
+where
+  "bi (BP x t) = {atom x}"
+
+thm lam_bp.fv
+thm lam_bp.supp
+thm lam_bp.eq_iff
+thm lam_bp.bn
+thm lam_bp.perm
+thm lam_bp.induct
+thm lam_bp.inducts
+thm lam_bp.distinct
+ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
+thm lam_bp.fv[simplified lam_bp.supp]
+
+end
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex1rec.thy	Tue Mar 23 08:42:02 2010 +0100
@@ -0,0 +1,33 @@
+theory Ex1rec
+imports "Parser" "../Attic/Prove"
+begin
+
+atom_decl name
+
+ML {* val _ = recursive := true *}
+nominal_datatype lam' =
+  VAR' "name"
+| APP' "lam'" "lam'"
+| LAM' x::"name" t::"lam'"  bind x in t
+| LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t
+and bp' =
+  BP' "name" "lam'"
+binder
+  bi'::"bp' \<Rightarrow> atom set"
+where
+  "bi' (BP' x t) = {atom x}"
+
+thm lam'_bp'.fv
+thm lam'_bp'.eq_iff[no_vars]
+thm lam'_bp'.bn
+thm lam'_bp'.perm
+thm lam'_bp'.induct
+thm lam'_bp'.inducts
+thm lam'_bp'.distinct
+ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
+thm lam'_bp'.fv[simplified lam'_bp'.supp]
+
+end
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex2.thy	Tue Mar 23 08:42:02 2010 +0100
@@ -0,0 +1,37 @@
+theory Ex2
+imports "Parser"
+begin
+
+text {* example 2 *}
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+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' \<Rightarrow> atom set"
+where
+  "f PN = {}"
+| "f (PD x y) = {atom x, atom y}"
+| "f (PS x) = {atom x}"
+
+thm trm'_pat'.fv
+thm trm'_pat'.eq_iff
+thm trm'_pat'.bn
+thm trm'_pat'.perm
+thm trm'_pat'.induct
+thm trm'_pat'.distinct
+thm trm'_pat'.fv[simplified trm'_pat'.supp]
+
+end
+
+
+
--- a/Nominal/Test.thy	Tue Mar 23 08:33:48 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 08:42:02 2010 +0100
@@ -1,88 +1,10 @@
 theory Test
-imports "Parser" "../Attic/Prove"
+imports "Parser"
 begin
 
 atom_decl name
 
-ML {* val _ = recursive := false *}
-
-text {* example 1, equivalent to example 2 from Terms *}
-
-nominal_datatype lam =
-  VAR "name"
-| APP "lam" "lam"
-| LAM x::"name" t::"lam" bind x in t
-| LET bp::"bp" t::"lam"   bind "bi bp" in t
-and bp =
-  BP "name" "lam"
-binder
-  bi::"bp \<Rightarrow> atom set"
-where
-  "bi (BP x t) = {atom x}"
-
-thm lam_bp.fv
-thm lam_bp.supp
-thm lam_bp.eq_iff
-thm lam_bp.bn
-thm lam_bp.perm
-thm lam_bp.induct
-thm lam_bp.inducts
-thm lam_bp.distinct
-ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
-thm lam_bp.fv[simplified lam_bp.supp]
-
-ML {* val _ = recursive := true *}
-
-nominal_datatype lam' =
-  VAR' "name"
-| APP' "lam'" "lam'"
-| LAM' x::"name" t::"lam'"  bind x in t
-| LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t
-and bp' =
-  BP' "name" "lam'"
-binder
-  bi'::"bp' \<Rightarrow> atom set"
-where
-  "bi' (BP' x t) = {atom x}"
-
-thm lam'_bp'.fv
-thm lam'_bp'.eq_iff[no_vars]
-thm lam'_bp'.bn
-thm lam'_bp'.perm
-thm lam'_bp'.induct
-thm lam'_bp'.inducts
-thm lam'_bp'.distinct
-ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
-
-thm lam'_bp'.fv[simplified lam'_bp'.supp]
-
-
-text {* example 2 *}
-
 ML {* val _ = recursive := false  *}
-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' \<Rightarrow> atom set"
-where
-  "f PN = {}"
-| "f (PD x y) = {atom x, atom y}"
-| "f (PS x) = {atom x}"
-
-thm trm'_pat'.fv
-thm trm'_pat'.eq_iff
-thm trm'_pat'.bn
-thm trm'_pat'.perm
-thm trm'_pat'.induct
-thm trm'_pat'.distinct
-thm trm'_pat'.fv[simplified trm'_pat'.supp]
 
 nominal_datatype trm0 =
   Var0 "name"
@@ -444,19 +366,6 @@
 | "bv8 (Bar1 v x b) = {atom v}"
 *)
 
-(* Type schemes with separate datatypes *)
-nominal_datatype T =
-  TVar "name"
-| TFun "T" "T"
-
-(* 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 *)
 
--- a/Nominal/TySch.thy	Tue Mar 23 08:33:48 2010 +0100
+++ b/Nominal/TySch.thy	Tue Mar 23 08:42:02 2010 +0100
@@ -147,4 +147,19 @@
   apply auto
   done
 
+(* PROBLEM:
+Type schemes with separate datatypes
+
+nominal_datatype T =
+  TVar "name"
+| TFun "T" "T"
+nominal_datatype TyS =
+  TAll xs::"name list" ty::"T" 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".
+*)
+
+
 end
nominal2