nipkow@51338: (*  Author:     Tobias Nipkow, TU München
nipkow@51338: 
nipkow@51338: A theory of types extended with a greatest and a least element.
nipkow@51338: Oriented towards numeric types, hence "\<infinity>" and "-\<infinity>".
nipkow@51338: *)
nipkow@51338: 
nipkow@51338: theory Extended
noschinl@53427: imports
noschinl@53427:   Main
noschinl@53427:   "~~/src/HOL/Library/Simps_Case_Conv"
nipkow@51338: begin
nipkow@51338: 
blanchet@58310: datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
nipkow@51338: 
nipkow@51357: 
nipkow@51338: instantiation extended :: (order)order
nipkow@51338: begin
nipkow@51338: 
nipkow@51338: fun less_eq_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
nipkow@51338: "Fin x \<le> Fin y = (x \<le> y)" |
nipkow@51338: "_     \<le> Pinf  = True" |
nipkow@51338: "Minf  \<le> _     = True" |
nipkow@51338: "(_::'a extended) \<le> _     = False"
nipkow@51338: 
noschinl@53427: case_of_simps less_eq_extended_case: less_eq_extended.simps
nipkow@51338: 
nipkow@51338: definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
nipkow@51338: "((x::'a extended) < y) = (x \<le> y & \<not> x \<ge> y)"
nipkow@51338: 
nipkow@51338: instance
noschinl@53427:   by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
nipkow@51338: 
nipkow@51338: end
nipkow@51338: 
nipkow@51338: instance extended :: (linorder)linorder
noschinl@53427:   by intro_classes (auto simp: less_eq_extended_case split:extended.splits)
nipkow@51338: 
nipkow@51338: lemma Minf_le[simp]: "Minf \<le> y"
nipkow@51338: by(cases y) auto
nipkow@51338: lemma le_Pinf[simp]: "x \<le> Pinf"
nipkow@51338: by(cases x) auto
nipkow@51338: lemma le_Minf[simp]: "x \<le> Minf \<longleftrightarrow> x = Minf"
nipkow@51338: by(cases x) auto
nipkow@51338: lemma Pinf_le[simp]: "Pinf \<le> x \<longleftrightarrow> x = Pinf"
nipkow@51338: by(cases x) auto
nipkow@51338: 
nipkow@51338: lemma less_extended_simps[simp]:
nipkow@51338:   "Fin x < Fin y = (x < y)"
nipkow@51338:   "Fin x < Pinf  = True"
nipkow@51338:   "Fin x < Minf  = False"
nipkow@51338:   "Pinf < h      = False"
nipkow@51338:   "Minf < Fin x  = True"
nipkow@51338:   "Minf < Pinf   = True"
nipkow@51338:   "l    < Minf   = False"
nipkow@51338: by (auto simp add: less_extended_def)
nipkow@51338: 
nipkow@51338: lemma min_extended_simps[simp]:
nipkow@51338:   "min (Fin x) (Fin y) = Fin(min x y)"
nipkow@51338:   "min xx      Pinf    = xx"
nipkow@51338:   "min xx      Minf    = Minf"
nipkow@51338:   "min Pinf    yy      = yy"
nipkow@51338:   "min Minf    yy      = Minf"
nipkow@51338: by (auto simp add: min_def)
nipkow@51338: 
nipkow@51338: lemma max_extended_simps[simp]:
nipkow@51338:   "max (Fin x) (Fin y) = Fin(max x y)"
nipkow@51338:   "max xx      Pinf    = Pinf"
nipkow@51338:   "max xx      Minf    = xx"
nipkow@51338:   "max Pinf    yy      = Pinf"
nipkow@51338:   "max Minf    yy      = yy"
nipkow@51338: by (auto simp add: max_def)
nipkow@51338: 
nipkow@51338: 
nipkow@51357: instantiation extended :: (zero)zero
nipkow@51357: begin
nipkow@51357: definition "0 = Fin(0::'a)"
nipkow@51357: instance ..
nipkow@51357: end
nipkow@51357: 
hoelzl@55124: declare zero_extended_def[symmetric, code_post]
hoelzl@55124: 
nipkow@51357: instantiation extended :: (one)one
nipkow@51357: begin
nipkow@51357: definition "1 = Fin(1::'a)"
nipkow@51357: instance ..
nipkow@51357: end
nipkow@51357: 
hoelzl@55124: declare one_extended_def[symmetric, code_post]
hoelzl@55124: 
nipkow@51338: instantiation extended :: (plus)plus
nipkow@51338: begin
nipkow@51338: 
nipkow@51338: text {* The following definition of of addition is totalized
nipkow@51338: to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined. *}
nipkow@51338: 
nipkow@51338: fun plus_extended where
nipkow@51338: "Fin x + Fin y = Fin(x+y)" |
nipkow@51338: "Fin x + Pinf  = Pinf" |
nipkow@51338: "Pinf  + Fin x = Pinf" |
nipkow@51338: "Pinf  + Pinf  = Pinf" |
nipkow@51338: "Minf  + Fin y = Minf" |
nipkow@51338: "Fin x + Minf  = Minf" |
nipkow@51338: "Minf  + Minf  = Minf" |
nipkow@51338: "Minf  + Pinf  = Pinf" |
nipkow@51338: "Pinf  + Minf  = Pinf"
nipkow@51338: 
noschinl@53427: case_of_simps plus_case: plus_extended.simps
noschinl@53427: 
nipkow@51338: instance ..
nipkow@51338: 
nipkow@51338: end
nipkow@51338: 
nipkow@51338: 
noschinl@53427: 
nipkow@51338: instance extended :: (ab_semigroup_add)ab_semigroup_add
noschinl@53427:   by intro_classes (simp_all add: ac_simps plus_case split: extended.splits)
nipkow@51338: 
nipkow@51338: instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add
noschinl@53427:   by intro_classes (auto simp: add_left_mono plus_case split: extended.splits)
nipkow@51338: 
nipkow@51357: instance extended :: (comm_monoid_add)comm_monoid_add
nipkow@51338: proof
nipkow@51338:   fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto
nipkow@51338: qed
nipkow@51338: 
nipkow@51338: instantiation extended :: (uminus)uminus
nipkow@51338: begin
nipkow@51338: 
nipkow@51338: fun uminus_extended where
nipkow@51338: "- (Fin x) = Fin (- x)" |
nipkow@51338: "- Pinf    = Minf" |
nipkow@51338: "- Minf    = Pinf"
nipkow@51338: 
nipkow@51338: instance ..
nipkow@51338: 
nipkow@51338: end
nipkow@51338: 
nipkow@51338: 
nipkow@51338: instantiation extended :: (ab_group_add)minus
nipkow@51338: begin
nipkow@51338: definition "x - y = x + -(y::'a extended)"
nipkow@51338: instance ..
nipkow@51338: end
nipkow@51338: 
nipkow@51338: lemma minus_extended_simps[simp]:
nipkow@51338:   "Fin x - Fin y = Fin(x - y)"
nipkow@51338:   "Fin x - Pinf  = Minf"
nipkow@51338:   "Fin x - Minf  = Pinf"
nipkow@51338:   "Pinf  - Fin y = Pinf"
nipkow@51338:   "Pinf  - Minf  = Pinf"
nipkow@51338:   "Minf  - Fin y = Minf"
nipkow@51338:   "Minf  - Pinf  = Minf"
nipkow@51338:   "Minf  - Minf  = Pinf"
nipkow@51338:   "Pinf  - Pinf  = Pinf"
nipkow@51338: by (simp_all add: minus_extended_def)
nipkow@51338: 
nipkow@51357: 
nipkow@51357: text{* Numerals: *}
nipkow@51357: 
nipkow@51357: instance extended :: ("{ab_semigroup_add,one}")numeral ..
nipkow@51357: 
hoelzl@55124: lemma Fin_numeral[code_post]: "Fin(numeral w) = numeral w"
nipkow@51357:   apply (induct w rule: num_induct)
nipkow@51357:   apply (simp only: numeral_One one_extended_def)
nipkow@51357:   apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
nipkow@51357:   done
nipkow@51357: 
hoelzl@55124: lemma Fin_neg_numeral[code_post]: "Fin (- numeral w) = - numeral w"
haftmann@54489: by (simp only: Fin_numeral uminus_extended.simps[symmetric])
nipkow@51358: 
nipkow@51357: 
nipkow@51338: instantiation extended :: (lattice)bounded_lattice
nipkow@51338: begin
nipkow@51338: 
nipkow@51338: definition "bot = Minf"
nipkow@51338: definition "top = Pinf"
nipkow@51338: 
nipkow@51338: fun inf_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
nipkow@51338: "inf_extended (Fin i) (Fin j) = Fin (inf i j)" |
nipkow@51338: "inf_extended a Minf = Minf" |
nipkow@51338: "inf_extended Minf a = Minf" |
nipkow@51338: "inf_extended Pinf a = a" |
nipkow@51338: "inf_extended a Pinf = a"
nipkow@51338: 
nipkow@51338: fun sup_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
nipkow@51338: "sup_extended (Fin i) (Fin j) = Fin (sup i j)" |
nipkow@51338: "sup_extended a Pinf = Pinf" |
nipkow@51338: "sup_extended Pinf a = Pinf" |
nipkow@51338: "sup_extended Minf a = a" |
nipkow@51338: "sup_extended a Minf = a"
nipkow@51338: 
noschinl@53427: case_of_simps inf_extended_case: inf_extended.simps
noschinl@53427: case_of_simps sup_extended_case: sup_extended.simps
noschinl@53427: 
nipkow@51338: instance
noschinl@53427:   by (intro_classes) (auto simp: inf_extended_case sup_extended_case less_eq_extended_case
noschinl@53427:     bot_extended_def top_extended_def split: extended.splits)
nipkow@51338: end
nipkow@51338: 
nipkow@51338: end
nipkow@51338: