16 

    17 lemma size_eqvt: "size (pi \<bullet> x) = size x"

    18 sorry (* Can this be shown? *)

    19 

    20 instantiation t and tyS :: size begin

    21 

    22 quotient_definition

    23   "size_t :: t \<Rightarrow> nat"

    24 is

    25   "size :: t_raw \<Rightarrow> nat"

    26 

    27 quotient_definition

    28   "size_tyS :: tyS \<Rightarrow> nat"

    29 is

    30   "size :: tyS_raw \<Rightarrow> nat"

    31 

    32 lemma size_rsp:

    33   "alpha_t_raw x y \<Longrightarrow> size x = size y"

    34   "alpha_tyS_raw a b \<Longrightarrow> size a = size b"

    35   apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)

    36   apply (simp_all only: t_raw_tyS_raw.size)

    37   apply (simp_all only: alpha_gen)

    38   apply clarify

    39   apply (simp_all only: size_eqvt)

    40   done

    41 

    42 lemma [quot_respect]:

    43   "(alpha_t_raw ===> op =) size size"

    44   "(alpha_tyS_raw ===> op =) size size"

    45   by (simp_all add: size_rsp)

    46 

    47 lemma [quot_preserve]:

    48   "(rep_t ---> id) size = size"

    49   "(rep_tyS ---> id) size = size"

    50   by (simp_all add: size_t_def size_tyS_def)

    51 

    52 instance

    53   by default

    54 

    55 end

    56 

    57 thm t_raw_tyS_raw.size(4)[quot_lifted]

    58 thm t_raw_tyS_raw.size(5)[quot_lifted]

    59 thm t_raw_tyS_raw.size(6)[quot_lifted]

    60