author  haftmann 
Tue, 21 Dec 2010 17:52:23 +0100  
changeset 41372  551eb49a6e91 
parent 40820  fd9c98ead9a9 
child 45802  b16f976db515 
permissions  rwrr 
35788  1 
(* Title: HOL/Library/Quotient_Sum.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 sum type *} 

6 

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

7 
theory Quotient_Sum 
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 

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

11 
fun 
40542
9a173a22771c
regeneralized type of option_rel and sum_rel (accident from 2989f9f3aa10)
haftmann
parents:
40465
diff
changeset

12 
sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + '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 
"sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

15 
 "sum_rel R1 R2 (Inl a1) (Inr b2) = False" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

16 
 "sum_rel R1 R2 (Inr a2) (Inl b1) = False" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

17 
 "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

18 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
35788
diff
changeset

19 
declare [[map sum = (sum_map, sum_rel)]] 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

20 

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

21 
lemma sum_rel_unfold: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

22 
"sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

23 
 (Inr x, Inr y) \<Rightarrow> R2 x y 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

24 
 _ \<Rightarrow> False)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

25 
by (cases x) (cases y, simp_all)+ 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

26 

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

27 
lemma sum_rel_map1: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

28 
"sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

29 
by (simp add: sum_rel_unfold split: sum.split) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

30 

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

31 
lemma sum_rel_map2: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

32 
"sum_rel R1 R2 x (sum_map f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

33 
by (simp add: sum_rel_unfold split: sum.split) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

34 

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

35 
lemma sum_map_id [id_simps]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

36 
"sum_map id id = id" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

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

38 

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

39 
lemma sum_rel_eq [id_simps]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

40 
"sum_rel (op =) (op =) = (op =)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

41 
by (simp add: sum_rel_unfold fun_eq_iff split: sum.split) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

42 

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

43 
lemma sum_reflp: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

44 
"reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

45 
by (auto simp add: sum_rel_unfold split: sum.splits intro!: reflpI elim: reflpE) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

46 

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

47 
lemma sum_symp: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

48 
"symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

49 
by (auto simp add: sum_rel_unfold split: sum.splits intro!: sympI elim: sympE) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

50 

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

51 
lemma sum_transp: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

52 
"transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

53 
by (auto simp add: sum_rel_unfold split: sum.splits intro!: transpI elim: transpE) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

54 

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

55 
lemma sum_equivp [quot_equiv]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

56 
"equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

57 
by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

58 

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

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

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

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

62 
shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

63 
apply (rule QuotientI) 
41372  64 
apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

65 
Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2]) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

66 
using Quotient_rel [OF q1] Quotient_rel [OF q2] 
41372  67 
apply (simp add: sum_rel_unfold comp_def split: sum.split) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

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

69 

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

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

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

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

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

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

75 

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

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

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

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

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

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

81 

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

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

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

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

85 
shows "(Rep1 > sum_map Abs1 Abs2) Inl = Inl" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

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

88 
done 
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:
40610
diff
changeset

90 
lemma sum_Inr_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 
assumes q2: "Quotient R2 Abs2 Rep2" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

93 
shows "(Rep2 > sum_map Abs1 Abs2) Inr = Inr" 
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 
apply(simp add: fun_eq_iff) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

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

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

97 

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

98 
end 