author  blanchet 
Fri, 24 Jan 2014 11:51:45 +0100  
changeset 55129  26bd1cba3ab5 
parent 55090  9475b16e520b 
child 55404  5cb95b79a51f 
permissions  rwrr 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

1 
(* Title: HOL/Lifting_Option.thy 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

2 
Author: Brian Huffman and Ondrej Kuncar 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

3 
Author: Andreas Lochbihler, Karlsruhe Institute of Technology 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

4 
*) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

5 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

6 
header {* Setup for Lifting/Transfer for the option type *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

7 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

8 
theory Lifting_Option 
55090
9475b16e520b
technical import to avoid infamous 'duplicate Option.size' error at merge time in 'List.thy'
blanchet
parents:
55089
diff
changeset

9 
imports Lifting Partial_Function 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

10 
begin 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

11 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

12 
subsection {* Relator and predicator properties *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

13 

53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

14 
definition 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

15 
option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

16 
where 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

17 
"option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

18 
 (Some x, Some y) \<Rightarrow> R x y 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

19 
 _ \<Rightarrow> False)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

20 

53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

21 
lemma option_rel_simps[simp]: 
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

22 
"option_rel R None None = True" 
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

23 
"option_rel R (Some x) None = False" 
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

24 
"option_rel R None (Some y) = False" 
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

25 
"option_rel R (Some x) (Some y) = R x y" 
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

26 
unfolding option_rel_def by simp_all 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

27 

53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

28 
abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where 
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

29 
"option_pred \<equiv> option_case True" 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

30 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

31 
lemma option_rel_eq [relator_eq]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

32 
"option_rel (op =) = (op =)" 
53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

33 
by (simp add: option_rel_def fun_eq_iff split: option.split) 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

34 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

35 
lemma option_rel_mono[relator_mono]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

36 
assumes "A \<le> B" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

37 
shows "(option_rel A) \<le> (option_rel B)" 
53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

38 
using assms by (auto simp: option_rel_def split: option.splits) 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

39 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

40 
lemma option_rel_OO[relator_distr]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

41 
"(option_rel A) OO (option_rel B) = option_rel (A OO B)" 
53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

42 
by (rule ext)+ (auto simp: option_rel_def OO_def split: option.split) 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

43 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

44 
lemma Domainp_option[relator_domain]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

45 
assumes "Domainp A = P" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

46 
shows "Domainp (option_rel A) = (option_pred P)" 
53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

47 
using assms unfolding Domainp_iff[abs_def] option_rel_def[abs_def] 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

48 
by (auto iff: fun_eq_iff split: option.split) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

49 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

50 
lemma reflp_option_rel[reflexivity_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

51 
"reflp R \<Longrightarrow> reflp (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

52 
unfolding reflp_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

53 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

54 
lemma left_total_option_rel[reflexivity_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

55 
"left_total R \<Longrightarrow> left_total (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

56 
unfolding left_total_def split_option_all split_option_ex by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

57 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

58 
lemma left_unique_option_rel [reflexivity_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

59 
"left_unique R \<Longrightarrow> left_unique (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

60 
unfolding left_unique_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

61 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

62 
lemma right_total_option_rel [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

63 
"right_total R \<Longrightarrow> right_total (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

64 
unfolding right_total_def split_option_all split_option_ex by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

65 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

66 
lemma right_unique_option_rel [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

67 
"right_unique R \<Longrightarrow> right_unique (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

68 
unfolding right_unique_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

69 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

70 
lemma bi_total_option_rel [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

71 
"bi_total R \<Longrightarrow> bi_total (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

72 
unfolding bi_total_def split_option_all split_option_ex by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

73 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

74 
lemma bi_unique_option_rel [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

75 
"bi_unique R \<Longrightarrow> bi_unique (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

76 
unfolding bi_unique_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

77 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

78 
lemma option_invariant_commute [invariant_commute]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

79 
"option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

80 
by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

81 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

82 
subsection {* Quotient theorem for the Lifting package *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

83 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

84 
lemma Quotient_option[quot_map]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

85 
assumes "Quotient R Abs Rep T" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

86 
shows "Quotient (option_rel R) (Option.map Abs) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

87 
(Option.map Rep) (option_rel T)" 
53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

88 
using assms unfolding Quotient_alt_def option_rel_def 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

89 
by (simp split: option.split) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

90 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

91 
subsection {* Transfer rules for the Transfer package *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

92 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

93 
context 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

94 
begin 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

95 
interpretation lifting_syntax . 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

96 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

97 
lemma None_transfer [transfer_rule]: "(option_rel A) None None" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

98 
by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

99 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

100 
lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

101 
unfolding fun_rel_def by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

102 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

103 
lemma option_case_transfer [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

104 
"(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

105 
unfolding fun_rel_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

106 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

107 
lemma option_map_transfer [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

108 
"((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

109 
unfolding Option.map_def by transfer_prover 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

110 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

111 
lemma option_bind_transfer [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

112 
"(option_rel A ===> (A ===> option_rel B) ===> option_rel B) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

113 
Option.bind Option.bind" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

114 
unfolding fun_rel_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

115 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

116 
end 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

117 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

118 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

119 
subsubsection {* BNF setup *} 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

120 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

121 
lemma option_rec_conv_option_case: "option_rec = option_case" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

122 
by (simp add: fun_eq_iff split: option.split) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

123 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

124 
bnf "'a option" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

125 
map: Option.map 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

126 
sets: Option.set 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

127 
bd: natLeq 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

128 
wits: None 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

129 
rel: option_rel 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

130 
proof  
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

131 
show "Option.map id = id" by (rule Option.map.id) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

132 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

133 
fix f g 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

134 
show "Option.map (g \<circ> f) = Option.map g \<circ> Option.map f" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

135 
by (auto simp add: fun_eq_iff Option.map_def split: option.split) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

136 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

137 
fix f g x 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

138 
assume "\<And>z. z \<in> Option.set x \<Longrightarrow> f z = g z" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

139 
thus "Option.map f x = Option.map g x" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

140 
by (simp cong: Option.map_cong) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

141 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

142 
fix f 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

143 
show "Option.set \<circ> Option.map f = op ` f \<circ> Option.set" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

144 
by fastforce 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

145 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

146 
show "card_order natLeq" by (rule natLeq_card_order) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

147 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

148 
show "cinfinite natLeq" by (rule natLeq_cinfinite) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

149 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

150 
fix x 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

151 
show "Option.set x \<le>o natLeq" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

152 
by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric]) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

153 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

154 
fix R S 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

155 
show "option_rel R OO option_rel S \<le> option_rel (R OO S)" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

156 
by (auto simp: option_rel_def split: option.splits) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

157 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

158 
fix z 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

159 
assume "z \<in> Option.set None" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

160 
thus False by simp 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

161 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

162 
fix R 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

163 
show "option_rel R = 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

164 
(Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

165 
Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

166 
unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

167 
by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some] 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

168 
split: option.splits) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

169 
qed 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

170 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

171 
end 