author | krauss |
Mon, 26 Feb 2007 21:34:16 +0100 | |
changeset 22359 | 94a794672c8b |
child 22371 | c9f5895972b0 |
permissions | -rw-r--r-- |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
1 |
theory SCT_Implementation |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
2 |
imports ExecutableSet SCT_Definition |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
3 |
begin |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
4 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
5 |
fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
6 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
7 |
"edges_match ((n, e, m), (n',e',m')) = (m = n')" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
8 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
9 |
fun connect_edges :: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
10 |
"('n \<times> ('e::times) \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
11 |
\<Rightarrow> ('n \<times> 'e \<times> 'n)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
12 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
13 |
"connect_edges ((n,e,m), (n', e', m')) = (n, e * e', m')" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
14 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
15 |
lemma grcomp_code[code]: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
16 |
"grcomp (Graph G) (Graph H) = Graph (connect_edges ` { x \<in> G\<times>H. edges_match x })" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
17 |
by (rule graph_ext) (auto simp:graph_mult_def has_edge_def image_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
18 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
19 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
20 |
definition test_SCT :: "acg \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
21 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
22 |
"test_SCT \<A> = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
23 |
(let \<T> = mk_tcl \<A> \<A> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
24 |
in (\<T> \<noteq> 0 \<and> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
25 |
(\<forall>(n,G,m)\<in>dest_graph \<T>. |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
26 |
n \<noteq> m \<or> G * G \<noteq> G \<or> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
27 |
(\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS))))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
28 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
29 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
30 |
lemma SCT'_exec: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
31 |
assumes a: "test_SCT \<A>" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
32 |
shows "SCT' \<A>" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
33 |
proof - |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
34 |
from mk_tcl_correctness2 a |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
35 |
have "mk_tcl \<A> \<A> = tcl \<A>" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
36 |
unfolding test_SCT_def Let_def by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
37 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
38 |
with a |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
39 |
show ?thesis |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
40 |
unfolding SCT'_def no_bad_graphs_def test_SCT_def Let_def has_edge_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
41 |
by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
42 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
43 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
44 |
code_modulename SML |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
45 |
Implementation Graphs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
46 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
47 |
lemma [code func]: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
48 |
"(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
49 |
"(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
50 |
unfolding graph_leq_def graph_less_def by rule+ |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
51 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
52 |
lemma [code func]: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
53 |
"(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
54 |
unfolding graph_plus_def .. |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
55 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
56 |
lemma [code func]: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
57 |
"(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
58 |
unfolding graph_mult_def .. |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
59 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
60 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
61 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
62 |
lemma SCT'_empty: "SCT' (Graph {})" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
63 |
unfolding SCT'_def no_bad_graphs_def graph_zero_def[symmetric] |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
64 |
tcl_zero |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
65 |
by (simp add:in_grzero) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
66 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
67 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
68 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
69 |
subsection {* Witness checking *} |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
70 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
71 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
72 |
definition test_SCT_witness :: "acg \<Rightarrow> acg \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
73 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
74 |
"test_SCT_witness A T = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
75 |
(A \<le> T \<and> A * T \<le> T \<and> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
76 |
(\<forall>(n,G,m)\<in>dest_graph T. |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
77 |
n \<noteq> m \<or> G * G \<noteq> G \<or> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
78 |
(\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
79 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
80 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
81 |
lemma no_bad_graphs_ucl: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
82 |
assumes "A \<le> B" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
83 |
assumes "no_bad_graphs B" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
84 |
shows "no_bad_graphs A" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
85 |
using prems |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
86 |
unfolding no_bad_graphs_def has_edge_def graph_leq_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
87 |
by blast |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
88 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
89 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
90 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
91 |
lemma SCT'_witness: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
92 |
assumes a: "test_SCT_witness A T" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
93 |
shows "SCT' A" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
94 |
proof - |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
95 |
from a have "A \<le> T" "A * T \<le> T" by (auto simp:test_SCT_witness_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
96 |
hence "A + A * T \<le> T" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
97 |
by (subst add_idem[of T, symmetric], rule add_mono) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
98 |
with star3' have "tcl A \<le> T" unfolding tcl_def . |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
99 |
moreover |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
100 |
from a have "no_bad_graphs T" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
101 |
unfolding no_bad_graphs_def test_SCT_witness_def has_edge_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
102 |
by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
103 |
ultimately |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
104 |
show ?thesis |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
105 |
unfolding SCT'_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
106 |
by (rule no_bad_graphs_ucl) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
107 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
108 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
109 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
110 |
code_modulename SML |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
111 |
Graphs SCT |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
112 |
Kleene_Algebras SCT |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
113 |
SCT_Implementation SCT |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
114 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
115 |
code_gen test_SCT (SML -) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
116 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
117 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
118 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
119 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
120 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
121 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
122 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
123 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
124 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
125 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
126 |