summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | kuncar |

Thu, 10 Apr 2014 17:48:33 +0200 | |

changeset 56526 | 58ac520db7ae |

parent 56525 | b5b6ad5dc2ae |

child 56527 | 907f04603177 |

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

src/HOL/Lifting_Product.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Lifting_Sum.thy | file | annotate | diff | comparison | revisions |

--- 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

--- 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