equal
deleted
inserted
replaced
1 (* Title: HOL/Lifting_Product.thy |
|
2 Author: Brian Huffman and Ondrej Kuncar |
|
3 *) |
|
4 |
|
5 section {* Setup for Lifting/Transfer for the product type *} |
|
6 |
|
7 theory Lifting_Product |
|
8 imports Lifting Basic_BNFs |
|
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 |
|
15 |
|
16 subsection {* Transfer rules for the Transfer package *} |
|
17 |
|
18 context |
|
19 begin |
|
20 interpretation lifting_syntax . |
|
21 |
|
22 declare Pair_transfer [transfer_rule] |
|
23 declare fst_transfer [transfer_rule] |
|
24 declare snd_transfer [transfer_rule] |
|
25 declare case_prod_transfer [transfer_rule] |
|
26 |
|
27 lemma curry_transfer [transfer_rule]: |
|
28 "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry" |
|
29 unfolding curry_def by transfer_prover |
|
30 |
|
31 lemma map_prod_transfer [transfer_rule]: |
|
32 "((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D) |
|
33 map_prod map_prod" |
|
34 unfolding map_prod_def [abs_def] by transfer_prover |
|
35 |
|
36 lemma rel_prod_transfer [transfer_rule]: |
|
37 "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> |
|
38 rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod" |
|
39 unfolding rel_fun_def by auto |
|
40 |
|
41 end |
|
42 |
|
43 end |
|