theory Util
imports
List_Util
"~~/src/HOL/Library/Infinite_Set"
"~~/src/HOL/Archimedean_Field"
"$AFP/Abstract-Rewriting/Abstract_Rewriting"
"$AFP/Abstract-Rewriting/Relative_Rewriting"
begin
lemma trans_O_iff: "trans A ⟷ A O A ⊆ A" unfolding trans_def by auto
lemma refl_O_iff: "refl A ⟷ Id ⊆ A" unfolding refl_on_def by auto
lemma foldr_append2 [simp]:
"foldr (op @ ∘ f) xs (ys @ zs) = foldr (op @ ∘ f) xs ys @ zs"
by (induct xs) simp_all
lemma foldr_append2_Nil [simp]:
"foldr (op @ ∘ f) xs [] @ zs = foldr (op @ ∘ f) xs zs"
unfolding foldr_append2 [symmetric] by simp
lemma UNION_set_zip:
"(⋃x ∈ set (zip [0..<length xs] (map f xs)). g x) = (⋃i < length xs. g (i, f (xs ! i)))"
by (auto simp: set_conv_nth)
lemma Id_on_union: "Id_on (A ∪ B) = Id_on A ∪ Id_on B" unfolding Id_on_def by auto
lemma relpow_union_cases: "(a,d) ∈ (A ∪ B)^^n ⟹ (a,d) ∈ B^^n ∨ (∃ b c k m. (a,b) ∈ B^^k ∧ (b,c) ∈ A ∧ (c,d) ∈ (A ∪ B)^^m ∧ n = Suc (k + m))"
proof (induct n arbitrary: a d)
case (Suc n a e)
let ?AB = "A ∪ B"
from Suc(2) obtain b where ab: "(a,b) ∈ ?AB" and be: "(b,e) ∈ ?AB^^n" by (rule relpow_Suc_E2)
from ab
show ?case
proof
assume "(a,b) ∈ A"
show ?thesis
proof (rule disjI2, intro exI conjI)
show "Suc n = Suc (0 + n)" by simp
show "(a,b) ∈ A" by fact
qed (insert be, auto)
next
assume ab: "(a,b) ∈ B"
from Suc(1)[OF be]
show ?thesis
proof
assume "(b,e) ∈ B ^^ n"
with ab show ?thesis
by (intro disjI1 relpow_Suc_I2)
next
assume "∃ c d k m. (b, c) ∈ B ^^ k ∧ (c, d) ∈ A ∧ (d, e) ∈ ?AB ^^ m ∧ n = Suc (k + m)"
then obtain c d k m where "(b, c) ∈ B ^^ k" and *: "(c, d) ∈ A" "(d, e) ∈ ?AB ^^ m" "n = Suc (k + m)" by blast
with ab have ac: "(a,c) ∈ B ^^ (Suc k)" by (intro relpow_Suc_I2)
show ?thesis
by (intro disjI2 exI conjI, rule ac, (rule *)+, simp add: *)
qed
qed
qed simp
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
lemma listsum_replicate_mono: assumes "w1 ≤ (w2 :: nat)"
shows "listsum (replicate n w1) ≤ listsum (replicate n w2)"
proof (induct n)
case (Suc n)
thus ?case using ‹w1 ≤ w2› by auto
qed simp
lemma all_gt_0_listsum_map:
assumes *: "⋀x. f x > (0::nat)"
and x: "x ∈ set xs" and len: "1 < length xs"
shows "f x < (∑x←xs. f x)"
using x len
proof (induct xs)
case (Cons y xs)
show ?case
proof (cases "y = x")
case True
with *[of "hd xs"] Cons(3) show ?thesis by (cases xs, auto)
next
case False
with Cons(2) have x: "x ∈ set xs" by auto
then obtain z zs where xs: "xs = z # zs" by (cases xs, auto)
show ?thesis
proof (cases "length zs")
case 0
with x xs *[of y] show ?thesis by auto
next
case (Suc n)
with xs have "1 < length xs" by auto
from Cons(1)[OF x this] show ?thesis by simp
qed
qed
qed simp
lemma zip_fst: "p ∈ set (zip as bs) ⟹ fst p ∈ set as"
by (cases p, rule set_zip_leftD, simp)
lemma zip_snd: "p ∈ set (zip as bs) ⟹ snd p ∈ set bs"
by (cases p, rule set_zip_rightD, simp)
text ‹functions for removing the i-th element of a list and adjusting an index for this removal›
definition remove_idx :: "nat ⇒ 'a list ⇒ 'a list" where
"remove_idx i xs ≡ take i xs @ drop (Suc i) xs"
lemma remove_idx_len:
assumes i: "i < length xs"
shows "length xs = Suc (length (remove_idx i xs))"
proof -
show ?thesis unfolding arg_cong[where f = "length", OF id_take_nth_drop[OF i]]
unfolding remove_idx_def by simp
qed
definition adjust_idx :: "nat ⇒ nat ⇒ nat" where
"adjust_idx i j ≡ (if j < i then j else (Suc j))"
definition adjust_idx_rev :: "nat ⇒ nat ⇒ nat" where
"adjust_idx_rev i j ≡ (if j < i then j else j - Suc 0)"
lemma adjust_idx_rev1: "adjust_idx_rev i (adjust_idx i j) = j"
unfolding adjust_idx_def adjust_idx_rev_def by (cases "i < j", auto)
lemma adjust_idx_rev2:
assumes "j ≠ i" shows "adjust_idx i (adjust_idx_rev i j) = j"
unfolding adjust_idx_def adjust_idx_rev_def using assms by (cases "i < j", auto)
lemma adjust_idx_i:
"adjust_idx i j ≠ i"
unfolding adjust_idx_def by (cases "j < i", auto)
lemma adjust_idx_nth:
assumes i: "i < length xs"
shows "remove_idx i xs ! j = xs ! adjust_idx i j" (is "?l = ?r")
proof -
let ?j = "adjust_idx i j"
from i have ltake: "length (take i xs) = i" by simp
note nth_xs = arg_cong[where f = "λ xs. xs ! ?j", OF id_take_nth_drop[OF i], unfolded nth_append ltake]
show ?thesis
proof (cases "j < i")
case True
hence j: "?j = j" unfolding adjust_idx_def by simp
show ?thesis unfolding nth_xs unfolding j remove_idx_def nth_append ltake
using True by simp
next
case False
hence j: "?j = Suc j" unfolding adjust_idx_def by simp
from i have lxs: "min (length xs) i = i" by simp
show ?thesis unfolding nth_xs unfolding j remove_idx_def nth_append
using False by (simp add: lxs)
qed
qed
lemma adjust_idx_rev_nth:
assumes i: "i < length xs"
and ji: "j ≠ i"
shows "remove_idx i xs ! adjust_idx_rev i j = xs ! j" (is "?l = ?r")
proof -
let ?j = "adjust_idx_rev i j"
from i have ltake: "length (take i xs) = i" by simp
note nth_xs = arg_cong[where f = "λ xs. xs ! j", OF id_take_nth_drop[OF i], unfolded nth_append ltake]
show ?thesis
proof (cases "j < i")
case True
hence j: "?j = j" unfolding adjust_idx_rev_def by simp
show ?thesis unfolding nth_xs unfolding j remove_idx_def nth_append ltake
using True by simp
next
case False
with ji have ji: "j > i" by auto
hence j: "?j = j - Suc 0" unfolding adjust_idx_rev_def by simp
show ?thesis unfolding nth_xs unfolding j remove_idx_def nth_append ltake
using ji by auto
qed
qed
lemma adjust_idx_length:
assumes i: "i < length xs"
and j: "j < length (remove_idx i xs)"
shows "adjust_idx i j < length xs"
using j unfolding remove_idx_len[OF i] adjust_idx_def by (cases "j < i", auto)
lemma adjust_idx_rev_length:
assumes "i < length xs"
and "j < length xs"
and "j ≠ i"
shows "adjust_idx_rev i j < length (remove_idx i xs)"
using assms by (cases "j < i") (simp_all add: adjust_idx_rev_def remove_idx_len[OF assms(1)])
lemma [code_unfold]:
"(set xs = set ys) = (set xs ⊆ set ys ∧ set ys ⊆ set xs)"
by auto
lemma zip_size_aux: "size_list (size o snd) (zip ts ls) ≤ (size_list size ls)"
proof (induct ls arbitrary: ts)
case (Cons l ls ts)
thus ?case by (cases ts, auto)
qed auto
lemma option_map_cong[fundef_cong]: "xs = ys ⟹ ⟦⋀ x. ys = Some x ⟹ f x = g x⟧ ⟹ map_option f xs = map_option g ys"
by (cases ys, auto)
lemma finite_distinct: "finite { xs . distinct xs ∧ set xs = X}" (is "finite (?S X)")
proof (cases "finite X")
case False
with finite_set have id: "?S X = {}" by auto
show ?thesis unfolding id by auto
next
case True
show ?thesis
proof (induct rule: finite_induct[OF True])
case 1
show ?case by simp
next
case (2 x X)
let ?L = "{0..< card (insert x X)} × ?S X"
from 2(3)
have fin: "finite ?L" by auto
let ?f = "λ (i,xs). take i xs @ x # drop i xs"
show ?case
proof (rule finite_surj[OF fin, of _ ?f], rule)
fix xs
assume "xs ∈ ?S (insert x X)"
hence dis: "distinct xs" and set: "set xs = insert x X" by auto
from distinct_card[OF dis] have len: "length xs = card (set xs)" by auto
from set[unfolded set_conv_nth] obtain i where x: "x = xs ! i" and i: "i < length xs" by auto
from i have min: "min (length xs) i = i" by simp
let ?ys = "take i xs @ drop (Suc i) xs"
from id_take_nth_drop[OF i] have xsi: "xs = take i xs @ xs ! i # drop (Suc i) xs" .
also have "... = ?f (i,?ys)" unfolding split
by (simp add: min x)
finally have xs: "xs = ?f (i,?ys)" .
show "xs ∈ ?f ` ?L"
proof (rule image_eqI, rule xs, rule SigmaI)
show "i ∈ {0..<card (insert x X)}" using i[unfolded len] set[symmetric] by simp
next
from dis xsi have disxsi: "distinct (take i xs @ xs ! i # drop (Suc i) xs)" by simp
note disxsi = disxsi[unfolded distinct_append x[symmetric]]
have xys: "x ∉ set ?ys" using disxsi by auto
from distinct_take_drop[OF dis i]
have disys: "distinct ?ys" .
have "insert x (set ?ys) = set xs" unfolding arg_cong[OF xsi, of set] x by simp
hence "insert x (set ?ys) = insert x X" unfolding set by simp
from this[unfolded insert_eq_iff[OF xys 2(2)]]
show "?ys ∈ ?S X" using disys by auto
qed
qed
qed
qed
lemma finite_distinct_subset:
assumes "finite X"
shows "finite { xs . distinct xs ∧ set xs ⊆ X}" (is "finite (?S X)")
proof -
let ?X = "{ { xs. distinct xs ∧ set xs = Y} | Y. Y ⊆ X}"
have id: "?S X = ⋃ ?X" by blast
show ?thesis unfolding id
proof (rule finite_Union)
show "finite ?X" using assms by auto
next
fix M
assume "M ∈ ?X"
with finite_distinct show "finite M" by auto
qed
qed
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)
def 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 map_of_filter:
assumes "P x"
shows "map_of [(x',y) ← ys. P x'] x = map_of ys x"
proof (induct ys)
case (Cons xy ys)
obtain x' y where xy: "xy = (x',y)" by force
show ?case
by (cases "x' = x", insert assms xy Cons, auto)
qed simp
lemma infinite_imp_elem: "¬ finite A ⟹ ∃ x. x ∈ A"
by (cases "A = {}", auto)
lemma infinite_imp_many_elems:
"infinite A ⟹ ∃ xs. set xs ⊆ A ∧ length xs = n ∧ distinct xs"
proof (induct n arbitrary: A)
case (Suc n)
from infinite_imp_elem[OF Suc(2)] obtain x where x: "x ∈ A" by auto
from Suc(2) have "infinite (A - {x})" by auto
from Suc(1)[OF this] obtain xs where "set xs ⊆ A - {x}" and "length xs = n" and "distinct xs" by auto
with x show ?case by (intro exI[of _ "x # xs"], auto)
qed auto
lemma inf_pigeonhole_principle:
assumes "∀k::nat. ∃i<n::nat. f k i"
shows "∃i<n. ∀k. ∃k'≥k. f k' i"
proof -
have nfin: "~ finite (UNIV :: nat set)" by auto
have fin: "finite ({i. i < n})" by auto
from pigeonhole_infinite_rel[OF nfin fin] assms
obtain i where i: "i < n" and nfin: "¬ finite {a. f a i}" by auto
show ?thesis
proof (intro exI conjI, rule i, intro allI)
fix k
have "finite {a. f a i ∧ a < k}" by auto
with nfin have "¬ finite ({a. f a i} - {a. f a i ∧ a < k})" by auto
from infinite_imp_elem[OF this]
obtain a where "f a i" and "a ≥ k" by auto
thus "∃ k' ≥ k. f k' i" by force
qed
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
hence 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
hence "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 op # xs ys = xs @ ys"
by (induct xs) simp_all
lemma foldl_flip_Cons[simp]:
"foldl (flip op #) 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 ⇒ string ⇒ 'a ⇒ 'a" where "debug i t x = x"
section ‹Auxiliary Lemmas›
lemma (in order) rtranclp_less_eq [simp]:
"(op ≤)⇧*⇧* = op ≤"
by (intro ext) (auto elim: rtranclp_induct)
lemma (in order) tranclp_less [simp]:
"(op <)⇧+⇧+ = op <"
by (intro ext) (auto elim: tranclp_induct)
lemma (in order) rtranclp_greater_eq [simp]:
"(op ≥)⇧*⇧* = op ≥"
by (intro ext) (auto elim: rtranclp_induct)
lemma (in order) tranclp_greater [simp]:
"(op >)⇧+⇧+ = op >"
by (intro ext) (auto elim: tranclp_induct)
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 "op ≥" 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
lemma set_subset_insertI: "set xs ⊆ set (List.insert x xs)" by auto
lemma set_removeAll_subset: "set (removeAll x xs) ⊆ set xs" by auto
lemma all_less_two: "(∀ i < Suc (Suc 0). P i) = (P 0 ∧ P (Suc 0))" (is "?l = ?r")
proof
assume ?l thus ?r by auto
next
assume r: ?r
show ?l
proof(intro allI impI)
fix i
assume "i < Suc (Suc 0)"
hence "i = 0 ∨ i = Suc 0" by auto
with r show "P i" by auto
qed
qed
subsection ‹Induction Rules›
text ‹Induction over a finite set of natural numbers.›
lemma bound_nat_induct[consumes 1]:
assumes "n ∈ {l..u}" and "P l" and "⋀n. ⟦P n; n ∈ {l..<u}⟧ ⟹ P (Suc n)"
shows "P n"
using assms
proof (induct n)
case (Suc n) thus ?case by (cases "Suc n = l") auto
qed simp
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)
thus ?case by (cases "i = n", auto)
qed simp
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) = (listsum (map f xs) ≤ listsum (map g ys))"
unfolding size_list_conv_listsum assms(1) by auto
have "map f xs = map f (map (op ! 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 (op ! 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 listsum_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'"
hence "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 thus ?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 map_of_append_Some:
"map_of xs y = Some z ⟹ map_of (xs @ ys) y = Some z"
by (induction xs) auto
lemma map_of_append_None:
"map_of xs y = None ⟹ map_of (xs @ ys) y = map_of ys y"
by (induction xs) auto
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
thus ?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)
find_theorems "map_of" "_ ++ _"
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)))"
thus "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))"
hence "i = j" using partition[unfolded is_partition_alt is_partition_alt_def] by (cases "i = j", auto)
thus "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
thus ?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
hence 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
hence 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"
thus "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)"
thus "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
thus ?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)
hence P: "P (?sim i)" by simp
from someI_ex[OF step[OF P]]
show ?case by auto
qed
} note main = this
def 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 relpow_Suc: "r ^^ Suc n = r O r ^^ n"
using relpow_add[of 1 n r] by auto
lemma converse_power: fixes r :: "'a rel" shows "(r¯)^^n = (r^^n)¯"
proof (induct n)
case (Suc n)
show ?case unfolding relpow.simps(2)[of _ "r¯"] relpow_Suc[of _ r]
by (simp add: Suc converse_relcomp)
qed simp
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 trans_refl_imp_rtrancl_id:
assumes "trans r" "refl r"
shows "r⇧* = r"
proof
show "r⇧* ⊆ r"
proof
fix x y
assume "(x,y) ∈ r⇧*"
thus "(x,y) ∈ r"
by (induct, insert assms, unfold refl_on_def trans_def, blast+)
qed
qed regexp
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"
thus False
proof
assume "A ≠ C"
then obtain x where "x ∈ (A - C) ∨ x ∈ (C - A)" by auto
thus False by (rule disjE) (insert assms, auto)
next
assume "B ≠ D"
then obtain y where "y ∈ (B - D) ∨ y ∈ (D - B)" by auto
thus 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)
thus ?thesis by simp
next
case False
hence m_upd: "(m(a ↦ c)) k = m k" by simp
from upd[unfolded m_upd] have "x ∈ ran m" by (auto simp: ran_def)
thus ?thesis by simp
qed
qed
lemma subset_UNION_ran:
assumes "m a = Some b"
and "set b ⊆ set c"
shows "UNION (ran (m(a ↦ c))) set = UNION (insert c (ran m)) set"
proof
show "UNION (ran (m(a ↦ c))) set ⊆ UNION (insert c (ran m)) set"
proof
fix x assume "x ∈ UNION (ran (m(a ↦ c))) set"
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 ∈ UNION (insert c (ran m)) set" by auto
qed
next
show "UNION (insert c (ran m)) set ⊆ UNION (ran (m(a ↦ c))) set"
proof
fix x assume "x ∈ UNION (insert c (ran m)) set"
then obtain rs where "rs ∈ insert c (ran m)" and x: "x ∈ set rs" by auto
hence "c = rs ∨ rs ∈ ran m" by auto
thus "x ∈ UNION (ran (m(a ↦ c))) set"
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
end