Theory HOL-Library.Type_Length

(*  Title:      HOL/Library/Type_Length.thy
    Author:     John Matthews, Galois Connections, Inc., Copyright 2006
*)

section ‹Assigning lengths to types by type classes›

theory Type_Length
imports Numeral_Type
begin

text ‹
  The aim of this is to allow any type as index type, but to provide a
  default instantiation for numeral types. This independence requires
  some duplication with the definitions in 🗏‹Numeral_Type.thy›.
›

class len0 =
  fixes len_of :: "'a itself  nat"

syntax "_type_length" :: "type  nat" ((1LENGTH/(1'(_'))))

translations "LENGTH('a)" 
  "CONST len_of (CONST Pure.type :: 'a itself)"

print_translation let
    fun len_of_itself_tr' ctxt [Const (const_syntaxPure.type, Type (_, [T]))] =
      Syntax.const syntax_const‹_type_length› $ Syntax_Phases.term_of_typ ctxt T
  in [(const_syntaxlen_of, len_of_itself_tr')] end

text ‹Some theorems are only true on words with length greater 0.›

class len = len0 +
  assumes len_gt_0 [iff]: "0 < LENGTH('a)"
begin

lemma len_not_eq_0 [simp]:
  "LENGTH('a)  0"
  by simp

end

instantiation num0 and num1 :: len0
begin

definition len_num0: "len_of (_ :: num0 itself) = 0"
definition len_num1: "len_of (_ :: num1 itself) = 1"

instance ..

end

instantiation bit0 and bit1 :: (len0) len0
begin

definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * LENGTH('a)"
definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * LENGTH('a) + 1"

instance ..

end

lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1

instance num1 :: len
  by standard simp
instance bit0 :: (len) len
  by standard simp
instance bit1 :: (len0) len
  by standard simp

instantiation Enum.finite_1 :: len
begin

definition
  "len_of_finite_1 (x :: Enum.finite_1 itself)  (1 :: nat)"

instance
  by standard (auto simp: len_of_finite_1_def)

end

instantiation Enum.finite_2 :: len
begin

definition
  "len_of_finite_2 (x :: Enum.finite_2 itself)  (2 :: nat)"

instance
  by standard (auto simp: len_of_finite_2_def)

end

instantiation Enum.finite_3 :: len
begin

definition
  "len_of_finite_3 (x :: Enum.finite_3 itself)  (4 :: nat)"

instance
  by standard (auto simp: len_of_finite_3_def)

end

lemma length_not_greater_eq_2_iff [simp]:
  ¬ 2  LENGTH('a::len)  LENGTH('a) = 1
  by (auto simp add: not_le dest: less_2_cases)

context linordered_idom
begin

lemma two_less_eq_exp_length [simp]:
  2  2 ^ LENGTH('b::len)
  using mult_left_mono [of 1 2 ^ (LENGTH('b::len) - 1) 2]
  by (cases LENGTH('b::len)) simp_all

end

lemma less_eq_decr_length_iff [simp]:
  n  LENGTH('a::len) - Suc 0  n < LENGTH('a)
  by (cases LENGTH('a)) (simp_all add: less_Suc_eq le_less)

lemma decr_length_less_iff [simp]:
  LENGTH('a::len) - Suc 0 < n  LENGTH('a)  n
  by (cases LENGTH('a)) auto

end