Quelle Conditionally_Complete_Lattices.thy Sprache: Isabelle

(*  Title:      HOL/Conditionally_Complete_Lattices.thy
    Author:     Amine Chaieb and L C Paulson, University of Cambridge
    Author:     Johannes Hölzl, TU München
    Author:     Luke S. Serafin, Carnegie Mellon University
*)

section \<open>Conditionally-complete Lattices\<close>

theory Conditionally_Complete_Lattices
imports Finite_Set Lattices_Big Set_Interval
begin

locale preordering_bdd = preordering
begin

definition bdd :: \<open>'a set \<Rightarrow> bool\<close>
  where unfold: \<open>bdd A \<longleftrightarrow> (\<exists>M. \<forall>x \<in> A. x \<^bold>\<le> M)\<close>

lemma empty [simp, intro]:
  \<open>bdd {}\<close>
  by (simp add: unfold)

lemma I [intro]:
  \<open>bdd A\<close> if \<open>\<And>x. x \<in> A \<Longrightarrow> x \<^bold>\<le> M\<close>
  using that by (auto simp add: unfold)

lemma E:
  assumes \<open>bdd A\<close>
  obtains M where \<open>\<And>x. x \<in> A \<Longrightarrow> x \<^bold>\<le> M\<close>
  using assms that by (auto simp add: unfold)

lemma I2:
  \<open>bdd (f ` A)\<close> if \<open>\<And>x. x \<in> A \<Longrightarrow> f x \<^bold>\<le> M\<close>
  using that by (auto simp add: unfold)

lemma mono:
  \<open>bdd A\<close> if \<open>bdd B\<close> \<open>A \<subseteq> B\<close>
  using that by (auto simp add: unfold)

lemma Int1 [simp]:
  \<open>bdd (A \<inter> B)\<close> if \<open>bdd A\<close>
  using mono that by auto

lemma Int2 [simp]:
  \<open>bdd (A \<inter> B)\<close> if \<open>bdd B\<close>
  using mono that by auto

end

subsection \<open>Preorders\<close>

context preorder
begin

sublocale bdd_above: preordering_bdd \<open>(\<le>)\<close> \<open>(<)\<close>
  defines bdd_above_primitive_def: bdd_above = bdd_above.bdd ..

sublocale bdd_below: preordering_bdd \<open>(\<ge>)\<close> \<open>(>)\<close>
  defines bdd_below_primitive_def: bdd_below = bdd_below.bdd ..

lemma bdd_above_def: \<open>bdd_above A \<longleftrightarrow> (\<exists>M. \<forall>x \<in> A. x \<le> M)\<close>
  by (fact bdd_above.unfold)

lemma bdd_below_def: \<open>bdd_below A \<longleftrightarrow> (\<exists>M. \<forall>x \<in> A. M \<le> x)\<close>
  by (fact bdd_below.unfold)

lemma bdd_aboveI: "(\x. x \ A \ x \ M) \ bdd_above A"
  by (fact bdd_above.I)

lemma bdd_belowI: "(\x. x \ A \ m \ x) \ bdd_below A"
  by (fact bdd_below.I)

lemma bdd_aboveI2: "(\x. x \ A \ f x \ M) \ bdd_above (f`A)"
  by (fact bdd_above.I2)

lemma bdd_belowI2: "(\x. x \ A \ m \ f x) \ bdd_below (f`A)"
  by (fact bdd_below.I2)

lemma bdd_above_empty: "bdd_above {}"
  by (fact bdd_above.empty)

lemma bdd_below_empty: "bdd_below {}"
  by (fact bdd_below.empty)

lemma bdd_above_mono: "bdd_above B \ A \ B \ bdd_above A"
  by (fact bdd_above.mono)

lemma bdd_below_mono: "bdd_below B \ A \ B \ bdd_below A"
  by (fact bdd_below.mono)

lemma bdd_above_Int1: "bdd_above A \ bdd_above (A \ B)"
  by (fact bdd_above.Int1)

lemma bdd_above_Int2: "bdd_above B \ bdd_above (A \ B)"
  by (fact bdd_above.Int2)

lemma bdd_below_Int1: "bdd_below A \ bdd_below (A \ B)"
  by (fact bdd_below.Int1)

lemma bdd_below_Int2: "bdd_below B \ bdd_below (A \ B)"
  by (fact bdd_below.Int2)

lemma bdd_above_Ioo [simp, intro]: "bdd_above {a <..< b}"
  by (auto simp add: bdd_above_def intro!: exI[of _ b] less_imp_le)

lemma bdd_above_Ico [simp, intro]: "bdd_above {a ..< b}"
  by (auto simp add: bdd_above_def intro!: exI[of _ b] less_imp_le)

lemma bdd_above_Iio [simp, intro]: "bdd_above {..< b}"
  by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le)

lemma bdd_above_Ioc [simp, intro]: "bdd_above {a <.. b}"
  by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le)

lemma bdd_above_Icc [simp, intro]: "bdd_above {a .. b}"
  by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le)

lemma bdd_above_Iic [simp, intro]: "bdd_above {.. b}"
  by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le)

lemma bdd_below_Ioo [simp, intro]: "bdd_below {a <..< b}"
  by (auto simp add: bdd_below_def intro!: exI[of _ a] less_imp_le)

lemma bdd_below_Ioc [simp, intro]: "bdd_below {a <.. b}"
  by (auto simp add: bdd_below_def intro!: exI[of _ a] less_imp_le)

lemma bdd_below_Ioi [simp, intro]: "bdd_below {a <..}"
  by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le)

lemma bdd_below_Ico [simp, intro]: "bdd_below {a ..< b}"
  by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le)

lemma bdd_below_Icc [simp, intro]: "bdd_below {a .. b}"
  by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le)

lemma bdd_below_Ici [simp, intro]: "bdd_below {a ..}"
  by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le)

end

context order_top
begin

lemma bdd_above_top [simp, intro!]: "bdd_above A"
  by (rule bdd_aboveI [of _ top]) simp

