Theory Auxx.Util
theory Util
imports
Polynomial_Factorization.Missing_List
"HOL-Library.Infinite_Set"
HOL.Archimedean_Field
"Abstract-Rewriting.Relative_Rewriting"
begin
lemma rtrancl_Id [simp]: "Id⇧* = Id"
by (auto elim: rtrancl.induct)
lemma relpow_2 [simp]: "r ^^ 2 = r O r"
by (metis Suc_1 relpow_1 relpow_Suc)
definition replace :: "'a ⇒ 'a set ⇒ 'a set ⇒ 'a set" where
"replace a bs M ≡ if a ∈ M then M - {a} ∪ bs else M"
definition replace_impl :: "'a ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
"replace_impl a bs M ≡ if a ∈ set M then bs @ filter (λ b. b ≠ a) M else M"
lemma replace_impl[simp]: "set (replace_impl a bs M) = replace a (set bs) (set M)"
unfolding replace_impl_def replace_def by auto
declare map_option_cong[fundef_cong]
lemma finite_card_eq_imp_bij_betw:
assumes "finite A"
and "card (f ` A) = card A"
shows "bij_betw f A (f ` A)"
using ‹card (f ` A) = card A›
unfolding inj_on_iff_eq_card [OF ‹finite A›, symmetric]
by (rule inj_on_imp_bij_betw)
text ‹Every bijective function between two subsets of a set can be turned
into a compatible renaming (with finite domain) on the full set.›
lemma bij_betw_extend:
assumes *: "bij_betw f A B"
and "A ⊆ V"
and "B ⊆ V"
and "finite A"
shows "∃g. finite {x. g x ≠ x} ∧
(∀x∈UNIV - (A ∪ B). g x = x) ∧
(∀x∈A. g x = f x) ∧
bij_betw g V V"
proof -
have "finite B" using assms by (metis bij_betw_finite)
have [simp]: "card A = card B" by (metis * bij_betw_same_card)
have "card (A - B) = card (B - A)"
proof -
have "card (A - B) = card A - card (A ∩ B)"
by (metis ‹finite A› card_Diff_subset_Int finite_Int)
moreover have "card (B - A) = card B - card (A ∩ B)"
by (metis ‹finite A› card_Diff_subset_Int finite_Int inf_commute)
ultimately show ?thesis by simp
qed
then obtain g where **: "bij_betw g (B - A) (A - B)"
by (metis ‹finite A› ‹finite B› bij_betw_iff_card finite_Diff)
define h where "h = (λx. if x ∈ A then f x else if x ∈ B - A then g x else x)"
have "bij_betw h A B"
by (metis (full_types) * bij_betw_cong h_def)
moreover have "bij_betw h (V - (A ∪ B)) (V - (A ∪ B))"
by (auto simp: bij_betw_def h_def inj_on_def)
moreover have "B ∩ (V - (A ∪ B)) = {}" by blast
ultimately have "bij_betw h (A ∪ (V - (A ∪ B))) (B ∪ (V - (A ∪ B)))"
by (rule bij_betw_combine)
moreover have "A ∪ (V - (A ∪ B)) = V - (B - A)"
and "B ∪ (V - (A ∪ B)) = V - (A - B)"
using ‹A ⊆ V› and ‹B ⊆ V› by blast+
ultimately have "bij_betw h (V - (B - A)) (V - (A - B))" by simp
moreover have "bij_betw h (B - A) (A - B)"
using ** by (auto simp: bij_betw_def h_def inj_on_def)
moreover have "(V - (A - B)) ∩ (A - B) = {}" by blast
ultimately have "bij_betw h ((V - (B - A)) ∪ (B - A)) ((V - (A - B)) ∪ (A - B))"
by (rule bij_betw_combine)
moreover have "(V - (B - A)) ∪ (B - A) = V"
and "(V - (A - B)) ∪ (A - B) = V"
using ‹A ⊆ V› and ‹B ⊆ V› by auto
ultimately have "bij_betw h V V" by simp
moreover have "∀x∈A. h x = f x" by (auto simp: h_def)
moreover have "finite {x. h x ≠ x}"
proof -
have "finite (A ∪ (B - A))" using ‹finite A› and ‹finite B› by auto
moreover have "{x. h x ≠ x} ⊆ (A ∪ (B - A))" by (auto simp: h_def)
ultimately show ?thesis by (metis finite_subset)
qed
moreover have "∀x∈UNIV - (A ∪ B). h x = x" by (simp add: h_def)
ultimately show ?thesis by blast
qed
lemma infinite_inj_on_remove_one:
fixes f :: "'a ⇒ 'b"
assumes inf: "infinite B"
and inj: "inj_on f A"
and ran: "range f ⊆ B"
shows "∃ g. inj_on g A ∧ range g ⊆ B - {b}"
proof -
from inf have inf: "infinite (B - {b})" by auto
from infinite_imp_elem[OF inf] obtain b' where b': "b' ∈ B - {b}" by force
from infinite_countable_subset[OF inf] obtain h :: "nat ⇒ 'b" where inj_h: "inj h" and ran_h: "range h ⊆ B - {b}" by auto
let ?h = "λ a. h (Suc (the_inv h (f a)))"
let ?f = "λ a. (if f a ∈ range h then ?h a else f a)"
let ?g = "λ a. if f a = b then h 0 else if a ∈ A then ?f a else b'"
show ?thesis
proof (rule exI[of _ ?g], unfold inj_on_def, intro conjI ballI impI)
fix a1 a2
assume a1: "a1 ∈ A" and a2: "a2 ∈ A" and id: "?g a1 = ?g a2"
show "a1 = a2"
proof (cases "f a1 = b")
case True
with id have id: "?g a2 = h 0" and fa1: "f a1 = b" by auto
show ?thesis
proof (cases "f a2 = b")
case True
with fa1 id a1 a2 inj show ?thesis unfolding inj_on_def by auto
next
case False
with id a2 have id: "?f a2 = h 0" by auto
with inj_h show ?thesis unfolding inj_on_def by (cases "f a2 ∈ range h", auto)
qed
next
case False
with id a1 have id: "?f a1 = ?g a2" by auto
show ?thesis
proof (cases "f a2 = b")
case True
with id have "?f a1 = h 0" by auto
with inj_h show ?thesis unfolding inj_on_def by (cases "f a1 ∈ range h", auto)
next
case False
with id a2 have id: "?f a1 = ?f a2" by auto
have "f a1 = f a2"
proof (cases "f a1 ∈ range h")
case True note r1 = this
with id have id: "?f a2 = ?h a1" by simp
then have r2: "f a2 ∈ range h" by (cases "f a2 ∈ range h", auto)
with id have id: "?h a1 = ?h a2" by simp
from r1 r2 obtain i1 i2 where h: "f a1 = h i1" "f a2 = h i2" by auto
from id[unfolded h the_inv_f_f[OF inj_h]] have "h (Suc i1) = h (Suc i2)" .
with inj_h have id: "i1 = i2" unfolding inj_on_def by auto
with h show "f a1 = f a2" by auto
next
case False note r1 = this
{
assume "f a2 ∈ range h"
with id have id: "?f a1 = ?h a2" by simp
then have "f a1 ∈ range h" by (cases "f a1 ∈ range h", auto)
with r1 have False by auto
}
with r1 id show ?thesis by auto
qed
with a1 a2 inj show ?thesis unfolding inj_on_def by auto
qed
qed
next
show "range ?g ⊆ B - {b}" using ran_h ran b' by auto
qed
qed
lemma infinite_inj_on_finite_remove_finite:
fixes f :: "'a ⇒ 'b" and B :: "'b set"
assumes inf: "infinite B"
and inj: "inj_on f A"
and fin: "finite B'"
and ran: "range f ⊆ B"
shows "∃ g. inj_on g A ∧ range g ⊆ B - B'"
using fin
proof (induct B')
case empty
show ?case using inj ran by auto
next
case (insert b B')
from insert(3) obtain g where inj: "inj_on (g :: 'a ⇒ 'b) A" and ran: "range g ⊆ B - B'" by auto
from insert(1) inf have "infinite (B - B')" by auto
from infinite_inj_on_remove_one[OF this inj ran, of b]
show ?case by auto
qed
subsection ‹Combinators›
definition const :: "'a ⇒ 'b ⇒ 'a" where
"const ≡ (λx y. x)"
definition flip :: "('a ⇒ 'b ⇒ 'c) ⇒ ('b ⇒ 'a ⇒ 'c)" where
"flip f ≡ (λx y. f y x)"
declare flip_def[simp]
lemma const_apply[simp]: "const x y = x"
by (simp add: const_def)
lemma foldr_Cons_append_conv [simp]:
"foldr (#) xs ys = xs @ ys"
by (induct xs) simp_all
lemma foldl_flip_Cons[simp]:
"foldl (flip (#)) xs ys = rev ys @ xs"
by (induct ys arbitrary: xs) simp_all
lemma foldr_flip_rev[simp]:
"foldr (flip f) (rev xs) a = foldl f a xs"
by (simp add: foldr_conv_foldl)
lemma foldl_flip_rev[simp]:
"foldl (flip f) a (rev xs) = foldr f xs a"
by (simp add: foldl_conv_foldr)
fun debug :: "(String.literal ⇒ String.literal) ⇒ String.literal ⇒ 'a ⇒ 'a" where "debug i t x = x"
section ‹Auxiliary Lemmas›
lemma down_chain_imp_eq:
fixes f :: "nat seq"
assumes "∀i. f i ≥ f (Suc i)"
shows "∃N. ∀i > N. f i = f (Suc i)"
proof -
let ?F = "{f i | i. True}"
from wf_less [unfolded wf_eq_minimal, THEN spec, of ?F]
obtain x where "x ∈ ?F" and *: "∀y. y < x ⟶ y ∉ ?F" by auto
obtain N where "f N = x" using ‹x ∈ ?F› by auto
moreover have "∀i > N. f i ∈ ?F" by auto
ultimately have "∀i > N. ¬ f i < x" using * by auto
moreover have "∀i > N. f N ≥ f i"
using chainp_imp_rtranclp [of "(≥)" f, OF assms] by simp
ultimately have "∀i > N. f i = f (Suc i)"
using ‹f N = x› by (auto) (metis less_SucI order.not_eq_order_implies_strict)
then show ?thesis ..
qed
fun max_f :: "(nat ⇒ nat) ⇒ nat ⇒ nat" where
"max_f f 0 = 0"
| "max_f f (Suc i) = max (f i) (max_f f i)"
lemma max_f: "i < n ⟹ f i ≤ max_f f n"
proof (induct n)
case (Suc n)
then show ?case by (cases "i = n", auto)
qed simp
lemma sum_list_take_eq:
fixes xs :: "nat list"
shows "k < i ⟹ i < length xs ⟹ sum_list (take i xs) =
sum_list (take k xs) + xs ! k + sum_list (take (i - Suc k) (drop (Suc k) xs))"
by (subst id_take_nth_drop [of k]) (auto simp: min_def drop_take)
lemma nth_equalityE:
"xs = ys ⟹ (length xs = length ys ⟹ (⋀i. i < length xs ⟹ xs ! i = ys ! i) ⟹ P) ⟹ P"
by simp
lemma sum_list_take [simp]:
"i < length (xs :: nat list) ⟹ sum_list (take i xs) ≤ sum_list xs"
by (induct xs arbitrary: i) (simp, case_tac i, auto)
lemma concat_nth:
assumes "m < length xs" and "n < length (xs ! m)"
and "i = sum_list (map length (take m xs)) + n"
shows "concat xs ! i = xs ! m ! n"
using assms
proof (induct xs arbitrary: m n i)
case (Cons x xs)
show ?case
proof (cases m)
case 0
then show ?thesis using Cons by (simp add: nth_append)
next
case (Suc k)
with Cons(1) [of k n "i - length x"] and Cons(2-)
show ?thesis by (simp_all add: nth_append)
qed
qed simp
lemma less_length_concat:
assumes "i < length (concat xs)"
shows "∃m n.
i = sum_list (map length (take m xs)) + n ∧
m < length xs ∧ n < length (xs ! m) ∧ concat xs ! i = xs ! m ! n"
using assms
proof (induct xs arbitrary: i rule: length_induct)
case (1 xs)
then show ?case
proof (cases xs)
case (Cons y ys)
note [simp] = this
{ assume *: "i < length y"
with 1 obtain n where "i = n" and "n < length y"
and "y ! i = y ! n" by simp
then have "i = sum_list (map length (take 0 xs)) + n"
and "0 < length xs" and "n < length (xs ! 0)"
and "concat xs ! i = xs ! 0 ! n"
using * by (auto simp: nth_append)
then have ?thesis by blast }
moreover
{ assume *: "i ≥ length y"
define j where "j = i - length y"
then have "length ys < length xs" "j < length (concat ys)"
using * and "1.prems" by auto
with 1 obtain m n where "j = sum_list (map length (take m ys)) + n"
and "m < length ys" and "n < length (ys ! m)"
and "concat ys ! j = ys ! m ! n" by blast
then have "i = sum_list (map length (take (Suc m) xs)) + n"
and "Suc m < length xs" and "n < length (xs ! Suc m)"
and "concat xs ! i = xs ! Suc m ! n"
using * by (simp_all add: j_def nth_append)
then have ?thesis by blast }
ultimately show ?thesis by force
qed simp
qed
lemma concat_nth_length:
"i < length uss ⟹ j < length (uss ! i) ⟹
sum_list (map length (take i uss)) + j < length (concat uss)"
by (induct uss arbitrary: i j) (simp, case_tac i, auto)
lemma concat_remove_nth:
assumes "i < length sss"
and "j < length (sss ! i)"
defines "k ≡ sum_list (map length (take i sss)) + j"
shows "concat (take i sss @ remove_nth j (sss ! i) # drop (Suc i) sss) = remove_nth k (concat sss)"
using assms
unfolding remove_nth_def
proof (induct sss rule: List.rev_induct)
case Nil then show ?case by auto
next
case (snoc ss sss)
then have "i = length sss ∨ i < length sss" by auto
then show ?case
proof
assume i:"i = length sss"
have "sum_list (map length sss) = length (concat sss)" by (simp add: length_concat)
with snoc i show ?thesis by simp
next
assume i:"i < length sss"
then have nth:"(sss @ [ss]) ! i = sss ! i" by (simp add: nth_append)
from i have drop:"drop (Suc i) (sss @ [ss]) = drop (Suc i) sss @ [ss]" by auto
from i have take:"take i (sss @ [ss]) = take i sss" by auto
from snoc(1)[OF i] snoc(2-) have 1:"concat (take i (sss @ [ss]) @
(take j ((sss @ [ss]) ! i) @ drop (Suc j) ((sss @ [ss]) ! i)) # drop (Suc i) (sss @ [ss])) =
take k (concat sss) @ drop (Suc k) (concat sss) @ ss" unfolding take nth drop by simp
from snoc(4) take have k:"k = sum_list (map length (take i sss)) + j" by auto
from nth snoc(3) have j: "j < length (sss ! i)" by auto
have takek:"take (sum_list (map length (take i sss)) + j) (concat (sss @ [ss])) =
take (sum_list (map length (take i sss)) + j) (concat sss)"
using concat_nth_length[OF i j] by auto
have dropk:"drop (Suc (sum_list (map length (take i sss)) + j)) (concat sss) @ ss =
drop (Suc (sum_list (map length (take i sss)) + j)) (concat (sss @ [ss]))"
using concat_nth_length[OF i j] by auto
have "take k (concat sss) @ drop (Suc k) (concat sss) @ ss =
take k (concat (sss @ [ss])) @ drop (Suc k) (concat (sss @ [ss]))"
unfolding k takek dropk ..
with 1 show ?thesis by auto
qed
qed
fun fold_map :: "('a ⇒ 'b ⇒ 'c × 'b) ⇒ 'a list ⇒ 'b ⇒ 'c list × 'b" where
"fold_map f [] y = ([], y)"
| "fold_map f (x#xs) y = (case f x y of
(x', y') ⇒ case fold_map f xs y' of
(xs', y'') ⇒ (x' # xs', y''))"
lemma fold_map_cong [fundef_cong]:
assumes "a = b" and "xs = ys"
and "⋀x. x ∈ set xs ⟹ f x = g x"
shows "fold_map f xs a = fold_map g ys b"
using assms by (induct ys arbitrary: a b xs) simp_all
lemma fold_map_map_conv:
assumes "⋀x ys. x ∈ set xs ⟹ f (g x) (g' x @ ys) = (h x, ys)"
shows "fold_map f (map g xs) (concat (map g' xs) @ ys) = (map h xs, ys)"
using assms by (induct xs) simp_all
lemma map_fst_fold_map:
"map f (fst (fold_map g xs y)) = fst (fold_map (λa b. apfst f (g a b)) xs y)"
by (induct xs arbitrary: y) (auto split: prod.splits, metis fst_conv)
lemma Max_le_Max:
assumes X: "finite X" "X ≠ {}" and Y: "finite Y" "Y ≠ {}"
shows "Max X ≤ Max Y ⟷ (∀x∈X. ∃y∈Y. x ≤ y)"
by (meson Max.boundedE Max_ge_iff Max_in assms)
lemma Max_less_Max:
assumes X: "finite X" "X ≠ {}" and Y: "finite Y" "Y ≠ {}"
shows "Max X < Max Y ⟷ (∀x∈X. ∃y∈Y. x < y)"
by (meson Max_less_iff assms eq_Max_iff less_le_trans)
lemma upt_append_upt: "i ≤ j ⟹ j ≤ k ⟹ [i..<j] @ [j..<k] = [i..<k]"
using upt_add_eq_append[of i j "k - j"] by auto
subsection ‹size estimations›
lemma size_list_pointwise2: assumes "length xs = length ys"
and "⋀ i. i < length ys ⟹ f (xs ! i) ≤ g (ys ! i)"
shows "size_list f xs ≤ size_list g ys"
proof -
have id: "(size_list f xs ≤ size_list g ys) = (sum_list (map f xs) ≤ sum_list (map g ys))"
unfolding size_list_conv_sum_list assms(1) by auto
have "map f xs = map f (map ((!) xs) [0..<length xs])" using map_nth[of xs] by simp
also have "... = map (λ i. f (xs ! i)) [0..<length xs]" (is "_ = ?xs") by simp
finally have xs: "map f xs = ?xs" .
have "map g ys = map g (map ((!) ys) [0..<length ys])" using map_nth[of ys] by simp
also have "... = map (λ i. g (ys ! i)) [0..<length xs]" (is "_ = ?ys") using assms by simp
finally have ys: "map g ys = ?ys" .
show ?thesis
unfolding id unfolding xs ys
by (rule sum_list_mono, insert assms, auto)
qed
lemma size_list_pointwise3: assumes len: "length xs = length ys"
and xs: "xs ≠ []"
and lt: "⋀ i. i < length ys ⟹ f (xs ! i) < g (ys ! i)"
shows "size_list f xs < size_list g ys"
proof -
from xs obtain x xs' where xs: "xs = x # xs'" by (cases xs, auto)
with len obtain y ys' where ys: "ys = y # ys'" by (cases ys, auto)
have "size_list f xs = f x + 1 + size_list f xs'" by (simp add: xs)
also have "size_list f xs' ≤ size_list g ys'"
proof (rule size_list_pointwise2)
fix i
assume "i < length ys'"
then have "Suc i < length ys" unfolding ys by simp
from lt[OF this]
show "f (xs' ! i) ≤ g (ys' ! i)" unfolding xs ys by auto
qed (insert len xs ys, simp)
also have "f x < g y" using lt[of 0] unfolding xs ys by simp
also have "g y + 1 + size_list g ys' = size_list g ys" unfolding ys by simp
finally show ?thesis by arith
qed
subsection ‹assignments from key-value pairs›
fun enum_vectors :: "'c list ⇒ 'v list ⇒ ('v × 'c)list list"
where "enum_vectors C [] = [[]]"
| "enum_vectors C (x # xs) = (let rec = enum_vectors C xs in concat (map (λ vec. map (λ c. (x,c) # vec) C) rec))"
definition fun_of :: "('v × 'c) list ⇒ 'v ⇒ 'c" where
[simp]: "fun_of vec x = the (map_of vec x)"
lemma enum_vectors_complete:
assumes "C ≠ []"
shows "∃ vec ∈ set (enum_vectors C xs). ∀ x ∈ set xs. ∀ c ∈ set C. α x = c ⟶ fun_of vec x = c"
proof (induct xs, simp)
case (Cons x xs)
from this obtain vec where enum: "vec ∈ set (enum_vectors C xs)" and eq: "∀ x ∈ set xs. ∀ c ∈ set C. α x = c ⟶ fun_of vec x = c" by auto
from enum have res: "set (map (λ c. (x,c) # vec) C) ⊆ set (enum_vectors C (x # xs)) " (is "_ ⊆ ?res") by auto
show ?case
proof (cases "α x ∈ set C")
case False
from assms have "hd C ∈ set C" by auto
with res have elem: "(x,hd C) # vec ∈ ?res" (is "?vec ∈ _") by auto
from eq False have "∀ y ∈ set (x # xs). ∀ c ∈ set C. α y = c ⟶ fun_of ?vec y = c" by auto
with elem show ?thesis by blast
next
case True
with res have elem: "(x, α x) # vec ∈ ?res" (is "?vec ∈ _") by auto
from eq True have "∀ y ∈ set (x # xs). ∀ c ∈ set C. α y = c ⟶ fun_of ?vec y = c" by auto
with elem show ?thesis by blast
qed
qed
lemma enum_vectors_sound:
assumes "y ∈ set xs" and "vec ∈ set (enum_vectors C xs)"
shows "fun_of vec y ∈ set C"
using assms
proof (induct xs arbitrary: vec, simp)
case (Cons x xs vec)
from Cons(3) obtain v vecc where vec: "vec = v # vecc" by auto
note C3 = Cons(3)[unfolded vec enum_vectors.simps Let_def]
from C3 have vecc: "vecc ∈ set (enum_vectors C xs)" by auto
from C3 obtain c where v: "v = (x,c)" and c: "c ∈ set C" by auto
show ?case
proof (cases "y = x")
case True
show ?thesis unfolding vec v True using c by auto
next
case False
with Cons(2) have y: "y ∈ set xs" by auto
from False have id: "fun_of vec y = fun_of vecc y"
unfolding vec v by auto
show ?thesis unfolding id
by (rule Cons(1)[OF y vecc])
qed
qed
declare fun_of_def[simp del]
lemma map_of_nth_zip_Some [simp]:
assumes "distinct vs" and "length vs ≤ length ts" and "i < length vs"
shows "map_of (zip vs ts) (vs ! i) = Some (ts ! i)"
using assms proof (induct i arbitrary: vs ts)
case 0 then show ?case by (induct ts) (induct vs, auto)+
next
case (Suc i) show ?case
proof (cases ts)
case Nil with Suc show ?thesis unfolding Nil by simp
next
case (Cons t ts')
note Cons' = this
show ?thesis
proof (cases vs)
case Nil from Suc show ?thesis unfolding Cons' Nil by simp
next
case (Cons v vs') from Suc show ?thesis unfolding Cons Cons' by auto
qed
qed
qed
lemma fun_of_concat:
assumes mem: "x ∈ set (map fst (τs i))"
and i: "i < n"
and ident: "⋀ i j. i < n ⟹ j < n ⟹ x ∈ set (map fst (τs i)) ⟹ x ∈ set (map fst (τs j)) ⟹ fun_of (τs i) x = fun_of (τs j) x"
shows "fun_of (concat (map τs [0..<n])) x = fun_of (τs i) x"
using assms
proof (induct n arbitrary: i τs)
case 0
then show ?case by simp
next
case (Suc n i τs) note IH = this
let ?τs = "λi. τs (Suc i)"
have id: "concat (map τs [0..<Suc n]) = τs 0 @ concat (map ?τs [0..<n])" unfolding map_upt_Suc by simp
let ?l = "map_of (τs 0) x"
show ?case
proof (cases i)
case 0
with IH(2) have x: "x ∈ set (map fst (τs 0))" by auto
then obtain y where xy: "(x,y) ∈ set (τs 0)" by auto
from map_of_eq_None_iff[of "τs 0" x] xy have "?l ≠ None" by force
then obtain y where look: "?l = Some y" by (cases "τs 0", auto)
show ?thesis unfolding 0 fun_of_def id look map_of_append_Some[OF look] by simp
next
case (Suc j)
with IH(3)
have 0: "0 < i" and j: "j < n" by auto
show ?thesis
proof (cases "x ∈ set (map fst (τs 0))")
case False
have l: "?l = None"
proof (cases "?l")
case (Some y)
from map_of_SomeD[OF this] and False show ?thesis by force
qed simp
show ?thesis unfolding fun_of_def id map_of_append_None[OF l]
unfolding fun_of_def[symmetric] Suc
proof (rule IH(1)[OF _ j])
show "x ∈ set (map fst (τs (Suc j)))" using IH(2) unfolding Suc .
next
fix i j
assume "i < n" and "j < n" and "x ∈ set (map fst (τs (Suc i)))" and "x ∈ set (map fst (τs (Suc j)))"
then show "fun_of (τs (Suc i)) x = fun_of (τs (Suc j)) x"
using IH(4)[of "Suc i" "Suc j"] by auto
qed
next
case True
then obtain y where xy: "(x,y) ∈ set (τs 0)" by auto
from map_of_eq_None_iff[of "τs 0" x] and xy have "?l ≠ None" by force
then obtain y where look: "?l = Some y" by (cases "τs 0", auto)
have "fun_of (concat (map τs [0..<Suc n])) x = fun_of (τs 0) x"
unfolding id fun_of_def look
map_of_append_Some[OF look] by simp
also have "... = fun_of (τs i) x"
proof (rule IH(4)[OF _ IH(3)])
from xy show "x ∈ set (map fst (τs 0))" by force
next
from IH(2) show "x ∈ set (map fst (τs i))" by force
qed simp
finally show ?thesis .
qed
qed
qed
lemma fun_of_concat_part: assumes mem: "x ∈ set (map fst (τs i))"
and i: "i < n"
and partition: "is_partition (map (λ i. set (map fst (τs i))) [0..<n])"
shows "fun_of (concat (map τs [0..<n])) x = fun_of (τs i) x"
proof (rule fun_of_concat, rule mem, rule i)
fix i j
assume "i < n" and "j < n" and "x ∈ set (map fst (τs i))" and "x ∈ set (map fst (τs j))"
then have "i = j" using partition[unfolded is_partition_alt is_partition_alt_def] by (cases "i = j", auto)
then show "fun_of (τs i) x = fun_of (τs j) x" by simp
qed
lemma fun_of_concat_merge:
assumes "⋀ i. i < length ts ⟹ x ∈ h (ts ! i) ⟹ fun_of (f i) x = (g ! i) x"
and "length ts = length g"
and "⋀ i. i < length ts ⟹ map_of (f i) x ≠ None ⟷ x ∈ h (ts ! i)"
and "x ∈ h (ts ! i)"
and "i < length ts"
shows "fun_of (concat (map f [0..<length ts])) x = fun_merge g (map h ts) x"
using assms
unfolding fun_merge_def fun_of_def
proof (induct ts arbitrary: i f g)
case Nil
then show ?case by simp
next
case (Cons xy ts)
let ?p' = "λ ts i. i < length (map h ts) ∧ x ∈ map h ts ! i"
let ?p = "?p' (xy # ts)"
let ?P = "?p' ts"
let ?L = "LEAST i. ?p i"
have id: "the (map_of (concat (map f [0..<length (xy # ts)])) x) =
the (map_of (f 0 @ concat (map (λ i. f (Suc i)) [0..<length ts])) x)"
(is "?l = the (map_of ( _ @ ?l') x)")
by (simp add: map_upt_Suc del: upt_Suc)
show ?case
proof (cases "map_of (f 0) x")
case (Some y)
from map_of_append_Some[OF Some]
have ly: "?l = y" unfolding id Some by simp
have "?p 0" using Cons(4)[of 0] using Some by auto
then have L0: "?L = 0"
by (rule Least_equality, simp)
from Cons(4)[of 0] Some have x: "x ∈ h xy" by auto
show ?thesis unfolding ly L0 using Cons(2)[of 0, unfolded Some] x by simp
next
case None
from map_of_append_None[OF None]
have ll: "?l = the (map_of ?l' x)" unfolding id by simp
from Cons(4)[of 0] None have x: "x ∉ h xy" by auto
then have p0: "¬ ?p 0" by simp
from Cons(5) Cons(6) have pI: "?p i" unfolding nth_map[OF Cons(6)] by simp
from Least_Suc[of ?p, OF pI p0] have L: "?L = Suc (LEAST m. ?P m)" by simp
from Cons(3) obtain a g' where g: "g = a # g'" by (cases g, auto)
from Cons(5) x obtain j where i: "i = Suc j" by (cases i, auto)
show ?thesis unfolding ll L g nth_Cons_Suc
proof (rule Cons(1))
from g Cons(3) show "length ts = length g'" by auto
next
from Cons(5) i show "x ∈ h (ts ! j)" by auto
next
from Cons(6) i show "j < length ts" by auto
next
fix m
assume "m < length ts"
then show "map_of (f (Suc m)) x ≠ None ⟷ x ∈ h (ts ! m)"
using Cons(4)[of "Suc m"] by auto
next
fix m
assume "m < length ts" and "x ∈ h (ts ! m)"
then show "the (map_of (f (Suc m)) x) = (g' ! m) x"
using Cons(2)[of "Suc m"] unfolding g by auto
qed
qed
qed
context
fixes P :: "'a ⇒ 'b ⇒ bool"
and R :: "'a rel"
and R' :: "'b rel"
assumes simulate: "⋀ s t s'. P s t ⟹ (s,s') ∈ R ⟹ ∃ t'. P s' t' ∧ (t,t') ∈ R'"
begin
lemma simulate_conditional_steps_count: assumes steps: "(s,s') ∈ R^^n"
and P: "P s t"
shows "∃ t'. P s' t' ∧ (t,t') ∈ R'^^n"
using steps
proof (induct n arbitrary: s')
case 0
with P show ?case by auto
next
case (Suc n s'')
from Suc(2) obtain s' where ss': "(s,s') ∈ R^^n" and ss'': "(s',s'') ∈ R" by auto
from Suc(1)[OF ss'] obtain t' where tt': "(t, t') ∈ R' ^^ n" and P: "P s' t'" by auto
from simulate[OF P ss''] tt' show ?case by auto
qed
lemma simulate_conditional_steps: assumes steps: "(s,s') ∈ R⇧*"
and P: "P s t"
shows "∃ t'. P s' t' ∧ (t,t') ∈ R'⇧*"
proof -
from steps obtain n where "(s,s') ∈ R^^n" by auto
from simulate_conditional_steps_count[OF this P]
show ?thesis by (blast intro: relpow_imp_rtrancl)
qed
end
context
fixes P :: "'a ⇒ 'b ⇒ bool"
and R S :: "'a rel"
and R' S' :: "'b rel"
assumes simulateR: "⋀ s t s'. P s t ⟹ (s,s') ∈ R ⟹ ∃ t'. P s' t' ∧ (t,t') ∈ R'"
and simulateS: "⋀ s t s'. P s t ⟹ (s,s') ∈ S ⟹ ∃ t'. P s' t' ∧ (t,t') ∈ S'"
begin
lemma simulate_conditional_relative_step: assumes step: "(s,s') ∈ relto R S"
and P: "P s t"
shows "∃ t'. P s' t' ∧ (t,t') ∈ relto R' S'"
proof -
from step obtain u v where su: "(s,u) ∈ S⇧*" and uv: "(u,v) ∈ R" and vs': "(v,s') ∈ S⇧*" by auto
have "∃ u'. P u u' ∧ (t,u') ∈ S'⇧*"
by (rule simulate_conditional_steps[of P, OF simulateS su P])
then obtain u' where P: "P u u'" and tu: "(t,u') ∈ S'⇧*" by blast
from simulateR[OF P uv] obtain v' where P: "P v v'" and uv: "(u',v') ∈ R'" by auto
have "∃ t'. P s' t' ∧ (v',t') ∈ S'⇧*"
by (rule simulate_conditional_steps[of P, OF simulateS vs' P])
then obtain t' where P: "P s' t'" and vt: "(v',t') ∈ S'⇧*" by blast
from tu uv vt have "(t,t') ∈ relto R' S'" by auto
with P show ?thesis by auto
qed
lemma simulate_conditional_relative_steps_count: assumes step: "(s,s') ∈ (relto R S)^^n"
and P: "P s t"
shows "∃ t'. P s' t' ∧ (t,t') ∈ (relto R' S')^^n"
by (rule simulate_conditional_steps_count[of P, OF simulate_conditional_relative_step step P])
end
locale relative_simulation_image =
fixes S :: "'a rel" and N :: "'a rel" and B :: "'b rel" and f :: "'a ⇒ 'b"
assumes S: "(x,y) ∈ S ⟹ (f x, f y) ∈ B^+"
and N: "(x,y) ∈ N ⟹ (f x, f y) ∈ B⇧*"
begin
lemma many_non_strict: "(x,y) ∈ N⇧* ⟹ (f x, f y) ∈ B⇧*"
proof (induct rule: rtrancl_induct)
case (step y z)
from step(3) N[OF step(2)] show ?case by auto
qed auto
lemma single_relative: assumes step: "(x,y) ∈ relto S N" shows "(f x, f y) ∈ B^+"
proof -
from step obtain u v where xu: "(x,u) ∈ N⇧*" and uv: "(u,v) ∈ S" and vy: "(v,y) ∈ N⇧*" by blast
from many_non_strict[OF xu] S[OF uv] many_non_strict[OF vy] show ?thesis by auto
qed
lemma count_relative: "(x,y) ∈ (relto S N)^^n ⟹ ∃ m ≥ n. (f x, f y) ∈ B^^m"
proof (induct n arbitrary: x y)
case (Suc n x y)
let ?R = "relto S N"
from Suc(2) obtain u where xu: "(x,u) ∈ ?R ^^ n" and uy: "(u,y) ∈ ?R" by auto
from single_relative[OF uy]
obtain n1 where n1: "n1 > 0" and uy: "(f u, f y) ∈ B ^^ n1" unfolding trancl_power by blast
from Suc(1)[OF xu] obtain m where m: "m ≥ n" and xu: "(f x, f u) ∈ B^^m" by auto
from xu uy have xy: "(f x, f y) ∈ B^^(m + n1)" unfolding relpow_add by blast
from m n1 have n: "m + n1 ≥ Suc n" by auto
from xy n show ?case by auto
next
case 0
then show ?case by (intro exI[of _ 0], auto)
qed
end
lemma rtrancl_map:
assumes simu: "⋀x y. (x, y) ∈ r ⟹ (f x, f y) ∈ s"
and steps: "(x, y) ∈ r⇧*"
shows "(f x, f y) ∈ s⇧*"
by (rule relative_simulation_image.many_non_strict[of "{}", OF _ steps], unfold_locales, insert simu, auto)
context
begin
private fun simulate :: "'a rel ⇒ ('a ⇒ bool) ⇒ 'a ⇒ nat ⇒ 'a" where
"simulate R P s 0 = s"
| "simulate R P s (Suc n) = (SOME u. (simulate R P s n,u) ∈ R ∧ P u)"
lemma conditional_steps_imp_not_SN_on: assumes start: "P s"
and step: "⋀ t. P t ⟹ ∃ u. (t,u) ∈ R ∧ P u"
shows "¬ SN_on R {s}"
proof -
let ?sim = "simulate R P s"
{
fix i
have "P (?sim i) ∧ (i > 0 ⟶ (?sim (i - 1), ?sim i) ∈ R)"
proof (induct i)
case 0 show ?case using start by auto
next
case (Suc i)
then have P: "P (?sim i)" by simp
from someI_ex[OF step[OF P]]
show ?case by auto
qed
} note main = this
define g where "g = ?sim"
have "g 0 = s" unfolding g_def by simp
{
fix i
from main[of "Suc i"]
have "(g i, g (Suc i)) ∈ R" unfolding g_def by auto
}
with ‹g 0 = s› show ?thesis by auto
qed
end
lemma finite_imp_eq [simp]:
"finite {x. P x ⟶ Q x} ⟷ finite {x. ¬ P x} ∧ finite {x. Q x}"
by (auto simp: Collect_imp_eq Collect_neg_eq)
lemma image_Pair_Un_imp_eq:
assumes "a ≠ b"
and "Pair a ` A ∪ Pair b ` B = Pair a ` C ∪ Pair b ` D"
shows "A = C ∧ B = D"
proof (rule ccontr)
presume "A ≠ C ∨ B ≠ D"
then show False
proof
assume "A ≠ C"
then obtain x where "x ∈ (A - C) ∨ x ∈ (C - A)" by auto
then show False by (rule disjE) (insert assms, auto)
next
assume "B ≠ D"
then obtain y where "y ∈ (B - D) ∨ y ∈ (D - B)" by auto
then show False by (rule disjE) (insert assms, auto)
qed
qed simp
lemma image_Pair_Un_eq[simp]:
"a ≠ b ⟹ Pair a ` A ∪ Pair b ` B = Pair a ` C ∪ Pair b ` D ⟷ A = C ∧ B = D"
using image_Pair_Un_imp_eq[of a b A B C D] by blast
lemma inj_Pair1: "inj (Pair a)" unfolding inj_on_def by auto
lemma Pair_image_diff_simps[simp]:
"a ≠ b ⟹ (Pair a ` A ∪ Pair b ` B) - (Pair a ` C) = (Pair a ` A - Pair a ` C) ∪ Pair b ` B"
"a ≠ b ⟹ (Pair a ` A ∪ Pair b ` B) - (Pair b ` C) = Pair a ` A ∪ (Pair b ` B - Pair b ` C)"
"a ≠ b ⟹ (Pair a ` A ∪ (Pair b ` B - Pair b ` C)) - Pair a ` D =
(Pair a ` A - Pair a ` D) ∪ (Pair b ` B - Pair b ` C)"
by auto
lemma Collect_Un: "{x ∈ A ∪ B. P x} = {x ∈ A. P x} ∪ {x ∈ B. P x}" by auto
lemma image_snd_Pair: "snd ` {x ∈ Pair a ` A. P x} = {x ∈ A. P (a, x)}" by force
lemma Collect_nested_conj: "{x ∈ {x ∈ A. P x}. Q x} = {x ∈ A. P x ∧ Q x}" by simp
lemma image_snd_Pair_Un[simp]: "snd ` (Pair x ` A ∪ (Pair y ` B)) = A ∪ B" by force
lemma ran_map_upd_Some:
assumes "m a = Some b"
shows "ran (m(a ↦ c)) ⊆ insert c (ran m)"
proof
fix x assume "x ∈ ran (m(a ↦ c))"
then obtain k where upd: "(m(a ↦ c)) k = Some x" by (auto simp: ran_def)
show "x ∈ insert c (ran m)"
proof (cases "a = k")
case True
from assms and upd have x: "x = c" by (simp add: True)
then show ?thesis by simp
next
case False
then have m_upd: "(m(a ↦ c)) k = m k" by simp
from upd[unfolded m_upd] have "x ∈ ran m" by (auto simp: ran_def)
then show ?thesis by simp
qed
qed
lemma subset_UNION_ran:
assumes "m a = Some b"
and "set b ⊆ set c"
shows "⋃ (set ` (ran (m(a ↦ c)))) = ⋃ (set ` (insert c (ran m)))" (is "?l = ?r")
proof
show "?l ⊆ ?r"
proof
fix x assume "x ∈ ?l"
then obtain rs where rs: "rs ∈ ran (m(a ↦ c))" and x: "x ∈ set rs" by auto
from ran_map_upd_Some[of m a b c, OF assms(1)] and rs
have "rs ∈ insert c (ran m)" by blast
with x show "x ∈ ?r" by auto
qed
next
show "?r ⊆ ?l"
proof
fix x assume "x ∈ ?r"
then obtain rs where "rs ∈ insert c (ran m)" and x: "x ∈ set rs" by auto
then have "c = rs ∨ rs ∈ ran m" by auto
then show "x ∈ ?l"
proof
assume c: "c = rs"
show ?thesis unfolding c using x by (auto simp: ran_def)
next
assume "rs ∈ ran m"
then obtain k where mk: "m k = Some rs" by (auto simp: ran_def)
show ?thesis
proof (cases "a = k")
case True
from assms(1) and mk have rs: "rs = b" by (simp add: True)
with assms(2) and x show ?thesis by (auto simp: ran_def)
next
case False
with mk have "rs ∈ ran (m(a ↦ c))" by (auto simp: ran_def)
with x show ?thesis by blast
qed
qed
qed
qed
locale abstract_closure =
fixes A B C :: "'a rel" and S :: "'a set" and P :: "'a ⇒ bool"
assumes S: "⋀ a b. a ∈ S ⟹ (a,b) ∈ C⇧* ⟹ P b"
and AC: "A ⊆ C⇧*"
and PAB: "⋀ a b. P a ⟹ P b ⟹ (a,b) ∈ A ⟹ (a,b) ∈ B"
begin
lemma A_steps_imp_P: assumes a: "a ∈ S"
and rel: "(a,b) ∈ A^^n" shows "P b"
proof -
from relpow_imp_rtrancl[OF rel] rtrancl_mono[OF AC] have "(a,b) ∈ C⇧*" by auto
from S[OF a this] show ?thesis .
qed
lemma A_steps_imp_B_steps_count: assumes a: "a ∈ S"
shows "(a,b) ∈ A^^n ⟹ (a,b) ∈ B^^n"
proof (induct n arbitrary: b)
case (Suc n c)
from Suc(2) obtain b where ab: "(a,b) ∈ A^^n" and bc: "(b,c) ∈ A" by auto
from Suc(1)[OF ab] have abB: "(a,b) ∈ B^^n" .
with PAB[OF A_steps_imp_P[OF a ab] A_steps_imp_P[OF a Suc(2)] bc]
show ?case by auto
qed auto
lemma A_steps_imp_B_steps: assumes a: "a ∈ S"
shows "(a,b) ∈ A⇧* ⟹ (a,b) ∈ B⇧*"
using A_steps_imp_B_steps_count[OF a, of b] unfolding rtrancl_is_UN_relpow by auto
end
locale abstract_closure_twice = abstract_closure +
fixes A' B' :: "'a rel"
assumes AC': "A' ⊆ C⇧*"
and PAB': "⋀ a b. P a ⟹ P b ⟹ (a,b) ∈ A' ⟹ (a,b) ∈ B'"
begin
lemma AA_steps_imp_P: assumes a: "a ∈ S"
and steps: "(a,b) ∈ (A ∪ A')⇧*" shows "P b"
proof -
from AC AC' have "A ∪ A' ⊆ C⇧*" by auto
from rtrancl_mono[OF this] steps have "(a,b) ∈ C⇧*" by auto
from S[OF a this] show ?thesis .
qed
lemma shift_closure: assumes a: "a ∈ S"
and ab: "(a,b) ∈ (A ∪ A')⇧*"
shows "abstract_closure_twice A B C {b} P A' B'"
proof -
{
fix c
assume bc: "(b,c) ∈ C⇧*"
from AC AC' have "(A ∪ A') ⊆ C⇧*" by auto
from ab rtrancl_mono[OF this] have ab: "(a,b) ∈ C⇧*" by auto
with bc have "(a,c) ∈ C⇧* O C⇧*" by auto
also have "… ⊆ C⇧*" by regexp
finally have "P c" by (rule S[OF a])
} note P = this
show ?thesis
by (unfold_locales, insert P AC' PAB' AC PAB, auto)
qed
lemma AA_step_imp_BB_step: assumes a: "a ∈ S"
and steps: "(a,b) ∈ relto A A'" shows "(a,b) ∈ relto B B'"
proof -
interpret alt: abstract_closure_twice A' B' C S P A B
by (unfold_locales, insert S AC' PAB' AC PAB, auto)
from steps obtain c d where ac: "(a,c) ∈ A'⇧*" and cd: "(c,d) ∈ A" and db: "(d,b) ∈ A'⇧*" by blast
from alt.A_steps_imp_B_steps[OF a ac] have ac': "(a,c) ∈ B'⇧*" by auto
from AA_steps_imp_P[OF a] have P: "⋀ b. (a,b) ∈ (A ∪ A')⇧* ⟹ P b" .
have ac: "(a,c) ∈ (A ∪ A')⇧*" using ac by regexp
have "(a,d) ∈ (A ∪ A')⇧* O A" using ac cd by auto
also have "… ⊆ (A ∪ A')⇧*" by regexp
finally have ad: "(a,d) ∈ (A ∪ A')⇧*" .
from PAB[OF P[OF ac] P[OF ad] cd] have cd': "(c,d) ∈ B" .
interpret alt2: abstract_closure_twice A' B' C "{d}" P A B
by (rule alt.shift_closure[OF a], insert ad, simp add: ac_simps)
from alt2.A_steps_imp_B_steps[OF _ db] have db': "(d,b) ∈ B'⇧*" by simp
from ac' cd' db' show ?thesis by blast
qed
lemma AA_steps_imp_BB_steps: assumes a: "a ∈ S"
and steps: "(a,b) ∈ (relto A A')^^n" shows "(a,b) ∈ (relto B B')^^n"
using steps
proof (induct n arbitrary: b)
case (Suc n c)
from Suc(2) obtain b where ab: "(a,b) ∈ (relto A A')^^n" and bc: "(b,c) ∈ relto A A'" by auto
from Suc(1)[OF ab] have ab': "(a,b) ∈ (relto B B')^^n" by auto
from relpow_imp_rtrancl[OF ab] have ab: "(a,b) ∈ (A ∪ A')⇧*" by regexp
interpret alt: abstract_closure_twice A B C "{b}" P A' B'
by (rule shift_closure[OF a ab])
from alt.AA_step_imp_BB_step[OF _ bc] have bc: "(b,c) ∈ relto B B'" by simp
from ab' bc show ?case by auto
qed simp
end
lemma in_set_idx: "a ∈ set as ⟹ ∃i. i < length as ∧ a = as ! i"
unfolding set_conv_nth by auto
lemma find_distinct:
assumes "distinct (map f xs)"
shows "find (λx. z = f x) xs = Some x ⟷ z = f x ∧ x ∈ set xs"
"find (λx. z = f x) xs = None ⟷ z ∉ f ` set xs"
using assms by (induct xs) auto
lemma distinct_alt:
assumes "∀ x. length (filter ((=) x) xs) ≤ 1"
shows "distinct xs"
using assms proof(induct xs)
case (Cons x xs)
then have IH:"distinct xs"
by (metis dual_order.trans filter.simps(2) impossible_Cons nle_le)
from Cons(2) have "length (filter ((=) x) xs) = 0"
by (metis (mono_tags) One_nat_def add.right_neutral add_Suc_right filter.simps(2) le_less length_0_conv less_Suc0 list.simps(3) list.size(4) nat.inject)
then have "x ∉ set (xs)"
by (metis filter_empty_conv length_0_conv)
with IH show ?case
by simp
qed simp
lemma nth_append_Cons: "(xs @ y # zs) ! i =
(if i < length xs then xs ! i else if i = length xs then y else zs ! (i - Suc (length xs)))"
by (cases i "length xs" rule: linorder_cases, auto simp: nth_append)
lemma max_list_leI: assumes "⋀ x. x ∈ set xs ⟹ x ≤ k"
shows "max_list xs ≤ k"
using assms
by (induct xs, auto)
lemma zip_symm: "(x, y) ∈ set (zip xs ys) ⟹ (y, x) ∈ set (zip ys xs)"
by (induct xs ys rule:list_induct2') auto
lemma sum_list_elem:
"(∑x←[y]. f x) = f y"
by simp
lemma sum_list_zero:
assumes "∀i < length xs. f (xs!i) = 0"
shows "(∑x←xs. f x) = 0"
by (metis assms map_eq_conv' monoid_add_class.sum_list_0)
text‹Lemmas about partitions needed for reasoning about unification with linear terms.›
lemma is_partition_union:
assumes "is_partition (x#y#xs)"
shows "is_partition ((x∪y)#xs)"
by (smt (z3) Sup_insert UnE UnI2 assms disjoint_iff is_partition_Cons list.set(2))
lemma is_partition_reorder:
assumes "is_partition (xs @ x # ys)"
shows "is_partition (x # xs @ ys)"
proof-
from assms have "is_partition (xs @ [x])"
by (metis append.simps is_partition_sublist)
then have "∀x' ∈ set xs. x ∩ x' = {}"
by (metis Int_commute append_Cons_nth_left in_set_conv_nth is_partition_def length_append_singleton lessI nth_append_length)
then have "x ∩ ⋃ (set xs) = {}"
by blast
moreover from assms have "x ∩ ⋃ (set ys) = {}"
by (metis append_Nil2 is_partition_Cons is_partition_sublist)
moreover from assms have "is_partition (xs@ys)"
by (metis append_Cons append_Nil append_Nil2 is_partition_sublist)
ultimately show ?thesis
by (smt (z3) Int_commute UnE Union_disjoint is_partition_Cons set_append)
qed
lemma is_partition_append:
assumes "is_partition xs" and "is_partition zs"
and "∀i < length xs. xs!i ∩ ⋃ (set zs) = {}"
shows "is_partition (xs@zs)"
by (smt (verit, del_insts) add_diff_inverse_nat assms(1) assms(2) assms(3) disjoint_iff is_partition_alt is_partition_alt_def length_append mem_simps(9) nat_add_left_cancel_less nth_append nth_mem)
lemma is_partition_intersection:
assumes "is_partition (xs@ys)"
shows "∀ i < length xs. xs!i ∩ ⋃ (set ys) = {}"
using assms proof(induct xs)
case (Cons x xs)
{fix i assume i:"i < length ys"
then have "ys!i = ((x#xs)@ys) ! ((length xs) + 1 + i)"
by simp
with i Cons(2) have "x ∩ ys!i = {}" unfolding is_partition_alt is_partition_alt_def
by (smt (verit, ccfv_SIG) Cons.prems Union_iff append.simps(2) append_assoc disjoint_iff in_set_conv_decomp is_partition_Cons nth_mem)
}
then have "x ∩ ⋃ (set ys) = {}" unfolding is_partition_alt is_partition_alt_def
by (metis Union_disjoint in_set_conv_nth inf_commute)
with Cons(1) show ?case
by (metis Cons.prems append_Cons in_set_conv_nth is_partition_Cons set_ConsD)
qed simp
lemma is_partition_reorder_list:
assumes "is_partition (xs@ys@zs@us)"
shows "is_partition (xs@zs@ys@us)"
proof-
have p1:"is_partition (xs@zs)"
by (metis append_Nil assms is_partition_sublist)
have p2:"is_partition (ys@us)"
by (metis append.right_neutral assms is_partition_sublist)
{fix i assume i:"i < length xs"
from assms have "is_partition (xs@ys@us)"
by (metis append.assoc append_Nil append_Nil2 is_partition_sublist)
with i have "xs!i ∩ ⋃ (set (ys@us)) = {}"
using is_partition_intersection by blast
}moreover
{fix i assume i:"i < length zs"
from assms have "is_partition (zs@us)"
by (metis append_self_conv is_partition_sublist)
with i have "zs!i ∩ ⋃ (set us) = {}"
using is_partition_intersection by blast
moreover have "zs!i ∩ ⋃ (set ys) = {}" proof-
from assms have "is_partition (ys@zs)"
by (metis append_Nil is_partition_sublist)
with i show ?thesis
using in_set_idx is_partition_intersection by fastforce
qed
ultimately have "zs!i ∩ ⋃ (set (ys@us)) = {}"
unfolding set_append by blast
}
ultimately show ?thesis using is_partition_append[OF p1 p2]
by (simp add: nth_append)
qed
lemma distinct_is_partition:
assumes "distinct xs"
shows "is_partition (map (λx. {x}) xs)"
using assms proof(induct xs)
case (Cons x xs)
then show ?case unfolding list.map(2) is_partition_Cons by force
qed (simp add: is_partition_Nil)
lemma filter_ex_index:
assumes "x = filter f xs ! i" "i < length (filter f xs)"
shows "∃j. j < length xs ∧ x = xs!j"
using assms proof(induct "xs" arbitrary:i)
case (Cons y ys)
show ?case proof(cases "f y")
case True
then have filter:"filter f (y#ys) = y#(filter f ys)" by simp
show ?thesis proof(cases i)
case 0
from Cons(2) show ?thesis unfolding filter 0 by auto
next
case (Suc n)
from Cons(2) have "x = filter f ys ! n"
unfolding Suc filter by simp
moreover from Cons(3) have "n < length (filter f ys)"
unfolding Suc filter by simp
ultimately obtain j where "j<length ys" and "x = ys ! j"
using Cons(1) by blast
then show ?thesis by auto
qed
next
case False
then have filter:"filter f (y#ys) = filter f ys" by simp
from Cons obtain j where "j<length ys" and "x = ys ! j"
unfolding filter by blast
then show ?thesis by auto
qed
qed simp
lemma distinct_filter2:
assumes "∀i < size xs. ∀ j < size xs. i ≠ j ∧ f (xs!i) ∧ f (xs!j) ⟶ xs!i ≠ xs!j"
shows "distinct (filter f xs)"
using assms proof(induct xs)
case (Cons x xs)
{fix i j assume "i < length xs" "j < length xs" "i ≠ j" "f (xs!i)" "f (xs!j)"
with Cons(2) have "xs!i ≠ xs!j"
by (metis not_less_eq nth_Cons_Suc Suc_inject length_Cons)
}
with Cons(1) have IH:"distinct (filter f xs)"
by presburger
show ?case proof(cases "f x")
case True
with Cons(2) have "∀j<length xs. f (xs ! j) ⟶ x ≠ xs ! j" by fastforce
then have "x ∉ set (filter f xs)" by (metis filter_set in_set_conv_nth member_filter)
then show ?thesis unfolding filter.simps using True IH by simp
next
case False
then show ?thesis unfolding filter.simps using IH by presburger
qed
qed simp
lemma distinct_is_partitition_sets:
assumes "distinct xs"
and "xs = concat ys"
shows "is_partition (map set ys)"
using assms proof(induct ys arbitrary:xs)
case (Cons y ys)
have "is_partition (map set ys)" proof-
from Cons(2,3) have "distinct (concat ys)"
unfolding concat.simps by simp
with Cons(1) show ?thesis by simp
qed
moreover from Cons(2,3) have "set y ∩ ⋃ (set (map set ys)) = {}"
using distinct_append[of y "concat ys"]by simp
ultimately show ?case
unfolding is_partition_Cons list.map by simp
qed (simp add: is_partition_Nil)
lemma remove_map: "j < length xs ⟹ remove_nth j (map f xs) = map f (remove_nth j xs)"
unfolding remove_nth_def by (auto simp: take_map drop_map)
end