Quelle  Tree.thy

section ‹Trees›

theory Tree imports Main begin

text ‹Sometimes it is nice to think of @{typ bool}s as directions in a binary tree›
hide_const (open) Left Right
type_synonym dir = bool
definition Left :: bool where "Left = True"
definition Right :: bool where "Right = False"
declare Left_def [simp]
declare Right_def [simp]

datatype tree =
  Leaf
| Branching (ltree: tree) (rtree: tree) 


subsection ‹Sizes›

fun treesize :: "tree ==> nat" where
  "treesize Leaf = 0"
| "treesize (Branching l r) = 1 + treesize l + treesize r"

lemma treesize_Leaf:
  assumes "treesize T = 0"
  shows "T = Leaf"
  using assms by (cases T) auto

lemma treesize_Branching:
  assumes "treesize T = Suc n"
  shows "∃l r. T = Branching l r" 
  using assms by (cases T) auto


subsection ‹Paths›

fun path :: "dir list ==> tree ==> bool" where
  "path [] T ⟷ True"
| "path (d#ds) (Branching T1 T2) ⟷ (if d then path ds T1 else path ds T2)"
| "path _ _ ⟷ False"

lemma path_inv_Leaf: "path p Leaf ⟷ p = []"
  by (induction p)  auto

lemma path_inv_Cons: "path (a#ds) T ⟶ (∃l r. T=Branching l r)"
  by  (cases T) (auto simp add: path_inv_Leaf)


lemma path_inv_Branching_Left: "path (Left#p) (Branching l r) ⟷ path p l"
  using Left_def Right_def path.cases by (induction p) auto

lemma path_inv_Branching_Right: "path (Right#p) (Branching l r) ⟷ path p r"
using Left_def Right_def path.cases by (induction p)  auto


lemma path_inv_Branching: 
  "path p (Branching l r) ⟷ (p=[] ∨ (∃a p'. p=a#p'∧ (a ⟶ path p' l) ∧ (¬a ⟶ path p' r)))" (is "?L ⟷ ?R")
proof
  assume ?L then show ?R by (induction p) auto
next
  assume r: ?R
  then show ?L
    proof
      assume "p = []" then show ?L by auto
    next
      assume "∃a p'. p=a#p'∧ (a ⟶ path p' l) ∧ (¬a ⟶ path p' r)"
      then obtain a p' where "p=a#p'∧ (a ⟶ path p' l) ∧ (¬a ⟶ path p' r)" by auto
      then show ?L by (cases a) auto
    qed
qed

lemma path_prefix: 
  assumes "path (ds1@ds2) T"
  shows "path ds1 T"
using assms proof (induction ds1 arbitrary: T)
  case (Cons a ds1)
  then have "∃l r. T = Branching l r" using path_inv_Leaf by (cases T) auto
  then obtain l r where p_lr: "T = Branching l r" by auto
  show ?case
    proof (cases a)
      assume atrue: "a"
      then have "path ((ds1) @ ds2) l" using p_lr Cons(2) path_inv_Branching by auto
      then have "path ds1 l" using Cons(1) by auto
      then show "path (a # ds1) T" using p_lr atrue by auto
    next
      assume afalse: "¬a"
      then have "path ((ds1) @ ds2) r" using p_lr Cons(2) path_inv_Branching by auto
      then have "path ds1 r" using Cons(1) by auto
      then show "path (a # ds1) T" using p_lr afalse by auto
    qed
next
  case (Nil) then show ?case  by auto
qed


subsection ‹Branches›

fun branch :: "dir list ==> tree ==> bool" where
  "branch [] Leaf ⟷ True"    
| "branch (d # ds) (Branching l r) ⟷ (if d then branch ds l else branch ds r)"
| "branch _ _ ⟷ False"

lemma has_branch: "∃b. branch b T"
proof (induction T)
  case (Leaf) 
  have "branch [] Leaf" by auto
  then show ?case by blast
next
  case (Branching T₁ T₂)
  then obtain b where "branch b T₁" by auto
  then have "branch (Left#b) (Branching T₁ T₂)"  by auto
  then show ?case by blast
qed

lemma branch_inv_Leaf: "branch b Leaf ⟷ b = []"
by (cases b) auto

lemma branch_inv_Branching_Left:  
  "branch (Left#b) (Branching l r) ⟷ branch b l"
by auto

lemma branch_inv_Branching_Right: 
  "branch (Right#b) (Branching l r) ⟷ branch b r"
by auto

lemma branch_inv_Branching: 
  "branch b (Branching l r) ⟷
     (∃a b'. b=a#b'∧ (a ⟶ branch b' l) ∧ (¬a ⟶ branch b' r))"
by (induction b) auto

lemma branch_inv_Leaf2:
  "T = Leaf ⟷ (∀b. branch b T ⟶ b = [])"
proof -
  {
    assume "T=Leaf"
    then have "∀b. branch b T ⟶ b = []" using branch_inv_Leaf by auto
  }
  moreover 
  {
    assume "∀b. branch b T ⟶ b = []"
    then have "∀b. branch b T ⟶ ¬(∃a b'. b = a # b')" by auto
    then have "∀b. branch b T ⟶ ¬(∃l r. branch b (Branching l r))" 
      using branch_inv_Branching by auto
    then have "T=Leaf" using has_branch[of T] by (metis branch.elims(2))
  }
  ultimately show "T = Leaf ⟷ (∀b. branch b T ⟶ b = [])" by auto
qed

lemma branch_is_path: 
  assumes"branch ds T"
  shows "path ds T"
using assms proof (induction T arbitrary: ds)
  case Leaf
  then have "ds = []" using branch_inv_Leaf by auto
  then show ?case  by auto
next
  case (Branching T₁ T₂) 
  then obtain a b where ds_p: "ds = a # b ∧ (a ⟶ branch b T₁) ∧ (¬ a ⟶ branch b T₂)" using branch_inv_Branching[of ds] by blast
  then have "(a ⟶ path b T₁) ∧ (¬a ⟶ path b T₂)" using Branching by auto
  then show "?case" using ds_p by (cases a) auto
qed

lemma Branching_Leaf_Leaf_Tree:
  assumes "T = Branching T1 T2"
  shows "(∃B. branch (B@[True]) T ∧ branch (B@[False]) T)"
using assms proof (induction T arbitrary: T1 T2)
  case Leaf then show ?case by auto
next
  case (Branching T1' T2')
  {
    assume "T1'=Leaf ∧ T2'=Leaf"
    then have "branch ([] @ [True]) (Branching T1' T2') ∧ branch ([] @ [False]) (Branching T1' T2')" by auto
    then have ?case by metis
  }
  moreover
  {
    fix T11 T12
    assume "T1' = Branching T11 T12"
    then obtain B where "branch (B @ [True]) T1'
                       ∧ branch (B @ [False]) T1'" using Branching by blast
    then have "branch (([True] @ B) @ [True]) (Branching T1' T2')
             ∧ branch (([True] @ B) @ [False]) (Branching T1' T2')" by auto
    then have ?case by blast
  }
  moreover
  {
    fix T11 T12
    assume "T2' = Branching T11 T12"
    then obtain B where "branch (B @ [True]) T2'
                       ∧ branch (B @ [False]) T2'" using Branching by blast
    then have "branch (([False] @ B) @ [True]) (Branching T1' T2')
             ∧ branch (([False] @ B) @ [False]) (Branching T1' T2')" by auto
    then have ?case by blast
  }
  ultimately show ?case using tree.exhaust by blast
qed


subsection ‹Internal Paths›

fun internal :: "dir list ==> tree ==> bool" where
  "internal [] (Branching l r) ⟷ True"
| "internal (d#ds) (Branching l r) ⟷ (if d then internal ds l else internal ds r)"
| "internal _ _ ⟷ False"

lemma internal_inv_Leaf: "¬internal b Leaf" using internal.simps by blast

lemma internal_inv_Branching_Left:  
  "internal (Left#b) (Branching l r) ⟷ internal b l" by auto

lemma internal_inv_Branching_Right: 
  "internal (Right#b) (Branching l r) ⟷ internal b r"
by auto

lemma internal_inv_Branching: 
  "internal p (Branching l r) ⟷ (p=[] ∨ (∃a p'. p=a#p'∧ (a ⟶ internal p' l) ∧ (¬a ⟶ internal p' r)))" (is "?L ⟷ ?R")
