Quelle Lattices.thy Sprache: Isabelle

(* Title: HOL/Lattices.thy
 Author: Tobias Nipkow
*)

section \<open>Abstract lattices\<close>

theory Lattices
imports Groups
begin

subsection \<open>Abstract semilattice\<close>

text \<open>
 These locales provide a basic structure for interpretation into
 bigger structures; extensions require careful thinking, otherwise
 undesired effects may occur due to interpretation.
\<close>

locale semilattice = abel_semigroup +
 assumes idem [simp]: "a \<^bold>* a = a"
begin

lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
 by (simp add: assoc [symmetric])

lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
 by (simp add: assoc)

end

locale semilattice_neutr = semilattice + comm_monoid

locale semilattice_order = semilattice +
 fixes less_eq :: "'a \ 'a \ bool" (infix \\<^bold>\\ 50)
 and less :: "'a \ 'a \ bool" (infix \\<^bold><\ 50)
 assumes order_iff: "a \<^bold>\ b \ a = a \<^bold>* b"
 and strict_order_iff: "a \<^bold>* b \ a \ b"
begin

lemma orderI: "a = a \<^bold>* b \ a \<^bold>\ b"
 by (simp add: order_iff)

lemma orderE:
 assumes "a \<^bold>\ b"
 obtains "a = a \<^bold>* b"
 using assms by (unfold order_iff)

sublocale ordering less_eq less
proof
 show "a \<^bold>\ b \ a \ b" for a b
 by (simp add: order_iff strict_order_iff)
next
 show "a \<^bold>\ a" for a
 by (simp add: order_iff)
next
 fix a b
 assume "a \<^bold>\ b" "b \<^bold>\ a"
 then have "a = a \<^bold>* b" "a \<^bold>* b = b"
 by (simp_all add: order_iff commute)
 then show "a = b" by simp
next
 fix a b c
 assume "a \<^bold>\ b" "b \<^bold>\ c"
 then have "a = a \<^bold>* b" "b = b \<^bold>* c"
 by (simp_all add: order_iff commute)
 then have "a = a \<^bold>* (b \<^bold>* c)"
 by simp
 then have "a = (a \<^bold>* b) \<^bold>* c"
 by (simp add: assoc)
 with \<open>a = a \<^bold>* b\<close> [symmetric] have "a = a \<^bold>* c" by simp
 then show "a \<^bold>\ c" by (rule orderI)
qed

lemma cobounded1 [simp]: "a \<^bold>* b \<^bold>\ a"
 by (simp add: order_iff commute)

lemma cobounded2 [simp]: "a \<^bold>* b \<^bold>\ b"
 by (simp add: order_iff)

lemma boundedI:
 assumes "a \<^bold>\ b" and "a \<^bold>\ c"
 shows "a \<^bold>\ b \<^bold>* c"
proof (rule orderI)
 from assms obtain "a \<^bold>* b = a" and "a \<^bold>* c = a"
 by (auto elim!: orderE)
 then show "a = a \<^bold>* (b \<^bold>* c)"
 by (simp add: assoc [symmetric])
qed

lemma boundedE:
 assumes "a \<^bold>\ b \<^bold>* c"
 obtains "a \<^bold>\ b" and "a \<^bold>\ c"
 using assms by (blast intro: trans cobounded1 cobounded2)

lemma bounded_iff [simp]: "a \<^bold>\ b \<^bold>* c \ a \<^bold>\ b \ a \<^bold>\ c"
 by (blast intro: boundedI elim: boundedE)

lemma strict_boundedE:
 assumes "a \<^bold>* c"
 obtains "a \<^bold>< b" and "a \<^bold>< c"
 using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+

lemma coboundedI1: "a \<^bold>\ c \ a \<^bold>* b \<^bold>\ c"
 by (rule trans) auto

lemma coboundedI2: "b \<^bold>\ c \ a \<^bold>* b \<^bold>\ c"
 by (rule trans) auto

