src/HOL/Library/Extended.thy
author nipkow
Tue Mar 05 15:26:57 2013 +0100 (2013-03-05)
changeset 51338 054d1653950f
child 51357 ac4c1cf1b001
permissions -rw-r--r--
New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow@51338
     1
(*  Author:     Tobias Nipkow, TU M√ľnchen
nipkow@51338
     2
nipkow@51338
     3
A theory of types extended with a greatest and a least element.
nipkow@51338
     4
Oriented towards numeric types, hence "\<infinity>" and "-\<infinity>".
nipkow@51338
     5
*)
nipkow@51338
     6
nipkow@51338
     7
theory Extended
nipkow@51338
     8
imports Main
nipkow@51338
     9
begin
nipkow@51338
    10
nipkow@51338
    11
datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
nipkow@51338
    12
nipkow@51338
    13
lemmas extended_cases2 = extended.exhaust[case_product extended.exhaust]
nipkow@51338
    14
lemmas extended_cases3 = extended.exhaust[case_product extended_cases2]
nipkow@51338
    15
nipkow@51338
    16
instantiation extended :: (order)order
nipkow@51338
    17
begin
nipkow@51338
    18
nipkow@51338
    19
fun less_eq_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
nipkow@51338
    20
"Fin x \<le> Fin y = (x \<le> y)" |
nipkow@51338
    21
"_     \<le> Pinf  = True" |
nipkow@51338
    22
"Minf  \<le> _     = True" |
nipkow@51338
    23
"(_::'a extended) \<le> _     = False"
nipkow@51338
    24
nipkow@51338
    25
lemma less_eq_extended_cases:
nipkow@51338
    26
  "x \<le> y = (case x of Fin x \<Rightarrow> (case y of Fin y \<Rightarrow> x \<le> y | Pinf \<Rightarrow> True | Minf \<Rightarrow> False)
nipkow@51338
    27
            | Pinf \<Rightarrow> y=Pinf | Minf \<Rightarrow> True)"
nipkow@51338
    28
by(induct x y rule: less_eq_extended.induct)(auto split: extended.split)
nipkow@51338
    29
nipkow@51338
    30
definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
nipkow@51338
    31
"((x::'a extended) < y) = (x \<le> y & \<not> x \<ge> y)"
nipkow@51338
    32
nipkow@51338
    33
instance
nipkow@51338
    34
proof
nipkow@51338
    35
  case goal1 show ?case by(rule less_extended_def)
nipkow@51338
    36
next
nipkow@51338
    37
  case goal2 show ?case by(cases x) auto
nipkow@51338
    38
next
nipkow@51338
    39
  case goal3 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
nipkow@51338
    40
next
nipkow@51338
    41
  case goal4 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
nipkow@51338
    42
qed
nipkow@51338
    43
nipkow@51338
    44
end
nipkow@51338
    45
nipkow@51338
    46
instance extended :: (linorder)linorder
nipkow@51338
    47
proof
nipkow@51338
    48
  case goal1 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
nipkow@51338
    49
qed
nipkow@51338
    50
nipkow@51338
    51
lemma Minf_le[simp]: "Minf \<le> y"
nipkow@51338
    52
by(cases y) auto
nipkow@51338
    53
lemma le_Pinf[simp]: "x \<le> Pinf"
nipkow@51338
    54
by(cases x) auto
nipkow@51338
    55
lemma le_Minf[simp]: "x \<le> Minf \<longleftrightarrow> x = Minf"
nipkow@51338
    56
by(cases x) auto
nipkow@51338
    57
lemma Pinf_le[simp]: "Pinf \<le> x \<longleftrightarrow> x = Pinf"
nipkow@51338
    58
by(cases x) auto
nipkow@51338
    59
nipkow@51338
    60
lemma less_extended_simps[simp]:
nipkow@51338
    61
  "Fin x < Fin y = (x < y)"