proof
  assume ?L then show ?R by (metis internal.simps(2) neq_Nil_conv) 
next
  assume r: ?R
  then show ?L
    proof
      assume "p = []" then show ?L by auto
    next
      assume "∃a p'. p=a#p'∧ (a ⟶ internal p' l) ∧ (¬a ⟶ internal p' r)"
      then obtain a p' where "p=a#p'∧ (a ⟶ internal p' l) ∧ (¬a ⟶ internal p' r)" by auto
      then show ?L by (cases a) auto
    qed
qed

lemma internal_is_path: 
  assumes "internal ds T"
  shows "path ds T"
using assms proof (induction T arbitrary: ds)
  case Leaf
  then have "False" using internal_inv_Leaf by auto
  then show ?case by auto
next
  case (Branching T₁ T₂) 
  then obtain a b where ds_p: "ds=[] ∨ ds = a # b ∧ (a ⟶ internal b T₁) ∧ (¬ a ⟶ internal b T₂)" using internal_inv_Branching by blast
  then have "ds = [] ∨ (a ⟶ path b T₁) ∧ (¬a ⟶ path b T₂)" using Branching by auto
  then show "?case" using ds_p by (cases a) auto
qed

lemma internal_prefix:
  assumes "internal (ds1@ds2@[d]) T"
  shows "internal ds1 T" (* more or less copy paste of path_prefix *)
using assms proof (induction ds1 arbitrary: T)
  case (Cons a ds1)
  then have "∃l r. T = Branching l r" using internal_inv_Leaf by (cases T) auto
  then obtain l r where p_lr: "T = Branching l r" by auto
  show ?case
    proof (cases a)
      assume atrue: "a"
      then have "internal ((ds1) @ ds2 @[d]) l" using p_lr Cons(2) internal_inv_Branching by auto
      then have "internal ds1 l" using Cons(1) by auto
      then show "internal (a # ds1) T" using p_lr atrue by auto
    next
      assume afalse: "~a"
      then have "internal ((ds1) @ ds2 @[d]) r" using p_lr Cons(2) internal_inv_Branching by auto
      then have "internal ds1 r" using Cons(1) by auto
      then show "internal (a # ds1) T" using p_lr afalse by auto
    qed
next
  case (Nil)
  then have "∃l r. T = Branching l r" using internal_inv_Leaf by (cases T) auto 
  then show ?case by auto
qed


lemma internal_branch:
  assumes "branch (ds1@ds2@[d]) T"
  shows "internal ds1 T" (* more or less copy paste of path_prefix *)
using assms proof (induction ds1 arbitrary: T)
  case (Cons a ds1)
  then have "∃l r. T = Branching l r" using branch_inv_Leaf by (cases T) auto
  then obtain l r where p_lr: "T = Branching l r" by auto
  show ?case
    proof (cases a)
      assume atrue: "a"
      then have "branch (ds1 @ ds2 @ [d]) l" using p_lr Cons(2) branch_inv_Branching by auto
      then have "internal ds1 l" using Cons(1) by auto
      then show "internal (a # ds1) T" using p_lr atrue by auto
    next
      assume afalse: "~a"
      then have "branch ((ds1) @ ds2 @[d]) r" using p_lr Cons(2) branch_inv_Branching by auto
      then have "internal ds1 r" using Cons(1) by auto
      then show "internal (a # ds1) T" using p_lr afalse by auto
    qed
next
  case (Nil)
  then have "∃l r. T = Branching l r" using branch_inv_Leaf by (cases T) auto 
  then show ?case by auto
qed


fun parent :: "dir list ==> dir list" where
  "parent ds = tl ds"


subsection ‹Deleting Nodes›

fun delete :: "dir list ==> tree ==> tree" where
  "delete [] T = Leaf"
| "delete (True#ds) (Branching T₁ T₂) = Branching (delete ds T₁) T₂"
| "delete (False#ds) (Branching T₁ T₂) = Branching T₁ (delete ds T₂)"
| "delete (a#ds) Leaf = Leaf"

lemma delete_Leaf: "delete T Leaf = Leaf" by (cases T) auto

lemma path_delete: 
  assumes "path p (delete ds T)"
  shows "path p T " (* What a huge proof... But the four cases can be proven shorter *)
using assms proof (induction p arbitrary: T ds)
  case Nil 
  then show ?case by simp
next
  case (Cons a p)
  then obtain b ds' where bds'_p: "ds=b#ds'" by (cases ds) auto

  have "∃dT1 dT2. delete ds T = Branching dT1 dT2" using Cons path_inv_Cons by auto
  then obtain dT1 dT2 where "delete ds T = Branching dT1 dT2" by auto

  then have "∃T1 T2. T=Branching T1 T2" (* Is there a lemma hidden here that I could extract? *)
        by (cases T; cases ds) auto
  then obtain T1 T2 where T1T2_p: "T=Branching T1 T2" by auto

  {
    assume a_p: "a"
    assume b_p: "¬b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching (T1) (delete ds' T2))" using b_p bds'_p T1T2_p by auto
    then have "path p T1" using a_p by auto
    then have ?case using T1T2_p a_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto
    then have "path p T2" using a_p by auto
    then have ?case using T1T2_p a_p by auto
  }
  moreover
  {
    assume a_p: "a"
    assume b_p: "b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto
    then have "path p (delete ds' T1)" using a_p by auto
    then have "path p T1" using Cons by auto
    then have ?case using T1T2_p a_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "¬b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching T1 (delete ds' T2))" using b_p bds'_p T1T2_p by auto
    then have "path p (delete ds' T2)" using a_p by auto
    then have "path p T2" using Cons by auto
    then have ?case using T1T2_p a_p by auto
  }
  ultimately show ?case by blast
qed

lemma branch_delete:
  assumes "branch p (delete ds T)"
  shows "branch p T ∨ p=ds" (* Adapted from above *)
using assms proof (induction p arbitrary: T ds)
  case Nil 
  then have "delete ds T = Leaf" by (cases "delete ds T") auto
  then have "ds = [] ∨ T = Leaf" using delete.elims by blast 
  then show ?case by auto
next
  case (Cons a p)
  then obtain b ds' where bds'_p: "ds=b#ds'" by (cases ds) auto

  have "∃dT1 dT2. delete ds T = Branching dT1 dT2" using Cons path_inv_Cons branch_is_path by blast
  then obtain dT1 dT2 where "delete ds T = Branching dT1 dT2" by auto

  then have "∃T1 T2. T=Branching T1 T2" (* Is there a lemma hidden here that I could extract? *)
        by (cases T; cases ds) auto
  then obtain T1 T2 where T1T2_p: "T=Branching T1 T2" by auto

  {
    assume a_p: "a"
    assume b_p: "¬b"
    have "branch (a # p) (delete ds T)" using Cons by -
    then have "branch (a # p) (Branching (T1) (delete ds' T2))" using b_p bds'_p T1T2_p by auto
    then have "branch p T1" using a_p by auto
    then have ?case using T1T2_p a_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "b"
    have "branch (a # p) (delete ds T)" using Cons by -
    then have "branch (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto
    then have "branch p T2" using a_p by auto
    then have ?case using T1T2_p a_p by auto
  }
  moreover
  {
    assume a_p: "a"
    assume b_p: "b"
    have "branch (a # p) (delete ds T)" using Cons by -
    then have "branch (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto
    then have "branch p (delete ds' T1)" using a_p by auto
    then have "branch p T1 ∨ p = ds'" using Cons by metis
    then have ?case using T1T2_p a_p using bds'_p a_p b_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "¬b"
    have "branch (a # p) (delete ds T)" using Cons by -
    then have "branch (a # p) (Branching T1 (delete ds' T2))" using b_p bds'_p T1T2_p by auto
    then have "branch p (delete ds' T2)" using a_p by auto
    then have "branch p T2 ∨ p = ds'" using Cons by metis
    then have ?case using T1T2_p a_p using bds'_p a_p b_p by auto
  }
  ultimately show ?case by blast
qed
  

lemma branch_delete_postfix: 
  assumes "path p (delete ds T)"
  shows "¬(∃c cs. p = ds @ c#cs)" (* Adapted from previous proof *)
using assms proof (induction p arbitrary: T ds)
  case Nil then show ?case by simp
