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