# HG changeset patch
# User haftmann
# Date 1391094543 -3600
# Node ID 6d0d93316daf9b0e07b9b00c73d64bbcdd07e770
# Parent  fafdf2424c57abdc2dadad8ca4362632e030c6c9
split rules for of_bool, similar to if

diff -r fafdf2424c57 -r 6d0d93316daf src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu Jan 30 17:34:42 2014 +0100
+++ b/src/HOL/Rings.thy	Thu Jan 30 16:09:03 2014 +0100
@@ -99,6 +99,14 @@
   "of_bool p = of_bool q \<longleftrightarrow> p = q"
   by (simp add: of_bool_def)
 
+lemma split_of_bool [split]:
+  "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"
+  by (cases p) simp_all
+
+lemma split_of_bool_asm:
+  "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
+  by (cases p) simp_all
+  
 end  
 
 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult