author | berghofe |
Wed, 11 Jul 2007 11:24:36 +0200 | |
changeset 23751 | a7c7edf2c5ad |
parent 23416 | b73a6b72f706 |
permissions | -rw-r--r-- |
22371 | 1 |
(* Title: HOL/Library/SCT_Definition.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:
23374
diff
changeset
|
6 |
header {* The Size-Change Principle (Definition) *} |
22665 | 7 |
|
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
8 |
theory SCT_Definition |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
9 |
imports Graphs Infinite_Set |
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 |
|
22665 | 12 |
subsection {* Size-Change Graphs *} |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
13 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
14 |
datatype sedge = |
22665 | 15 |
LESS ("\<down>") |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
16 |
| LEQ ("\<Down>") |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
17 |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22665
diff
changeset
|
18 |
instance sedge :: one |
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22665
diff
changeset
|
19 |
one_sedge_def: "1 \<equiv> \<Down>" .. |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
20 |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22665
diff
changeset
|
21 |
instance sedge :: times |
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22665
diff
changeset
|
22 |
mult_sedge_def:" a * b \<equiv> if a = \<down> then \<down> else b" .. |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
23 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
24 |
instance sedge :: comm_monoid_mult |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
25 |
proof |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
26 |
fix a b c :: sedge |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
27 |
show "a * b * c = a * (b * c)" by (simp add:mult_sedge_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
28 |
show "1 * a = a" by (simp add:mult_sedge_def one_sedge_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
29 |
show "a * b = b * a" unfolding mult_sedge_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
30 |
by (cases a, simp) (cases b, auto) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
31 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
32 |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22665
diff
changeset
|
33 |
lemma sedge_UNIV: |
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22665
diff
changeset
|
34 |
"UNIV = { LESS, LEQ }" |
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
35 |
proof (intro equalityI subsetI) |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
36 |
fix x show "x \<in> { LESS, LEQ }" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
37 |
by (cases x) auto |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
38 |
qed auto |
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22665
diff
changeset
|
39 |
|
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
40 |
instance sedge :: finite |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
41 |
proof |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
42 |
show "finite (UNIV::sedge set)" |
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22665
diff
changeset
|
43 |
by (simp add: sedge_UNIV) |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
44 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
45 |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22665
diff
changeset
|
46 |
lemmas [code func] = sedge_UNIV |
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22665
diff
changeset
|
47 |
|
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
48 |
|
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
49 |
types 'a scg = "('a, sedge) graph" |
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
50 |
types 'a acg = "('a, 'a scg) graph" |
22359
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 |
|
22665 | 53 |
subsection {* Size-Change Termination *} |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
54 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
55 |
abbreviation (input) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
56 |
"desc P Q == ((\<exists>n.\<forall>i\<ge>n. P i) \<and> (\<exists>\<^sub>\<infinity>i. Q i))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
57 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
58 |
abbreviation (input) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
59 |
"dsc G i j \<equiv> has_edge G i LESS j" |
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 |
abbreviation (input) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
62 |
"eq G i j \<equiv> has_edge G i LEQ j" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
63 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
64 |
abbreviation |
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
65 |
eql :: "'a scg \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
66 |
("_ \<turnstile> _ \<leadsto> _") |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
67 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
68 |
"eql G i j \<equiv> has_edge G i LESS j \<or> has_edge G i LEQ j" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
69 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
70 |
|
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
71 |
abbreviation (input) descat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool" |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
72 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
73 |
"descat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
74 |
|
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
75 |
abbreviation (input) eqat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool" |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
76 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
77 |
"eqat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
78 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
79 |
|
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
80 |
abbreviation (input) eqlat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool" |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
81 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
82 |
"eqlat p \<theta> i \<equiv> (has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
83 |
\<or> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i)))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
84 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
85 |
|
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
86 |
definition is_desc_thread :: "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> bool" |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
87 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
88 |
"is_desc_thread \<theta> p = ((\<exists>n.\<forall>i\<ge>n. eqlat p \<theta> i) \<and> (\<exists>\<^sub>\<infinity>i. descat p \<theta> i))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
89 |
|
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
90 |
definition SCT :: "'a acg \<Rightarrow> bool" |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
91 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
92 |
"SCT \<A> = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
93 |
(\<forall>p. has_ipath \<A> p \<longrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> p))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
94 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
95 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
96 |
|
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
97 |
definition no_bad_graphs :: "'a acg \<Rightarrow> bool" |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
98 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
99 |
"no_bad_graphs A = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
100 |
(\<forall>n G. has_edge A n G n \<and> G * G = G |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
101 |
\<longrightarrow> (\<exists>p. has_edge G p LESS p))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
102 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
103 |
|
23416
b73a6b72f706
generalized proofs so that call graphs can have any node type.
krauss
parents:
23374
diff
changeset
|
104 |
definition SCT' :: "'a acg \<Rightarrow> bool" |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
105 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
106 |
"SCT' A = no_bad_graphs (tcl A)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
107 |
|
22665 | 108 |
end |