summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Lifting_Sum.thy

author | kuncar |

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

changeset 56526 | 58ac520db7ae |

parent 56525 | b5b6ad5dc2ae |

child 58889 | 5b7a9633cfa8 |

permissions | -rw-r--r-- |

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

(* Title: HOL/Lifting_Sum.thy Author: Brian Huffman and Ondrej Kuncar *) header {* Setup for Lifting/Transfer for the sum type *} theory Lifting_Sum 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 begin interpretation lifting_syntax . lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl" unfolding rel_fun_def by simp lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr" unfolding rel_fun_def by simp lemma case_sum_transfer [transfer_rule]: "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum" unfolding rel_fun_def rel_sum_def by (simp split: sum.split) end end