nipkow@51338
    62
  "Fin x < Pinf  = True"
nipkow@51338
    63
  "Fin x < Minf  = False"
nipkow@51338
    64
  "Pinf < h      = False"
nipkow@51338
    65
  "Minf < Fin x  = True"
nipkow@51338
    66
  "Minf < Pinf   = True"
nipkow@51338
    67
  "l    < Minf   = False"
nipkow@51338
    68
by (auto simp add: less_extended_def)
nipkow@51338
    69
nipkow@51338
    70
lemma min_extended_simps[simp]:
nipkow@51338
    71
  "min (Fin x) (Fin y) = Fin(min x y)"
nipkow@51338
    72
  "min xx      Pinf    = xx"
nipkow@51338
    73
  "min xx      Minf    = Minf"
nipkow@51338
    74
  "min Pinf    yy      = yy"
nipkow@51338
    75
  "min Minf    yy      = Minf"
nipkow@51338
    76
by (auto simp add: min_def)
nipkow@51338
    77
nipkow@51338
    78
lemma max_extended_simps[simp]:
nipkow@51338
    79
  "max (Fin x) (Fin y) = Fin(max x y)"
nipkow@51338
    80
  "max xx      Pinf    = Pinf"
nipkow@51338
    81
  "max xx      Minf    = xx"
nipkow@51338
    82
  "max Pinf    yy      = Pinf"
nipkow@51338
    83
  "max Minf    yy      = yy"
nipkow@51338
    84
by (auto simp add: max_def)
nipkow@51338
    85
nipkow@51338
    86
nipkow@51338
    87
instantiation extended :: (plus)plus
nipkow@51338
    88
begin
nipkow@51338
    89
nipkow@51338
    90
text {* The following definition of of addition is totalized
nipkow@51338
    91
to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined. *}
nipkow@51338
    92
nipkow@51338
    93
fun plus_extended where
nipkow@51338
    94
"Fin x + Fin y = Fin(x+y)" |
nipkow@51338
    95
"Fin x + Pinf  = Pinf" |
nipkow@51338
    96
"Pinf  + Fin x = Pinf" |
nipkow@51338
    97
"Pinf  + Pinf  = Pinf" |
nipkow@51338
    98
"Minf  + Fin y = Minf" |
nipkow@51338
    99
"Fin x + Minf  = Minf" |
nipkow@51338
   100
"Minf  + Minf  = Minf" |
nipkow@51338
   101
"Minf  + Pinf  = Pinf" |
nipkow@51338
   102
"Pinf  + Minf  = Pinf"
nipkow@51338
   103
nipkow@51338
   104
instance ..
nipkow@51338
   105
nipkow@51338
   106
end
nipkow@51338
   107
nipkow@51338
   108
nipkow@51338
   109
instance extended :: (ab_semigroup_add)ab_semigroup_add
nipkow@51338
   110
proof
nipkow@51338
   111
  fix a b c :: "'a extended"
nipkow@51338
   112
  show "a + b = b + a"
nipkow@51338
   113
    by (induct a b rule: plus_extended.induct) (simp_all add: ac_simps)
nipkow@51338
   114
  show "a + b + c = a + (b + c)"
nipkow@51338
   115
    by (cases rule: extended_cases3[of a b c]) (simp_all add: ac_simps)
nipkow@51338
   116
qed
nipkow@51338
   117
nipkow@51338
   118
instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add
nipkow@51338
   119
proof
nipkow@51338
   120
  fix a b c :: "'a extended"
nipkow@51338
   121
  assume "a \<le> b" then show "c + a \<le> c + b"
nipkow@51338
   122
    by (cases rule: extended_cases3[of a b c]) (auto simp: add_left_mono)
nipkow@51338
   123
qed
nipkow@51338
   124
nipkow@51338
   125
instantiation extended :: (comm_monoid_add)comm_monoid_add
nipkow@51338
   126
