section \<open>A constructive datatype for bytes\<close>

theory Byte
  imports
    Code_Extras
    "HOL-Library.Rewrite"
begin

subsection \<open>Bits\<close>

definition nat_of_bool :: "bool \<Rightarrow> nat" where
"nat_of_bool b = (if b then 1 else 0)"

fun bits_of_nat :: "nat \<Rightarrow> bool list" where
"bits_of_nat 0 = []" |
"bits_of_nat n = (n mod 2 = 1) # bits_of_nat (n div 2)"

fun nat_of_bits :: "bool list \<Rightarrow> nat" where
"nat_of_bits [] = 0" |
"nat_of_bits (b # bs) = nat_of_bool b + 2 * nat_of_bits bs"

lemma nat_of_bits_replicate: "nat_of_bits (replicate k False) = 0"
by (induction k) (auto simp: nat_of_bool_def)

lemma nat_of_bits_app: "nat_of_bits (xs @ ys) = nat_of_bits xs + 2 ^ length xs * nat_of_bits ys"
by (induction xs) auto

lemma nat_of_bits_of_nat: "nat_of_bits (bits_of_nat n) = n"
  apply (induction n rule: bits_of_nat.induct)
  apply (auto simp: nat_of_bool_def)
  apply presburger+
  done

lemma nat_of_bits_surj: "surj nat_of_bits"
  apply standard
  apply auto
  apply (rule image_eqI[where x = "bits_of_nat y" for y])
  apply (rule nat_of_bits_of_nat[symmetric])
  by auto

lemma exists_nat_of_bits: "\<exists>bs. nat_of_bits bs = n"
using nat_of_bits_surj unfolding surj_def by metis

lemma nat_zero_even_odd_cases[case_names zero even odd]:
  fixes n :: nat
  shows "(n = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>n'. n' > 0 \<Longrightarrow> n = 2 * n' \<Longrightarrow> P) \<Longrightarrow> (\<And>n'. n = 2 * n' + 1 \<Longrightarrow> P) \<Longrightarrow> P"
  apply (cases "n = 0"; cases "n mod 2 = 0"; auto)
  by (metis add.right_neutral add_Suc_right div_mult_mod_eq mult.commute)

lemma nat_zero_even_odd_induct[case_names zero even odd]:
  fixes n :: nat
  assumes "P 0"
  assumes "(\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (2 * n))"
  assumes "(\<And>n. P n \<Longrightarrow> P (2 * n + 1))"
  shows "P n"
  using assms
  apply induction_schema
  apply (erule nat_zero_even_odd_cases; assumption)
  apply lexicographic_order
  done

lemma exists_nat_of_bits':
  assumes "n < 2 ^ k"
  obtains bs where "length bs \<le> k" "nat_of_bits bs = n"
using assms proof (induction n arbitrary: k thesis rule: nat_zero_even_odd_induct)
  case zero
  show ?case
    by (rule zero(1)[where bs = "[]"]) auto
next
  case (even n)
  then obtain k' where "k = Suc k'"
    by (metis One_nat_def Suc_mult_cancel1 bits_of_nat.cases gr0_conv_Suc less_Suc0 mult.commute mult_zero_left numeral_2_eq_2 power.simps(1))
  hence "n < 2 ^ k'"
    using even by auto

  then obtain bs' where "length bs' \<le> k'" "nat_of_bits bs' = n"
    using even by auto

  show ?case
    apply (rule even(3)[where bs = "False # bs'"])
    using \<open>length bs' \<le> k'\<close> \<open>k = _\<close> apply simp
    using \<open>nat_of_bits bs' = n\<close> apply (simp add: nat_of_bool_def)
    done
next
  case (odd n)
  then obtain k' where "k = Suc k'"
    by (metis One_nat_def Suc_eq_plus1 bits_of_nat.cases less_Suc0 power_0)

  hence "n < 2 ^ k'"
    using odd by auto

  then obtain bs' where "length bs' \<le> k'" "nat_of_bits bs' = n"
    using odd by auto

  show ?case
    apply (rule odd(2)[where bs = "True # bs'"])
    using \<open>length bs' \<le> k'\<close> \<open>k = _\<close> apply simp
    using \<open>nat_of_bits bs' = n\<close> apply (simp add: nat_of_bool_def)
    done
qed

lemma nat_of_bits_pow2: "nat_of_bits bs < 2 ^ length bs"
by (induction bs) (auto simp: nat_of_bool_def)