lemma strict_coboundedI1: "a \<^bold>< c \ a \<^bold>* b \<^bold>< c"
 using irrefl
 by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order
 elim: strict_boundedE)

lemma strict_coboundedI2: "b \<^bold>< c \ a \<^bold>* b \<^bold>< c"
 using strict_coboundedI1 [of b c a] by (simp add: commute)

lemma mono: "a \<^bold>\ c \ b \<^bold>\ d \ a \<^bold>* b \<^bold>\ c \<^bold>* d"
 by (blast intro: boundedI coboundedI1 coboundedI2)

lemma absorb1: "a \<^bold>\ b \ a \<^bold>* b = a"
 by (rule antisym) (auto simp: refl)

lemma absorb2: "b \<^bold>\ a \ a \<^bold>* b = b"
 by (rule antisym) (auto simp: refl)

lemma absorb3: "a \<^bold>* b = a"
 by (rule absorb1) (rule strict_implies_order)

lemma absorb4: "b \<^bold>< a \ a \<^bold>* b = b"
 by (rule absorb2) (rule strict_implies_order)

lemma absorb_iff1: "a \<^bold>\ b \ a \<^bold>* b = a"
 using order_iff by auto

lemma absorb_iff2: "b \<^bold>\ a \ a \<^bold>* b = b"
 using order_iff by (auto simp add: commute)

end

locale semilattice_neutr_order = semilattice_neutr + semilattice_order
begin

sublocale ordering_top less_eq less "\<^bold>1"
 by standard (simp add: order_iff)

lemma eq_neutr_iff [simp]: \<open>a \<^bold>* b = \<^bold>1 \<longleftrightarrow> a = \<^bold>1 \<and> b = \<^bold>1\<close>
 by (simp add: eq_iff)

lemma neutr_eq_iff [simp]: \<open>\<^bold>1 = a \<^bold>* b \<longleftrightarrow> a = \<^bold>1 \<and> b = \<^bold>1\<close>
 by (simp add: eq_iff)

end

text \<open>Interpretations for boolean operators\<close>

interpretation conj: semilattice_neutr \<open>(\<and>)\<close> True
 by standard auto

interpretation disj: semilattice_neutr \<open>(\<or>)\<close> False
 by standard auto

declare conj_assoc [ac_simps del] disj_assoc [ac_simps del] \<comment> \<open>already simp by default\<close>

subsection \<open>Syntactic infimum and supremum operations\<close>

class inf =
 fixes inf :: "'a \ 'a \ 'a" (infixl \\\ 70)

class sup =
 fixes sup :: "'a \ 'a \ 'a" (infixl \\\ 65)

subsection \<open>Concrete lattices\<close>

class semilattice_inf = order + inf +
 assumes inf_le1 [simp]: "x \ y \ x"
 and inf_le2 [simp]: "x \ y \ y"
 and inf_greatest: "x \ y \ x \ z \ x \ y \ z"

class semilattice_sup = order + sup +
 assumes sup_ge1 [simp]: "x \ x \ y"
 and sup_ge2 [simp]: "y \ x \ y"
 and sup_least: "y \ x \ z \ x \ y \ z \ x"
begin

text \<open>Dual lattice.\<close>
lemma dual_semilattice: "class.semilattice_inf sup greater_eq greater"
 by (rule class.semilattice_inf.intro, rule dual_order)
 (unfold_locales, simp_all add: sup_least)

end

class lattice = semilattice_inf + semilattice_sup

subsubsection \<open>Intro and elim rules\<close>

context semilattice_inf
begin

lemma le_infI1: "a \ x \ a \ b \ x"
 by (rule order_trans) auto

lemma le_infI2: "b \ x \ a \ b \ x"
 by (rule order_trans) auto

lemma le_infI: "x \ a \ x \ b \ x \ a \ b"
 by (fact inf_greatest) (* FIXME: duplicate lemma *)

lemma le_infE: "x \ a \ b \ (x \ a \ x \ b \ P) \ P"
 by (blast intro: order_trans inf_le1 inf_le2)

