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