author  kuncar 
Thu, 10 Apr 2014 17:48:33 +0200  
changeset 56526  58ac520db7ae 
parent 56525  b5b6ad5dc2ae 
child 58444  ed95293f14b6 
permissions  rwrr 
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 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

5 
header {* Setup for Lifting/Transfer for the product type *} 
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 

55944  22 
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair" 
55945  23 
unfolding rel_fun_def rel_prod_def by simp 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

24 

55944  25 
lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst" 
55945  26 
unfolding rel_fun_def rel_prod_def by simp 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

27 

55944  28 
lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd" 
55945  29 
unfolding rel_fun_def rel_prod_def by simp 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

30 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55085
diff
changeset

31 
lemma case_prod_transfer [transfer_rule]: 
55944  32 
"((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod" 
55945  33 
unfolding rel_fun_def rel_prod_def by simp 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

34 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

35 
lemma curry_transfer [transfer_rule]: 
55944  36 
"((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

37 
unfolding curry_def by transfer_prover 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

38 

55932  39 
lemma map_prod_transfer [transfer_rule]: 
55944  40 
"((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D) 
55932  41 
map_prod map_prod" 
42 
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

43 

55944  44 
lemma rel_prod_transfer [transfer_rule]: 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

45 
"((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> 
55944  46 
rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod" 
55945  47 
unfolding rel_fun_def by auto 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

48 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

49 
end 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

50 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

51 
end 