--- a/Nominal/TySch.thy	Sat Mar 20 09:27:28 2010 +0100
+++ b/Nominal/TySch.thy	Sat Mar 20 10:12:09 2010 +0100
@@ -14,6 +14,51 @@
 and tyS =
   All xs::"name fset" ty::"t" bind xs in ty
 
+lemma size_eqvt: "size (pi \<bullet> x) = size x"
+sorry (* Can this be shown? *)
+
+instantiation t and tyS :: size begin
+
+quotient_definition
+  "size_t :: t \<Rightarrow> nat"
+is
+  "size :: t_raw \<Rightarrow> nat"
+
+quotient_definition
+  "size_tyS :: tyS \<Rightarrow> nat"
+is
+  "size :: tyS_raw \<Rightarrow> nat"
+
+lemma size_rsp:
+  "alpha_t_raw x y \<Longrightarrow> size x = size y"
+  "alpha_tyS_raw a b \<Longrightarrow> size a = size b"
+  apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
+  apply (simp_all only: t_raw_tyS_raw.size)
+  apply (simp_all only: alpha_gen)
+  apply clarify
+  apply (simp_all only: size_eqvt)
+  done
+
+lemma [quot_respect]:
+  "(alpha_t_raw ===> op =) size size"
+  "(alpha_tyS_raw ===> op =) size size"
+  by (simp_all add: size_rsp)
+
+lemma [quot_preserve]:
+  "(rep_t ---> id) size = size"
+  "(rep_tyS ---> id) size = size"
+  by (simp_all add: size_t_def size_tyS_def)
+
+instance
+  by default
+
+end
+
+thm t_raw_tyS_raw.size(4)[quot_lifted]
+thm t_raw_tyS_raw.size(5)[quot_lifted]
+thm t_raw_tyS_raw.size(6)[quot_lifted]
+
+
 thm t_tyS.fv
 thm t_tyS.eq_iff
 thm t_tyS.bn