10782
|
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 |
Addsimps [derive_def, derive1_def, symcl_def, A_def, R_def,
|
|
10 |
above_def, reach_def, reverse_def, neighbors_def];
|
|
11 |
|
|
12 |
(*All vertex sets are finite \\<dots>*)
|
|
13 |
AddIffs [[subset_UNIV, finite_vertex_univ] MRS finite_subset];
|
|
14 |
|
|
15 |
(* and relatons over vertex are finite too *)
|
|
16 |
AddIffs [[subset_UNIV, [finite_vertex_univ, finite_vertex_univ]
|
|
17 |
MRS finite_Prod_UNIV] MRS finite_subset];
|
|
18 |
|
|
19 |
|
|
20 |
(* The equalities (above i r = {}) = (A i r = {})
|
|
21 |
and (reach i r = {}) = (R i r) rely on the following theorem *)
|
|
22 |
|
10797
|
23 |
Goal "((r^+)```{i} = {}) = (r```{i} = {})";
|
10782
|
24 |
by Auto_tac;
|
|
25 |
by (etac trancl_induct 1);
|
|
26 |
by Auto_tac;
|
|
27 |
qed "image0_trancl_iff_image0_r";
|
|
28 |
|
|
29 |
(* Another form usefull in some situation *)
|
10797
|
30 |
Goal "(r```{i}={}) = (ALL x. ((i,x):r^+) = False)";
|
10782
|
31 |
by Auto_tac;
|
|
32 |
by (dtac (image0_trancl_iff_image0_r RS ssubst) 1);
|
|
33 |
by Auto_tac;
|
|
34 |
qed "image0_r_iff_image0_trancl";
|
|
35 |
|
|
36 |
|
|
37 |
(* In finite universe acyclic coincides with wf *)
|
|
38 |
Goal
|
|
39 |
"!!r::(vertex*vertex)set. acyclic r = wf r";
|
|
40 |
by (auto_tac (claset(), simpset() addsimps [wf_iff_acyclic_if_finite]));
|
|
41 |
qed "acyclic_eq_wf";
|
|
42 |
|
|
43 |
(* derive and derive1 are equivalent *)
|
|
44 |
Goal "derive i r q = derive1 i r q";
|
|
45 |
by Auto_tac;
|
|
46 |
qed "derive_derive1_eq";
|
|
47 |
|
|
48 |
(* Lemma 1 *)
|
|
49 |
Goalw [reach_def]
|
|
50 |
"[| x:reach i q; derive1 k r q |] ==> x~=k --> x:reach i r";
|
|
51 |
by (etac ImageE 1);
|
|
52 |
by (etac trancl_induct 1);
|
|
53 |
by (case_tac "i=k" 1);
|
|
54 |
by (auto_tac (claset() addIs [r_into_trancl], simpset()));
|
|
55 |
by (dres_inst_tac [("x", "y")] spec 1);
|
|
56 |
by (rotate_tac ~1 1);
|
|
57 |
by (dres_inst_tac [("x", "z")] spec 1);
|
|
58 |
by (auto_tac (claset() addDs [r_into_trancl] addIs [trancl_trans], simpset()));
|
|
59 |
qed "lemma1_a";
|
|
60 |
|
|
61 |
Goal "ALL k r q. derive k r q -->(reach i q <= (reach i r Un {k}))";
|
|
62 |
by (REPEAT(rtac allI 1));
|
|
63 |
by (rtac impI 1);
|
|
64 |
by (rtac subsetI 1 THEN dtac lemma1_a 1);
|
|
65 |
by (auto_tac (claset(), simpset() addsimps [derive_derive1_eq]
|
|
66 |
delsimps [reach_def, derive_def, derive1_def]));
|
|
67 |
qed "reach_lemma";
|
|
68 |
|
|
69 |
(* An other possible formulation of the above theorem based on
|
|
70 |
the equivalence x:reach y r = y:above x r *)
|
|
71 |
Goal
|
|
72 |
"(ALL i. reach i q <= (reach i r Un {k})) =\
|
|
73 |
\ (ALL x. x~=k --> (ALL i. i~:above x r --> i~:above x q))";
|
|
74 |
by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
|
|
75 |
qed "reach_above_lemma";
|
|
76 |
|
|
77 |
(* Lemma 2 *)
|
|
78 |
Goal
|
10797
|
79 |
"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)```{z}={})";
|
10782
|
80 |
by Auto_tac;
|
|
81 |
by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1);
|
|
82 |
by Auto_tac;
|
|
83 |
qed "maximal_converse_image0";
|
|
84 |
|
|
85 |
Goal
|
|
86 |
"acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})";
|
|
87 |
by (full_simp_tac (simpset()
|
|
88 |
addsimps [acyclic_eq_wf, wf_eq_minimal]) 1);
|
10797
|
89 |
by (dres_inst_tac [("x", "((r^-1)^+)```{i}")] spec 1);
|
10782
|
90 |
by Auto_tac;
|
|
91 |
by (rotate_tac ~1 1);
|
|
92 |
by (asm_full_simp_tac (simpset()
|
|
93 |
addsimps [maximal_converse_image0, trancl_converse]) 1);
|
|
94 |
qed "above_lemma_a";
|
|
95 |
|
|
96 |
|
|
97 |
Goal
|
|
98 |
"acyclic r ==> above i r~={}-->(EX j:above i r. above j r = {})";
|
|
99 |
by (dtac above_lemma_a 1);
|
|
100 |
by (auto_tac (claset(), simpset()
|
|
101 |
addsimps [image0_trancl_iff_image0_r]));
|
|
102 |
qed "above_lemma_b";
|
|
103 |
|
|
104 |
|
|
105 |
|
|
106 |
|
|
107 |
|
|
108 |
|
|
109 |
|
|
110 |
|
|
111 |
|
|
112 |
|
|
113 |
|
|
114 |
|
|
115 |
|
|
116 |
|