author  kuncar 
Fri, 09 Dec 2011 18:07:04 +0100  
changeset 45802  b16f976db515 
parent 41372  551eb49a6e91 
child 47094  1a7ad2601cb5 
permissions  rwrr 
35788  1 
(* Title: HOL/Library/Quotient_Product.thy 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

2 
Author: Cezary Kaliszyk and Christian Urban 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

3 
*) 
35788  4 

5 
header {* Quotient infrastructure for the product type *} 

6 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

7 
theory Quotient_Product 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

8 
imports Main Quotient_Syntax 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

9 
begin 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

10 

40465
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

11 
definition 
40541
7850b4cc1507
regeneralized type of prod_rel (accident from 2989f9f3aa10)
haftmann
parents:
40465
diff
changeset

12 
prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

13 
where 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

14 
"prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

15 

45802  16 
declare [[map prod = prod_rel]] 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

17 

40465
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

18 
lemma prod_rel_apply [simp]: 
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

19 
"prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d" 
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

20 
by (simp add: prod_rel_def) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

21 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

22 
lemma map_pair_id [id_simps]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

23 
shows "map_pair id id = id" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

24 
by (simp add: fun_eq_iff) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

25 

fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

26 
lemma prod_rel_eq [id_simps]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

27 
shows "prod_rel (op =) (op =) = (op =)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

28 
by (simp add: fun_eq_iff) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

29 

fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

30 
lemma prod_equivp [quot_equiv]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

31 
assumes "equivp R1" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

32 
assumes "equivp R2" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

33 
shows "equivp (prod_rel R1 R2)" 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

34 
using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

35 

fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

36 
lemma prod_quotient [quot_thm]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

37 
assumes "Quotient R1 Abs1 Rep1" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

38 
assumes "Quotient R2 Abs2 Rep2" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

39 
shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

40 
apply (rule QuotientI) 
41372  41 
apply (simp add: map_pair.compositionality comp_def map_pair.identity 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

42 
Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)]) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

43 
apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)]) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

44 
using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)] 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

45 
apply (auto simp add: split_paired_all) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

46 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

47 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

48 
lemma Pair_rsp [quot_respect]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

49 
assumes q1: "Quotient R1 Abs1 Rep1" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

50 
assumes q2: "Quotient R2 Abs2 Rep2" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

51 
shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" 
40465
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

52 
by (auto simp add: prod_rel_def) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

53 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

54 
lemma Pair_prs [quot_preserve]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

55 
assumes q1: "Quotient R1 Abs1 Rep1" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

56 
assumes q2: "Quotient R2 Abs2 Rep2" 
40607  57 
shows "(Rep1 > Rep2 > (map_pair Abs1 Abs2)) Pair = Pair" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

58 
apply(simp add: fun_eq_iff) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

59 
apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

60 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

61 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

62 
lemma fst_rsp [quot_respect]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

63 
assumes "Quotient R1 Abs1 Rep1" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

64 
assumes "Quotient R2 Abs2 Rep2" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

65 
shows "(prod_rel R1 R2 ===> R1) fst fst" 
40465
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

66 
by auto 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

67 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

68 
lemma fst_prs [quot_preserve]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

69 
assumes q1: "Quotient R1 Abs1 Rep1" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

70 
assumes q2: "Quotient R2 Abs2 Rep2" 
40607  71 
shows "(map_pair Rep1 Rep2 > Abs1) fst = fst" 
40465
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

72 
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1]) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

73 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

74 
lemma snd_rsp [quot_respect]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

75 
assumes "Quotient R1 Abs1 Rep1" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

76 
assumes "Quotient R2 Abs2 Rep2" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

77 
shows "(prod_rel R1 R2 ===> R2) snd snd" 
40465
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

78 
by auto 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

79 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

80 
lemma snd_prs [quot_preserve]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

81 
assumes q1: "Quotient R1 Abs1 Rep1" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

82 
assumes q2: "Quotient R2 Abs2 Rep2" 
40607  83 
shows "(map_pair Rep1 Rep2 > Abs2) snd = snd" 
40465
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

84 
by (simp add: fun_eq_iff Quotient_abs_rep[OF q2]) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

85 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

86 
lemma split_rsp [quot_respect]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

87 
shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" 
40465
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

88 
by (auto intro!: fun_relI elim!: fun_relE) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

89 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40607
diff
changeset

90 
lemma split_prs [quot_preserve]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

91 
assumes q1: "Quotient R1 Abs1 Rep1" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

92 
and q2: "Quotient R2 Abs2 Rep2" 
40607  93 
shows "(((Abs1 > Abs2 > id) > map_pair Rep1 Rep2 > id) split) = split" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

94 
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

95 

36695
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

96 
lemma [quot_respect]: 
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

97 
shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> 
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

98 
prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel" 
40465
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

99 
by (auto simp add: fun_rel_def) 
36695
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

100 

b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

101 
lemma [quot_preserve]: 
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

102 
assumes q1: "Quotient R1 abs1 rep1" 
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

103 
and q2: "Quotient R2 abs2 rep2" 
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

104 
shows "((abs1 > abs1 > id) > (abs2 > abs2 > id) > 
40607  105 
map_pair rep1 rep2 > map_pair rep1 rep2 > id) prod_rel = prod_rel" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

106 
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) 
36695
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

107 

b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

108 
lemma [quot_preserve]: 
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

109 
shows"(prod_rel ((rep1 > rep1 > id) R1) ((rep2 > rep2 > id) R2) 
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

110 
(l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))" 
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

111 
by simp 
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

112 

b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

113 
declare Pair_eq[quot_preserve] 
b434506fb0d4
respectfullness and preservation of prod_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35788
diff
changeset

114 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

115 
end 