end

context order_bot
begin

lemma bdd_below_bot [simp, intro!]: "bdd_below A"
  by (rule bdd_belowI [of _ bot]) simp

end

lemma bdd_above_image_mono: "mono f \ bdd_above A \ bdd_above (f`A)"
  by (auto simp: bdd_above_def mono_def)

lemma bdd_below_image_mono: "mono f \ bdd_below A \ bdd_below (f`A)"
  by (auto simp: bdd_below_def mono_def)

lemma bdd_above_image_antimono: "antimono f \ bdd_below A \ bdd_above (f`A)"
  by (auto simp: bdd_above_def bdd_below_def antimono_def)

lemma bdd_below_image_antimono: "antimono f \ bdd_above A \ bdd_below (f`A)"
  by (auto simp: bdd_above_def bdd_below_def antimono_def)

lemma
  fixes X :: "'a::ordered_ab_group_add set"
  shows bdd_above_uminus[simp]: "bdd_above (uminus ` X) \ bdd_below X"
    and bdd_below_uminus[simp]: "bdd_below (uminus ` X) \ bdd_above X"
  using bdd_above_image_antimono[of uminus X] bdd_below_image_antimono[of uminus "uminus`X"]
  using bdd_below_image_antimono[of uminus X] bdd_above_image_antimono[of uminus "uminus`X"]
  by (auto simp: antimono_def image_image)

subsection \<open>Lattices\<close>

context lattice
begin

lemma bdd_above_insert [simp]: "bdd_above (insert a A) = bdd_above A"
  by (auto simp: bdd_above_def intro: le_supI2 sup_ge1)

lemma bdd_below_insert [simp]: "bdd_below (insert a A) = bdd_below A"
  by (auto simp: bdd_below_def intro: le_infI2 inf_le1)

lemma bdd_finite [simp]:
  assumes "finite A" shows bdd_above_finite: "bdd_above A" and bdd_below_finite: "bdd_below A"
  using assms by (induct rule: finite_induct, auto)

lemma bdd_above_Un [simp]: "bdd_above (A \ B) = (bdd_above A \ bdd_above B)"
proof
  assume "bdd_above (A \ B)"
  thus "bdd_above A \ bdd_above B" unfolding bdd_above_def by auto
next
  assume "bdd_above A \ bdd_above B"
  then obtain a b where "\x\A. x \ a" "\x\B. x \ b" unfolding bdd_above_def by auto
  hence "\x \ A \ B. x \ sup a b" by (auto intro: Un_iff le_supI1 le_supI2)
  thus "bdd_above (A \ B)" unfolding bdd_above_def ..
qed

lemma bdd_below_Un [simp]: "bdd_below (A \ B) = (bdd_below A \ bdd_below B)"
proof
  assume "bdd_below (A \ B)"
  thus "bdd_below A \ bdd_below B" unfolding bdd_below_def by auto
next
  assume "bdd_below A \ bdd_below B"
  then obtain a b where "\x\A. a \ x" "\x\B. b \ x" unfolding bdd_below_def by auto
  hence "\x \ A \ B. inf a b \ x" by (auto intro: Un_iff le_infI1 le_infI2)
  thus "bdd_below (A \ B)" unfolding bdd_below_def ..
qed

lemma bdd_above_image_sup[simp]:
  "bdd_above ((\x. sup (f x) (g x)) ` A) \ bdd_above (f`A) \ bdd_above (g`A)"
by (auto simp: bdd_above_def intro: le_supI1 le_supI2)

lemma bdd_below_image_inf[simp]:
  "bdd_below ((\x. inf (f x) (g x)) ` A) \ bdd_below (f`A) \ bdd_below (g`A)"
by (auto simp: bdd_below_def intro: le_infI1 le_infI2)

lemma bdd_below_UN[simp]: "finite I \ bdd_below (\i\I. A i) = (\i \ I. bdd_below (A i))"
by (induction I rule: finite.induct) auto

lemma bdd_above_UN[simp]: "finite I \ bdd_above (\i\I. A i) = (\i \ I. bdd_above (A i))"
by (induction I rule: finite.induct) auto

end

text \<open>

To avoid name classes with the \<^class>\<open>complete_lattice\<close>-class we prefix \<^const>\<open>Sup\<close> and
\<^const>\<open>Inf\<close> in theorem names with c.

\<close>

subsection \<open>Conditionally complete lattices\<close>

class conditionally_complete_lattice = lattice + Sup + Inf +
  assumes cInf_lower: "x \ X \ bdd_below X \ Inf X \ x"
    and cInf_greatest: "X \ {} \ (\x. x \ X \ z \ x) \ z \ Inf X"
  assumes cSup_upper: "x \ X \ bdd_above X \ x \ Sup X"
    and cSup_least: "X \ {} \ (\x. x \ X \ x \ z) \ Sup X \ z"
begin

lemma cSup_upper2: "x \ X \ y \ x \ bdd_above X \ y \ Sup X"
  by (metis cSup_upper order_trans)

lemma cInf_lower2: "x \ X \ x \ y \ bdd_below X \ Inf X \ y"
  by (metis cInf_lower order_trans)

lemma cSup_mono: "B \ {} \ bdd_above A \ (\b. b \ B \ \a\A. b \ a) \ Sup B \ Sup A"
  by (metis cSup_least cSup_upper2)

lemma cInf_mono: "B \ {} \ bdd_below A \ (\b. b \ B \ \a\A. a \ b) \ Inf A \ Inf B"
  by (metis cInf_greatest cInf_lower2)

lemma cSup_subset_mono: "A \ {} \ bdd_above B \ A \ B \ Sup A \ Sup B"
  by (metis cSup_least cSup_upper subsetD)

lemma cInf_superset_mono: "A \ {} \ bdd_below B \ A \ B \ Inf B \ Inf A"
  by (metis cInf_greatest cInf_lower subsetD)

lemma cSup_eq_maximum: "z \ X \ (\x. x \ X \ x \ z) \ Sup X = z"
  by (intro order.antisym cSup_upper[of z X] cSup_least[of X z]) auto