lemma bits_of_nat_inject: "bits_of_nat x = bits_of_nat y \<Longrightarrow> x = y"
proof (induction x arbitrary: y rule: bits_of_nat.induct)
  case 1
  hence "bits_of_nat y = []"
    by simp
  thus ?case
    by (auto elim: bits_of_nat.elims)
next
  case (2 x)
  hence *: "bits_of_nat y = (Suc x mod 2 = Suc 0) # bits_of_nat (Suc x div 2)"
    by simp
  then obtain y' where "y = Suc y'"
    by (auto elim: bits_of_nat.elims)

  hence "Suc x mod 2 = y mod 2" "bits_of_nat (Suc x div 2) = bits_of_nat (y div 2)"
    using * by auto

  hence "Suc x div 2 = y div 2"
    using 2 by auto

  show ?case
    using \<open>Suc x div 2 = y div 2\<close> \<open>Suc x mod 2 = y mod 2\<close>
    by (metis div_mult_mod_eq)
qed

lemma bits_of_nat_inj: "inj bits_of_nat"
using bits_of_nat_inject by standard auto

lemma nat_of_bits_inject:
  assumes "length xs = length ys"
  assumes "nat_of_bits xs = nat_of_bits ys"
  shows "xs = ys"
using assms
by (induction xs ys rule: list_induct2) (auto simp: nat_of_bool_def split: if_splits)


subsection \<open>Bytes\<close>

datatype byte =
  Byte (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool)
       (digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool)

definition bits_of_byte :: "byte \<Rightarrow> bool list" where
"bits_of_byte b = [digit0 b, digit1 b, digit2 b, digit3 b, digit4 b, digit5 b, digit6 b, digit7 b]"

lemma bits_of_byte_length[simp]: "length (bits_of_byte b) = 8"
unfolding bits_of_byte_def by simp

lemma bits_of_byte_inject: "bits_of_byte x = bits_of_byte y \<Longrightarrow> x = y"
unfolding bits_of_byte_def
by (cases x; cases y) auto

definition nth_or_else :: "'a list \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" where
"nth_or_else xs a n = (if n < length xs then xs ! n else a)"

lemma nth_or_else_code[code]:
  "nth_or_else [] a n = a"
  "nth_or_else (x # xs) a 0 = x"
  "nth_or_else (x # xs) a (Suc n) = nth_or_else xs a n"
unfolding nth_or_else_def
by auto

definition byte_of_bits :: "bool list \<Rightarrow> byte" where
"byte_of_bits bs =
  Byte (nth_or_else bs False 0)
       (nth_or_else bs False 1)
       (nth_or_else bs False 2)
       (nth_or_else bs False 3)
       (nth_or_else bs False 4)
       (nth_or_else bs False 5)
       (nth_or_else bs False 6)
       (nth_or_else bs False 7)"

lemma [simp, code_unfold]:
  "byte_of_bits [] = Byte False False False False False False False False"
  "byte_of_bits [b1] = Byte b1 False False False False False False False"
  "byte_of_bits [b1, b2] = Byte b1 b2 False False False False False False"
  "byte_of_bits [b1, b2, b3] = Byte b1 b2 b3 False False False False False"
  "byte_of_bits [b1, b2, b3, b4] = Byte b1 b2 b3 b4 False False False False"
  "byte_of_bits [b1, b2, b3, b4, b5] = Byte b1 b2 b3 b4 b5 False False False"
  "byte_of_bits [b1, b2, b3, b4, b5, b6] = Byte b1 b2 b3 b4 b5 b6 False False"
  "byte_of_bits [b1, b2, b3, b4, b5, b6, b7] = Byte b1 b2 b3 b4 b5 b6 b7 False"
  "byte_of_bits [b1, b2, b3, b4, b5, b6, b7, b8] = Byte b1 b2 b3 b4 b5 b6 b7 b8"
unfolding byte_of_bits_def
by (auto simp: nth_or_else_def)

lemma byte_of_bits_of_byte: "byte_of_bits (bits_of_byte b) = b"
by (cases b) (auto simp: byte_of_bits_def bits_of_byte_def nth_or_else_def)

lemma bits_of_byte_of_bits: "length bs = 8 \<Longrightarrow> bits_of_byte (byte_of_bits bs) = bs"
unfolding byte_of_bits_def bits_of_byte_def nth_or_else_def
  apply auto
  apply (rewrite in "_ = \<hole>" map_nth[symmetric])
  by (simp add: numeral_nat)

definition nat_of_byte :: "byte \<Rightarrow> nat" where
"nat_of_byte b = nat_of_bits (bits_of_byte b)"

