src/HOL/Library/Extended.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (4 months ago) changeset 69946 494934c30f38 parent 67091 1393c2340eec permissions -rw-r--r--
improved code equations taken over from AFP
1 (*  Author:     Tobias Nipkow, TU München
3 A theory of types extended with a greatest and a least element.
4 Oriented towards numeric types, hence "\<infinity>" and "-\<infinity>".
5 *)
7 theory Extended
8   imports Simps_Case_Conv
9 begin
11 datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
14 instantiation extended :: (order)order
15 begin
17 fun less_eq_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
18 "Fin x \<le> Fin y = (x \<le> y)" |
19 "_     \<le> Pinf  = True" |
20 "Minf  \<le> _     = True" |
21 "(_::'a extended) \<le> _     = False"
23 case_of_simps less_eq_extended_case: less_eq_extended.simps
25 definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
26 "((x::'a extended) < y) = (x \<le> y \<and> \<not> y \<le> x)"
28 instance
29   by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
31 end
33 instance extended :: (linorder)linorder
34   by intro_classes (auto simp: less_eq_extended_case split:extended.splits)
36 lemma Minf_le[simp]: "Minf \<le> y"
37 by(cases y) auto
38 lemma le_Pinf[simp]: "x \<le> Pinf"
39 by(cases x) auto
40 lemma le_Minf[simp]: "x \<le> Minf \<longleftrightarrow> x = Minf"
41 by(cases x) auto
42 lemma Pinf_le[simp]: "Pinf \<le> x \<longleftrightarrow> x = Pinf"
43 by(cases x) auto
45 lemma less_extended_simps[simp]:
46   "Fin x < Fin y = (x < y)"
47   "Fin x < Pinf  = True"
48   "Fin x < Minf  = False"
49   "Pinf < h      = False"
50   "Minf < Fin x  = True"
51   "Minf < Pinf   = True"
52   "l    < Minf   = False"
53 by (auto simp add: less_extended_def)
55 lemma min_extended_simps[simp]:
56   "min (Fin x) (Fin y) = Fin(min x y)"
57   "min xx      Pinf    = xx"
58   "min xx      Minf    = Minf"
59   "min Pinf    yy      = yy"
60   "min Minf    yy      = Minf"
61 by (auto simp add: min_def)
63 lemma max_extended_simps[simp]:
64   "max (Fin x) (Fin y) = Fin(max x y)"
65   "max xx      Pinf    = Pinf"
66   "max xx      Minf    = xx"
67   "max Pinf    yy      = Pinf"
68   "max Minf    yy      = yy"
69 by (auto simp add: max_def)
72 instantiation extended :: (zero)zero
73 begin
74 definition "0 = Fin(0::'a)"
75 instance ..
76 end
78 declare zero_extended_def[symmetric, code_post]
80 instantiation extended :: (one)one
81 begin
82 definition "1 = Fin(1::'a)"
83 instance ..
84 end
86 declare one_extended_def[symmetric, code_post]
88 instantiation extended :: (plus)plus
89 begin
91 text \<open>The following definition of of addition is totalized
92 to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined.\<close>
94 fun plus_extended where
95 "Fin x + Fin y = Fin(x+y)" |
96 "Fin x + Pinf  = Pinf" |
97 "Pinf  + Fin x = Pinf" |
98 "Pinf  + Pinf  = Pinf" |
99 "Minf  + Fin y = Minf" |
100 "Fin x + Minf  = Minf" |
101 "Minf  + Minf  = Minf" |
102 "Minf  + Pinf  = Pinf" |
103 "Pinf  + Minf  = Pinf"
105 case_of_simps plus_case: plus_extended.simps
107 instance ..
109 end
114   by intro_classes (simp_all add: ac_simps plus_case split: extended.splits)
117   by intro_classes (auto simp: add_left_mono plus_case split: extended.splits)
120 proof
121   fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto
122 qed
124 instantiation extended :: (uminus)uminus
125 begin
127 fun uminus_extended where
128 "- (Fin x) = Fin (- x)" |
129 "- Pinf    = Minf" |
130 "- Minf    = Pinf"
132 instance ..
134 end
138 begin
139 definition "x - y = x + -(y::'a extended)"
140 instance ..
141 end
143 lemma minus_extended_simps[simp]:
144   "Fin x - Fin y = Fin(x - y)"
145   "Fin x - Pinf  = Minf"
146   "Fin x - Minf  = Pinf"
147   "Pinf  - Fin y = Pinf"
148   "Pinf  - Minf  = Pinf"
149   "Minf  - Fin y = Minf"
150   "Minf  - Pinf  = Minf"
151   "Minf  - Minf  = Pinf"
152   "Pinf  - Pinf  = Pinf"
156 text\<open>Numerals:\<close>
158 instance extended :: ("{ab_semigroup_add,one}")numeral ..
160 lemma Fin_numeral[code_post]: "Fin(numeral w) = numeral w"
161   apply (induct w rule: num_induct)
162   apply (simp only: numeral_One one_extended_def)
163   apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
164   done
166 lemma Fin_neg_numeral[code_post]: "Fin (- numeral w) = - numeral w"
167 by (simp only: Fin_numeral uminus_extended.simps[symmetric])
170 instantiation extended :: (lattice)bounded_lattice
171 begin
173 definition "bot = Minf"
174 definition "top = Pinf"
176 fun inf_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
177 "inf_extended (Fin i) (Fin j) = Fin (inf i j)" |
178 "inf_extended a Minf = Minf" |
179 "inf_extended Minf a = Minf" |
180 "inf_extended Pinf a = a" |
181 "inf_extended a Pinf = a"
183 fun sup_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
184 "sup_extended (Fin i) (Fin j) = Fin (sup i j)" |
185 "sup_extended a Pinf = Pinf" |
186 "sup_extended Pinf a = Pinf" |
187 "sup_extended Minf a = a" |
188 "sup_extended a Minf = a"
190 case_of_simps inf_extended_case: inf_extended.simps
191 case_of_simps sup_extended_case: sup_extended.simps
193 instance
194   by (intro_classes) (auto simp: inf_extended_case sup_extended_case less_eq_extended_case
195     bot_extended_def top_extended_def split: extended.splits)
196 end
198 end