equal
deleted
inserted
replaced
5 header {* Setup for Lifting/Transfer for the sum type *} |
5 header {* Setup for Lifting/Transfer for the sum type *} |
6 |
6 |
7 theory Lifting_Sum |
7 theory Lifting_Sum |
8 imports Lifting Basic_BNFs |
8 imports Lifting Basic_BNFs |
9 begin |
9 begin |
|
10 |
|
11 (* The following lemma can be deleted when sum is added to FP sugar *) |
|
12 lemma sum_pred_inject [simp]: |
|
13 "pred_sum P1 P2 (Inl a) = P1 a" and "pred_sum P1 P2 (Inr a) = P2 a" |
|
14 unfolding pred_sum_def fun_eq_iff sum_set_simps by auto |
10 |
15 |
11 subsection {* Transfer rules for the Transfer package *} |
16 subsection {* Transfer rules for the Transfer package *} |
12 |
17 |
13 context |
18 context |
14 begin |
19 begin |