src/HOL/Library/Extended.thy
 author wenzelm Mon Dec 28 01:28:28 2015 +0100 (2015-12-28) changeset 61945 1135b8de26c3 parent 60500 903bb1495239 child 65366 10ca63a18e56 permissions -rw-r--r--
more symbols;
```     1 (*  Author:     Tobias Nipkow, TU München
```
```     2
```
```     3 A theory of types extended with a greatest and a least element.
```
```     4 Oriented towards numeric types, hence "\<infinity>" and "-\<infinity>".
```
```     5 *)
```
```     6
```
```     7 theory Extended
```
```     8 imports
```
```     9   Main
```
```    10   "~~/src/HOL/Library/Simps_Case_Conv"
```
```    11 begin
```
```    12
```
```    13 datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
```
```    14
```
```    15
```
```    16 instantiation extended :: (order)order
```
```    17 begin
```
```    18
```
```    19 fun less_eq_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
```
```    20 "Fin x \<le> Fin y = (x \<le> y)" |
```
```    21 "_     \<le> Pinf  = True" |
```
```    22 "Minf  \<le> _     = True" |
```
```    23 "(_::'a extended) \<le> _     = False"
```
```    24
```
```    25 case_of_simps less_eq_extended_case: less_eq_extended.simps
```
```    26
```
```    27 definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
```
```    28 "((x::'a extended) < y) = (x \<le> y & \<not> y \<le> x)"
```
```    29
```
```    30 instance
```
```    31   by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
```
```    32
```
```    33 end
```
```    34
```
```    35 instance extended :: (linorder)linorder
```
```    36   by intro_classes (auto simp: less_eq_extended_case split:extended.splits)
```
```    37
```
```    38 lemma Minf_le[simp]: "Minf \<le> y"
```
```    39 by(cases y) auto
```
```    40 lemma le_Pinf[simp]: "x \<le> Pinf"
```
```    41 by(cases x) auto
```
```    42 lemma le_Minf[simp]: "x \<le> Minf \<longleftrightarrow> x = Minf"
```
```    43 by(cases x) auto
```
```    44 lemma Pinf_le[simp]: "Pinf \<le> x \<longleftrightarrow> x = Pinf"
```
```    45 by(cases x) auto
```
```    46
```
```    47 lemma less_extended_simps[simp]:
```
```    48   "Fin x < Fin y = (x < y)"
```
```    49   "Fin x < Pinf  = True"
```
```    50   "Fin x < Minf  = False"
```
```    51   "Pinf < h      = False"
```
```    52   "Minf < Fin x  = True"
```
```    53   "Minf < Pinf   = True"
```
```    54   "l    < Minf   = False"
```
```    55 by (auto simp add: less_extended_def)
```
```    56
```
```    57 lemma min_extended_simps[simp]:
```
```    58   "min (Fin x) (Fin y) = Fin(min x y)"
```
```    59   "min xx      Pinf    = xx"
```
```    60   "min xx      Minf    = Minf"
```
```    61   "min Pinf    yy      = yy"
```
```    62   "min Minf    yy      = Minf"
```
```    63 by (auto simp add: min_def)
```
```    64
```
```    65 lemma max_extended_simps[simp]:
```
```    66   "max (Fin x) (Fin y) = Fin(max x y)"
```
```    67   "max xx      Pinf    = Pinf"
```
```    68   "max xx      Minf    = xx"
```
```    69   "max Pinf    yy      = Pinf"
```
```    70   "max Minf    yy      = yy"
```
```    71 by (auto simp add: max_def)
```
```    72
```
```    73
```
```    74 instantiation extended :: (zero)zero
```
```    75 begin
```
```    76 definition "0 = Fin(0::'a)"
```
```    77 instance ..
```
```    78 end
```
```    79
```
```    80 declare zero_extended_def[symmetric, code_post]
```
```    81
```
```    82 instantiation extended :: (one)one
```
```    83 begin
```
```    84 definition "1 = Fin(1::'a)"
```
```    85 instance ..
```
```    86 end
```
```    87
```
```    88 declare one_extended_def[symmetric, code_post]
```
```    89
```
```    90 instantiation extended :: (plus)plus
```
```    91 begin
```
```    92
```
```    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>
```
```    95
```
```    96 fun plus_extended where
```
```    97 "Fin x + Fin y = Fin(x+y)" |
```
```    98 "Fin x + Pinf  = Pinf" |
```
```    99 "Pinf  + Fin x = Pinf" |
```
```   100 "Pinf  + Pinf  = Pinf" |
```
```   101 "Minf  + Fin y = Minf" |
```
```   102 "Fin x + Minf  = Minf" |
```
```   103 "Minf  + Minf  = Minf" |
```
```   104 "Minf  + Pinf  = Pinf" |
```
```   105 "Pinf  + Minf  = Pinf"
```
```   106
```
```   107 case_of_simps plus_case: plus_extended.simps
```
```   108
```
```   109 instance ..
```
```   110
```
```   111 end
```
```   112
```
```   113
```
```   114
```
```   115 instance extended :: (ab_semigroup_add)ab_semigroup_add
```
```   116   by intro_classes (simp_all add: ac_simps plus_case split: extended.splits)
```
```   117
```
```   118 instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add
```
```   119   by intro_classes (auto simp: add_left_mono plus_case split: extended.splits)
```
```   120
```
```   121 instance extended :: (comm_monoid_add)comm_monoid_add
```
```   122 proof
```
```   123   fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto
```
```   124 qed
```
```   125
```
```   126 instantiation extended :: (uminus)uminus
```
```   127 begin
```
```   128
```
```   129 fun uminus_extended where
```
```   130 "- (Fin x) = Fin (- x)" |
```
```   131 "- Pinf    = Minf" |
```
```   132 "- Minf    = Pinf"
```
```   133
```
```   134 instance ..
```
```   135
```
```   136 end
```
```   137
```
```   138
```
```   139 instantiation extended :: (ab_group_add)minus
```
```   140 begin
```
```   141 definition "x - y = x + -(y::'a extended)"
```
```   142 instance ..
```
```   143 end
```
```   144
```
```   145 lemma minus_extended_simps[simp]:
```
```   146   "Fin x - Fin y = Fin(x - y)"
```
```   147   "Fin x - Pinf  = Minf"
```
```   148   "Fin x - Minf  = Pinf"
```
```   149   "Pinf  - Fin y = Pinf"
```
```   150   "Pinf  - Minf  = Pinf"
```
```   151   "Minf  - Fin y = Minf"
```
```   152   "Minf  - Pinf  = Minf"
```
```   153   "Minf  - Minf  = Pinf"
```
```   154   "Pinf  - Pinf  = Pinf"
```
```   155 by (simp_all add: minus_extended_def)
```
```   156
```
```   157
```
```   158 text\<open>Numerals:\<close>
```
```   159
```
```   160 instance extended :: ("{ab_semigroup_add,one}")numeral ..
```
```   161
```
```   162 lemma Fin_numeral[code_post]: "Fin(numeral w) = numeral w"
```
```   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
```
```   168 lemma Fin_neg_numeral[code_post]: "Fin (- numeral w) = - numeral w"
```
```   169 by (simp only: Fin_numeral uminus_extended.simps[symmetric])
```
```   170
```
```   171
```
```   172 instantiation extended :: (lattice)bounded_lattice
```
```   173 begin
```
```   174
```
```   175 definition "bot = Minf"
```
```   176 definition "top = Pinf"
```
```   177
```
```   178 fun inf_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
```
```   179 "inf_extended (Fin i) (Fin j) = Fin (inf i j)" |
```
```   180 "inf_extended a Minf = Minf" |
```
```   181 "inf_extended Minf a = Minf" |
```
```   182 "inf_extended Pinf a = a" |
```
```   183 "inf_extended a Pinf = a"
```
```   184
```
```   185 fun sup_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
```
```   186 "sup_extended (Fin i) (Fin j) = Fin (sup i j)" |
```
```   187 "sup_extended a Pinf = Pinf" |
```
```   188 "sup_extended Pinf a = Pinf" |
```
```   189 "sup_extended Minf a = a" |
```
```   190 "sup_extended a Minf = a"
```
```   191
```
```   192 case_of_simps inf_extended_case: inf_extended.simps
```
```   193 case_of_simps sup_extended_case: sup_extended.simps
```
```   194
```
```   195 instance
```
```   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)
```
```   198 end
```
```   199
```
```   200 end
```
```   201
```