1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Extended.thy	Tue Mar 05 15:27:08 2013 +0100
     1.3 @@ -0,0 +1,201 @@
     1.4 +(*  Author:     Tobias Nipkow, TU München
     1.5 +
     1.6 +A theory of types extended with a greatest and a least element.
     1.7 +Oriented towards numeric types, hence "\<infinity>" and "-\<infinity>".
     1.8 +*)
     1.9 +
    1.10 +theory Extended
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
    1.15 +
    1.16 +lemmas extended_cases2 = extended.exhaust[case_product extended.exhaust]
    1.17 +lemmas extended_cases3 = extended.exhaust[case_product extended_cases2]
    1.18 +
    1.19 +instantiation extended :: (order)order
    1.20 +begin
    1.21 +
    1.22 +fun less_eq_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
    1.23 +"Fin x \<le> Fin y = (x \<le> y)" |
    1.24 +"_     \<le> Pinf  = True" |
    1.25 +"Minf  \<le> _     = True" |
    1.26 +"(_::'a extended) \<le> _     = False"
    1.27 +
    1.28 +lemma less_eq_extended_cases:
    1.29 +  "x \<le> y = (case x of Fin x \<Rightarrow> (case y of Fin y \<Rightarrow> x \<le> y | Pinf \<Rightarrow> True | Minf \<Rightarrow> False)
    1.30 +            | Pinf \<Rightarrow> y=Pinf | Minf \<Rightarrow> True)"
    1.31 +by(induct x y rule: less_eq_extended.induct)(auto split: extended.split)
    1.32 +
    1.33 +definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
    1.34 +"((x::'a extended) < y) = (x \<le> y & \<not> x \<ge> y)"
    1.35 +
    1.36 +instance
    1.37 +proof
    1.38 +  case goal1 show ?case by(rule less_extended_def)
    1.39 +next
    1.40 +  case goal2 show ?case by(cases x) auto
    1.41 +next
    1.42 +  case goal3 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
    1.43 +next
    1.44 +  case goal4 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
    1.45 +qed
    1.46 +
    1.47 +end
    1.48 +
    1.49 +instance extended :: (linorder)linorder
    1.50 +proof
    1.51 +  case goal1 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
    1.52 +qed
    1.53 +
    1.54 +lemma Minf_le[simp]: "Minf \<le> y"
    1.55 +by(cases y) auto
    1.56 +lemma le_Pinf[simp]: "x \<le> Pinf"
    1.57 +by(cases x) auto
    1.58 +lemma le_Minf[simp]: "x \<le> Minf \<longleftrightarrow> x = Minf"
    1.59 +by(cases x) auto
    1.60 +lemma Pinf_le[simp]: "Pinf \<le> x \<longleftrightarrow> x = Pinf"
    1.61 +by(cases x) auto
    1.62 +
    1.63 +lemma less_extended_simps[simp]:
    1.64 +  "Fin x < Fin y = (x < y)"
    1.65 +  "Fin x < Pinf  = True"
    1.66 +  "Fin x < Minf  = False"
    1.67 +  "Pinf < h      = False"
    1.68 +  "Minf < Fin x  = True"
    1.69 +  "Minf < Pinf   = True"
    1.70 +  "l    < Minf   = False"
    1.71 +by (auto simp add: less_extended_def)
    1.72 +
    1.73 +lemma min_extended_simps[simp]:
    1.74 +  "min (Fin x) (Fin y) = Fin(min x y)"
    1.75 +  "min xx      Pinf    = xx"
    1.76 +  "min xx      Minf    = Minf"
    1.77 +  "min Pinf    yy      = yy"
    1.78 +  "min Minf    yy      = Minf"
    1.79 +by (auto simp add: min_def)
    1.80 +
    1.81 +lemma max_extended_simps[simp]:
    1.82 +  "max (Fin x) (Fin y) = Fin(max x y)"
    1.83 +  "max xx      Pinf    = Pinf"
    1.84 +  "max xx      Minf    = xx"
    1.85 +  "max Pinf    yy      = Pinf"
    1.86 +  "max Minf    yy      = yy"
    1.87 +by (auto simp add: max_def)
    1.88 +
    1.89 +
    1.90 +instantiation extended :: (plus)plus
    1.91 +begin
    1.92 +
    1.93 +text {* The following definition of of addition is totalized
    1.94 +to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined. *}
    1.95 +
    1.96 +fun plus_extended where
    1.97 +"Fin x + Fin y = Fin(x+y)" |
    1.98 +"Fin x + Pinf  = Pinf" |
    1.99 +"Pinf  + Fin x = Pinf" |
   1.100 +"Pinf  + Pinf  = Pinf" |
   1.101 +"Minf  + Fin y = Minf" |
   1.102 +"Fin x + Minf  = Minf" |
   1.103 +"Minf  + Minf  = Minf" |
   1.104 +"Minf  + Pinf  = Pinf" |
   1.105 +"Pinf  + Minf  = Pinf"
   1.106 +
   1.107 +instance ..
   1.108 +
   1.109 +end
   1.110 +
   1.111 +
   1.112 +instance extended :: (ab_semigroup_add)ab_semigroup_add
   1.113 +proof
   1.114 +  fix a b c :: "'a extended"
   1.115 +  show "a + b = b + a"
   1.116 +    by (induct a b rule: plus_extended.induct) (simp_all add: ac_simps)
   1.117 +  show "a + b + c = a + (b + c)"
   1.118 +    by (cases rule: extended_cases3[of a b c]) (simp_all add: ac_simps)
   1.119 +qed
   1.120 +
   1.121 +instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add
   1.122 +proof
   1.123 +  fix a b c :: "'a extended"
   1.124 +  assume "a \<le> b" then show "c + a \<le> c + b"
   1.125 +    by (cases rule: extended_cases3[of a b c]) (auto simp: add_left_mono)
   1.126 +qed
   1.127 +
   1.128 +instantiation extended :: (comm_monoid_add)comm_monoid_add
   1.129 +begin
   1.130 +
   1.131 +definition "0 = Fin 0"
   1.132 +
   1.133 +instance
   1.134 +proof
   1.135 +  fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto
   1.136 +qed
   1.137 +
   1.138 +end
   1.139 +
   1.140 +instantiation extended :: (uminus)uminus
   1.141 +begin
   1.142 +
   1.143 +fun uminus_extended where
   1.144 +"- (Fin x) = Fin (- x)" |
   1.145 +"- Pinf    = Minf" |
   1.146 +"- Minf    = Pinf"
   1.147 +
   1.148 +instance ..
   1.149 +
   1.150 +end
   1.151 +
   1.152 +
   1.153 +instantiation extended :: (ab_group_add)minus
   1.154 +begin
   1.155 +definition "x - y = x + -(y::'a extended)"
   1.156 +instance ..
   1.157 +end
   1.158 +
   1.159 +lemma minus_extended_simps[simp]:
   1.160 +  "Fin x - Fin y = Fin(x - y)"
   1.161 +  "Fin x - Pinf  = Minf"
   1.162 +  "Fin x - Minf  = Pinf"
   1.163 +  "Pinf  - Fin y = Pinf"
   1.164 +  "Pinf  - Minf  = Pinf"
   1.165 +  "Minf  - Fin y = Minf"
   1.166 +  "Minf  - Pinf  = Minf"
   1.167 +  "Minf  - Minf  = Pinf"
   1.168 +  "Pinf  - Pinf  = Pinf"
   1.169 +by (simp_all add: minus_extended_def)
   1.170 +
   1.171 +instantiation extended :: (lattice)bounded_lattice
   1.172 +begin
   1.173 +
   1.174 +definition "bot = Minf"
   1.175 +definition "top = Pinf"
   1.176 +
   1.177 +fun inf_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
   1.178 +"inf_extended (Fin i) (Fin j) = Fin (inf i j)" |
   1.179 +"inf_extended a Minf = Minf" |
   1.180 +"inf_extended Minf a = Minf" |
   1.181 +"inf_extended Pinf a = a" |
   1.182 +"inf_extended a Pinf = a"
   1.183 +
   1.184 +fun sup_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
   1.185 +"sup_extended (Fin i) (Fin j) = Fin (sup i j)" |
   1.186 +"sup_extended a Pinf = Pinf" |
   1.187 +"sup_extended Pinf a = Pinf" |
   1.188 +"sup_extended Minf a = a" |
   1.189 +"sup_extended a Minf = a"
   1.190 +
   1.191 +instance
   1.192 +proof
   1.193 +  fix x y z ::"'a extended"
   1.194 +  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"
   1.195 +    "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"
   1.196 +    apply (atomize (full))
   1.197 +    apply (cases rule: extended_cases3[of x y z])
   1.198 +    apply (auto simp: bot_extended_def top_extended_def)
   1.199 +    done
   1.200 +qed
   1.201 +end
   1.202 +
   1.203 +end
   1.204 +

     2.1 --- a/src/HOL/Library/Library.thy	Tue Mar 05 13:03:24 2013 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Tue Mar 05 15:27:08 2013 +0100
     2.3 @@ -17,7 +17,7 @@
     2.4    Diagonal_Subsequence
     2.5    Dlist
     2.6    Eval_Witness
     2.7 -  Extended_Nat
     2.8 +  Extended Extended_Nat Extended_Real
     2.9    FinFun
    2.10    Float
    2.11    Formal_Power_Series