src/HOL/Library/Extended.thy
author wenzelm
Wed, 17 Jun 2015 11:03:05 +0200
changeset 60500 903bb1495239
parent 60343 063698416239
child 65366 10ca63a18e56
permissions -rw-r--r--
isabelle update_cartouches;
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
53427
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
     8
imports
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
     9
  Main
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
    10
  "~~/src/HOL/Library/Simps_Case_Conv"
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    11
begin
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    12
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    13
datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    14
51357
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    15
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    16
instantiation extended :: (order)order
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    17
begin
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    18
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    19
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
    20
"Fin x \<le> Fin y = (x \<le> y)" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    21
"_     \<le> Pinf  = True" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    22
"Minf  \<le> _     = True" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    23
"(_::'a extended) \<le> _     = False"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    24
53427
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
    25
case_of_simps less_eq_extended_case: less_eq_extended.simps
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    26
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    27
definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
60343
063698416239 correct sort constraints for abbreviations in type classes
haftmann
parents: 58310
diff changeset
    28
"((x::'a extended) < y) = (x \<le> y & \<not> y \<le> x)"
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    29
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    30
instance
53427
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
    31
  by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    32
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    33
end
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    34
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    35
instance extended :: (linorder)linorder
53427
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
    36
  by intro_classes (auto simp: less_eq_extended_case split:extended.splits)
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    37
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    38
lemma Minf_le[simp]: "Minf \<le> y"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    39
by(cases y) auto
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    40
lemma le_Pinf[simp]: "x \<le> Pinf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    41
by(cases x) auto
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    42
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
    43
by(cases x) auto
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    44
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
    45
by(cases x) auto
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
lemma less_extended_simps[simp]:
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    48
  "Fin x < Fin y = (x < y)"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    49
  "Fin x < Pinf  = True"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    50
  "Fin x < Minf  = False"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    51
  "Pinf < h      = False"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    52
  "Minf < Fin x  = True"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    53
  "Minf < Pinf   = True"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    54
  "l    < Minf   = False"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    55
by (auto simp add: less_extended_def)
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    56
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    57
lemma min_extended_simps[simp]:
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    58
  "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
    59
  "min xx      Pinf    = xx"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    60
  "min xx      Minf    = Minf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    61
  "min Pinf    yy      = yy"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    62
  "min Minf    yy      = Minf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    63
by (auto simp add: min_def)
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    64
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    65
lemma max_extended_simps[simp]:
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    66
  "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
    67
  "max xx      Pinf    = Pinf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    68
  "max xx      Minf    = xx"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    69
  "max Pinf    yy      = Pinf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    70
  "max Minf    yy      = yy"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    71
by (auto simp add: max_def)
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    72
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    73
51357
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    74
instantiation extended :: (zero)zero
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    75
begin
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    76
definition "0 = Fin(0::'a)"
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    77
instance ..
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    78
end
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    79
55124
ffabc0a5853e hide extended.Fin in code generator output
hoelzl
parents: 54489
diff changeset
    80
declare zero_extended_def[symmetric, code_post]
ffabc0a5853e hide extended.Fin in code generator output
hoelzl
parents: 54489
diff changeset
    81
51357
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    82
instantiation extended :: (one)one
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    83
begin
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    84
definition "1 = Fin(1::'a)"
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    85
instance ..
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    86
end
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
    87
55124
ffabc0a5853e hide extended.Fin in code generator output
hoelzl
parents: 54489
diff changeset
    88
declare one_extended_def[symmetric, code_post]
ffabc0a5853e hide extended.Fin in code generator output
hoelzl
parents: 54489
diff changeset
    89
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    90
instantiation extended :: (plus)plus
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    91
begin
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    92
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60343
diff changeset
    93
text \<open>The following definition of of addition is totalized
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60343
diff changeset
    94
to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined.\<close>
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    95
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    96
fun plus_extended where
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    97
"Fin x + Fin y = Fin(x+y)" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    98
"Fin x + Pinf  = Pinf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
    99
"Pinf  + Fin x = Pinf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   100
"Pinf  + Pinf  = Pinf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   101
"Minf  + Fin y = Minf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   102
"Fin x + Minf  = Minf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   103
"Minf  + Minf  = Minf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   104
"Minf  + Pinf  = Pinf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   105
"Pinf  + Minf  = Pinf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   106
53427
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
   107
