src/HOL/Library/Extended.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 67091 1393c2340eec
permissions -rw-r--r--
improved code equations taken over from AFP
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
wenzelm@65366
     8
  imports Simps_Case_Conv
nipkow@51338
     9
begin
nipkow@51338
    10
blanchet@58310
    11
datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
nipkow@51338
    12
nipkow@51357
    13
nipkow@51338
    14
instantiation extended :: (order)order
nipkow@51338
    15
begin
nipkow@51338
    16
nipkow@51338
    17
fun less_eq_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
nipkow@51338
    18
"Fin x \<le> Fin y = (x \<le> y)" |
nipkow@51338
    19
"_     \<le> Pinf  = True" |
nipkow@51338
    20
"Minf  \<le> _     = True" |
nipkow@51338
    21
"(_::'a extended) \<le> _     = False"
nipkow@51338
    22
noschinl@53427
    23
case_of_simps less_eq_extended_case: less_eq_extended.simps
nipkow@51338
    24
nipkow@51338
    25
definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
wenzelm@67091
    26
"((x::'a extended) < y) = (x \<le> y \<and> \<not> y \<le> x)"
nipkow@51338
    27
nipkow@51338
    28
instance
noschinl@53427
    29
  by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
nipkow@51338
    30
nipkow@51338
    31
end
nipkow@51338
    32
nipkow@51338
    33
instance extended :: (linorder)linorder
noschinl@53427
    34
  by intro_classes (auto simp: less_eq_extended_case split:extended.splits)
nipkow@51338
    35
nipkow@51338
    36
lemma Minf_le[simp]: "Minf \<le> y"
nipkow@51338
    37
by(cases y) auto
nipkow@51338
    38
lemma le_Pinf[simp]: "x \<le> Pinf"
nipkow@51338
    39
by(cases x) auto
nipkow@51338
    40
lemma le_Minf[simp]: "x \<le> Minf \<longleftrightarrow> x = Minf"
nipkow@51338
    41
by(cases x) auto
nipkow@51338
    42
lemma Pinf_le[simp]: "Pinf \<le> x \<longleftrightarrow> x = Pinf"
nipkow@51338
    43
by(cases x) auto
nipkow@51338
    44
nipkow@51338
    45
lemma less_extended_simps[simp]:
nipkow@51338
    46
  "Fin x < Fin y = (x < y)"
nipkow@51338
    47
  "Fin x < Pinf  = True"
nipkow@51338
    48
  "Fin x < Minf  = False"
nipkow@51338
    49
  "Pinf < h      = False"
nipkow@51338
    50
  "Minf < Fin x  = True"
nipkow@51338
    51
  "Minf < Pinf   = True"
nipkow@51338
    52
  "l    < Minf   = False"
nipkow@51338
    53
by (auto simp add: less_extended_def)
nipkow@51338
    54
nipkow@51338
    55
lemma min_extended_simps[simp]:
nipkow@51338
    56
  "min (Fin x) (Fin y) = Fin(min x y)"
nipkow@51338
    57
  "min xx      Pinf    = xx"
nipkow@51338
    58
  "min xx      Minf    = Minf"
nipkow@51338
    59
  "min Pinf    yy      = yy"
nipkow@51338
    60
  "min Minf    yy      = Minf"
nipkow@51338
    61
by (auto simp add: min_def)
nipkow@51338
    62
nipkow@51338
    63
lemma max_extended_simps[simp]:
nipkow@51338
    64
  "max (Fin x) (Fin y) = Fin(max x y)"
nipkow@51338
    65
  "max xx      Pinf    = Pinf"
nipkow@51338
    66
  "max xx      Minf    = xx"
nipkow@51338
    67
  "max Pinf    yy      = Pinf"
nipkow@51338
    68
  "max Minf    yy      = yy"
nipkow@51338
    69
by (auto simp add: max_def)
nipkow@51338
    70
nipkow@51338
    71
nipkow@51357
    72
instantiation extended :: (zero)zero
nipkow@51357
    73
begin
nipkow@51357
    74
definition "0 = Fin(0::'a)"
nipkow@51357
    75
instance ..
nipkow@51357
    76
end
nipkow@51357
    77
hoelzl@55124
    78
declare zero_extended_def[symmetric, code_post]
hoelzl@55124
    79
nipkow@51357
    80
instantiation extended :: (one)one
nipkow@51357
    81
begin
nipkow@51357
    82
definition "1 = Fin(1::'a)"
nipkow@51357
    83
instance ..
nipkow@51357
    84
end
nipkow@51357
    85
hoelzl@55124
    86
declare one_extended_def[symmetric, code_post]
hoelzl@55124
    87
nipkow@51338
    88
instantiation extended :: (plus)plus
nipkow@51338
    89
begin
nipkow@51338
    90
wenzelm@60500
    91
text \<open>The following definition of of addition is totalized
wenzelm@60500
    92
to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined.\<close>
nipkow@51338
    93
nipkow@51338
    94
fun plus_extended where
nipkow@51338
    95
"Fin x + Fin y = Fin(x+y)" |
nipkow@51338
    96
"Fin x + Pinf  = Pinf" |
nipkow@51338
    97
"Pinf  + Fin x = Pinf" |
nipkow@51338
    98
"Pinf  + Pinf  = Pinf" |
nipkow@51338
    99
"Minf  + Fin y = Minf" |
nipkow@51338
   100
"Fin x + Minf  = Minf" |
nipkow@51338
   101
