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