--- a/Nominal/Ex/TypeSchemes.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -6,7 +6,7 @@
 
 atom_decl name
 
-declare [[STEPS = 21]]
+declare [[STEPS = 100]]
 
 nominal_datatype ty =
   Var "name"
@@ -19,74 +19,11 @@
   Var2 "name"
 | Fun2 "ty2" "ty2"
 
-
 nominal_datatype tys2 =
   All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
 
 
-lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
-
-
-
-(* below we define manually the function for size *)
-
-lemma size_eqvt_raw:
-  "size (pi \<bullet> t  :: ty_raw)  = size t"
-  "size (pi \<bullet> ts :: tys_raw) = size ts"
-  apply (induct rule: ty_raw_tys_raw.inducts)
-  apply simp_all
-  done
-
-instantiation ty and tys :: size 
-begin
-
-quotient_definition
-  "size_ty :: ty \<Rightarrow> nat"
-is
-  "size :: ty_raw \<Rightarrow> nat"
-
-quotient_definition
-  "size_tys :: tys \<Rightarrow> nat"
-is
-  "size :: tys_raw \<Rightarrow> nat"
-
-lemma size_rsp:
-  "alpha_ty_raw x y \<Longrightarrow> size x = size y"
-  "alpha_tys_raw a b \<Longrightarrow> size a = size b"
-  apply (induct rule: alpha_ty_raw_alpha_tys_raw.inducts)
-  apply (simp_all only: ty_raw_tys_raw.size)
-  apply (simp_all only: alphas)
-  apply clarify
-  apply (simp_all only: size_eqvt_raw)
-  done
-
-lemma [quot_respect]:
-  "(alpha_ty_raw ===> op =) size size"
-  "(alpha_tys_raw ===> op =) size size"
-  by (simp_all add: size_rsp)
-
-lemma [quot_preserve]:
-  "(rep_ty ---> id) size = size"
-  "(rep_tys ---> id) size = size"
-  by (simp_all add: size_ty_def size_tys_def)
-
-instance
-  by default
-
-end
-
-thm ty_raw_tys_raw.size(4)[quot_lifted]
-thm ty_raw_tys_raw.size(5)[quot_lifted]
-thm ty_raw_tys_raw.size(6)[quot_lifted]
-
-
-thm ty_tys.fv
-thm ty_tys.eq_iff
-thm ty_tys.bn
-thm ty_tys.perm
-thm ty_tys.inducts
-thm ty_tys.distinct
-
+(*
 ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *}
 
 lemma strong_induct:
@@ -278,19 +215,6 @@
   done
 
 end
-
-(* 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".
 *)