1(* Title: HOL/UNITY/Comp/PriorityAux.thy 2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory 3 Copyright 2001 University of Cambridge 4 5Auxiliary definitions needed in Priority.thy 6*) 7 8theory PriorityAux 9imports "../UNITY_Main" 10begin 11 12typedecl vertex 13 14definition symcl :: "(vertex*vertex)set=>(vertex*vertex)set" where 15 "symcl r == r \<union> (r\<inverse>)" 16 \<comment> \<open>symmetric closure: removes the orientation of a relation\<close> 17 18definition neighbors :: "[vertex, (vertex*vertex)set]=>vertex set" where 19 "neighbors i r == ((r \<union> r\<inverse>)``{i}) - {i}" 20 \<comment> \<open>Neighbors of a vertex i\<close> 21 22definition R :: "[vertex, (vertex*vertex)set]=>vertex set" where 23 "R i r == r``{i}" 24 25definition A :: "[vertex, (vertex*vertex)set]=>vertex set" where 26 "A i r == (r\<inverse>)``{i}" 27 28definition reach :: "[vertex, (vertex*vertex)set]=> vertex set" where 29 "reach i r == (r\<^sup>+)``{i}" 30 \<comment> \<open>reachable and above vertices: the original notation was R* and A*\<close> 31 32definition above :: "[vertex, (vertex*vertex)set]=> vertex set" where 33 "above i r == ((r\<inverse>)\<^sup>+)``{i}" 34 35definition reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set" where 36 "reverse i r == (r - {(x,y). x=i | y=i} \<inter> r) \<union> ({(x,y). x=i|y=i} \<inter> r)\<inverse>" 37 38definition derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" where 39 \<comment> \<open>The original definition\<close> 40 "derive1 i r q == symcl r = symcl q & 41 (\<forall>k k'. k\<noteq>i & k'\<noteq>i -->((k,k') \<in> r) = ((k,k') \<in> q)) \<and> 42 A i r = {} & R i q = {}" 43 44definition derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" where 45 \<comment> \<open>Our alternative definition\<close> 46 "derive i r q == A i r = {} & (q = reverse i r)" 47 48axiomatization where 49 finite_vertex_univ: "finite (UNIV :: vertex set)" 50 \<comment> \<open>we assume that the universe of vertices is finite\<close> 51 52declare derive_def [simp] derive1_def [simp] symcl_def [simp] 53 A_def [simp] R_def [simp] 54 above_def [simp] reach_def [simp] 55 reverse_def [simp] neighbors_def [simp] 56 57text\<open>All vertex sets are finite\<close> 58declare finite_subset [OF subset_UNIV finite_vertex_univ, iff] 59 60text\<open>and relatons over vertex are finite too\<close> 61 62lemmas finite_UNIV_Prod = 63 finite_Prod_UNIV [OF finite_vertex_univ finite_vertex_univ] 64 65declare finite_subset [OF subset_UNIV finite_UNIV_Prod, iff] 66 67 68(* The equalities (above i r = {}) = (A i r = {}) 69 and (reach i r = {}) = (R i r) rely on the following theorem *) 70 71lemma image0_trancl_iff_image0_r: "((r\<^sup>+)``{i} = {}) = (r``{i} = {})" 72apply auto 73apply (erule trancl_induct, auto) 74done 75 76(* Another form usefull in some situation *) 77lemma image0_r_iff_image0_trancl: "(r``{i}={}) = (\<forall>x. ((i,x) \<in> r\<^sup>+) = False)" 78apply auto 79apply (drule image0_trancl_iff_image0_r [THEN ssubst], auto) 80done 81 82 83(* In finite universe acyclic coincides with wf *) 84lemma acyclic_eq_wf: "!!r::(vertex*vertex)set. acyclic r = wf r" 85by (auto simp add: wf_iff_acyclic_if_finite) 86 87(* derive and derive1 are equivalent *) 88lemma derive_derive1_eq: "derive i r q = derive1 i r q" 89by auto 90 91(* Lemma 1 *) 92lemma lemma1_a: 93 "[| x \<in> reach i q; derive1 k r q |] ==> x\<noteq>k --> x \<in> reach i r" 94apply (unfold reach_def) 95apply (erule ImageE) 96apply (erule trancl_induct) 97 apply (cases "i=k", simp_all) 98 apply (blast, blast, clarify) 99apply (drule_tac x = y in spec) 100apply (drule_tac x = z in spec) 101apply (blast dest: r_into_trancl intro: trancl_trans) 102done 103 104lemma reach_lemma: "derive k r q ==> reach i q \<subseteq> (reach i r \<union> {k})" 105apply clarify 106apply (drule lemma1_a) 107apply (auto simp add: derive_derive1_eq 108 simp del: reach_def derive_def derive1_def) 109done 110 111(* An other possible formulation of the above theorem based on 112 the equivalence x \<in> reach y r = y \<in> above x r *) 113lemma reach_above_lemma: 114 "(\<forall>i. reach i q \<subseteq> (reach i r \<union> {k})) = 115 (\<forall>x. x\<noteq>k --> (\<forall>i. i \<notin> above x r --> i \<notin> above x q))" 116by (auto simp add: trancl_converse) 117 118(* Lemma 2 *) 119lemma maximal_converse_image0: 120 "(z, i) \<in> r\<^sup>+ \<Longrightarrow> (\<forall>y. (y, z) \<in> r \<longrightarrow> (y,i) \<notin> r\<^sup>+) = ((r\<inverse>)``{z}={})" 121apply auto 122apply (frule_tac r = r in trancl_into_trancl2, auto) 123done 124 125lemma above_lemma_a: 126 "acyclic r ==> A i r\<noteq>{}-->(\<exists>j \<in> above i r. A j r = {})" 127apply (simp add: acyclic_eq_wf wf_eq_minimal) 128apply (drule_tac x = " ((r\<inverse>)\<^sup>+) ``{i}" in spec) 129apply auto 130apply (simp add: maximal_converse_image0 trancl_converse) 131done 132 133lemma above_lemma_b: 134 "acyclic r ==> above i r\<noteq>{}-->(\<exists>j \<in> above i r. above j r = {})" 135apply (drule above_lemma_a) 136apply (auto simp add: image0_trancl_iff_image0_r) 137done 138 139end 140