# HG changeset patch
# User haftmann
# Date 1207309227 -7200
# Node ID d2fc9a18ee8ae62753d4ca8b13bbc74f11442544
# Parent  799983936aad1c33affb97a379e54df36487b0d5
tuned

diff -r 799983936aad -r d2fc9a18ee8a src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Fri Apr 04 13:40:26 2008 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy	Fri Apr 04 13:40:27 2008 +0200
@@ -9,28 +9,9 @@
 imports Main Parity
 begin
 
-datatype bit = B0 | B1
-
-definition
-  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
-  "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
-
-lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
-  unfolding Bit_def Bit0_def by simp
+lemma contentsI: "y = {x} ==> contents y = x" 
+  unfolding contents_def by auto -- {* FIXME move *}
 
-lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w"
-  unfolding Bit_def Bit1_def by simp
-
-lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
-
-hide (open) const B0 B1
-
-lemma contentsI: "y = {x} ==> contents y = x" 
-  unfolding contents_def by auto
-
-lemma prod_case_split: "prod_case = split"
-  by (rule ext)+ auto
- 
 lemmas split_split = prod.split [unfolded prod_case_split] 
 lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
 lemmas "split.splits" = split_split split_split_asm 
@@ -46,11 +27,6 @@
 
 lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by auto
 
-constdefs
-  -- "alternative way of defining @{text bin_last}, @{text bin_rest}"
-  bin_rl :: "int => int * bit" 
-  "bin_rl w == SOME (r, l). w = r BIT l"
-
 declare iszero_0 [iff]
 
 lemmas xtr1 = xtrans(1)
@@ -62,21 +38,6 @@
 lemmas xtr7 = xtrans(7)
 lemmas xtr8 = xtrans(8)
 
-lemma Min_ne_Pls [iff]:  
-  "Int.Min ~= Int.Pls"
-  unfolding Min_def Pls_def by auto
-
-lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]
-
-lemmas PlsMin_defs [intro!] = 
-  Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]
-
-lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]
-
-lemma number_of_False_cong: 
-  "False \<Longrightarrow> number_of x = number_of y"
-  by (rule FalseE)
-
 lemmas nat_simps = diff_add_inverse2 diff_add_inverse
 lemmas nat_iffs = le_add1 le_add2
 
@@ -152,141 +113,6 @@
 lemmas zdiv_le_dividend = xtr3 [OF zdiv_1 [symmetric] zdiv_mono2,
   simplified int_one_le_iff_zero_less, simplified, standard]
   
