Theory Word_Lib.Typedef_Morphisms

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(*
  Author: Jeremy Dawson and Gerwin Klein, NICTA

  Consequences of type definition theorems, and of extended type definition.
*)

section ‹Type Definition Theorems›

theory Typedef_Morphisms
  imports Main "HOL-Library.Word" Bit_Comprehension Bits_Int
begin

subsection "More lemmas about normal type definitions"

lemma tdD1: "type_definition Rep Abs A  x. Rep x  A"
  and tdD2: "type_definition Rep Abs A  x. Abs (Rep x) = x"
  and tdD3: "type_definition Rep Abs A  y. y  A  Rep (Abs y) = y"
  by (auto simp: type_definition_def)

lemma td_nat_int: "type_definition int nat (Collect ((≤) 0))"
  unfolding type_definition_def by auto

context type_definition
begin

declare Rep [iff] Rep_inverse [simp] Rep_inject [simp]

lemma Abs_eqD: "Abs x = Abs y  x  A  y  A  x = y"
  by (simp add: Abs_inject)

lemma Abs_inverse': "r  A  Abs r = a  Rep a = r"
  by (safe elim!: Abs_inverse)

lemma Rep_comp_inverse: "Rep  f = g  Abs  g = f"
  using Rep_inverse by auto

lemma Rep_eqD [elim!]: "Rep x = Rep y  x = y"
  by simp

lemma Rep_inverse': "Rep a = r  Abs r = a"
  by (safe intro!: Rep_inverse)

lemma comp_Abs_inverse: "f  Abs = g  g  Rep = f"
  using Rep_inverse by auto

lemma set_Rep: "A = range Rep"
proof (rule set_eqI)
  show "x  A  x  range Rep" for x
    by (auto dest: Abs_inverse [of x, symmetric])
qed

lemma set_Rep_Abs: "A = range (Rep  Abs)"
proof (rule set_eqI)
  show "x  A  x  range (Rep  Abs)" for x
    by (auto dest: Abs_inverse [of x, symmetric])
qed

lemma Abs_inj_on: "inj_on Abs A"
  unfolding inj_on_def
  by (auto dest: Abs_inject [THEN iffD1])

lemma image: "Abs ` A = UNIV"
  by (fact Abs_image)

lemmas td_thm = type_definition_axioms

lemma fns1: "Rep  fa = fr  Rep  fa  Abs = Abs  fr  Abs  fr  Rep = fa"
  by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc)

lemmas fns1a = disjI1 [THEN fns1]
lemmas fns1b = disjI2 [THEN fns1]

lemma fns4: "Rep  fa  Abs = fr  Rep  fa = fr  Rep  fa  Abs = Abs  fr"
  by auto

end

interpretation nat_int: type_definition int nat "Collect ((≤) 0)"
  by (rule td_nat_int)

declare
  nat_int.Rep_cases [cases del]
  nat_int.Abs_cases [cases del]
  nat_int.Rep_induct [induct del]
  nat_int.Abs_induct [induct del]


subsection "Extended form of type definition predicate"

lemma td_conds:
  "norm  norm = norm 
    fr  norm = norm  fr  norm  fr  norm = fr  norm  norm  fr  norm = norm  fr"
  apply safe
    apply (simp_all add: comp_assoc)
   apply (simp_all add: o_assoc)
  done

lemma fn_comm_power: "fa  tr = tr  fr  fa ^^ n  tr = tr  fr ^^ n"
  apply (rule ext)
  apply (induct n)
   apply (auto dest: fun_cong)
  done

lemmas fn_comm_power' =
  ext [THEN fn_comm_power, THEN fun_cong, unfolded o_def]


locale td_ext = type_definition +
  fixes norm
  assumes eq_norm: "x. Rep (Abs x) = norm x"
begin

lemma Abs_norm [simp]: "Abs (norm x) = Abs x"
  using eq_norm [of x] by (auto elim: Rep_inverse')

lemma td_th: "g  Abs = f  f (Rep x) = g x"
  by (drule comp_Abs_inverse [symmetric]) simp

lemma eq_norm': "Rep  Abs = norm"
  by (auto simp: eq_norm)

lemma norm_Rep [simp]: "norm (Rep x) = Rep x"
  by (auto simp: eq_norm' intro: td_th)

lemmas td = td_thm

lemma set_iff_norm: "w  A  w = norm w"
  by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric])

lemma inverse_norm: "Abs n = w  Rep w = norm n"
  apply (rule iffI)
   apply (clarsimp simp add: eq_norm)
  apply (simp add: eq_norm' [symmetric])
  done

lemma norm_eq_iff: "norm x = norm y  Abs x = Abs y"
  by (simp add: eq_norm' [symmetric])

lemma norm_comps:
  "Abs  norm = Abs"
  "norm  Rep = Rep"
  "norm  norm = norm"
  by (auto simp: eq_norm' [symmetric] o_def)

lemmas norm_norm [simp] = norm_comps

lemma fns5: "Rep  fa  Abs = fr  fr  norm = fr  norm  fr = fr"
  by (fold eq_norm') auto

text ‹
  following give conditions for converses to td_fns1›
   the condition norm ∘ fr ∘ norm = fr ∘ norm› says that
    fr› takes normalised arguments to normalised results
   norm ∘ fr ∘ norm = norm ∘ fr› says that fr›
    takes norm-equivalent arguments to norm-equivalent results
   fr ∘ norm = fr› says that fr›
    takes norm-equivalent arguments to the same result
   norm ∘ fr = fr› says that fr› takes any argument to a normalised result
›
lemma fns2: "Abs  fr  Rep = fa  norm  fr  norm = fr  norm  Rep  fa = fr  Rep"
  apply (fold eq_norm')
  apply safe
   prefer 2
   apply (simp add: o_assoc)
  apply (rule ext)
  apply (drule_tac x="Rep x" in fun_cong)
  apply auto
  done

lemma fns3: "Abs  fr  Rep = fa  norm  fr  norm = norm  fr  fa  Abs = Abs  fr"
  apply (fold eq_norm')
  apply safe
   prefer 2
   apply (simp add: comp_assoc)
  apply (rule ext)
  apply (drule_tac f="a  b" for a b in fun_cong)
  apply simp
  done

lemma fns: "fr  norm = norm  fr  fa  Abs = Abs  fr  Rep  fa = fr  Rep"
  apply safe
   apply (frule fns1b)
   prefer 2
   apply (frule fns1a)
   apply (rule fns3 [THEN iffD1])
     prefer 3
     apply (rule fns2 [THEN iffD1])
       apply (simp_all add: comp_assoc)
   apply (simp_all add: o_assoc)
  done

lemma range_norm: "range (Rep  Abs) = A"
  by (simp add: set_Rep_Abs)

end

lemmas td_ext_def' =
  td_ext_def [unfolded type_definition_def td_ext_axioms_def]


subsection ‹Type-definition locale instantiations›

definition uints :: "nat  int set"
  ― ‹the sets of integers representing the words›
  where "uints n = range (take_bit n)"

definition sints :: "nat  int set"
  where "sints n = range (signed_take_bit (n - 1))"

lemma uints_num: "uints n = {i. 0  i  i < 2 ^ n}"
  by (simp add: uints_def range_bintrunc)

lemma sints_num: "sints n = {i. - (2 ^ (n - 1))  i  i < 2 ^ (n - 1)}"
  by (simp add: sints_def range_sbintrunc)

definition unats :: "nat  nat set"
  where "unats n = {i. i < 2 ^ n}"

― ‹naturals›
lemma uints_unats: "uints n = int ` unats n"
  apply (unfold unats_def uints_num)
  apply safe
    apply (rule_tac image_eqI)
     apply (erule_tac nat_0_le [symmetric])
  by auto

lemma unats_uints: "unats n = nat ` uints n"
  by (auto simp: uints_unats image_iff)

lemma td_ext_uint:
  "td_ext (uint :: 'a word  int) word_of_int (uints (LENGTH('a::len)))
    (λw::int. w mod 2 ^ LENGTH('a))"
  apply (unfold td_ext_def')
  apply transfer
  apply (simp add: uints_num take_bit_eq_mod)
  done

interpretation word_uint:
  td_ext
    "uint::'a::len word  int"
    word_of_int
    "uints (LENGTH('a::len))"
    "λw. w mod 2 ^ LENGTH('a::len)"
  by (fact td_ext_uint)

lemmas td_uint = word_uint.td_thm
lemmas int_word_uint = word_uint.eq_norm

lemma td_ext_ubin:
  "td_ext (uint :: 'a word  int) word_of_int (uints (LENGTH('a::len)))
    (take_bit (LENGTH('a)))"
  apply standard
  apply transfer
  apply simp
  done

interpretation word_ubin:
  td_ext
    "uint::'a::len word  int"
    word_of_int
    "uints (LENGTH('a::len))"
    "take_bit (LENGTH('a::len))"
  by (fact td_ext_ubin)

lemma td_ext_unat [OF refl]:
  "n = LENGTH('a::len) 
    td_ext (unat :: 'a word  nat) of_nat (unats n) (λi. i mod 2 ^ n)"
  apply (standard; transfer)
     apply (simp_all add: unats_def take_bit_of_nat take_bit_nat_eq_self_iff
      flip: take_bit_eq_mod)
  done

lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]

interpretation word_unat:
  td_ext
    "unat::'a::len word  nat"
    of_nat
    "unats (LENGTH('a::len))"
    "λi. i mod 2 ^ LENGTH('a::len)"
  by (rule td_ext_unat)

lemmas td_unat = word_unat.td_thm

lemma unat_le: "y  unat z  y  unats (LENGTH('a))"
  for z :: "'a::len word"
  apply (unfold unats_def)
  apply clarsimp
  apply (metis le_unat_uoi unsigned_less)
  done

lemma td_ext_sbin:
  "td_ext (sint :: 'a word  int) word_of_int (sints (LENGTH('a::len)))
    (signed_take_bit (LENGTH('a) - 1))"
  by (standard; transfer) (auto simp add: sints_def)

lemma td_ext_sint:
  "td_ext (sint :: 'a word  int) word_of_int (sints (LENGTH('a::len)))
     (λw. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) -
         2 ^ (LENGTH('a) - 1))"
  using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)

text ‹
  We do sint› before sbin›, before sint› is the user version
  and interpretations do not produce thm duplicates. I.e.
  we get the name word_sint.Rep_eqD›, but not word_sbin.Req_eqD›,
  because the latter is the same thm as the former.
›
interpretation word_sint:
  td_ext
    "sint ::'a::len word  int"
    word_of_int
    "sints (LENGTH('a::len))"
    "λw. (w + 2^(LENGTH('a::len) - 1)) mod 2^LENGTH('a::len) -
      2 ^ (LENGTH('a::len) - 1)"
  by (rule td_ext_sint)

interpretation word_sbin:
  td_ext
    "sint ::'a::len word  int"
    word_of_int
    "sints (LENGTH('a::len))"
    "signed_take_bit (LENGTH('a::len) - 1)"
  by (rule td_ext_sbin)

lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm]

lemmas td_sint = word_sint.td

lemma uints_mod: "uints n = range (λw. w mod 2 ^ n)"
  by (fact uints_def [unfolded no_bintr_alt1])

lemmas bintr_num =
  word_ubin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
lemmas sbintr_num =
  word_sbin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b

lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]

interpretation test_bit:
  td_ext
    "bit :: 'a::len word  nat  bool"
    set_bits
    "{f. i. f i  i < LENGTH('a::len)}"
    "(λh i. h i  i < LENGTH('a::len))"
  by standard (auto simp add: bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq)

lemmas td_nth = test_bit.td_thm

lemma sints_subset:
  "m  n  sints m  sints n"
  apply (simp add: sints_num)
  apply clarsimp
  apply (rule conjI)
   apply (erule order_trans[rotated])
   apply simp
  apply (erule order_less_le_trans)
  apply simp
  done

lemma uints_mono_iff: "uints l  uints m  l  m"
  using power_increasing_iff[of "2::int" l m]
  apply (auto simp: uints_num subset_iff simp del: power_increasing_iff)
  apply (meson less_irrefl not_le zero_le_numeral zero_le_power)
  done

lemmas uints_monoI = uints_mono_iff[THEN iffD2]

lemma Bit_in_uints_Suc: "of_bool c + 2 * w  uints (Suc m)" if "w  uints m"
  using that
  by (auto simp: uints_num)

lemma Bit_in_uintsI: "of_bool c + 2 * w  uints m" if "w  uints (m - 1)" "m > 0"
  using Bit_in_uints_Suc[OF that(1)] that(2)
  by auto

lemma bin_cat_in_uintsI:
  concat_bit n b a  uints m if a  uints l m  l + n
proof -
  from m  l + n obtain q where m = l + n + q
    using le_Suc_ex by blast
  then have (2::int) ^ m = 2 ^ n * 2 ^ (l + q)
    by (simp add: ac_simps power_add)
  moreover have a mod 2 ^ (l + q) = a
    using a  uints l
    by (auto simp add: uints_def take_bit_eq_mod power_add Divides.mod_mult2_eq)
  ultimately have concat_bit n b a = take_bit m (concat_bit n b a)
    by (simp add: concat_bit_eq take_bit_eq_mod push_bit_eq_mult Divides.mod_mult2_eq)
  then show ?thesis
    by (simp add: uints_def)
qed

end