author | haftmann |
Fri, 24 Aug 2007 14:14:20 +0200 | |
changeset 24423 | ae9cd0e92423 |
parent 24348 | c708ea5b109a |
permissions | -rw-r--r-- |
22371 | 1 |
(* Title: HOL/Library/SCT_Implementation.thy |
2 |
ID: $Id$ |
|
3 |
Author: Alexander Krauss, TU Muenchen |
|
4 |
*) |
|
5 |
||
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
6 |
header {* Implemtation of the SCT criterion *} |
22665 | 7 |
|
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
8 |
theory SCT_Implementation |
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24348
diff
changeset
|
9 |
imports SCT_Definition SCT_Theorem |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
10 |
begin |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
11 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
12 |
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
|
13 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
14 |
"edges_match ((n, e, m), (n',e',m')) = (m = n')" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
15 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
16 |
fun connect_edges :: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
17 |
"('n \<times> ('e::times) \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
18 |
\<Rightarrow> ('n \<times> 'e \<times> 'n)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
19 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
20 |
"connect_edges ((n,e,m), (n', e', m')) = (n, e * e', m')" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
21 |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22665
diff
changeset
|
22 |
lemma grcomp_code [code]: |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
23 |
"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
|
24 |
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
|
25 |
|
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
26 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
27 |
lemma mk_tcl_finite_terminates: |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
28 |
fixes A :: "'a acg" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
29 |
assumes fA: "finite_acg A" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
30 |
shows "mk_tcl_dom (A, A)" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
31 |
proof - |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
32 |
from fA have fin_tcl: "finite_acg (tcl A)" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
33 |
by (simp add:finite_tcl) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
34 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
35 |
hence "finite (dest_graph (tcl A))" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
36 |
unfolding finite_acg_def finite_graph_def .. |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
37 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
38 |
let ?count = "\<lambda>G. card (dest_graph G)" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
39 |
let ?N = "?count (tcl A)" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
40 |
let ?m = "\<lambda>X. ?N - (?count X)" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
41 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
42 |
let ?P = "\<lambda>X. mk_tcl_dom (A, X)" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
43 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
44 |
{ |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
45 |
fix X |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
46 |
assume "X \<le> tcl A" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
47 |
then |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
48 |
have "mk_tcl_dom (A, X)" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
49 |
proof (induct X rule:measure_induct_rule[of ?m]) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
50 |
case (less X) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
51 |
show ?case |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
52 |
proof (cases "X * A \<le> X") |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
53 |
case True |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
54 |
with mk_tcl.domintros show ?thesis by auto |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
55 |
next |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
56 |
case False |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
57 |
then have l: "X < X + X * A" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
58 |
unfolding graph_less_def graph_leq_def graph_plus_def |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
59 |
by auto |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
60 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
61 |
from `X \<le> tcl A` |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
62 |
have "X * A \<le> tcl A * A" by (simp add:mult_mono) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
63 |
also have "\<dots> \<le> A + tcl A * A" by simp |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
64 |
also have "\<dots> = tcl A" by (simp add:tcl_unfold_right[symmetric]) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
65 |
finally have "X * A \<le> tcl A" . |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
66 |
with `X \<le> tcl A` |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
67 |
have "X + X * A \<le> tcl A + tcl A" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
68 |
by (rule add_mono) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
69 |
hence less_tcl: "X + X * A \<le> tcl A" by simp |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
70 |
hence "X < tcl A" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
71 |
using l `X \<le> tcl A` by auto |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
72 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
73 |
from less_tcl fin_tcl |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
74 |
have "finite_acg (X + X * A)" by (rule finite_acg_subset) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
75 |
hence "finite (dest_graph (X + X * A))" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
76 |
unfolding finite_acg_def finite_graph_def .. |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
77 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
78 |
hence X: "?count X < ?count (X + X * A)" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
79 |
using l[simplified graph_less_def graph_leq_def] |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
80 |
by (rule psubset_card_mono) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
81 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
82 |
have "?count X < ?N" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
83 |
apply (rule psubset_card_mono) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
84 |
by fact (rule `X < tcl A`[simplified graph_less_def]) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
85 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
86 |
with X have "?m (X + X * A) < ?m X" by arith |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
87 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
88 |
from less.hyps this less_tcl |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
89 |
have "mk_tcl_dom (A, X + X * A)" . |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
90 |
with mk_tcl.domintros show ?thesis . |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
91 |
qed |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
92 |
qed |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
93 |
} |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
94 |
from this less_tcl show ?thesis . |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
95 |
qed |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
96 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
97 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
98 |
lemma mk_tcl_finite_tcl: |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
99 |
fixes A :: "'a acg" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
100 |
assumes fA: "finite_acg A" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
101 |
shows "mk_tcl A A = tcl A" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
102 |
using mk_tcl_finite_terminates[OF fA] |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
103 |
by (simp only: tcl_def mk_tcl_correctness star_commute) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
104 |
|
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
105 |
definition test_SCT :: "nat acg \<Rightarrow> bool" |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
106 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
107 |
"test_SCT \<A> = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
108 |
(let \<T> = mk_tcl \<A> \<A> |
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
109 |
in (\<forall>(n,G,m)\<in>dest_graph \<T>. |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
110 |
n \<noteq> m \<or> G * G \<noteq> G \<or> |
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
111 |
(\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))" |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
112 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
113 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
114 |
lemma SCT'_exec: |
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
115 |
assumes fin: "finite_acg A" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
116 |
shows "SCT' A = test_SCT A" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
117 |
using mk_tcl_finite_tcl[OF fin] |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
118 |
unfolding test_SCT_def Let_def |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
119 |
unfolding SCT'_def no_bad_graphs_def has_edge_def |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
120 |
by force |
22359
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 |
code_modulename SML |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
123 |
Implementation Graphs |
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 |
lemma [code func]: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
126 |
"(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
|
127 |
"(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
|
128 |
unfolding graph_leq_def graph_less_def by rule+ |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
129 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
130 |
lemma [code func]: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
131 |
"(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
|
132 |
unfolding graph_plus_def .. |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
133 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
134 |
lemma [code func]: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
135 |
"(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
|
136 |
unfolding graph_mult_def .. |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
137 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
138 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
139 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
140 |
lemma SCT'_empty: "SCT' (Graph {})" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
141 |
unfolding SCT'_def no_bad_graphs_def graph_zero_def[symmetric] |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
142 |
tcl_zero |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
143 |
by (simp add:in_grzero) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
144 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
145 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
146 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
147 |
subsection {* Witness checking *} |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
148 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
149 |
|
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23394
diff
changeset
|
150 |
definition test_SCT_witness :: "nat acg \<Rightarrow> nat acg \<Rightarrow> bool" |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
151 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
152 |
"test_SCT_witness A T = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
153 |
(A \<le> T \<and> A * T \<le> T \<and> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
154 |
(\<forall>(n,G,m)\<in>dest_graph T. |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
155 |
n \<noteq> m \<or> G * G \<noteq> G \<or> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
156 |
(\<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
|
157 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
158 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
159 |
lemma no_bad_graphs_ucl: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
160 |
assumes "A \<le> B" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
161 |
assumes "no_bad_graphs B" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
162 |
shows "no_bad_graphs A" |
23394 | 163 |
using assms |
164 |
unfolding no_bad_graphs_def has_edge_def graph_leq_def |
|
165 |
by blast |
|
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
166 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
167 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
168 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
169 |
lemma SCT'_witness: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
170 |
assumes a: "test_SCT_witness A T" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
171 |
shows "SCT' A" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
172 |
proof - |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
173 |
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
|
174 |
hence "A + A * T \<le> T" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
175 |
by (subst add_idem[of T, symmetric], rule add_mono) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
176 |
with star3' have "tcl A \<le> T" unfolding tcl_def . |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
177 |
moreover |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
178 |
from a have "no_bad_graphs T" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
179 |
unfolding no_bad_graphs_def test_SCT_witness_def has_edge_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
180 |
by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
181 |
ultimately |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
182 |
show ?thesis |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
183 |
unfolding SCT'_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
184 |
by (rule no_bad_graphs_ucl) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
185 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
186 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
187 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
188 |
code_modulename SML |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
189 |
Graphs SCT |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
190 |
Kleene_Algebras SCT |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
191 |
SCT_Implementation SCT |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
192 |
|
24348 | 193 |
export_code test_SCT in SML |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
194 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
195 |
end |