author  kuncar 
Thu, 24 May 2012 14:20:23 +0200  
changeset 47982  7aa35601ff65 
parent 47936  756f30eac792 
child 51377  7da251a6c16e 
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 

47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47936
diff
changeset

49 
lemma sum_reflp[reflexivity_rule]: 
40820
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 

47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47936
diff
changeset

53 
lemma sum_left_total[reflexivity_rule]: 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47936
diff
changeset

54 
"left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47936
diff
changeset

55 
apply (intro left_totalI) 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47936
diff
changeset

56 
unfolding split_sum_ex 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47936
diff
changeset

57 
by (case_tac x) (auto elim: left_totalE) 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47936
diff
changeset

58 

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

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

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

61 
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

62 

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

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

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

65 
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

66 

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

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

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

69 
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

70 

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

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

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

73 
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

74 

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

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

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

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

78 

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

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

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

81 
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

82 

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

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

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

85 
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

86 

47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47634
diff
changeset

87 
subsection {* Transfer rules for transfer package *} 
47624
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 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

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

91 

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

92 
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

93 
unfolding fun_rel_def by simp 
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 sum_case_transfer [transfer_rule]: 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

96 
"((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

97 
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

98 

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

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

100 

47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47635
diff
changeset

101 
lemma Quotient_sum[quot_map]: 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

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

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

104 
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

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

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

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

108 

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

109 
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

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

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

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

113 

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

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

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

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

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

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

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

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

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

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

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

124 

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

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

126 

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

127 
lemma sum_quotient [quot_thm]: 
47308  128 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
129 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

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

131 
apply (rule Quotient3I) 

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

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

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

137 

47308  138 
declare [[mapQ3 sum = (sum_rel, sum_quotient)]] 
47094  139 

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

140 
lemma sum_Inl_rsp [quot_respect]: 
47308  141 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
142 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

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

143 
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

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

145 

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

146 
lemma sum_Inr_rsp [quot_respect]: 
47308  147 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
148 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

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

149 
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

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

151 

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

152 
lemma sum_Inl_prs [quot_preserve]: 
47308  153 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
154 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

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

155 
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

156 
apply(simp add: fun_eq_iff) 
47308  157 
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

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

159 

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

160 
lemma sum_Inr_prs [quot_preserve]: 
47308  161 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
162 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

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

163 
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

164 
apply(simp add: fun_eq_iff) 
47308  165 
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

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

167 

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

168 
end 