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