Impressum ProgressSets.thy Sprache: Isabelle

(*  Title:      HOL/UNITY/ProgressSets.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   2003  University of Cambridge

Progress Sets.  From

    David Meier and Beverly Sanders,
    Composing Leads-to Properties
    Theoretical Computer Science 243:1-2 (2000), 339-361.

    David Meier,
    Progress Properties in Program Refinement and Parallel Composition
    Swiss Federal Institute of Technology Zurich (1997)
*)

section\<open>Progress Sets\<close>

theory ProgressSets imports Transformers begin

subsection \<open>Complete Lattices and the Operator \<^term>\<open>cl\<close>\<close>

definition lattice :: "'a set set => bool" where
   \<comment> \<open>Meier calls them closure sets, but they are just complete lattices\<close>
   "lattice L ==
         (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)"

definition cl :: "['a set set, 'a set] => 'a set" where
   \<comment> \<open>short for ``closure''\<close>
   "cl L r == \{x. x\L & r \ x}"

lemma UNIV_in_lattice: "lattice L ==> UNIV \ L"
by (force simp add: lattice_def)

lemma empty_in_lattice: "lattice L ==> {} \ L"
by (force simp add: lattice_def)

lemma Union_in_lattice: "[|M \ L; lattice L|] ==> \M \ L"
by (simp add: lattice_def)

lemma Inter_in_lattice: "[|M \ L; lattice L|] ==> \M \ L"
by (simp add: lattice_def)

lemma UN_in_lattice:
     "[|lattice L; !!i. i\I ==> r i \ L|] ==> (\i\I. r i) \ L"
apply (blast intro: Union_in_lattice)
done

lemma INT_in_lattice:
     "[|lattice L; !!i. i\I ==> r i \ L|] ==> (\i\I. r i) \ L"
apply (blast intro: Inter_in_lattice)
done

lemma Un_in_lattice: "[|x\L; y\L; lattice L|] ==> x\y \ L"
  using Union_in_lattice [of "{x, y}" L] by simp

lemma Int_in_lattice: "[|x\L; y\L; lattice L|] ==> x\y \ L"
  using Inter_in_lattice [of "{x, y}" L] by simp

lemma lattice_stable: "lattice {X. F \ stable X}"
by (simp add: lattice_def stable_def constrains_def, blast)

text\<open>The next three results state that \<^term>\<open>cl L r\<close> is the minimal
element of \<^term>\<open>L\<close> that includes \<^term>\<open>r\<close>.\<close>
lemma cl_in_lattice: "lattice L ==> cl L r \ L"
  by (simp add: lattice_def cl_def)

lemma cl_least: "[|c\L; r\c|] ==> cl L r \ c"
by (force simp add: cl_def)

text\<open>The next three lemmas constitute assertion (4.61)\<close>
lemma cl_mono: "r \ r' ==> cl L r \ cl L r'"
by (simp add: cl_def, blast)

lemma subset_cl: "r \ cl L r"
by (simp add: cl_def le_Inf_iff)

text\<open>A reformulation of @{thm subset_cl}\<close>
lemma clI: "x \ r ==> x \ cl L r"
by (simp add: cl_def, blast)

text\<open>A reformulation of @{thm cl_least}\<close>
lemma clD: "[|c \ cl L r; B \ L; r \ B|] ==> c \ B"
by (force simp add: cl_def)

lemma cl_UN_subset: "(\i\I. cl L (r i)) \ cl L (\i\I. r i)"
by (simp add: cl_def, blast)

lemma cl_Un: "lattice L ==> cl L (r\s) = cl L r \ cl L s"
apply (rule equalityI)
prefer 2
  apply (simp add: cl_def, blast)
apply (rule cl_least)
apply (blast intro: Un_in_lattice cl_in_lattice)
apply (blast intro: subset_cl [THEN subsetD])
done

lemma cl_UN: "lattice L ==> cl L (\i\I. r i) = (\i\I. cl L (r i))"
apply (rule equalityI)
prefer 2 apply (simp add: cl_def, blast)
apply (rule cl_least)
apply (blast intro: UN_in_lattice cl_in_lattice)
apply (blast intro: subset_cl [THEN subsetD])
done

