author  blanchet 
Mon, 20 Jan 2014 21:32:41 +0100  
changeset 55085  0e8e4dc55866 
parent 55083  0a689157e3ce 
child 55414  eab03e9cee8a 
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 

55085
0e8e4dc55866
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
55083
diff
changeset

20 
lemmas prod_rel_eq[relator_eq] = prod.rel_eq 
0e8e4dc55866
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
55083
diff
changeset

21 
lemmas prod_rel_mono[relator_mono] = prod.rel_mono 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

22 

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

23 
lemma prod_rel_OO[relator_distr]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

24 
"(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

25 
by (rule ext)+ (auto simp: prod_rel_def OO_def) 
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" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

30 
shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

31 
using assms unfolding prod_rel_def prod_pred_def by blast 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

32 

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

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

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

35 
assumes "reflp R2" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

36 
shows "reflp (prod_rel R1 R2)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

37 
using assms by (auto intro!: reflpI elim: reflpE) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

38 

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

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

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

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

42 
shows "left_total (prod_rel R1 R2)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

44 

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

45 
lemma left_unique_prod_rel [reflexivity_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

46 
assumes "left_unique R1" and "left_unique R2" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

47 
shows "left_unique (prod_rel R1 R2)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

49 

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

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

51 
assumes "right_total R1" and "right_total R2" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

52 
shows "right_total (prod_rel R1 R2)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

54 

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

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

56 
assumes "right_unique R1" and "right_unique R2" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

57 
shows "right_unique (prod_rel R1 R2)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

59 

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

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

61 
assumes "bi_total R1" and "bi_total R2" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

62 
shows "bi_total (prod_rel R1 R2)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

64 

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

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

66 
assumes "bi_unique R1" and "bi_unique R2" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

67 
shows "bi_unique (prod_rel R1 R2)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

68 
using assms unfolding bi_unique_def prod_rel_def by auto 
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 prod_invariant_commute [invariant_commute]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

71 
"prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

72 
by (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) blast 
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 {* Quotient theorem for the Lifting 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 
lemma Quotient_prod[quot_map]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

78 
assumes "Quotient R2 Abs2 Rep2 T2" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

79 
shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

80 
(map_pair Rep1 Rep2) (prod_rel T1 T2)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

82 

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

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

84 

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

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

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

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

88 

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

89 
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

90 
unfolding fun_rel_def prod_rel_def by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

91 

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

92 
lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

93 
unfolding fun_rel_def prod_rel_def by simp 
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 snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

96 
unfolding fun_rel_def prod_rel_def by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

97 

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

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

99 
"((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

100 
unfolding fun_rel_def prod_rel_def by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

101 

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

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

103 
"((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

105 

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

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

107 
"((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

109 
unfolding map_pair_def [abs_def] by transfer_prover 
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 
lemma prod_rel_transfer [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

113 
prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

114 
unfolding fun_rel_def by auto 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

115 

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

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

117 

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

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

119 