src/HOL/Word/BinInduct.thy

declare bin_rest_BIT_bin_last [simp]

(*
  ID:     $Id$
  Author: Brian Huffman
*)

header {* Binary Integers as an Inductive Datatype *}

theory BinInduct imports Main begin

subsection {* Injectivity and distinctness of constructors *}

lemma BIT_eq: "x BIT a = y BIT b \<Longrightarrow> x = y \<and> a = b"
  by (simp add: eq_number_of_BIT_BIT [unfolded number_of_is_id])

lemma BIT_eq_iff: "(x BIT a = y BIT b) = (x = y \<and> a = b)"
  by (safe dest!: BIT_eq)

lemma BIT_eq_Pls: "(w BIT b = Numeral.Pls) = (w = Numeral.Pls \<and> b = bit.B0)"
  by (subst Pls_0_eq [symmetric], simp only: BIT_eq_iff)

lemma BIT_eq_Min: "(w BIT b = Numeral.Min) = (w = Numeral.Min \<and> b = bit.B1)"
  by (subst Min_1_eq [symmetric], simp only: BIT_eq_iff)

lemma Pls_eq_BIT: "(Numeral.Pls = w BIT b) = (w = Numeral.Pls \<and> b = bit.B0)"
  by (subst eq_commute, rule BIT_eq_Pls)

lemma Min_eq_BIT: "(Numeral.Min = w BIT b) = (w = Numeral.Min \<and> b = bit.B1)"
  by (subst eq_commute, rule BIT_eq_Min)

lemma Min_neq_Pls: "Numeral.Min \<noteq> Numeral.Pls"
  unfolding Min_def Pls_def by simp

lemma Pls_neq_Min: "Numeral.Pls \<noteq> Numeral.Min"
  unfolding Min_def Pls_def by simp

lemmas bin_injects [simp] =
  BIT_eq_iff BIT_eq_Pls BIT_eq_Min
  Pls_eq_BIT Min_eq_BIT Min_neq_Pls Pls_neq_Min


subsection {* Induction and case analysis *}

inductive
  is_numeral :: "int \<Rightarrow> bool"
where
  Pls: "is_numeral Numeral.Pls"
| Min: "is_numeral Numeral.Min"
| B0: "is_numeral z \<Longrightarrow> is_numeral (z BIT bit.B0)"
| B1: "is_numeral z \<Longrightarrow> is_numeral (z BIT bit.B1)"

lemma is_numeral_succ: "is_numeral z \<Longrightarrow> is_numeral (Numeral.succ z)"
  by (erule is_numeral.induct, simp_all add: is_numeral.intros)

lemma is_numeral_pred: "is_numeral z \<Longrightarrow> is_numeral (Numeral.pred z)"
  by (erule is_numeral.induct, simp_all add: is_numeral.intros)

lemma is_numeral_uminus: "is_numeral z \<Longrightarrow> is_numeral (uminus z)"
  by (erule is_numeral.induct, simp_all add: is_numeral.intros is_numeral_pred)

lemma is_numeral_int: "is_numeral (int n)"
  apply (induct "n")
  apply (simp add: is_numeral.Pls [unfolded Numeral.Pls_def])
  apply (drule is_numeral_succ [unfolded Numeral.succ_def])
  apply (simp add: add_commute)
  done

lemma is_numeral: "is_numeral z"
  by (induct "z") (simp_all only: is_numeral_int is_numeral_uminus)

lemma int_bin_induct [case_names Pls Min B0 B1]:
  assumes Pls: "P Numeral.Pls"
  assumes Min: "P Numeral.Min"
  assumes B0: "\<And>x. \<lbrakk>P x; x \<noteq> Numeral.Pls\<rbrakk> \<Longrightarrow> P (x BIT bit.B0)"
  assumes B1: "\<And>x. \<lbrakk>P x; x \<noteq> Numeral.Min\<rbrakk> \<Longrightarrow> P (x BIT bit.B1)"
  shows "P x"
