SSL PriorityAux.thy Interaktion und
PortierbarkeitIsabelle

(*  Title:      HOL/UNITY/Comp/PriorityAux.thy
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    Copyright   2001  University of Cambridge

Auxiliary definitions needed in Priority.thy
*)

theory PriorityAux
imports "../UNITY_Main"
begin

typedecl vertex

definition symcl :: "(vertex*vertex)set=>(vertex*vertex)set" where
  "symcl r == r \ (r\)"
    \<comment> \<open>symmetric closure: removes the orientation of a relation\<close>

definition neighbors :: "[vertex, (vertex*vertex)set]=>vertex set" where
  "neighbors i r == ((r \ r\)``{i}) - {i}"
    \<comment> \<open>Neighbors of a vertex i\<close>

definition R :: "[vertex, (vertex*vertex)set]=>vertex set" where
  "R i r == r``{i}"

definition A :: "[vertex, (vertex*vertex)set]=>vertex set" where
  "A i r == (r\)``{i}"

definition reach :: "[vertex, (vertex*vertex)set]=> vertex set" where
  "reach i r == (r\<^sup>+)``{i}"
    \<comment> \<open>reachable and above vertices: the original notation was R* and A*\<close>

definition above :: "[vertex, (vertex*vertex)set]=> vertex set" where
  "above i r == ((r\)\<^sup>+)``{i}"

definition reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set" where
  "reverse i r == (r - {(x,y). x=i | y=i} \ r) \ ({(x,y). x=i|y=i} \ r)\"

definition derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" where
    \<comment> \<open>The original definition\<close>
  "derive1 i r q == symcl r = symcl q &
                    (\<forall>k k'. k\<noteq>i & k'\<noteq>i -->((k,k') \<in> r) = ((k,k') \<in> q)) \<and>
                    A i r = {} & R i q = {}"

definition derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" where
    \<comment> \<open>Our alternative definition\<close>
  "derive i r q == A i r = {} & (q = reverse i r)"

axiomatization where
  finite_vertex_univ:  "finite (UNIV :: vertex set)"
    \<comment> \<open>we assume that the universe of vertices is finite\<close>

declare derive_def [simp] derive1_def [simp] symcl_def [simp]
        A_def [simp] R_def [simp]
        above_def [simp] reach_def [simp]
        reverse_def [simp] neighbors_def [simp]

text\<open>All vertex sets are finite\<close>
declare finite_subset [OF subset_UNIV finite_vertex_univ, iff]

text\<open>and relatons over vertex are finite too\<close>

lemmas finite_UNIV_Prod =
       finite_Prod_UNIV [OF finite_vertex_univ finite_vertex_univ]

declare finite_subset [OF subset_UNIV finite_UNIV_Prod, iff]

(* The equalities (above i r = {}) = (A i r = {})
   and (reach i r = {}) = (R i r) rely on the following theorem  *)

lemma image0_trancl_iff_image0_r: "((r\<^sup>+)``{i} = {}) = (r``{i} = {})"
apply auto
apply (erule trancl_induct, auto)
done

(* Another form usefull in some situation *)
lemma image0_r_iff_image0_trancl: "(r``{i}={}) = (\x. ((i,x) \ r\<^sup>+) = False)"
apply auto
apply (drule image0_trancl_iff_image0_r [THEN ssubst], auto)
done

(* In finite universe acyclic coincides with wf *)
lemma acyclic_eq_wf: "!!r::(vertex*vertex)set. acyclic r = wf r"
by (auto simp add: wf_iff_acyclic_if_finite)

(* derive and derive1 are equivalent *)
lemma derive_derive1_eq: "derive i r q = derive1 i r q"
by auto

(* Lemma 1 *)
lemma lemma1_a:
     "[| x \ reach i q; derive1 k r q |] ==> x\k --> x \ reach i r"
apply (unfold reach_def)
apply (erule ImageE)
apply (erule trancl_induct)
apply (cases "i=k", simp_all)
apply (blast, blast, clarify)
apply (drule_tac x = y in spec)
apply (drule_tac x = z in spec)
apply (blast dest: r_into_trancl intro: trancl_trans)
done

lemma reach_lemma: "derive k r q ==> reach i q \ (reach i r \ {k})"
apply clarify
apply (drule lemma1_a)
apply (auto simp add: derive_derive1_eq
            simp del: reach_def derive_def derive1_def)
done

(* An other possible formulation of the above theorem based on
   the equivalence x \<in> reach y r = y \<in> above x r                  *)
lemma reach_above_lemma:
      "(\i. reach i q \ (reach i r \ {k})) =
       (\<forall>x. x\<noteq>k --> (\<forall>i. i \<notin> above x r --> i \<notin> above x q))"
by (auto simp add: trancl_converse)

(* Lemma 2 *)
lemma maximal_converse_image0:
     "(z, i) \ r\<^sup>+ \ (\y. (y, z) \ r \ (y,i) \ r\<^sup>+) = ((r\)``{z}={})"
apply auto
apply (frule_tac r = r in trancl_into_trancl2, auto)
done

lemma above_lemma_a:
     "acyclic r ==> A i r\{}-->(\j \ above i r. A j r = {})"
apply (simp add: acyclic_eq_wf wf_eq_minimal)
apply (drule_tac x = " ((r\)\<^sup>+) ``{i}" in spec)
apply auto
apply (simp add: maximal_converse_image0 trancl_converse)
done

lemma above_lemma_b:
     "acyclic r ==> above i r\{}-->(\j \ above i r. above j r = {})"
apply (drule above_lemma_a)
apply (auto simp add: image0_trancl_iff_image0_r)
done

end

quality100%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

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.

SSL PriorityAux.thy Interaktion und PortierbarkeitIsabelle

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

Haftungshinweis

Bemerkung:

SSL PriorityAux.thy Interaktion und
PortierbarkeitIsabelle