# HG changeset patch
# User huffman
# Date 1324650858 -3600
# Node ID ae70b6830f1517c55eca43f7b21c8db9c61b3b9d
# Parent  fc303e8f5c2067a8c70bc057fc419464e298e6d9
add lemmas bin_cat_zero and bin_split_zero

diff -r fc303e8f5c20 -r ae70b6830f15 src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Fri Dec 23 15:24:22 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Fri Dec 23 15:34:18 2011 +0100
@@ -535,8 +535,11 @@
   apply (case_tac m, auto)
   done
 
+lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
+  by (induct n arbitrary: w) (auto simp: Int.Pls_def)
+
 lemma bin_cat_Pls [simp]: "bin_cat Int.Pls n w = bintrunc n w"
-  by (induct n arbitrary: w) auto
+  unfolding Pls_def by (rule bin_cat_zero)
 
 lemma bintr_cat1: 
   "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
@@ -566,9 +569,12 @@
   "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
   by (induct n arbitrary: w) auto
 
+lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
+  by (induct n) (auto simp: Int.Pls_def)
+
 lemma bin_split_Pls [simp]:
   "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
-  by (induct n) (auto simp: Let_def BIT_simps split: ls_splits)
+  unfolding Pls_def by (rule bin_split_zero)
 
 lemma bin_split_Min [simp]:
   "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)"