src/HOL/Library/Extended.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 53427 415354b68f0c
child 54489 03ff4d1e6784
permissions -rw-r--r--
more simplification rules on unary and binary minus
     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> x \<ge> y)"
    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 instantiation extended :: (one)one
    81 begin
    82 definition "1 = Fin(1::'a)"
    83 instance ..
    84 end
    85 
    86 instantiation extended :: (plus)plus
    87 begin
    88 
    89 text {* The following definition of of addition is totalized
    90 to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined. *}
    91 
    92 fun plus_extended where
    93 "Fin x + Fin y = Fin(x+y)" |
    94 "Fin x + Pinf  = Pinf" |
    95 "Pinf  + Fin x = Pinf" |
    96 "Pinf  + Pinf  = Pinf" |
    97 "Minf  + Fin y = Minf" |
    98 "Fin x + Minf  = Minf" |
    99 "Minf  + Minf  = Minf" |
   100 "Minf  + Pinf  = Pinf" |
   101 "Pinf  + Minf  = Pinf"
   102 
   103 case_of_simps plus_case: plus_extended.simps
   104 
   105 instance ..
   106 
   107 end
   108 
   109 
   110 
   111 instance extended :: (ab_semigroup_add)ab_semigroup_add
   112   by intro_classes (simp_all add: ac_simps plus_case split: extended.splits)
   113 
   114 instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add
   115   by intro_classes (auto simp: add_left_mono plus_case split: extended.splits)
   116 
   117 instance extended :: (comm_monoid_add)comm_monoid_add
   118 proof
   119   fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto
   120 qed
   121 
   122 instantiation extended :: (uminus)uminus
   123 begin
   124 
   125 fun uminus_extended where
   126 "- (Fin x) = Fin (- x)" |
   127 "- Pinf    = Minf" |
   128 "- Minf    = Pinf"
   129 
   130 instance ..
   131 
   132 end
   133 
   134 
   135 instantiation extended :: (ab_group_add)minus
   136 begin
   137 definition "x - y = x + -(y::'a extended)"
   138 instance ..
   139 end
   140 
   141 lemma minus_extended_simps[simp]:
   142   "Fin x - Fin y = Fin(x - y)"
   143   "Fin x - Pinf  = Minf"
   144   "Fin x - Minf  = Pinf"
   145   "Pinf  - Fin y = Pinf"
   146   "Pinf  - Minf  = Pinf"
   147   "Minf  - Fin y = Minf"
   148   "Minf  - Pinf  = Minf"
   149   "Minf  - Minf  = Pinf"
   150   "Pinf  - Pinf  = Pinf"
   151 by (simp_all add: minus_extended_def)
   152 
   153 
   154 text{* Numerals: *}
   155 
   156 instance extended :: ("{ab_semigroup_add,one}")numeral ..
   157 
   158 lemma Fin_numeral: "Fin(numeral w) = numeral w"
   159   apply (induct w rule: num_induct)
   160   apply (simp only: numeral_One one_extended_def)
   161   apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
   162   done
   163 
   164 lemma Fin_neg_numeral: "Fin(neg_numeral w) = - numeral w"
   165 by (simp only: Fin_numeral minus_numeral[symmetric] uminus_extended.simps[symmetric])
   166 
   167 
   168 instantiation extended :: (lattice)bounded_lattice
   169 begin
   170 
   171 definition "bot = Minf"
   172 definition "top = Pinf"
   173 
   174 fun inf_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
   175 "inf_extended (Fin i) (Fin j) = Fin (inf i j)" |
   176 "inf_extended a Minf = Minf" |
   177 "inf_extended Minf a = Minf" |
   178 "inf_extended Pinf a = a" |
   179 "inf_extended a Pinf = a"
   180 
   181 fun sup_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
   182 "sup_extended (Fin i) (Fin j) = Fin (sup i j)" |
   183 "sup_extended a Pinf = Pinf" |
   184 "sup_extended Pinf a = Pinf" |
   185 "sup_extended Minf a = a" |
   186 "sup_extended a Minf = a"
   187 
   188 case_of_simps inf_extended_case: inf_extended.simps
   189 case_of_simps sup_extended_case: sup_extended.simps
   190 
   191 instance
   192   by (intro_classes) (auto simp: inf_extended_case sup_extended_case less_eq_extended_case
   193     bot_extended_def top_extended_def split: extended.splits)
   194 end
   195 
   196 end
   197