author  kuncar 
Fri, 20 Apr 2012 18:29:21 +0200  
changeset 47634  091bcd569441 
parent 47624  16d433895d2e 
child 47635  ebb79474262c 
permissions  rwrr 
47455  1 
(* Title: HOL/Library/Quotient_Sum.thy 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

2 
Author: Cezary Kaliszyk, Christian Urban and Brian Huffman 
35222
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 

47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

11 
subsection {* Relator for sum type *} 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

12 

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

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

14 
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

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

16 
"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

17 
 "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

18 
 "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

19 
 "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

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 

47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

39 
lemma sum_rel_eq [id_simps, relator_eq]: 
40820
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 

47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

43 
lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

44 
by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

45 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

46 
lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

47 
by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

48 

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

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

50 
"reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)" 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

51 
unfolding reflp_def split_sum_all sum_rel.simps by fast 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

52 

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

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

54 
"symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)" 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

55 
unfolding symp_def split_sum_all sum_rel.simps by fast 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

56 

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

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

58 
"transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)" 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

59 
unfolding transp_def split_sum_all sum_rel.simps by fast 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

60 

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

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

62 
"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

63 
by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE) 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

64 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

65 
lemma right_total_sum_rel [transfer_rule]: 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

66 
"right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

67 
unfolding right_total_def split_sum_all split_sum_ex by simp 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

68 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

69 
lemma right_unique_sum_rel [transfer_rule]: 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

70 
"right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (sum_rel R1 R2)" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

71 
unfolding right_unique_def split_sum_all by simp 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

72 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

73 
lemma bi_total_sum_rel [transfer_rule]: 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

74 
"bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (sum_rel R1 R2)" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

75 
using assms unfolding bi_total_def split_sum_all split_sum_ex by simp 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

76 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

77 
lemma bi_unique_sum_rel [transfer_rule]: 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

78 
"bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

79 
using assms unfolding bi_unique_def split_sum_all by simp 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

80 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

81 
subsection {* Correspondence rules for transfer package *} 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

82 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

83 
lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

84 
unfolding fun_rel_def by simp 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

85 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

86 
lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

87 
unfolding fun_rel_def by simp 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

88 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

89 
lemma sum_case_transfer [transfer_rule]: 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

90 
"((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

91 
unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split) 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

92 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

93 
subsection {* Setup for lifting package *} 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

94 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

95 
lemma Quotient_sum: 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

96 
assumes "Quotient R1 Abs1 Rep1 T1" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

97 
assumes "Quotient R2 Abs2 Rep2 T2" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

98 
shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

99 
(sum_map Rep1 Rep2) (sum_rel T1 T2)" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

100 
using assms unfolding Quotient_alt_def 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

101 
by (simp add: split_sum_all) 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

102 

16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

103 
declare [[map sum = (sum_rel, Quotient_sum)]] 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

104 

47634
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

105 
fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool" 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

106 
where 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

107 
"sum_pred R1 R2 (Inl a) = R1 a" 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

108 
 "sum_pred R1 R2 (Inr a) = R2 a" 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

109 

091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

110 
lemma sum_invariant_commute [invariant_commute]: 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

111 
"sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)" 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

112 
apply (simp add: fun_eq_iff Lifting.invariant_def) 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

113 
apply (intro allI) 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

114 
apply (case_tac x rule: sum.exhaust) 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

115 
apply (case_tac xa rule: sum.exhaust) 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

116 
apply auto[2] 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

117 
apply (case_tac xa rule: sum.exhaust) 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

118 
apply auto 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

119 
done 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

120 

47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

121 
subsection {* Rules for quotient package *} 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

122 

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

123 
lemma sum_quotient [quot_thm]: 
47308  124 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
125 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

126 
shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" 

127 
apply (rule Quotient3I) 

41372  128 
apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2 
47308  129 
Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2]) 
130 
using Quotient3_rel [OF q1] Quotient3_rel [OF q2] 

41372  131 
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

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

133 

47308  134 
declare [[mapQ3 sum = (sum_rel, sum_quotient)]] 
47094  135 

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

136 
lemma sum_Inl_rsp [quot_respect]: 
47308  137 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
138 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

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

139 
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

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

141 

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

142 
lemma sum_Inr_rsp [quot_respect]: 
47308  143 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
144 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

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

145 
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

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

147 

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

148 
lemma sum_Inl_prs [quot_preserve]: 
47308  149 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
150 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

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

151 
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

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

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

155 

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

156 
lemma sum_Inr_prs [quot_preserve]: 
47308  157 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
158 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

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

159 
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

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

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

163 

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

164 
end 