Theory Graph

section ‹Address Graph›

theory Graph
imports Main
begin

text ‹
This theory introduces the graph to be marked as a relation next on
nodes (addresses). We assume that we have a special node nil (the
null address). We have a node root from which we start marking the graph. 
We also assume that nil is not related by next to any node and any node is 
not 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 ‹
On lists of nodes we introduce two operations similar to
existing hd and tl for getting the head and the tail of
a list. The new function head applied to a nonempty list
returns the head of the list, and it reurns nil when
applied to the empty list. The function tail returns the
tail of the list when applied to a non-empty list, and
it 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