next
  case (Cons a p)
  then obtain b ds' where bds'_p: "ds=b#ds'" by (cases ds) auto

  have "∃dT1 dT2. delete ds T = Branching dT1 dT2" using Cons path_inv_Cons by auto
  then obtain dT1 dT2 where "delete ds T = Branching dT1 dT2" by auto

  then have "∃T1 T2. T=Branching T1 T2" (* Is there a lemma hidden here that I could extract? *)
        by (cases T; cases ds) auto
  then obtain T1 T2 where T1T2_p: "T=Branching T1 T2" by auto

  {
    assume a_p: "a"
    assume b_p: "¬b"
    then have ?case using T1T2_p a_p b_p bds'_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "b"
    then have ?case using T1T2_p a_p b_p bds'_p by auto
  }
  moreover
  {
    assume a_p: "a"
    assume b_p: "b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto
    then have "path p (delete ds' T1)" using a_p by auto
    then have "¬ (∃c cs. p = ds' @ c # cs)" using Cons by auto
    then have ?case using T1T2_p a_p b_p bds'_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "¬b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching T1 (delete ds' T2))" using b_p bds'_p T1T2_p by auto
    then have "path p (delete ds' T2)" using a_p by auto
    then have "¬ (∃c cs. p = ds' @ c # cs)" using Cons by auto
    then have ?case using T1T2_p a_p b_p bds'_p by auto
  }
  ultimately show ?case by blast
qed

lemma treezise_delete: 
  assumes "internal p T"
  shows "treesize (delete p T) < treesize T"
using assms proof (induction p arbitrary: T)
  case (Nil)
  then have "∃T1 T2. T = Branching T1 T2" by (cases T) auto
  then obtain T1 T2 where T1T2_p: "T = Branching T1 T2" by auto 
  then show ?case by auto
next
  case (Cons a p) 
  then have "∃T1 T2. T = Branching T1 T2" using path_inv_Cons internal_is_path by blast
  then obtain T1 T2 where T1T2_p: "T = Branching T1 T2" by auto
  show ?case
    proof (cases a)
      assume a_p: a
      from a_p have "delete (a#p) T = (Branching (delete p T1) T2)" using T1T2_p by auto
      moreover
      from a_p have "internal p T1" using T1T2_p Cons by auto
      then have "treesize (delete p T1) < treesize T1" using Cons by auto
      ultimately
      show ?thesis using T1T2_p by auto
    next
      assume a_p: "¬a"
      from a_p have "delete (a#p) T = (Branching T1 (delete p T2))" using T1T2_p by auto
      moreover
      from a_p have "internal p T2" using T1T2_p Cons by auto
      then have "treesize (delete p T2) < treesize T2" using Cons by auto
      ultimately
      show ?thesis using T1T2_p by auto
    qed
qed


fun cutoff :: "(dir list ==> bool) ==> dir list ==> tree ==> tree" where
  "cutoff red ds (Branching T₁ T₂) =
     (if red ds then Leaf else Branching (cutoff red (ds@[Left]) T₁) (cutoff red (ds@[Right]) T₂))"
| "cutoff red ds Leaf = Leaf"
text ‹Initially you should call @{const cutoff} with @{term "ds = []"}.
 If all branches are red, then @{const cutoff} gives a subtree.
 If all branches are red, then so are the ones in @{const cutoff}.
 The internal paths of @{const cutoff} are not red.›

lemma treesize_cutoff: "treesize (cutoff red ds T) ≤ treesize T"
proof (induction T arbitrary: ds)
  case Leaf then show ?case by auto
next
  case (Branching T1 T2) 
  then have "treesize (cutoff red (ds@[Left]) T1) + treesize (cutoff red (ds@[Right]) T2) ≤ treesize T1 + treesize T2" using add_mono by blast
  then show ?case by auto
qed

abbreviation anypath :: "tree ==> (dir list ==> bool) ==> bool" where
  "anypath T P ≡ ∀p. path p T ⟶ P p"

abbreviation anybranch :: "tree ==> (dir list ==> bool) ==> bool" where
  "anybranch T P ≡ ∀p. branch p T ⟶ P p"

abbreviation anyinternal :: "tree ==> (dir list ==> bool) ==> bool" where
  "anyinternal T P ≡ ∀p. internal p T ⟶ P p"

