# HG changeset patch
# User krauss
# Date 1172657532 -3600
# Node ID c9f5895972b06d06e3e4102c99bf438bbba6bbc0
# Parent  44679bbcf43be123c7e930537f6ebe00e9120802
added headers

diff -r 44679bbcf43b -r c9f5895972b0 src/HOL/Library/Graphs.thy
--- 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
diff -r 44679bbcf43b -r c9f5895972b0 src/HOL/Library/Kleene_Algebras.thy
--- 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
diff -r 44679bbcf43b -r c9f5895972b0 src/HOL/Library/SCT_Definition.thy
--- 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
diff -r 44679bbcf43b -r c9f5895972b0 src/HOL/Library/SCT_Examples.thy
--- 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
diff -r 44679bbcf43b -r c9f5895972b0 src/HOL/Library/SCT_Implementation.thy
--- 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
diff -r 44679bbcf43b -r c9f5895972b0 src/HOL/Library/SCT_Interpretation.thy
--- 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
diff -r 44679bbcf43b -r c9f5895972b0 src/HOL/Library/SCT_Misc.thy
--- 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
diff -r 44679bbcf43b -r c9f5895972b0 src/HOL/Library/SCT_Theorem.thy
--- 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
-
-
-
-
-
-
-
diff -r 44679bbcf43b -r c9f5895972b0 src/HOL/Library/Size_Change_Termination.thy
--- 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
diff -r 44679bbcf43b -r c9f5895972b0 src/HOL/Library/size_change_termination.ML
--- 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