lemma cInf_eq_minimum: "z \ X \ (\x. x \ X \ z \ x) \ Inf X = z"
  by (intro order.antisym cInf_lower[of z X] cInf_greatest[of X z]) auto

lemma cSup_le_iff: "S \ {} \ bdd_above S \ Sup S \ a \ (\x\S. x \ a)"
  by (metis order_trans cSup_upper cSup_least)

lemma le_cInf_iff: "S \ {} \ bdd_below S \ a \ Inf S \ (\x\S. a \ x)"
  by (metis order_trans cInf_lower cInf_greatest)

lemma cSup_eq_non_empty:
  assumes 1: "X \ {}"
  assumes 2: "\x. x \ X \ x \ a"
  assumes 3: "\y. (\x. x \ X \ x \ y) \ a \ y"
  shows "Sup X = a"
  by (intro 3 1 order.antisym cSup_least) (auto intro: 2 1 cSup_upper)

lemma cInf_eq_non_empty:
  assumes 1: "X \ {}"
  assumes 2: "\x. x \ X \ a \ x"
  assumes 3: "\y. (\x. x \ X \ y \ x) \ y \ a"
  shows "Inf X = a"
  by (intro 3 1 order.antisym cInf_greatest) (auto intro: 2 1 cInf_lower)

lemma cInf_cSup: "S \ {} \ bdd_below S \ Inf S = Sup {x. \s\S. x \ s}"
  by (rule cInf_eq_non_empty) (auto intro!: cSup_upper cSup_least simp: bdd_below_def)

lemma cSup_cInf: "S \ {} \ bdd_above S \ Sup S = Inf {x. \s\S. s \ x}"
  by (rule cSup_eq_non_empty) (auto intro!: cInf_lower cInf_greatest simp: bdd_above_def)

lemma cSup_insert: "X \ {} \ bdd_above X \ Sup (insert a X) = sup a (Sup X)"
  by (intro cSup_eq_non_empty) (auto intro: le_supI2 cSup_upper cSup_least)

lemma cInf_insert: "X \ {} \ bdd_below X \ Inf (insert a X) = inf a (Inf X)"
  by (intro cInf_eq_non_empty) (auto intro: le_infI2 cInf_lower cInf_greatest)

lemma cSup_singleton [simp]: "Sup {x} = x"
  by (intro cSup_eq_maximum) auto

lemma cInf_singleton [simp]: "Inf {x} = x"
  by (intro cInf_eq_minimum) auto

lemma cSup_insert_If:  "bdd_above X \ Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
  using cSup_insert[of X] by simp

lemma cInf_insert_If: "bdd_below X \ Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
  using cInf_insert[of X] by simp

lemma le_cSup_finite: "finite X \ x \ X \ x \ Sup X"
proof (induct X arbitrary: x rule: finite_induct)
  case (insert x X y) then show ?case
    by (cases "X = {}") (auto simp: cSup_insert intro: le_supI2)
qed simp

lemma cInf_le_finite: "finite X \ x \ X \ Inf X \ x"
proof (induct X arbitrary: x rule: finite_induct)
  case (insert x X y) then show ?case
    by (cases "X = {}") (auto simp: cInf_insert intro: le_infI2)
qed simp

lemma cSup_eq_Sup_fin: "finite X \ X \ {} \ Sup X = Sup_fin X"
  by (induct X rule: finite_ne_induct) (simp_all add: cSup_insert)

lemma cInf_eq_Inf_fin: "finite X \ X \ {} \ Inf X = Inf_fin X"
  by (induct X rule: finite_ne_induct) (simp_all add: cInf_insert)

lemma cSup_atMost[simp]: "Sup {..x} = x"
  by (auto intro!: cSup_eq_maximum)

lemma cSup_greaterThanAtMost[simp]: "y < x \ Sup {y<..x} = x"
  by (auto intro!: cSup_eq_maximum)

lemma cSup_atLeastAtMost[simp]: "y \ x \ Sup {y..x} = x"
  by (auto intro!: cSup_eq_maximum)

lemma cInf_atLeast[simp]: "Inf {x..} = x"
  by (auto intro!: cInf_eq_minimum)

lemma cInf_atLeastLessThan[simp]: "y < x \ Inf {y..
  by (auto intro!: cInf_eq_minimum)

lemma cInf_atLeastAtMost[simp]: "y \ x \ Inf {y..x} = y"
  by (auto intro!: cInf_eq_minimum)

lemma cINF_lower: "bdd_below (f ` A) \ x \ A \ \(f ` A) \ f x"
  using cInf_lower [of _ "f ` A"] by simp

lemma cINF_greatest: "A \ {} \ (\x. x \ A \ m \ f x) \ m \ \(f ` A)"
  using cInf_greatest [of "f ` A"] by auto

lemma cSUP_upper: "x \ A \ bdd_above (f ` A) \ f x \ \(f ` A)"
  using cSup_upper [of _ "f ` A"] by simp

lemma cSUP_least: "A \ {} \ (\x. x \ A \ f x \ M) \ \(f ` A) \ M"
  using cSup_least [of "f ` A"] by auto

lemma cINF_lower2: "bdd_below (f ` A) \ x \ A \ f x \ u \ \(f ` A) \ u"
  by (auto intro: cINF_lower order_trans)

lemma cSUP_upper2: "bdd_above (f ` A) \ x \ A \ u \ f x \ u \ \(f ` A)"
  by (auto intro: cSUP_upper order_trans)

lemma cSUP_const [simp]: "A \ {} \ (\x\A. c) = c"
  by (intro order.antisym cSUP_least) (auto intro: cSUP_upper)

lemma cINF_const [simp]: "A \ {} \ (\x\A. c) = c"
  by (intro order.antisym cINF_greatest) (auto intro: cINF_lower)

lemma le_cINF_iff: "A \ {} \ bdd_below (f ` A) \ u \ \(f ` A) \ (\x\A. u \ f x)"
  by (metis cINF_greatest cINF_lower order_trans)

lemma cSUP_le_iff: "A \ {} \ bdd_above (f ` A) \ \(f ` A) \ u \ (\x\A. f x \ u)"
  by (metis cSUP_least cSUP_upper order_trans)

lemma less_cINF_D: "bdd_below (f`A) \ y < (\i\A. f i) \ i \ A \ y < f i"
  by (metis cINF_lower less_le_trans)

lemma cSUP_lessD: "bdd_above (f`A) \ (\i\A. f i) < y \ i \ A \ f i < y"
  by (metis cSUP_upper le_less_trans)

lemma cINF_insert: "A \ {} \ bdd_below (f ` A) \ \(f ` insert a A) = inf (f a) (\(f ` A))"
  by (simp add: cInf_insert)

lemma cSUP_insert: "A \ {} \ bdd_above (f ` A) \ \(f ` insert a A) = sup (f a) (\(f ` A))"
  by (simp add: cSup_insert)

lemma cINF_mono: "B \ {} \ bdd_below (f ` A) \ (\m. m \ B \ \n\A. f n \ g m) \ \(f ` A) \ \(g ` B)"
  using cInf_mono [of "g ` B" "f ` A"] by auto

lemma cSUP_mono: "A \ {} \ bdd_above (g ` B) \ (\n. n \ A \ \m\B. f n \ g m) \ \(f ` A) \ \(g ` B)"
  using cSup_mono [of "f ` A" "g ` B"] by auto

lemma cINF_superset_mono: "A \ {} \ bdd_below (g ` B) \ A \ B \ (\x. x \ B \ g x \ f x) \ \(g ` B) \ \(f ` A)"
  by (rule cINF_mono) auto

lemma cSUP_subset_mono:
  "\A \ {}; bdd_above (g ` B); A \ B; \x. x \ A \ f x \ g x\ \ \ (f ` A) \ \ (g ` B)"
  by (rule cSUP_mono) auto

lemma less_eq_cInf_inter: "bdd_below A \ bdd_below B \ A \ B \ {} \ inf (Inf A) (Inf B) \ Inf (A \ B)"
  by (metis cInf_superset_mono lattice_class.inf_sup_ord(1) le_infI1)

lemma cSup_inter_less_eq: "bdd_above A \ bdd_above B \ A \ B \ {} \ Sup (A \ B) \ sup (Sup A) (Sup B) "
  by (metis cSup_subset_mono lattice_class.inf_sup_ord(1) le_supI1)

lemma cInf_union_distrib: "A \ {} \ bdd_below A \ B \ {} \ bdd_below B \ Inf (A \ B) = inf (Inf A) (Inf B)"
  by (intro order.antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower)

lemma cINF_union: "A \ {} \ bdd_below (f ` A) \ B \ {} \ bdd_below (f ` B) \ \ (f ` (A \ B)) = \ (f ` A) \ \ (f ` B)"
  using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un)

lemma cSup_union_distrib: "A \ {} \ bdd_above A \ B \ {} \ bdd_above B \ Sup (A \ B) = sup (Sup A) (Sup B)"
  by (intro order.antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper)

lemma cSUP_union: "A \ {} \ bdd_above (f ` A) \ B \ {} \ bdd_above (f ` B) \ \ (f ` (A \ B)) = \ (f ` A) \ \ (f ` B)"
  using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un)

lemma cINF_inf_distrib: "A \ {} \ bdd_below (f`A) \ bdd_below (g`A) \ \ (f ` A) \ \ (g ` A) = (\a\A. inf (f a) (g a))"
  by (intro order.antisym le_infI cINF_greatest cINF_lower2)
     (auto intro: le_infI1 le_infI2 cINF_greatest cINF_lower le_infI)

lemma SUP_sup_distrib: "A \ {} \ bdd_above (f`A) \ bdd_above (g`A) \ \ (f ` A) \ \ (g ` A) = (\a\A. sup (f a) (g a))"
  by (intro order.antisym le_supI cSUP_least cSUP_upper2)
     (auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI)

lemma cInf_le_cSup:
  "A \ {} \ bdd_above A \ bdd_below A \ Inf A \ Sup A"
  by (auto intro!: cSup_upper2[of "SOME a. a \ A"] intro: someI cInf_lower)

  context
    fixes f :: "'a \ 'b::conditionally_complete_lattice"
    assumes "mono f"
  begin

  lemma mono_cInf: "\bdd_below A; A\{}\ \ f (Inf A) \ (INF x\A. f x)"
    by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cINF_greatest cInf_lower monoD)

  lemma mono_cSup: "\bdd_above A; A\{}\ \ (SUP x\A. f x) \ f (Sup A)"
    by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cSUP_least cSup_upper monoD)

  lemma mono_cINF: "\bdd_below (A`I); I\{}\ \ f (INF i\I. A i) \ (INF x\I. f (A x))"
    by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cINF_greatest cINF_lower monoD)

  lemma mono_cSUP: "\bdd_above (A`I); I\{}\ \ (SUP x\I. f (A x)) \ f (SUP i\I. A i)"
    by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cSUP_least cSUP_upper monoD)

  end

end

text \<open>The special case of well-orderings\<close>

lemma wellorder_InfI:
  fixes k :: "'a::{wellorder,conditionally_complete_lattice}"
  assumes "k \ A" shows "Inf A \ A"
  using wellorder_class.LeastI [of "\x. x \ A" k]
  by (simp add: Least_le assms cInf_eq_minimum)

lemma wellorder_Inf_le1:
  fixes k :: "'a::{wellorder,conditionally_complete_lattice}"
  assumes "k \ A" shows "Inf A \ k"
  by (meson Least_le assms bdd_below.I cInf_lower)

subsection \<open>Complete lattices\<close>

instance complete_lattice \<subseteq> conditionally_complete_lattice
  by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)

lemma cSup_eq:
  fixes a :: "'a :: {conditionally_complete_lattice, no_bot}"
  assumes upper: "\x. x \ X \ x \ a"
  assumes least: "\y. (\x. x \ X \ x \ y) \ a \ y"
  shows "Sup X = a"
proof cases
  assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
qed (intro cSup_eq_non_empty assms)

lemma cSup_unique:
  fixes b :: "'a :: {conditionally_complete_lattice, no_bot}"
  assumes "\c. (\x \ s. x \ c) \ b \ c"
  shows "Sup s = b"
  by (metis assms cSup_eq order.refl)

lemma cInf_eq:
  fixes a :: "'a :: {conditionally_complete_lattice, no_top}"
  assumes upper: "\x. x \ X \ a \ x"
  assumes least: "\y. (\x. x \ X \ y \ x) \ y \ a"
  shows "Inf X = a"
proof cases
  assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
qed (intro cInf_eq_non_empty assms)

lemma cInf_unique:
  fixes b :: "'a :: {conditionally_complete_lattice, no_top}"
  assumes "\c. (\x \ s. x \ c) \ b \ c"
  shows "Inf s = b"
  by (meson assms cInf_eq order.refl)

class conditionally_complete_linorder = conditionally_complete_lattice + linorder
begin

lemma less_cSup_iff:
  "X \ {} \ bdd_above X \ y < Sup X \ (\x\X. y < x)"
  by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)

lemma cInf_less_iff: "X \ {} \ bdd_below X \ Inf X < y \ (\x\X. x < y)"
  by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)

lemma cINF_less_iff: "A \ {} \ bdd_below (f`A) \ (\i\A. f i) < a \ (\x\A. f x < a)"
  using cInf_less_iff[of "f`A"] by auto

lemma less_cSUP_iff: "A \ {} \ bdd_above (f`A) \ a < (\i\A. f i) \ (\x\A. a < f x)"
  using less_cSup_iff[of "f`A"] by auto

lemma less_cSupE:
  assumes "y < Sup X" "X \ {}" obtains x where "x \ X" "y < x"
  by (metis cSup_least assms not_le that)

lemma less_cSupD:
  "X \ {} \ z < Sup X \ \x\X. z < x"
  by (metis less_cSup_iff not_le_imp_less bdd_above_def)

lemma cInf_lessD:
  "X \ {} \ Inf X < z \ \x\X. x < z"
  by (metis cInf_less_iff not_le_imp_less bdd_below_def)

lemma complete_interval:
  assumes "a < b" and "P a" and "\ P b"
  shows "\c. a \ c \ c \ b \ (\x. a \ x \ x < c \ P x) \
             (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
proof (rule exI [where x = "Sup {d. \x. a \ x \ x < d \ P x}"], safe)
  show "a \ Sup {d. \c. a \ c \ c < d \ P c}"
    by (rule cSup_upper, auto simp: bdd_above_def)
       (metis \<open>a < b\<close> \<open>\<not> P b\<close> linear less_le)
next
  show "Sup {d. \c. a \ c \ c < d \ P c} \ b"
    by (rule cSup_least)
       (use \<open>a<b\<close> \<open>\<not> P b\<close> in \<open>auto simp add: less_le_not_le\<close>)
next
  fix x
  assume x: "a \ x" and lt: "x < Sup {d. \c. a \ c \ c < d \ P c}"
  show "P x"
    by (rule less_cSupE [OF lt]) (use less_le_not_le x in \<open>auto\<close>)
next
  fix d
  assume 0: "\x. a \ x \ x < d \ P x"
  then have "d \ {d. \c. a \ c \ c < d \ P c}"
    by auto
  moreover have "bdd_above {d. \c. a \ c \ c < d \ P c}"
    unfolding bdd_above_def using \<open>a<b\<close> \<open>\<not> P b\<close> linear
    by (simp add: less_le) blast
  ultimately show "d \ Sup {d. \c. a \ c \ c < d \ P c}"
    by (auto simp: cSup_upper)
qed

end

subsection \<open>Instances\<close>

instance complete_linorder < conditionally_complete_linorder
  ..

lemma cSup_eq_Max: "finite (X::'a::conditionally_complete_linorder set) \ X \ {} \ Sup X = Max X"
  using cSup_eq_Sup_fin[of X] by (simp add: Sup_fin_Max)

lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \ X \ {} \ Inf X = Min X"
  using cInf_eq_Inf_fin[of X] by (simp add: Inf_fin_Min)

lemma cSup_lessThan[simp]: "Sup {..
  by (auto intro!: cSup_eq_non_empty intro: dense_le)

lemma cSup_greaterThanLessThan[simp]: "y < x \ Sup {y<..
  by (auto intro!: cSup_eq_non_empty intro: dense_le_bounded)

lemma cSup_atLeastLessThan[simp]: "y < x \ Sup {y..
  by (auto intro!: cSup_eq_non_empty intro: dense_le_bounded)

lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, no_top, dense_linorder} <..} = x"
  by (auto intro!: cInf_eq_non_empty intro: dense_ge)

lemma cInf_greaterThanAtMost[simp]: "y < x \ Inf {y<..x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
  by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded)

lemma cInf_greaterThanLessThan[simp]: "y < x \ Inf {y<..
  by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded)

lemma Sup_inverse_eq_inverse_Inf:
  fixes f::"'b \ 'a::{conditionally_complete_linorder,linordered_field}"
  assumes "bdd_above (range f)" "L > 0" and geL: "\x. f x \ L"
  shows "(SUP x. 1 / f x) = 1 / (INF x. f x)"
proof (rule antisym)
  have bdd_f: "bdd_below (range f)"
    by (meson assms bdd_belowI2)
  have "Inf (range f) \ L"
    by (simp add: cINF_greatest geL)
  have bdd_invf: "bdd_above (range (\x. 1 / f x))"
  proof (rule bdd_aboveI2)
    show "\x. 1 / f x \ 1/L"
      using assms by (auto simp: divide_simps)
  qed
  moreover have le_inverse_Inf: "1 / f x \ 1 / Inf (range f)" for x
  proof -
    have "Inf (range f) \ f x"
      by (simp add: bdd_f cInf_lower)
    then show ?thesis
      using assms \<open>L \<le> Inf (range f)\<close> by (auto simp: divide_simps)
  qed
  ultimately show *: "(SUP x. 1 / f x) \ 1 / Inf (range f)"
    by (auto simp: cSup_le_iff cINF_lower)
  have "1 / (SUP x. 1 / f x) \ f y" for y
  proof (cases "(SUP x. 1 / f x) < 0")
    case True
    with assms show ?thesis
      by (meson less_asym' order_trans linorder_not_le zero_le_divide_1_iff)
  next
    case False
    have "1 / f y \ (SUP x. 1 / f x)"
      by (simp add: bdd_invf cSup_upper)
    with False assms show ?thesis
      by (metis (no_types) div_by_1 divide_divide_eq_right dual_order.strict_trans1 inverse_eq_divide
          inverse_le_imp_le mult.left_neutral)
  qed
  then have "1 / (SUP x. 1 / f x) \ Inf (range f)"
    using bdd_f by (simp add: le_cInf_iff)
  moreover have "(SUP x. 1 / f x) > 0"
    using assms cSUP_upper [OF _ bdd_invf] by (meson UNIV_I less_le_trans zero_less_divide_1_iff)
  ultimately show "1 / Inf (range f) \ (SUP t. 1 / f t)"
    using \<open>L \<le> Inf (range f)\<close> \<open>L>0\<close> by (auto simp: field_simps)
qed

lemma Inf_inverse_eq_inverse_Sup:
  fixes f::"'b \ 'a::{conditionally_complete_linorder,linordered_field}"
  assumes "bdd_above (range f)" "L > 0" and geL: "\x. f x \ L"
  shows  "(INF x. 1 / f x) = 1 / (SUP x. f x)"
proof -
  obtain M where "M>0" and M: "\x. f x \ M"
    by (meson assms cSup_upper dual_order.strict_trans1 rangeI)
  have bdd: "bdd_above (range (inverse \ f))"
    using assms le_imp_inverse_le by (auto simp: bdd_above_def)
  have "f x > 0" for x
    using \<open>L>0\<close> geL order_less_le_trans by blast
  then have [simp]: "1 / inverse(f x) = f x" "1 / M \ 1 / f x" for x
    using M \<open>M>0\<close> by (auto simp: divide_simps)
  show ?thesis
    using Sup_inverse_eq_inverse_Inf [OF bdd, of "inverse M"] \<open>M>0\<close>
    by (simp add: inverse_eq_divide)
qed

lemma Inf_insert_finite:
  fixes S :: "'a::conditionally_complete_linorder set"
  shows "finite S \ Inf (insert x S) = (if S = {} then x else min x (Inf S))"
  by (simp add: cInf_eq_Min)

lemma Sup_insert_finite:
  fixes S :: "'a::conditionally_complete_linorder set"
  shows "finite S \ Sup (insert x S) = (if S = {} then x else max x (Sup S))"
  by (simp add: cSup_insert sup_max)

lemma finite_imp_less_Inf:
  fixes a :: "'a::conditionally_complete_linorder"
  shows "\finite X; x \ X; \x. x\X \ a < x\ \ a < Inf X"
  by (induction X rule: finite_induct) (simp_all add: cInf_eq_Min Inf_insert_finite)

lemma finite_less_Inf_iff:
  fixes a :: "'a :: conditionally_complete_linorder"
  shows "\finite X; X \ {}\ \ a < Inf X \ (\x \ X. a < x)"
  by (auto simp: cInf_eq_Min)

lemma finite_imp_Sup_less:
  fixes a :: "'a::conditionally_complete_linorder"
  shows "\finite X; x \ X; \x. x\X \ a > x\ \ a > Sup X"
  by (induction X rule: finite_induct) (simp_all add: cSup_eq_Max Sup_insert_finite)

lemma finite_Sup_less_iff:
  fixes a :: "'a :: conditionally_complete_linorder"
  shows "\finite X; X \ {}\ \ a > Sup X \ (\x \ X. a > x)"
  by (auto simp: cSup_eq_Max)

class linear_continuum = conditionally_complete_linorder + dense_linorder +
  assumes UNIV_not_singleton: "\a b::'a. a \ b"
begin

lemma ex_gt_or_lt: "\b. a < b \ b < a"
  by (metis UNIV_not_singleton neq_iff)

end

context
  fixes f::"'a \ 'b::{conditionally_complete_linorder,ordered_ab_group_add}"
begin

lemma bdd_above_uminus_image: "bdd_above ((\x. - f x) ` A) \ bdd_below (f ` A)"
  by (metis bdd_above_uminus image_image)

lemma bdd_below_uminus_image: "bdd_below ((\x. - f x) ` A) \ bdd_above (f ` A)"
  by (metis bdd_below_uminus image_image)

lemma uminus_cSUP:
  assumes "bdd_above (f ` A)" "A \ {}"
  shows  "- (SUP x\A. f x) = (INF x\A. - f x)"
proof (rule antisym)
  show "(INF x\A. - f x) \ - Sup (f ` A)"
    by (metis cINF_lower cSUP_least bdd_below_uminus_image assms le_minus_iff)
  have *: "\x. x \A \ f x \ Sup (f ` A)"
    by (simp add: assms cSup_upper)
  then show "- Sup (f ` A) \ (INF x\A. - f x)"
    by (simp add: assms cINF_greatest)
qed

end

context
  fixes f::"'a \ 'b::{conditionally_complete_linorder,ordered_ab_group_add}"
begin

lemma uminus_cINF:
  assumes "bdd_below (f ` A)" "A \ {}"
  shows  "- (INF x\A. f x) = (SUP x\A. - f x)"
  by (metis (mono_tags, lifting) INF_cong uminus_cSUP assms bdd_above_uminus_image minus_equation_iff)

lemma Sup_add_eq:
  assumes "bdd_above (f ` A)" "A \ {}"
  shows  "(SUP x\A. a + f x) = a + (SUP x\A. f x)" (is "?L=?R")
proof (rule antisym)
  have bdd: "bdd_above ((\x. a + f x) ` A)"
    by (metis assms bdd_above_image_mono image_image mono_add)
  with assms show "?L \ ?R"
    by (simp add: assms cSup_le_iff cSUP_upper)
  have "\x. x \ A \ f x \ (SUP x\A. a + f x) - a"
    by (simp add: bdd cSup_upper le_diff_eq)
  with \<open>A \<noteq> {}\<close> have "\<Squnion> (f ` A) \<le> (\<Squnion>x\<in>A. a + f x) - a"
    by (simp add: cSUP_least)
  then show "?R \ ?L"
    by (metis add.commute le_diff_eq)
qed

lemma Inf_add_eq: \<comment>\<open>you don't get a shorter proof by duality\<close>
  assumes "bdd_below (f ` A)" "A \ {}"
  shows  "(INF x\A. a + f x) = a + (INF x\A. f x)" (is "?L=?R")
proof (rule antisym)
  show "?R \ ?L"
    using assms mono_add mono_cINF by blast
  have bdd: "bdd_below ((\x. a + f x) ` A)"
    by (metis add_left_mono assms(1) bdd_below.E bdd_below.I2 imageI)
  with assms have "\x. x \ A \ f x \ (INF x\A. a + f x) - a"
    by (simp add: cInf_lower diff_le_eq)
  with \<open>A \<noteq> {}\<close> have "(\<Sqinter>x\<in>A. a + f x) - a \<le> \<Sqinter> (f ` A)"
    by (simp add: cINF_greatest)
  with assms show "?L \ ?R"
    by (metis add.commute diff_le_eq)
qed

end

instantiation nat :: conditionally_complete_linorder
begin

definition "Sup (X::nat set) = (if X={} then 0 else Max X)"
definition "Inf (X::nat set) = (LEAST n. n \ X)"

lemma bdd_above_nat: "bdd_above X \ finite (X::nat set)"
proof
  assume "bdd_above X"
  then obtain z where "X \ {.. z}"
    by (auto simp: bdd_above_def)
  then show "finite X"
    by (rule finite_subset) simp
qed simp

instance
proof
  fix x :: nat
  fix X :: "nat set"
  show "Inf X \ x" if "x \ X" "bdd_below X"
    using that by (simp add: Inf_nat_def Least_le)
  show "x \ Inf X" if "X \ {}" "\y. y \ X \ x \ y"
    using that unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex)
  show "x \ Sup X" if "x \ X" "bdd_above X"
    using that by (auto simp add: Sup_nat_def bdd_above_nat)
  show "Sup X \ x" if "X \ {}" "\y. y \ X \ y \ x"
  proof -
    from that have "bdd_above X"
      by (auto simp: bdd_above_def)
    with that show ?thesis
      by (simp add: Sup_nat_def bdd_above_nat)
  qed
