author  nipkow 
Wed, 06 Mar 2013 14:10:07 +0100  
changeset 51358  0c376ef98559 
parent 51357  ac4c1cf1b001 
child 53427  415354b68f0c 
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 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

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

10 

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

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

12 

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

13 
lemmas extended_cases2 = extended.exhaust[case_product extended.exhaust] 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

14 
lemmas extended_cases3 = extended.exhaust[case_product extended_cases2] 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

15 

51357  16 

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

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

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

19 

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

20 
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

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

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

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

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

25 

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

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

27 
"x \<le> y = (case x of Fin x \<Rightarrow> (case y of Fin y \<Rightarrow> x \<le> y  Pinf \<Rightarrow> True  Minf \<Rightarrow> False) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

28 
 Pinf \<Rightarrow> y=Pinf  Minf \<Rightarrow> True)" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

29 
by(induct x y rule: less_eq_extended.induct)(auto split: extended.split) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

30 

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

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

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

33 

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

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

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

36 
case goal1 show ?case by(rule less_extended_def) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

38 
case goal2 show ?case by(cases x) auto 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

40 
case goal3 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

42 
case goal4 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

44 

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

45 
end 
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 
instance extended :: (linorder)linorder 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

49 
case goal1 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

51 

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

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

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

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

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

56 
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

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

58 
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

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

60 

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

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

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

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

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

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

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

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

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

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

70 

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

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

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

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

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

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

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

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

78 

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

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

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

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

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

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

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

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

86 

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

87 

51357  88 
instantiation extended :: (zero)zero 
89 
begin 

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

91 
instance .. 

92 
end 

93 

94 
instantiation extended :: (one)one 

95 
begin 

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

97 
instance .. 

98 
end 

99 

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

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

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

102 

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

103 
text {* The following definition of of addition is totalized 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

104 
to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined. *} 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

105 

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

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

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

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

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

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

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

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

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

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

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

116 

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

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

118 

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

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

120 

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

121 

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

122 
instance extended :: (ab_semigroup_add)ab_semigroup_add 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

124 
fix a b c :: "'a extended" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

125 
show "a + b = b + a" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

126 
by (induct a b rule: plus_extended.induct) (simp_all add: ac_simps) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

127 
show "a + b + c = a + (b + c)" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

128 
by (cases rule: extended_cases3[of a b c]) (simp_all add: ac_simps) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

130 

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

131 
instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

133 
fix a b c :: "'a extended" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

134 
assume "a \<le> b" then show "c + a \<le> c + b" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

135 
by (cases rule: extended_cases3[of a b c]) (auto simp: add_left_mono) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

137 

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

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

140 
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

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

142 

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

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

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

145 

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

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

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

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

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

150 

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

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

152 

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

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

154 

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

155 

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

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

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

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

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

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

161 

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

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

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

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

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

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

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

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

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

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

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

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

173 

51357  174 

175 
text{* Numerals: *} 

176 

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

178 

179 
lemma Fin_numeral: "Fin(numeral w) = numeral w" 

180 
apply (induct w rule: num_induct) 

181 
apply (simp only: numeral_One one_extended_def) 

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

183 
done 

184 

51358  185 
lemma Fin_neg_numeral: "Fin(neg_numeral w) =  numeral w" 
186 
by (simp only: Fin_numeral minus_numeral[symmetric] uminus_extended.simps[symmetric]) 

187 

51357  188 

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

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

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

191 

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

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

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

194 

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

195 
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

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

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

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

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

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

201 

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

202 
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

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

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

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

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

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

208 

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

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

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

211 
fix x y z ::"'a extended" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

212 
show "inf x y \<le> x" "inf x y \<le> y" "\<lbrakk>x \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> x \<le> inf y z" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

213 
"x \<le> sup x y" "y \<le> sup x y" "\<lbrakk>y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> sup y z \<le> x" "bot \<le> x" "x \<le> top" 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

214 
apply (atomize (full)) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

215 
apply (cases rule: extended_cases3[of x y z]) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

216 
apply (auto simp: bot_extended_def top_extended_def) 
054d1653950f
New theory of infinityextended types; should replace Extended_xyz eventually
nipkow
parents:
diff
changeset

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

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

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

220 

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

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

222 