Theory BinInduct

header {* Integers as an Inductive Datatype *}

theory BinInduct imports Main begin

subsection {* Inductive property of BIT *}

consts Numerals :: "int set"
inductive Numerals
intros
  Numerals_Pls: "Numeral.Pls ∈ Numerals"
  Numerals_Min: "Numeral.Min ∈ Numerals"
  Numerals_B0: "z ∈ Numerals ==> z BIT bit.B0 ∈ Numerals"
  Numerals_B1: "z ∈ Numerals ==> z BIT bit.B1 ∈ Numerals"

lemma Numerals_succ: "z ∈ Numerals ==> Numeral.succ z ∈ Numerals"
by (erule Numerals.induct, simp_all add: Numerals.intros)

lemma Numerals_pred: "z ∈ Numerals ==> Numeral.pred z ∈ Numerals"
by (erule Numerals.induct, simp_all add: Numerals.intros)

lemma Numerals_uminus: "z ∈ Numerals ==> uminus z ∈ Numerals"
by (erule Numerals.induct, simp_all add: Numerals.intros Numerals_pred)

lemma Numerals_int: "int n ∈ Numerals"
apply (induct "n")
apply (simp add: Numerals_Pls [unfolded Numeral.Pls_def])
apply (drule Numerals_succ [unfolded Numeral.succ_def])
apply (simp add: add_commute)
done

lemma mem_Numerals: "z ∈ Numerals"
by (induct "z") (simp_all only: Numerals_int Numerals_uminus)

lemma BIT_induct [case_names Pls Min B0 B1]:
  assumes Pls: "P Numeral.Pls"
  assumes Min: "P Numeral.Min"
  assumes B0: "!!x. [|P x; x ≠ Numeral.Pls|] ==> P (x BIT bit.B0)"
  assumes B1: "!!x. [|P x; x ≠ Numeral.Min|] ==> P (x BIT bit.B1)"
  shows "P x"
apply (induct x rule: Numerals.induct [OF mem_Numerals])
apply (rule Pls)
apply (rule Min)
apply (case_tac "z = Numeral.Pls", simp)
apply (erule (1) B0)
apply (case_tac "z = Numeral.Min", simp)
apply (erule (1) B1)
done

subsection {* Injectivity of BIT *}

lemma BIT_inject: "x BIT a = y BIT b ==> x = y ∧ a = b"
apply (drule_tac f="number_of :: int => int" in arg_cong)
apply (case_tac "a", case_tac [!] "b")
apply (simp_all add: succ_def pred_def)
apply (simp_all add: number_of_is_id iszero_def)
done

lemma BIT_eq: "(x BIT a = y BIT b) = (x = y ∧ a = b)"
by (safe dest!: BIT_inject)

lemma BIT_eq_Pls: "(w BIT b = Numeral.Pls) = (w = Numeral.Pls ∧ b = bit.B0)"
by (subst Pls_0_eq [symmetric], simp only: BIT_eq)

lemma BIT_eq_Min: "(w BIT b = Numeral.Min) = (w = Numeral.Min ∧ b = bit.B1)"
by (subst Min_1_eq [symmetric], simp only: BIT_eq)

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

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

lemma Min_neq_Pls: "Numeral.Min ≠ Numeral.Pls"
by (unfold Min_def Pls_def) simp

lemma Pls_neq_Min: "Numeral.Pls ≠ Numeral.Min"
by (unfold Min_def Pls_def) simp

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

lemma BIT_exhausts: "∃w b. x = w BIT b"
apply (induct x rule: BIT_induct)
apply (fast intro: Pls_0_eq [symmetric] Min_1_eq [symmetric])+
done

definition
  div2 :: "int => int" where
  "div2 x = (THE w. ∃b. x = w BIT b)"

definition
  lsb :: "int => bit" where
  "lsb x = (THE b. ∃w. x = w BIT b)"

lemma div2_BIT [simp]: "div2 (w BIT b) = w"
by (unfold div2_def, rule the_equality, fast, simp)

lemma div2_Pls [simp]: "div2 Numeral.Pls = Numeral.Pls"
by (subst Pls_0_eq [symmetric], rule div2_BIT)

lemma div2_Min [simp]: "div2 Numeral.Min = Numeral.Min"
by (subst Min_1_eq [symmetric], rule div2_BIT)

lemma lsb_BIT [simp]: "lsb (w BIT b) = b"
by (unfold lsb_def, rule the_equality, fast, simp)

lemma lsb_Pls [simp]: "lsb Numeral.Pls = bit.B0"
by (subst Pls_0_eq [symmetric], rule lsb_BIT)

