# HG changeset patch
# User huffman
# Date 1187793875 -7200
# Node ID 371f8c6b2101980a41e3228ad7bb7e2de86d8b2e
# Parent  8d83b1e7c3dd75cea2d6357503b4793ced6f8bbb
move if_simps from BinBoolList to Num_Lemmas

diff -r 8d83b1e7c3dd -r 371f8c6b2101 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Wed Aug 22 12:21:17 2007 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Wed Aug 22 16:44:35 2007 +0200
@@ -961,12 +961,6 @@
 lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)"
   by auto
 
-lemma if_Not_x: "(if p then ~ x else x) = (p = (~ x))"
-  by auto
-
-lemma if_x_Not: "(if p then x else ~ x) = (p = x)"
-  by auto
-
 lemma if_same_and: "(If p x y & If p u v) = (if p then x & u else y & v)"
   by auto
 
@@ -986,13 +980,6 @@
   "(if xc then [xab] else [an]) = [if xc then xab else an]"
   by auto
 
-lemma if_bool_simps:
-  "If p True y = (p | y) & If p False y = (~p & y) & 
-    If p y True = (p --> y) & If p y False = (p & y)"
-  by auto
-
-lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
-
 lemmas seqr = eq_reflection [where x = "size ?w"]
 
 lemmas tl_Nil = tl.simps (1)
diff -r 8d83b1e7c3dd -r 371f8c6b2101 src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Wed Aug 22 12:21:17 2007 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy	Wed Aug 22 16:44:35 2007 +0200
@@ -522,4 +522,19 @@
   apply (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])
   done
 
+subsection "if simps"
+
+lemma if_Not_x: "(if p then ~ x else x) = (p = (~ x))"
+  by auto
+
+lemma if_x_Not: "(if p then x else ~ x) = (p = x)"
+  by auto
+
+lemma if_bool_simps:
+  "If p True y = (p | y) & If p False y = (~p & y) & 
+    If p y True = (p --> y) & If p y False = (p & y)"
+  by auto
+
+lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
+
 end