equal
deleted
inserted
replaced
5 header {* Setup for Lifting/Transfer for the product type *} |
5 header {* Setup for Lifting/Transfer for the product type *} |
6 |
6 |
7 theory Lifting_Product |
7 theory Lifting_Product |
8 imports Lifting Basic_BNFs |
8 imports Lifting Basic_BNFs |
9 begin |
9 begin |
|
10 |
|
11 (* The following lemma can be deleted when product is added to FP sugar *) |
|
12 lemma prod_pred_inject [simp]: |
|
13 "pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)" |
|
14 unfolding pred_prod_def fun_eq_iff prod_set_simps by blast |
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 |