-(** ways in which type Bin resembles a datatype **)
-
-lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
-  apply (unfold Bit_def)
-  apply (simp (no_asm_use) split: bit.split_asm)
-     apply simp_all
-   apply (drule_tac f=even in arg_cong, clarsimp)+
-  done
-     
-lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE, standard]
-
-lemma BIT_eq_iff [simp]: 
-  "(u BIT b = v BIT c) = (u = v \<and> b = c)"
-  by (rule iffI) auto
-
-lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]]
-
-lemma less_Bits: 
-  "(v BIT b < w BIT c) = (v < w | v <= w & b = bit.B0 & c = bit.B1)"
-  unfolding Bit_def by (auto split: bit.split)
-
-lemma le_Bits: 
-  "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= bit.B1 | c ~= bit.B0))" 
-  unfolding Bit_def by (auto split: bit.split)
-
-lemma neB1E [elim!]:
-  assumes ne: "y \<noteq> bit.B1"
-  assumes y: "y = bit.B0 \<Longrightarrow> P"
-  shows "P"
-  apply (rule y)
-  apply (cases y rule: bit.exhaust, simp)
-  apply (simp add: ne)
-  done
-
-lemma bin_ex_rl: "EX w b. w BIT b = bin"
-  apply (unfold Bit_def)
-  apply (cases "even bin")
-   apply (clarsimp simp: even_equiv_def)
-   apply (auto simp: odd_equiv_def split: bit.split)
-  done
-
-lemma bin_exhaust:
-  assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
-  shows "Q"
-  apply (insert bin_ex_rl [of bin])  
-  apply (erule exE)+
-  apply (rule Q)
-  apply force
-  done
-
-lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
-  apply (unfold bin_rl_def)
-  apply safe
-   apply (cases w rule: bin_exhaust)
-   apply auto
-  done
-
-lemma bin_rl_simps [simp]:
-  "bin_rl Int.Pls = (Int.Pls, bit.B0)"
-  "bin_rl Int.Min = (Int.Min, bit.B1)"
-  "bin_rl (r BIT b) = (r, b)"
-  "bin_rl (Int.Bit0 r) = (r, bit.B0)"
-  "bin_rl (Int.Bit1 r) = (r, bit.B1)"
-  unfolding bin_rl_char by simp_all
-
-lemma bin_abs_lem:
-  "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
-    nat (abs w) < nat (abs bin)"
-  apply (clarsimp simp add: bin_rl_char)
-  apply (unfold Pls_def Min_def Bit_def)
-  apply (cases b)
-   apply (clarsimp, arith)
-  apply (clarsimp, arith)
-  done
-
-lemma bin_induct:
-  assumes PPls: "P Int.Pls"
-    and PMin: "P Int.Min"
-    and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
-  shows "P bin"
-  apply (rule_tac P=P and a=bin and f1="nat o abs" 
-                  in wf_measure [THEN wf_induct])
-  apply (simp add: measure_def inv_image_def)
-  apply (case_tac x rule: bin_exhaust)
-  apply (frule bin_abs_lem)
-  apply (auto simp add : PPls PMin PBit)
-  done
-
-lemma numeral_induct:
-  assumes Pls: "P Int.Pls"
-  assumes Min: "P Int.Min"
-  assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)"
-  assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)"
-  shows "P x"
-  apply (induct x rule: bin_induct)
-    apply (rule Pls)
-   apply (rule Min)
-  apply (case_tac bit)
-   apply (case_tac "bin = Int.Pls")
-    apply simp
-   apply (simp add: Bit0)
-  apply (case_tac "bin = Int.Min")
-   apply simp
-  apply (simp add: Bit1)
-  done
-
-lemma no_no [simp]: "number_of (number_of i) = i"
-  unfolding number_of_eq by simp
-
-lemma Bit_B0:
-  "k BIT bit.B0 = k + k"
-   by (unfold Bit_def) simp
-
-lemma Bit_B1:
-  "k BIT bit.B1 = k + k + 1"
-   by (unfold Bit_def) simp
-  
-lemma Bit_B0_2t: "k BIT bit.B0 = 2 * k"
-  by (rule trans, rule Bit_B0) simp
-
-lemma Bit_B1_2t: "k BIT bit.B1 = 2 * k + 1"
-  by (rule trans, rule Bit_B1) simp
-
-lemma B_mod_2': 
-  "X = 2 ==> (w BIT bit.B1) mod X = 1 & (w BIT bit.B0) mod X = 0"
-  apply (simp (no_asm) only: Bit_B0 Bit_B1)
-  apply (simp add: z1pmod2)
-  done
-
-lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
-  unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
-
-lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
-  unfolding numeral_simps number_of_is_id by simp
-
 lemma axxbyy:
   "a + m + m = b + n + n ==> (a = 0 | a = 1) ==> (b = 0 | b = 1) ==>  
    a = b & m = (n :: int)"
diff -r 799983936aad -r d2fc9a18ee8a src/HOL/Word/Size.thy
--- a/src/HOL/Word/Size.thy	Fri Apr 04 13:40:26 2008 +0200
+++ b/src/HOL/Word/Size.thy	Fri Apr 04 13:40:27 2008 +0200
@@ -6,7 +6,7 @@
     Used primarily to parameterize machine word sizes. 
 *)
 
-header "The size class"
+header "The len classes"
 
 theory Size
 imports Numeral_Type
@@ -15,7 +15,7 @@
 text {*
   The aim of this is to allow any type as index type, but to provide a
   default instantiation for numeral types. This independence requires
-  some duplication with the definitions in Numeral\_Type.
+  some duplication with the definitions in @{text "Numeral_Type"}.
 *}
 
 class len0 = type +
diff -r 799983936aad -r d2fc9a18ee8a src/HOL/Word/TdThs.thy
--- a/src/HOL/Word/TdThs.thy	Fri Apr 04 13:40:26 2008 +0200
+++ b/src/HOL/Word/TdThs.thy	Fri Apr 04 13:40:27 2008 +0200
@@ -8,7 +8,9 @@
 
 header {* Type Definition Theorems *}
 
-theory TdThs imports Main begin
+theory TdThs
+imports Main
+begin
 
 section "More lemmas about normal type definitions"
 
diff -r 799983936aad -r d2fc9a18ee8a src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Fri Apr 04 13:40:26 2008 +0200
+++ b/src/HOL/Word/WordArith.thy	Fri Apr 04 13:40:27 2008 +0200
@@ -9,8 +9,9 @@
 
 header {* Word Arithmetic *}
 
-theory WordArith imports WordDefinition begin
-
+theory WordArith
+imports WordDefinition
+begin
 
 lemma word_less_alt: "(a < b) = (uint a < uint b)"
   unfolding word_less_def word_le_def
diff -r 799983936aad -r d2fc9a18ee8a src/HOL/Word/WordMain.thy
--- a/src/HOL/Word/WordMain.thy	Fri Apr 04 13:40:26 2008 +0200
+++ b/src/HOL/Word/WordMain.thy	Fri Apr 04 13:40:27 2008 +0200
@@ -7,7 +7,8 @@
 
 header {* Main Word Library *}
 
-theory WordMain imports WordGenLib
+theory WordMain
+imports WordGenLib
 begin
 
 lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]