--- a/Nominal/Ex/ExPS8.thy	Mon Sep 20 21:52:45 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-theory ExPS8
-imports "../Nominal2"
-begin
-
-(* example 8 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-declare [[STEPS = 31]]
-
-nominal_datatype fun_pats: exp =
-  EVar name
-| EUnit 
-| EPair exp exp
-| ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e
-and fnclause =
-  K x::name p::pat f::exp bind (set) "b_pat p" in f
-and fnclauses =
-  S fnclause
-| ORs fnclause fnclauses
-and lrb =
-  Clause fnclauses
-and lrbs =
-  Single lrb
-| More lrb lrbs
-and pat =
-  PVar name
-| PUnit
-| PPair pat pat
-binder
-  b_lrbs :: "lrbs \<Rightarrow> atom set" and
-  b_pat :: "pat \<Rightarrow> atom set" and
-  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
-  b_fnclause :: "fnclause \<Rightarrow> atom set" and
-  b_lrb :: "lrb \<Rightarrow> atom set"
-where
-  "b_lrbs (Single l) = b_lrb l"
-| "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"
-| "b_pat (PVar x) = {atom x}"
-| "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_lrb (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp) = {atom x}"
-
-thm fun_pats.distinct
-thm fun_pats.induct
-thm fun_pats.inducts
-thm fun_pats.exhaust
-thm fun_pats.fv_defs
-thm fun_pats.bn_defs
-thm fun_pats.perm_simps
-thm fun_pats.eq_iff
-thm fun_pats.fv_bn_eqvt
-thm fun_pats.size_eqvt
-thm fun_pats.supports
-thm fun_pats.fsupp
-thm fun_pats.supp
-
-lemma
-  "(fv_exp x = supp x) \<and>
-   (fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and>
-   (fv_fnclauses xb = supp xb \<and> fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb) \<and>
-   (fv_lrb xc = supp xc \<and> fv_b_fnclause xc = supp_rel alpha_b_fnclause xc) \<and>
-   (fv_lrbs xd = supp xd \<and> fv_b_lrbs xd = supp_rel alpha_b_lrbs xd) \<and>
-   (fv_pat xe = supp xe \<and> fv_b_pat xe = supp_rel alpha_b_pat xe)"
-apply(rule fun_pats.induct)
-apply(tactic {* ALLGOALS (TRY o rtac @{thm conjI})*})
-thm fun_pats.inducts
-oops
-
-
-lemma
-  "fv_exp x = supp x" and
-  "fv_fnclause y = supp y" and
-  "fv_fnclauses xb = supp xb" and
-  "fv_lrb xc = supp xc" and
-  "fv_lrbs xd = supp xd" and
-  "fv_pat xe = supp xe" and
-  "fv_b_lrbs xd = supp_rel alpha_b_lrbs xd" and
-  "fv_b_pat xe = supp_rel alpha_b_pat xe" and
-  "fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and 
-  "fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and
-  "fv_b_lrb y = supp_rel alpha_b_lrb y"
-thm fun_pats.inducts
-apply(induct rule: fun_pats.inducts(1)[where ?exp="x::exp"] 
-                   fun_pats.inducts(2)[where ?fnclause="y"]
-                   fun_pats.inducts(3)[where ?fnclauses="xb"]
-                   fun_pats.inducts(4)[where ?lrb="xc"] 
-                   fun_pats.inducts(5)[where ?lrbs="xd"]
-                   fun_pats.inducts(6)[where ?pat="xe"])
-thm fun_pats.inducts
-oops
-
-end
-
-
-