"Minf  + Minf  = Minf" |
nipkow@51338
   102
"Minf  + Pinf  = Pinf" |
nipkow@51338
   103
"Pinf  + Minf  = Pinf"
nipkow@51338
   104
noschinl@53427
   105
case_of_simps plus_case: plus_extended.simps
noschinl@53427
   106
nipkow@51338
   107
instance ..
nipkow@51338
   108
nipkow@51338
   109
end
nipkow@51338
   110
nipkow@51338
   111
noschinl@53427
   112
nipkow@51338
   113
instance extended :: (ab_semigroup_add)ab_semigroup_add
noschinl@53427
   114
  by intro_classes (simp_all add: ac_simps plus_case split: extended.splits)
nipkow@51338
   115
nipkow@51338
   116
instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add
noschinl@53427
   117
  by intro_classes (auto simp: add_left_mono plus_case split: extended.splits)
nipkow@51338
   118
nipkow@51357
   119
instance extended :: (comm_monoid_add)comm_monoid_add
nipkow@51338
   120
proof
nipkow@51338
   121
  fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto
nipkow@51338
   122
qed
nipkow@51338
   123
nipkow@51338
   124
instantiation extended :: (uminus)uminus
nipkow@51338
   125
begin
nipkow@51338
   126
nipkow@51338
   127
fun uminus_extended where
nipkow@51338
   128
"- (Fin x) = Fin (- x)" |
nipkow@51338
   129
"- Pinf    = Minf" |
nipkow@51338
   130
"- Minf    = Pinf"
nipkow@51338
   131
nipkow@51338
   132
instance ..
nipkow@51338
   133
nipkow@51338
   134
end
nipkow@51338
   135
nipkow@51338
   136
nipkow@51338
   137
instantiation extended :: (ab_group_add)minus
nipkow@51338
   138
begin
nipkow@51338
   139
definition "x - y = x + -(y::'a extended)"
nipkow@51338
   140
instance ..
nipkow@51338
   141
end
nipkow@51338
   142
nipkow@51338
   143
lemma minus_extended_simps[simp]:
nipkow@51338
   144
  "Fin x - Fin y = Fin(x - y)"
nipkow@51338
   145
  "Fin x - Pinf  = Minf"
nipkow@51338
   146
  "Fin x - Minf  = Pinf"
nipkow@51338
   147
  "Pinf  - Fin y = Pinf"
nipkow@51338
   148
  "Pinf  - Minf  = Pinf"
nipkow@51338
   149
  "Minf  - Fin y = Minf"
nipkow@51338
   150
  "Minf  - Pinf  = Minf"
nipkow@51338
   151
  "Minf  - Minf  = Pinf"
nipkow@51338
   152
  "Pinf  - Pinf  = Pinf"
nipkow@51338
   153
by (simp_all add: minus_extended_def)
nipkow@51338
   154
nipkow@51357
   155
wenzelm@60500
   156
text\<open>Numerals:\<close>
nipkow@51357
   157
nipkow@51357
   158
instance extended :: ("{ab_semigroup_add,one}")numeral ..
nipkow@51357
   159
hoelzl@55124
   160
lemma Fin_numeral[code_post]: "Fin(numeral w) = numeral w"
nipkow@51357
   161
  apply (induct w rule: num_induct)
nipkow@51357
   162
  apply (simp only: numeral_One one_extended_def)
nipkow@51357
   163
  apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
nipkow@51357
   164
  done
nipkow@51357
   165
hoelzl@55124
   166
lemma Fin_neg_numeral[code_post]: "Fin (- numeral w) = - numeral w"
haftmann@54489
   167
by (simp only: Fin_numeral uminus_extended.simps[symmetric])
nipkow@51358
   168
nipkow@51357
   169
nipkow@51338
   170
instantiation extended :: (lattice)bounded_lattice
nipkow@51338
   171
begin
nipkow@51338
   172
nipkow@51338
   173
definition "bot = Minf"
nipkow@51338
   174
definition "top = Pinf"
nipkow@51338
   175
nipkow@51338
   176
fun inf_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
nipkow@51338
   177
"inf_extended (Fin i) (Fin j) = Fin (inf i j)" |
nipkow@51338
   178
"inf_extended a Minf = Minf" |
nipkow@51338
   179
"inf_extended Minf a = Minf" |
nipkow@51338
   180
"inf_extended Pinf a = a" |
nipkow@51338
   181
"inf_extended a Pinf = a"
nipkow@51338
   182
nipkow@51338
   183
fun sup_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
nipkow@51338
   184
"sup_extended (Fin i) (Fin j) = Fin (sup i j)" |
nipkow@51338
   185
"sup_extended a Pinf = Pinf" |
nipkow@51338
   186
"sup_extended Pinf a = Pinf" |
nipkow@51338
   187
"sup_extended Minf a = a" |
nipkow@51338
   188
"sup_extended a Minf = a"
nipkow@51338
   189
noschinl@53427
   190
case_of_simps inf_extended_case: inf_extended.simps
noschinl@53427
   191
case_of_simps sup_extended_case: sup_extended.simps
noschinl@53427
   192
nipkow@51338
   193
instance
noschinl@53427
   194
  by (intro_classes) (auto simp: inf_extended_case sup_extended_case less_eq_extended_case
noschinl@53427
   195
    bot_extended_def top_extended_def split: extended.splits)
nipkow@51338
   196
end
nipkow@51338
   197
nipkow@51338
   198
end
nipkow@51338
   199