src/HOL/Library/Graphs.thy

 (*  Title:      HOL/Library/Graphs.thy
     ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 *)
 
+header ""
+
 theory Graphs
 imports Main SCT_Misc Kleene_Algebras ExecutableSet
 begin
 
-
-section {* Basic types, Size Change Graphs *}
+subsection {* Basic types, Size Change Graphs *}
 
 datatype ('a, 'b) graph = 
   Graph "('a \<times> 'b \<times> 'a) set"
 
 fun dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set"

 ("_ \<turnstile> _ \<leadsto>\<^bsup>_\<^esup> _")
 where
   "has_edge G n e n' = ((n, e, n') \<in> dest_graph G)"
 
 
-
-section {* Graph composition *}
+subsection {* Graph composition *}
 
 fun grcomp :: "('n, 'e::times) graph \<Rightarrow> ('n, 'e) graph  \<Rightarrow> ('n, 'e) graph"
 where
   "grcomp (Graph G) (Graph H) = 
   Graph {(p,b,q) | p b q. 

 lemma in_grzero:
   "has_edge 0 p b q = False"
   by (simp add:graph_zero_def has_edge_def)
 
 
-
-subsection {* Multiplicative Structure *}
+subsubsection {* Multiplicative Structure *}
 
 instance graph :: (type, times) mult_zero
   graph_mult_def: "G * H == grcomp G H" 
 proof
   fix a :: "('a, 'b) graph"

   apply (auto simp: tcl_is_SUP in_SUP)
   apply (rule_tac x = "n - 1" in exI, auto)
   done
 
 
-
-section {* Infinite Paths *}
+subsection {* Infinite Paths *}
 
 types ('n, 'e) ipath = "('n \<times> 'e) sequence"
 
 definition has_ipath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) ipath \<Rightarrow> bool"
 where
   "has_ipath G p = 
   (\<forall>i. has_edge G (fst (p i)) (snd (p i)) (fst (p (Suc i))))"
 
 
-
-section {* Finite Paths *}
+subsection {* Finite Paths *}
 
 types ('n, 'e) fpath = "('n \<times> ('e \<times> 'n) list)"
 
 inductive2  has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool" 
   for G :: "('n, 'e) graph"

     by (auto simp:end_node_def nth.simps intro:has_fpath.intros split:nat.split)
   thus ?case using Suc by auto
 qed
 
 
-
-
-
-section {* Sub-Paths *}
-
+subsection {* Sub-Paths *}
 
 definition sub_path :: "('n, 'e) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ('n, 'e) fpath"
 ("(_\<langle>_,_\<rangle>)")
 where
   "p\<langle>i,j\<rangle> =