1 (* Title: HOL/Library/SCT_Implementation.thy |
|
2 ID: $Id$ |
|
3 Author: Alexander Krauss, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Implemtation of the SCT criterion *} |
|
7 |
|
8 theory Implementation |
|
9 imports Correctness |
|
10 begin |
|
11 |
|
12 fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool" |
|
13 where |
|
14 "edges_match ((n, e, m), (n',e',m')) = (m = n')" |
|
15 |
|
16 fun connect_edges :: |
|
17 "('n \<times> ('e::times) \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) |
|
18 \<Rightarrow> ('n \<times> 'e \<times> 'n)" |
|
19 where |
|
20 "connect_edges ((n,e,m), (n', e', m')) = (n, e * e', m')" |
|
21 |
|
22 lemma grcomp_code [code]: |
|
23 "grcomp (Graph G) (Graph H) = Graph (connect_edges ` { x \<in> G\<times>H. edges_match x })" |
|
24 by (rule graph_ext) (auto simp:graph_mult_def has_edge_def image_def) |
|
25 |
|
26 |
|
27 lemma mk_tcl_finite_terminates: |
|
28 fixes A :: "'a acg" |
|
29 assumes fA: "finite_acg A" |
|
30 shows "mk_tcl_dom (A, A)" |
|
31 proof - |
|
32 from fA have fin_tcl: "finite_acg (tcl A)" |
|
33 by (simp add:finite_tcl) |
|
34 |
|
35 hence "finite (dest_graph (tcl A))" |
|
36 unfolding finite_acg_def finite_graph_def .. |
|
37 |
|
38 let ?count = "\<lambda>G. card (dest_graph G)" |
|
39 let ?N = "?count (tcl A)" |
|
40 let ?m = "\<lambda>X. ?N - (?count X)" |
|
41 |
|
42 let ?P = "\<lambda>X. mk_tcl_dom (A, X)" |
|
43 |
|
44 { |
|
45 fix X |
|
46 assume "X \<le> tcl A" |
|
47 then |
|
48 have "mk_tcl_dom (A, X)" |
|
49 proof (induct X rule:measure_induct_rule[of ?m]) |
|
50 case (less X) |
|
51 show ?case |
|
52 proof (cases "X * A \<le> X") |
|
53 case True |
|
54 with mk_tcl.domintros show ?thesis by auto |
|
55 next |
|
56 case False |
|
57 then have l: "X < X + X * A" |
|
58 unfolding graph_less_def graph_leq_def graph_plus_def |
|
59 by auto |
|
60 |
|
61 from `X \<le> tcl A` |
|
62 have "X * A \<le> tcl A * A" by (simp add:mult_mono) |
|
63 also have "\<dots> \<le> A + tcl A * A" by simp |
|
64 also have "\<dots> = tcl A" by (simp add:tcl_unfold_right[symmetric]) |
|
65 finally have "X * A \<le> tcl A" . |
|
66 with `X \<le> tcl A` |
|
67 have "X + X * A \<le> tcl A + tcl A" |
|
68 by (rule add_mono) |
|
69 hence less_tcl: "X + X * A \<le> tcl A" by simp |
|
70 hence "X < tcl A" |
|
71 using l `X \<le> tcl A` by auto |
|
72 |
|
73 from less_tcl fin_tcl |
|
74 have "finite_acg (X + X * A)" by (rule finite_acg_subset) |
|
75 hence "finite (dest_graph (X + X * A))" |
|
76 unfolding finite_acg_def finite_graph_def .. |
|
77 |
|
78 hence X: "?count X < ?count (X + X * A)" |
|
79 using l[simplified graph_less_def graph_leq_def] |
|
80 by (rule psubset_card_mono) |
|
81 |
|
82 have "?count X < ?N" |
|
83 apply (rule psubset_card_mono) |
|
84 by fact (rule `X < tcl A`[simplified graph_less_def]) |
|
85 |
|
86 with X have "?m (X + X * A) < ?m X" by arith |
|
87 |
|
88 from less.hyps this less_tcl |
|
89 have "mk_tcl_dom (A, X + X * A)" . |
|
90 with mk_tcl.domintros show ?thesis . |
|
91 qed |
|
92 qed |
|
93 } |
|
94 from this less_tcl show ?thesis . |
|
95 qed |
|
96 |
|
97 |
|
98 lemma mk_tcl_finite_tcl: |
|
99 fixes A :: "'a acg" |
|
100 assumes fA: "finite_acg A" |
|
101 shows "mk_tcl A A = tcl A" |
|
102 using mk_tcl_finite_terminates[OF fA] |
|
103 by (simp only: tcl_def mk_tcl_correctness star_simulation) |
|
104 |
|
105 definition test_SCT :: "nat acg \<Rightarrow> bool" |
|
106 where |
|
107 "test_SCT \<A> = |
|
108 (let \<T> = mk_tcl \<A> \<A> |
|
109 in (\<forall>(n,G,m)\<in>dest_graph \<T>. |
|
110 n \<noteq> m \<or> G * G \<noteq> G \<or> |
|
111 (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))" |
|
112 |
|
113 |
|
114 lemma SCT'_exec: |
|
115 assumes fin: "finite_acg A" |
|
116 shows "SCT' A = test_SCT A" |
|
117 using mk_tcl_finite_tcl[OF fin] |
|
118 unfolding test_SCT_def Let_def |
|
119 unfolding SCT'_def no_bad_graphs_def has_edge_def |
|
120 by force |
|
121 |
|
122 code_modulename SML |
|
123 Implementation Graphs |
|
124 |
|
125 lemma [code]: |
|
126 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H" |
|
127 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H" |
|
128 unfolding graph_leq_def graph_less_def by rule+ |
|
129 |
|
130 lemma [code]: |
|
131 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)" |
|
132 unfolding graph_plus_def .. |
|
133 |
|
134 lemma [code]: |
|
135 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H" |
|
136 unfolding graph_mult_def .. |
|
137 |
|
138 |
|
139 |
|
140 lemma SCT'_empty: "SCT' (Graph {})" |
|
141 unfolding SCT'_def no_bad_graphs_def graph_zero_def[symmetric] |
|
142 tcl_zero |
|
143 by (simp add:in_grzero) |
|
144 |
|
145 |
|
146 |
|
147 subsection {* Witness checking *} |
|
148 |
|
149 definition test_SCT_witness :: "nat acg \<Rightarrow> nat acg \<Rightarrow> bool" |
|
150 where |
|
151 "test_SCT_witness A T = |
|
152 (A \<le> T \<and> A * T \<le> T \<and> |
|
153 (\<forall>(n,G,m)\<in>dest_graph T. |
|
154 n \<noteq> m \<or> G * G \<noteq> G \<or> |
|
155 (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))" |
|
156 |
|
157 lemma no_bad_graphs_ucl: |
|
158 assumes "A \<le> B" |
|
159 assumes "no_bad_graphs B" |
|
160 shows "no_bad_graphs A" |
|
161 using assms |
|
162 unfolding no_bad_graphs_def has_edge_def graph_leq_def |
|
163 by blast |
|
164 |
|
165 lemma SCT'_witness: |
|
166 assumes a: "test_SCT_witness A T" |
|
167 shows "SCT' A" |
|
168 proof - |
|
169 from a have "A \<le> T" "A * T \<le> T" by (auto simp:test_SCT_witness_def) |
|
170 hence "A + A * T \<le> T" |
|
171 by (subst add_idem[of T, symmetric], rule add_mono) |
|
172 with star3' have "tcl A \<le> T" unfolding tcl_def . |
|
173 moreover |
|
174 from a have "no_bad_graphs T" |
|
175 unfolding no_bad_graphs_def test_SCT_witness_def has_edge_def |
|
176 by auto |
|
177 ultimately |
|
178 show ?thesis |
|
179 unfolding SCT'_def |
|
180 by (rule no_bad_graphs_ucl) |
|
181 qed |
|
182 |
|
183 (* ML {* @{code test_SCT} *} *) |
|
184 |
|
185 end |
|