author  kuncar 
Wed, 15 May 2013 12:10:39 +0200  
changeset 51994  82cc2aeb7d13 
parent 51956  a4d81cdebf8b 
child 53010  ec5e6f69bd65 
permissions  rwrr 
47455  1 
(* Title: HOL/Library/Quotient_Option.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 option type *} 

6 

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

7 
theory Quotient_Option 
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 option 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:
40464
diff
changeset

14 
option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<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 
"option_rel R None None = True" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

17 
 "option_rel R (Some x) None = False" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

18 
 "option_rel R None (Some x) = False" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

19 
 "option_rel R (Some x) (Some y) = R x y" 
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:
40542
diff
changeset

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

22 
"option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

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

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

25 
by (cases x) (cases y, simp_all)+ 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

26 

51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

27 
fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

28 
where 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

29 
"option_pred R None = True" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

30 
 "option_pred R (Some x) = R x" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

31 

a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

32 
lemma option_pred_unfold: 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

33 
"option_pred P x = (case x of None \<Rightarrow> True 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

34 
 Some x \<Rightarrow> P x)" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

35 
by (cases x) simp_all 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

36 

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

37 
lemma option_rel_map1: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

38 
"option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

39 
by (simp add: option_rel_unfold split: option.split) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

40 

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

41 
lemma option_rel_map2: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

42 
"option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

43 
by (simp add: option_rel_unfold split: option.split) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

44 

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

45 
lemma option_map_id [id_simps]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

46 
"Option.map id = id" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

47 
by (simp add: id_def Option.map.identity fun_eq_iff) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

48 

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

49 
lemma option_rel_eq [id_simps, relator_eq]: 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

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

51 
by (simp add: option_rel_unfold fun_eq_iff split: option.split) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

52 

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

53 
lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

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

55 

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

56 
lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

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

58 

51377  59 
lemma option_rel_mono[relator_mono]: 
60 
assumes "A \<le> B" 

61 
shows "(option_rel A) \<le> (option_rel B)" 

62 
using assms by (auto simp: option_rel_unfold split: option.splits) 

63 

64 
lemma option_rel_OO[relator_distr]: 

65 
"(option_rel A) OO (option_rel B) = option_rel (A OO B)" 

66 
by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split) 

67 

51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

68 
lemma Domainp_option[relator_domain]: 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

69 
assumes "Domainp A = P" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

70 
shows "Domainp (option_rel A) = (option_pred P)" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

71 
using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def] 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

72 
by (auto iff: fun_eq_iff split: option.split) 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

73 

51994  74 
lemma reflp_option_rel[reflexivity_rule]: 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

75 
"reflp R \<Longrightarrow> reflp (option_rel R)" 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

76 
unfolding reflp_def split_option_all by simp 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

77 

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

79 
"left_total R \<Longrightarrow> left_total (option_rel R)" 
51994  80 
unfolding left_total_def split_option_all split_option_ex by simp 
81 

82 
lemma left_unique_option_rel [reflexivity_rule]: 

83 
"left_unique R \<Longrightarrow> left_unique (option_rel R)" 

84 
unfolding left_unique_def split_option_all by simp 

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

85 

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

86 
lemma option_symp: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

87 
"symp R \<Longrightarrow> symp (option_rel R)" 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

88 
unfolding symp_def split_option_all option_rel.simps by fast 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

89 

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

90 
lemma option_transp: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

91 
"transp R \<Longrightarrow> transp (option_rel R)" 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

92 
unfolding transp_def split_option_all option_rel.simps by fast 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

93 

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

94 
lemma option_equivp [quot_equiv]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

95 
"equivp R \<Longrightarrow> equivp (option_rel R)" 
51994  96 
by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE) 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

97 

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

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

99 
"right_total R \<Longrightarrow> right_total (option_rel R)" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

100 
unfolding right_total_def split_option_all split_option_ex by simp 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

101 

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

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

103 
"right_unique R \<Longrightarrow> right_unique (option_rel R)" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

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

105 

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

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

107 
"bi_total R \<Longrightarrow> bi_total (option_rel R)" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

108 
unfolding bi_total_def split_option_all split_option_ex by simp 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

109 

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

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

111 
"bi_unique R \<Longrightarrow> bi_unique (option_rel R)" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

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

113 

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

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

115 

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

116 
lemma None_transfer [transfer_rule]: "(option_rel A) None None" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

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

118 

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

119 
lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

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

121 

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

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

123 
"(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

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

125 

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

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

127 
"((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map" 
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47634
diff
changeset

128 
unfolding Option.map_def by transfer_prover 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

129 

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

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

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

132 
Option.bind Option.bind" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

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

134 

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

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

136 

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

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

138 
assumes "Quotient R Abs Rep T" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

139 
shows "Quotient (option_rel R) (Option.map Abs) 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

140 
(Option.map Rep) (option_rel T)" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

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

142 
by (simp split: option.split) 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

143 

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

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

145 
"option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)" 
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset

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

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

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

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

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

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

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

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

154 

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

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

156 

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

157 
lemma option_quotient [quot_thm]: 
47308  158 
assumes "Quotient3 R Abs Rep" 
159 
shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)" 

160 
apply (rule Quotient3I) 

161 
apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms]) 

162 
using Quotient3_rel [OF assms] 

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

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

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

165 

47308  166 
declare [[mapQ3 option = (option_rel, option_quotient)]] 
47094  167 

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

168 
lemma option_None_rsp [quot_respect]: 
47308  169 
assumes q: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

170 
shows "option_rel R None None" 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

171 
by (rule None_transfer) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

172 

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

173 
lemma option_Some_rsp [quot_respect]: 
47308  174 
assumes q: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

175 
shows "(R ===> option_rel R) Some Some" 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

176 
by (rule Some_transfer) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

177 

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

178 
lemma option_None_prs [quot_preserve]: 
47308  179 
assumes q: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

180 
shows "Option.map Abs None = None" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

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

182 

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

183 
lemma option_Some_prs [quot_preserve]: 
47308  184 
assumes q: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

185 
shows "(Rep > Option.map Abs) Some = Some" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

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

189 

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

190 
end 