author  wenzelm 
Wed, 17 Jun 2015 11:03:05 +0200  
changeset 60500  903bb1495239 
parent 60343  063698416239 
child 65366  10ca63a18e56 
permissions  rwrr 
51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

1 
(* Author: Tobias Nipkow, TU München 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

2 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

3 
A theory of types extended with a greatest and a least element. 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

4 
Oriented towards numeric types, hence "\<infinity>" and "\<infinity>". 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

5 
*) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

6 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

7 
theory Extended 
53427  8 
imports 
9 
Main 

10 
"~~/src/HOL/Library/Simps_Case_Conv" 

51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

11 
begin 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

12 

58310  13 
datatype 'a extended = Fin 'a  Pinf ("\<infinity>")  Minf ("\<infinity>") 
51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

14 

51357  15 

51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

16 
instantiation extended :: (order)order 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

17 
begin 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

18 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

19 
fun less_eq_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

20 
"Fin x \<le> Fin y = (x \<le> y)"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

21 
"_ \<le> Pinf = True"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

22 
"Minf \<le> _ = True"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

23 
"(_::'a extended) \<le> _ = False" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

24 

53427  25 
case_of_simps less_eq_extended_case: less_eq_extended.simps 
51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

26 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

27 
definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where 
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
58310
diff
changeset

28 
"((x::'a extended) < y) = (x \<le> y & \<not> y \<le> x)" 
51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

29 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

30 
instance 
53427  31 
by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits) 
51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

32 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

33 
end 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

34 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

35 
instance extended :: (linorder)linorder 
53427  36 
by intro_classes (auto simp: less_eq_extended_case split:extended.splits) 
51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

37 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

38 
lemma Minf_le[simp]: "Minf \<le> y" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

39 
by(cases y) auto 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

40 
lemma le_Pinf[simp]: "x \<le> Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

41 
by(cases x) auto 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

42 
lemma le_Minf[simp]: "x \<le> Minf \<longleftrightarrow> x = Minf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

43 
by(cases x) auto 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

44 
lemma Pinf_le[simp]: "Pinf \<le> x \<longleftrightarrow> x = Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

45 
by(cases x) auto 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

46 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

47 
lemma less_extended_simps[simp]: 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

48 
"Fin x < Fin y = (x < y)" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

49 
"Fin x < Pinf = True" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

50 
"Fin x < Minf = False" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

51 
"Pinf < h = False" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

52 
"Minf < Fin x = True" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

53 
"Minf < Pinf = True" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

54 
"l < Minf = False" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

55 
by (auto simp add: less_extended_def) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

56 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

57 
lemma min_extended_simps[simp]: 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

58 
"min (Fin x) (Fin y) = Fin(min x y)" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

59 
"min xx Pinf = xx" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

60 
"min xx Minf = Minf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

61 
"min Pinf yy = yy" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

62 
"min Minf yy = Minf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

63 
by (auto simp add: min_def) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

64 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

65 
lemma max_extended_simps[simp]: 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

66 
"max (Fin x) (Fin y) = Fin(max x y)" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

67 
"max xx Pinf = Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

68 
"max xx Minf = xx" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

69 
"max Pinf yy = Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

70 
"max Minf yy = yy" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

71 
by (auto simp add: max_def) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

72 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

73 

51357  74 
instantiation extended :: (zero)zero 
75 
begin 

76 
definition "0 = Fin(0::'a)" 

77 
instance .. 

78 
end 

79 

55124  80 
declare zero_extended_def[symmetric, code_post] 
81 

51357  82 
instantiation extended :: (one)one 
83 
begin 

84 
definition "1 = Fin(1::'a)" 

85 
instance .. 

86 
end 

87 

55124  88 
declare one_extended_def[symmetric, code_post] 
89 

51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

90 
instantiation extended :: (plus)plus 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

91 
begin 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

92 

60500  93 
text \<open>The following definition of of addition is totalized 
94 
to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined.\<close> 

51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

95 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

96 
fun plus_extended where 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

97 
"Fin x + Fin y = Fin(x+y)"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