lemma cutoff_branch': 
  assumes "anybranch T (λb. red(ds@b))"
  shows "anybranch (cutoff red ds T) (λb. red(ds@b))"
using assms proof (induction T arbitrary: ds) (* This proof seems a bit excessive for such a simple theorem *)
  case (Leaf) 
  let ?T = "cutoff red ds Leaf"
  {
    fix b
    assume "branch b ?T"
    then have "branch b Leaf" by auto
    then have "red(ds@b)" using Leaf by auto
  }
  then show ?case by simp
next
  case (Branching T₁ T₂)
  let ?T = "cutoff red ds (Branching T₁ T₂)"
  from Branching have "∀p. branch (Left#p) (Branching T₁ T₂) ⟶ red (ds @ (Left#p))" by blast
  then have "∀p. branch p T₁ ⟶ red (ds @ (Left#p))"  by auto
  then have "anybranch T₁ (λp. red ((ds @ [Left]) @ p))" by auto
  then have aa: "anybranch (cutoff red (ds @ [Left]) T₁) (λp. red ((ds @ [Left]) @ p))
         " using Branching by blast

  from Branching have "∀p. branch (Right#p) (Branching T₁ T₂) ⟶ red (ds @ (Right#p))" by blast
  then have "∀p. branch p T₂ ⟶ red (ds @ (Right#p))" by auto
  then have "anybranch T₂ (λp. red ((ds @ [Right]) @ p))" by auto
  then have bb: "anybranch (cutoff red (ds @ [Right]) T₂) (λp. red ((ds @ [Right]) @ p))
         " using Branching by blast
  {           
    fix b
    assume b_p: "branch b ?T"
    have "red ds ∨ ¬red ds" by auto
    then have "red(ds@b)"
      proof
        assume ds_p: "red ds"
        then have "?T = Leaf" by auto
        then have "b = []" using b_p branch_inv_Leaf by auto
        then show "red(ds@b)" using ds_p by auto
      next
        assume ds_p: "¬red ds"
        let ?T₁' = "cutoff red (ds@[Left]) T₁"
        let ?T₂' = "cutoff red (ds@[Right]) T₂"
        from ds_p have "?T = Branching ?T₁' ?T₂'" by auto
        from this b_p obtain a b' where "b = a # b' ∧ (a ⟶ branch b' ?T₁') ∧ (¬a ⟶ branch b' ?T₂' )" using branch_inv_Branching[of b ?T₁' ?T₂'] by auto
        then show "red(ds@b)" using aa bb by (cases a) auto
      qed
  }
  then show ?case by blast
qed

lemma cutoff_branch: 
  assumes "anybranch T (λp. red p)"
  shows "anybranch (cutoff red [] T) (λp. red p)" 
  using assms cutoff_branch'[of T red "[]"] by auto

lemma cutoff_internal': 
  assumes "anybranch T (λb. red(ds@b))" 
  shows "anyinternal (cutoff red ds T) (λb. ¬red(ds@b))"
using assms proof (induction T arbitrary: ds) (* This proof seems a bit excessive for such a simple theorem *)
  case (Leaf) then show ?case using internal_inv_Leaf by simp
