Quelle Extended_Nat.thy Sprache: Isabelle

(*  Title:      HOL/Library/Extended_Nat.thy
    Author:     David von Oheimb, TU Muenchen;  Florian Haftmann, TU Muenchen
    Contributions: David Trachtenherz, TU Muenchen
*)

section \<open>Extended natural numbers (i.e. with infinity)\<close>

theory Extended_Nat
imports Main Countable Order_Continuity
begin

class infinity =
  fixes infinity :: "'a"  (\<open>\<infinity>\<close>)

context
  fixes f :: "nat \ 'a::{canonically_ordered_monoid_add, linorder_topology, complete_linorder}"
begin

lemma sums_SUP[simp, intro]: "f sums (SUP n. \i
  unfolding sums_def by (intro LIMSEQ_SUP monoI sum_mono2 zero_le) auto

lemma suminf_eq_SUP: "suminf f = (SUP n. \i
  using sums_SUP by (rule sums_unique[symmetric])

end

subsection \<open>Type definition\<close>

text \<open>
  We extend the standard natural numbers by a special value indicating
  infinity.
\<close>

typedef enat = "UNIV :: nat option set" ..

text \<open>TODO: introduce enat as coinductive datatype, enat is just \<^const>\<open>of_nat\<close>\<close>

definition enat :: "nat \ enat" where
  "enat n = Abs_enat (Some n)"

instantiation enat :: infinity
begin

definition "\ = Abs_enat None"
instance ..

end

instance enat :: countable
proof
  show "\to_nat::enat \ nat. inj to_nat"
    by (rule exI[of _ "to_nat \ Rep_enat"]) (simp add: inj_on_def Rep_enat_inject)
qed

old_rep_datatype enat "\ :: enat"
proof -
  fix P i assume "\j. P (enat j)" "P \"
  then show "P i"
  proof induct
    case (Abs_enat y) then show ?case
      by (cases y rule: option.exhaust)
         (auto simp: enat_def infinity_enat_def)
  qed
qed (auto simp add: enat_def infinity_enat_def Abs_enat_inject)

declare [[coercion "enat::nat\enat"]]

lemmas enat2_cases = enat.exhaust[case_product enat.exhaust]
lemmas enat3_cases = enat.exhaust[case_product enat.exhaust enat.exhaust]

lemma not_infinity_eq [iff]: "(x \ \) = (\i. x = enat i)"
  by (cases x) auto

lemma not_enat_eq [iff]: "(\y. x \ enat y) = (x = \)"
  by (cases x) auto

lemma enat_ex_split: "(\c::enat. P c) \ P \ \ (\c::nat. P c)"
  by (metis enat.exhaust)

primrec the_enat :: "enat \ nat"
  where "the_enat (enat n) = n"

subsection \<open>Constructors and numbers\<close>

instantiation enat :: zero_neq_one
begin

definition
  "0 = enat 0"

definition
  "1 = enat 1"

instance
  proof qed (simp add: zero_enat_def one_enat_def)

end

definition eSuc :: "enat \ enat" where
  "eSuc i = (case i of enat n \ enat (Suc n) | \ \ \)"

lemma enat_0 [code_post]: "enat 0 = 0"
  by (simp add: zero_enat_def)

lemma enat_1 [code_post]: "enat 1 = 1"
  by (simp add: one_enat_def)

lemma enat_0_iff: "enat x = 0 \ x = 0" "0 = enat x \ x = 0"
  by (auto simp add: zero_enat_def)

lemma enat_1_iff: "enat x = 1 \ x = 1" "1 = enat x \ x = 1"
  by (auto simp add: one_enat_def)

lemma one_eSuc: "1 = eSuc 0"
  by (simp add: zero_enat_def one_enat_def eSuc_def)

lemma infinity_ne_i0 [simp]: "(\::enat) \ 0"
  by (simp add: zero_enat_def)

lemma i0_ne_infinity [simp]: "0 \ (\::enat)"
  by (simp add: zero_enat_def)

lemma zero_one_enat_neq:
  "\ 0 = (1::enat)"
  "\ 1 = (0::enat)"
  unfolding zero_enat_def one_enat_def by simp_all