lemma nat_of_byte_inject: "nat_of_byte x = nat_of_byte y \<Longrightarrow> x = y"
unfolding nat_of_byte_def
by (metis bits_of_byte_length bits_of_byte_inject nat_of_bits_inject)

lemma nat_of_byte_256: "nat_of_byte b < 256"
proof -
  have "nat_of_bits (bits_of_byte b) < 2 ^ length (bits_of_byte b)"
    by (rule nat_of_bits_pow2)
  hence "nat_of_bits (bits_of_byte b) < 256"
    by simp
  thus ?thesis
    unfolding nat_of_byte_def .
qed

definition byte_of_nat :: "nat \<Rightarrow> byte" where
"byte_of_nat n = byte_of_bits (bits_of_nat n)"

lemma exists_nat_of_byte:
  assumes "n < 256"
  shows "\<exists>b. nat_of_byte b = n"
proof -
  obtain bs where "length bs \<le> 8" "nat_of_bits bs = n"
    using assms exists_nat_of_bits'[where k = 8] by auto
  have "nat_of_byte (byte_of_bits (bs @ replicate (8 - length bs) False)) = n"
    unfolding nat_of_byte_def
    apply (subst bits_of_byte_of_bits)
    apply simp
    using \<open>length bs \<le> 8\<close> apply force
    apply (simp add: nat_of_bits_app nat_of_bits_replicate)
    apply fact
    done
  thus ?thesis
    by auto
qed

context
  includes char.lifting
begin

lift_definition char_of_byte :: "byte \<Rightarrow> char" is nat_of_byte
by (fact nat_of_byte_256)

free_constructors (plugins del: code codetype) case_char for char_of_byte
proof -
  fix P y
  show P if "\<And>x. y = char_of_byte x \<Longrightarrow> P"
    using that
    apply transfer
    using exists_nat_of_byte by metis
next
  show "char_of_byte x = char_of_byte y \<longleftrightarrow> x = y" for x y
    apply transfer
    using nat_of_byte_inject by metis
qed

end


subsection \<open>Code\<close>

named_theorems char_byte_literals

lemma [char_byte_literals]: "0 = char_of_byte (Byte False False False False False False False False)"
unfolding zero_char_def char_of_byte.abs_eq char_of_nat_def nat_of_byte_def
by (rule arg_cong[where f = Abs_char]) code_simp

local_setup \<open>fn lthy =>
  let
    fun mk_bool true = @{const HOL.True}
      | mk_bool false = @{const HOL.False}

    fun mk_bits 0 = []
      | mk_bits n = mk_bool (n mod 2 = 1) :: mk_bits (n div 2)

    fun mk_byte n =
      let val bits = mk_bits n in
        list_comb (@{const Byte}, mk_bits n @ replicate (8 - length bits) (mk_bool false))
      end

    fun mk_goal n =
      HOLogic.mk_eq (@{const String.Char} $ HOLogic.mk_numeral n, @{const char_of_byte} $ mk_byte n)
    val goals = map (HOLogic.mk_Trueprop o mk_goal) (1 upto 255)
    fun cong ctxt = Drule.infer_instantiate ctxt [(("f", 0), @{cterm Abs_char})] @{thm arg_cong}

    val thms =
      Goal.prove_common lthy (SOME ~1) [] [] goals (fn {context = ctxt, ...} =>
        Local_Defs.unfold_tac ctxt @{thms String.Char_def char_of_byte.abs_eq char_of_nat_def nat_of_byte_def} THEN
          Goal.conjunction_tac 1 THEN
            PARALLEL_ALLGOALS (resolve_tac ctxt [cong ctxt] THEN' Code_Simp.dynamic_tac ctxt))
  in
    Local_Theory.note ((Binding.empty, @{attributes [char_byte_literals]}), thms) lthy
    |> snd
  end
\<close>

definition abort :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
[simp, code del]: "abort f = f ()"

bundle char_byte_representation begin

declare [["code_datatype" char_of_byte]]

declare [[code drop: equal_char_inst.equal_char String.Char]]

lemma [code]: "HOL.equal (char_of_byte b1) (char_of_byte b2) = (b1 = b2)"
by (subst equal) auto

declare char_of_byte.rep_eq[code]
declare integer_of_char_Char_code[code del]
declare integer_of_char_zero[code del]
declare integer_of_char_def[code]

declare char_byte_literals[code_unfold]
declare char_byte_literals[symmetric, code_post]

lemma [code_unfold]: "Code.abort x f = abort f"
by simp

declare [[code abort: abort]]

end

end