# HG changeset patch
# User haftmann
# Date 1387805061 -3600
# Node ID a303daddebbf7c75b41ee47520ad8528944100b4
# Parent  d6cf9a5b9be911fba134c3d8a21bf0d6ef18f92d
syntactically tuned

diff -r d6cf9a5b9be9 -r a303daddebbf src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Mon Dec 23 14:24:20 2013 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Mon Dec 23 14:24:21 2013 +0100
@@ -482,25 +482,30 @@
 
 subsection {* Splitting and concatenation *}
 
-definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
+definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
+where
   "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
 
-fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
+where
   "bin_rsplit_aux n m c bs =
     (if m = 0 | n = 0 then bs else
       let (a, b) = bin_split n c 
       in bin_rsplit_aux n (m - n) a (b # bs))"
 
-definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
+definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
+where
   "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
 
-fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
+where
   "bin_rsplitl_aux n m c bs =
     (if m = 0 | n = 0 then bs else
       let (a, b) = bin_split (min m n) c 
       in bin_rsplitl_aux n (m - n) a (b # bs))"
 
-definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
+definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
+where
   "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
 
 declare bin_rsplit_aux.simps [simp del]
diff -r d6cf9a5b9be9 -r a303daddebbf src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Mon Dec 23 14:24:20 2013 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Mon Dec 23 14:24:21 2013 +0100
@@ -10,7 +10,8 @@
 
 subsection {* Constructors and destructors for binary integers *}
 
-definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90) where
+definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90)
+where
   "k BIT b = (if b then 1 else 0) + k + k"
 
 lemma Bit_B0:
@@ -27,14 +28,16 @@
 lemma Bit_B1_2t: "k BIT True = 2 * k + 1"
   by (rule trans, rule Bit_B1) simp
 
-definition bin_last :: "int \<Rightarrow> bool" where
+definition bin_last :: "int \<Rightarrow> bool"
+where
   "bin_last w \<longleftrightarrow> w mod 2 = 1"
 
 lemma bin_last_odd:
   "bin_last = odd"
   by (rule ext) (simp add: bin_last_def even_def)
 
-definition bin_rest :: "int \<Rightarrow> int" where
+definition bin_rest :: "int \<Rightarrow> int"
+where
   "bin_rest w = w div 2"
 
 lemma bin_rl_simp [simp]:
@@ -271,7 +274,8 @@
 
 subsection {* Truncating binary integers *}
 
-definition bin_sign :: "int \<Rightarrow> int" where
+definition bin_sign :: "int \<Rightarrow> int"
+where
   bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
 
 lemma bin_sign_simps [simp]:
diff -r d6cf9a5b9be9 -r a303daddebbf src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Mon Dec 23 14:24:20 2013 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Mon Dec 23 14:24:21 2013 +0100
@@ -31,27 +31,33 @@
 
 subsection {* Operations on lists of booleans *}
 
-primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
+primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
+where
   Nil: "bl_to_bin_aux [] w = w"
   | Cons: "bl_to_bin_aux (b # bs) w = 
       bl_to_bin_aux bs (w BIT b)"
 
-definition bl_to_bin :: "bool list \<Rightarrow> int" where
+definition bl_to_bin :: "bool list \<Rightarrow> int"
+where
   bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
 
-primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
+primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
+where
   Z: "bin_to_bl_aux 0 w bl = bl"
   | Suc: "bin_to_bl_aux (Suc n) w bl =
       bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
 
-definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
+definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
+where
   bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
 
-primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
+primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list"
+where
   Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
   | Z: "bl_of_nth 0 f = []"
 
-primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
   Z: "takefill fill 0 xs = []"
   | Suc: "takefill fill (Suc n) xs = (
       case xs of [] => fill # takefill fill n xs
@@ -65,21 +71,25 @@
   assuming input list(s) the same length, and don't extend them. 
 *}
 
-primrec rbl_succ :: "bool list => bool list" where
+primrec rbl_succ :: "bool list => bool list"
+where
   Nil: "rbl_succ Nil = Nil"
   | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
 
-primrec rbl_pred :: "bool list => bool list" where
+primrec rbl_pred :: "bool list => bool list"
+where
   Nil: "rbl_pred Nil = Nil"
   | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
 
-primrec rbl_add :: "bool list => bool list => bool list" where
+primrec rbl_add :: "bool list => bool list => bool list"
+where
   -- "result is length of first arg, second arg may be longer"
   Nil: "rbl_add Nil x = Nil"
   | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in 
     (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
 
-primrec rbl_mult :: "bool list => bool list => bool list" where
+primrec rbl_mult :: "bool list => bool list => bool list"
+where
   -- "result is length of first arg, second arg may be longer"
   Nil: "rbl_mult Nil x = Nil"
   | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
diff -r d6cf9a5b9be9 -r a303daddebbf src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Dec 23 14:24:20 2013 +0100
+++ b/src/HOL/Word/Word.thy	Mon Dec 23 14:24:21 2013 +0100
@@ -35,7 +35,8 @@
   shows "uint w mod 2 ^ len_of TYPE('a) = uint w"
   using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)
 
-definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
+definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
+where
   -- {* representation of words using unsigned or signed bins, 
         only difference in these is the type class *}
   "word_of_int k = Abs_word (k mod 2 ^ len_of TYPE('a))" 
@@ -72,7 +73,8 @@
 instantiation word :: (len0) equal
 begin
 
-definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
+definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
+where
   "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
 
 instance proof
@@ -101,31 +103,39 @@
 
 subsection {* Type conversions and casting *}
 
-definition sint :: "'a :: len word => int" where
+definition sint :: "'a :: len word => int"
+where
   -- {* treats the most-significant-bit as a sign bit *}
   sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"
 
-definition unat :: "'a :: len0 word => nat" where
+definition unat :: "'a :: len0 word => nat"
+where
   "unat w = nat (uint w)"
 
-definition uints :: "nat => int set" where
+definition uints :: "nat => int set"
+where
   -- "the sets of integers representing the words"
   "uints n = range (bintrunc n)"
 
-definition sints :: "nat => int set" where
+definition sints :: "nat => int set"
+where
   "sints n = range (sbintrunc (n - 1))"
 
-definition unats :: "nat => nat set" where
+definition unats :: "nat => nat set"
+where
   "unats n = {i. i < 2 ^ n}"
 
-definition norm_sint :: "nat => int => int" where
+definition norm_sint :: "nat => int => int"
+where
   "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
 
-definition scast :: "'a :: len word => 'b :: len word" where
+definition scast :: "'a :: len word => 'b :: len word"
+where
   -- "cast a word to a different length"
   "scast w = word_of_int (sint w)"
 
-definition ucast :: "'a :: len0 word => 'b :: len0 word" where
+definition ucast :: "'a :: len0 word => 'b :: len0 word"
+where
   "ucast w = word_of_int (uint w)"
 
 instantiation word :: (len0) size
@@ -138,29 +148,37 @@
 
 end
 
-definition source_size :: "('a :: len0 word => 'b) => nat" where
+definition source_size :: "('a :: len0 word => 'b) => nat"
+where
   -- "whether a cast (or other) function is to a longer or shorter length"
   "source_size c = (let arb = undefined ; x = c arb in size arb)"  
 
-definition target_size :: "('a => 'b :: len0 word) => nat" where
+definition target_size :: "('a => 'b :: len0 word) => nat"
+where
   "target_size c = size (c undefined)"
 
-definition is_up :: "('a :: len0 word => 'b :: len0 word) => bool" where
+definition is_up :: "('a :: len0 word => 'b :: len0 word) => bool"
+where
   "is_up c \<longleftrightarrow> source_size c <= target_size c"
 
-definition is_down :: "('a :: len0 word => 'b :: len0 word) => bool" where
+definition is_down :: "('a :: len0 word => 'b :: len0 word) => bool"
+where
   "is_down c \<longleftrightarrow> target_size c <= source_size c"
 
-definition of_bl :: "bool list => 'a :: len0 word" where
+definition of_bl :: "bool list => 'a :: len0 word"
+where
   "of_bl bl = word_of_int (bl_to_bin bl)"
 
-definition to_bl :: "'a :: len0 word => bool list" where
+definition to_bl :: "'a :: len0 word => bool list"
+where
   "to_bl w = bin_to_bl (len_of TYPE ('a)) (uint w)"
 
-definition word_reverse :: "'a :: len0 word => 'a word" where
+definition word_reverse :: "'a :: len0 word => 'a word"
+where
   "word_reverse w = of_bl (rev (to_bl w))"
 
-definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" where
+definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" 
+where
   "word_int_case f w = f (uint w)"
 
 translations
@@ -232,7 +250,8 @@
 subsection {* Correspondence relation for theorem transfer *}
 
 definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
-  where "cr_word \<equiv> (\<lambda>x y. word_of_int x = y)"
+where
+  "cr_word = (\<lambda>x y. word_of_int x = y)"
 
 lemma Quotient_word:
   "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
@@ -341,7 +360,8 @@
   apply (simp add: word_of_nat wi_hom_sub)
   done
 
-definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
+definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
+where
   "a udvd b = (EX n>=0. uint b = n * uint a)"
 
 
@@ -361,10 +381,12 @@
 
 end
 
-definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
+definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50)
+where
   "a <=s b = (sint a <= sint b)"
 
-definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) where
+definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
+where
   "(x <s y) = (x <=s y & x ~= y)"
 
 
@@ -398,10 +420,12 @@
 definition
   word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
 
-definition shiftl1 :: "'a word \<Rightarrow> 'a word" where
+definition shiftl1 :: "'a word \<Rightarrow> 'a word"
+where
   "shiftl1 w = word_of_int (uint w BIT False)"
 
-definition shiftr1 :: "'a word \<Rightarrow> 'a word" where
+definition shiftr1 :: "'a word \<Rightarrow> 'a word"
+where
   -- "shift right as unsigned or as signed, ie logical or arithmetic"
   "shiftr1 w = word_of_int (bin_rest (uint w))"
 
@@ -434,76 +458,95 @@
 
 end
 
-definition setBit :: "'a :: len0 word => nat => 'a word" where 
+definition setBit :: "'a :: len0 word => nat => 'a word"
+where 
   "setBit w n = set_bit w n True"
 
-definition clearBit :: "'a :: len0 word => nat => 'a word" where
+definition clearBit :: "'a :: len0 word => nat => 'a word"
+where
   "clearBit w n = set_bit w n False"
 
 
 subsection "Shift operations"
 
-definition sshiftr1 :: "'a :: len word => 'a word" where 
+definition sshiftr1 :: "'a :: len word => 'a word"
+where 
   "sshiftr1 w = word_of_int (bin_rest (sint w))"
 