next                                                     
  case (Branching T₁ T₂)
  let ?T = "cutoff red ds (Branching T₁ T₂)"
  from Branching have "∀p. branch (Left#p) (Branching T₁ T₂) ⟶ red (ds @ (Left#p))" by blast
  then have "∀p. branch p T₁ ⟶ red (ds @ (Left#p))" by auto
  then have "anybranch T₁ (λp. red ((ds @ [Left]) @ p))" by auto
  then have aa: "anyinternal (cutoff red (ds @ [Left]) T₁) (λp. ¬ red ((ds @ [Left]) @ p))" using Branching by blast

  from Branching have "∀p. branch (Right#p) (Branching T₁ T₂) ⟶ red (ds @ (Right#p))" by blast
  then have "∀p. branch p T₂ ⟶ red (ds @ (Right#p))" by auto
  then have "anybranch T₂ (λp. red ((ds @ [Right]) @ p))" by auto
  then have bb: "anyinternal (cutoff red (ds @ [Right]) T₂) (λp. ¬ red ((ds @ [Right]) @ p))" using Branching by blast
  {
    fix p
    assume b_p: "internal p ?T"
    then have ds_p: "¬red ds" using internal_inv_Leaf by auto
    have "p=[] ∨ p≠[]" by auto
    then have "¬red(ds@p)"
      proof
        assume "p=[]" then show "¬red(ds@p)" using ds_p by auto
      next
        let ?T₁' = "cutoff red (ds@[Left]) T₁"
        let ?T₂' = "cutoff red (ds@[Right]) T₂"
        assume "p≠[]"
        moreover
        have "?T = Branching ?T₁' ?T₂'" using ds_p by auto
        ultimately
        obtain a p' where b_p: "p = a # p' ∧
             (a ⟶ internal p' (cutoff red (ds @ [Left]) T₁)) ∧
             (¬ a ⟶ internal p' (cutoff red (ds @ [Right]) T₂))" 
          using b_p internal_inv_Branching[of p ?T₁' ?T₂'] by auto
        then have "¬red(ds @ [a] @ p')" using aa bb by (cases a) auto
        then show "¬red(ds @ p)" using b_p by simp
      qed
  }
  then show ?case by blast
qed

lemma cutoff_internal:
  assumes  "anybranch T red"
  shows "anyinternal (cutoff red [] T) (λp. ¬red p)" 
  using assms cutoff_internal'[of T red "[]"] by auto

lemma cutoff_branch_internal': 
  assumes "anybranch T red"
  shows "anyinternal (cutoff red [] T) (λp. ¬red p) ∧ anybranch (cutoff red [] T) (λp. red p)" 
  using assms cutoff_internal[of T] cutoff_branch[of T] by blast

lemma cutoff_branch_internal: 
  assumes "anybranch T red"
  shows "∃T'. anyinternal T' (λp. ¬red p) ∧ anybranch T' (λp. red p)" 
  using assms cutoff_branch_internal' by blast


section ‹Possibly Infinite Trees›
text ‹Possibly infinite trees are of type @{typ "dir list set"}.›

abbreviation wf_tree :: "dir list set ==> bool" where
  "wf_tree T ≡ (∀ds d. (ds @ d) ∈ T ⟶ ds ∈ T)"

text ‹The subtree in with root r›
fun subtree :: "dir list set ==> dir list ==> dir list set" where 
  "subtree T r = {ds ∈ T. ∃ds'. ds = r @ ds'}" 

text ‹A subtree of a tree is either in the left branch, the right branch, or is the tree itself›
lemma subtree_pos: 
  "subtree T ds ⊆ subtree T (ds @ [Left]) ∪ subtree T (ds @ [Right]) ∪ {ds}"
proof (rule subsetI; rule Set.UnCI)
  let ?subtree = "subtree T"
  fix x
  assume asm: "x ∈ ?subtree ds"
  assume "x ∉ {ds}"
  then have "x ≠ ds" by simp
  then have "∃e d. x = ds @ [d] @ e" using asm list.exhaust by auto
  then have "(∃e. x = ds @ [Left] @ e) ∨ (∃e. x = ds @ [Right] @ e)" using bool.exhaust by auto
  then show "x ∈ ?subtree (ds @ [Left]) ∪ ?subtree (ds @ [Right])" using asm by auto
qed


subsection ‹Infinite Paths›

abbreviation wf_infpath :: "(nat ==> 'a list) ==> bool" where
  "wf_infpath f ≡ (f 0 = []) ∧ (∀n. ∃a. f (Suc n) = (f n) @ [a])"

lemma infpath_length:
  assumes "wf_infpath f"
  shows "length (f n) = n"
using assms proof (induction n)
  case 0 then show ?case by auto
next
  case (Suc n) then show ?case by (metis length_append_singleton)
qed

lemma chain_prefix: 
  assumes "wf_infpath f"
  assumes "n₁ ≤ n₂"
  shows "∃a. (f n₁) @ a = (f n₂)"
using assms proof (induction n₂)
  case (Suc n₂)
  then have "n₁ ≤ n₂ ∨ n₁ = Suc n₂" by auto
  then show ?case
    proof
      assume "n₁ ≤ n₂"
      then obtain a where a: "f n₁ @ a = f n₂" using Suc by auto
      have b: "∃b. f (Suc n₂) = f n₂ @ [b]" using Suc by auto 
      from a b have "∃b. f n₁ @ (a @ [b]) = f (Suc n₂)" by auto
      then show "∃c. f n₁ @ c = f (Suc n₂)" by blast
    next
      assume "n₁ = Suc n₂"
      then have "f n₁ @ [] = f (Suc n₂)" by auto
      then show "∃a. f n₁ @ a = f (Suc n₂)" by auto
    qed
qed auto

text ‹If we make a lookup in a list, then looking up in an extension gives us the same value.›
lemma ith_in_extension:
  assumes chain: "wf_infpath f"
  assumes smalli: "i < length (f n₁)"
  assumes n₁n₂: "n₁ ≤ n₂"
  shows "f n₁ ! i = f n₂ ! i"
proof -
  from chain n₁n₂ have "∃a. f n₁ @ a = f n₂" using chain_prefix by blast
  then obtain a where a_p: "f n₁ @ a = f n₂" by auto
  have "(f n₁ @ a) ! i = f n₁ ! i" using smalli by (simp add: nth_append) 
  then show ?thesis using a_p by auto
qed


section ‹König's Lemma›

lemma inf_subs: 
  assumes inf: "¬finite(subtree T ds)"
  shows "¬finite(subtree T (ds @ [Left])) ∨ ¬finite(subtree T (ds @ [Right]))"
proof -
  let ?subtree = "subtree T"
  {
    assume asms: "finite(?subtree(ds @ [Left]))"
                 "finite(?subtree(ds @ [Right]))"
    have "?subtree ds ⊆ ?subtree (ds @ [Left] ) ∪ ?subtree (ds @ [Right]) ∪ {ds} " 
      using subtree_pos by auto
    then have "finite(?subtree (ds))" using asms by (simp add: finite_subset)
  } 
  then show "¬finite(?subtree (ds @ [Left])) ∨ ¬finite(?subtree (ds @ [Right]))" using inf by auto
qed

fun buildchain :: "(dir list ==> dir list) ==> nat ==> dir list" where
  "buildchain next 0 = []"
| "buildchain next (Suc n) = next (buildchain next n)"

lemma konig:
  assumes inf: "¬finite T"
  assumes wellformed: "wf_tree T"
  shows "∃c. wf_infpath c ∧ (∀n. (c n) ∈ T)"
proof
  let ?subtree = "subtree T"
  let ?nextnode = "λds. (if ¬finite (?subtree (ds @ [Left])) then ds @ [Left] else ds @ [Right])" 

  let ?c = "buildchain ?nextnode"

  have is_chain: "wf_infpath ?c" by auto

  from wellformed have prefix: "∀ds d. (ds @ d) ∈ T ⟶ ds ∈ T" by blast

  { 
    fix n
    have "(?c n) ∈ T ∧ ¬finite (?subtree (?c n))"
      proof (induction n)
        case 0
        have "∃ds. ds ∈ T" using inf by (simp add: not_finite_existsD)
        then obtain ds where "ds ∈ T" by auto
        then have "([]@ds) ∈ T" by auto
        then have "[] ∈ T" using prefix by blast 
        then show ?case using inf by auto
      next
        case (Suc n)
        from Suc have next_in:  "(?c n) ∈ T" by auto
        from Suc have next_inf: "¬finite (?subtree (?c n))" by auto

        from next_inf have next_next_inf:
           "¬finite (?subtree (?nextnode (?c n)))" 
              using inf_subs by auto
        then have "∃ds. ds ∈ ?subtree (?nextnode (?c n))"
          by (simp add: not_finite_existsD)
        then obtain ds where dss: "ds ∈ ?subtree (?nextnode (?c n))" by auto
        then have "ds ∈ T" "∃suf. ds = (?nextnode (?c n)) @ suf" by auto
        then obtain suf where "ds ∈ T ∧ ds = (?nextnode (?c n)) @ suf" by auto
        then have "(?nextnode (?c n)) ∈ T"
          using prefix by blast
              
        then have "(?c (Suc n)) ∈ T" by auto
        then show ?case using next_next_inf by auto
      qed
  }
  then show "wf_infpath ?c ∧ (∀n. (?c n)∈ T) " using is_chain by auto
qed

end