Theory Util
section ‹Utility Definitions and Properties›
text ‹This file contains various definitions and lemmata not closely related to finite state
machines or testing.›
theory Util
imports Main "HOL-Library.FSet" "HOL-Library.Sublist" "HOL-Library.Mapping"
begin
subsection ‹Converting Sets to Maps›
text ‹This subsection introduces a function @{text "set_as_map"} that transforms a set of
@{text "('a × 'b)"} tuples to a map mapping each first value @{text "x"} of the contained tuples
to all second values @{text "y"} such that @{text "(x,y)"} is contained in the set.›
definition set_as_map :: "('a × 'c) set ⇒ ('a ⇒ 'c set option)" where
"set_as_map s = (λ x . if (∃ z . (x,z) ∈ s) then Some {z . (x,z) ∈ s} else None)"
lemma set_as_map_code[code] :
"set_as_map (set xs) = (foldl (λ m (x,z) . case m x of
None ⇒ m (x ↦ {z}) |
Some zs ⇒ m (x ↦ (insert z zs)))
Map.empty
xs)"
proof -
let ?f = "λ xs . (foldl (λ m (x,z) . case m x of
None ⇒ m (x ↦ {z}) |
Some zs ⇒ m (x ↦ (insert z zs)))
Map.empty
xs)"
have "(?f xs) = (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None)"
proof (induction xs rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc xz xs)
then obtain x z where "xz = (x,z)"
by force
have *: "(?f (xs@[(x,z)])) = (case (?f xs) x of
None ⇒ (?f xs) (x ↦ {z}) |
Some zs ⇒ (?f xs) (x ↦ (insert z zs)))"
by auto
then show ?case proof (cases "(?f xs) x")
case None
then have **: "(?f (xs@[(x,z)])) = (?f xs) (x ↦ {z})" using * by auto
have scheme: "⋀ m k v . (m(k ↦ v)) = (λk' . if k' = k then Some v else m k')"
by auto
have m1: "(?f (xs@[(x,z)])) = (λ x' . if x' = x then Some {z} else (?f xs) x')"
unfolding **
unfolding scheme by force
have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = None"
using None snoc by auto
then have "¬(∃ z . (x,z) ∈ set xs)"
by (metis (mono_tags, lifting) option.distinct(1))
then have "(∃ z . (x,z) ∈ set (xs@[(x,z)]))" and "{z' . (x,z') ∈ set (xs@[(x,z)])} = {z}"
by auto
then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)]))
then Some {z' . (x',z') ∈ set (xs@[(x,z)])}
else None)
= (λ x' . if x' = x
then Some {z} else (λ x . if (∃ z . (x,z) ∈ set xs)
then Some {z . (x,z) ∈ set xs}
else None) x')"
by force
show ?thesis using m1 m2 snoc
using ‹xz = (x, z)› by presburger
next
case (Some zs)
then have **: "(?f (xs@[(x,z)])) = (?f xs) (x ↦ (insert z zs))" using * by auto
have scheme: "⋀ m k v . (m(k ↦ v)) = (λk' . if k' = k then Some v else m k')"
by auto
have m1: "(?f (xs@[(x,z)])) = (λ x' . if x' = x then Some (insert z zs) else (?f xs) x')"
unfolding **
unfolding scheme by force
have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = Some zs"
using Some snoc by auto
then have "(∃ z . (x,z) ∈ set xs)"
unfolding case_prod_conv using option.distinct(2) by metis
then have "(∃ z . (x,z) ∈ set (xs@[(x,z)]))" by simp
have "{z' . (x,z') ∈ set (xs@[(x,z)])} = insert z zs"
proof -
have "Some {z . (x,z) ∈ set xs} = Some zs"
using ‹(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x
= Some zs›
unfolding case_prod_conv using option.distinct(2) by metis
then have "{z . (x,z) ∈ set xs} = zs" by auto
then show ?thesis by auto
qed
have "⋀ a . (λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)]))
then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
= (λ x' . if x' = x
then Some (insert z zs)
else (λ x . if (∃ z . (x,z) ∈ set xs)
then Some {z . (x,z) ∈ set xs} else None) x') a"
proof -
fix a show "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)]))
then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
= (λ x' . if x' = x
then Some (insert z zs)
else (λ x . if (∃ z . (x,z) ∈ set xs)
then Some {z . (x,z) ∈ set xs} else None) x') a"
using ‹{z' . (x,z') ∈ set (xs@[(x,z)])} = insert z zs› ‹(∃ z . (x,z) ∈ set (xs@[(x,z)]))›
by (cases "a = x"; auto)
qed
then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)]))
then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None)
= (λ x' . if x' = x
then Some (insert z zs)
else (λ x . if (∃ z . (x,z) ∈ set xs)
then Some {z . (x,z) ∈ set xs} else None) x')"
by auto
show ?thesis using m1 m2 snoc
using ‹xz = (x, z)› by presburger
qed
qed
then show ?thesis
unfolding set_as_map_def by simp
qed
abbreviation "member_option x ms ≡ (case ms of None ⇒ False | Some xs ⇒ x ∈ xs)"
notation member_option ("(_∈⇩o_)" [1000] 1000)
abbreviation(input) "lookup_with_default f d ≡ (λ x . case f x of None ⇒ d | Some xs ⇒ xs)"
abbreviation(input) "m2f f ≡ lookup_with_default f {}"
abbreviation(input) "lookup_with_default_by f g d ≡ (λ x . case f x of None ⇒ g d | Some xs ⇒ g xs)"
abbreviation(input) "m2f_by g f ≡ lookup_with_default_by f g {}"
lemma m2f_by_from_m2f :
"(m2f_by g f xs) = g (m2f f xs)"
by (simp add: option.case_eq_if)
lemma set_as_map_containment :
assumes "(x,y) ∈ zs"
shows "y ∈ (m2f (set_as_map zs)) x"
using assms unfolding set_as_map_def
by auto
lemma set_as_map_elem :
assumes "y ∈ m2f (set_as_map xs) x"
shows "(x,y) ∈ xs"
using assms unfolding set_as_map_def
proof -
assume a1: "y ∈ (case if ∃z. (x, z) ∈ xs then Some {z. (x, z) ∈ xs} else None of None ⇒ {} | Some xs ⇒ xs)"
then have "∃a. (x, a) ∈ xs"
using all_not_in_conv by fastforce
then show ?thesis
using a1 by simp
qed
subsection ‹Utility Lemmata for existing functions on lists›
subsubsection ‹Utility Lemmata for @{text "find"}›
lemma find_result_props :
assumes "find P xs = Some x"
shows "x ∈ set xs" and "P x"
proof -
show "x ∈ set xs" using assms by (metis find_Some_iff nth_mem)
show "P x" using assms by (metis find_Some_iff)
qed
lemma find_set :
assumes "find P xs = Some x"
shows "x ∈ set xs"
using assms proof(induction xs)
case Nil
then show ?case by auto
next
case (Cons a xs)
then show ?case
by (metis find.simps(2) list.set_intros(1) list.set_intros(2) option.inject)
qed
lemma find_condition :
assumes "find P xs = Some x"
shows "P x"
using assms proof(induction xs)
case Nil
then show ?case by auto
next
case (Cons a xs)
then show ?case
by (metis find.simps(2) option.inject)
qed
lemma find_from :
assumes "∃ x ∈ set xs . P x"
shows "find P xs ≠ None"
by (metis assms find_None_iff)
lemma find_sort_containment :
assumes "find P (sort xs) = Some x"
shows "x ∈ set xs"
using assms find_set by force
lemma find_sort_index :
assumes "find P xs = Some x"
shows "∃ i < length xs . xs ! i = x ∧ (∀ j < i . ¬ P (xs ! j))"
using assms proof (induction xs arbitrary: x)
case Nil
then show ?case by auto
next
case (Cons a xs)
show ?case proof (cases "P a")
case True
then show ?thesis
using Cons.prems unfolding find.simps by auto
next
case False
then have "find P (a#xs) = find P xs"
unfolding find.simps by auto
then have "find P xs = Some x"
using Cons.prems by auto
then show ?thesis
using Cons.IH False
by (metis Cons.prems find_Some_iff)
qed
qed
lemma find_sort_least :
assumes "find P (sort xs) = Some x"
shows "∀ x' ∈ set xs . x ≤ x' ∨ ¬ P x'"
and "x = (LEAST x' ∈ set xs . P x')"
proof -
obtain i where "i < length (sort xs)"
and "(sort xs) ! i = x"
and "(∀ j < i . ¬ P ((sort xs) ! j))"
using find_sort_index[OF assms] by blast
have "⋀ j . j > i ⟹ j < length xs ⟹ (sort xs) ! i ≤ (sort xs) ! j"
by (simp add: sorted_nth_mono)
then have "⋀ j . j < length xs ⟹ (sort xs) ! i ≤ (sort xs) ! j ∨ ¬ P ((sort xs) ! j)"
using ‹(∀ j < i . ¬ P ((sort xs) ! j))›
by (metis not_less_iff_gr_or_eq order_refl)
then show "∀ x' ∈ set xs . x ≤ x' ∨ ¬ P x'"
by (metis ‹sort xs ! i = x› in_set_conv_nth length_sort set_sort)
then show "x = (LEAST x' ∈ set xs . P x')"
using find_set[OF assms] find_condition[OF assms]
by (metis (mono_tags, lifting) Least_equality set_sort)
qed
subsubsection ‹Utility Lemmata for @{text "filter"}›
lemma filter_take_length :
"length (filter P (take i xs)) ≤ length (filter P xs)"
by (metis append_take_drop_id filter_append le0 le_add_same_cancel1 length_append)
lemma filter_double :
assumes "x ∈ set (filter P1 xs)"
and "P2 x"
shows "x ∈ set (filter P2 (filter P1 xs))"
by (metis (no_types) assms(1) assms(2) filter_set member_filter)
lemma filter_list_set :
assumes "x ∈ set xs"
and "P x"
shows "x ∈ set (filter P xs)"
by (simp add: assms(1) assms(2))
lemma filter_list_set_not_contained :
assumes "x ∈ set xs"
and "¬ P x"
shows "x ∉ set (filter P xs)"
by (simp add: assms(1) assms(2))
lemma filter_map_elem : "t ∈ set (map g (filter f xs)) ⟹ ∃ x ∈ set xs . f x ∧ t = g x"
by auto
subsubsection ‹Utility Lemmata for @{text "concat"}›
lemma concat_map_elem :
assumes "y ∈ set (concat (map f xs))"
obtains x where "x ∈ set xs"
and "y ∈ set (f x)"
using assms proof (induction xs)
case Nil
then show ?case by auto
next
case (Cons a xs)
then show ?case
proof (cases "y ∈ set (f a)")
case True
then show ?thesis
using Cons.prems(1) by auto
next
case False
then have "y ∈ set (concat (map f xs))"
using Cons by auto
have "∃ x . x ∈ set xs ∧ y ∈ set (f x)"
proof (rule ccontr)
assume "¬(∃x. x ∈ set xs ∧ y ∈ set (f x))"
then have "¬(y ∈ set (concat (map f xs)))"
by auto
then show False
using ‹y ∈ set (concat (map f xs))› by auto
qed
then show ?thesis
using Cons.prems(1) by auto
qed
qed
lemma set_concat_map_sublist :
assumes "x ∈ set (concat (map f xs))"
and "set xs ⊆ set xs'"
shows "x ∈ set (concat (map f xs'))"
using assms by (induction xs) (auto)
lemma set_concat_map_elem :
assumes "x ∈ set (concat (map f xs))"
shows "∃ x' ∈ set xs . x ∈ set (f x')"
using assms by auto
lemma concat_replicate_length : "length (concat (replicate n xs)) = n * (length xs)"
by (induction n; simp)
subsection ‹Enumerating Lists›
fun lists_of_length :: "'a list ⇒ nat ⇒ 'a list list" where
"lists_of_length T 0 = [[]]" |
"lists_of_length T (Suc n) = concat (map (λ xs . map (λ x . x#xs) T ) (lists_of_length T n))"
lemma lists_of_length_containment :
assumes "set xs ⊆ set T"
and "length xs = n"
shows "xs ∈ set (lists_of_length T n)"
using assms proof (induction xs arbitrary: n)
case Nil
then show ?case by auto
next
case (Cons a xs)
then obtain k where "n = Suc k"
by auto
then have "xs ∈ set (lists_of_length T k)"
using Cons by auto
moreover have "a ∈ set T"
using Cons by auto
ultimately show ?case
using ‹n = Suc k› by auto
qed
lemma lists_of_length_length :
assumes "xs ∈ set (lists_of_length T n)"
shows "length xs = n"
proof -
have "∀ xs ∈ set (lists_of_length T n) . length xs = n"
by (induction n; simp)
then show ?thesis using assms by blast
qed
lemma lists_of_length_elems :
assumes "xs ∈ set (lists_of_length T n)"
shows "set xs ⊆ set T"
proof -
have "∀ xs ∈ set (lists_of_length T n) . set xs ⊆ set T"
by (induction n; simp)
then show ?thesis using assms by blast
qed
lemma lists_of_length_list_set :
"set (lists_of_length xs k) = {xs' . length xs' = k ∧ set xs' ⊆ set xs}"
using lists_of_length_containment[of _ xs k]
lists_of_length_length[of _ xs k]
lists_of_length_elems[of _ xs k]
by blast
subsubsection ‹Enumerating List Subsets›
fun generate_selector_lists :: "nat ⇒ bool list list" where
"generate_selector_lists k = lists_of_length [False,True] k"
lemma generate_selector_lists_set :
"set (generate_selector_lists k) = {(bs :: bool list) . length bs = k}"
using lists_of_length_list_set by auto
lemma selector_list_index_set:
assumes "length ms = length bs"
shows "set (map fst (filter snd (zip ms bs))) = { ms ! i | i . i < length bs ∧ bs ! i}"
using assms proof (induction bs arbitrary: ms rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc b bs)
let ?ms = "butlast ms"
let ?m = "last ms"
have "length ?ms = length bs" using snoc.prems by auto
have "map fst (filter snd (zip ms (bs @ [b])))
= (map fst (filter snd (zip ?ms bs))) @ (map fst (filter snd (zip [?m] [b])))"
by (metis ‹length (butlast ms) = length bs› append_eq_conv_conj filter_append length_0_conv
map_append snoc.prems snoc_eq_iff_butlast zip_append2)
then have *: "set (map fst (filter snd (zip ms (bs @ [b]))))
= set (map fst (filter snd (zip ?ms bs))) ∪ set (map fst (filter snd (zip [?m] [b])))"
by simp
have "{ms ! i |i. i < length (bs @ [b]) ∧ (bs @ [b]) ! i}
= {ms ! i |i. i ≤ (length bs) ∧ (bs @ [b]) ! i}"
by auto
moreover have "{ms ! i |i. i ≤ (length bs) ∧ (bs @ [b]) ! i}
= {ms ! i |i. i < length bs ∧ (bs @ [b]) ! i}
∪ {ms ! i |i. i = length bs ∧ (bs @ [b]) ! i}"
by fastforce
moreover have "{ms ! i |i. i < length bs ∧ (bs @ [b]) ! i} = {?ms ! i |i. i < length bs ∧ bs ! i}"
using ‹length ?ms = length bs› by (metis butlast_snoc nth_butlast)
ultimately have **: "{ms ! i |i. i < length (bs @ [b]) ∧ (bs @ [b]) ! i}
= {?ms ! i |i. i < length bs ∧ bs ! i}
∪ {ms ! i |i. i = length bs ∧ (bs @ [b]) ! i}"
by simp
have "set (map fst (filter snd (zip [?m] [b]))) = {ms ! i |i. i = length bs ∧ (bs @ [b]) ! i}"
proof (cases b)
case True
then have "set (map fst (filter snd (zip [?m] [b]))) = {?m}" by fastforce
moreover have "{ms ! i |i. i = length bs ∧ (bs @ [b]) ! i} = {?m}"
proof -
have "(bs @ [b]) ! length bs"
by (simp add: True)
moreover have "ms ! length bs = ?m"
by (metis last_conv_nth length_0_conv length_butlast snoc.prems snoc_eq_iff_butlast)
ultimately show ?thesis by fastforce
qed
ultimately show ?thesis by auto
next
case False
then show ?thesis by auto
qed
then have "set (map fst (filter snd (zip (butlast ms) bs)))
∪ set (map fst (filter snd (zip [?m] [b])))
= {butlast ms ! i |i. i < length bs ∧ bs ! i}
∪ {ms ! i |i. i = length bs ∧ (bs @ [b]) ! i}"
using snoc.IH[OF ‹length ?ms = length bs›] by blast
then show ?case using * **
by simp
qed
lemma selector_list_ex :
assumes "set xs ⊆ set ms"
shows "∃ bs . length bs = length ms ∧ set xs = set (map fst (filter snd (zip ms bs)))"
using assms proof (induction xs rule: rev_induct)
case Nil
let ?bs = "replicate (length ms) False"
have "set [] = set (map fst (filter snd (zip ms ?bs)))"
by (metis filter_False in_set_zip length_replicate list.simps(8) nth_replicate)
moreover have "length ?bs = length ms" by auto
ultimately show ?case by blast
next
case (snoc a xs)
then have "set xs ⊆ set ms" and "a ∈ set ms" by auto
then obtain bs where "length bs = length ms" and "set xs = set (map fst (filter snd (zip ms bs)))"
using snoc.IH by auto
from ‹a ∈ set ms› obtain i where "i < length ms" and "ms ! i = a"
by (meson in_set_conv_nth)
let ?bs = "list_update bs i True"
have "length ms = length ?bs" using ‹length bs = length ms› by auto
have "length ?bs = length bs" by auto
have "set (map fst (filter snd (zip ms ?bs))) = {ms ! i |i. i < length ?bs ∧ ?bs ! i}"
using selector_list_index_set[OF ‹length ms = length ?bs›] by assumption
have "⋀ j . j < length ?bs ⟹ j ≠ i ⟹ ?bs ! j = bs ! j"
by auto
then have "{ms ! j |j. j < length bs ∧ j ≠ i ∧ bs ! j}
= {ms ! j |j. j < length ?bs ∧ j ≠ i ∧ ?bs ! j}"
using ‹length ?bs = length bs› by fastforce
have "{ms ! j |j. j < length ?bs ∧ j = i ∧ ?bs ! j} = {a}"
using ‹length bs = length ms› ‹i < length ms› ‹ms ! i = a› by auto
then have "{ms ! i |i. i < length ?bs ∧ ?bs ! i}
= insert a {ms ! j |j. j < length ?bs ∧ j ≠ i ∧ ?bs ! j}"
by fastforce
have "{ms ! j |j. j < length bs ∧ j = i ∧ bs ! j} ⊆ {ms ! j |j. j < length ?bs ∧ j = i ∧ ?bs ! j}"
by (simp add: Collect_mono)
then have "{ms ! j |j. j < length bs ∧ j = i ∧ bs ! j} ⊆ {a}"
using ‹{ms ! j |j. j < length ?bs ∧ j = i ∧ ?bs ! j} = {a}›
by auto
moreover have "{ms ! j |j. j < length bs ∧ bs ! j}
= {ms ! j |j. j < length bs ∧ j = i ∧ bs ! j}
∪ {ms ! j |j. j < length bs ∧ j ≠ i ∧ bs ! j}"
by fastforce
ultimately have "{ms ! i |i. i < length ?bs ∧ ?bs ! i}
= insert a {ms ! i |i. i < length bs ∧ bs ! i}"
using ‹{ms ! j |j. j < length bs ∧ j ≠ i ∧ bs ! j}
= {ms ! j |j. j < length ?bs ∧ j ≠ i ∧ ?bs ! j}›
using ‹{ms ! ia |ia. ia < length (bs[i := True])
∧ bs[i := True] ! ia}
= insert a {ms ! j |j. j < length (bs[i := True])
∧ j ≠ i ∧ bs[i := True] ! j}›
by auto
moreover have "set (map fst (filter snd (zip ms bs))) = {ms ! i |i. i < length bs ∧ bs ! i}"
using selector_list_index_set[of ms bs] ‹length bs = length ms› by auto
ultimately have "set (a#xs) = set (map fst (filter snd (zip ms ?bs)))"
using ‹set (map fst (filter snd (zip ms ?bs))) = {ms ! i |i. i < length ?bs ∧ ?bs ! i}›
‹set xs = set (map fst (filter snd (zip ms bs)))›
by auto
then show ?case
using ‹length ms = length ?bs›
by (metis Un_commute insert_def list.set(1) list.simps(15) set_append singleton_conv)
qed
subsubsection ‹Enumerating Choices from Lists of Lists›
fun generate_choices :: "('a × ('b list)) list ⇒ ('a × 'b option) list list" where
"generate_choices [] = [[]]" |
"generate_choices (xys#xyss) =
concat (map (λ xy' . map (λ xys' . xy' # xys') (generate_choices xyss))
((fst xys, None) # (map (λ y . (fst xys, Some y)) (snd xys))))"
lemma concat_map_hd_tl_elem:
assumes "hd cs ∈ set P1"
and "tl cs ∈ set P2"
and "length cs > 0"
shows "cs ∈ set (concat (map (λ xy' . map (λ xys' . xy' # xys') P2) P1))"
proof -
have "hd cs # tl cs = cs" using assms(3) by auto
moreover have "hd cs # tl cs ∈ set (concat (map (λ xy' . map (λ xys' . xy' # xys') P2) P1))"
using assms(1,2) by auto
ultimately show ?thesis
by auto
qed
lemma generate_choices_hd_tl :
"cs ∈ set (generate_choices (xys#xyss))
= (length cs = length (xys#xyss)
∧ fst (hd cs) = fst xys
∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys))))
∧ (tl cs ∈ set (generate_choices xyss)))"
proof (induction xyss arbitrary: cs xys)
case Nil
have "(cs ∈ set (generate_choices [xys]))
= (cs ∈ set ([(fst xys, None)] # map (λy. [(fst xys, Some y)]) (snd xys)))"
unfolding generate_choices.simps by auto
moreover have "(cs ∈ set ([(fst xys, None)] # map (λy. [(fst xys, Some y)]) (snd xys)))
⟹ (length cs = length [xys] ∧
fst (hd cs) = fst xys ∧
(snd (hd cs) = None ∨ snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)) ∧
tl cs ∈ set (generate_choices []))"
by auto
moreover have "(length cs = length [xys] ∧
fst (hd cs) = fst xys ∧
(snd (hd cs) = None ∨ snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)) ∧
tl cs ∈ set (generate_choices []))
⟹ (cs ∈ set ([(fst xys, None)] # map (λy. [(fst xys, Some y)]) (snd xys)))"
unfolding generate_choices.simps(1)
proof -
assume a1: "length cs = length [xys]
∧ fst (hd cs) = fst xys
∧ (snd (hd cs) = None ∨ snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys))
∧ tl cs ∈ set [[]]"
have f2: "∀ps. ps = [] ∨ ps = (hd ps::'a × 'b option) # tl ps"
by (meson list.exhaust_sel)
have f3: "cs ≠ []"
using a1 by fastforce
have "snd (hd cs) = None ⟶ (fst xys, None) = hd cs"
using a1 by (metis prod.exhaust_sel)
moreover
{ assume "hd cs # tl cs ≠ [(fst xys, Some (the (snd (hd cs))))]"
then have "snd (hd cs) = None"
using a1 by (metis (no_types) length_0_conv length_tl list.sel(3)
option.collapse prod.exhaust_sel) }
ultimately have "cs ∈ insert [(fst xys, None)] ((λb. [(fst xys, Some b)]) ` set (snd xys))"
using f3 f2 a1 by fastforce
then show ?thesis
by simp
qed
ultimately show ?case by blast
next
case (Cons a xyss)
have "length cs = length (xys#a#xyss)
⟹ fst (hd cs) = fst xys
⟹ (snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)))
⟹ (tl cs ∈ set (generate_choices (a#xyss)))
⟹ cs ∈ set (generate_choices (xys#a#xyss))"
proof -
assume "length cs = length (xys#a#xyss)"
and "fst (hd cs) = fst xys"
and "(snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)))"
and "(tl cs ∈ set (generate_choices (a#xyss)))"
then have "length cs > 0" by auto
have "(hd cs) ∈ set ((fst xys, None) # (map (λ y . (fst xys, Some y)) (snd xys)))"
using ‹fst (hd cs) = fst xys›
‹(snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)))›
by (metis (no_types, lifting) image_eqI list.set_intros(1) list.set_intros(2)
option.collapse prod.collapse set_map)
show "cs ∈ set (generate_choices ((xys#(a#xyss))))"
using generate_choices.simps(2)[of xys "a#xyss"]
concat_map_hd_tl_elem[OF ‹(hd cs) ∈ set ((fst xys, None) # (map (λ y . (fst xys, Some y)) (snd xys)))›
‹(tl cs ∈ set (generate_choices (a#xyss)))›
‹length cs > 0›]
by auto
qed
moreover have "cs ∈ set (generate_choices (xys#a#xyss))
⟹ length cs = length (xys#a#xyss)
∧ fst (hd cs) = fst xys
∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None
∧ the (snd (hd cs)) ∈ set (snd xys))))
∧ (tl cs ∈ set (generate_choices (a#xyss)))"
proof -
assume "cs ∈ set (generate_choices (xys#a#xyss))"
then have p3: "tl cs ∈ set (generate_choices (a#xyss))"
using generate_choices.simps(2)[of xys "a#xyss"] by fastforce
then have "length (tl cs) = length (a # xyss)" using Cons.IH[of "tl cs" "a"] by simp
then have p1: "length cs = length (xys#a#xyss)" by auto
have p2 : "fst (hd cs) = fst xys ∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None
∧ the (snd (hd cs)) ∈ set (snd xys))))"
using ‹cs ∈ set (generate_choices (xys#a#xyss))› generate_choices.simps(2)[of xys "a#xyss"]
by fastforce
show ?thesis using p1 p2 p3 by simp
qed
ultimately show ?case by blast
qed
lemma list_append_idx_prop :
"(∀ i . (i < length xs ⟶ P (xs ! i)))
= (∀ j . ((j < length (ys@xs) ∧ j ≥ length ys) ⟶ P ((ys@xs) ! j)))"
proof -
have "⋀ j . ∀i<length xs. P (xs ! i) ⟹ j < length (ys @ xs)
⟹ length ys ≤ j ⟶ P ((ys @ xs) ! j)"
by (simp add: nth_append)
moreover have "⋀ i . (∀ j . ((j < length (ys@xs) ∧ j ≥ length ys) ⟶ P ((ys@xs) ! j)))
⟹ i < length xs ⟹ P (xs ! i)"
proof -
fix i assume "(∀ j . ((j < length (ys@xs) ∧ j ≥ length ys) ⟶ P ((ys@xs) ! j)))"
and "i < length xs"
then have "P ((ys@xs) ! (length ys + i))"
by (metis add_strict_left_mono le_add1 length_append)
moreover have "P (xs ! i) = P ((ys@xs) ! (length ys + i))"
by simp
ultimately show "P (xs ! i)" by blast
qed
ultimately show ?thesis by blast
qed
lemma list_append_idx_prop2 :
assumes "length xs' = length xs"
and "length ys' = length ys"
shows "(∀ i . (i < length xs ⟶ P (xs ! i) (xs' ! i)))
= (∀ j . ((j < length (ys@xs) ∧ j ≥ length ys) ⟶ P ((ys@xs) ! j) ((ys'@xs') ! j)))"
proof -
have "∀i<length xs. P (xs ! i) (xs' ! i) ⟹
∀j. j < length (ys @ xs) ∧ length ys ≤ j ⟶ P ((ys @ xs) ! j) ((ys' @ xs') ! j)"
using assms
proof -
assume a1: "∀i<length xs. P (xs ! i) (xs' ! i)"
{ fix nn :: nat
have ff1: "∀n na. (na::nat) + n - n = na"
by simp
have ff2: "∀n na. (na::nat) ≤ n + na"
by auto
then have ff3: "∀as n. (ys' @ as) ! n = as ! (n - length ys) ∨ ¬ length ys ≤ n"
using ff1 by (metis (no_types) add.commute assms(2) eq_diff_iff nth_append_length_plus)
have ff4: "∀n bs bsa. ((bsa @ bs) ! n::'b) = bs ! (n - length bsa) ∨ ¬ length bsa ≤ n"
using ff2 ff1 by (metis (no_types) add.commute eq_diff_iff nth_append_length_plus)
have "∀n na nb. ((n::nat) + nb ≤ na ∨ ¬ n ≤ na - nb) ∨ ¬ nb ≤ na"
using ff2 ff1 by (metis le_diff_iff)
then have "(¬ nn < length (ys @ xs) ∨ ¬ length ys ≤ nn)
∨ P ((ys @ xs) ! nn) ((ys' @ xs') ! nn)"
using ff4 ff3 a1 by (metis add.commute length_append not_le) }
then show ?thesis
by blast
qed
moreover have "(∀j. j < length (ys @ xs) ∧ length ys ≤ j ⟶ P ((ys @ xs) ! j) ((ys' @ xs') ! j))
⟹ ∀i<length xs. P (xs ! i) (xs' ! i)"
using assms
by (metis le_add1 length_append nat_add_left_cancel_less nth_append_length_plus)
ultimately show ?thesis by blast
qed
lemma generate_choices_idx :
"cs ∈ set (generate_choices xyss)
= (length cs = length xyss
∧ (∀ i < length cs . (fst (cs ! i)) = (fst (xyss ! i))
∧ ((snd (cs ! i)) = None
∨ ((snd (cs ! i)) ≠ None ∧ the (snd (cs ! i)) ∈ set (snd (xyss ! i))))))"
proof (induction xyss arbitrary: cs)
case Nil
then show ?case by auto
next
case (Cons xys xyss)
have "cs ∈ set (generate_choices (xys#xyss))
= (length cs = length (xys#xyss)
∧ fst (hd cs) = fst xys
∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys))))
∧ (tl cs ∈ set (generate_choices xyss)))"
using generate_choices_hd_tl by metis
then have "cs ∈ set (generate_choices (xys#xyss))
= (length cs = length (xys#xyss)
∧ fst (hd cs) = fst xys
∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys))))
∧ (length (tl cs) = length xyss ∧
(∀i<length (tl cs).
fst (tl cs ! i) = fst (xyss ! i) ∧
(snd (tl cs ! i) = None
∨ snd (tl cs ! i) ≠ None ∧ the (snd (tl cs ! i)) ∈ set (snd (xyss ! i))))))"
using Cons.IH[of "tl cs"] by blast
then have *: "cs ∈ set (generate_choices (xys#xyss))
= (length cs = length (xys#xyss)
∧ fst (hd cs) = fst xys
∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys))))
∧ (∀i<length (tl cs).
fst (tl cs ! i) = fst (xyss ! i) ∧
(snd (tl cs ! i) = None
∨ snd (tl cs ! i) ≠ None ∧ the (snd (tl cs ! i)) ∈ set (snd (xyss ! i)))))"
by auto
have "cs ∈ set (generate_choices (xys#xyss)) ⟹ (length cs = length (xys # xyss) ∧
(∀i<length cs.
fst (cs ! i) = fst ((xys # xyss) ! i) ∧
(snd (cs ! i) = None ∨
snd (cs ! i) ≠ None ∧ the (snd (cs ! i)) ∈ set (snd ((xys # xyss) ! i)))))"
proof -
assume "cs ∈ set (generate_choices (xys#xyss))"
then have p1: "length cs = length (xys#xyss)"
and p2: "fst (hd cs) = fst xys "
and p3: "((snd (hd cs) = None
∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys))))"
and p4: "(∀i<length (tl cs).
fst (tl cs ! i) = fst (xyss ! i) ∧
(snd (tl cs ! i) = None
∨ snd (tl cs ! i) ≠ None ∧ the (snd (tl cs ! i)) ∈ set (snd (xyss ! i))))"
using * by blast+
then have "length xyss = length (tl cs)" and "length (xys # xyss) = length ([hd cs] @ tl cs)"
by auto
have "[hd cs]@(tl cs) = cs"
by (metis (no_types) p1 append.left_neutral append_Cons length_greater_0_conv
list.collapse list.simps(3))
then have p4b: "(∀i<length cs. i > 0 ⟶
(fst (cs ! i) = fst ((xys#xyss) ! i) ∧
(snd (cs ! i) = None
∨ snd (cs ! i) ≠ None ∧ the (snd (cs ! i)) ∈ set (snd ((xys#xyss) ! i)))))"
using p4 list_append_idx_prop2[of xyss "tl cs" "xys#xyss" "[hd cs]@(tl cs)"
"λ x y . fst x = fst y
∧ (snd x = None
∨ snd x ≠ None ∧ the (snd x) ∈ set (snd y))",
OF ‹length xyss = length (tl cs)›
‹length (xys # xyss) = length ([hd cs] @ tl cs)›]
by (metis (no_types, lifting) One_nat_def Suc_pred
‹length (xys # xyss) = length ([hd cs] @ tl cs)› ‹length xyss = length (tl cs)›
length_Cons list.size(3) not_less_eq nth_Cons_pos nth_append)
have p4a :"(fst (cs ! 0) = fst ((xys#xyss) ! 0) ∧ (snd (cs ! 0) = None
∨ snd (cs ! 0) ≠ None ∧ the (snd (cs ! 0)) ∈ set (snd ((xys#xyss) ! 0))))"
using p1 p2 p3 by (metis hd_conv_nth length_greater_0_conv list.simps(3) nth_Cons_0)
show ?thesis using p1 p4a p4b by fastforce
qed
moreover have "(length cs = length (xys # xyss) ∧
(∀i<length cs.
fst (cs ! i) = fst ((xys # xyss) ! i) ∧
(snd (cs ! i) = None ∨
snd (cs ! i) ≠ None ∧ the (snd (cs ! i)) ∈ set (snd ((xys # xyss) ! i)))))
⟹ cs ∈ set (generate_choices (xys#xyss))"
using *
by (metis (no_types, lifting) Nitpick.size_list_simp(2) Suc_mono hd_conv_nth
length_greater_0_conv length_tl list.sel(3) list.simps(3) nth_Cons_0 nth_tl)
ultimately show ?case by blast
qed
subsection ‹Finding the Index of the First Element of a List Satisfying a Property›
fun find_index :: "('a ⇒ bool) ⇒ 'a list ⇒ nat option" where
"find_index f [] = None" |
"find_index f (x#xs) = (if f x
then Some 0
else (case find_index f xs of Some k ⇒ Some (Suc k) | None ⇒ None))"
lemma find_index_index :
assumes "find_index f xs = Some k"
shows "k < length xs" and "f (xs ! k)" and "⋀ j . j < k ⟹ ¬ f (xs ! j)"
proof -
have "(k < length xs) ∧ (f (xs ! k)) ∧ (∀ j < k . ¬ (f (xs ! j)))"
using assms proof (induction xs arbitrary: k)
case Nil
then show ?case by auto
next
case (Cons x xs)
show ?case proof (cases "f x")
case True
then show ?thesis using Cons.prems by auto
next
case False
then have "find_index f (x#xs)
= (case find_index f xs of Some k ⇒ Some (Suc k) | None ⇒ None)"
by auto
then have "(case find_index f xs of Some k ⇒ Some (Suc k) | None ⇒ None) = Some k"
using Cons.prems by auto
then obtain k' where "find_index f xs = Some k'" and "k = Suc k'"
by (metis option.case_eq_if option.collapse option.distinct(1) option.sel)
have "k < length (x # xs) ∧ f ((x # xs) ! k)"
using Cons.IH[OF ‹find_index f xs = Some k'›] ‹k = Suc k'›
by auto
moreover have "(∀j<k. ¬ f ((x # xs) ! j))"
using Cons.IH[OF ‹find_index f xs = Some k'›] ‹k = Suc k'› False less_Suc_eq_0_disj
by auto
ultimately show ?thesis by presburger
qed
qed
then show "k < length xs" and "f (xs ! k)" and "⋀ j . j < k ⟹ ¬ f (xs ! j)" by simp+
qed
lemma find_index_exhaustive :
assumes "∃ x ∈ set xs . f x"
shows "find_index f xs ≠ None"
using assms proof (induction xs)
case Nil
then show ?case by auto
next
case (Cons x xs)
then show ?case by (cases "f x"; auto)
qed
subsection ‹List Distinctness from Sorting›
lemma non_distinct_repetition_indices :
assumes "¬ distinct xs"
shows "∃ i j . i < j ∧ j < length xs ∧ xs ! i = xs ! j"
by (metis assms distinct_conv_nth le_neq_implies_less not_le)
lemma non_distinct_repetition_indices_rev :
assumes "i < j" and "j < length xs" and "xs ! i = xs ! j"
shows "¬ distinct xs"
using assms nth_eq_iff_index_eq by fastforce
lemma ordered_list_distinct :
fixes xs :: "('a::preorder) list"
assumes "⋀ i . Suc i < length xs ⟹ (xs ! i) < (xs ! (Suc i))"
shows "distinct xs"
proof -
have "⋀ i j . i < j ⟹ j < length xs ⟹ (xs ! i) < (xs ! j)"
proof -
fix i j assume "i < j" and "j < length xs"
then show "xs ! i < xs ! j"
using assms proof (induction xs arbitrary: i j rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc a xs)
show ?case proof (cases "j < length xs")
case True
show ?thesis using snoc.IH[OF snoc.prems(1) True] snoc.prems(3)
proof -
have f1: "i < length xs"
using True less_trans snoc.prems(1) by blast
have f2: "∀is isa n. if n < length is then (is @ isa) ! n
= (is ! n::integer) else (is @ isa) ! n = isa ! (n - length is)"
by (meson nth_append)
then have f3: "(xs @ [a]) ! i = xs ! i"
using f1
by (simp add: nth_append)
have "xs ! i < xs ! j"
using f2
by (metis Suc_lessD ‹(⋀i. Suc i < length xs ⟹ xs ! i < xs ! Suc i) ⟹ xs ! i < xs ! j›
butlast_snoc length_append_singleton less_SucI nth_butlast snoc.prems(3))
then show ?thesis
using f3 f2 True
by (simp add: nth_append)
qed
next
case False
then have "(xs @ [a]) ! j = a"
using snoc.prems(2)
by (metis length_append_singleton less_SucE nth_append_length)
consider "j = 1" | "j > 1"
using ‹i < j›
by linarith
then show ?thesis proof cases
case 1
then have "i = 0" and "j = Suc i" using ‹i < j› by linarith+
then show ?thesis
using snoc.prems(3)
using snoc.prems(2) by blast
next
case 2
then consider "i < j - 1" | "i = j - 1" using ‹i < j› by linarith+
then show ?thesis proof cases
case 1
have "(⋀i. Suc i < length xs ⟹ xs ! i < xs ! Suc i) ⟹ xs ! i < xs ! (j - 1)"
using snoc.IH[OF 1] snoc.prems(2) 2 by simp
then have le1: "(xs @ [a]) ! i < (xs @ [a]) ! (j -1)"
using snoc.prems(2)
by (metis "2" False One_nat_def Suc_diff_Suc Suc_lessD diff_zero snoc.prems(3)
length_append_singleton less_SucE not_less_eq nth_append snoc.prems(1))
moreover have le2: "(xs @ [a]) ! (j -1) < (xs @ [a]) ! j"
using snoc.prems(2,3) 2 less_trans
by (metis (full_types) One_nat_def Suc_diff_Suc diff_zero less_numeral_extra(1))
ultimately show ?thesis
using less_trans by blast
next
case 2
then have "j = Suc i" using ‹1 < j› by linarith
then show ?thesis
using snoc.prems(3)
using snoc.prems(2) by blast
qed
qed
qed
qed
qed
then show ?thesis
by (metis less_asym non_distinct_repetition_indices)
qed
lemma ordered_list_distinct_rev :
fixes xs :: "('a::preorder) list"
assumes "⋀ i . Suc i < length xs ⟹ (xs ! i) > (xs ! (Suc i))"
shows "distinct xs"
proof -
have "⋀ i . Suc i < length (rev xs) ⟹ ((rev xs) ! i) < ((rev xs) ! (Suc i))"
using assms
proof -
fix i :: nat
assume a1: "Suc i < length (rev xs)"
obtain nn :: "nat ⇒ nat ⇒ nat" where
"∀x0 x1. (∃v2. x1 = Suc v2 ∧ v2 < x0) = (x1 = Suc (nn x0 x1) ∧ nn x0 x1 < x0)"
by moura
then have f2: "∀n na. (¬ n < Suc na ∨ n = 0 ∨ n = Suc (nn na n) ∧ nn na n < na)
∧ (n < Suc na ∨ n ≠ 0 ∧ (∀nb. n ≠ Suc nb ∨ ¬ nb < na))"
by (meson less_Suc_eq_0_disj)
have f3: "Suc (length xs - Suc (Suc i)) = length (rev xs) - Suc i"
using a1 by (simp add: Suc_diff_Suc)
have "i < length (rev xs)"
using a1 by (meson Suc_lessD)
then have "i < length xs"
by simp
then show "rev xs ! i < rev xs ! Suc i"
using f3 f2 a1 by (metis (no_types) assms diff_less length_rev not_less_iff_gr_or_eq rev_nth)
qed
then have "distinct (rev xs)"
using ordered_list_distinct[of "rev xs"] by blast
then show ?thesis by auto
qed
subsection ‹Calculating Prefixes and Suffixes›
fun suffixes :: "'a list ⇒ 'a list list" where
"suffixes [] = [[]]" |
"suffixes (x#xs) = (suffixes xs) @ [x#xs]"
lemma suffixes_set :
"set (suffixes xs) = {zs . ∃ ys . ys@zs = xs}"
proof (induction xs)
case Nil
then show ?case by auto
next
case (Cons x xs)
then have *: "set (suffixes (x#xs)) = {zs . ∃ ys . ys@zs = xs} ∪ {x#xs}"
by auto
have "{zs . ∃ ys . ys@zs = xs} = {zs . ∃ ys . x#ys@zs = x#xs}"
by force
then have "{zs . ∃ ys . ys@zs = xs} = {zs . ∃ ys . ys@zs = x#xs ∧ ys ≠ []}"
by (metis Cons_eq_append_conv list.distinct(1))
moreover have "{x#xs} = {zs . ∃ ys . ys@zs = x#xs ∧ ys = []}"
by force
ultimately show ?case using * by force
qed
lemma prefixes_set : "set (prefixes xs) = {xs' . ∃ xs'' . xs'@xs'' = xs}"
proof (induction xs)
case Nil
then show ?case by auto
next
case (Cons x xs)
moreover have "prefixes (x#xs) = [] # map ((#) x) (prefixes xs)"
by auto
ultimately have *: "set (prefixes (x#xs)) = insert [] (((#) x) ` {xs'. ∃xs''. xs' @ xs'' = xs})"
by auto
also have "… = {xs' . ∃ xs'' . xs'@xs'' = (x#xs)}"
proof
show "insert [] ((#) x ` {xs'. ∃xs''. xs' @ xs'' = xs}) ⊆ {xs'. ∃xs''. xs' @ xs'' = x # xs}"
by auto
show "{xs'. ∃xs''. xs' @ xs'' = x # xs} ⊆ insert [] ((#) x ` {xs'. ∃xs''. xs' @ xs'' = xs})"
proof
fix y assume "y ∈ {xs'. ∃xs''. xs' @ xs'' = x # xs}"
then obtain y' where "y@y' = x # xs"
by blast
then show "y ∈ insert [] ((#) x ` {xs'. ∃xs''. xs' @ xs'' = xs})"
by (cases y; auto)
qed
qed
finally show ?case .
qed
fun is_prefix :: "'a list ⇒ 'a list ⇒ bool" where
"is_prefix [] _ = True" |
"is_prefix (x#xs) [] = False" |
"is_prefix (x#xs) (y#ys) = (x = y ∧ is_prefix xs ys)"
lemma is_prefix_prefix : "is_prefix xs ys = (∃ xs' . ys = xs@xs')"
proof (induction xs arbitrary: ys)
case Nil
then show ?case by auto
next
case (Cons x xs)
show ?case proof (cases "is_prefix (x#xs) ys")
case True
then show ?thesis using Cons.IH
by (metis append_Cons is_prefix.simps(2) is_prefix.simps(3) neq_Nil_conv)
next
case False
then show ?thesis
using Cons.IH by auto
qed
qed
fun add_prefixes :: "'a list list ⇒ 'a list list" where
"add_prefixes xs = concat (map prefixes xs)"
lemma add_prefixes_set : "set (add_prefixes xs) = {xs' . ∃ xs'' . xs'@xs'' ∈ set xs}"
proof -
have "set (add_prefixes xs) = {xs' . ∃ x ∈ set xs . xs' ∈ set (prefixes x)}"
unfolding add_prefixes.simps by auto
also have "… = {xs' . ∃ xs'' . xs'@xs'' ∈ set xs}"
proof (induction xs)
case Nil
then show ?case using prefixes_set by auto
next
case (Cons a xs)
then show ?case
proof -
have "⋀ xs' . xs' ∈ {xs'. ∃x∈set (a # xs). xs' ∈ set (prefixes x)}
⟷ xs' ∈ {xs'. ∃xs''. xs' @ xs'' ∈ set (a # xs)}"
proof -
fix xs'
show "xs' ∈ {xs'. ∃x∈set (a # xs). xs' ∈ set (prefixes x)}
⟷ xs' ∈ {xs'. ∃xs''. xs' @ xs'' ∈ set (a # xs)}"
unfolding prefixes_set by force
qed
then show ?thesis by blast
qed
qed
finally show ?thesis by blast
qed
lemma prefixes_set_ob :
assumes "xs ∈ set (prefixes xss)"
obtains xs' where "xss = xs@xs'"
using assms unfolding prefixes_set
by auto
lemma prefixes_finite : "finite { x ∈ set (prefixes xs) . P x}"
by (metis Collect_mem_eq List.finite_set finite_Collect_conjI)
lemma prefixes_set_Cons_insert: "set (prefixes (w' @ [xy])) = Set.insert (w'@[xy]) (set (prefixes (w')))"
unfolding prefixes_set
proof (induction w' arbitrary: xy rule: rev_induct)
case Nil
then show ?case
by (auto; simp add: append_eq_Cons_conv)
next
case (snoc x xs)
then show ?case
by (auto; metis (no_types, opaque_lifting) butlast.simps(2) butlast_append butlast_snoc)
qed
lemma prefixes_set_subset:
"set (prefixes xs) ⊆ set (prefixes (xs@ys))"
unfolding prefixes_set by auto
lemma prefixes_prefix_subset :
assumes "xs ∈ set (prefixes ys)"
shows "set (prefixes xs) ⊆ set (prefixes ys)"
using assms unfolding prefixes_set by auto
lemma prefixes_butlast_is_prefix :
"butlast xs ∈ set (prefixes xs)"
unfolding prefixes_set
by (metis (mono_tags, lifting) append_butlast_last_id butlast.simps(1) mem_Collect_eq self_append_conv2)
lemma prefixes_take_iff :
"xs ∈ set (prefixes ys) ⟷ take (length xs) ys = xs"
proof
show "xs ∈ set (prefixes ys) ⟹ take (length xs) ys = xs"
unfolding prefixes_set
by (simp add: append_eq_conv_conj)
show "take (length xs) ys = xs ⟹ xs ∈ set (prefixes ys)"
unfolding prefixes_set
by (metis (mono_tags, lifting) append_take_drop_id mem_Collect_eq)
qed
lemma prefixes_set_Nil : "[] ∈ list.set (prefixes xs)"
by (metis append.left_neutral list.set_intros(1) prefixes.simps(1) prefixes_set_subset subset_iff)
lemma prefixes_prefixes :
assumes "ys ∈ list.set (prefixes xs)"
"zs ∈ list.set (prefixes xs)"
shows "ys ∈ list.set (prefixes zs) ∨ zs ∈ list.set (prefixes ys)"
proof (rule ccontr)
let ?ys = "take (length ys) zs"
let ?zs = "take (length zs) ys"
assume "¬ (ys ∈ list.set (prefixes zs) ∨ zs ∈ list.set (prefixes ys))"
then have "?ys ≠ ys" and "?zs ≠ zs"
using prefixes_take_iff by blast+
moreover have "?ys = ys ∨ ?zs = zs"
using assms
by (metis linear min.commute prefixes_take_iff take_all_iff take_take)
ultimately show False
by simp
qed
subsubsection ‹Pairs of Distinct Prefixes›
fun prefix_pairs :: "'a list ⇒ ('a list × 'a list) list"
where "prefix_pairs [] = []" |
"prefix_pairs xs = prefix_pairs (butlast xs) @ (map (λ ys. (ys,xs)) (butlast (prefixes xs)))"
lemma prefixes_butlast :
"set (butlast (prefixes xs)) = {ys . ∃ zs . ys@zs = xs ∧ zs ≠ []}"
proof (induction "length xs" arbitrary: xs)
case 0
then show ?case by auto
next
case (Suc k)
then obtain x xs' where "xs = x#xs'" and "k = length xs' "
by (metis length_Suc_conv)
then have "prefixes xs = [] # map ((#) x) (prefixes xs')"
by auto
then have "butlast (prefixes xs) = [] # map ((#) x) (butlast (prefixes xs'))"
by (simp add: map_butlast)
then have "set (butlast (prefixes xs)) = insert [] (((#) x) ` {ys . ∃ zs . ys@zs = xs' ∧ zs ≠ []})"
using Suc.hyps(1)[OF ‹k = length xs'›]
by auto
also have "… = {ys . ∃ zs . ys@zs = (x#xs') ∧ zs ≠ []}"
proof
show "insert [] ((#) x ` {ys. ∃zs. ys @ zs = xs' ∧ zs ≠ []}) ⊆ {ys. ∃zs. ys @ zs = x # xs' ∧ zs ≠ []}"
by auto
show "{ys. ∃zs. ys @ zs = x # xs' ∧ zs ≠ []} ⊆ insert [] ((#) x ` {ys. ∃zs. ys @ zs = xs' ∧ zs ≠ []})"
proof
fix ys assume "ys ∈ {ys. ∃zs. ys @ zs = x # xs' ∧ zs ≠ []}"
then show "ys ∈ insert [] ((#) x ` {ys. ∃zs. ys @ zs = xs' ∧ zs ≠ []})"
by (cases ys; auto)
qed
qed
finally show ?case
unfolding ‹xs = x#xs'› .
qed
lemma prefix_pairs_set :
"set (prefix_pairs xs) = {(zs,ys) | zs ys . ∃ xs1 xs2 . zs@xs1 = ys ∧ ys@xs2 = xs ∧ xs1 ≠ []}"
proof (induction xs rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc x xs)
have "prefix_pairs (xs @ [x]) = prefix_pairs (butlast (xs @ [x])) @ (map (λ ys. (ys,(xs @ [x]))) (butlast (prefixes (xs @ [x]))))"
by (cases "(xs @ [x])"; auto)
then have *: "prefix_pairs (xs @ [x]) = prefix_pairs xs @ (map (λ ys. (ys,(xs @ [x]))) (butlast (prefixes (xs @ [x]))))"
by auto
have "set (prefix_pairs xs) = {(zs, ys) |zs ys. ∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 = xs ∧ xs1 ≠ []}"
using snoc.IH by assumption
then have "set (prefix_pairs xs) = {(zs, ys) |zs ys. ∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 @ [x] = xs@[x] ∧ xs1 ≠ []}"
by auto
also have "... = {(zs, ys) |zs ys. ∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 = xs @[x] ∧ xs1 ≠ [] ∧ xs2 ≠ []}"
proof -
let ?P1 = "λ zs ys . (∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 @ [x] = xs@[x] ∧ xs1 ≠ [])"
let ?P2 = "λ zs ys . (∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 = xs @[x] ∧ xs1 ≠ [] ∧ xs2 ≠ [])"
have "⋀ ys zs . ?P2 zs ys ⟹ ?P1 zs ys"
by (metis append_assoc butlast_append butlast_snoc)
then have "⋀ ys zs . ?P1 ys zs = ?P2 ys zs"
by blast
then show ?thesis by force
qed
finally have "set (prefix_pairs xs) = {(zs, ys) |zs ys. ∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 = xs @ [x] ∧ xs1 ≠ [] ∧ xs2 ≠ []}"
by assumption
moreover have "set (map (λ ys. (ys,(xs @ [x]))) (butlast (prefixes (xs @ [x])))) = {(zs, ys) |zs ys. ∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 = xs @ [x] ∧ xs1 ≠ [] ∧ xs2 = []}"
using prefixes_butlast[of "xs@[x]"] by force
ultimately show ?case using * by force
qed
lemma prefix_pairs_set_alt :
"set (prefix_pairs xs) = {(xs1,xs1@xs2) | xs1 xs2 . xs2 ≠ [] ∧ (∃ xs3 . xs1@xs2@xs3 = xs)}"
unfolding prefix_pairs_set by auto
lemma prefixes_Cons :
assumes "(x#xs) ∈ set (prefixes (y#ys))"
shows "x = y" and "xs ∈ set (prefixes ys)"
proof -
show "x = y"
by (metis Cons_eq_appendI assms nth_Cons_0 prefixes_set_ob)
show "xs ∈ set (prefixes ys)"
proof -
obtain xs' xs'' where "(x#xs) = xs'" and "(y#ys) = xs'@xs''"
by (meson assms prefixes_set_ob)
then have "xs' = x#tl xs'"
by auto
then have "xs = tl xs'"
using ‹(x#xs) = xs'› by auto
moreover have "ys = (tl xs')@xs''"
using ‹(y#ys) = xs'@xs''› ‹xs' = x#tl xs'›
by (metis append_Cons list.inject)
ultimately show ?thesis
unfolding prefixes_set by blast
qed
qed
lemma prefixes_prepend :
assumes "xs' ∈ set (prefixes xs)"
shows "ys@xs' ∈ set (prefixes (ys@xs))"
proof -
obtain xs'' where "xs = xs'@xs''"
using assms
using prefixes_set_ob by auto
then have "(ys@xs) = (ys@xs')@xs''"
by auto
then show ?thesis
unfolding prefixes_set by auto
qed
lemma prefixes_prefix_suffix_ob :
assumes "a ∈ set (prefixes (b@c))"
and "a ∉ set (prefixes b)"
obtains c' c'' where "c = c'@c''"
and "a = b@c'"
and "c' ≠ []"
proof -
have "∃ c' c'' . c = c'@c'' ∧ a = b@c' ∧ c' ≠ []"
using assms
proof (induction b arbitrary: a)
case Nil
then show ?case
unfolding prefixes_set
by fastforce
next
case (Cons x xs)
show ?case proof (cases a)
case Nil
then show ?thesis
by (metis Cons.prems(2) list.size(3) prefixes_take_iff take_eq_Nil)
next
case (Cons a' as)
then have "a' # as ∈ set (prefixes (x #(xs@c)))"
using Cons.prems(1) by auto
have "a' = x" and "as ∈ set (prefixes (xs@c))"
using prefixes_Cons[OF ‹a' # as ∈ set (prefixes (x #(xs@c)))›]
by auto
moreover have "as ∉ set (prefixes xs)"
using ‹a ∉ set (prefixes (x # xs))› unfolding Cons ‹a' = x› prefixes_set by auto
ultimately obtain c' c'' where "c = c'@c''"
and "as = xs@c'"
and "c' ≠ []"
using Cons.IH by blast
then have "c = c'@c''" and "a = (x#xs)@c'" and "c' ≠ []"
unfolding Cons ‹a' = x› by auto
then show ?thesis
using that by blast
qed
qed
then show ?thesis using that by blast
qed
fun list_ordered_pairs :: "'a list ⇒ ('a × 'a) list" where
"list_ordered_pairs [] = []" |
"list_ordered_pairs (x#xs) = (map (Pair x) xs) @ (list_ordered_pairs xs)"
lemma list_ordered_pairs_set_containment :
assumes "x ∈ list.set xs"
and "y ∈ list.set xs"
and "x ≠ y"
shows "(x,y) ∈ list.set (list_ordered_pairs xs) ∨ (y,x) ∈ list.set (list_ordered_pairs xs)"
using assms by (induction xs; auto)
subsection ‹Calculating Distinct Non-Reflexive Pairs over List Elements›