author  kuncar 
Tue, 13 Aug 2013 15:59:22 +0200  
changeset 53010  ec5e6f69bd65 
parent 51994  82cc2aeb7d13 
child 53012  cb82606b8215 
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 

51377  53 
lemma option_rel_mono[relator_mono]: 
54 
assumes "A \<le> B" 

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

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

57 

58 
lemma option_rel_OO[relator_distr]: 

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

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

61 

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

62 
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

63 
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

64 
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

65 
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

66 
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

67 

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

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

70 
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

71 

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

73 
"left_total R \<Longrightarrow> left_total (option_rel R)" 
51994  74 
unfolding left_total_def split_option_all split_option_ex by simp 
75 

76 
lemma left_unique_option_rel [reflexivity_rule]: 

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

78 
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

79 

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

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

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

82 
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

83 

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

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

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

86 
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

87 

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

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

89 
"equivp R \<Longrightarrow> equivp (option_rel R)" 
51994  90 
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

91 

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

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

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

94 
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

95 

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

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

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

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

99 

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

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

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

102 
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

103 

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

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

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

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

107 

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

108 
subsection {* Transfer rules for transfer package *} 
47624
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 None_transfer [transfer_rule]: "(option_rel A) None None" 
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

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

112 

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

113 
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

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

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

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

119 

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

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

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

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

123 

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

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

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

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

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

128 

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

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

130 

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

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

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

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

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

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

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

137 

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

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

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

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

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

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

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

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

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

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

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

148 

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

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

150 

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

151 
lemma option_quotient [quot_thm]: 
47308  152 
assumes "Quotient3 R Abs Rep" 
153 
shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)" 

154 
apply (rule Quotient3I) 

155 
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]) 

156 
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

157 
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

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

159 

47308  160 
declare [[mapQ3 option = (option_rel, option_quotient)]] 
47094  161 

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

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

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

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

166 

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

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

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

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

171 

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

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

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

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

176 

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

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

179 
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

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

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

183 

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

184 
end 