--- a/src/HOL/Library/Graphs.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/Graphs.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,3 +1,8 @@
+(* Title: HOL/Library/Graphs.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory Graphs
imports Main SCT_Misc Kleene_Algebras ExecutableSet
begin
--- a/src/HOL/Library/Kleene_Algebras.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/Kleene_Algebras.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,3 +1,8 @@
+(* Title: HOL/Library/Kleene_Algebras.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory Kleene_Algebras
imports Main
begin
--- a/src/HOL/Library/SCT_Definition.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/SCT_Definition.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,3 +1,8 @@
+(* Title: HOL/Library/SCT_Definition.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory SCT_Definition
imports Graphs Infinite_Set
begin
--- a/src/HOL/Library/SCT_Examples.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/SCT_Examples.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,9 +1,12 @@
+(* Title: HOL/Library/SCT_Examples.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory SCT_Examples
imports Size_Change_Termination
begin
-
-
function f :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
"f n 0 = n"
@@ -23,7 +26,6 @@
apply (rule SCT'_exec)
by eval (* Evaluate to true *)
-
function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
"p m n r = (if r>0 then p m (r - 1) n else
@@ -61,7 +63,6 @@
apply (rule SCT'_exec)
by eval
-
function (sequential)
bar :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
@@ -79,5 +80,4 @@
apply (simp add:finite_acg_ins finite_acg_empty)
by (rule SCT'_empty)
-
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/SCT_Implementation.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/SCT_Implementation.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,3 +1,8 @@
+(* Title: HOL/Library/SCT_Implementation.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory SCT_Implementation
imports ExecutableSet SCT_Definition
begin
--- a/src/HOL/Library/SCT_Interpretation.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/SCT_Interpretation.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,8 +1,12 @@
+(* Title: HOL/Library/SCT_Interpretation.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory SCT_Interpretation
imports Main SCT_Misc SCT_Definition
begin
-
definition
"idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))"
@@ -409,5 +413,4 @@
thus "acc R x" ..
qed
-
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/SCT_Misc.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/SCT_Misc.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,8 +1,12 @@
+(* Title: HOL/Library/SCT_Misc.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory SCT_Misc
imports Main
begin
-
subsection {* Searching in lists *}
fun index_of :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
@@ -18,8 +22,6 @@
"(x \<in> set l) = (index_of l x < length l)"
by (induct l) auto
-
-
subsection {* Some reasoning tools *}
lemma inc_induct[consumes 1]:
@@ -56,7 +58,6 @@
thus "P i" by (rule step)
qed
-
lemma three_cases:
assumes "a1 \<Longrightarrow> thesis"
assumes "a2 \<Longrightarrow> thesis"
@@ -66,7 +67,6 @@
using prems
by auto
-
section {* Sequences *}
types
@@ -101,7 +101,6 @@
show ?case by auto
qed auto
-
lemma increasing_bij:
assumes [simp]: "increasing s"
shows "(s i < s j) = (i < j)"
@@ -116,9 +115,6 @@
qed
qed (simp add:increasing_strict)
-
-
-
subsection {* Sections induced by an increasing sequence *}
abbreviation
@@ -127,7 +123,6 @@
definition
"section_of s n = (LEAST i. n < s (Suc i))"
-
lemma section_help:
assumes [intro, simp]: "increasing s"
shows "\<exists>i. n < s (Suc i)"
@@ -143,7 +138,6 @@
unfolding section_of_def
by (rule LeastI_ex) (rule section_help)
-
lemma section_of1:
assumes [simp, intro]: "increasing s"
assumes "s i \<le> n"
@@ -193,7 +187,6 @@
ultimately show ?thesis by simp
qed
qed
-
lemma in_section_of:
assumes [simp, intro]: "increasing s"
@@ -202,5 +195,4 @@
using prems
by (auto intro:section_of1 section_of2)
-
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/SCT_Theorem.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/SCT_Theorem.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,11 +1,14 @@
+(* Title: HOL/Library/SCT_Theorem.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory SCT_Theorem
imports Main Ramsey SCT_Misc SCT_Definition
begin
-
section {* The size change criterion SCT *}
-
definition is_thread :: "nat \<Rightarrow> nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> bool"
where
"is_thread n \<theta> p = (\<forall>i\<ge>n. eqlat p \<theta> i)"
@@ -30,8 +33,6 @@
"has_desc_fth p i j n m =
(\<exists>\<theta>. is_desc_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
-
-
section {* Bounded graphs and threads *}
definition
@@ -48,14 +49,12 @@
definition (* = finite (range \<theta>) *)
"bounded_th (P::nat) n \<theta> = (\<forall>i>n. \<theta> i < P)"
-
definition
"finite_scg (G::scg) = (\<exists>P. bounded_scg P G)"
definition
"finite_acg (A::acg) = (\<exists>P. bounded_acg P A)"
-
lemma "finite (insert x A) = finite A"
by simp
@@ -82,7 +81,6 @@
by (auto intro: finite_cartesian_product finite_atLeastAtMost)
qed
next
-
assume "finite G"
thus "finite_scg (Graph G)"
proof induct
@@ -110,19 +108,15 @@
qed
qed
-
lemma finite_acg_empty:
"finite_acg (Graph {})"
unfolding finite_acg_def bounded_acg_def has_edge_def
by auto
-
-
lemma bounded_scg_up: "bounded_scg P G \<Longrightarrow> P \<le> Q \<Longrightarrow> bounded_scg Q G"
unfolding bounded_scg_def
by force
-
lemma bounded_up: "bounded_acg P G \<Longrightarrow> P \<le> Q \<Longrightarrow> bounded_acg Q G"
unfolding bounded_acg_def
apply auto
@@ -1401,16 +1395,4 @@
by simp
qed
-
-
-
-
-
end
-
-
-
-
-
-
-
--- a/src/HOL/Library/Size_Change_Termination.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/Size_Change_Termination.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,12 +1,13 @@
+(* Title: HOL/Library/Size_Change_Termination.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory Size_Change_Termination
imports SCT_Theorem SCT_Interpretation SCT_Implementation
uses "size_change_termination.ML"
begin
-use "size_change_termination.ML"
-
-
-
section {* Simplifier setup *}
text {* This is needed to run the SCT algorithm in the simplifier: *}
@@ -99,6 +100,4 @@
lemmas sctTest_congs =
if_weak_cong let_weak_cong setbcomp_cong
-
-
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/size_change_termination.ML Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/size_change_termination.ML Wed Feb 28 11:12:12 2007 +0100
@@ -1,3 +1,7 @@
+(* Title: HOL/Library/size_change_termination.ML
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
structure SCT = struct