lemma infinity_ne_i1 [simp]: "(\::enat) \ 1"
  by (simp add: one_enat_def)

lemma i1_ne_infinity [simp]: "1 \ (\::enat)"
  by (simp add: one_enat_def)

lemma eSuc_enat: "eSuc (enat n) = enat (Suc n)"
  by (simp add: eSuc_def)

lemma eSuc_infinity [simp]: "eSuc \ = \"
  by (simp add: eSuc_def)

lemma eSuc_ne_0 [simp]: "eSuc n \ 0"
  by (simp add: eSuc_def zero_enat_def split: enat.splits)

lemma zero_ne_eSuc [simp]: "0 \ eSuc n"
  by (rule eSuc_ne_0 [symmetric])

lemma eSuc_inject [simp]: "eSuc m = eSuc n \ m = n"
  by (simp add: eSuc_def split: enat.splits)

lemma eSuc_enat_iff: "eSuc x = enat y \ (\n. y = Suc n \ x = enat n)"
  by (cases y) (auto simp: enat_0 eSuc_enat[symmetric])

lemma enat_eSuc_iff: "enat y = eSuc x \ (\n. y = Suc n \ enat n = x)"
  by (cases y) (auto simp: enat_0 eSuc_enat[symmetric])

subsection \<open>Addition\<close>

instantiation enat :: comm_monoid_add
begin

definition [nitpick_simp]:
  "m + n = (case m of \ \ \ | enat m \ (case n of \ \ \ | enat n \ enat (m + n)))"

lemma plus_enat_simps [simp, code]:
  fixes q :: enat
  shows "enat m + enat n = enat (m + n)"
    and "\ + q = \"
    and "q + \ = \"
  by (simp_all add: plus_enat_def split: enat.splits)

instance
proof
  fix n m q :: enat
  show "n + m + q = n + (m + q)"
    by (cases n m q rule: enat3_cases) auto
  show "n + m = m + n"
    by (cases n m rule: enat2_cases) auto
  show "0 + n = n"
    by (cases n) (simp_all add: zero_enat_def)
qed

end

lemma eSuc_plus_1:
  "eSuc n = n + 1"
  by (cases n) (simp_all add: eSuc_enat one_enat_def)

lemma plus_1_eSuc:
  "1 + q = eSuc q"
  "q + 1 = eSuc q"
  by (simp_all add: eSuc_plus_1 ac_simps)

lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
  by (simp add: eSuc_plus_1 ac_simps)

lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
  by (metis add.commute iadd_Suc)

subsection \<open>Multiplication\<close>

instantiation enat :: "{comm_semiring_1, semiring_no_zero_divisors}"
begin

definition times_enat_def [nitpick_simp]:
  "m * n = (case m of \ \ if n = 0 then 0 else \ | enat m \
    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | enat n \<Rightarrow> enat (m * n)))"

lemma times_enat_simps [simp, code]:
  "enat m * enat n = enat (m * n)"
  "\ * \ = (\::enat)"
  "\ * enat n = (if n = 0 then 0 else \)"
  "enat m * \ = (if m = 0 then 0 else \)"
  unfolding times_enat_def zero_enat_def
  by (simp_all split: enat.split)

instance
proof
  fix a b c :: enat
  show distr: "(a + b) * c = a * c + b * c"
    unfolding times_enat_def zero_enat_def
    by (simp split: enat.split add: distrib_right)
  show "a * (b + c) = a * b + a * c"
    by (cases a b c rule: enat3_cases) (auto simp: times_enat_def zero_enat_def distrib_left)
qed (auto simp: times_enat_def zero_enat_def one_enat_def split: enat.split)

end

lemma mult_eSuc: "eSuc m * n = n + m * n"
  unfolding eSuc_plus_1 by (simp add: algebra_simps)

lemma mult_eSuc_right: "m * eSuc n = m + m * n"
  by (metis mult.commute mult_eSuc)

lemma of_nat_eq_enat: "of_nat n = enat n"
  by (induct n) (auto simp: enat_0 plus_1_eSuc eSuc_enat)

instance enat :: semiring_char_0
proof
  have "inj enat" by (rule injI) simp
  then show "inj (\n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