qed

end

lemma Inf_nat_def1:
  fixes K::"nat set"
  assumes "K \ {}"
  shows "Inf K \ K"
by (auto simp add: Min_def Inf_nat_def) (meson LeastI assms bot.extremum_unique subsetI)

lemma Sup_nat_empty [simp]: "Sup {} = (0::nat)"
  by (auto simp add: Sup_nat_def)

instantiation int :: conditionally_complete_linorder
begin

definition "Sup (X::int set) = (THE x. x \ X \ (\y\X. y \ x))"
definition "Inf (X::int set) = - (Sup (uminus ` X))"

instance
proof
  { fix x :: int and X :: "int set" assume "X \ {}" "bdd_above X"
    then obtain x y where "X \ {..y}" "x \ X"
      by (auto simp: bdd_above_def)
    then have *: "finite (X \ {x..y})" "X \ {x..y} \ {}" and "x \ y"
      by (auto simp: subset_eq)
    have "\!x\X. (\y\X. y \ x)"
    proof
      { fix z assume "z \ X"
        have "z \ Max (X \ {x..y})"
        proof cases
          assume "x \ z" with \z \ X\ \X \ {..y}\ *(1) show ?thesis
            by (auto intro!: Max_ge)
        next
          assume "\ x \ z"
          then have "z < x" by simp
          also have "x \ Max (X \ {x..y})"
            using \<open>x \<in> X\<close> *(1) \<open>x \<le> y\<close> by (intro Max_ge) auto
          finally show ?thesis by simp
        qed }
      note le = this
      with Max_in[OF *] show ex: "Max (X \ {x..y}) \ X \ (\z\X. z \ Max (X \ {x..y}))" by auto

      fix z assume *: "z \ X \ (\y\X. y \ z)"
      with le have "z \ Max (X \ {x..y})"
        by auto
      moreover have "Max (X \ {x..y}) \ z"
        using * ex by auto
      ultimately show "z = Max (X \ {x..y})"
        by auto
    qed
    then have "Sup X \ X \ (\y\X. y \ Sup X)"
      unfolding Sup_int_def by (rule theI') }
  note Sup_int = this

  { fix x :: int and X :: "int set" assume "x \ X" "bdd_above X" then show "x \ Sup X"
      using Sup_int[of X] by auto }
  note le_Sup = this
  { fix x :: int and X :: "int set" assume "X \ {}" "\y. y \ X \ y \ x" then show "Sup X \ x"
      using Sup_int[of X] by (auto simp: bdd_above_def) }
  note Sup_le = this

  { fix x :: int and X :: "int set" assume "x \ X" "bdd_below X" then show "Inf X \ x"
      using le_Sup[of "-x" "uminus ` X"] by (auto simp: Inf_int_def) }
  { fix x :: int and X :: "int set" assume "X \ {}" "\y. y \ X \ x \ y" then show "x \ Inf X"
      using Sup_le[of "uminus ` X" "-x"] by (force simp: Inf_int_def) }
qed
end

lemma interval_cases:
  fixes S :: "'a :: conditionally_complete_linorder set"
  assumes ivl: "\a b x. a \ S \ b \ S \ a \ x \ x \ b \ x \ S"
  shows "\a b. S = {} \
    S = UNIV \<or>
    S = {..<b} \<or>
    S = {..b} \<or>
    S = {a<..} \<or>
    S = {a..} \<or>
    S = {a<..<b} \<or>
    S = {a<..b} \<or>
    S = {a..<b} \<or>
    S = {a..b}"
proof -
  define lower upper where "lower = {x. \s\S. s \ x}" and "upper = {x. \s\S. x \ s}"
  with ivl have "S = lower \ upper"
    by auto
  moreover
  have "\a. upper = UNIV \ upper = {} \ upper = {.. a} \ upper = {..< a}"
  proof cases
    assume *: "bdd_above S \ S \ {}"
    from * have "upper \ {.. Sup S}"
      by (auto simp: upper_def intro: cSup_upper2)
    moreover from * have "{..< Sup S} \ upper"
      by (force simp add: less_cSup_iff upper_def subset_eq Ball_def)
    ultimately have "upper = {.. Sup S} \ upper = {..< Sup S}"
      unfolding ivl_disj_un(2)[symmetric] by auto
    then show ?thesis by auto
  next
    assume "\ (bdd_above S \ S \ {})"
    then have "upper = UNIV \ upper = {}"
      by (auto simp: upper_def bdd_above_def not_le dest: less_imp_le)
    then show ?thesis
      by auto
  qed
  moreover
  have "\b. lower = UNIV \ lower = {} \ lower = {b ..} \ lower = {b <..}"
  proof cases
    assume *: "bdd_below S \ S \ {}"
    from * have "lower \ {Inf S ..}"
      by (auto simp: lower_def intro: cInf_lower2)
    moreover from * have "{Inf S <..} \ lower"
      by (force simp add: cInf_less_iff lower_def subset_eq Ball_def)
    ultimately have "lower = {Inf S ..} \ lower = {Inf S <..}"
      unfolding ivl_disj_un(1)[symmetric] by auto
    then show ?thesis by auto
  next
    assume "\ (bdd_below S \ S \ {})"
    then have "lower = UNIV \ lower = {}"
      by (auto simp: lower_def bdd_below_def not_le dest: less_imp_le)
    then show ?thesis
      by auto
  qed
  ultimately show ?thesis
    unfolding greaterThanAtMost_def greaterThanLessThan_def atLeastAtMost_def atLeastLessThan_def
    by (metis inf_bot_left inf_bot_right inf_top.left_neutral inf_top.right_neutral)
qed

lemma cSUP_eq_cINF_D:
  fixes f :: "_ \ 'b::conditionally_complete_lattice"
  assumes eq: "(\x\A. f x) = (\x\A. f x)"
     and bdd: "bdd_above (f ` A)" "bdd_below (f ` A)"
     and a: "a \ A"
  shows "f a = (\x\A. f x)"
proof (rule antisym)
  show "f a \ \ (f ` A)"
    by (metis a bdd(1) eq cSUP_upper)
  show "\ (f ` A) \ f a"
    using a bdd by (auto simp: cINF_lower)
qed

lemma cSUP_UNION:
  fixes f :: "_ \ 'b::conditionally_complete_lattice"
  assumes ne: "A \ {}" "\x. x \ A \ B(x) \ {}"
      and bdd_UN: "bdd_above (\x\A. f ` B x)"
  shows "(\z \ \x\A. B x. f z) = (\x\A. \z\B x. f z)"
proof -
  have bdd: "\x. x \ A \ bdd_above (f ` B x)"
    using bdd_UN by (meson UN_upper bdd_above_mono)
  obtain M where "\x y. x \ A \ y \ B(x) \ f y \ M"
    using bdd_UN by (auto simp: bdd_above_def)
  then have bdd2: "bdd_above ((\x. \z\B x. f z) ` A)"
    unfolding bdd_above_def by (force simp: bdd cSUP_le_iff ne(2))
  have "(\z \ \x\A. B x. f z) \ (\x\A. \z\B x. f z)"
    using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper2 simp: bdd2 bdd)
  moreover have "(\x\A. \z\B x. f z) \ (\ z \ \x\A. B x. f z)"
    using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper simp: image_UN bdd_UN)
  ultimately show ?thesis
    by (rule order_antisym)
