Theory AutoCorres2.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 = Some z⟧ ⟹ ran (f (y := None)) = ran f - {z}"
by (force simp: ran_def inj_on_def dom_def intro!: set_eqI)
lemma is_inv_None_upd:
"⟦ is_inv f g; g x = Some y⟧ ⟹ is_inv (f(y := None)) (g(x := None))"
apply (subst is_inv_def)
apply (clarsimp simp: dom_upd)
apply (drule is_inv_SomeD, erule is_inv_com)
apply (frule is_inv_inj)
apply (auto simp: ran_upd' is_inv_def dest: is_inv_SomeD is_inv_inj)
done
lemma is_inv_inj2:
"is_inv f g ⟹ inj_on g (dom g)"
using is_inv_com is_inv_inj by blast
text ‹Map inversion (implicitly assuming injectivity).›
definition
"the_inv_map m = (λs. if s∈ran m then Some (THE x. m x = Some s) else None)"
text ‹Map inversion can be expressed by function inversion.›
lemma the_inv_map_def2:
"the_inv_map m = (Some ∘ the_inv_into (dom m) (the ∘ m)) |` (ran m)"
apply (rule ext)
apply (clarsimp simp: the_inv_map_def the_inv_into_def dom_def)
apply (rule arg_cong[where f=The])
apply (rule ext)
apply auto
done
text ‹The domain of a function composition with Some is the universal set.›
lemma dom_comp_Some[simp]: "dom (comp Some f) = UNIV" by (simp add: dom_def)
text ‹Assuming injectivity, map inversion produces an inversive map.›
lemma is_inv_the_inv_map:
"inj_on m (dom m) ⟹ is_inv m (the_inv_map m)"
apply (simp add: is_inv_def)
apply (intro conjI allI impI)
apply (simp add: the_inv_map_def2)
apply (auto simp add: the_inv_map_def inj_on_def dom_def intro: ranI)
done
lemma the_the_inv_mapI:
"inj_on m (dom m) ⟹ m x = Some y ⟹ the (the_inv_map m y) = x"
by (auto simp: the_inv_map_def ran_def inj_on_def dom_def)
lemma eq_restrict_map_None:
"restrict_map m A x = None ⟷ x ~: (A ∩ dom m)"
by (auto simp: restrict_map_def split: if_split_asm)
lemma eq_the_inv_map_None[simp]: "the_inv_map m x = None ⟷ x∉ran m"
by (simp add: the_inv_map_def2 eq_restrict_map_None)
lemma is_inv_unique:
"is_inv f g ⟹ is_inv f h ⟹ g=h"
apply (rule ext)
subgoal for x
apply (clarsimp simp: is_inv_def dom_def Collect_eq ran_def)
apply (drule_tac x=x in spec)+
apply (cases "g x", clarsimp+)
done
done
lemma range_convergence1:
"⟦ ∀z. x < z ∧ z ≤ y ⟶ P z; ∀z > y. P (z :: 'a :: linorder) ⟧ ⟹ ∀z > x. P z"
using not_le by blast
lemma range_convergence2:
"⟦ ∀z. x < z ∧ z ≤ y ⟶ P z; ∀z. z > y ∧ z < w ⟶ P (z :: 'a :: linorder) ⟧
⟹ ∀z. z > x ∧ z < w ⟶ P z"
using range_convergence1[where P="λz. z < w ⟶ P z" and x=x and y=y]
by auto
lemma zip_upt_Cons:
"a < b ⟹ zip [a ..< b] (x # xs) = (a, x) # zip [Suc a ..< b] xs"
by (simp add: upt_conv_Cons)
lemma map_comp_eq:
"f ∘⇩m g = case_option None f ∘ g"
apply (rule ext)
subgoal for x by (cases "g x", auto)
done
lemma dom_If_Some:
"dom (λx. if x ∈ S then Some v else f x) = (S ∪ dom f)"
by (auto split: if_split)
lemma foldl_fun_upd_const:
"foldl (λs x. s(f x := v)) s xs
= (λx. if x ∈ f ` set xs then v else s x)"
by (induct xs arbitrary: s) auto
lemma foldl_id:
"foldl (λs x. s) s xs = s"
by (induct xs) auto
lemma SucSucMinus: "2 ≤ n ⟹ Suc (Suc (n - 2)) = n" by arith
lemma ball_to_all:
"(⋀x. (x ∈ A) = (P x)) ⟹ (∀x ∈ A. B x) = (∀x. P x ⟶ B x)"
by blast
lemma case_option_If:
"case_option P (λx. Q) v = (if v = None then P else Q)"
by clarsimp
lemma case_option_If2:
"case_option P Q v = If (v ≠ None) (Q (the v)) P"
by (simp split: option.split)
lemma if3_fold:
"(if P then x else if Q then y else x) = (if P ∨ ¬ Q then x else y)"
by simp
lemma rtrancl_insert:
assumes x_new: "⋀y. (x,y) ∉ R"
shows "R^* `` insert x S = insert x (R^* `` S)"
proof -
have "R^* `` insert x S = R^* `` ({x} ∪ S)" by simp
also
have "R^* `` ({x} ∪ S) = R^* `` {x} ∪ R^* `` S"
by (subst Image_Un) simp
also
have "R^* `` {x} = {x}"
by (meson Image_closed_trancl Image_singleton_iff subsetI x_new)
finally
show ?thesis by simp
qed
lemma ran_del_subset:
"y ∈ ran (f (x := None)) ⟹ y ∈ ran f"
by (auto simp: ran_def split: if_split_asm)
lemma trancl_sub_lift:
assumes sub: "⋀p p'. (p,p') ∈ r ⟹ (p,p') ∈ r'"
shows "(p,p') ∈ r^+ ⟹ (p,p') ∈ r'^+"
by (fastforce intro: trancl_mono sub)
lemma trancl_step_lift:
assumes x_step: "⋀p p'. (p,p') ∈ r' ⟹ (p,p') ∈ r ∨ (p = x ∧ p' = y)"
assumes y_new: "⋀p'. ¬(y,p') ∈ r"
shows "(p,p') ∈ r'^+ ⟹ (p,p') ∈ r^+ ∨ ((p,x) ∈ r^+ ∧ p' = y) ∨ (p = x ∧ p' = y)"
apply (erule trancl_induct)
apply (drule x_step)
apply fastforce
apply (erule disjE)
apply (drule x_step)
apply (erule disjE)
apply (drule trancl_trans, drule r_into_trancl, assumption)
apply blast
apply fastforce
apply (fastforce simp: y_new dest: x_step)
done
lemma rtrancl_simulate_weak:
assumes r: "(x,z) ∈ R⇧*"
assumes s: "⋀y. (x,y) ∈ R ⟹ (y,z) ∈ R⇧* ⟹ (x,y) ∈ R' ∧ (y,z) ∈ R'⇧*"
shows "(x,z) ∈ R'⇧*"
apply (rule converse_rtranclE[OF r])
apply simp
apply (frule (1) s)
apply clarsimp
by (rule converse_rtrancl_into_rtrancl)
lemma list_case_If2:
"case_list f g xs = If (xs = []) f (g (hd xs) (tl xs))"
by (simp split: list.split)
lemma length_ineq_not_Nil:
"length xs > n ⟹ xs ≠ []"
"length xs ≥ n ⟹ n ≠ 0 ⟶ xs ≠ []"
"¬ length xs < n ⟹ n ≠ 0 ⟶ xs ≠ []"
"¬ length xs ≤ n ⟹ xs ≠ []"
by auto
lemma numeral_eqs:
"2 = Suc (Suc 0)"
"3 = Suc (Suc (Suc 0))"
"4 = Suc (Suc (Suc (Suc 0)))"
"5 = Suc (Suc (Suc (Suc (Suc 0))))"
"6 = Suc (Suc (Suc (Suc (Suc (Suc 0)))))"
by simp+
lemma psubset_singleton:
"(S ⊂ {x}) = (S = {})"
by blast
lemma length_takeWhile_ge:
"length (takeWhile f xs) = n ⟹ length xs = n ∨ (length xs > n ∧ ¬ f (xs ! n))"
by (induct xs arbitrary: n) (auto split: if_split_asm)
lemma length_takeWhile_le:
"¬ f (xs ! n) ⟹ length (takeWhile f xs) ≤ n"
apply (induct xs arbitrary: n; simp)
subgoal for x xs n by (cases n; simp)
done
lemma length_takeWhile_gt:
"n < length (takeWhile f xs)
⟹ (∃ys zs. length ys = Suc n ∧ xs = ys @ zs ∧ takeWhile f xs = ys @ takeWhile f zs)"
apply (induct xs arbitrary: n; simp split: if_split_asm)
subgoal for a xs n
apply (cases n; simp)
apply (rule exI[where x="[a]"])
apply simp
apply (erule meta_allE, drule(1) meta_mp)
apply clarsimp
subgoal for _ ys zs
apply (rule exI[where x="a # ys"])
apply simp
done
done
done
lemma hd_drop_conv_nth2:
"n < length xs ⟹ hd (drop n xs) = xs ! n"
by (rule hd_drop_conv_nth) clarsimp
lemma map_upt_eq_vals_D:
"⟦ map f [0 ..< n] = ys; m < length ys ⟧ ⟹ f m = ys ! m"
by clarsimp
lemma length_le_helper:
"⟦ n ≤ length xs; n ≠ 0 ⟧ ⟹ xs ≠ [] ∧ n - 1 ≤ length (tl xs)"
by (cases xs, simp_all)
lemma all_ex_eq_helper:
"(∀v. (∃v'. v = f v' ∧ P v v') ⟶ Q v)
= (∀v'. P (f v') v' ⟶ Q (f v'))"
by auto
lemma nat_less_cases':
"(x::nat) < y ⟹ x = y - 1 ∨ x < y - 1"
by auto
lemma less_numeral_nat_iff_disj:
"(n::nat) < numeral m ⟷ n = numeral m - 1 ∨ n < numeral m - 1"
apply clarsimp
using less_SucE numeral_eq_Suc by presburger
lemma filter_to_shorter_upto:
"n ≤ m ⟹ filter (λx. x < n) [0 ..< m] = [0 ..< n]"
by (induct m) (auto elim: le_SucE)
lemma in_emptyE: "⟦ A = {}; x ∈ A ⟧ ⟹ P" by blast
lemma Ball_emptyI:
"S = {} ⟹ (∀x ∈ S. P x)"
by simp
lemma allfEI:
"⟦ ∀x. P x; ⋀x. P (f x) ⟹ Q x ⟧ ⟹ ∀x. Q x"
by fastforce
lemma cart_singleton_empty2:
"({x} × S = {}) = (S = {})"
"({} = S × {e}) = (S = {})"
by auto
lemma cases_simp_conj:
"((P ⟶ Q) ∧ (¬ P ⟶ Q) ∧ R) = (Q ∧ R)"
by fastforce
lemma domE :
"⟦ x ∈ dom m; ⋀r. ⟦m x = Some r⟧ ⟹ P ⟧ ⟹ P"
by clarsimp
lemma dom_eqD:
"⟦ f x = Some v; dom f = S ⟧ ⟹ x ∈ S"
by clarsimp
lemma exception_set_finite1:
"finite {x. P x} ⟹ finite {x. (x = y ⟶ Q x) ∧ P x}"
by (simp add: Collect_conj_eq)
lemma exception_set_finite2:
"finite {x. P x} ⟹ finite {x. x ≠ y ⟶ P x}"
by (simp add: imp_conv_disj)
lemmas exception_set_finite = exception_set_finite1 exception_set_finite2
lemma exfEI:
"⟦ ∃x. P x; ⋀x. P x ⟹ Q (f x) ⟧ ⟹ ∃x. Q x"
by fastforce
lemma Collect_int_vars:
"{s. P rv s} ∩ {s. rv = xf s} = {s. P (xf s) s} ∩ {s. rv = xf s}"
by auto
lemma if_0_1_eq:
"((if P then 1 else 0) = (case Q of True ⇒ of_nat 1 | False ⇒ of_nat 0)) = (P = Q)"
by (simp split: if_split bool.split)
lemma modify_map_exists_cte :
"(∃cte. modify_map m p f p' = Some cte) = (∃cte. m p' = Some cte)"
by (simp add: modify_map_def)
lemma dom_eqI:
assumes c1: "⋀x y. P x = Some y ⟹ ∃y. Q x = Some y"
and c2: "⋀x y. Q x = Some y ⟹ ∃y. P x = Some y"
shows "dom P = dom Q"
unfolding dom_def by (auto simp: c1 c2)
lemma dvd_reduce_multiple:
fixes k :: nat
shows "(k dvd k * m + n) = (k dvd n)"
by (induct m) (auto simp: add_ac)
lemma image_iff2:
"inj f ⟹ f x ∈ f ` S = (x ∈ S)"
by (rule inj_image_mem_iff)
lemma map_comp_restrict_map_Some_iff:
"((g ∘⇩m (m |` S)) x = Some y) = ((g ∘⇩m m) x = Some y ∧ x ∈ S)"
by (auto simp add: map_comp_Some_iff restrict_map_Some_iff)
lemma range_subsetD:
fixes a :: "'a :: order"
shows "⟦ {a..b} ⊆ {c..d}; a ≤ b ⟧ ⟹ c ≤ a ∧ b ≤ d"
by simp
lemma case_option_dom:
"(case f x of None ⇒ a | Some v ⇒ b v) = (if x ∈ dom f then b (the (f x)) else a)"
by (auto split: option.split)
lemma contrapos_imp:
"P ⟶ Q ⟹ ¬ Q ⟶ ¬ P"
by clarsimp
lemma filter_eq_If:
"distinct xs ⟹ filter (λv. v = x) xs = (if x ∈ set xs then [x] else [])"
by (induct xs) auto
lemma (in semigroup_add) foldl_assoc:
shows "foldl (+) (x+y) zs = x + (foldl (+) y zs)"
by (induct zs arbitrary: y) (simp_all add:add.assoc)
lemma (in monoid_add) foldl_absorb0:
shows "x + (foldl (+) 0 zs) = foldl (+) x zs"
by (induct zs) (simp_all add:foldl_assoc)
lemma foldl_conv_concat:
"foldl (@) xs xss = xs @ concat xss"
proof (induct xss arbitrary: xs)
case Nil show ?case by simp
next
interpret monoid_add "(@)" "[]" proof qed simp_all
case Cons then show ?case by (simp add: foldl_absorb0)
qed
lemma foldl_concat_concat:
"foldl (@) [] (xs @ ys) = foldl (@) [] xs @ foldl (@) [] ys"
by (simp add: foldl_conv_concat)
lemma foldl_does_nothing:
"⟦ ⋀x. x ∈ set xs ⟹ f s x = s ⟧ ⟹ foldl f s xs = s"
by (induct xs) auto
lemma foldl_use_filter:
"⟦ ⋀v x. ⟦ ¬ g x; x ∈ set xs ⟧ ⟹ f v x = v ⟧ ⟹ foldl f v xs = foldl f v (filter g xs)"
by (induct xs arbitrary: v) auto
lemma map_comp_update_lift:
assumes fv: "f v = Some v'"
shows "(f ∘⇩m (g(ptr ↦ v))) = ((f ∘⇩m g)(ptr ↦ v'))"
by (simp add: fv map_comp_update)
lemma restrict_map_cong:
assumes sv: "S = S'"
and rl: "⋀p. p ∈ S' ⟹ mp p = mp' p"
shows "mp |` S = mp' |` S'"
using expand_restrict_map_eq rl sv by auto
lemma case_option_over_if:
"case_option P Q (if G then None else Some v)
= (if G then P else Q v)"
"case_option P Q (if G then Some v else None)
= (if G then Q v else P)"
by (simp split: if_split)+
lemma map_length_cong:
"⟦ length xs = length ys; ⋀x y. (x, y) ∈ set (zip xs ys) ⟹ f x = g y ⟧
⟹ map f xs = map g ys"
apply atomize
apply (erule rev_mp, erule list_induct2)
apply auto
done
lemma take_min_len:
"take (min (length xs) n) xs = take n xs"
by (simp add: min_def)
lemmas interval_empty = atLeastatMost_empty_iff
lemma fold_and_false[simp]:
"¬(fold (∧) xs False)"
apply clarsimp
apply (induct xs)
apply simp
apply simp
done
lemma fold_and_true:
"fold (∧) xs True ⟹ ∀i < length xs. xs ! i"
apply clarsimp
apply (induct xs)
apply simp
subgoal for a xs i
by (cases "i = 0"; cases a; auto)
done
lemma fold_or_true[simp]:
"fold (∨) xs True"
by (induct xs, simp+)
lemma fold_or_false:
"¬(fold (∨) xs False) ⟹ ∀i < length xs. ¬(xs ! i)"
apply (induct xs, simp+)
subgoal for a xs
apply (cases a, simp+)
apply (rule allI)
subgoal for i by (cases "i = 0", simp+)
done
done
section ‹ Take, drop, zip, ‹list_all› etc rules ›
method two_induct for xs ys =
((induct xs arbitrary: ys; simp?), (case_tac ys; simp)?)
lemma map_fst_zip_prefix:
"map fst (zip xs ys) ≤ xs"
by (two_induct xs ys)
lemma map_snd_zip_prefix:
"map snd (zip xs ys) ≤ ys"
by (two_induct xs ys)
lemma nth_upt_0 [simp]:
"i < length xs ⟹ [0..<length xs] ! i = i"
by simp
lemma take_insert_nth:
"i < length xs⟹ insert (xs ! i) (set (take i xs)) = set (take (Suc i) xs)"
by (subst take_Suc_conv_app_nth, assumption, fastforce)
lemma zip_take_drop:
"⟦n < length xs; length ys = length xs⟧ ⟹
zip xs (take n ys @ a # drop (Suc n) ys) =
zip (take n xs) (take n ys) @ (xs ! n, a) # zip (drop (Suc n) xs) (drop (Suc n) ys)"
by (subst id_take_nth_drop, assumption, simp)
lemma take_nth_distinct:
"⟦distinct xs; n < length xs; xs ! n ∈ set (take n xs)⟧ ⟹ False"
by (fastforce simp: distinct_conv_nth in_set_conv_nth)
lemma take_drop_append:
"drop a xs = take b (drop a xs) @ drop (a + b) xs"
by (metis append_take_drop_id drop_drop add.commute)
lemma drop_take_drop:
"drop a (take (b + a) xs) @ drop (b + a) xs = drop a xs"
by (metis add.commute take_drop take_drop_append)
lemma not_prefixI:
"⟦ xs ≠ ys; length xs = length ys⟧ ⟹ ¬ xs ≤ ys"
by (auto elim: prefixE)
lemma map_fst_zip':
"length xs ≤ length ys ⟹ map fst (zip xs ys) = xs"
by (metis length_map length_zip map_fst_zip_prefix min_absorb1 not_prefixI)
lemma zip_take_triv:
"n ≥ length bs ⟹ zip (take n as) bs = zip as bs"
apply (induct bs arbitrary: n as; simp)
subgoal for a bs n as by (cases n; cases "as"; simp)
done
lemma zip_take_triv2:
"length as ≤ n ⟹ zip as (take n bs) = zip as bs"
apply (induct as arbitrary: n bs; simp)
subgoal for a bs n as by (cases n; cases "as"; simp)
done
lemma zip_take_length:
"zip xs (take (length xs) ys) = zip xs ys"
by (metis order_refl zip_take_triv2)
lemma zip_singleton:
"ys ≠ [] ⟹ zip [a] ys = [(a, ys ! 0)]"
by (cases ys, simp_all)
lemma zip_append_singleton:
"⟦i = length xs; length xs < length ys⟧ ⟹ zip (xs @ [a]) ys = (zip xs ys) @ [(a,ys ! i)]"
by (induct xs; cases ys; simp)
(clarsimp simp: zip_append1 zip_take_length zip_singleton)
lemma ranE:
"⟦ v ∈ ran f; ⋀x. f x = Some v ⟹ R⟧ ⟹ R"
by (auto simp: ran_def)
lemma ran_map_option_restrict_eq:
"⟦ x ∈ ran (map_option f o g); x ∉ ran (map_option f o (g |` (- {y}))) ⟧
⟹ ∃v. g y = Some v ∧ f v = x"
apply (clarsimp simp: elim!: ranE)
subgoal for w z
apply (cases "w = y")
apply clarsimp
apply (erule notE, rule ranI[where a=w])
apply (simp add: restrict_map_def)
done
done
lemma map_of_zip_range:
"⟦length xs = length ys; distinct xs⟧ ⟹ (λx. (the (map_of (zip xs ys) x))) ` set xs = set ys"
apply (clarsimp simp: image_def)
apply (subst ran_map_of_zip [symmetric, where xs=xs and ys=ys]; simp?)
apply (clarsimp simp: ran_def)
apply (rule equalityI)
apply clarsimp
apply (rename_tac x)
apply (frule_tac x=x in map_of_zip_is_Some; fastforce)
apply (clarsimp simp: set_zip)
by (metis domI dom_map_of_zip nth_mem ranE ran_map_of_zip option.sel)
lemma map_zip_fst:
"length xs = length ys ⟹ map (λ(x, y). f x) (zip xs ys) = map f xs"
by (two_induct xs ys)
lemma map_zip_fst':
"length xs ≤ length ys ⟹ map (λ(x, y). f x) (zip xs ys) = map f xs"
by (metis length_map map_fst_zip' map_zip_fst zip_map_fst_snd)
lemma map_zip_snd:
"length xs = length ys ⟹ map (λ(x, y). f y) (zip xs ys) = map f ys"
by (two_induct xs ys)
lemma map_zip_snd':
"length ys ≤ length xs ⟹ map (λ(x, y). f y) (zip xs ys) = map f ys"
by (two_induct xs ys)
lemma map_of_zip_tuple_in:
"⟦(x, y) ∈ set (zip xs ys); distinct xs⟧ ⟹ map_of (zip xs ys) x = Some y"
by (two_induct xs ys) (auto intro: in_set_zipE)
lemma in_set_zip1:
"(x, y) ∈ set (zip xs ys) ⟹ x ∈ set xs"
by (erule in_set_zipE)
lemma in_set_zip2:
"(x, y) ∈ set (zip xs ys) ⟹ y ∈ set ys"
by (erule in_set_zipE)
lemma map_zip_snd_take:
"map (λ(x, y). f y) (zip xs ys) = map f (take (length xs) ys)"
apply (subst map_zip_snd' [symmetric, where xs=xs and ys="take (length xs) ys"], simp)
apply (subst zip_take_length [symmetric], simp)
done
lemma map_of_zip_is_index:
"⟦length xs = length ys; x ∈ set xs⟧ ⟹ ∃i. (map_of (zip xs ys)) x = Some (ys ! i)"
apply (induct rule: list_induct2; simp)
apply (rule conjI; clarsimp)
apply (metis nth_Cons_0)
apply (metis nth_Cons_Suc)
done
lemma map_of_zip_take_update:
"⟦i < length xs; length xs ≤ length ys; distinct xs⟧
⟹ (map_of (zip (take i xs) ys))(xs ! i ↦ (ys ! i)) = map_of (zip (take (Suc i) xs) ys)"
apply (rule ext)
subgoal for x
apply (cases "x=xs ! i"; clarsimp)
apply (rule map_of_is_SomeI[symmetric])
apply (simp add: map_fst_zip')
apply (force simp add: set_zip)
apply (clarsimp simp: take_Suc_conv_app_nth zip_append_singleton map_add_def split: option.splits)
done
done
lemma map_of_zip_is_Some':
"length xs ≤ length ys ⟹ (x ∈ set xs) = (∃y. map_of (zip xs ys) x = Some y)"
apply (subst zip_take_length[symmetric])
apply (rule map_of_zip_is_Some)
by (metis length_take min_absorb2)
lemma map_of_zip_inj:
"⟦distinct xs; distinct ys; length xs = length ys⟧
⟹ inj_on (λx. (the (map_of (zip xs ys) x))) (set xs)"
apply (clarsimp simp: inj_on_def)
apply (subst (asm) map_of_zip_is_Some, assumption)+
apply clarsimp
apply (clarsimp simp: set_zip)
by (metis nth_eq_iff_index_eq)
lemma map_of_zip_inj':
"⟦distinct xs; distinct ys; length xs ≤ length ys⟧
⟹ inj_on (λx. (the (map_of (zip xs ys) x))) (set xs)"
apply (subst zip_take_length[symmetric])
apply (erule map_of_zip_inj, simp)
by (metis length_take min_absorb2)
lemma list_all_nth:
"⟦list_all P xs; i < length xs⟧ ⟹ P (xs ! i)"
by (metis list_all_length)
lemma list_all_update:
"⟦list_all P xs; i < length xs; ⋀x. P x ⟹ P (f x)⟧
⟹ list_all P (xs [i := f (xs ! i)])"
by (metis length_list_update list_all_length nth_list_update)
lemma list_allI:
"⟦list_all P xs; ⋀x. P x ⟹ P' x⟧ ⟹ list_all P' xs"
by (metis list_all_length)
lemma list_all_imp_filter:
"list_all (λx. f x ⟶ g x) xs = list_all (λx. g x) [x←xs . f x]"
by (fastforce simp: Ball_set_list_all[symmetric])
lemma list_all_imp_filter2:
"list_all (λx. f x ⟶ g x) xs = list_all (λx. ¬f x) [x←xs . (λx. ¬g x) x]"
by (fastforce simp: Ball_set_list_all[symmetric])
lemma list_all_imp_chain:
"⟦list_all (λx. f x ⟶ g x) xs; list_all (λx. f' x ⟶ f x) xs⟧
⟹ list_all (λx. f' x ⟶ g x) xs"
by (clarsimp simp: Ball_set_list_all [symmetric])
lemma inj_Pair:
"inj_on (Pair x) S"
by (rule inj_onI, simp)
lemma inj_on_split:
"inj_on f S ⟹ inj_on (λx. (z, f x)) S"
by (auto simp: inj_on_def)
lemma split_state_strg:
"(∃x. f s = x ∧ P x s) ⟶ P (f s) s" by clarsimp
lemma theD:
"⟦the (f x) = y; x ∈ dom f ⟧ ⟹ f x = Some y"
by (auto simp add: dom_def)
lemma bspec_split:
"⟦ ∀(a, b) ∈ S. P a b; (a, b) ∈ S ⟧ ⟹ P a b"
by fastforce
lemma set_zip_same:
"set (zip xs xs) = Id ∩ (set xs × set xs)"
by (induct xs) auto
lemma ball_ran_updI:
"(∀x ∈ ran m. P x) ⟹ P v ⟹ (∀x ∈ ran (m (y ↦ v)). P x)"
by (auto simp add: ran_def)
lemma not_psubset_eq:
"⟦ ¬ A ⊂ B; A ⊆ B ⟧ ⟹ A = B"
by blast
lemma set_as_imp:
"(A ∩ P ∪ B ∩ -P) = {s. (s ∈ P ⟶ s ∈ A) ∧ (s ∉ P ⟶ s ∈ B)}"
by auto
lemma in_image_op_plus:
"(x + y ∈ (+) x ` S) = ((y :: 'a :: ring) ∈ S)"
by (simp add: image_def)
lemma insert_subtract_new:
"x ∉ S ⟹ (insert x S - S) = {x}"
by auto
lemmas zip_is_empty = zip_eq_Nil_iff
lemma minus_Suc_0_lt:
"a ≠ 0 ⟹ a - Suc 0 < a"
by simp
lemma fst_last_zip_upt:
"zip [0 ..< m] xs ≠ [] ⟹
fst (last (zip [0 ..< m] xs)) = (if length xs < m then length xs - 1 else m - 1)"
apply (subst last_conv_nth, assumption)
apply (simp only: One_nat_def)
apply (subst nth_zip; simp)
apply (rule order_less_le_trans[OF minus_Suc_0_lt]; simp)
apply (rule order_less_le_trans[OF minus_Suc_0_lt]; simp)
done
lemma neq_into_nprefix:
"⟦ x ≠ take (length x) y ⟧ ⟹ ¬ x ≤ y"
by (clarsimp simp: prefix_def less_eq_list_def)
lemma suffix_eqI:
"⟦ suffix xs as; suffix xs bs; length as = length bs;
take (length as - length xs) as ≤ take (length bs - length xs) bs⟧ ⟹ as = bs"
by (clarsimp elim!: prefixE suffixE)
lemma suffix_Cons_mem:
"suffix (x # xs) as ⟹ x ∈ set as"
by (metis in_set_conv_decomp suffix_def)
lemma distinct_imply_not_in_tail:
"⟦ distinct list; suffix (y # ys) list⟧ ⟹ y ∉ set ys"
by (clarsimp simp:suffix_def)
lemma list_induct_suffix [case_names Nil Cons]:
assumes nilr: "P []"
and consr: "⋀x xs. ⟦P xs; suffix (x # xs) as ⟧ ⟹ P (x # xs)"
shows "P as"
proof -
define as' where "as' == as"
have "suffix as as'" unfolding as'_def by simp
then show ?thesis
proof (induct as)
case Nil show ?case by fact
next
case (Cons x xs)
show ?case
proof (rule consr)
from Cons.prems show "suffix (x # xs) as" unfolding as'_def .
then have "suffix xs as'" by (auto dest: suffix_ConsD simp: as'_def)
then show "P xs" using Cons.hyps by simp
qed
qed
qed
text ‹Parallel etc. and lemmas for list prefix›
lemma prefix_induct [consumes 1, case_names Nil Cons]:
fixes prefix
assumes np: "prefix ≤ lst"
and base: "⋀xs. P [] xs"
and rl: "⋀x xs y ys. ⟦ x = y; xs ≤ ys; P xs ys ⟧ ⟹ P (x#xs) (y#ys)"
shows "P prefix lst"
using np
proof (induct prefix arbitrary: lst)
case Nil show ?case by fact
next
case (Cons x xs)
have prem: "(x # xs) ≤ lst" by fact
then obtain y ys where lv: "lst = y # ys"
by (rule prefixE, auto)
have ih: "⋀lst. xs ≤ lst ⟹ P xs lst" by fact
show ?case using prem
by (auto simp: lv intro!: rl ih)
qed
lemma not_prefix_cases:
fixes prefix
assumes pfx: "¬ prefix ≤ lst"
and c1: "⟦ prefix ≠ []; lst = [] ⟧ ⟹ R"
and c2: "⋀a as x xs. ⟦ prefix = a#as; lst = x#xs; x = a; ¬ as ≤ xs⟧ ⟹ R"
and c3: "⋀a as x xs. ⟦ prefix = a#as; lst = x#xs; x ≠ a⟧ ⟹ R"
shows "R"
proof (cases prefix)
case Nil then show ?thesis using pfx by simp
next
case (Cons a as)
have c: "prefix = a#as" by fact
show ?thesis
proof (cases lst)
case Nil then show ?thesis
by (intro c1, simp add: Cons)
next
case (Cons x xs)
show ?thesis
proof (cases "x = a")
case True
show ?thesis
proof (intro c2)
show "¬ as ≤ xs" using pfx c Cons True
by simp
qed fact+
next
case False
show ?thesis by (rule c3) fact+
qed
qed
qed
lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]:
fixes prefix
assumes np: "¬ prefix ≤ lst"
and base: "⋀x xs. P (x#xs) []"
and r1: "⋀x xs y ys. x ≠ y ⟹ P (x#xs) (y#ys)"
and r2: "⋀x xs y ys. ⟦ x = y; ¬ xs ≤ ys; P xs ys ⟧ ⟹ P (x#xs) (y#ys)"
shows "P prefix lst"
using np
proof (induct lst arbitrary: prefix)
case Nil then show ?case
by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)
next
case (Cons y ys)
have npfx: "¬ prefix ≤ (y # ys)" by fact
then obtain x xs where pv: "prefix = x # xs"
by (rule not_prefix_cases) auto
have ih: "⋀prefix. ¬ prefix ≤ ys ⟹ P prefix ys" by fact
show ?case using npfx
by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih)
qed
lemma rsubst:
"⟦ P s; s = t ⟧ ⟹ P t"
by simp
lemma ex_impE: "((∃x. P x) ⟶ Q) ⟹ P x ⟹ Q"
by blast
lemma option_Some_value_independent:
"⟦ f x = Some v; ⋀v'. f x = Some v' ⟹ f y = Some v' ⟧ ⟹ f y = Some v"
by blast
text ‹Some int bitwise lemmas. Helpers for proofs about 🗏‹NatBitwise.thy››
lemma int_2p_eq_shiftl:
"(2::int)^x = 1 << x"
by (simp add: shiftl_int_def)
lemma nat_int_mul:
"nat (int a * b) = a * nat b"
by (simp add: nat_mult_distrib)
lemma int_shiftl_less_cancel:
"n ≤ m ⟹ ((x :: int) << n < y << m) = (x < y << (m - n))"
apply (drule le_Suc_ex)
apply (clarsimp simp: shiftl_int_def power_add)
done
lemma int_shiftl_lt_2p_bits:
"0 ≤ (x::int) ⟹ x < 1 << n ⟹ ∀i ≥ n. ¬ x !! i"
apply (clarsimp simp: shiftl_int_def)
by (metis bit_take_bit_iff not_less take_bit_int_eq_self_iff)
lemmas int_eq_test_bit = bin_eq_iff
lemmas int_eq_test_bitI = int_eq_test_bit[THEN iffD2, rule_format]
lemma le_nat_shrink_left:
"y ≤ z ⟹ y = Suc x ⟹ x < z"
by simp
lemma length_ge_split:
"n < length xs ⟹ ∃x xs'. xs = x # xs' ∧ n ≤ length xs'"
by (cases xs) auto
text ‹Support for defining enumerations on datatypes derived from enumerations›
lemma distinct_map_enum:
"⟦ (∀ x y. (F x = F y ⟶ x = y )) ⟧
⟹ distinct (map F (enum_class.enum :: 'a :: enum list))"
by (simp add: distinct_map inj_onI)
lemma if_option_None_eq:
"((if P then None else Some x) = None) = P"
by (auto split: if_splits)
lemma not_in_ran_None_upd:
"x ∉ ran m ⟹ x ∉ ran (m(y := None))"
by (auto simp: ran_def split: if_split)
text ‹Prevent clarsimp and others from creating Some from not None by folding this and unfolding
again when safe.›
definition
"not_None x = (x ≠ None)"
lemma sorted_wrt_hd_min: "⟦ ⋀x. P x x; sorted_wrt P xs ⟧ ⟹ (∀x ∈ set xs. P (hd xs) x)"
by (induction xs) auto
lemma disjoint_no_subset: "A ∩ B = {} ⟹ A ≠ {} ⟹ A ⊆ B ⟹ False"
by blast
lemma map_prod_split_case: "map_prod f g x = (case x of (a, b) => (f a, g b))"
by (cases x) (auto)
lemma map_prod_split_prj: "map_prod f g x = (f (fst x), g (snd x))"
by (cases x) (auto)
end