lemma lsb_Min [simp]: "lsb Numeral.Min = bit.B1"
by (subst Min_1_eq [symmetric], rule lsb_BIT)

lemma div2_BIT_lsb: "(div2 x) BIT (lsb x) = x"
by (induct x rule: BIT_induct) simp_all

lemmas div2_lsb_simps =
  div2_BIT div2_Pls div2_Min
  lsb_BIT lsb_Pls lsb_Min
  div2_BIT_lsb

lemma wf_div2: "wf {(div2 w, w) |w. w ≠ Numeral.Pls ∧ w ≠ Numeral.Min}"
 apply (rule wfUNIVI, simp (no_asm_use))
 apply (rename_tac "z", induct_tac "z" rule: BIT_induct)
    apply (drule spec, erule mp, simp)
   apply (drule spec, erule mp, simp)
  apply (drule spec, erule mp, simp)
 apply (drule spec, erule mp, simp)
done

subsection {* Testing bit positions *}

consts getbit :: "int => nat => bit"

primrec
  "getbit x 0 = lsb x"
  "getbit x (Suc n) = getbit (div2 x) n"

lemma getbit_Pls: "getbit Numeral.Pls n = bit.B0"
by (induct n) simp_all

lemma getbit_Min: "getbit Numeral.Min n = bit.B1"
by (induct n) simp_all

lemma getbit_Pls_rev:
   "(∀n. getbit x n = bit.B0) ==> x = Numeral.Pls"
proof (induct x rule: BIT_induct)
  case Pls
  show ?case by simp
next
  case Min
  thus ?case by (simp add: getbit_Min)
next
  case (B0 z)
  have "∀n. getbit (z BIT bit.B0) (Suc n) = bit.B0" using B0(3) by fast
  hence "∀n. getbit z n = bit.B0" by simp
  hence "z = Numeral.Pls" by (rule B0(1))
  thus ?case by simp
next
  case (B1 z)
  have "getbit (z BIT bit.B1) 0 = bit.B0" using B1(3) by fast
  thus ?case by simp
qed

lemma getbit_Min_rev:
   "(∀n. getbit x n = bit.B1) ==> x = Numeral.Min"
proof (induct x rule: BIT_induct)
  case Pls
  thus ?case by (simp add: getbit_Pls)
next
  case Min
  show ?case by simp
next
  case (B0 z)
  have "getbit (z BIT bit.B0) 0 = bit.B1" using B0(3) by fast
  thus ?case by simp
next
  case (B1 z)
  have "∀n. getbit (z BIT bit.B1) (Suc n) = bit.B1" using B1(3) by fast
  hence "∀n. getbit z n = bit.B1" by simp
  hence "z = Numeral.Min" by (rule B1(1))
  thus ?case by simp
qed

lemma getbit_ext: "!!x. ∀n. getbit x n = getbit y n ==> (x::int) = y"
proof (induct y rule: BIT_induct)
  case Pls
  hence "∀n. getbit x n = bit.B0" by (simp add: getbit_Pls)
  thus ?case by (rule getbit_Pls_rev)
next
  case Min
  hence "∀n. getbit x n = bit.B1" by (simp add: getbit_Min)
  thus ?case by (rule getbit_Min_rev)
next
  case (B0 z)
  have "∀n. getbit x (Suc n) = getbit (z BIT bit.B0) (Suc n)"
    using B0(3) by fast
  hence "∀n. getbit (div2 x) n = getbit z n" by simp
  hence 1: "div2 x = z" by (rule B0(1))
  have "getbit x 0 = getbit (z BIT bit.B0) 0" using B0(3) by fast
  hence 2: "lsb x = bit.B0" by simp
  from 1 2 have "div2 x BIT lsb x = z BIT bit.B0" by simp
  thus "x = z BIT bit.B0" by (simp only: div2_BIT_lsb)
next
  case (B1 z)
  have "∀n. getbit x (Suc n) = getbit (z BIT bit.B1) (Suc n)"
    using B1(3) by fast
  hence "∀n. getbit (div2 x) n = getbit z n" by simp
  hence 1: "div2 x = z" by (rule B1(1))
  have "getbit x 0 = getbit (z BIT bit.B1) 0" using B1(3) by fast
  hence 2: "lsb x = bit.B1" by simp
  from 1 2 have "div2 x BIT lsb x = z BIT bit.B1" by simp
  thus "x = z BIT bit.B1" by (simp only: div2_BIT_lsb)
qed

lemma expand_getbit_eq:
  "((x::int) = y) = (∀n. getbit x n = getbit y n)"
by (safe intro!: getbit_ext)

end