author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 58448 | a1d4e7473c98 |
permissions | -rw-r--r-- |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
1 |
(* Title: HOL/Lifting_Product.thy |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
2 |
Author: Brian Huffman and Ondrej Kuncar |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
3 |
*) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
4 |
|
58889 | 5 |
section {* Setup for Lifting/Transfer for the product type *} |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
6 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
7 |
theory Lifting_Product |
55083 | 8 |
imports Lifting Basic_BNFs |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
9 |
begin |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
10 |
|
56526
58ac520db7ae
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
kuncar
parents:
56525
diff
changeset
|
11 |
(* The following lemma can be deleted when product is added to FP sugar *) |
58ac520db7ae
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
kuncar
parents:
56525
diff
changeset
|
12 |
lemma prod_pred_inject [simp]: |
58ac520db7ae
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
kuncar
parents:
56525
diff
changeset
|
13 |
"pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)" |
58ac520db7ae
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
kuncar
parents:
56525
diff
changeset
|
14 |
unfolding pred_prod_def fun_eq_iff prod_set_simps by blast |
58ac520db7ae
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
kuncar
parents:
56525
diff
changeset
|
15 |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
16 |
subsection {* Transfer rules for the Transfer package *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
17 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
18 |
context |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
19 |
begin |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
20 |
interpretation lifting_syntax . |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
21 |
|
58448 | 22 |
declare Pair_transfer [transfer_rule] |
58444 | 23 |
declare fst_transfer [transfer_rule] |
24 |
declare snd_transfer [transfer_rule] |
|
58446 | 25 |
declare case_prod_transfer [transfer_rule] |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
26 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
27 |
lemma curry_transfer [transfer_rule]: |
55944 | 28 |
"((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
29 |
unfolding curry_def by transfer_prover |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
30 |
|
55932 | 31 |
lemma map_prod_transfer [transfer_rule]: |
55944 | 32 |
"((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D) |
55932 | 33 |
map_prod map_prod" |
34 |
unfolding map_prod_def [abs_def] by transfer_prover |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
35 |
|
55944 | 36 |
lemma rel_prod_transfer [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
37 |
"((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> |
55944 | 38 |
rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod" |
55945 | 39 |
unfolding rel_fun_def by auto |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
40 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
41 |
end |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
42 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
43 |
end |