# HG changeset patch
# User huffman
# Date 1187880400 -7200
# Node ID 2943ae5255d0ab219f5c7e4b95685296f3cdfc45
# Parent  35485c476d9e90c905c6963e28ea98174e58a565
theory of integers as an inductive datatype

diff -r 35485c476d9e -r 2943ae5255d0 src/HOL/Word/BinInduct.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/BinInduct.thy	Thu Aug 23 16:46:40 2007 +0200
@@ -0,0 +1,171 @@
+(*
+  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: "(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