lemma cl_Int_subset: "cl L (r\s) \ cl L r \ cl L s"
by (simp add: cl_def, blast)

lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
by (simp add: cl_def, blast)

lemma cl_ident: "r\L ==> cl L r = r"
by (force simp add: cl_def)

lemma cl_empty [simp]: "lattice L ==> cl L {} = {}"
by (simp add: cl_ident empty_in_lattice)

lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV"
by (simp add: cl_ident UNIV_in_lattice)

text\<open>Assertion (4.62)\<close>
lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\L)"
apply (rule iffI)
apply (erule subst)
apply (erule cl_in_lattice)
apply (erule cl_ident)
done

lemma cl_subset_in_lattice: "[|cl L r \ r; lattice L|] ==> r\L"
by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)

subsection \<open>Progress Sets and the Main Lemma\<close>
text\<open>A progress set satisfies certain closure conditions and is a
simple way of including the set \<^term>\<open>wens_set F B\<close>.\<close>

definition closed :: "['a program, 'a set, 'a set, 'a set set] => bool" where
   "closed F T B L == \M. \act \ Acts F. B\M & T\M \ L -->
                              T \<inter> (B \<union> wp act M) \<in> L"

definition progress_set :: "['a program, 'a set, 'a set] => 'a set set set" where
   "progress_set F T B ==
      {L. lattice L & B \<in> L & T \<in> L & closed F T B L}"

lemma closedD:
   "[|closed F T B L; act \ Acts F; B\M; T\M \ L|]
    ==> T \<inter> (B \<union> wp act M) \<in> L"
by (simp add: closed_def)

text\<open>Note: the formalization below replaces Meier's \<^term>\<open>q\<close> by \<^term>\<open>B\<close>
and \<^term>\<open>m\<close> by \<^term>\<open>X\<close>.\<close>

text\<open>Part of the proof of the claim at the bottom of page 97.  It's
proved separately because the argument requires a generalization over
all \<^term>\<open>act \<in> Acts F\<close>.\<close>
lemma lattice_awp_lemma:
  assumes TXC:  "T\X \ C" \ \induction hypothesis in theorem below\
      and BsubX:  "B \ X" \ \holds in inductive step\
      and latt: "lattice C"
      and TC:   "T \ C"
      and BC:   "B \ C"
      and clos: "closed F T B C"
    shows "T \ (B \ awp F (X \ cl C (T\r))) \ C"
apply (simp del: INT_simps add: awp_def INT_extend_simps)
apply (rule INT_in_lattice [OF latt])
apply (erule closedD [OF clos])
apply (simp add: subset_trans [OF BsubX Un_upper1])
apply (subgoal_tac "T \ (X \ cl C (T\r)) = (T\X) \ cl C (T\r)")
prefer 2 apply (blast intro: TC clD)
apply (erule ssubst)
apply (blast intro: Un_in_lattice latt cl_in_lattice TXC)
done

text\<open>Remainder of the proof of the claim at the bottom of page 97.\<close>
lemma lattice_lemma:
  assumes TXC:  "T\X \ C" \ \induction hypothesis in theorem below\
      and BsubX:  "B \ X" \ \holds in inductive step\
      and act:  "act \ Acts F"
      and latt: "lattice C"
      and TC:   "T \ C"
      and BC:   "B \ C"
      and clos: "closed F T B C"
    shows "T \ (wp act X \ awp F (X \ cl C (T\r)) \ X) \ C"
apply (subgoal_tac "T \ (B \ wp act X) \ C")
prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
apply (drule Int_in_lattice
              [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
                    latt])
apply (subgoal_tac
         "T \ (B \ wp act X) \ (T \ (B \ awp F (X \ cl C (T\r)))) =
          T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))")
prefer 2 apply blast
apply simp
apply (drule Un_in_lattice [OF _ TXC latt])
apply (subgoal_tac
         "T \ (B \ wp act X \ awp F (X \ cl C (T\r))) \ T\X =
          T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)")
