author | kuncar |
Thu, 10 Apr 2014 17:48:33 +0200 | |
changeset 57868 | 58ac520db7ae |
parent 57867 | b5b6ad5dc2ae |
permissions | -rw-r--r-- |
kuncar@54149 | 1 |
(* Title: HOL/Lifting_Sum.thy |
kuncar@54149 | 2 |
Author: Brian Huffman and Ondrej Kuncar |
kuncar@54149 | 3 |
*) |
kuncar@54149 | 4 |
|
kuncar@54149 | 5 |
header {* Setup for Lifting/Transfer for the sum type *} |
kuncar@54149 | 6 |
|
kuncar@54149 | 7 |
theory Lifting_Sum |
blanchet@56425 | 8 |
imports Lifting Basic_BNFs |
kuncar@54149 | 9 |
begin |
kuncar@54149 | 10 |
|
kuncar@57868 | 11 |
(* The following lemma can be deleted when sum is added to FP sugar *) |
kuncar@57868 | 12 |
lemma sum_pred_inject [simp]: |
kuncar@57868 | 13 |
"pred_sum P1 P2 (Inl a) = P1 a" and "pred_sum P1 P2 (Inr a) = P2 a" |
kuncar@57868 | 14 |
unfolding pred_sum_def fun_eq_iff sum_set_simps by auto |
kuncar@57868 | 15 |
|
kuncar@54149 | 16 |
subsection {* Transfer rules for the Transfer package *} |
kuncar@54149 | 17 |
|
kuncar@54149 | 18 |
context |
kuncar@54149 | 19 |
begin |
kuncar@54149 | 20 |
interpretation lifting_syntax . |
kuncar@54149 | 21 |
|
blanchet@57285 | 22 |
lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl" |
blanchet@57287 | 23 |
unfolding rel_fun_def by simp |
kuncar@54149 | 24 |
|
blanchet@57285 | 25 |
lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr" |
blanchet@57287 | 26 |
unfolding rel_fun_def by simp |
kuncar@54149 | 27 |
|
blanchet@56756 | 28 |
lemma case_sum_transfer [transfer_rule]: |
blanchet@57285 | 29 |
"((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum" |
blanchet@57287 | 30 |
unfolding rel_fun_def rel_sum_def by (simp split: sum.split) |
kuncar@54149 | 31 |
|
kuncar@54149 | 32 |
end |
kuncar@54149 | 33 |
|
kuncar@54149 | 34 |
end |