(* Title: Koenig's lemma with paths modelled as coinductive lists Author: Andreas Lochbihler *) section ‹Example: Koenig's lemma› theory Koenigslemma imports "../Coinductive_List" begin type_synonym 'node graph = "'node ⇒ 'node ⇒ bool" type_synonym 'node path = "'node llist" coinductive_set paths :: "'node graph ⇒ 'node path set" for graph :: "'node graph" where Empty: "LNil ∈ paths graph" | Single: "LCons x LNil ∈ paths graph" | LCons: "⟦ graph x y; LCons y xs ∈ paths graph ⟧ ⟹ LCons x (LCons y xs) ∈ paths graph" definition connected :: "'node graph ⇒ bool" where "connected graph ⟷ (∀n n'. ∃xs. llist_of (n # xs @ [n']) ∈ paths graph)" inductive_set reachable_via :: "'node graph ⇒ 'node set ⇒ 'node ⇒ 'node set" for graph :: "'node graph" and ns :: "'node set" and n :: "'node" where "⟦ LCons n xs ∈ paths graph; n' ∈ lset xs; lset xs ⊆ ns ⟧ ⟹ n' ∈ reachable_via graph ns n" lemma connectedD: "connected graph ⟹ ∃xs. llist_of (n # xs @ [n']) ∈ paths graph" unfolding connected_def by blast lemma paths_LConsD: assumes "LCons x xs ∈ paths graph" shows "xs ∈ paths graph" using assms by(coinduct)(fastforce elim: paths.cases del: disjCI) lemma paths_lappendD1: assumes "lappend xs ys ∈ paths graph" shows "xs ∈ paths graph" using assms apply coinduct apply(erule paths.cases) apply(simp add: lappend_eq_LNil_iff) apply(case_tac x) apply simp apply(simp add: lappend_eq_LNil_iff) apply(case_tac x) apply simp apply(case_tac x22) apply simp apply simp done lemma paths_lappendD2: assumes "lfinite xs" and "lappend xs ys ∈ paths graph" shows "ys ∈ paths graph" using assms by induct(fastforce elim: paths.cases intro: paths.intros)+ lemma path_avoid_node: assumes path: "LCons n xs ∈ paths graph" and set: "x ∈ lset xs" and n_neq_x: "n ≠ x" shows "∃xs'. LCons n xs' ∈ paths graph ∧ lset xs' ⊆ lset xs ∧ x ∈ lset xs' ∧ n ∉ lset xs'" proof - from set obtain xs' xs'' where "lfinite xs'" and xs: "xs = lappend xs' (LCons x xs'')" and "x ∉ lset xs'" by(blast dest: split_llist_first) show ?thesis proof(cases "n ∈ lset xs'") case False let ?xs' = "lappend xs' (LCons x LNil)" from xs path have "lappend (LCons n (lappend xs' (LCons x LNil))) xs'' ∈ paths graph" by(simp add: lappend_assoc) hence "LCons n ?xs' ∈ paths graph" by(rule paths_lappendD1) moreover have "x ∈ lset ?xs'" "lset ?xs' ⊆ lset xs" "n ∉ lset ?xs'" using xs False ‹lfinite xs'› n_neq_x by auto ultimately show ?thesis by blast next case True from ‹lfinite xs'› obtain XS' where xs': "xs' = llist_of XS'" unfolding lfinite_eq_range_llist_of by blast with True have "n ∈ set XS'" by simp from split_list_last[OF this] obtain ys zs where XS': "XS' = ys @ n # zs" and "n ∉ set zs" by blast let ?xs' = "lappend (llist_of zs) (LCons x LNil)" have "lfinite (LCons n (llist_of ys))" by simp moreover from xs xs' XS' path have "lappend (LCons n (llist_of ys)) (lappend (LCons n ?xs') xs'') ∈ paths graph" by(simp add: lappend_assoc)(metis lappend_assoc lappend_llist_of_LCons lappend_llist_of_llist_of llist_of.simps(2)) ultimately have "lappend (LCons n ?xs') xs'' ∈ paths graph" by(rule paths_lappendD2) hence "LCons n ?xs' ∈ paths graph" by(rule paths_lappendD1) moreover have "x ∈ lset ?xs'" "lset ?xs' ⊆ lset xs" "n ∉ lset ?xs'" using xs xs' XS' ‹lfinite xs'› n_neq_x ‹n ∉ set zs› by auto ultimately show ?thesis by blast qed qed lemma reachable_via_subset_unfold: "reachable_via graph ns n ⊆ (⋃n' ∈ {n'. graph n n'} ∩ ns. insert n' (reachable_via graph (ns - {n'}) n'))" (is "?lhs ⊆ ?rhs") proof(rule subsetI) fix x assume "x ∈ ?lhs" then obtain xs where path: "LCons n xs ∈ paths graph" and "x ∈ lset xs" "lset xs ⊆ ns" by cases from ‹x ∈ lset xs› obtain n' xs' where xs: "xs = LCons n' xs'" by(cases xs) auto with path have "graph n n'" by cases simp_all moreover from ‹lset xs ⊆ ns› xs have "n' ∈ ns" by simp ultimately have "n' ∈ {n'. graph n n'} ∩ ns" by simp thus "x ∈ ?rhs" proof(rule UN_I) show "x ∈ insert n' (reachable_via graph (ns - {n'}) n')" proof(cases "x = n'") case True thus ?thesis by simp next case False with xs ‹x ∈ lset xs› have "x ∈ lset xs'" by simp with path xs have path': "LCons n' xs' ∈ paths graph" by cases simp_all from ‹lset xs ⊆ ns› xs have "lset xs' ⊆ ns" by simp from path_avoid_node[OF path' ‹x ∈ lset xs'›] False obtain xs'' where path'': "LCons n' xs'' ∈ paths graph" and "lset xs'' ⊆ lset xs'" "x ∈ lset xs''" "n' ∉ lset xs''" by blast with False ‹lset xs ⊆ ns› xs show ?thesis by(auto intro: reachable_via.intros) qed qed qed theorem koenigslemma: fixes graph :: "'node graph" and n :: 'node assumes connected: "connected graph" and infinite: "infinite (UNIV :: 'node set)" and finite_branching: "⋀n. finite {n'. graph n n'}" shows "∃xs ∈ paths graph. n ∈ lset xs ∧ ¬ lfinite xs ∧ ldistinct xs" proof(intro bexI conjI) let ?P = "λ(n, ns) n'. graph n n' ∧ infinite (reachable_via graph (- insert n (insert n' ns)) n') ∧ n' ∉ insert n ns" define LTL where "LTL = (λ(n, ns). let n' = SOME n'. ?P (n, ns) n' in (n', insert n ns))" define f where "f = unfold_llist (λ_. False) fst LTL" define ns :: "'node set" where "ns = {}" { fix n ns assume "infinite (reachable_via graph (- insert n ns) n)" hence "∃n'. ?P (n, ns) n'" proof(rule contrapos_np) assume "¬ ?thesis" hence fin: "⋀n'. ⟦ graph n n'; n' ∉ insert n ns ⟧ ⟹ finite (reachable_via graph (- insert n (insert n' ns)) n')" by blast from reachable_via_subset_unfold[of graph "- insert n ns" n] show "finite (reachable_via graph (- insert n ns) n)" proof(rule finite_subset[OF _ finite_UN_I]) from finite_branching[of n] show "finite ({n'. graph n n'} ∩ - insert n ns)" by blast next fix n' assume "n' ∈ {n'. graph n n'} ∩ - insert n ns" hence "graph n n'" "n' ∉ insert n ns" by simp_all from fin[OF this] have "finite (reachable_via graph (- insert n (insert n' ns)) n')" . moreover have "- insert n (insert n' ns) = - insert n ns - {n'}" by auto ultimately show "finite (insert n' (reachable_via graph (- insert n ns - {n'}) n'))" by simp qed qed } note ex_P_I = this { fix n ns have "¬ lnull (f (n, ns))" "lhd (f (n, ns)) = n" "ltl (f (n, ns)) = (let n' = SOME n'. ?P (n, ns) n' in f (n', insert n ns))" by(simp_all add: f_def LTL_def) } note f_simps [simp] = this { fix n :: 'node and ns :: "'node set" and x :: 'node assume "x ∈ lset (f (n, ns))" "n ∉ ns" and "finite ns" "infinite (reachable_via graph (- insert n ns) n)" hence "x ∉ ns" proof(induct "f (n, ns)" arbitrary: n ns rule: lset_induct) case find thus ?case by(auto 4 4 dest: sym eq_LConsD) next case (step x' xs) let ?n' = "Eps (?P (n, ns))" and ?ns' = "insert n ns" from eq_LConsD[OF ‹LCons x' xs = f (n, ns)›[symmetric]] have [simp]: "x' = n" and xs: "xs = f (?n', ?ns')" by auto from ‹infinite (reachable_via graph (- insert n ns) n)› have "∃n'. ?P (n, ns) n'" by(rule ex_P_I) hence P: "?P (n, ns) ?n'" by(rule someI_ex) moreover have "insert ?n' ?ns' = insert n (insert ?n' ns)" by auto ultimately have "?n' ∉ ?ns'" "finite ?ns'" and "infinite (reachable_via graph (- insert ?n' ?ns') ?n')" using ‹finite ns› by auto with xs have "x ∉ ?ns'" by(rule step) thus ?case by simp qed } note lset = this show "n ∈ lset (f (n, ns))" using llist.set_sel(1)[OF f_simps(1), of n ns] by(simp del: llist.set_sel(1)) show "¬ lfinite (f (n, ns))" proof assume "lfinite (f (n, ns))" thus False by(induct "f (n, ns)" arbitrary: n ns rule: lfinite_induct) auto qed let ?X = "λxs. ∃n ns. xs = f (n, ns) ∧ finite ns ∧ infinite (reachable_via graph (- insert n ns) n)" have "reachable_via graph (- {n}) n ⊇ - {n}" proof(rule subsetI) fix n' :: 'node assume "n' ∈ - {n}" hence "n ≠ n'" by auto from connected obtain xs where "llist_of (n # xs @ [n']) ∈ paths graph" by(blast dest: connectedD) hence "LCons n (llist_of (xs @ [n'])) ∈ paths graph" and "n' ∈ lset (llist_of (xs @ [n']))" by simp_all from path_avoid_node[OF this ‹n ≠ n'›] show "n' ∈ reachable_via graph (- {n}) n" by(auto intro: reachable_via.intros) qed hence "infinite (reachable_via graph (- {n}) n)" using infinite by(auto dest: finite_subset) hence X: "?X (f (n, {}))" by(auto) thus "f (n, {}) ∈ paths graph" proof(coinduct) case (paths xs) then obtain n ns where xs_def: "xs = f (n, ns)" and "finite ns" and "infinite (reachable_via graph (- insert n ns) n)" by blast from ‹infinite (reachable_via graph (- insert n ns) n)› have "∃n'. ?P (n, ns) n'" by(rule ex_P_I) hence P: "?P (n, ns) (Eps (?P (n, ns)))" by(rule someI_ex) let ?n' = "Eps (?P (n, ns))" let ?ns' = "insert n ns" let ?n'' = "Eps (?P (?n', ?ns'))" let ?ns'' = "insert ?n' ?ns'" have "xs = LCons n (LCons ?n' (f (?n'', ?ns'')))" unfolding xs_def by(auto 4 3 intro: llist.expand) moreover from P have "graph n ?n'" by simp moreover { have "LCons ?n' (f (?n'', ?ns'')) = f (?n', ?ns')" by(rule llist.expand) simp_all moreover have "finite ?ns'" using ‹finite ns› by simp moreover have "insert ?n' ?ns' = insert n (insert ?n' ns)" by auto hence "infinite (reachable_via graph (- insert ?n' ?ns') ?n')" using P by simp ultimately have "?X (LCons ?n' (f (?n'', ?ns'')))" by blast } ultimately have ?LCons by simp thus ?case by simp qed from ‹infinite (reachable_via graph (- {n}) n)› have "infinite (reachable_via graph (- insert n ns) n) ∧ finite ns" by(simp add: ns_def) thus "ldistinct (f (n, ns))" proof(coinduction arbitrary: n ns) case (ldistinct n ns) then obtain "finite ns" and "infinite (reachable_via graph (- insert n ns) n)" by simp from ‹infinite (reachable_via graph (- insert n ns) n)› have "∃n'. ?P (n, ns) n'" by(rule ex_P_I) hence P: "?P (n, ns) (Eps (?P (n, ns)))" by(rule someI_ex) let ?n' = "Eps (?P (n, ns))" let ?ns' = "insert n ns" have eq: "insert ?n' ?ns' = insert n (insert ?n' ns)" by auto hence "n ∉ lset (f (?n', ?ns'))" using P ‹finite ns› by(auto dest: lset) moreover from ‹finite ns› P eq have "infinite (reachable_via graph (- insert ?n' ?ns') ?n')" by simp ultimately show ?case using ‹finite ns› by auto qed qed end