case_of_simps plus_case: plus_extended.simps
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
   108
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   109
instance ..
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   110
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   111
end
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   112
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   113
53427
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
   114
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   115
instance extended :: (ab_semigroup_add)ab_semigroup_add
53427
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
   116
  by intro_classes (simp_all add: ac_simps plus_case split: extended.splits)
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   117
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   118
instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add
53427
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
   119
  by intro_classes (auto simp: add_left_mono plus_case split: extended.splits)
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   120
51357
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
   121
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
   122
proof
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   123
  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
   124
qed
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   125
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   126
instantiation extended :: (uminus)uminus
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   127
begin
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   128
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   129
fun uminus_extended where
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   130
"- (Fin x) = Fin (- x)" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   131
"- Pinf    = Minf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   132
"- Minf    = Pinf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   133
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   134
instance ..
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   135
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   136
end
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   137
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   138
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   139
instantiation extended :: (ab_group_add)minus
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   140
begin
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   141
definition "x - y = x + -(y::'a extended)"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   142
instance ..
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   143
end
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   144
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   145
lemma minus_extended_simps[simp]:
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   146
  "Fin x - Fin y = Fin(x - y)"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   147
  "Fin x - Pinf  = Minf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   148
  "Fin x - Minf  = Pinf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   149
  "Pinf  - Fin y = Pinf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   150
  "Pinf  - Minf  = Pinf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   151
  "Minf  - Fin y = Minf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   152
  "Minf  - Pinf  = Minf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   153
  "Minf  - Minf  = Pinf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   154
  "Pinf  - Pinf  = Pinf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   155
by (simp_all add: minus_extended_def)
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   156
51357
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
   157
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60343
diff changeset
   158
text\<open>Numerals:\<close>
51357
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
   159
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
   160
instance extended :: ("{ab_semigroup_add,one}")numeral ..
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
   161
55124
ffabc0a5853e hide extended.Fin in code generator output
hoelzl
parents: 54489
diff changeset
   162
lemma Fin_numeral[code_post]: "Fin(numeral w) = numeral w"
51357
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
   163
  apply (induct w rule: num_induct)
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
   164
  apply (simp only: numeral_One one_extended_def)
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
   165
  apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
   166
  done
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
   167
55124
ffabc0a5853e hide extended.Fin in code generator output
hoelzl
parents: 54489
diff changeset
   168
lemma Fin_neg_numeral[code_post]: "Fin (- numeral w) = - numeral w"
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 53427
diff changeset
   169
by (simp only: Fin_numeral uminus_extended.simps[symmetric])
51358
0c376ef98559 added lemma
nipkow
parents: 51357
diff changeset
   170
51357
ac4c1cf1b001 extended numerals
nipkow
parents: 51338
diff changeset
   171
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   172
instantiation extended :: (lattice)bounded_lattice
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   173
begin
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   174
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   175
definition "bot = Minf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   176
definition "top = Pinf"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   177
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   178
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
   179
"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
   180
"inf_extended a Minf = Minf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   181
"inf_extended Minf a = Minf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   182
"inf_extended Pinf a = a" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   183
"inf_extended a Pinf = a"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   184
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   185
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
   186
"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
   187
"sup_extended a Pinf = Pinf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   188
"sup_extended Pinf a = Pinf" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   189
"sup_extended Minf a = a" |
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   190
"sup_extended a Minf = a"
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   191
53427
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
   192
case_of_simps inf_extended_case: inf_extended.simps
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
   193
case_of_simps sup_extended_case: sup_extended.simps
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
   194
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   195
instance
53427
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
   196
  by (intro_classes) (auto simp: inf_extended_case sup_extended_case less_eq_extended_case
415354b68f0c use case_of_simps
noschinl
parents: 51358
diff changeset
   197
    bot_extended_def top_extended_def split: extended.splits)
51338
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   198
end
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   199
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   200
end
054d1653950f New theory of infinity-extended types; should replace Extended_xyz eventually
nipkow
parents:
diff changeset
   201