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
     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 Simps_Case_Conv
     9 begin
    10 
    11 datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
    12 
    13 
    14 instantiation extended :: (order)order
    15 begin
    16 
    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"
    22 
    23 case_of_simps less_eq_extended_case: less_eq_extended.simps
    24 
    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)"
    27 
    28 instance
    29   by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
    30 
    31 end
    32 
    33 instance extended :: (linorder)linorder
    34   by intro_classes (auto simp: less_eq_extended_case split:extended.splits)
    35 
    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
    44 
    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)
    54 
    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)
    62 
    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)
    70 
    71 
    72 instantiation extended :: (zero)zero
    73 begin
    74 definition "0 = Fin(0::'a)"
    75 instance ..
    76 end
    77 
    78 declare zero_extended_def[symmetric, code_post]
    79 
    80 instantiation extended :: (one)one
    81 begin
    82 definition "1 = Fin(1::'a)"
    83 instance ..
    84 end
    85 
    86 declare one_extended_def[symmetric, code_post]
    87 
    88 instantiation extended :: (plus)plus
    89 begin
    90 
    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>
    93 
    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"
   104 
   105 case_of_simps plus_case: plus_extended.simps
   106 
   107 instance ..
   108 
   109 end
   110 
   111 
   112 
   113 instance extended :: (ab_semigroup_add)ab_semigroup_add
   114   by intro_classes (simp_all add: ac_simps plus_case split: extended.splits)
   115 
   116 instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add
   117   by intro_classes (auto simp: add_left_mono plus_case split: extended.splits)
   118 
   119 instance extended :: (comm_monoid_add)comm_monoid_add
   120 proof
   121   fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto
   122 qed
   123 
   124 instantiation extended :: (uminus)uminus
   125 begin
   126 
   127 fun uminus_extended where
   128 "- (Fin x) = Fin (- x)" |
   129 "- Pinf    = Minf" |
   130 "- Minf    = Pinf"
   131 
   132 instance ..
   133 
   134 end
   135 
   136 
   137 instantiation extended :: (ab_group_add)minus
   138 begin
   139 definition "x - y = x + -(y::'a extended)"
   140 instance ..
   141 end
   142 
   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"
   153 by (simp_all add: minus_extended_def)
   154 
   155 
   156 text\<open>Numerals:\<close>
   157 
   158 instance extended :: ("{ab_semigroup_add,one}")numeral ..
   159 
   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
   165 
   166 lemma Fin_neg_numeral[code_post]: "Fin (- numeral w) = - numeral w"
   167 by (simp only: Fin_numeral uminus_extended.simps[symmetric])
   168 
   169 
   170 instantiation extended :: (lattice)bounded_lattice
   171 begin
   172 
   173 definition "bot = Minf"
   174 definition "top = Pinf"
   175 
   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"
   182 
   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"
   189 
   190 case_of_simps inf_extended_case: inf_extended.simps
   191 case_of_simps sup_extended_case: sup_extended.simps
   192 
   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
   197 
   198 end
   199