src/HOL/Library/Word.thy

 
 primrec bitval :: "bit => nat" where
     "bitval \<zero> = 0"
   | "bitval \<one> = 1"
 
-consts
-  bitnot :: "bit => bit"
-  bitand :: "bit => bit => bit" (infixr "bitand" 35)
-  bitor  :: "bit => bit => bit" (infixr "bitor"  30)
-  bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
+primrec bitnot :: "bit => bit" where
+    bitnot_zero: "(bitnot \<zero>) = \<one>"
+  | bitnot_one : "(bitnot \<one>)  = \<zero>"
+
+primrec bitand :: "bit => bit => bit" (infixr "bitand" 35) where
+    bitand_zero: "(\<zero> bitand y) = \<zero>"
+  | bitand_one:  "(\<one> bitand y) = y"
+
+primrec bitor  :: "bit => bit => bit" (infixr "bitor"  30) where
+    bitor_zero: "(\<zero> bitor y) = y"
+  | bitor_one:  "(\<one> bitor y) = \<one>"
+
+primrec bitxor :: "bit => bit => bit" (infixr "bitxor" 30) where
+    bitxor_zero: "(\<zero> bitxor y) = y"
+  | bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
 
 notation (xsymbols)
   bitnot ("\<not>\<^sub>b _" [40] 40) and
   bitand (infixr "\<and>\<^sub>b" 35) and
   bitor  (infixr "\<or>\<^sub>b" 30) and

 notation (HTML output)
   bitnot ("\<not>\<^sub>b _" [40] 40) and
   bitand (infixr "\<and>\<^sub>b" 35) and
   bitor  (infixr "\<or>\<^sub>b" 30) and
   bitxor (infixr "\<oplus>\<^sub>b" 30)
-
-primrec
-  bitnot_zero: "(bitnot \<zero>) = \<one>"
-  bitnot_one : "(bitnot \<one>)  = \<zero>"
-
-primrec
-  bitand_zero: "(\<zero> bitand y) = \<zero>"
-  bitand_one:  "(\<one> bitand y) = y"
-
-primrec
-  bitor_zero: "(\<zero> bitor y) = y"
-  bitor_one:  "(\<one> bitor y) = \<one>"
-
-primrec
-  bitxor_zero: "(\<zero> bitxor y) = y"
-  bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
 
 lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b"
   by (cases b) simp_all
 
 lemma bitand_cancel [simp]: "(b bitand b) = b"

   also have "... = bv_extend n b (b#w)"
     by (simp add: bv_extend_def)
   finally show "bv_extend n b w = bv_extend n b (b#w)" .
 qed
 
-consts
-  rem_initial :: "bit => bit list => bit list"
-primrec
-  "rem_initial b [] = []"
-  "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
+primrec rem_initial :: "bit => bit list => bit list" where
+    "rem_initial b [] = []"
+  | "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
 
 lemma rem_initial_length: "length (rem_initial b w) \<le> length w"
   by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all)
 
 lemma rem_initial_equal:

     by arith
 qed
 
 subsection {* Signed Vectors *}
 
-consts
-  norm_signed :: "bit list => bit list"
-primrec
-  norm_signed_Nil: "norm_signed [] = []"
-  norm_signed_Cons: "norm_signed (b#bs) =
-    (case b of
-      \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
-    | \<one> => b#rem_initial b bs)"
+primrec norm_signed :: "bit list => bit list" where
+    norm_signed_Nil: "norm_signed [] = []"
+  | norm_signed_Cons: "norm_signed (b#bs) =
+      (case b of
+        \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
+      | \<one> => b#rem_initial b bs)"
 
 lemma norm_signed0 [simp]: "norm_signed [\<zero>] = []"
   by simp
 
 lemma norm_signed1 [simp]: "norm_signed [\<one>] = [\<one>]"

 
 lemma bv_extend_norm_signed: "bv_msb w = b ==> bv_extend (length w) b (norm_signed w) = w"
 proof (rule bit_list_cases [of w],simp_all)
   fix xs
   show "bv_extend (Suc (length xs)) \<zero> (norm_signed (\<zero>#xs)) = \<zero>#xs"
-  proof (simp add: norm_signed_list_def,auto)
+  proof (simp add: norm_signed_def,auto)
     assume "norm_unsigned xs = []"
     hence xx: "rem_initial \<zero> xs = []"
       by (simp add: norm_unsigned_def)
     have "bv_extend (Suc (length xs)) \<zero> (\<zero>#rem_initial \<zero> xs) = \<zero>#xs"
       apply (simp add: bv_extend_def replicate_app_Cons_same)

 lemmas [simp] = length_nat_non0
 
 lemma "nat_to_bv (number_of Int.Pls) = []"
   by simp
 
-consts
-  fast_bv_to_nat_helper :: "[bit list, int] => int"
-primrec
-  fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
-  fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
-    fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
+primrec fast_bv_to_nat_helper :: "[bit list, int] => int" where
+    fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
+  | fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
+      fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
 
 declare fast_bv_to_nat_helper.simps [code del]
 
 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
     fast_bv_to_nat_helper bs (Int.Bit0 bin)"