proof (induct x rule: is_numeral.induct [OF is_numeral])
  from Pls show "P Numeral.Pls" .
  from Min show "P Numeral.Min" .
  fix z
  show "P z \<Longrightarrow> P (z BIT bit.B0)"
    by (cases "z = Numeral.Pls", auto intro: Pls B0)
  show "P z \<Longrightarrow> P (z BIT bit.B1)"
    by (cases "z = Numeral.Min", auto intro: Min B1)
qed

lemma bin_induct [case_names Pls Min Bit]:
  assumes Pls: "P Numeral.Pls"
  assumes Min: "P Numeral.Min"
  assumes Bit: "\<And>bin bit. P bin \<Longrightarrow> P (bin BIT bit)"
  shows "P x"
  by (induct x rule: int_bin_induct) (auto intro: assms)

lemma BIT_exhausts: "\<exists>w b. x = w BIT b"
  by (induct x rule: bin_induct)
     (fast intro: Pls_0_eq [symmetric] Min_1_eq [symmetric])+

lemma BIT_cases: "(\<And>w b. x = w BIT b \<Longrightarrow> Q) \<Longrightarrow> Q"
  by (insert BIT_exhausts [of x], auto)


subsection {* Destructors for BIT *}

definition
  bin_rest :: "int \<Rightarrow> int" where
  "bin_rest x = (THE w. \<exists>b. x = w BIT b)"

definition
  bin_last :: "int \<Rightarrow> bit" where
  "bin_last x = (THE b. \<exists>w. x = w BIT b)"

lemma bin_rest_BIT [simp]: "bin_rest (w BIT b) = w"
  by (unfold bin_rest_def, rule the_equality, fast, simp)

lemma bin_rest_Pls [simp]: "bin_rest Numeral.Pls = Numeral.Pls"
  by (subst Pls_0_eq [symmetric], rule bin_rest_BIT)

lemma bin_rest_Min [simp]: "bin_rest Numeral.Min = Numeral.Min"
  by (subst Min_1_eq [symmetric], rule bin_rest_BIT)

lemma bin_last_BIT [simp]: "bin_last (w BIT b) = b"
  by (unfold bin_last_def, rule the_equality, fast, simp)

lemma bin_last_Pls [simp]: "bin_last Numeral.Pls = bit.B0"
  by (subst Pls_0_eq [symmetric], rule bin_last_BIT)

lemma bin_last_Min [simp]: "bin_last Numeral.Min = bit.B1"
  by (subst Min_1_eq [symmetric], rule bin_last_BIT)

lemma bin_rest_BIT_bin_last [simp]: "(bin_rest x) BIT (bin_last x) = x"
  by (cases x rule: BIT_cases) simp

lemma wf_bin_rest:
  "wf {(bin_rest w, w) |w. w \<noteq> Numeral.Pls \<and> w \<noteq> Numeral.Min}"
  apply (rule wfUNIVI, simp (no_asm_use))
  apply (rename_tac "z", induct_tac "z" rule: bin_induct)
  apply (drule spec, erule mp, simp)+
  done

subsection {* Size function *}

function
  binsize :: "int \<Rightarrow> nat"
where
  "binsize z = (if z = Numeral.Pls \<or> z = Numeral.Min
                 then 0 else Suc (binsize (bin_rest z)))"
  by pat_completeness simp

termination binsize
  apply (relation "{(bin_rest w, w) |w. w \<noteq> Numeral.Pls \<and> w \<noteq> Numeral.Min}")
  apply (rule wf_bin_rest)
  apply simp
  done

instance int :: size
  int_size_def: "size \<equiv> binsize" ..

lemma int_size_simps [simp]:
  "size Numeral.Pls = 0"
  "size Numeral.Min = 0"
  "size (w BIT bit.B0) = (if w = Numeral.Pls then 0 else Suc (size w))"
  "size (w BIT bit.B1) = (if w = Numeral.Min then 0 else Suc (size w))"
  unfolding int_size_def by simp_all

lemma size_bin_rest [simp]: "size (bin_rest w) = size w - 1"
  by (induct w rule: int_bin_induct) simp_all

lemma int_size_gt_zero_iff [simp]:
  "(0 < size w) = (w \<noteq> Numeral.Pls \<and> w \<noteq> Numeral.Min)"
  by (induct w rule: int_bin_induct) simp_all

end