-definition bshiftr1 :: "bool => 'a :: len word => 'a word" where
+definition bshiftr1 :: "bool => 'a :: len word => 'a word"
+where
   "bshiftr1 b w = of_bl (b # butlast (to_bl w))"
 
-definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55) where
+definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
+where
   "w >>> n = (sshiftr1 ^^ n) w"
 
-definition mask :: "nat => 'a::len word" where
+definition mask :: "nat => 'a::len word"
+where
   "mask n = (1 << n) - 1"
 
-definition revcast :: "'a :: len0 word => 'b :: len0 word" where
+definition revcast :: "'a :: len0 word => 'b :: len0 word"
+where
   "revcast w =  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
 
-definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where
+definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word"
+where
   "slice1 n w = of_bl (takefill False n (to_bl w))"
 
-definition slice :: "nat => 'a :: len0 word => 'b :: len0 word" where
+definition slice :: "nat => 'a :: len0 word => 'b :: len0 word"
+where
   "slice n w = slice1 (size w - n) w"
 
 
 subsection "Rotation"
 
-definition rotater1 :: "'a list => 'a list" where
+definition rotater1 :: "'a list => 'a list"
+where
   "rotater1 ys = 
     (case ys of [] => [] | x # xs => last ys # butlast ys)"
 
-definition rotater :: "nat => 'a list => 'a list" where
+definition rotater :: "nat => 'a list => 'a list"
+where
   "rotater n = rotater1 ^^ n"
 
-definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word" where
+definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"
+where
   "word_rotr n w = of_bl (rotater n (to_bl w))"
 
-definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word" where
+definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word"
+where
   "word_rotl n w = of_bl (rotate n (to_bl w))"
 
-definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word" where
+definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word"
+where
   "word_roti i w = (if i >= 0 then word_rotr (nat i) w
                     else word_rotl (nat (- i)) w)"
 
 
 subsection "Split and cat operations"
 
-definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word" where
+definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word"
+where
   "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
 
-definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)" where
+definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)"
+where
   "word_split a = 
    (case bin_split (len_of TYPE ('c)) (uint a) of 
      (u, v) => (word_of_int u, word_of_int v))"
 
-definition word_rcat :: "'a :: len0 word list => 'b :: len0 word" where
+definition word_rcat :: "'a :: len0 word list => 'b :: len0 word"
+where
   "word_rcat ws = 
   word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
 
-definition word_rsplit :: "'a :: len0 word => 'b :: len word list" where
+definition word_rsplit :: "'a :: len0 word => 'b :: len word list"
+where
   "word_rsplit w = 
   map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
 
-definition max_word :: "'a::len word" -- "Largest representable machine integer." where
+definition max_word :: "'a::len word" -- "Largest representable machine integer."
+where
   "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
 
 (* FIXME: only provide one theorem name *)
@@ -4536,7 +4579,8 @@
 
 subsection {* Recursion combinator for words *}
 
-definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
+definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
+where
   "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
 
 lemma word_rec_0: "word_rec z s 0 = z"