qed

lemma imult_is_infinity: "((a::enat) * b = \) = (a = \ \ b \ 0 \ b = \ \ a \ 0)"
  by (auto simp add: times_enat_def zero_enat_def split: enat.split)

subsection \<open>Numerals\<close>

lemma numeral_eq_enat:
  "numeral k = enat (numeral k)"
  by (metis of_nat_eq_enat of_nat_numeral)

lemma enat_numeral [code_abbrev]:
  "enat (numeral k) = numeral k"
  using numeral_eq_enat ..

lemma infinity_ne_numeral [simp]: "(\::enat) \ numeral k"
  by (simp add: numeral_eq_enat)

lemma numeral_ne_infinity [simp]: "numeral k \ (\::enat)"
  by (simp add: numeral_eq_enat)

lemma eSuc_numeral [simp]: "eSuc (numeral k) = numeral (k + Num.One)"
  by (simp only: eSuc_plus_1 numeral_plus_one)

subsection \<open>Subtraction\<close>

instantiation enat :: minus
begin

definition diff_enat_def:
"a - b = (case a of (enat x) \ (case b of (enat y) \ enat (x - y) | \ \ 0)
          | \<infinity> \<Rightarrow> \<infinity>)"

instance ..

end

lemma idiff_enat_enat [simp, code]: "enat a - enat b = enat (a - b)"
  by (simp add: diff_enat_def)

lemma idiff_infinity [simp, code]: "\ - n = (\::enat)"
  by (simp add: diff_enat_def)

lemma idiff_infinity_right [simp, code]: "enat a - \ = 0"
  by (simp add: diff_enat_def)

lemma idiff_0 [simp]: "(0::enat) - n = 0"
  by (cases n, simp_all add: zero_enat_def)

lemmas idiff_enat_0 [simp] = idiff_0 [unfolded zero_enat_def]

lemma idiff_0_right [simp]: "(n::enat) - 0 = n"
  by (cases n) (simp_all add: zero_enat_def)

lemmas idiff_enat_0_right [simp] = idiff_0_right [unfolded zero_enat_def]

lemma idiff_self [simp]: "n \ \ \ (n::enat) - n = 0"
  by (auto simp: zero_enat_def)

lemma eSuc_minus_eSuc [simp]: "eSuc n - eSuc m = n - m"
  by (simp add: eSuc_def split: enat.split)

lemma eSuc_minus_1 [simp]: "eSuc n - 1 = n"
  by (simp add: one_enat_def flip: eSuc_enat zero_enat_def)

(*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*)

subsection \<open>Ordering\<close>

instantiation enat :: linordered_ab_semigroup_add
begin

definition [nitpick_simp]:
  "m \ n = (case n of enat n1 \ (case m of enat m1 \ m1 \ n1 | \ \ False)
    | \<infinity> \<Rightarrow> True)"

definition [nitpick_simp]:
  "m < n = (case m of enat m1 \ (case n of enat n1 \ m1 < n1 | \ \ True)
    | \<infinity> \<Rightarrow> False)"

lemma enat_ord_simps [simp]:
  "enat m \ enat n \ m \ n"
  "enat m < enat n \ m < n"
  "q \ (\::enat)"
  "q < (\::enat) \ q \ \"
  "(\::enat) \ q \ q = \"
  "(\::enat) < q \ False"
  by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)

lemma numeral_le_enat_iff[simp]:
  shows "numeral m \ enat n \ numeral m \ n"
  by (auto simp: numeral_eq_enat)

lemma numeral_less_enat_iff[simp]:
  shows "numeral m < enat n \ numeral m < n"
  by (auto simp: numeral_eq_enat)

lemma enat_ord_code [code]:
  "enat m \ enat n \ m \ n"
  "enat m < enat n \ m < n"
  "q \ (\::enat) \ True"
  "enat m < \ \ True"
  "\ \ enat n \ False"
  "(\::enat) < q \ False"
  by simp_all

instance
  by standard (auto simp add: less_eq_enat_def less_enat_def plus_enat_def split: enat.splits)

end

