# HG changeset patch
# User kuncar
# Date 1397144913 -7200
# Node ID 58ac520db7aef40b1c350164b8921b5254c5678e
# Parent  b5b6ad5dc2aea0cfbdc9b511a42dc8df789d6f87
add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons

diff -r b5b6ad5dc2ae -r 58ac520db7ae src/HOL/Lifting_Product.thy
--- a/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:32 2014 +0200
+++ b/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:33 2014 +0200
@@ -8,6 +8,11 @@
 imports Lifting Basic_BNFs
 begin
 
+(* The following lemma can be deleted when product is added to FP sugar *)
+lemma prod_pred_inject [simp]:
+  "pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)"
+  unfolding pred_prod_def fun_eq_iff prod_set_simps by blast
+
 subsection {* Transfer rules for the Transfer package *}
 
 context
diff -r b5b6ad5dc2ae -r 58ac520db7ae src/HOL/Lifting_Sum.thy
--- a/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:32 2014 +0200
+++ b/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:33 2014 +0200
@@ -8,6 +8,11 @@
 imports Lifting Basic_BNFs
 begin
 
+(* The following lemma can be deleted when sum is added to FP sugar *)
+lemma sum_pred_inject [simp]:
+  "pred_sum P1 P2 (Inl a) = P1 a" and "pred_sum P1 P2 (Inr a) = P2 a"
+  unfolding pred_sum_def fun_eq_iff sum_set_simps by auto
+
 subsection {* Transfer rules for the Transfer package *}
 
 context