98 
"Fin x + Pinf = Pinf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

99 
"Pinf + Fin x = Pinf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

100 
"Pinf + Pinf = Pinf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

101 
"Minf + Fin y = Minf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

102 
"Fin x + Minf = Minf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

103 
"Minf + Minf = Minf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

104 
"Minf + Pinf = Pinf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

105 
"Pinf + Minf = Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

106 

53427  107 
case_of_simps plus_case: plus_extended.simps 
108 

51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

109 
instance .. 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

110 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

111 
end 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

112 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

113 

53427  114 

51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

115 
instance extended :: (ab_semigroup_add)ab_semigroup_add 
53427  116 
by intro_classes (simp_all add: ac_simps plus_case split: extended.splits) 
51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

117 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

118 
instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add 
53427  119 
by intro_classes (auto simp: add_left_mono plus_case split: extended.splits) 
51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

120 

51357  121 
instance extended :: (comm_monoid_add)comm_monoid_add 
51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

122 
proof 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

123 
fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

124 
qed 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

125 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

126 
instantiation extended :: (uminus)uminus 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

127 
begin 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

128 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

129 
fun uminus_extended where 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

130 
" (Fin x) = Fin ( x)"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

131 
" Pinf = Minf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

132 
" Minf = Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

133 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

134 
instance .. 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

135 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

136 
end 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

137 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

138 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

139 
instantiation extended :: (ab_group_add)minus 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

140 
begin 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

141 
definition "x  y = x + (y::'a extended)" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

142 
instance .. 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

143 
end 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

144 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

145 
lemma minus_extended_simps[simp]: 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

146 
"Fin x  Fin y = Fin(x  y)" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

147 
"Fin x  Pinf = Minf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

148 
"Fin x  Minf = Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

149 
"Pinf  Fin y = Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

150 
"Pinf  Minf = Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

151 
"Minf  Fin y = Minf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

152 
"Minf  Pinf = Minf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

153 
"Minf  Minf = Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

154 
"Pinf  Pinf = Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

155 
by (simp_all add: minus_extended_def) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

156 

51357  157 

60500  158 
text\<open>Numerals:\<close> 
51357  159 

160 
instance extended :: ("{ab_semigroup_add,one}")numeral .. 

161 

55124  162 
lemma Fin_numeral[code_post]: "Fin(numeral w) = numeral w" 
51357  163 
apply (induct w rule: num_induct) 
164 
apply (simp only: numeral_One one_extended_def) 

165 
apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric]) 

166 
done 

167 

55124  168 
lemma Fin_neg_numeral[code_post]: "Fin ( numeral w) =  numeral w" 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
53427
diff
changeset

169 
by (simp only: Fin_numeral uminus_extended.simps[symmetric]) 
51358  170 

51357  171 

51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

172 
instantiation extended :: (lattice)bounded_lattice 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

173 
begin 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

174 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

175 
definition "bot = Minf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

176 
definition "top = Pinf" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

177 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

178 
fun inf_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

179 
"inf_extended (Fin i) (Fin j) = Fin (inf i j)"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

180 
"inf_extended a Minf = Minf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

181 
"inf_extended Minf a = Minf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

182 
"inf_extended Pinf a = a"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

183 
"inf_extended a Pinf = a" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

184 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

185 
fun sup_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

186 
"sup_extended (Fin i) (Fin j) = Fin (sup i j)"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

187 
"sup_extended a Pinf = Pinf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

188 
"sup_extended Pinf a = Pinf"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

189 
"sup_extended Minf a = a"  
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

190 
"sup_extended a Minf = a" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

191 

53427  192 
case_of_simps inf_extended_case: inf_extended.simps 
193 
case_of_simps sup_extended_case: sup_extended.simps 

194 

51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

195 
instance 
53427  196 
by (intro_classes) (auto simp: inf_extended_case sup_extended_case less_eq_extended_case 
197 
bot_extended_def top_extended_def split: extended.splits) 

51338
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

198 
end 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

199 

054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

200 
end 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

201 