--- a/src/HOL/Word/BinInduct.thy Tue Aug 28 19:45:45 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-(*
- 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