author  kuncar 
Thu, 10 Apr 2014 17:48:15 +0200  
changeset 56520  3373f5d1e074 
parent 56519  c1048f5bbb45 
child 56525  b5b6ad5dc2ae 
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 

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

11 
subsection {* Relator and predicator properties *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

12 

56092
1ba075db8fe4
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
blanchet
parents:
55945
diff
changeset

13 
definition pred_prod :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" 
1ba075db8fe4
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
blanchet
parents:
55945
diff
changeset

14 
where "pred_prod R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)" 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

15 

56092
1ba075db8fe4
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
blanchet
parents:
55945
diff
changeset

16 
lemma pred_prod_apply [simp]: 
1ba075db8fe4
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
blanchet
parents:
55945
diff
changeset

17 
"pred_prod P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b" 
1ba075db8fe4
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
blanchet
parents:
55945
diff
changeset

18 
by (simp add: pred_prod_def) 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

19 

55944  20 
lemmas rel_prod_eq[relator_eq] = prod.rel_eq 
21 
lemmas rel_prod_mono[relator_mono] = prod.rel_mono 

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

22 

55944  23 
lemma rel_prod_OO[relator_distr]: 
24 
"(rel_prod A B) OO (rel_prod C D) = rel_prod (A OO C) (B OO D)" 

25 
by (rule ext)+ (auto simp: rel_prod_def OO_def) 

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

26 

56520
3373f5d1e074
abstract Domainp in relator_domain rules => more natural statement of the rule
kuncar
parents:
56519
diff
changeset

27 
lemma Domainp_prod[relator_domain]: 
3373f5d1e074
abstract Domainp in relator_domain rules => more natural statement of the rule
kuncar
parents:
56519
diff
changeset

28 
"Domainp (rel_prod T1 T2) = (pred_prod (Domainp T1) (Domainp T2))" 
3373f5d1e074
abstract Domainp in relator_domain rules => more natural statement of the rule
kuncar
parents:
56519
diff
changeset

29 
unfolding rel_prod_def pred_prod_def by blast 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

30 

56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56092
diff
changeset

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

32 
assumes "left_total R1" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

33 
assumes "left_total R2" 
55944  34 
shows "left_total (rel_prod R1 R2)" 
35 
using assms unfolding left_total_def rel_prod_def by auto 

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

36 

56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56092
diff
changeset

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

38 
assumes "left_unique R1" and "left_unique R2" 
55944  39 
shows "left_unique (rel_prod R1 R2)" 
40 
using assms unfolding left_unique_def rel_prod_def by auto 

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

41 

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

43 
assumes "right_total R1" and "right_total R2" 
55944  44 
shows "right_total (rel_prod R1 R2)" 
45 
using assms unfolding right_total_def rel_prod_def by auto 

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

46 

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

48 
assumes "right_unique R1" and "right_unique R2" 
55944  49 
shows "right_unique (rel_prod R1 R2)" 
50 
using assms unfolding right_unique_def rel_prod_def by auto 

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

51 

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

53 
assumes "bi_total R1" and "bi_total R2" 
55944  54 
shows "bi_total (rel_prod R1 R2)" 
55 
using assms unfolding bi_total_def rel_prod_def by auto 

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

56 

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

58 
assumes "bi_unique R1" and "bi_unique R2" 
55944  59 
shows "bi_unique (rel_prod R1 R2)" 
60 
using assms unfolding bi_unique_def rel_prod_def by auto 

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

61 

56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

62 
lemma prod_relator_eq_onp [relator_eq_onp]: 
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

63 
"rel_prod (eq_onp P1) (eq_onp P2) = eq_onp (pred_prod P1 P2)" 
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

64 
by (simp add: fun_eq_iff rel_prod_def pred_prod_def eq_onp_def) blast 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

65 

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

66 
subsection {* Quotient theorem for the Lifting package *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

67 

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

68 
lemma Quotient_prod[quot_map]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

69 
assumes "Quotient R1 Abs1 Rep1 T1" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

70 
assumes "Quotient R2 Abs2 Rep2 T2" 
55944  71 
shows "Quotient (rel_prod R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2) (rel_prod T1 T2)" 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

72 
using assms unfolding Quotient_alt_def by auto 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

73 

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

74 
subsection {* Transfer rules for the Transfer package *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

75 

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

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

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

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

79 

55944  80 
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair" 
55945  81 
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

82 

55944  83 
lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst" 
55945  84 
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

85 

55944  86 
lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd" 
55945  87 
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

88 

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

89 
lemma case_prod_transfer [transfer_rule]: 
55944  90 
"((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod" 
55945  91 
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

92 

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

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

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

96 

55932  97 
lemma map_prod_transfer [transfer_rule]: 
55944  98 
"((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D) 
55932  99 
map_prod map_prod" 
100 
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

101 

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

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

106 

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

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

108 

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

109 
end 