begin
nipkow@51338
   127
nipkow@51338
   128
definition "0 = Fin 0"
nipkow@51338
   129
nipkow@51338
   130
instance
nipkow@51338
   131
proof
nipkow@51338
   132
  fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto
nipkow@51338
   133
qed
nipkow@51338
   134
nipkow@51338
   135
end
nipkow@51338
   136
nipkow@51338
   137
instantiation extended :: (uminus)uminus
nipkow@51338
   138
begin
nipkow@51338
   139
nipkow@51338
   140
fun uminus_extended where
nipkow@51338
   141
"- (Fin x) = Fin (- x)" |
nipkow@51338
   142
"- Pinf    = Minf" |
nipkow@51338
   143
"- Minf    = Pinf"
nipkow@51338
   144
nipkow@51338
   145
instance ..
nipkow@51338
   146
nipkow@51338
   147
end
nipkow@51338
   148
nipkow@51338
   149
nipkow@51338
   150
instantiation extended :: (ab_group_add)minus
nipkow@51338
   151
begin
nipkow@51338
   152
definition "x - y = x + -(y::'a extended)"
nipkow@51338
   153
instance ..
nipkow@51338
   154
end
nipkow@51338
   155
nipkow@51338
   156
lemma minus_extended_simps[simp]:
nipkow@51338
   157
  "Fin x - Fin y = Fin(x - y)"
nipkow@51338
   158
  "Fin x - Pinf  = Minf"
nipkow@51338
   159
  "Fin x - Minf  = Pinf"
nipkow@51338
   160
  "Pinf  - Fin y = Pinf"
nipkow@51338
   161
  "Pinf  - Minf  = Pinf"
nipkow@51338
   162
  "Minf  - Fin y = Minf"
nipkow@51338
   163
  "Minf  - Pinf  = Minf"
nipkow@51338
   164
  "Minf  - Minf  = Pinf"
nipkow@51338
   165
  "Pinf  - Pinf  = Pinf"
nipkow@51338
   166
by (simp_all add: minus_extended_def)
nipkow@51338
   167
nipkow@51338
   168
instantiation extended :: (lattice)bounded_lattice
nipkow@51338
   169
begin
nipkow@51338
   170
nipkow@51338
   171
definition "bot = Minf"
nipkow@51338
   172
definition "top = Pinf"
nipkow@51338
   173
nipkow@51338
   174
fun inf_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
nipkow@51338
   175
"inf_extended (Fin i) (Fin j) = Fin (inf i j)" |
nipkow@51338
   176
"inf_extended a Minf = Minf" |
nipkow@51338
   177
"inf_extended Minf a = Minf" |
nipkow@51338
   178
"inf_extended Pinf a = a" |
nipkow@51338
   179
"inf_extended a Pinf = a"
nipkow@51338
   180
nipkow@51338
   181
fun sup_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
nipkow@51338
   182
"sup_extended (Fin i) (Fin j) = Fin (sup i j)" |
nipkow@51338
   183
"sup_extended a Pinf = Pinf" |
nipkow@51338
   184
"sup_extended Pinf a = Pinf" |
nipkow@51338
   185
"sup_extended Minf a = a" |
nipkow@51338
   186
"sup_extended a Minf = a"
nipkow@51338
   187
nipkow@51338
   188
instance
nipkow@51338
   189
proof
nipkow@51338
   190
  fix x y z ::"'a extended"
nipkow@51338
   191
  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"
nipkow@51338
   192
    "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"
nipkow@51338
   193
    apply (atomize (full))
nipkow@51338
   194
    apply (cases rule: extended_cases3[of x y z])
nipkow@51338
   195
    apply (auto simp: bot_extended_def top_extended_def)
nipkow@51338
   196
    done
nipkow@51338
   197
qed
nipkow@51338
   198
end
nipkow@51338
   199
nipkow@51338
   200
end
nipkow@51338
   201