instance enat :: dioid
proof
  fix a b :: enat show "(a \ b) = (\c. b = a + c)"
    by (cases a b rule: enat2_cases) (auto simp: le_iff_add enat_ex_split)
qed

instance enat :: "{linordered_nonzero_semiring, strict_ordered_comm_monoid_add}"
proof
  fix a b c :: enat
  show "a \ b \ 0 \ c \c * a \ c * b"
    unfolding times_enat_def less_eq_enat_def zero_enat_def
    by (simp split: enat.splits)
  show "a < b \ c < d \ a + c < b + d" for a b c d :: enat
    by (cases a b c d rule: enat2_cases[case_product enat2_cases]) auto
  show "a < b \ a + 1 < b + 1"
    by (metis add_right_mono eSuc_minus_1 eSuc_plus_1 less_le)
qed (simp add: zero_enat_def one_enat_def)

(* BH: These equations are already proven generally for any type in
class linordered_semidom. However, enat is not in that class because
it does not have the cancellation property. Would it be worthwhile to
a generalize linordered_semidom to a new class that includes enat? *)

lemma add_diff_assoc_enat: "z \ y \ x + (y - z) = x + y - (z::enat)"
by(cases x)(auto simp add: diff_enat_def split: enat.split)

lemma enat_ord_number [simp]:
  "(numeral m :: enat) \ numeral n \ (numeral m :: nat) \ numeral n"
  "(numeral m :: enat) < numeral n \ (numeral m :: nat) < numeral n"
  by (simp_all add: numeral_eq_enat)

lemma infinity_ileE [elim!]: "\ \ enat m \ R"
  by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)

lemma infinity_ilessE [elim!]: "\ < enat m \ R"
  by simp

lemma eSuc_ile_mono [simp]: "eSuc n \ eSuc m \ n \ m"
  by (simp add: eSuc_def less_eq_enat_def split: enat.splits)

lemma eSuc_mono [simp]: "eSuc n < eSuc m \ n < m"
  by (simp add: eSuc_def less_enat_def split: enat.splits)

lemma ile_eSuc [simp]: "n \ eSuc n"
  by (simp add: eSuc_def less_eq_enat_def split: enat.splits)

lemma not_eSuc_ilei0 [simp]: "\ eSuc n \ 0"
  by (simp add: zero_enat_def eSuc_def less_eq_enat_def split: enat.splits)

lemma i0_iless_eSuc [simp]: "0 < eSuc n"
  by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.splits)

lemma iless_eSuc0[simp]: "(n < eSuc 0) = (n = 0)"
  by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.split)

lemma ileI1: "m < n \ eSuc m \ n"
  by (simp add: eSuc_def less_eq_enat_def less_enat_def split: enat.splits)

lemma Suc_ile_eq: "enat (Suc m) \ n \ enat m < n"
  by (cases n) auto

lemma iless_Suc_eq [simp]: "enat m < eSuc n \ enat m \ n"
  by (auto simp add: eSuc_def less_enat_def split: enat.splits)

lemma imult_infinity: "(0::enat) < n \ \ * n = \"
  by (simp add: zero_enat_def less_enat_def split: enat.splits)

lemma imult_infinity_right: "(0::enat) < n \ n * \ = \"
  by (simp add: zero_enat_def less_enat_def split: enat.splits)

lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \ 0 < n)"
  by (simp only: zero_less_iff_neq_zero mult_eq_0_iff, simp)

lemma mono_eSuc: "mono eSuc"
  by (simp add: mono_def)

lemma min_enat_simps [simp]:
  "min (enat m) (enat n) = enat (min m n)"
  "min q 0 = 0"
  "min 0 q = 0"
  "min q (\::enat) = q"
  "min (\::enat) q = q"
  by (auto simp add: min_def)

lemma max_enat_simps [simp]:
  "max (enat m) (enat n) = enat (max m n)"
  "max q 0 = q"
  "max 0 q = q"
  "max q \ = (\::enat)"
  "max \ q = (\::enat)"
  by (simp_all add: max_def)

lemma enat_ile: "n \ enat m \ \k. n = enat k"
  by (cases n) simp_all

lemma enat_iless: "n < enat m \ \k. n = enat k"
  by (cases n) simp_all

lemma iadd_le_enat_iff:
  "x + y \ enat n \ (\y' x'. x = enat x' \ y = enat y' \ x' + y' \ n)"
by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all

lemma chain_incr: "\i. \j. Y i < Y j \ \j. enat k < Y j"
proof (induction k)
  case 0
  then show ?case
    using enat_0 zero_less_iff_neq_zero by fastforce
next
  case (Suc k)
  then show ?case
    by (meson Suc_ile_eq order_le_less_trans)
qed

lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)"
  by (simp add: eSuc_def split: enat.split)

lemma eSuc_Max:
  assumes "finite A" "A \ {}"
  shows "eSuc (Max A) = Max (eSuc ` A)"
  by (simp add: assms mono_Max_commute mono_eSuc)

instantiation enat :: "{order_bot, order_top}"
begin

definition bot_enat :: enat where "bot_enat = 0"
definition top_enat :: enat where "top_enat = \"

instance
  by standard (simp_all add: bot_enat_def top_enat_def)

end

lemma finite_enat_bounded:
  assumes le_fin: "\y. y \ A \ y \ enat n"
  shows "finite A"
proof (rule finite_subset)
  show "finite (enat ` {..n})" by blast
  have "A \ enat ` {..n}"
    using enat_ile le_fin by fastforce
  then show "A \ enat ` {..n}" .
qed

subsection \<open>Cancellation simprocs\<close>

lemma add_diff_cancel_enat[simp]: "x \ \ \ x + y - x = (y::enat)"
  by (metis add.commute add.right_neutral add_diff_assoc_enat idiff_self order_refl)

lemma enat_add_left_cancel: "a + b = a + c \ a = (\::enat) \ b = c"
  unfolding plus_enat_def by (simp split: enat.split)

lemma enat_add_left_cancel_le: "a + b \ a + c \ a = (\::enat) \ b \ c"
  unfolding plus_enat_def by (simp split: enat.split)

lemma enat_add_left_cancel_less: "a + b < a + c \ a \ (\::enat) \ b < c"
  unfolding plus_enat_def by (simp split: enat.split)

lemma plus_eq_infty_iff_enat: "(m::enat) + n = \ \ m=\ \ n=\"
  using enat_add_left_cancel by fastforce

ML \<open>
structure Cancel_Enat_Common =
struct
  (* copied from src/HOL/Tools/nat_numeral_simprocs.ML *)
  fun find_first_t _    _ []         = raise TERM("find_first_t", [])
    | find_first_t past u (t::terms) =
          if u aconv t then (rev past @ terms)
          else find_first_t (t::past) u terms

  fun dest_summing (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ t $ u, ts) =
        dest_summing (t, dest_summing (u, ts))
    | dest_summing (t, ts) = t :: ts

  val mk_sum = Arith_Data.long_mk_sum
  fun dest_sum t = dest_summing (t, [])
  val find_first = find_first_t []
  val trans_tac = Numeral_Simprocs.trans_tac
  val norm_ss =
    simpset_of (put_simpset HOL_basic_ss \<^context>
      |> Simplifier.add_simps @{thms ac_simps add_0_left add_0_right})
  fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
  fun simplify_meta_eq ctxt cancel_th th =
    Arith_Data.simplify_meta_eq [] ctxt
      ([th, cancel_th] MRS trans)
  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
end

structure Eq_Enat_Cancel = ExtractCommonTermFun
(open Cancel_Enat_Common
  val mk_bal = HOLogic.mk_eq
  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>HOL.eq\<close> \<^typ>\<open>enat\<close>
  fun simp_conv _ _ = SOME @{thm enat_add_left_cancel}
)

structure Le_Enat_Cancel = ExtractCommonTermFun
(open Cancel_Enat_Common
  val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less_eq\<close>
  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less_eq\<close> \<^typ>\<open>enat\<close>
  fun simp_conv _ _ = SOME @{thm enat_add_left_cancel_le}
)

structure Less_Enat_Cancel = ExtractCommonTermFun
(open Cancel_Enat_Common
  val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less\<close>
  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less\<close> \<^typ>\<open>enat\<close>
  fun simp_conv _ _ = SOME @{thm enat_add_left_cancel_less}
)
\<close>

