# HG changeset patch
# User haftmann
# Date 1377198943 -7200
# Node ID 3a93bc5d33707809d928c3e39da8a5ba4946f570
# Parent  2fb458aceb78261de55e4f108102cf473f91875d
congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj

diff -r 2fb458aceb78 -r 3a93bc5d3370 src/HOL/HOL.thy
--- 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 =