Quelle  Graph.thy

section ‹Address Graph›

theory Graph
imports Main
begin

text ‹
  theory introduces the graph to be marked as a relation next on
  (addresses). We assume that we have a special node nil (the
  address). We have a node root from which we start marking the graph.
  also assume that nil is not related by next to any node and any node is
  related by next to nil.
 ›

locale node = 
  fixes nil    :: "'node"
  fixes root   :: "'node"

locale graph = node +
  fixes "next" :: "('node × 'node) set"
  assumes next_not_nil_left: "(!! x . (nil, x) ∉ next)" 
  assumes next_not_nil_right: "(!! x . (x, nil) ∉ next)"
begin

text ‹
  lists of nodes we introduce two operations similar to
  hd and tl for getting the head and the tail of
  list. The new function head applied to a nonempty list
  the head of the list, and it reurns nil when
  to the empty list. The function tail returns the
  of the list when applied to a non-empty list, and
  returns the empty list otherwise.
 ›
  definition
    "head S ≡ (if S = [] then nil else (hd S))"
    
  definition
    "tail (S::'a list) ≡ (if S = [] then [] else (tl S))"

  lemma [simp]: "((nil, x) ∈ next) = False"
    by (simp add: next_not_nil_left)
  
  lemma [simp]: "((x, nil) ∈ next) = False"
    by (simp add: next_not_nil_right)


  theorem head_not_nil [simp]:
    "(head S ≠ nil) = (head S = hd S ∧ tail S = tl S ∧ hd S ≠ nil ∧ S ≠ [])"
    by (simp add: head_def tail_def)
  
  theorem nonempty_head [simp]:
    "head (x # S) = x"
    by (simp add: head_def)

  theorem nonempty_tail [simp]:
    "tail (x # S) = S"
    by (simp add: tail_def)

  definition (in graph)
    "reach x ≡ {y . (x, y) ∈ next^* ∧ y ≠ nil}"

  theorem (in graph) reach_nil [simp]: "reach nil = {}"
    apply (simp add: reach_def, safe)
    apply (drule rtrancl_induct)
    by auto

  theorem (in graph)  reach_next: "b ∈ reach a ==> (b, c) ∈ next ==> c ∈ reach a"
    apply (simp add: reach_def)
    by auto

  definition (in graph) 
    "path S mrk ≡ {x . (∃ s . s ∈ S ∧ (s, x) ∈ next O (next ∩ ((-mrk)×(-mrk)))^* )}"
  end
  
end