theory Util
imports
"Polynomial_Factorization.Missing_List"
"HOL-Library.Infinite_Set"
HOL.Archimedean_Field
"Abstract-Rewriting.Relative_Rewriting"
begin
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 set_equality_code_unfold[code_unfold]:
"(set xs = set ys) = (set xs ⊆ set ys ∧ set ys ⊆ set xs)"
by (rule set_eq_subset)
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
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
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) = (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 (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 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'"
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 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 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"
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