congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj

--- a/src/HOL/HOL.thy	Thu Aug 22 17:19:51 2013 +0200
+++ b/src/HOL/HOL.thy	Thu Aug 22 21:15:43 2013 +0200
@@ -1695,12 +1695,22 @@
 
 subsubsection {* Generic code generator preprocessor setup *}
 
+lemma conj_left_cong:
+  "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
+  by (fact arg_cong)
+
+lemma disj_left_cong:
+  "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
+  by (fact arg_cong)
+
 setup {*
   Code_Preproc.map_pre (put_simpset HOL_basic_ss)
   #> Code_Preproc.map_post (put_simpset HOL_basic_ss)
-  #> Code_Simp.map_ss (put_simpset HOL_basic_ss)
+  #> Code_Simp.map_ss (put_simpset HOL_basic_ss
+    #> Simplifier.add_cong @{thm conj_left_cong} #> Simplifier.add_cong @{thm disj_left_cong})
 *}
 
+
 subsubsection {* Equality *}
 
 class equal =