lemma le_inf_iff: "x \ y \ z \ x \ y \ x \ z"
 by (blast intro: le_infI elim: le_infE) (* [simp] via bounded_iff *)

lemma le_iff_inf: "x \ y \ x \ y = x"
 by (auto intro: le_infI1 order.antisym dest: order.eq_iff [THEN iffD1] simp add: le_inf_iff)

lemma inf_mono: "a \ c \ b \ d \ a \ b \ c \ d"
 by (fast intro: inf_greatest le_infI1 le_infI2)

end

context semilattice_sup
begin

lemma le_supI1: "x \ a \ x \ a \ b"
 by (rule order_trans) auto

lemma le_supI2: "x \ b \ x \ a \ b"
 by (rule order_trans) auto

lemma le_supI: "a \ x \ b \ x \ a \ b \ x"
 by (fact sup_least) (* FIXME: duplicate lemma *)

lemma le_supE: "a \ b \ x \ (a \ x \ b \ x \ P) \ P"
 by (blast intro: order_trans sup_ge1 sup_ge2)

lemma le_sup_iff: "x \ y \ z \ x \ z \ y \ z"
 by (blast intro: le_supI elim: le_supE) (* [simp] via bounded_iff *)

lemma le_iff_sup: "x \ y \ x \ y = y"
 by (auto intro: le_supI2 order.antisym dest: order.eq_iff [THEN iffD1] simp add: le_sup_iff)

lemma sup_mono: "a \ c \ b \ d \ a \ b \ c \ d"
 by (fast intro: sup_least le_supI1 le_supI2)

end

subsubsection \<open>Equational laws\<close>

context semilattice_inf
begin

sublocale inf: semilattice inf
proof
 fix a b c
 show "(a \ b) \ c = a \ (b \ c)"
 by (rule order.antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff)
 show "a \ b = b \ a"
 by (rule order.antisym) (auto simp add: le_inf_iff)
 show "a \ a = a"
 by (rule order.antisym) (auto simp add: le_inf_iff)
qed

sublocale inf: semilattice_order inf less_eq less
 by standard (auto simp add: le_iff_inf less_le)

lemma inf_assoc: "(x \ y) \ z = x \ (y \ z)"
 by (fact inf.assoc)

lemma inf_commute: "(x \ y) = (y \ x)"
 by (fact inf.commute)

lemma inf_left_commute: "x \ (y \ z) = y \ (x \ z)"
 by (fact inf.left_commute)

lemma inf_idem: "x \ x = x"
 by (fact inf.idem) (* already simp *)

lemma inf_left_idem: "x \ (x \ y) = x \ y"
 by (fact inf.left_idem) (* already simp *)

lemma inf_right_idem: "(x \ y) \ y = x \ y"
 by (fact inf.right_idem) (* already simp *)

lemma inf_absorb1: "x \ y \ x \ y = x"
 by (rule order.antisym) auto

lemma inf_absorb2: "y \ x \ x \ y = y"
 by (rule order.antisym) auto

lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem

end

context semilattice_sup
begin

sublocale sup: semilattice sup
proof
 fix a b c
 show "(a \ b) \ c = a \ (b \ c)"
 by (rule order.antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff)
 show "a \ b = b \ a"
 by (rule order.antisym) (auto simp add: le_sup_iff)
 show "a \ a = a"
 by (rule order.antisym) (auto simp add: le_sup_iff)
qed

sublocale sup: semilattice_order sup greater_eq greater
 by standard (auto simp add: le_iff_sup sup.commute less_le)

lemma sup_assoc: "(x \ y) \ z = x \ (y \ z)"
 by (fact sup.assoc)

lemma sup_commute: "(x \ y) = (y \ x)"
 by (fact sup.commute)

lemma sup_left_commute: "x \ (y \ z) = y \ (x \ z)"
 by (fact sup.left_commute)

lemma sup_idem: "x \ x = x"
 by (fact sup.idem) (* already simp *)

lemma sup_left_idem [simp]: "x \ (x \ y) = x \ y"
 by (fact sup.left_idem)

lemma sup_absorb1: "y \ x \ x \ y = x"
 by (rule order.antisym) auto

lemma sup_absorb2: "x \ y \ x \ y = y"
 by (rule order.antisym) auto

lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem

end

context lattice
begin

lemma dual_lattice: "class.lattice sup (\) (>) inf"
 by (rule class.lattice.intro,
 rule dual_semilattice,
 rule class.semilattice_sup.intro,
 rule dual_order)
 (unfold_locales, auto)

lemma inf_sup_absorb [simp]: "x \ (x \ y) = x"
 by (blast intro: order.antisym inf_le1 inf_greatest sup_ge1)

lemma sup_inf_absorb [simp]: "x \ (x \ y) = x"
 by (blast intro: order.antisym sup_ge1 sup_least inf_le1)

lemmas inf_sup_aci = inf_aci sup_aci

lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2

text \<open>Towards distributivity.\<close>

lemma distrib_sup_le: "x \ (y \ z) \ (x \ y) \ (x \ z)"
 by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)

lemma distrib_inf_le: "(x \ y) \ (x \ z) \ x \ (y \ z)"
 by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)

text \<open>If you have one of them, you have them all.\<close>

lemma distrib_imp1:
 assumes distrib: "\x y z. x \ (y \ z) = (x \ y) \ (x \ z)"
 shows "x \ (y \ z) = (x \ y) \ (x \ z)"
proof-
 have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)"
 by simp
 also have "\ = x \ (z \ (x \ y))"
 by (simp add: distrib inf_commute sup_assoc del: sup_inf_absorb)
 also have "\ = ((x \ y) \ x) \ ((x \ y) \ z)"
 by (simp add: inf_commute)
 also have "\ = (x \ y) \ (x \ z)" by(simp add:distrib)
 finally show ?thesis .
qed

lemma distrib_imp2:
 assumes distrib: "\x y z. x \ (y \ z) = (x \ y) \ (x \ z)"
 shows "x \ (y \ z) = (x \ y) \ (x \ z)"
proof-
 have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)"
 by simp
 also have "\ = x \ (z \ (x \ y))"
 by (simp add: distrib sup_commute inf_assoc del: inf_sup_absorb)
 also have "\ = ((x \ y) \ x) \ ((x \ y) \ z)"
 by (simp add: sup_commute)
 also have "\ = (x \ y) \ (x \ z)" by (simp add:distrib)
 finally show ?thesis .
qed

end

subsubsection \<open>Strict order\<close>

context semilattice_inf
begin

lemma less_infI1: "a < x \ a \ b < x"
 by (auto simp add: less_le inf_absorb1 intro: le_infI1)

lemma less_infI2: "b < x \ a \ b < x"
 by (auto simp add: less_le inf_absorb2 intro: le_infI2)

end

context semilattice_sup
begin

lemma less_supI1: "x < a \ x < a \ b"
 using dual_semilattice
 by (rule semilattice_inf.less_infI1)

lemma less_supI2: "x Distributive lattices\<close>

class distrib_lattice = lattice +
 assumes sup_inf_distrib1: "x \ (y \ z) = (x \ y) \ (x \ z)"

context distrib_lattice
begin

lemma sup_inf_distrib2: "(y \ z) \ x = (y \ x) \ (z \ x)"
 by (simp add: sup_commute sup_inf_distrib1)

lemma inf_sup_distrib1: "x \ (y \ z) = (x \ y) \ (x \ z)"
 by (rule distrib_imp2 [OF sup_inf_distrib1])

lemma inf_sup_distrib2: "(y \ z) \ x = (y \ x) \ (z \ x)"
 by (simp add: inf_commute inf_sup_distrib1)

lemma dual_distrib_lattice: "class.distrib_lattice sup (\) (>) inf"
 by (rule class.distrib_lattice.intro, rule dual_lattice)
 (unfold_locales, fact inf_sup_distrib1)

lemmas sup_inf_distrib = sup_inf_distrib1 sup_inf_distrib2