qed

lemma cINF_UNION:
  fixes f :: "_ \ 'b::conditionally_complete_lattice"
  assumes ne: "A \ {}" "\x. x \ A \ B(x) \ {}"
      and bdd_UN: "bdd_below (\x\A. f ` B x)"
  shows "(\z \ \x\A. B x. f z) = (\x\A. \z\B x. f z)"
proof -
  have bdd: "\x. x \ A \ bdd_below (f ` B x)"
    using bdd_UN by (meson UN_upper bdd_below_mono)
  obtain M where "\x y. x \ A \ y \ B(x) \ f y \ M"
    using bdd_UN by (auto simp: bdd_below_def)
  then have bdd2: "bdd_below ((\x. \z\B x. f z) ` A)"
    unfolding bdd_below_def by (force simp: bdd le_cINF_iff ne(2))
  have "(\z \ \x\A. B x. f z) \ (\x\A. \z\B x. f z)"
    using assms by (fastforce simp add: intro!: cINF_greatest intro: cINF_lower simp: bdd2 bdd)
  moreover have "(\x\A. \z\B x. f z) \ (\z \ \x\A. B x. f z)"
    using assms  by (fastforce simp add: intro!: cINF_greatest intro: cINF_lower2  simp: bdd bdd_UN bdd2)
  ultimately show ?thesis
    by (rule order_antisym)
qed

lemma cSup_abs_le:
  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
  shows "S \ {} \ (\x. x\S \ \x\ \ a) \ \Sup S\ \ a"
  apply (auto simp add: abs_le_iff intro: cSup_least)
  by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans)

end

quality95%

¤ Dauer der Verarbeitung: 0.25 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.