author  blanchet 
Thu, 06 Mar 2014 15:29:18 +0100  
changeset 55944  7ab8f003fe41 
parent 55932  68c5104d2204 
child 55945  e96383acecf9 
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 

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

13 
definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

15 

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

16 
lemma prod_pred_apply [simp]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

17 
"prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

18 
by (simp add: prod_pred_def) 
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 

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

27 
lemma Domainp_prod[relator_domain]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

28 
assumes "Domainp T1 = P1" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

29 
assumes "Domainp T2 = P2" 
55944  30 
shows "Domainp (rel_prod T1 T2) = (prod_pred P1 P2)" 
31 
using assms unfolding rel_prod_def prod_pred_def by blast 

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

32 

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

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

35 
assumes "left_total R2" 
55944  36 
shows "left_total (rel_prod R1 R2)" 
37 
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

38 

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

40 
assumes "left_unique R1" and "left_unique R2" 
55944  41 
shows "left_unique (rel_prod R1 R2)" 
42 
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

43 

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

45 
assumes "right_total R1" and "right_total R2" 
55944  46 
shows "right_total (rel_prod R1 R2)" 
47 
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

48 

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

50 
assumes "right_unique R1" and "right_unique R2" 
55944  51 
shows "right_unique (rel_prod R1 R2)" 
52 
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

53 

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

55 
assumes "bi_total R1" and "bi_total R2" 
55944  56 
shows "bi_total (rel_prod R1 R2)" 
57 
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

58 

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

60 
assumes "bi_unique R1" and "bi_unique R2" 
55944  61 
shows "bi_unique (rel_prod R1 R2)" 
62 
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

63 

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

64 
lemma prod_invariant_commute [invariant_commute]: 
55944  65 
"rel_prod (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)" 
66 
by (simp add: fun_eq_iff rel_prod_def prod_pred_def Lifting.invariant_def) blast 

53012
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 
subsection {* Quotient theorem for the Lifting package *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

69 

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

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

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

72 
assumes "Quotient R2 Abs2 Rep2 T2" 
55944  73 
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

74 
using assms unfolding Quotient_alt_def by auto 
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 
subsection {* Transfer rules for the Transfer package *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

77 

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

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

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

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

81 

55944  82 
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair" 
83 
unfolding fun_rel_def rel_prod_def by simp 

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

84 

55944  85 
lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst" 
86 
unfolding fun_rel_def rel_prod_def by simp 

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

87 

55944  88 
lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd" 
89 
unfolding fun_rel_def rel_prod_def by simp 

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

90 

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

91 
lemma case_prod_transfer [transfer_rule]: 
55944  92 
"((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod" 
93 
unfolding fun_rel_def rel_prod_def by simp 

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

94 

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

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

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

98 

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

103 

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

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

107 
unfolding fun_rel_def by auto 
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 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

110 

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

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

112 