theory Tree imports Main begin
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)
section {* Sizes *}
fun treesize :: "tree ⇒ nat" where
"treesize Leaf = 0"
| "treesize (Branching l r) = 1 + treesize l + treesize r"
lemma treesize_Leaf: "treesize T = 0 ⟹ T = Leaf" by (cases T) auto
lemma treesize_Branching: "treesize T = Suc n ⟹ ∃l r. T = Branching l r" by (cases T) auto
section {* 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: "path (ds1@ds2) T ⟹ path ds1 T"
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
section {* 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⇩1 T⇩2)
then obtain b where "branch b T⇩1" by auto
then have "branch (Left#b) (Branching T⇩1 T⇩2)" 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:
"branch ds T ⟹ path ds T"
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⇩1 T⇩2)
then obtain a b where ds_p: "ds = a # b ∧ (a ⟶ branch b T⇩1) ∧ (¬ a ⟶ branch b T⇩2)" using branch_inv_Branching[of ds] by blast
then have "(a ⟶ path b T⇩1) ∧ (¬a ⟶ path b T⇩2)" using Branching by auto
then show "?case" using ds_p by (cases a) auto
qed
lemma Branching_Leaf_Leaf_Tree: "T = Branching T1 T2 ⟹ (∃B. branch (B@[True]) T ∧ branch (B@[False]) T)"
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
section {* 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:
"internal ds T ⟹ path ds T"
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⇩1 T⇩2)
then obtain a b where ds_p: "ds=[] ∨ ds = a # b ∧ (a ⟶ internal b T⇩1) ∧ (¬ a ⟶ internal b T⇩2)" using internal_inv_Branching by blast
then have "ds = [] ∨ (a ⟶ path b T⇩1) ∧ (¬a ⟶ path b T⇩2)" using Branching by auto
then show "?case" using ds_p by (cases a) auto
qed
lemma internal_prefix: "internal (ds1@ds2@[d]) T ⟹ internal ds1 T"
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: "branch (ds1@ds2@[d]) T ⟹ internal ds1 T"
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"
section {* Deleting Nodes *}
fun delete :: "dir list ⇒ tree ⇒ tree" where
"delete [] T = Leaf"
| "delete (True#ds) (Branching T⇩1 T⇩2) = Branching (delete ds T⇩1) T⇩2"
| "delete (False#ds) (Branching T⇩1 T⇩2) = Branching T⇩1 (delete ds T⇩2)"
| "delete (a#ds) Leaf = Leaf"
lemma delete_Leaf: "delete T Leaf = Leaf" by (cases T) auto
lemma path_delete: "path p (delete ds T) ⟹ path p T "
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"
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: "branch p (delete ds T) ⟹ branch p T ∨ p=ds"
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"
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: "path p (delete ds T) ⟹ ¬(∃c cs. p = ds @ c#cs)"
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"
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: "internal p T ⟹ treesize (delete p T) < treesize T"
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⇩1 T⇩2) =
(if red ds then Leaf else Branching (cutoff red (ds@[Left]) T⇩1) (cutoff red (ds@[Right]) T⇩2))"
| "cutoff red ds Leaf = Leaf"
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':
"anybranch T (λb. red(ds@b)) ⟹ anybranch (cutoff red ds T) (λb. red(ds@b))"
proof (induction T arbitrary: ds)
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⇩1 T⇩2)
let ?T = "cutoff red ds (Branching T⇩1 T⇩2)"
from Branching have "∀p. branch (Left#p) (Branching T⇩1 T⇩2) ⟶ red (ds @ (Left#p))" by blast
then have "∀p. branch p T⇩1 ⟶ red (ds @ (Left#p))" by auto
then have "anybranch T⇩1 (λp. red ((ds @ [Left]) @ p))" by auto
then have aa: "anybranch (cutoff red (ds @ [Left]) T⇩1) (λp. red ((ds @ [Left]) @ p))
" using Branching by blast
from Branching have "∀p. branch (Right#p) (Branching T⇩1 T⇩2) ⟶ red (ds @ (Right#p))" by blast
then have "∀p. branch p T⇩2 ⟶ red (ds @ (Right#p))" by auto
then have "anybranch T⇩2 (λp. red ((ds @ [Right]) @ p))" by auto
then have bb: "anybranch (cutoff red (ds @ [Right]) T⇩2) (λ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⇩1' = "cutoff red (ds@[Left]) T⇩1"
let ?T⇩2' = "cutoff red (ds@[Right]) T⇩2"
from ds_p have "?T = Branching ?T⇩1' ?T⇩2'" by auto
from this b_p obtain a b' where "b = a # b' ∧ (a ⟶ branch b' ?T⇩1') ∧ (¬a ⟶ branch b' ?T⇩2' )" using branch_inv_Branching[of b ?T⇩1' ?T⇩2'] by auto
then show "red(ds@b)" using aa bb by (cases a) auto
qed
}
then show ?case by blast
qed
lemma cutoff_branch: "anybranch T (λp. red p) ⟹ anybranch (cutoff red [] T) (λp. red p)"
using cutoff_branch'[of T red "[]"] by auto
lemma cutoff_internal':
"anybranch T (λb. red(ds@b)) ⟹ anyinternal (cutoff red ds T) (λb. ¬red(ds@b))"
proof (induction T arbitrary: ds)
case (Leaf) then show ?case using internal_inv_Leaf by simp
next
case (Branching T⇩1 T⇩2)
let ?T = "cutoff red ds (Branching T⇩1 T⇩2)"
from Branching have "∀p. branch (Left#p) (Branching T⇩1 T⇩2) ⟶ red (ds @ (Left#p))" by blast
then have "∀p. branch p T⇩1 ⟶ red (ds @ (Left#p))" by auto
then have "anybranch T⇩1 (λp. red ((ds @ [Left]) @ p))" by auto
then have aa: "anyinternal (cutoff red (ds @ [Left]) T⇩1) (λp. ¬ red ((ds @ [Left]) @ p))" using Branching by blast
from Branching have "∀p. branch (Right#p) (Branching T⇩1 T⇩2) ⟶ red (ds @ (Right#p))" by blast
then have "∀p. branch p T⇩2 ⟶ red (ds @ (Right#p))" by auto
then have "anybranch T⇩2 (λp. red ((ds @ [Right]) @ p))" by auto
then have bb: "anyinternal (cutoff red (ds @ [Right]) T⇩2) (λ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⇩1' = "cutoff red (ds@[Left]) T⇩1"
let ?T⇩2' = "cutoff red (ds@[Right]) T⇩2"
assume "p≠[]"
moreover
have "?T = Branching ?T⇩1' ?T⇩2'" using ds_p by auto
ultimately
obtain a p' where b_p: "p = a # p' ∧
(a ⟶ internal p' (cutoff red (ds @ [Left]) T⇩1)) ∧
(¬ a ⟶ internal p' (cutoff red (ds @ [Right]) T⇩2))"
using b_p internal_inv_Branching[of p ?T⇩1' ?T⇩2'] 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: "anybranch T red ⟹ anyinternal (cutoff red [] T) (λp. ¬red p)"
using cutoff_internal'[of T red "[]"] by auto
lemma cutoff_branch_internal':
"anybranch T red ⟹ anyinternal (cutoff red [] T) (λp. ¬red p) ∧ anybranch (cutoff red [] T) (λp. red p)"
using cutoff_internal[of T] cutoff_branch[of T] by blast
lemma cutoff_branch_internal:
"anybranch T red ⟹ ∃T'. anyinternal T' (λp. ¬red p) ∧ anybranch T' (λp. red p)"
using cutoff_branch_internal' by blast
section {* Possibly Infinite Trees *}
abbreviation wf_tree :: "dir list set ⇒ bool" where
"wf_tree T ≡ (∀ds d. (ds @ d) ∈ T ⟶ ds ∈ T)"
fun subtree :: "dir list set ⇒ dir list ⇒ dir list set" where
"subtree T r = {ds ∈ T. ∃ds'. ds = r @ ds'}"
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
section {* 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: "wf_infpath f ⟹ length (f n) = n"
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: "wf_infpath f ⟹ n⇩1 ≤ n⇩2 ⟹ ∃a. (f n⇩1) @ a = (f n⇩2)"
proof (induction n⇩2)
case (Suc n⇩2)
then have "n⇩1 ≤ n⇩2 ∨ n⇩1 = Suc n⇩2" by auto
then show ?case
proof
assume "n⇩1 ≤ n⇩2"
then obtain a where a: "f n⇩1 @ a = f n⇩2" using Suc by auto
have b: "∃b. f (Suc n⇩2) = f n⇩2 @ [b]" using Suc by auto
from a b have "∃b. f n⇩1 @ (a @ [b]) = f (Suc n⇩2)" by auto
then show "∃c. f n⇩1 @ c = f (Suc n⇩2)" by blast
next
assume "n⇩1 = Suc n⇩2"
then have "f n⇩1 @ [] = f (Suc n⇩2)" by auto
then show "∃a. f n⇩1 @ a = f (Suc n⇩2)" by auto
qed
qed auto
lemma ith_in_extension:
assumes chain: "wf_infpath f"
assumes smalli: "i < length (f n⇩1)"
assumes n⇩1n⇩2: "n⇩1 ≤ n⇩2"
shows "f n⇩1 ! i = f n⇩2 ! i"
proof -
from chain n⇩1n⇩2 have "∃a. f n⇩1 @ a = f n⇩2" using chain_prefix by blast
then obtain a where a_p: "f n⇩1 @ a = f n⇩2" by auto
have "(f n⇩1 @ a) ! i = f n⇩1 ! 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 T (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[of "[]"] by auto
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[of "?nextnode (?c n)" suf] by auto
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