simproc_setup enat_eq_cancel
  ("(l::enat) + m = n" | "(l::enat) = m + n") =
  \<open>K (fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>

simproc_setup enat_le_cancel
  ("(l::enat) + m \ n" | "(l::enat) \ m + n") =
  \<open>K (fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>

simproc_setup enat_less_cancel
  ("(l::enat) + m < n" | "(l::enat) < m + n") =
  \<open>K (fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>

text \<open>TODO: add regression tests for these simprocs\<close>

text \<open>TODO: add simprocs for combining and cancelling numerals\<close>

subsection \<open>Well-ordering\<close>

lemma less_enatE:
  "\n < enat m; \k. \n = enat k; k < m\ \ P\ \ P"
  using enat_iless enat_ord_simps(2) by blast

lemma less_infinityE:
  "\n < \; \k. n = enat k \ P\ \ P"
  by auto

lemma enat_less_induct:
  assumes "\n. \m::enat. m < n \ P m \ P n"
  shows "P n"
proof -
  have "P (enat k)" for k
    by (induction k rule: less_induct) (metis less_enatE assms)
  then show ?thesis
    by (metis enat.exhaust less_infinityE assms)
qed

instance enat :: wellorder
proof
  fix P and n
  assume hyp: "(\n::enat. (\m::enat. m < n \ P m) \ P n)"
  show "P n" by (blast intro: enat_less_induct hyp)
qed

subsection \<open>Complete Lattice\<close>

instantiation enat :: complete_lattice
begin

definition inf_enat :: "enat \ enat \ enat" where
  "inf_enat = min"

definition sup_enat :: "enat \ enat \ enat" where
  "sup_enat = max"

definition Inf_enat :: "enat set \ enat" where
  "Inf_enat A = (if A = {} then \ else (LEAST x. x \ A))"

definition Sup_enat :: "enat set \ enat" where
  "Sup_enat A = (if A = {} then 0 else if finite A then Max A else \)"

instance
proof
  fix x :: "enat" and A :: "enat set"
  show "x \ A \ Inf A \ x"
    unfolding Inf_enat_def by (auto intro: Least_le)
  show "(\y. y \ A \ x \ y) \ x \ Inf A"
    unfolding Inf_enat_def
    by (cases "A = {}") (auto intro: LeastI2_ex)
  show "x \ A \ x \ Sup A"
    unfolding Sup_enat_def by (cases "finite A") auto
  show "(\y. y \ A \ y \ x) \ Sup A \ x"
    unfolding Sup_enat_def using finite_enat_bounded by auto
qed (simp_all add: inf_enat_def sup_enat_def bot_enat_def top_enat_def Inf_enat_def Sup_enat_def)

end

instance enat :: complete_linorder ..

lemma eSuc_Sup: "A \ {} \ eSuc (Sup A) = Sup (eSuc ` A)"
  by(auto simp add: Sup_enat_def eSuc_Max inj_on_def dest: finite_imageD)

lemma sup_continuous_eSuc: "sup_continuous f \ sup_continuous (\x. eSuc (f x))"
  using eSuc_Sup [of "_ ` UNIV"] by (auto simp: sup_continuous_def image_comp)

subsection \<open>Traditional theorem names\<close>

lemmas enat_defs = zero_enat_def one_enat_def eSuc_def
  plus_enat_def less_eq_enat_def less_enat_def

lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \ n = 0)"
  by (rule add_eq_0_iff_both_eq_0)

lemma i0_lb : "(0::enat) \ n"
  by (rule zero_le)

lemma ile0_eq: "n \ (0::enat) \ n = 0"
  by (rule le_zero_eq)

lemma not_iless0: "\ n < (0::enat)"
  by (rule not_less_zero)

lemma i0_less[simp]: "(0::enat) < n \ n \ 0"
  by (rule zero_less_iff_neq_zero)

lemma imult_is_0: "((m::enat) * n = 0) = (m = 0 \ n = 0)"
  by (rule mult_eq_0_iff)

end

quality99%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.