apply simp
apply (blast intro: BsubX [THEN subsetD])
done

text\<open>Induction step for the main lemma\<close>
lemma progress_induction_step:
  assumes TXC:  "T\X \ C" \ \induction hypothesis in theorem below\
      and act:  "act \ Acts F"
      and Xwens: "X \ wens_set F B"
      and latt: "lattice C"
      and  TC:  "T \ C"
      and  BC:  "B \ C"
      and clos: "closed F T B C"
      and Fstable: "F \ stable T"
  shows "T \ wens F act X \ C"
proof -
  from Xwens have BsubX: "B \ X"
    by (rule wens_set_imp_subset)
  let ?r = "wens F act X"
  have "?r \ (wp act X \ awp F (X\?r)) \ X"
    by (simp add: wens_unfold [symmetric])
  then have "T\?r \ T \ ((wp act X \ awp F (X\?r)) \ X)"
    by blast
  then have "T\?r \ T \ ((wp act X \ awp F (T \ (X\?r))) \ X)"
    by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast)
  then have "T\?r \ T \ ((wp act X \ awp F (X \ cl C (T\?r))) \ X)"
    by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
  then have "cl C (T\?r) \
             cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))"
    by (rule cl_mono)
  then have "cl C (T\?r) \
             T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
    by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
  then have "cl C (T\?r) \ (wp act X \ awp F (X \ cl C (T\?r))) \ X"
    by blast
  then have "cl C (T\?r) \ ?r"
    by (blast intro!: subset_wens)
  then have cl_subset: "cl C (T\?r) \ T\?r"
    by (simp add: cl_ident TC
                  subset_trans [OF cl_mono [OF Int_lower1]])
  show ?thesis
    by (rule cl_subset_in_lattice [OF cl_subset latt])
qed

text\<open>Proved on page 96 of Meier's thesis.  The special case when
   \<^term>\<open>T=UNIV\<close> states that every progress set for the program \<^term>\<open>F\<close>
   and set \<^term>\<open>B\<close> includes the set \<^term>\<open>wens_set F B\<close>.\<close>
lemma progress_set_lemma:
     "[|C \ progress_set F T B; r \ wens_set F B; F \ stable T|] ==> T\r \ C"
apply (simp add: progress_set_def, clarify)
apply (erule wens_set.induct)
  txt\<open>Base\<close>
  apply (simp add: Int_in_lattice)
txt\<open>The difficult \<^term>\<open>wens\<close> case\<close>
apply (simp add: progress_induction_step)
txt\<open>Disjunctive case\<close>
apply (subgoal_tac "(\U\W. T \ U) \ C")
apply simp
apply (blast intro: UN_in_lattice)
done

subsection \<open>The Progress Set Union Theorem\<close>

lemma closed_mono:
  assumes BB': "B \ B'"
      and TBwp: "T \ (B \ wp act M) \ C"
      and B'C: "B' \<in> C"
      and TC:   "T \ C"
      and latt: "lattice C"
  shows "T \ (B' \ wp act M) \ C"
proof -
  from TBwp have "(T\B) \ (T \ wp act M) \ C"
    by (simp add: Int_Un_distrib)
  then have TBBC: "(T\B') \ ((T\B) \ (T \ wp act M)) \ C"
    by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt)
  show ?thesis
    by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC],
        blast intro: BB' [THEN subsetD])
qed

lemma progress_set_mono:
    assumes BB': "B \ B'"
    shows
     "[| B' \ C; C \ progress_set F T B|]
      ==> C \<in> progress_set F T B'"