lemmas inf_sup_distrib = inf_sup_distrib1 inf_sup_distrib2

lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2

end

subsection \<open>Bounded lattices\<close>

class bounded_semilattice_inf_top = semilattice_inf + order_top
begin

sublocale inf_top: semilattice_neutr inf top
 + inf_top: semilattice_neutr_order inf top less_eq less
proof
 show "x \ \ = x" for x
 by (rule inf_absorb1) simp
qed

lemma inf_top_left: "\ \ x = x"
 by (fact inf_top.left_neutral)

lemma inf_top_right: "x \ \ = x"
 by (fact inf_top.right_neutral)

lemma inf_eq_top_iff: "x \ y = \ \ x = \ \ y = \"
 by (fact inf_top.eq_neutr_iff)

lemma top_eq_inf_iff: "\ = x \ y \ x = \ \ y = \"
 by (fact inf_top.neutr_eq_iff)

end

class bounded_semilattice_sup_bot = semilattice_sup + order_bot
begin

sublocale sup_bot: semilattice_neutr sup bot
 + sup_bot: semilattice_neutr_order sup bot greater_eq greater
proof
 show "x \ \ = x" for x
 by (rule sup_absorb1) simp
qed

lemma sup_bot_left: "\ \ x = x"
 by (fact sup_bot.left_neutral)

lemma sup_bot_right: "x \ \ = x"
 by (fact sup_bot.right_neutral)

lemma sup_eq_bot_iff: "x \ y = \ \ x = \ \ y = \"
 by (fact sup_bot.eq_neutr_iff)

lemma bot_eq_sup_iff: "\ = x \ y \ x = \ \ y = \"
 by (fact sup_bot.neutr_eq_iff)

end

class bounded_lattice_bot = lattice + order_bot
begin

subclass bounded_semilattice_sup_bot ..

lemma inf_bot_left [simp]: "\ \ x = \"
 by (rule inf_absorb1) simp

lemma inf_bot_right [simp]: "x \ \ = \"
 by (rule inf_absorb2) simp

end

class bounded_lattice_top = lattice + order_top
begin

subclass bounded_semilattice_inf_top ..

lemma sup_top_left [simp]: "\ \ x = \"
 by (rule sup_absorb1) simp

lemma sup_top_right [simp]: "x \ \ = \"
 by (rule sup_absorb2) simp

end

class bounded_lattice = lattice + order_bot + order_top
begin

subclass bounded_lattice_bot ..
subclass bounded_lattice_top ..

lemma dual_bounded_lattice: "class.bounded_lattice sup greater_eq greater inf \ \"
 by unfold_locales (auto simp add: less_le_not_le)

end

subsection \<open>\<open>min/max\<close> as special case of lattice\<close>

context linorder
begin

sublocale min: semilattice_order min less_eq less
 + max: semilattice_order max greater_eq greater
 by standard (auto simp add: min_def max_def)

declare min.absorb1 [simp] min.absorb2 [simp]
 min.absorb3 [simp] min.absorb4 [simp]
 max.absorb1 [simp] max.absorb2 [simp]
 max.absorb3 [simp] max.absorb4 [simp]

lemma min_le_iff_disj: "min x y \ z \ x \ z \ y \ z"
 unfolding min_def using linear by (auto intro: order_trans)

lemma le_max_iff_disj: "z \ max x y \ z \ x \ z \ y"
 unfolding max_def using linear by (auto intro: order_trans)

lemma min_less_iff_disj: "min x y < z \ x < z \ y < z"
 unfolding min_def le_less using less_linear by (auto intro: less_trans)

lemma less_max_iff_disj: "z < max x y \ z < x \ z < y"
 unfolding max_def le_less using less_linear by (auto intro: less_trans)

lemma min_less_iff_conj [simp]: "z < min x y \ z < x \ z < y"
 unfolding min_def le_less using less_linear by (auto intro: less_trans)

lemma max_less_iff_conj [simp]: "max x y < z \ x < z \ y < z"
 unfolding max_def le_less using less_linear by (auto intro: less_trans)

lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)"
 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)

lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)"
 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)

lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)"
 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)

lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)"
 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)

lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2

lemma split_min [no_atp]: "P (min i j) \ (i \ j \ P i) \ (\ i \ j \ P j)"
 by (simp add: min_def)

lemma split_max [no_atp]: "P (max i j) \ (i \ j \ P j) \ (\ i \ j \ P i)"
 by (simp add: max_def)

lemma split_min_lin [no_atp]:
 \<open>P (min a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a P a) \<and> (b < a \<longrightarrow> P b)\<close>
 by (cases a b rule: linorder_cases) auto

lemma split_max_lin [no_atp]:
 \<open>P (max a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a P b) \<and> (b < a \<longrightarrow> P a)\<close>
 by (cases a b rule: linorder_cases) auto

end

lemma inf_min: "inf = (min :: 'a::{semilattice_inf,linorder} \ 'a \ 'a)"
 by (auto intro: antisym simp add: min_def fun_eq_iff)

lemma sup_max: "sup = (max :: 'a::{semilattice_sup,linorder} \ 'a \ 'a)"
 by (auto intro: antisym simp add: max_def fun_eq_iff)

subsection \<open>Uniqueness of inf and sup\<close>

lemma (in semilattice_inf) inf_unique:
 fixes f (infixl \<open>\<triangle>\<close> 70)
 assumes le1: "\x y. x \ y \ x"
 and le2: "\x y. x \ y \ y"
 and greatest: "\x y z. x \ y \ x \ z \ x \ y \ z"
 shows "x \ y = x \ y"
proof (rule order.antisym)
 show "x \ y \ x \ y"
 by (rule le_infI) (rule le1, rule le2)
 have leI: "\x y z. x \ y \ x \ z \ x \ y \ z"
 by (blast intro: greatest)
 show "x \ y \ x \ y"
 by (rule leI) simp_all
qed

lemma (in semilattice_sup) sup_unique:
 fixes f (infixl \<open>\<nabla>\<close> 70)
 assumes ge1 [simp]: "\x y. x \ x \ y"
 and ge2: "\x y. y \ x \ y"
 and least: "\x y z. y \ x \ z \ x \ y \ z \ x"
 shows "x \ y = x \ y"
proof (rule order.antisym)
 show "x \ y \ x \ y"
 by (rule le_supI) (rule ge1, rule ge2)
 have leI: "\x y z. x \ z \ y \ z \ x \ y \ z"
 by (blast intro: least)
 show "x \ y \ x \ y"
 by (rule leI) simp_all
qed

subsection \<open>Lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close>

instantiation "fun" :: (type, semilattice_sup) semilattice_sup
begin

definition "f \ g = (\x. f x \ g x)"

lemma sup_apply [simp, code]: "(f \ g) x = f x \ g x"
 by (simp add: sup_fun_def)

instance
 by standard (simp_all add: le_fun_def)

end

instantiation "fun" :: (type, semilattice_inf) semilattice_inf
begin

definition "f \ g = (\x. f x \ g x)"

lemma inf_apply [simp, code]: "(f \ g) x = f x \ g x"
 by (simp add: inf_fun_def)

instance by standard (simp_all add: le_fun_def)

end

instance "fun" :: (type, lattice) lattice ..

instance "fun" :: (type, distrib_lattice) distrib_lattice
 by standard (rule ext, simp add: sup_inf_distrib1)

instance "fun" :: (type, bounded_lattice) bounded_lattice ..

instantiation "fun" :: (type, uminus) uminus
begin

definition fun_Compl_def: "- A = (\x. - A x)"

lemma uminus_apply [simp, code]: "(- A) x = - (A x)"
 by (simp add: fun_Compl_def)

instance ..

end

instantiation "fun" :: (type, minus) minus
begin

definition fun_diff_def: "A - B = (\x. A x - B x)"

lemma minus_apply [simp, code]: "(A - B) x = A x - B x"
 by (simp add: fun_diff_def)

instance ..

end

end

quality98%

¤ 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.