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