Theory HOL-Statespace.DistinctTreeProver

(*  Title:      HOL/Statespace/DistinctTreeProver.thy
    Author:     Norbert Schirmer, TU Muenchen
*)

section ‹Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}›

theory DistinctTreeProver 
imports Main
begin

text ‹A state space manages a set of (abstract) names and assumes
that the names are distinct. The names are stored as parameters of a
locale and distinctness as an assumption. The most common request is
to proof distinctness of two given names. We maintain the names in a
balanced binary tree and formulate a predicate that all nodes in the
tree have distinct names. This setup leads to logarithmic certificates.
›

subsection ‹The Binary Tree›

datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip


text ‹The boolean flag in the node marks the content of the node as
deleted, without having to build a new tree. We prefer the boolean
flag to an option type, so that the ML-layer can still use the node
content to facilitate binary search in the tree. The ML code keeps the
nodes sorted using the term order. We do not have to push ordering to
the HOL level.›

subsection ‹Distinctness of Nodes›


primrec set_of :: "'a tree ⇒ 'a set"
where
  "set_of Tip = {}"
| "set_of (Node l x d r) = (if d then {} else {x}) ∪ set_of l ∪ set_of r"

primrec all_distinct :: "'a tree ⇒ bool"
where
  "all_distinct Tip = True"
| "all_distinct (Node l x d r) =
    ((d ∨ (x ∉ set_of l ∧ x ∉ set_of r)) ∧ 
      set_of l ∩ set_of r = {} ∧
      all_distinct l ∧ all_distinct r)"

text ‹Given a binary tree term‹t› for which 
const‹all_distinct› holds, given two different nodes contained in the tree,
we want to write a ML function that generates a logarithmic
certificate that the content of the nodes is distinct. We use the
following lemmas to achieve this.› 

lemma all_distinct_left: "all_distinct (Node l x b r) ⟹ all_distinct l"
  by simp

lemma all_distinct_right: "all_distinct (Node l x b r) ⟹ all_distinct r"
  by simp

lemma distinct_left: "all_distinct (Node l x False r) ⟹ y ∈ set_of l ⟹ x ≠ y"
  by auto

lemma distinct_right: "all_distinct (Node l x False r) ⟹ y ∈ set_of r ⟹ x ≠ y"
  by auto

lemma distinct_left_right:
    "all_distinct (Node l z b r) ⟹ x ∈ set_of l ⟹ y ∈ set_of r ⟹ x ≠ y"
  by auto

lemma in_set_root: "x ∈ set_of (Node l x False r)"
  by simp

lemma in_set_left: "y ∈ set_of l ⟹  y ∈ set_of (Node l x False r)"
  by simp

lemma in_set_right: "y ∈ set_of r ⟹  y ∈ set_of (Node l x False r)"
  by simp

lemma swap_neq: "x ≠ y ⟹ y ≠ x"
  by blast

lemma neq_to_eq_False: "x≠y ⟹ (x=y)≡False"
  by simp

subsection ‹Containment of Trees›

text ‹When deriving a state space from other ones, we create a new
name tree which contains all the names of the parent state spaces and
assume the predicate const‹all_distinct›. We then prove that the new
locale interprets all parent locales. Hence we have to show that the
new distinctness assumption on all names implies the distinctness
assumptions of the parent locales. This proof is implemented in ML. We
do this efficiently by defining a kind of containment check of trees
by ``subtraction''.  We subtract the parent tree from the new tree. If
this succeeds we know that const‹all_distinct› of the new tree
implies const‹all_distinct› of the parent tree.  The resulting
certificate is of the order term‹n * log(m)› where term‹n› is
the size of the (smaller) parent tree and term‹m› the size of the
(bigger) new tree.›


primrec delete :: "'a ⇒ 'a tree ⇒ 'a tree option"
where
  "delete x Tip = None"
| "delete x (Node l y d r) = (case delete x l of
                                Some l' ⇒
                                 (case delete x r of 
                                    Some r' ⇒ Some (Node l' y (d ∨ (x=y)) r')
                                  | None ⇒ Some (Node l' y (d ∨ (x=y)) r))
                               | None ⇒
                                  (case delete x r of 
                                     Some r' ⇒ Some (Node l y (d ∨ (x=y)) r')
                                   | None ⇒ if x=y ∧ ¬d then Some (Node l y True r)
                                             else None))"