by (simp add: progress_set_def closed_def closed_mono [OF BB']
                 subset_trans [OF BB'])

theorem progress_set_Union:
  assumes leadsTo: "F \ A leadsTo B'"
      and prog: "C \ progress_set F T B"
      and Fstable: "F \ stable T"
      and BB': "B \ B'"
      and B'C: "B' \<in> C"
      and Gco: "!!X. X\C ==> G \ X-B co X"
  shows "F\G \ T\A leadsTo B'"
apply (insert prog Fstable)
apply (rule leadsTo_Join [OF leadsTo])
  apply (force simp add: progress_set_def awp_iff_stable [symmetric])
apply (simp add: awp_iff_constrains)
apply (drule progress_set_mono [OF BB' B'C])
apply (blast intro: progress_set_lemma Gco constrains_weaken_L
                    BB' [THEN subsetD])
done

subsection \<open>Some Progress Sets\<close>

lemma UNIV_in_progress_set: "UNIV \ progress_set F T B"
by (simp add: progress_set_def lattice_def closed_def)

subsubsection \<open>Lattices and Relations\<close>
text\<open>From Meier's thesis, section 4.5.3\<close>

definition relcl :: "'a set set => ('a * 'a) set" where
    \<comment> \<open>Derived relation from a lattice\<close>
    "relcl L == {(x,y). y \ cl L {x}}"

definition latticeof :: "('a * 'a) set => 'a set set" where
    \<comment> \<open>Derived lattice from a relation: the set of upwards-closed sets\<close>
    "latticeof r == {X. \s t. s \ X & (s,t) \ r --> t \ X}"

lemma relcl_refl: "(a,a) \ relcl L"
by (simp add: relcl_def subset_cl [THEN subsetD])

lemma relcl_trans:
     "[| (a,b) \ relcl L; (b,c) \ relcl L; lattice L |] ==> (a,c) \ relcl L"
apply (simp add: relcl_def)
apply (blast intro: clD cl_in_lattice)
done

lemma refl_relcl: "lattice L ==> refl (relcl L)"
by (simp add: refl_onI relcl_def subset_cl [THEN subsetD])

lemma trans_relcl: "lattice L ==> trans (relcl L)"
by (blast intro: relcl_trans transI)

lemma lattice_latticeof: "lattice (latticeof r)"
by (auto simp add: lattice_def latticeof_def)

lemma lattice_singletonI:
     "[|lattice L; !!s. s \ X ==> {s} \ L|] ==> X \ L"
apply (cut_tac UN_singleton [of X])
apply (erule subst)
apply (simp only: UN_in_lattice)
done

text\<open>Equation (4.71) of Meier's thesis.  He gives no proof.\<close>
lemma cl_latticeof:
     "[|refl r; trans r|]
      ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}"
apply (rule equalityI)
apply (rule cl_least)
  apply (simp (no_asm_use) add: latticeof_def trans_def, blast)
apply (simp add: latticeof_def refl_on_def, blast)
apply (simp add: latticeof_def, clarify)
apply (unfold cl_def, blast)
done

text\<open>Related to (4.71).\<close>
lemma cl_eq_Collect_relcl:
     "lattice L ==> cl L X = {t. \s. s\X & (s,t) \ relcl L}"
apply (cut_tac UN_singleton [of X])
apply (erule subst)
apply (force simp only: relcl_def cl_UN)
done

text\<open>Meier's theorem of section 4.5.3\<close>
theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L"
apply (rule equalityI)
prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify)
apply (rename_tac X)
apply (rule cl_subset_in_lattice)
prefer 2 apply assumption
apply (drule cl_ident_iff [OF lattice_latticeof, THEN iffD2])
apply (drule equalityD1)
apply (rule subset_trans)
prefer 2 apply assumption
apply (thin_tac "_ \ X")
apply (cut_tac A=X in UN_singleton)
apply (erule subst)
apply (simp only: cl_UN lattice_latticeof
                  cl_latticeof [OF refl_relcl trans_relcl])
apply (simp add: relcl_def)
done

theorem relcl_latticeof_eq:
     "[|refl r; trans r|] ==> relcl (latticeof r) = r"
by (simp add: relcl_def cl_latticeof)

subsubsection \<open>Decoupling Theorems\<close>

definition decoupled :: "['a program, 'a program] => bool" where
   "decoupled F G ==
        \<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)"

text\<open>Rao's Decoupling Theorem\<close>
lemma stableco: "F \ stable A ==> F \ A-B co A"
by (simp add: stable_def constrains_def, blast)

theorem decoupling:
  assumes leadsTo: "F \ A leadsTo B"
      and Gstable: "G \ stable B"
      and dec:     "decoupled F G"
  shows "F\G \ A leadsTo B"
proof -
  have prog: "{X. G \ stable X} \ progress_set F UNIV B"
    by (simp add: progress_set_def lattice_stable Gstable closed_def
                  stable_Un [OF Gstable] dec [unfolded decoupled_def])
  have "F\G \ (UNIV\A) leadsTo B"
    by (rule progress_set_Union [OF leadsTo prog],
        simp_all add: Gstable stableco)
  thus ?thesis by simp
qed

text\<open>Rao's Weak Decoupling Theorem\<close>
theorem weak_decoupling:
  assumes leadsTo: "F \ A leadsTo B"
      and stable: "F\G \ stable B"
      and dec:     "decoupled F (F\G)"
  shows "F\G \ A leadsTo B"
proof -
  have prog: "{X. F\G \ stable X} \ progress_set F UNIV B"
    by (simp del: Join_stable
             add: progress_set_def lattice_stable stable closed_def
                  stable_Un [OF stable] dec [unfolded decoupled_def])
  have "F\G \ (UNIV\A) leadsTo B"
    by (rule progress_set_Union [OF leadsTo prog],
        simp_all del: Join_stable add: stable,
        simp add: stableco)
  thus ?thesis by simp
qed

text\<open>The ``Decoupling via \<^term>\<open>G'\<close> Union Theorem''\<close>
theorem decoupling_via_aux:
  assumes leadsTo: "F \ A leadsTo B"
      and prog: "{X. G' \ stable X} \ progress_set F UNIV B"
      and GG': "G \ G'"
               \<comment> \<open>Beware!  This is the converse of the refinement relation!\<close>
  shows "F\G \ A leadsTo B"
proof -
  from prog have stable: "G' \ stable B"
    by (simp add: progress_set_def)
  have "F\G \ (UNIV\A) leadsTo B"
    by (rule progress_set_Union [OF leadsTo prog],
        simp_all add: stable stableco component_stable [OF GG'])
  thus ?thesis by simp
qed

subsection\<open>Composition Theorems Based on Monotonicity and Commutativity\<close>

subsubsection\<open>Commutativity of \<^term>\<open>cl L\<close> and assignment.\<close>
definition commutes :: "['a program, 'a set, 'a set, 'a set set] => bool" where
   "commutes F T B L ==
       \<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M -->
           cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"

text\<open>From Meier's thesis, section 4.5.6\<close>
lemma commutativity1_lemma:
  assumes commutes: "commutes F T B L"
      and lattice:  "lattice L"
      and BL: "B \ L"
      and TL: "T \ L"
  shows "closed F T B L"
apply (simp add: closed_def, clarify)
apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])
apply (simp add: Int_Un_distrib cl_Un [OF lattice]
                 cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
apply (subgoal_tac "cl L (T \ wp act M) \ T \ (B \ wp act (cl L (T \ M)))")
prefer 2
apply (cut_tac commutes, simp add: commutes_def)
apply (erule subset_trans)
apply (simp add: cl_ident)
apply (blast intro: rev_subsetD [OF _ wp_mono])
done

text\<open>Version packaged with @{thm progress_set_Union}\<close>
lemma commutativity1:
  assumes leadsTo: "F \ A leadsTo B"
      and lattice:  "lattice L"
      and BL: "B \ L"
      and TL: "T \ L"
      and Fstable: "F \ stable T"
      and Gco: "!!X. X\L ==> G \ X-B co X"
      and commutes: "commutes F T B L"
  shows "F\G \ T\A leadsTo B"
by (rule progress_set_Union [OF leadsTo _ Fstable subset_refl BL Gco],
    simp add: progress_set_def commutativity1_lemma commutes lattice BL TL)

text\<open>Possibly move to Relation.thy, after \<^term>\<open>single_valued\<close>\<close>
definition funof :: "[('a*'b)set, 'a] => 'b" where
   "funof r == (\x. THE y. (x,y) \ r)"

lemma funof_eq: "[|single_valued r; (x,y) \ r|] ==> funof r x = y"
by (simp add: funof_def single_valued_def, blast)

lemma funof_Pair_in:
     "[|single_valued r; x \ Domain r|] ==> (x, funof r x) \ r"
by (force simp add: funof_eq)

lemma funof_in:
     "[|r``{x} \ A; single_valued r; x \ Domain r|] ==> funof r x \ A"
by (force simp add: funof_eq)

lemma funof_imp_wp: "[|funof act t \ A; single_valued act|] ==> t \ wp act A"
by (force simp add: in_wp_iff funof_eq)

subsubsection\<open>Commutativity of Functions and Relation\<close>
text\<open>Thesis, page 109\<close>

(*FIXME: this proof is still an ungodly mess*)
text\<open>From Meier's thesis, section 4.5.6\<close>
lemma commutativity2_lemma:
  assumes dcommutes:
      "\act s t. act \ Acts F \ s \ T \ (s, t) \ relcl L \
        s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
    and determ: "!!act. act \ Acts F ==> single_valued act"
    and total: "!!act. act \ Acts F ==> Domain act = UNIV"
    and lattice:  "lattice L"
    and BL: "B \ L"
    and TL: "T \ L"
    and Fstable: "F \ stable T"
  shows  "commutes F T B L"
proof -
  { fix M and act and t
    assume 1: "B \ M" "act \ Acts F" "t \ cl L (T \ wp act M)"
    then have "\s. (s,t) \ relcl L \ s \ T \ wp act M"
      by (force simp add: cl_eq_Collect_relcl [OF lattice])
    then obtain s where 2: "(s, t) \ relcl L" "s \ T" "s \ wp act M"
      by blast
    then have 3: "\u\L. s \ u --> t \ u"
      apply (intro ballI impI)
      apply (subst cl_ident [symmetric], assumption)
      apply (simp add: relcl_def)
      apply (blast intro: cl_mono [THEN [2] rev_subsetD])
      done
    with 1 2 Fstable have 4: "funof act s \ T\M"
      by (force intro!: funof_in
        simp add: wp_def stable_def constrains_def determ total)
    with 1 2 3 have 5: "s \ B | t \ B | (funof act s, funof act t) \ relcl L"
      by (intro dcommutes) assumption+
    with 1 2 3 4 have "t \ B | funof act t \ cl L (T\M)"
      by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD])
    with 1 2 3 4 5 have "t \ B | t \ wp act (cl L (T\M))"
      by (blast intro: funof_imp_wp determ)
    with 2 3 have "t \ T \ (t \ B \ t \ wp act (cl L (T \ M)))"
      by (blast intro: TL cl_mono [THEN [2] rev_subsetD])
    then have"t \ T \ (B \ wp act (cl L (T \ M)))"
      by simp
  }
  then show "commutes F T B L" unfolding commutes_def by clarify
qed

text\<open>Version packaged with @{thm progress_set_Union}\<close>
lemma commutativity2:
  assumes leadsTo: "F \ A leadsTo B"
      and dcommutes:
        "\act \ Acts F.
         \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L -->
                      s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
      and determ: "!!act. act \ Acts F ==> single_valued act"
      and total: "!!act. act \ Acts F ==> Domain act = UNIV"
      and lattice:  "lattice L"
      and BL: "B \ L"
      and TL: "T \ L"
      and Fstable: "F \ stable T"
      and Gco: "!!X. X\L ==> G \ X-B co X"
  shows "F\G \ T\A leadsTo B"
apply (rule commutativity1 [OF leadsTo lattice])
apply (simp_all add: Gco commutativity2_lemma dcommutes determ total
                     lattice BL TL Fstable)
done

subsection \<open>Monotonicity\<close>
text\<open>From Meier's thesis, section 4.5.7, page 110\<close>
(*to be continued?*)

end

quality100%

¤ 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.0.13Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.