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