lemma delete_Some_set_of: "delete x t = Some t' ⟹ set_of t' ⊆ set_of t"
proof (induct t arbitrary: t')
  case Tip thus ?case by simp
next
  case (Node l y d r)
  have del: "delete x (Node l y d r) = Some t'" by fact
  show ?case
  proof (cases "delete x l")
    case (Some l')
    note x_l_Some = this
    with Node.hyps
    have l'_l: "set_of l' ⊆ set_of l"
      by simp
    show ?thesis
    proof (cases "delete x r")
      case (Some r')
      with Node.hyps
      have "set_of r' ⊆ set_of r"
        by simp
      with l'_l Some x_l_Some del
      show ?thesis
        by (auto split: if_split_asm)
    next
      case None
      with l'_l Some x_l_Some del
      show ?thesis
        by (fastforce split: if_split_asm)
    qed
  next
    case None
    note x_l_None = this
    show ?thesis
    proof (cases "delete x r")
      case (Some r')
      with Node.hyps
      have "set_of r' ⊆ set_of r"
        by simp
      with Some x_l_None del
      show ?thesis
        by (fastforce split: if_split_asm)
    next
      case None
      with x_l_None del
      show ?thesis
        by (fastforce split: if_split_asm)
    qed
  qed
qed

lemma delete_Some_all_distinct:
  "delete x t = Some t' ⟹ all_distinct t ⟹ all_distinct t'"
proof (induct t arbitrary: t')
  case Tip thus ?case by simp
next
  case (Node l y d r)
  have del: "delete x (Node l y d r) = Some t'" by fact
  have "all_distinct (Node l y d r)" by fact
  then obtain
    dist_l: "all_distinct l" and
    dist_r: "all_distinct r" and
    d: "d ∨ (y ∉ set_of l ∧ y ∉ set_of r)" and
    dist_l_r: "set_of l ∩ set_of r = {}"
    by auto
  show ?case
  proof (cases "delete x l")
    case (Some l')
    note x_l_Some = this
    from Node.hyps (1) [OF Some dist_l]
    have dist_l': "all_distinct l'"
      by simp
    from delete_Some_set_of [OF x_l_Some]
    have l'_l: "set_of l' ⊆ set_of l".
    show ?thesis
    proof (cases "delete x r")
      case (Some r')
      from Node.hyps (2) [OF Some dist_r]
      have dist_r': "all_distinct r'"
        by simp
      from delete_Some_set_of [OF Some]
      have "set_of r' ⊆ set_of r".
      
      with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r
      show ?thesis
        by fastforce
    next
      case None
      with l'_l dist_l'  x_l_Some del d dist_l_r dist_r
      show ?thesis
        by fastforce
    qed
  next
    case None
    note x_l_None = this
    show ?thesis
    proof (cases "delete x r")
      case (Some r')
      with Node.hyps (2) [OF Some dist_r]
      have dist_r': "all_distinct r'"
        by simp
      from delete_Some_set_of [OF Some]
      have "set_of r' ⊆ set_of r".
      with Some dist_r' x_l_None del dist_l d dist_l_r
      show ?thesis
        by fastforce
    next
      case None
      with x_l_None del dist_l dist_r d dist_l_r
      show ?thesis
        by (fastforce split: if_split_asm)
    qed
  qed
qed

lemma delete_None_set_of_conv: "delete x t = None = (x ∉ set_of t)"
proof (induct t)
  case Tip thus ?case by simp
next
  case (Node l y d r)
  thus ?case
    by (auto split: option.splits)
qed

lemma delete_Some_x_set_of:
  "delete x t = Some t' ⟹ x ∈ set_of t ∧ x ∉ set_of t'"
proof (induct t arbitrary: t')
  case Tip thus ?case by simp
next
  case (Node l y d r)
  have del: "delete x (Node l y d r) = Some t'" by fact
  show ?case
  proof (cases "delete x l")
    case (Some l')
    note x_l_Some = this
    from Node.hyps (1) [OF Some]
    obtain x_l: "x ∈ set_of l" "x ∉ set_of l'"
      by simp
    show ?thesis
    proof (cases "delete x r")
      case (Some r')
      from Node.hyps (2) [OF Some]
      obtain x_r: "x ∈ set_of r" "x ∉ set_of r'"
        by simp
      from x_r x_l Some x_l_Some del 
      show ?thesis
        by (clarsimp split: if_split_asm)
    next
      case None
      then have "x ∉ set_of r"
        by (simp add: delete_None_set_of_conv)
      with x_l None x_l_Some del
      show ?thesis
        by (clarsimp split: if_split_asm)
    qed
  next
    case None
    note x_l_None = this
    then have x_notin_l: "x ∉ set_of l"
      by (simp add: delete_None_set_of_conv)
    show ?thesis
    proof (cases "delete x r")
      case (Some r')
      from Node.hyps (2) [OF Some]
      obtain x_r: "x ∈ set_of r" "x ∉ set_of r'"
        by simp
      from x_r x_notin_l Some x_l_None del 
      show ?thesis
        by (clarsimp split: if_split_asm)
    next
      case None
      then have "x ∉ set_of r"
        by (simp add: delete_None_set_of_conv)
      with None x_l_None x_notin_l del
      show ?thesis
        by (clarsimp split: if_split_asm)
    qed
  qed
qed


primrec subtract :: "'a tree ⇒ 'a tree ⇒ 'a tree option"
where
  "subtract Tip t = Some t"
| "subtract (Node l x b r) t =
     (case delete x t of
        Some t' ⇒ (case subtract l t' of 
                     Some t'' ⇒ subtract r t''
                    | None ⇒ None)
       | None ⇒ None)"

lemma subtract_Some_set_of_res: 
  "subtract t1 t2 = Some t ⟹ set_of t ⊆ set_of t2"
proof (induct t1 arbitrary: t2 t)
  case Tip thus ?case by simp
next
  case (Node l x b r)
  have sub: "subtract (Node l x b r) t2 = Some t" by fact
  show ?case
  proof (cases "delete x t2")
    case (Some t2')
    note del_x_Some = this
    from delete_Some_set_of [OF Some] 
    have t2'_t2: "set_of t2' ⊆ set_of t2" .
    show ?thesis
    proof (cases "subtract l t2'")
      case (Some t2'')
      note sub_l_Some = this
      from Node.hyps (1) [OF Some] 
      have t2''_t2': "set_of t2'' ⊆ set_of t2'" .
      show ?thesis
      proof (cases "subtract r t2''")
        case (Some t2''')
        from Node.hyps (2) [OF Some ] 
        have "set_of t2''' ⊆ set_of t2''" .
        with Some sub_l_Some del_x_Some sub t2''_t2' t2'_t2
        show ?thesis
          by simp
      next
        case None
        with del_x_Some sub_l_Some sub
        show ?thesis
          by simp
      qed
    next
      case None
      with del_x_Some sub 
      show ?thesis
        by simp
    qed
  next
    case None
    with sub show ?thesis by simp
  qed
qed

lemma subtract_Some_set_of: 
  "subtract t1 t2 = Some t ⟹ set_of t1 ⊆ set_of t2"
proof (induct t1 arbitrary: t2 t)
  case Tip thus ?case by simp
next
  case (Node l x d r)
  have sub: "subtract (Node l x d r) t2 = Some t" by fact
  show ?case
  proof (cases "delete x t2")
    case (Some t2')
    note del_x_Some = this
    from delete_Some_set_of [OF Some] 
    have t2'_t2: "set_of t2' ⊆ set_of t2" .
    from delete_None_set_of_conv [of x t2] Some
    have x_t2: "x ∈ set_of t2"
      by simp
    show ?thesis
    proof (cases "subtract l t2'")
      case (Some t2'')
      note sub_l_Some = this
      from Node.hyps (1) [OF Some] 
      have l_t2': "set_of l ⊆ set_of t2'" .
      from subtract_Some_set_of_res [OF Some]
      have t2''_t2': "set_of t2'' ⊆ set_of t2'" .
      show ?thesis
      proof (cases "subtract r t2''")
        case (Some t2''')
        from Node.hyps (2) [OF Some ] 
        have r_t2'': "set_of r ⊆ set_of t2''" .
        from Some sub_l_Some del_x_Some sub r_t2'' l_t2' t2'_t2 t2''_t2' x_t2
        show ?thesis
          by auto
      next
        case None
        with del_x_Some sub_l_Some sub
        show ?thesis
          by simp
      qed
    next
      case None
      with del_x_Some sub 
      show ?thesis
        by simp
    qed
  next
    case None
    with sub show ?thesis by simp
  qed
qed

lemma subtract_Some_all_distinct_res: 
  "subtract t1 t2 = Some t ⟹ all_distinct t2 ⟹ all_distinct t"
proof (induct t1 arbitrary: t2 t)
  case Tip thus ?case by simp
next
  case (Node l x d r)
  have sub: "subtract (Node l x d r) t2 = Some t" by fact
  have dist_t2: "all_distinct t2" by fact
  show ?case
  proof (cases "delete x t2")
    case (Some t2')
    note del_x_Some = this
    from delete_Some_all_distinct [OF Some dist_t2] 
    have dist_t2': "all_distinct t2'" .
    show ?thesis
    proof (cases "subtract l t2'")
      case (Some t2'')
      note sub_l_Some = this
      from Node.hyps (1) [OF Some dist_t2'] 
      have dist_t2'': "all_distinct t2''" .
      show ?thesis
      proof (cases "subtract r t2''")
        case (Some t2''')
        from Node.hyps (2) [OF Some dist_t2''] 
        have dist_t2''': "all_distinct t2'''" .
        from Some sub_l_Some del_x_Some sub 
             dist_t2'''
        show ?thesis
          by simp
      next
        case None
        with del_x_Some sub_l_Some sub
        show ?thesis
          by simp
      qed
    next
      case None
      with del_x_Some sub 
      show ?thesis
        by simp
    qed
  next
    case None
    with sub show ?thesis by simp
  qed
qed


lemma subtract_Some_dist_res: 
  "subtract t1 t2 = Some t ⟹ set_of t1 ∩ set_of t = {}"
proof (induct t1 arbitrary: t2 t)
  case Tip thus ?case by simp
next
  case (Node l x d r)
  have sub: "subtract (Node l x d r) t2 = Some t" by fact
  show ?case
  proof (cases "delete x t2")
    case (Some t2')
    note del_x_Some = this
    from delete_Some_x_set_of [OF Some]
    obtain x_t2: "x ∈ set_of t2" and x_not_t2': "x ∉ set_of t2'"
      by simp
    from delete_Some_set_of [OF Some]
    have t2'_t2: "set_of t2' ⊆ set_of t2" .
    show ?thesis
    proof (cases "subtract l t2'")
      case (Some t2'')
      note sub_l_Some = this
      from Node.hyps (1) [OF Some ] 
      have dist_l_t2'': "set_of l ∩ set_of t2'' = {}".
      from subtract_Some_set_of_res [OF Some]
      have t2''_t2': "set_of t2'' ⊆ set_of t2'" .
      show ?thesis
      proof (cases "subtract r t2''")
        case (Some t2''')
        from Node.hyps (2) [OF Some] 
        have dist_r_t2''': "set_of r ∩ set_of t2''' = {}" .
        from subtract_Some_set_of_res [OF Some]
        have t2'''_t2'': "set_of t2''' ⊆ set_of t2''".
        
        from Some sub_l_Some del_x_Some sub t2'''_t2'' dist_l_t2'' dist_r_t2'''
             t2''_t2' t2'_t2 x_not_t2'
        show ?thesis
          by auto
      next
        case None
        with del_x_Some sub_l_Some sub
        show ?thesis
          by simp
      qed
    next
      case None
      with del_x_Some sub 
      show ?thesis
        by simp
    qed
  next
    case None
    with sub show ?thesis by simp
  qed
qed
        
lemma subtract_Some_all_distinct:
  "subtract t1 t2 = Some t ⟹ all_distinct t2 ⟹ all_distinct t1"
proof (induct t1 arbitrary: t2 t)
  case Tip thus ?case by simp
next
  case (Node l x d r)
  have sub: "subtract (Node l x d r) t2 = Some t" by fact
  have dist_t2: "all_distinct t2" by fact
  show ?case
  proof (cases "delete x t2")
    case (Some t2')
    note del_x_Some = this
    from delete_Some_all_distinct [OF Some dist_t2 ] 
    have dist_t2': "all_distinct t2'" .
    from delete_Some_set_of [OF Some]
    have t2'_t2: "set_of t2' ⊆ set_of t2" .
    from delete_Some_x_set_of [OF Some]
    obtain x_t2: "x ∈ set_of t2" and x_not_t2': "x ∉ set_of t2'"
      by simp

    show ?thesis
    proof (cases "subtract l t2'")
      case (Some t2'')
      note sub_l_Some = this
      from Node.hyps (1) [OF Some dist_t2' ] 
      have dist_l: "all_distinct l" .
      from subtract_Some_all_distinct_res [OF Some dist_t2'] 
      have dist_t2'': "all_distinct t2''" .
      from subtract_Some_set_of [OF Some]
      have l_t2': "set_of l ⊆ set_of t2'" .
      from subtract_Some_set_of_res [OF Some]
      have t2''_t2': "set_of t2'' ⊆ set_of t2'" .
      from subtract_Some_dist_res [OF Some]
      have dist_l_t2'': "set_of l ∩ set_of t2'' = {}".
      show ?thesis
      proof (cases "subtract r t2''")
        case (Some t2''')
        from Node.hyps (2) [OF Some dist_t2''] 
        have dist_r: "all_distinct r" .
        from subtract_Some_set_of [OF Some]
        have r_t2'': "set_of r ⊆ set_of t2''" .
        from subtract_Some_dist_res [OF Some]
        have dist_r_t2''': "set_of r ∩ set_of t2''' = {}".

        from dist_l dist_r Some sub_l_Some del_x_Some r_t2'' l_t2' x_t2 x_not_t2' 
             t2''_t2' dist_l_t2'' dist_r_t2'''
        show ?thesis
          by auto
      next
        case None
        with del_x_Some sub_l_Some sub
        show ?thesis
          by simp
      qed
    next
      case None
      with del_x_Some sub 
      show ?thesis
        by simp
    qed
  next
    case None
    with sub show ?thesis by simp
  qed
qed


lemma delete_left:
  assumes dist: "all_distinct (Node l y d r)" 
  assumes del_l: "delete x l = Some l'"
  shows "delete x (Node l y d r) = Some (Node l' y d r)"
proof -
  from delete_Some_x_set_of [OF del_l]
  obtain x: "x ∈ set_of l"
    by simp
  with dist 
  have "delete x r = None"
    by (cases "delete x r") (auto dest:delete_Some_x_set_of)

  with x 
  show ?thesis
    using del_l dist
    by (auto split: option.splits)
qed

lemma delete_right:
  assumes dist: "all_distinct (Node l y d r)" 
  assumes del_r: "delete x r = Some r'"
  shows "delete x (Node l y d r) = Some (Node l y d r')"
proof -
  from delete_Some_x_set_of [OF del_r]
  obtain x: "x ∈ set_of r"
    by simp
  with dist 
  have "delete x l = None"
    by (cases "delete x l") (auto dest:delete_Some_x_set_of)

  with x 
  show ?thesis
    using del_r dist
    by (auto split: option.splits)
qed

lemma delete_root: 
  assumes dist: "all_distinct (Node l x False r)" 
  shows "delete x (Node l x False r) = Some (Node l x True r)"
proof -
  from dist have "delete x r = None"
    by (cases "delete x r") (auto dest:delete_Some_x_set_of)
  moreover
  from dist have "delete x l = None"
    by (cases "delete x l") (auto dest:delete_Some_x_set_of)
  ultimately show ?thesis
    using dist
       by (auto split: option.splits)
qed               

lemma subtract_Node:
 assumes del: "delete x t = Some t'"                                
 assumes sub_l: "subtract l t' = Some t''"
 assumes sub_r: "subtract r t'' = Some t'''"
 shows "subtract (Node l x False r) t = Some t'''"
using del sub_l sub_r
by simp

lemma subtract_Tip: "subtract Tip t = Some t"
  by simp
 
text ‹Now we have all the theorems in place that are needed for the
certificate generating ML functions.›

ML_file ‹distinct_tree_prover.ML›

end