Theory More_Lib
chapter "Misc. Definitions and Lemmas"
theory More_Lib
imports
Introduction_AutoCorres2
"HOL-Library.Prefix_Order"
"Word_Lib.Word_Lib_Sumo"
"HOL-Eisbach.Eisbach_Tools"
begin
abbreviation (input)
split :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a × 'b ⇒ 'c"
where
"split == case_prod"
lemma hd_map_simp:
"b ≠ [] ⟹ hd (map a b) = a (hd b)"
by (rule hd_map)
lemma tl_map_simp:
"tl (map a b) = map a (tl b)"
by (induct b,auto)
lemma Collect_eq:
"{x. P x} = {x. Q x} ⟷ (∀x. P x = Q x)"
by (rule iffI) auto
lemma iff_impI: "⟦P ⟹ Q = R⟧ ⟹ (P ⟶ Q) = (P ⟶ R)" by blast
definition
fun_app :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixr ‹$› 10) where
"f $ x ≡ f x"
declare fun_app_def [iff]
lemma fun_app_cong[fundef_cong]:
"⟦ f x = f' x' ⟧ ⟹ (f $ x) = (f' $ x')"
by simp
lemma fun_app_apply_cong[fundef_cong]:
"f x y = f' x' y' ⟹ (f $ x) y = (f' $ x') y'"
by simp
lemma if_apply_cong[fundef_cong]:
"⟦ P = P'; x = x'; P' ⟹ f x' = f' x'; ¬ P' ⟹ g x' = g' x' ⟧
⟹ (if P then f else g) x = (if P' then f' else g') x'"
by simp
lemma case_prod_apply_cong[fundef_cong]:
"⟦ f (fst p) (snd p) s = f' (fst p') (snd p') s' ⟧ ⟹ case_prod f p s = case_prod f' p' s'"
by (simp add: split_def)
lemma prod_injects:
"(x,y) = p ⟹ x = fst p ∧ y = snd p"
"p = (x,y) ⟹ x = fst p ∧ y = snd p"
by auto
definition
pred_imp :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ bool"
where
"pred_imp P Q ≡ ∀x. P x ⟶ Q x"
lemma pred_impI: "(⋀x. P x ⟹ Q x) ⟹ pred_imp P Q"
by (simp add: pred_imp_def)
definition
pred_conj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixl ‹and› 35)
where
"pred_conj P Q ≡ λx. P x ∧ Q x"
definition
pred_disj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixl ‹or› 30)
where
"pred_disj P Q ≡ λx. P x ∨ Q x"
definition
pred_neg :: "('a ⇒ bool) ⇒ ('a ⇒ bool)" (‹(‹open_block notation=‹prefix pred_neg››not _)› [40] 40)
where
"pred_neg P ≡ λx. ¬ P x"
lemma pred_neg_simp[simp]:
"(not P) s ⟷ ¬ (P s)"
by (simp add: pred_neg_def)
definition "K ≡ λx y. x"
definition
zipWith :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a list ⇒ 'b list ⇒ 'c list" where
"zipWith f xs ys ≡ map (case_prod f) (zip xs ys)"
primrec
delete :: "'a ⇒ 'a list ⇒ 'a list"
where
"delete y [] = []"
| "delete y (x#xs) = (if y=x then xs else x # delete y xs)"
definition
"swp f ≡ λx y. f y x"
lemma swp_apply[simp]: "swp f y x = f x y"
by (simp add: swp_def)
primrec (nonexhaustive)
theRight :: "'a + 'b ⇒ 'b" where
"theRight (Inr x) = x"
primrec (nonexhaustive)
theLeft :: "'a + 'b ⇒ 'a" where
"theLeft (Inl x) = x"
definition
"isLeft x ≡ (∃y. x = Inl y)"
definition
"isRight x ≡ (∃y. x = Inr y)"
definition
"const x ≡ λy. x"
primrec
opt_rel :: "('a ⇒ 'b ⇒ bool) ⇒ 'a option ⇒ 'b option ⇒ bool"
where
"opt_rel f None y = (y = None)"
| "opt_rel f (Some x) y = (∃y'. y = Some y' ∧ f x y')"
lemma opt_rel_None_rhs[simp]:
"opt_rel f x None = (x = None)"
by (cases x, simp_all)
lemma opt_rel_Some_rhs[simp]:
"opt_rel f x (Some y) = (∃x'. x = Some x' ∧ f x' y)"
by (cases x, simp_all)
lemma tranclD2:
"(x, y) ∈ R⇧+ ⟹ ∃z. (x, z) ∈ R⇧* ∧ (z, y) ∈ R"
by (erule tranclE) auto
lemma linorder_min_same1 [simp]:
"(min y x = y) = (y ≤ (x::'a::linorder))"
by (auto simp: min_def linorder_not_less)
lemma linorder_min_same2 [simp]:
"(min x y = y) = (y ≤ (x::'a::linorder))"
by (auto simp: min_def linorder_not_le)
text ‹A combinator for pairing up well-formed relations.
The divisor function splits the population in halves,
with the True half greater than the False half, and
the supplied relations control the order within the halves.›
definition
wf_sum :: "('a ⇒ bool) ⇒ ('a × 'a) set ⇒ ('a × 'a) set ⇒ ('a × 'a) set"
where
"wf_sum divisor r r' ≡
({(x, y). ¬ divisor x ∧ ¬ divisor y} ∩ r')
∪ {(x, y). ¬ divisor x ∧ divisor y}
∪ ({(x, y). divisor x ∧ divisor y} ∩ r)"
lemma wf_sum_wf:
"⟦ wf r; wf r' ⟧ ⟹ wf (wf_sum divisor r r')"
apply (simp add: wf_sum_def)
apply (rule wf_Un)+
apply (erule wf_Int2)
apply (rule wf_subset
[where r="measure (λx. If (divisor x) 1 0)"])
apply simp
apply clarsimp
apply blast
apply (erule wf_Int2)
apply blast
done
abbreviation(input)
"option_map == map_option"
lemmas option_map_def = map_option_case
lemma False_implies_equals [simp]:
"((False ⟹ P) ⟹ PROP Q) ≡ PROP Q"
apply (rule equal_intr_rule)
apply (erule meta_mp)
apply simp
apply simp
done
lemma split_paired_Ball:
"(∀x ∈ A. P x) = (∀x y. (x,y) ∈ A ⟶ P (x,y))"
by auto
lemma split_paired_Bex:
"(∃x ∈ A. P x) = (∃x y. (x,y) ∈ A ∧ P (x,y))"
by auto
lemma bexI_minus:
"⟦ P x; x ∈ A; x ∉ B ⟧ ⟹ ∃x ∈ A - B. P x"
unfolding Bex_def by blast
lemma delete_remove1:
"delete x xs = remove1 x xs"
by (induct xs, auto)
lemma ignore_if:
"(y and z) s ⟹ (if x then y else z) s"
by (clarsimp simp: pred_conj_def)
lemma zipWith_Nil2 :
"zipWith f xs [] = []"
unfolding zipWith_def by simp
lemma isRight_right_map:
"isRight (case_sum Inl (Inr o f) v) = isRight v"
by (simp add: isRight_def split: sum.split)
lemma zipWith_nth:
"⟦ n < min (length xs) (length ys) ⟧ ⟹ zipWith f xs ys ! n = f (xs ! n) (ys ! n)"
unfolding zipWith_def by simp
lemma length_zipWith [simp]:
"length (zipWith f xs ys) = min (length xs) (length ys)"
unfolding zipWith_def by simp
lemma first_in_uptoD:
"a ≤ b ⟹ (a::'a::order) ∈ {a..b}"
by simp
lemma construct_singleton:
"⟦ S ≠ {}; ∀s∈S. ∀s'. s ≠ s' ⟶ s' ∉ S ⟧ ⟹ ∃x. S = {x}"
by blast
lemmas insort_com = insort_left_comm
lemma bleeding_obvious:
"(P ⟹ True) ≡ (Trueprop True)"
by auto
lemma Some_helper:
"x = Some y ⟹ x ≠ None"
by simp
lemma in_empty_interE:
"⟦ A ∩ B = {}; x ∈ A; x ∈ B ⟧ ⟹ False"
by blast
lemma None_upd_eq:
"g x = None ⟹ g(x := None) = g"
by (rule ext) simp
lemma exx [iff]: "∃x. x" by blast
lemma ExNot [iff]: "Ex Not" by blast
lemma cases_simp2 [simp]:
"((¬ P ⟶ Q) ∧ (P ⟶ Q)) = Q"
by blast
lemma a_imp_b_imp_b:
"((a ⟶ b) ⟶ b) = (a ∨ b)"
by blast
lemma length_neq:
"length as ≠ length bs ⟹ as ≠ bs" by auto
lemma take_neq_length:
"⟦ x ≠ y; x ≤ length as; y ≤ length bs⟧ ⟹ take x as ≠ take y bs"
by (rule length_neq, simp)
lemma eq_concat_lenD:
"xs = ys @ zs ⟹ length xs = length ys + length zs"
by simp
lemma map_upt_reindex': "map f [a ..< b] = map (λn. f (n + a - x)) [x ..< x + b - a]"
by (rule nth_equalityI; clarsimp simp: add.commute)
lemma map_upt_reindex: "map f [a ..< b] = map (λn. f (n + a)) [0 ..< b - a]"
by (subst map_upt_reindex' [where x=0]) clarsimp
lemma notemptyI:
"x ∈ S ⟹ S ≠ {}"
by clarsimp
lemma setcomp_Max_has_prop:
assumes a: "P x"
shows "P (Max {(x::'a::{finite,linorder}). P x})"
proof -
from a have "Max {x. P x} ∈ {x. P x}"
by - (rule Max_in, auto intro: notemptyI)
thus ?thesis by auto
qed
lemma cons_set_intro:
"lst = x # xs ⟹ x ∈ set lst"
by fastforce
lemma list_all2_conj_nth:
assumes lall: "list_all2 P as cs"
and rl: "⋀n. ⟦P (as ! n) (cs ! n); n < length as⟧ ⟹ Q (as ! n) (cs ! n)"
shows "list_all2 (λa b. P a b ∧ Q a b) as cs"
proof (rule list_all2_all_nthI)
from lall show "length as = length cs" ..
next
fix n
assume "n < length as"
show "P (as ! n) (cs ! n) ∧ Q (as ! n) (cs ! n)"
proof
from lall show "P (as ! n) (cs ! n)" by (rule list_all2_nthD) fact
thus "Q (as ! n) (cs ! n)" by (rule rl) fact
qed
qed
lemma list_all2_conj:
assumes lall1: "list_all2 P as cs"
and lall2: "list_all2 Q as cs"
shows "list_all2 (λa b. P a b ∧ Q a b) as cs"
proof (rule list_all2_all_nthI)
from lall1 show "length as = length cs" ..
next
fix n
assume "n < length as"
show "P (as ! n) (cs ! n) ∧ Q (as ! n) (cs ! n)"
proof
from lall1 show "P (as ! n) (cs ! n)" by (rule list_all2_nthD) fact
from lall2 show "Q (as ! n) (cs ! n)" by (rule list_all2_nthD) fact
qed
qed
lemma all_set_into_list_all2:
assumes lall: "∀x ∈ set ls. P x"
and "length ls = length ls'"
shows "list_all2 (λa b. P a) ls ls'"
proof (rule list_all2_all_nthI)
fix n
assume "n < length ls"
from lall show "P (ls ! n)"
by (rule bspec [OF _ nth_mem]) fact
qed fact
lemma GREATEST_lessE:
fixes x :: "'a :: order"
assumes gts: "(GREATEST x. P x) < X"
and px: "P x"
and gtst: "∃max. P max ∧ (∀z. P z ⟶ (z ≤ max))"
shows "x < X"
proof -
from gtst obtain max where pm: "P max" and g': "⋀z. P z ⟹ z ≤ max"
by auto
hence "(GREATEST x. P x) = max"
by (auto intro: Greatest_equality)
moreover have "x ≤ max" using px by (rule g')
ultimately show ?thesis using gts by simp
qed
lemma set_has_max:
fixes ls :: "('a :: linorder) list"
assumes ls: "ls ≠ []"
shows "∃max ∈ set ls. ∀z ∈ set ls. z ≤ max"
using ls
proof (induct ls)
case Nil thus ?case by simp
next
case (Cons l ls)
show ?case
proof (cases "ls = []")
case True
thus ?thesis by simp
next
case False
then obtain max where mv: "max ∈ set ls" and mm: "∀z ∈ set ls. z ≤ max" using Cons.hyps
by auto
show ?thesis
proof (cases "max ≤ l")
case True
have "l ∈ set (l # ls)" by simp
thus ?thesis
proof
from mm show "∀z ∈ set (l # ls). z ≤ l" using True by auto
qed
next
case False
from mv have "max ∈ set (l # ls)" by simp
thus ?thesis
proof
from mm show "∀z ∈ set (l # ls). z ≤ max" using False by auto
qed
qed
qed
qed
lemma True_notin_set_replicate_conv:
"True ∉ set ls = (ls = replicate (length ls) False)"
by (induct ls) simp+
lemma Collect_singleton_eqI:
"(⋀x. P x = (x = v)) ⟹ {x. P x} = {v}"
by auto
lemma exEI:
"⟦ ∃y. P y; ⋀x. P x ⟹ Q x ⟧ ⟹ ∃z. Q z"
by (rule ex_forward)
lemma allEI:
assumes "∀x. P x"
assumes "⋀x. P x ⟹ Q x"
shows "∀x. Q x"
using assms by (rule all_forward)
text ‹General lemmas that should be in the library›
lemma dom_ran:
"x ∈ dom f ⟹ the (f x) ∈ ran f"
by (simp add: domD ranI)
lemma orthD1:
"⟦ S ∩ S' = {}; x ∈ S⟧ ⟹ x ∉ S'" by auto
lemma orthD2:
"⟦ S ∩ S' = {}; x ∈ S'⟧ ⟹ x ∉ S" by auto
lemma distinct_element:
"⟦ b ∩ d = {}; a ∈ b; c ∈ d⟧⟹ a ≠ c"
by auto
lemma ball_reorder:
"(∀x ∈ A. ∀y ∈ B. P x y) = (∀y ∈ B. ∀x ∈ A. P x y)"
by auto
lemma hd_map: "ls ≠ [] ⟹ hd (map f ls) = f (hd ls)"
by (cases ls) auto
lemma tl_map: "tl (map f ls) = map f (tl ls)"
by (cases ls) auto
lemma not_NilE:
"⟦ xs ≠ []; ⋀x xs'. xs = x # xs' ⟹ R ⟧ ⟹ R"
by (cases xs) auto
lemma length_SucE:
"⟦ length xs = Suc n; ⋀x xs'. xs = x # xs' ⟹ R ⟧ ⟹ R"
by (cases xs) auto
lemma map_upt_unfold:
assumes ab: "a < b"
shows "map f [a ..< b] = f a # map f [Suc a ..< b]"
using assms upt_conv_Cons by auto
lemma tl_nat_list_simp:
"tl [a..<b] = [a + 1 ..<b]"
by (induct b, auto)
lemma image_Collect2:
"case_prod f ` {x. P (fst x) (snd x)} = {f x y |x y. P x y}"
by (subst image_Collect) simp
lemma image_id':
"id ` Y = Y"
by clarsimp
lemma image_invert:
assumes r: "f ∘ g = id"
and g: "B = g ` A"
shows "A = f ` B"
by (simp add: g image_comp r)
lemma Collect_image_fun_cong:
assumes rl: "⋀a. P a ⟹ f a = g a"
shows "{f x | x. P x} = {g x | x. P x}"
using rl by force
lemma inj_on_take:
shows "inj_on (take n) {x. drop n x = k}"
proof (rule inj_onI)
fix x y
assume xv: "x ∈ {x. drop n x = k}"
and yv: "y ∈ {x. drop n x = k}"
and tk: "take n x = take n y"
from xv have "take n x @ k = x"
using append_take_drop_id mem_Collect_eq by auto
moreover from yv tk
have "take n x @ k = y"
using append_take_drop_id mem_Collect_eq by auto
ultimately show "x = y" by simp
qed
lemma foldr_upd_dom:
"dom (foldr (λp ps. ps (p ↦ f p)) as g) = dom g ∪ set as"
proof (induct as)
case Nil thus ?case by simp
next
case (Cons a as)
show ?case
proof (cases "a ∈ set as ∨ a ∈ dom g")
case True
hence ain: "a ∈ dom g ∪ set as" by auto
hence "dom g ∪ set (a # as) = dom g ∪ set as" by auto
thus ?thesis using Cons by fastforce
next
case False
hence "a ∉ (dom g ∪ set as)" by simp
hence "dom g ∪ set (a # as) = insert a (dom g ∪ set as)" by simp
thus ?thesis using Cons by fastforce
qed
qed
lemma foldr_upd_app:
assumes xin: "x ∈ set as"
shows "(foldr (λp ps. ps (p ↦ f p)) as g) x = Some (f x)"
(is "(?f as g) x = Some (f x)")
using xin
proof (induct as arbitrary: x)
case Nil thus ?case by simp
next
case (Cons a as)
from Cons.prems show ?case by (subst foldr.simps) (auto intro: Cons.hyps)
qed
lemma foldr_upd_app_other:
assumes xin: "x ∉ set as"
shows "(foldr (λp ps. ps (p ↦ f p)) as g) x = g x"
(is "(?f as g) x = g x")
using xin
proof (induct as arbitrary: x)
case Nil thus ?case by simp
next
case (Cons a as)
from Cons.prems show ?case
by (subst foldr.simps) (auto intro: Cons.hyps)
qed
lemma foldr_upd_app_if:
"foldr (λp ps. ps(p ↦ f p)) as g = (λx. if x ∈ set as then Some (f x) else g x)"
by (auto simp: foldr_upd_app foldr_upd_app_other)
lemma foldl_fun_upd_value:
"⋀Y. foldl (λf p. f(p := X p)) Y e p = (if p∈set e then X p else Y p)"
by (induct e) simp_all
lemma foldr_fun_upd_value:
"⋀Y. foldr (λp f. f(p := X p)) e Y p = (if p∈set e then X p else Y p)"
by (induct e) simp_all
lemma foldl_fun_upd_eq_foldr:
"!!m. foldl (λf p. f(p := g p)) m xs = foldr (λp f. f(p := g p)) xs m"
by (rule ext) (simp add: foldl_fun_upd_value foldr_fun_upd_value)
lemma Cons_eq_neq:
"⟦ y = x; x # xs ≠ y # ys ⟧ ⟹ xs ≠ ys"
by simp
lemma map_upt_append:
assumes lt: "x ≤ y"
and lt2: "a ≤ x"
shows "map f [a ..< y] = map f [a ..< x] @ map f [x ..< y]"
proof (subst map_append [symmetric], rule arg_cong [where f = "map f"])
from lt obtain k where ky: "x + k = y"
by (auto simp: le_iff_add)
thus "[a ..< y] = [a ..< x] @ [x ..< y]"
using lt2
by (auto intro: upt_add_eq_append)
qed
lemma Min_image_distrib:
assumes minf: "⋀x y. ⟦ x ∈ A; y ∈ A ⟧ ⟹ min (f x) (f y) = f (min x y)"
and fa: "finite A"
and ane: "A ≠ {}"
shows "Min (f ` A) = f (Min A)"
proof -
have rl: "⋀F. ⟦ F ⊆ A; F ≠ {} ⟧ ⟹ Min (f ` F) = f (Min F)"
proof -
fix F
assume fa: "F ⊆ A" and fne: "F ≠ {}"
have "finite F" by (rule finite_subset) fact+
thus "?thesis F"
unfolding min_def using fa fne fa
proof (induct rule: finite_subset_induct)
case empty
thus ?case by simp
next
case (insert x F)
thus ?case
by (cases "F = {}") (auto dest: Min_in intro: minf)
qed
qed
show ?thesis by (rule rl [OF order_refl]) fact+
qed
lemma min_of_mono':
assumes "(f a ≤ f c) = (a ≤ c)"
shows "min (f a) (f c) = f (min a c)"
unfolding min_def
by (subst if_distrib [where f = f, symmetric], rule arg_cong [where f = f], rule if_cong [OF _ refl refl]) fact+
lemma nat_diff_less:
fixes x :: nat
shows "⟦ x < y + z; z ≤ x⟧ ⟹ x - z < y"
using less_diff_conv2 by blast
lemma take_map_Not:
"(take n (map Not xs) = take n xs) = (n = 0 ∨ xs = [])"
by (cases n; simp) (cases xs; simp)
lemma union_trans:
assumes SR: "⋀x y z. ⟦ (x,y) ∈ S; (y,z) ∈ R ⟧ ⟹ (x,z) ∈ S^*"
shows "(R ∪ S)^* = R^* ∪ R^* O S^*"
apply (rule set_eqI)
apply clarsimp
apply (rule iffI)
apply (erule rtrancl_induct; simp)
apply (erule disjE)
apply (erule disjE)
apply (drule (1) rtrancl_into_rtrancl)
apply blast
apply clarsimp
apply (drule rtranclD [where R=S])
apply (erule disjE)
apply simp
apply (erule conjE)
apply (drule tranclD2)
apply (elim exE conjE)
apply (drule (1) SR)
apply (drule (1) rtrancl_trans)
apply blast
apply (rule disjI2)
apply (erule disjE)
apply (blast intro: in_rtrancl_UnI)
apply clarsimp
apply (drule (1) rtrancl_into_rtrancl)
apply (erule (1) relcompI)
apply (erule disjE)
apply (blast intro: in_rtrancl_UnI)
apply clarsimp
apply (blast intro: in_rtrancl_UnI rtrancl_trans)
done
lemma trancl_trancl:
"(R⇧+)⇧+ = R⇧+"
by auto
text ‹Some rules for showing that the reflexive transitive closure of a
relation/predicate doesn't add much if it was already transitively
closed.›
lemma rtrancl_eq_reflc_trans:
assumes trans: "trans X"
shows "rtrancl X = X ∪ Id"
by (simp only: rtrancl_trancl_reflcl trancl_id[OF trans])
lemma rtrancl_id:
assumes refl: "Id ⊆ X"
assumes trans: "trans X"
shows "rtrancl X = X"
using refl rtrancl_eq_reflc_trans[OF trans]
by blast
lemma rtranclp_eq_reflcp_transp:
assumes trans: "transp X"
shows "rtranclp X = (λx y. X x y ∨ x = y)"
by (simp add: Enum.rtranclp_rtrancl_eq fun_eq_iff
rtrancl_eq_reflc_trans trans[unfolded transp_trans])
lemma rtranclp_id:
shows "reflp X ⟹ transp X ⟹ rtranclp X = X"
apply (simp add: rtranclp_eq_reflcp_transp)
apply (auto simp: fun_eq_iff elim: reflpD)
done
lemmas rtranclp_id2 = rtranclp_id[unfolded reflp_def transp_relcompp le_fun_def]
lemma if_1_0_0:
"((if P then 1 else 0) = (0 :: ('a :: zero_neq_one))) = (¬ P)"
by (simp split: if_split)
lemma neq_Nil_lengthI:
"Suc 0 ≤ length xs ⟹ xs ≠ []"
by (cases xs, auto)
lemmas ex_with_length = Ex_list_of_length
lemma in_singleton:
"S = {x} ⟹ x ∈ S"
by simp
lemma singleton_set:
"x ∈ set [a] ⟹ x = a"
by auto
lemma take_drop_eqI:
assumes t: "take n xs = take n ys"
assumes d: "drop n xs = drop n ys"
shows "xs = ys"
proof -
have "xs = take n xs @ drop n xs" by simp
with t d
have "xs = take n ys @ drop n ys" by simp
moreover
have "ys = take n ys @ drop n ys" by simp
ultimately
show ?thesis by simp
qed
lemma append_len2:
"zs = xs @ ys ⟹ length xs = length zs - length ys"
by auto
lemma if_flip:
"(if ¬P then T else F) = (if P then F else T)"
by simp
lemma not_in_domIff:"f x = None = (x ∉ dom f)"
by blast
lemma not_in_domD:
"x ∉ dom f ⟹ f x = None"
by (simp add:not_in_domIff)
definition
"graph_of f ≡ {(x,y). f x = Some y}"
lemma graph_of_None_update:
"graph_of (f (p := None)) = graph_of f - {p} × UNIV"
by (auto simp: graph_of_def split: if_split_asm)
lemma graph_of_Some_update:
"graph_of (f (p ↦ v)) = (graph_of f - {p} × UNIV) ∪ {(p,v)}"
by (auto simp: graph_of_def split: if_split_asm)
lemma graph_of_restrict_map:
"graph_of (m |` S) ⊆ graph_of m"
by (simp add: graph_of_def restrict_map_def subset_iff)
lemma graph_ofD:
"(x,y) ∈ graph_of f ⟹ f x = Some y"
by (simp add: graph_of_def)
lemma graph_ofI:
"m x = Some y ⟹ (x, y) ∈ graph_of m"
by (simp add: graph_of_def)
lemma graph_of_empty :
"graph_of Map.empty = {}"
by (simp add: graph_of_def)
lemma graph_of_in_ranD: "∀y ∈ ran f. P y ⟹ (x,y) ∈ graph_of f ⟹ P y"
by (auto simp: graph_of_def ran_def)
lemma graph_of_SomeD:
"⟦ graph_of f ⊆ graph_of g; f x = Some y ⟧ ⟹ g x = Some y"
unfolding graph_of_def
by auto
lemma graph_of_comp:
"⟦ g x = y; f y = Some z ⟧ ⟹ (x,z) ∈ graph_of (f ∘ g)"
by (auto simp: graph_of_def)
lemma in_set_zip_refl :
"(x,y) ∈ set (zip xs xs) = (y = x ∧ x ∈ set xs)"
by (induct xs) auto
lemma map_conv_upd:
"m v = None ⟹ m o (f (x := v)) = (m o f) (x := None)"
by (rule ext) (clarsimp simp: o_def)
lemma sum_all_ex [simp]:
"(∀a. x ≠ Inl a) = (∃a. x = Inr a)"
"(∀a. x ≠ Inr a) = (∃a. x = Inl a)"
by (metis Inr_not_Inl sum.exhaust)+
lemma split_distrib: "case_prod (λa b. T (f a b)) = (λx. T (case_prod (λa b. f a b) x))"
by (clarsimp simp: split_def)
lemma case_sum_triv [simp]:
"(case x of Inl x ⇒ Inl x | Inr x ⇒ Inr x) = x"
by (clarsimp split: sum.splits)
lemma set_eq_UNIV: "({a. P a} = UNIV) = (∀a. P a)"
by force
lemma allE2:
"⟦∀x y. P x y; P x y ⟹ R⟧ ⟹ R"
by blast
lemma allE3: "⟦ ∀x y z. P x y z; P x y z ⟹ R ⟧ ⟹ R"
by auto
lemma my_BallE: "⟦ ∀x ∈ A. P x; y ∈ A; P y ⟹ Q ⟧ ⟹ Q"
by (simp add: Ball_def)
lemma unit_Inl_or_Inr [simp]:
"(a ≠ Inl ()) = (a = Inr ())"
"(a ≠ Inr ()) = (a = Inl ())"
by (cases a; clarsimp)+
lemma disjE_L: "⟦ a ∨ b; a ⟹ R; ⟦ ¬ a; b ⟧ ⟹ R ⟧ ⟹ R"
by blast
lemma disjE_R: "⟦ a ∨ b; ⟦ ¬ b; a ⟧ ⟹ R; ⟦ b ⟧ ⟹ R ⟧ ⟹ R"
by blast
lemma int_max_thms:
"(a :: int) ≤ max a b"
"(b :: int) ≤ max a b"
by (auto simp: max_def)
lemma sgn_negation [simp]:
"sgn (-(x::int)) = - sgn x"
by (clarsimp simp: sgn_if)
lemma sgn_sgn_nonneg [simp]:
"sgn (a :: int) * sgn a ≠ -1"
by (clarsimp simp: sgn_if)
lemma inj_inj_on:
"inj f ⟹ inj_on f A"
by (metis injD inj_onI)
lemma ex_eqI:
"⟦⋀x. f x = g x⟧ ⟹ (∃x. f x) = (∃x. g x)"
by simp
lemma pre_post_ex:
"⟦∃x. P x; ⋀x. P x ⟹ Q x⟧ ⟹ ∃x. Q x"
by auto
lemma ex_conj_increase:
"((∃x. P x) ∧ Q) = (∃x. P x ∧ Q)"
"(R ∧ (∃x. S x)) = (∃x. R ∧ S x)"
by simp+
lemma all_conj_increase:
"(( ∀x. P x) ∧ Q) = (∀x. P x ∧ Q)"
"(R ∧ (∀x. S x)) = (∀x. R ∧ S x)"
by simp+
lemma Ball_conj_increase:
"xs ≠ {} ⟹ (( ∀x ∈ xs. P x) ∧ Q) = (∀x ∈ xs. P x ∧ Q)"
"xs ≠ {} ⟹ (R ∧ (∀x ∈ xs. S x)) = (∀x ∈ xs. R ∧ S x)"
by auto
lemma disjoint_subset:
assumes "A' ⊆ A" and "A ∩ B = {}"
shows "A' ∩ B = {}"
using assms by auto
lemma disjoint_subset2:
assumes "B' ⊆ B" and "A ∩ B = {}"
shows "A ∩ B' = {}"
using assms by auto
lemma UN_nth_mem:
"i < length xs ⟹ f (xs ! i) ⊆ (⋃x∈set xs. f x)"
by (metis UN_upper nth_mem)
lemma Union_equal:
"f ` A = f ` B ⟹ (⋃x ∈ A. f x) = (⋃x ∈ B. f x)"
by blast
lemma UN_Diff_disjoint:
"i < length xs ⟹ (A - (⋃x∈set xs. f x)) ∩ f (xs ! i) = {}"
by (metis Diff_disjoint Int_commute UN_nth_mem disjoint_subset)
lemma image_list_update:
"f a = f (xs ! i)
⟹ f ` set (xs [i := a]) = f ` set xs"
by (metis list_update_id map_update set_map)
lemma Union_list_update_id:
"f a = f (xs ! i) ⟹ (⋃x∈set (xs [i := a]). f x) = (⋃x∈set xs. f x)"
by (rule Union_equal) (erule image_list_update)
lemma Union_list_update_id':
"⟦i < length xs; ⋀x. g (f x) = g x⟧
⟹ (⋃x∈set (xs [i := f (xs ! i)]). g x) = (⋃x∈set xs. g x)"
by (metis Union_list_update_id)
lemma Union_subset:
"⟦⋀x. x ∈ A ⟹ (f x) ⊆ (g x)⟧ ⟹ (⋃x ∈ A. f x) ⊆ (⋃x ∈ A. g x)"
by (metis UN_mono order_refl)
lemma UN_sub_empty:
"⟦list_all P xs; ⋀x. P x ⟹ f x = g x⟧ ⟹ (⋃x∈set xs. f x) - (⋃x∈set xs. g x) = {}"
by (simp add: Ball_set_list_all[symmetric] Union_subset)
lemma bij_betw_fun_updI:
"⟦x ∉ A; y ∉ B; bij_betw f A B⟧ ⟹ bij_betw (f(x := y)) (insert x A) (insert y B)"
by (clarsimp simp: bij_betw_def fun_upd_image inj_on_fun_updI split: if_split_asm; blast)
definition
"bij_betw_map f A B ≡ bij_betw f A (Some ` B)"
lemma bij_betw_map_fun_updI:
"⟦x ∉ A; y ∉ B; bij_betw_map f A B⟧
⟹ bij_betw_map (f(x ↦ y)) (insert x A) (insert y B)"
unfolding bij_betw_map_def by clarsimp (erule bij_betw_fun_updI; clarsimp)
lemma bij_betw_map_imp_inj_on:
"bij_betw_map f A B ⟹ inj_on f A"
by (simp add: bij_betw_map_def bij_betw_imp_inj_on)
lemma bij_betw_empty_dom_exists:
"r = {} ⟹ ∃t. bij_betw t {} r"
by (clarsimp simp: bij_betw_def)
lemma bij_betw_map_empty_dom_exists:
"r = {} ⟹ ∃t. bij_betw_map t {} r"
by (clarsimp simp: bij_betw_map_def bij_betw_empty_dom_exists)
lemma funpow_add [simp]:
fixes f :: "'a ⇒ 'a"
shows "(f ^^ a) ((f ^^ b) s) = (f ^^ (a + b)) s"
by (metis comp_apply funpow_add)
lemma funpow_unfold:
fixes f :: "'a ⇒ 'a"
assumes "n > 0"
shows "f ^^ n = (f ^^ (n - 1)) ∘ f"
by (metis Suc_diff_1 assms funpow_Suc_right)
lemma relpow_unfold: "n > 0 ⟹ S ^^ n = (S ^^ (n - 1)) O S"
by (cases n, auto)
definition
equiv_of :: "('s ⇒ 't) ⇒ ('s × 's) set"
where
"equiv_of proj ≡ {(a, b). proj a = proj b}"
lemma equiv_of_is_equiv_relation [simp]:
"equiv UNIV (equiv_of proj)"
by (auto simp: equiv_of_def intro!: equivI refl_onI symI transI)
lemma in_equiv_of [simp]:
"((a, b) ∈ equiv_of f) ⟷ (f a = f b)"
by (clarsimp simp: equiv_of_def)
lemma equiv_relation_to_projection:
fixes R :: "('a × 'a) set"
assumes equiv: "equiv UNIV R"
shows "∃f :: 'a ⇒ 'a set. ∀x y. f x = f y ⟷ (x, y) ∈ R"
apply (rule exI [of _ "λx. {y. (x, y) ∈ R}"])
apply clarsimp
subgoal for x y
apply (cases "(x, y) ∈ R")
apply clarsimp
apply (rule set_eqI)
apply clarsimp
apply (metis equivE sym_def trans_def equiv)
apply (clarsimp)
apply (metis UNIV_I equiv equivE mem_Collect_eq refl_on_def)
done
done
lemma range_constant [simp]:
"range (λ_. k) = {k}"
by (clarsimp simp: image_def)
lemma dom_unpack:
"dom (map_of (map (λx. (f x, g x)) xs)) = set (map (λx. f x) xs)"
by (simp add: dom_map_of_conv_image_fst image_image)
lemma fold_to_disj:
"fold (++) ms a x = Some y ⟹ (∃b ∈ set ms. b x = Some y) ∨ a x = Some y"
by (induct ms arbitrary:a x y; clarsimp) blast
lemma fold_ignore1:
"a x = Some y ⟹ fold (++) ms a x = Some y"
by (induct ms arbitrary:a x y; clarsimp)
lemma fold_ignore2:
"fold (++) ms a x = None ⟹ a x = None"
by (metis fold_ignore1 option.collapse)
lemma fold_ignore3:
"fold (++) ms a x = None ⟹ (∀b ∈ set ms. b x = None)"
by (induct ms arbitrary:a x; clarsimp) (meson fold_ignore2 map_add_None)
lemma fold_ignore4:
"b ∈ set ms ⟹ b x = Some y ⟹ ∃y. fold (++) ms a x = Some y"
using fold_ignore3 by fastforce
lemma dom_unpack2:
"dom (fold (++) ms Map.empty) = ⋃(set (map dom ms))"
apply (induct ms; clarsimp simp:dom_def)
apply (rule equalityI; clarsimp)
apply (drule fold_to_disj)
apply (erule disjE)
apply clarsimp
apply (rename_tac b)
apply (erule_tac x=b in ballE; clarsimp)
apply clarsimp
apply (rule conjI)
apply clarsimp
subgoal for _ _ _ y
apply (rule exI[where x = y])
apply (erule fold_ignore1)
done
apply clarsimp
apply (rename_tac y)
apply (erule_tac y=y in fold_ignore4; clarsimp)
done
lemma fold_ignore5:"fold (++) ms a x = Some y ⟹ a x = Some y ∨ (∃b ∈ set ms. b x = Some y)"
by (induct ms arbitrary:a x y; clarsimp) blast
lemma dom_inter_nothing:"dom f ∩ dom g = {} ⟹ ∀x. f x = None ∨ g x = None"
by auto
lemma fold_ignore6:
"f x = None ⟹ fold (++) ms f x = fold (++) ms Map.empty x"
apply (induct ms arbitrary:f x; clarsimp simp:map_add_def)
by (metis (no_types, lifting) fold_ignore1 option.collapse option.simps(4))
lemma fold_ignore7:
"m x = m' x ⟹ fold (++) ms m x = fold (++) ms m' x"
apply (cases "m x")
apply (frule_tac ms=ms in fold_ignore6)
apply (cut_tac f=m' and ms=ms and x=x in fold_ignore6)
apply clarsimp+
apply (rename_tac a)
apply (cut_tac ms=ms and a=m and x=x and y=a in fold_ignore1, clarsimp)
apply (cut_tac ms=ms and a=m' and x=x and y=a in fold_ignore1; clarsimp)
done
lemma fold_ignore8:
"fold (++) ms [x ↦ y] = (fold (++) ms Map.empty)(x ↦ y)"
apply (rule ext)
subgoal for xa
apply (cases "xa = x")
apply clarsimp
apply (rule fold_ignore1)
apply clarsimp
apply (subst fold_ignore6; clarsimp)
done
done
lemma fold_ignore9:
"⟦fold (++) ms [x ↦ y] x' = Some z; x = x'⟧ ⟹ y = z"
by (subst (asm) fold_ignore8) clarsimp
lemma fold_to_map_of:
"fold (++) (map (λx. [f x ↦ g x]) xs) Map.empty = map_of (map (λx. (f x, g x)) xs)"
apply (rule ext)
subgoal for x
apply (cases "fold (++) (map (λx. [f x ↦ g x]) xs) Map.empty x")
apply clarsimp
apply (drule fold_ignore3)
apply (clarsimp split:if_split_asm)
apply (rule sym)
apply (subst map_of_eq_None_iff)
apply clarsimp
apply (rename_tac xa)
apply (erule_tac x=xa in ballE; clarsimp)
apply clarsimp
apply (frule fold_ignore5; clarsimp split:if_split_asm)
apply (subst map_add_map_of_foldr[where m=Map.empty, simplified])
apply (induct xs arbitrary:f g; clarsimp split:if_split)
apply (rule conjI; clarsimp)
apply (drule fold_ignore9; clarsimp)
apply (cut_tac ms="map (λx. [f x ↦ g x]) xs" and f="[f a ↦ g a]" and x="f b" in fold_ignore6, clarsimp)
apply auto
done
done
lemma if_n_0_0:
"((if P then n else 0) ≠ 0) = (P ∧ n ≠ 0)"
by (simp split: if_split)
lemma insert_dom:
assumes fx: "f x = Some y"
shows "insert x (dom f) = dom f"
unfolding dom_def using fx by auto
lemma map_comp_subset_dom:
"dom (prj ∘⇩m f) ⊆ dom f"
unfolding dom_def
by (auto simp: map_comp_Some_iff)
lemmas map_comp_subset_domD = subsetD [OF map_comp_subset_dom]
lemma dom_map_comp:
"x ∈ dom (prj ∘⇩m f) = (∃y z. f x = Some y ∧ prj y = Some z)"
by (fastforce simp: dom_def map_comp_Some_iff)
lemma map_option_Some_eq2:
"(Some y = map_option f x) = (∃z. x = Some z ∧ f z = y)"
by (metis map_option_eq_Some)
lemma map_option_eq_dom_eq:
assumes ome: "map_option f ∘ g = map_option f ∘ g'"
shows "dom g = dom g'"
proof (rule set_eqI)
fix x
{
assume "x ∈ dom g"
hence "Some (f (the (g x))) = (map_option f ∘ g) x"
by (auto simp: map_option_case split: option.splits)
also have "… = (map_option f ∘ g') x" by (simp add: ome)
finally have "x ∈ dom g'"
by (auto simp: map_option_case split: option.splits)
} moreover
{
assume "x ∈ dom g'"
hence "Some (f (the (g' x))) = (map_option f ∘ g') x"
by (auto simp: map_option_case split: option.splits)
also have "… = (map_option f ∘ g) x" by (simp add: ome)
finally have "x ∈ dom g"
by (auto simp: map_option_case split: option.splits)
} ultimately show "(x ∈ dom g) = (x ∈ dom g')" by auto
qed
lemma cart_singleton_image:
"S × {s} = (λv. (v, s)) ` S"
by auto
lemma singleton_eq_o2s:
"({x} = set_option v) = (v = Some x)"
by (cases v, auto)
lemma option_set_singleton_eq:
"(set_option opt = {v}) = (opt = Some v)"
by (cases opt, simp_all)
lemmas option_set_singleton_eqs
= option_set_singleton_eq
trans[OF eq_commute option_set_singleton_eq]
lemma map_option_comp2:
"map_option (f o g) = map_option f o map_option g"
by (simp add: option.map_comp fun_eq_iff)
lemma compD:
"⟦f ∘ g = f ∘ g'; g x = v ⟧ ⟹ f (g' x) = f v"
by (metis comp_apply)
lemma map_option_comp_eqE:
assumes om: "map_option f ∘ mp = map_option f ∘ mp'"
and p1: "⟦ mp x = None; mp' x = None ⟧ ⟹ P"
and p2: "⋀v v'. ⟦ mp x = Some v; mp' x = Some v'; f v = f v' ⟧ ⟹ P"
shows "P"
proof (cases "mp x")
case None
hence "x ∉ dom mp" by (simp add: domIff)
hence "mp' x = None" by (simp add: map_option_eq_dom_eq [OF om] domIff)
with None show ?thesis by (rule p1)
next
case (Some v)
hence "x ∈ dom mp" by clarsimp
then obtain v' where Some': "mp' x = Some v'" by (clarsimp simp add: map_option_eq_dom_eq [OF om])
with Some show ?thesis
proof (rule p2)
show "f v = f v'" using Some' compD [OF om, OF Some] by simp
qed
qed
lemma Some_the:
"x ∈ dom f ⟹ f x = Some (the (f x))"
by clarsimp
lemma map_comp_update:
"f ∘⇩m (g(x ↦ v)) = (f ∘⇩m g)(x := f v)"
apply (intro ext)
subgoal for y by (cases "g y"; simp)
done
lemma restrict_map_eqI:
assumes req: "A |` S = B |` S"
and mem: "x ∈ S"
shows "A x = B x"
proof -
from mem have "A x = (A |` S) x" by simp
also have "… = (B |` S) x" using req by simp
also have "… = B x" using mem by simp
finally show ?thesis .
qed
lemma map_comp_eqI:
assumes dm: "dom g = dom g'"
and fg: "⋀x. x ∈ dom g' ⟹ f (the (g' x)) = f (the (g x))"
shows "f ∘⇩m g = f ∘⇩m g'"
apply (rule ext)
subgoal for x
apply (cases "x ∈ dom g")
apply (frule subst [OF dm])
apply (clarsimp split: option.splits)
apply (frule domI [where m = g'])
apply (drule fg)
apply simp
apply (frule subst [OF dm])
apply clarsimp
apply (drule not_sym)
apply (clarsimp simp: map_comp_Some_iff)
done
done
definition
"modify_map m p f ≡ m (p := map_option f (m p))"
lemma modify_map_id:
"modify_map m p id = m"
by (auto simp add: modify_map_def map_option_case split: option.splits)
lemma modify_map_addr_com:
assumes com: "x ≠ y"
shows "modify_map (modify_map m x g) y f = modify_map (modify_map m y f) x g"
by (rule ext) (simp add: modify_map_def map_option_case com split: option.splits)
lemma modify_map_dom :
"dom (modify_map m p f) = dom m"
unfolding modify_map_def by (auto simp: dom_def)
lemma modify_map_None:
"m x = None ⟹ modify_map m x f = m"
by (rule ext) (simp add: modify_map_def)
lemma modify_map_ndom :
"x ∉ dom m ⟹ modify_map m x f = m"
by (rule modify_map_None) clarsimp
lemma modify_map_app:
"(modify_map m p f) q = (if p = q then map_option f (m p) else m q)"
unfolding modify_map_def by simp
lemma modify_map_apply:
"m p = Some x ⟹ modify_map m p f = m (p ↦ f x)"
by (simp add: modify_map_def)
lemma modify_map_com:
assumes com: "⋀x. f (g x) = g (f x)"
shows "modify_map (modify_map m x g) y f = modify_map (modify_map m y f) x g"
using assms by (auto simp: modify_map_def map_option_case split: option.splits)
lemma modify_map_comp:
"modify_map m x (f o g) = modify_map (modify_map m x g) x f"
by (rule ext) (simp add: modify_map_def option.map_comp)
lemma modify_map_exists_eq:
"(∃cte. modify_map m p' f p= Some cte) = (∃cte. m p = Some cte)"
by (auto simp: modify_map_def split: if_splits)
lemma modify_map_other:
"p ≠ q ⟹ (modify_map m p f) q = (m q)"
by (simp add: modify_map_app)
lemma modify_map_same:
"modify_map m p f p = map_option f (m p)"
by (simp add: modify_map_app)
lemma next_update_is_modify:
"⟦ m p = Some cte'; cte = f cte' ⟧ ⟹ (m(p ↦ cte)) = modify_map m p f"
unfolding modify_map_def by simp
lemma nat_power_minus_less:
"a < 2 ^ (x - n) ⟹ (a :: nat) < 2 ^ x"
by (erule order_less_le_trans) simp
lemma neg_rtranclI:
"⟦ x ≠ y; (x, y) ∉ R⇧+ ⟧ ⟹ (x, y) ∉ R⇧*"
by (meson rtranclD)
lemma neg_rtrancl_into_trancl:
"¬ (x, y) ∈ R⇧* ⟹ ¬ (x, y) ∈ R⇧+"
by (erule contrapos_nn, erule trancl_into_rtrancl)
lemma set_neqI:
"⟦ x ∈ S; x ∉ S' ⟧ ⟹ S ≠ S'"
by clarsimp
lemma set_pair_UN:
"{x. P x} = ⋃ ((λxa. {xa} × {xb. P (xa, xb)}) ` {xa. ∃xb. P (xa, xb)})"
by fastforce
lemma singleton_elemD: "S = {x} ⟹ x ∈ S"
by simp
lemma singleton_eqD: "A = {x} ⟹ x ∈ A"
by blast
lemma ball_ran_fun_updI:
"⟦ ∀v ∈ ran m. P v; ∀v. y = Some v ⟶ P v ⟧ ⟹ ∀v ∈ ran (m (x := y)). P v"
by (auto simp add: ran_def)
lemma ball_ran_eq:
"(∀y ∈ ran m. P y) = (∀x y. m x = Some y ⟶ P y)"
by (auto simp add: ran_def)
lemma cart_helper:
"({} = {x} × S) = (S = {})"
by blast
lemmas converse_trancl_induct' = converse_trancl_induct [consumes 1, case_names base step]
lemma disjCI2: "(¬ P ⟹ Q) ⟹ P ∨ Q" by blast
lemma insert_UNIV :
"insert x UNIV = UNIV"
by blast
lemma not_singletonE:
"⟦ ∀p. S ≠ {p}; S ≠ {}; ⋀p p'. ⟦ p ≠ p'; p ∈ S; p' ∈ S ⟧ ⟹ R ⟧ ⟹ R"
by blast
lemma not_singleton_oneE:
"⟦ ∀p. S ≠ {p}; p ∈ S; ⋀p'. ⟦ p ≠ p'; p' ∈ S ⟧ ⟹ R ⟧ ⟹ R"
using not_singletonE by fastforce
lemma ball_ran_modify_map_eq:
"⟦ ∀v. m x = Some v ⟶ P (f v) = P v ⟧
⟹ (∀v ∈ ran (modify_map m x f). P v) = (∀v ∈ ran m. P v)"
by (auto simp: modify_map_def ball_ran_eq)
lemma eq_singleton_redux:
"⟦ S = {x} ⟧ ⟹ x ∈ S"
by simp
lemma if_eq_elem_helperE:
"⟦ x ∈ (if P then S else S'); ⟦ P; x ∈ S ⟧ ⟹ a = b; ⟦ ¬ P; x ∈ S' ⟧ ⟹ a = c ⟧
⟹ a = (if P then b else c)"
by fastforce
lemma if_option_Some:
"((if P then None else Some x) = Some y) = (¬P ∧ x = y)"
by simp
lemma insert_minus_eq:
"x ∉ A ⟹ A - S = (A - (S - {x}))"
by auto
lemma modify_map_K_D:
"modify_map m p (λx. y) p' = Some v ⟹ (m (p ↦ y)) p' = Some v"
by (simp add: modify_map_def split: if_split_asm)
lemma tranclE2:
assumes trancl: "(a, b) ∈ r⇧+"
and base: "(a, b) ∈ r ⟹ P"
and step: "⋀c. ⟦(a, c) ∈ r; (c, b) ∈ r⇧+⟧ ⟹ P"
shows "P"
using trancl base step
proof -
note rl = converse_trancl_induct [where P = "λx. x = a ⟶ P"]
from trancl have "a = a ⟶ P"
by (rule rl, (iprover intro: base step)+)
thus ?thesis by simp
qed
lemmas tranclE2' = tranclE2 [consumes 1, case_names base trancl]
lemma weak_imp_cong:
"⟦ P = R; Q = S ⟧ ⟹ (P ⟶ Q) = (R ⟶ S)"
by simp
lemma Collect_Diff_restrict_simp:
"T - {x ∈ T. Q x} = T - {x. Q x}"
by (auto intro: Collect_cong)
lemma Collect_Int_pred_eq:
"{x ∈ S. P x} ∩ {x ∈ T. P x} = {x ∈ (S ∩ T). P x}"
by (simp add: Collect_conj_eq [symmetric] conj_comms)
lemma Collect_restrict_predR:
"{x. P x} ∩ T = {} ⟹ {x. P x} ∩ {x ∈ T. Q x} = {}"
by (fastforce simp: disjoint_iff_not_equal)
lemma Diff_Un2:
assumes emptyad: "A ∩ D = {}"
and emptybc: "B ∩ C = {}"
shows "(A ∪ B) - (C ∪ D) = (A - C) ∪ (B - D)"
proof -
have "(A ∪ B) - (C ∪ D) = (A ∪ B - C) ∩ (A ∪ B - D)"
by (rule Diff_Un)
also have "… = ((A - C) ∪ B) ∩ (A ∪ (B - D))" using emptyad emptybc
by (simp add: Un_Diff Diff_triv)
also have "… = (A - C) ∪ (B - D)"
proof -
have "(A - C) ∩ (A ∪ (B - D)) = A - C" using emptyad emptybc
by (metis Diff_Int2 Diff_Int_distrib2 inf_sup_absorb)
moreover
have "B ∩ (A ∪ (B - D)) = B - D" using emptyad emptybc
by (metis Int_Diff Un_Diff Un_Diff_Int Un_commute Un_empty_left inf_sup_absorb)
ultimately show ?thesis
by (simp add: Int_Un_distrib2)
qed
finally show ?thesis .
qed
lemma ballEI:
"⟦ ∀x ∈ S. Q x; ⋀x. ⟦ x ∈ S; Q x ⟧ ⟹ P x ⟧ ⟹ ∀x ∈ S. P x"
by auto
lemma dom_if_None:
"dom (λx. if P x then None else f x) = dom f - {x. P x}"
by (simp add: dom_def) fastforce
lemma restrict_map_Some_iff:
"((m |` S) x = Some y) = (m x = Some y ∧ x ∈ S)"
by (cases "x ∈ S", simp_all)
lemma context_case_bools:
"⟦ ⋀v. P v ⟹ R v; ⟦ ¬ P v; ⋀v. P v ⟹ R v ⟧ ⟹ R v ⟧ ⟹ R v"
by (cases "P v", simp_all)
lemma inj_on_fun_upd_strongerI:
"⟦inj_on f A; y ∉ f ` (A - {x})⟧ ⟹ inj_on (f(x := y)) A"
by (fastforce simp: inj_on_def)
lemma less_handy_casesE:
"⟦ m < n; m = 0 ⟹ R; ⋀m' n'. ⟦ n = Suc n'; m = Suc m'; m < n ⟧ ⟹ R ⟧ ⟹ R"
by (cases n; simp) (cases m; simp)
lemma subset_drop_Diff_strg:
"(A ⊆ C) ⟶ (A - B ⊆ C)"
by blast
lemma inj_case_bool:
"inj (case_bool a b) = (a ≠ b)"
by (auto dest: inj_onD[where x=True and y=False] intro: inj_onI split: bool.split_asm)
lemma foldl_fun_upd:
"foldl (λs r. s (r := g r)) f rs = (λx. if x ∈ set rs then g x else f x)"
by (induct rs arbitrary: f) (auto simp: fun_eq_iff)
lemma all_rv_choice_fn_eq_pred:
"⟦ ⋀rv. P rv ⟹ ∃fn. f rv = g fn ⟧ ⟹ ∃fn. ∀rv. P rv ⟶ f rv = g (fn rv)"
apply (rule exI[where x="λrv. SOME h. f rv = g h"])
apply (clarsimp split: if_split)
by (meson someI_ex)
lemma ex_const_function:
"∃f. ∀s. f (f' s) = v"
by force
lemma if_Const_helper:
"If P (Con x) (Con y) = Con (If P x y)"
by (simp split: if_split)
lemmas if_Some_helper = if_Const_helper[where Con=Some]
lemma expand_restrict_map_eq:
"(m |` S = m' |` S) = (∀x. x ∈ S ⟶ m x = m' x)"
by (simp add: fun_eq_iff restrict_map_def split: if_split)
lemma disj_imp_rhs:
"(P ⟹ Q) ⟹ (P ∨ Q) = Q"
by blast
lemma remove1_filter:
"distinct xs ⟹ remove1 x xs = filter (λy. x ≠ y) xs"
by (induct xs) (auto intro!: filter_True [symmetric])
lemma Int_Union_empty:
"(⋀x. x ∈ S ⟹ A ∩ P x = {}) ⟹ A ∩ (⋃x ∈ S. P x) = {}"
by auto
lemma UN_Int_empty:
"(⋀x. x ∈ S ⟹ P x ∩ T = {}) ⟹ (⋃x ∈ S. P x) ∩ T = {}"
by auto
lemma disjointI:
"⟦⋀x y. ⟦ x ∈ A; y ∈ B ⟧ ⟹ x ≠ y ⟧ ⟹ A ∩ B = {}"
by auto
lemma UN_disjointI:
assumes rl: "⋀x y. ⟦ x ∈ A; y ∈ B ⟧ ⟹ P x ∩ Q y = {}"
shows "(⋃x ∈ A. P x) ∩ (⋃x ∈ B. Q x) = {}"
by (auto dest: rl)
lemma UN_set_member:
assumes sub: "A ⊆ (⋃x ∈ S. P x)"
and nz: "A ≠ {}"
shows "∃x ∈ S. P x ∩ A ≠ {}"
proof -
from nz obtain z where zA: "z ∈ A" by fastforce
with sub obtain x where "x ∈ S" and "z ∈ P x" by auto
hence "P x ∩ A ≠ {}" using zA by auto
thus ?thesis using sub nz by auto
qed
lemma append_Cons_cases [consumes 1, case_names pre mid post]:
"⟦(x, y) ∈ set (as @ b # bs);
(x, y) ∈ set as ⟹ R;
⟦(x, y) ∉ set as; (x, y) ∉ set bs; (x, y) = b⟧ ⟹ R;
(x, y) ∈ set bs ⟹ R⟧ ⟹ R"
by auto
lemma cart_singletons:
"{a} × {b} = {(a, b)}"
by blast
lemma disjoint_subset_neg1:
"⟦ B ∩ C = {}; A ⊆ B; A ≠ {} ⟧ ⟹ ¬ A ⊆ C"
by auto
lemma disjoint_subset_neg2:
"⟦ B ∩ C = {}; A ⊆ C; A ≠ {} ⟧ ⟹ ¬ A ⊆ B"
by auto
lemma iffE2:
"⟦ P = Q; ⟦ P; Q ⟧ ⟹ R; ⟦ ¬ P; ¬ Q ⟧ ⟹ R ⟧ ⟹ R"
by blast
lemma list_case_If:
"(case xs of [] ⇒ P | _ ⇒ Q) = (if xs = [] then P else Q)"
by (rule list.case_eq_if)
lemma remove1_Nil_in_set:
"⟦ remove1 x xs = []; xs ≠ [] ⟧ ⟹ x ∈ set xs"
by (induct xs) (auto split: if_split_asm)
lemma remove1_empty:
"(remove1 v xs = []) = (xs = [v] ∨ xs = [])"
by (cases xs; simp)
lemma set_remove1:
"x ∈ set (remove1 y xs) ⟹ x ∈ set xs"
by (induct xs) (auto split: if_split_asm)
lemma If_rearrage:
"(if P then if Q then x else y else z) = (if P ∧ Q then x else if P then y else z)"
by simp
lemma disjI2_strg:
"Q ⟶ (P ∨ Q)"
by simp
lemma eq_imp_strg:
"P t ⟶ (t = s ⟶ P s)"
by clarsimp
lemma if_both_strengthen:
"P ∧ Q ⟶ (if G then P else Q)"
by simp
lemma if_both_strengthen2:
"P s ∧ Q s ⟶ (if G then P else Q) s"
by simp
lemma if_swap:
"(if P then Q else R) = (if ¬P then R else Q)" by simp
lemma imp_consequent:
"P ⟶ Q ⟶ P" by simp
lemma list_case_helper:
"xs ≠ [] ⟹ case_list f g xs = g (hd xs) (tl xs)"
by (cases xs, simp_all)
lemma list_cons_rewrite:
"(∀x xs. L = x # xs ⟶ P x xs) = (L ≠ [] ⟶ P (hd L) (tl L))"
by (auto simp: neq_Nil_conv)
lemma list_not_Nil_manip:
"⟦ xs = y # ys; case xs of [] ⇒ False | (y # ys) ⇒ P y ys ⟧ ⟹ P y ys"
by simp
lemma ran_ball_triv:
"⋀P m S. ⟦ ∀x ∈ (ran S). P x ; m ∈ (ran S) ⟧ ⟹ P m"
by blast
lemma singleton_tuple_cartesian:
"({(a, b)} = S × T) = ({a} = S ∧ {b} = T)"
"(S × T = {(a, b)}) = ({a} = S ∧ {b} = T)"
by blast+
lemma strengthen_ignore_if:
"A s ∧ B s ⟶ (if P then A else B) s"
by clarsimp
lemma case_sum_True :
"(case r of Inl a ⇒ True | Inr b ⇒ f b) = (∀b. r = Inr b ⟶ f b)"
by (cases r) auto
lemma sym_ex_elim:
"F x = y ⟹ ∃x. y = F x"
by auto
lemma tl_drop_1 :
"tl xs = drop 1 xs"
by (simp add: drop_Suc)
lemma upt_lhs_sub_map:
"[x ..< y] = map ((+) x) [0 ..< y - x]"
by (induct y) (auto simp: Suc_diff_le)
lemma upto_0_to_4:
"[0..<4] = 0 # [1..<4]"
by (subst upt_rec) simp
lemma disjEI:
"⟦ P ∨ Q; P ⟹ R; Q ⟹ S ⟧
⟹ R ∨ S"
by fastforce
lemma dom_fun_upd2:
"s x = Some z ⟹ dom (s (x ↦ y)) = dom s"
by (simp add: insert_absorb domI)
lemma foldl_True :
"foldl (∨) True bs"
by (induct bs) auto
lemma image_set_comp:
"f ` {g x | x. Q x} = (f ∘ g) ` {x. Q x}"
by fastforce
lemma mutual_exE:
"⟦ ∃x. P x; ⋀x. P x ⟹ Q x ⟧ ⟹ ∃x. Q x"
by blast
lemma nat_diff_eq:
fixes x :: nat
shows "⟦ x - y = x - z; y < x⟧ ⟹ y = z"
by arith
lemma comp_upd_simp:
"(f ∘ (g (x := y))) = ((f ∘ g) (x := f y))"
by (rule fun_upd_comp)
lemma dom_option_map:
"dom (map_option f o m) = dom m"
by (rule dom_map_option_comp)
lemma drop_imp:
"P ⟹ (A ⟶ P) ∧ (B ⟶ P)" by blast
lemma inj_on_fun_updI2:
"⟦ inj_on f A; y ∉ f ` (A - {x}) ⟧ ⟹ inj_on (f(x := y)) A"
by (rule inj_on_fun_upd_strongerI)
lemma inj_on_fun_upd_elsewhere:
"x ∉ S ⟹ inj_on (f (x := y)) S = inj_on f S"
by (simp add: inj_on_def) blast
lemma not_Some_eq_tuple:
"(∀y z. x ≠ Some (y, z)) = (x = None)"
by (cases x, simp_all)
lemma ran_option_map:
"ran (map_option f o m) = f ` ran m"
by (auto simp add: ran_def)
lemma All_less_Ball:
"(∀x < n. P x) = (∀x∈{..< n}. P x)"
by fastforce
lemma Int_image_empty:
"⟦ ⋀x y. f x ≠ g y ⟧
⟹ f ` S ∩ g ` T = {}"
by auto
lemma Max_prop:
"⟦ Max S ∈ S ⟹ P (Max S); (S :: ('a :: {finite, linorder}) set) ≠ {} ⟧ ⟹ P (Max S)"
by auto
lemma Min_prop:
"⟦ Min S ∈ S ⟹ P (Min S); (S :: ('a :: {finite, linorder}) set) ≠ {} ⟧ ⟹ P (Min S)"
by auto
lemma findSomeD:
"find P xs = Some x ⟹ P x ∧ x ∈ set xs"
by (induct xs) (auto split: if_split_asm)
lemma findNoneD:
"find P xs = None ⟹ ∀x ∈ set xs. ¬P x"
by (induct xs) (auto split: if_split_asm)
lemma dom_upd:
"dom (λx. if x = y then None else f x) = dom f - {y}"
by (rule set_eqI) (auto split: if_split_asm)
definition
is_inv :: "('a ⇀ 'b) ⇒ ('b ⇀ 'a) ⇒ bool" where
"is_inv f g ≡ ran f = dom g ∧ (∀x y. f x = Some y ⟶ g y = Some x)"
lemma is_inv_NoneD:
assumes "g x = None"
assumes "is_inv f g"
shows "x ∉ ran f"
proof -
from assms
have "x ∉ dom g" by (auto simp: ran_def)
moreover
from assms
have "ran f = dom g"
by (simp add: is_inv_def)
ultimately
show ?thesis by simp
qed
lemma is_inv_SomeD:
"⟦ f x = Some y; is_inv f g ⟧ ⟹ g y = Some x"
by (simp add: is_inv_def)
lemma is_inv_com:
"is_inv f g ⟹ is_inv g f"
apply (unfold is_inv_def)
apply safe
apply (clarsimp simp: ran_def dom_def set_eq_iff)
apply (rename_tac a)
apply (erule_tac x=a in allE)
apply clarsimp
apply (clarsimp simp: ran_def dom_def set_eq_iff)
apply blast
apply (clarsimp simp: ran_def dom_def set_eq_iff)
apply (rename_tac x y)
apply (erule_tac x=x in allE)
apply clarsimp
done
lemma is_inv_inj:
"is_inv f g ⟹ inj_on f (dom f)"
apply (frule is_inv_com)
apply (clarsimp simp: inj_on_def)
apply (drule (1) is_inv_SomeD)
apply (auto dest: is_inv_SomeD)
done
lemma ran_upd':
"⟦inj_on f (dom f); f y =<