Theory Basic_Extensions
section ‹Basics›
theory Basic_Extensions
imports "HOL-Library.Infinite_Set"
begin
subsection ‹Types›
type_synonym 'a step = "'a ⇒ 'a"
subsection ‹Rules›
declare less_imp_le[dest, simp]
declare le_funI[intro]
declare le_funE[elim]
declare le_funD[dest]
lemma IdI'[intro]:
assumes "x = y"
shows "(x, y) ∈ Id"
using assms by auto
lemma (in order) order_le_cases:
assumes "x ≤ y"
obtains (eq) "x = y" | (lt) "x < y"
using assms le_less by auto
lemma (in linorder) linorder_cases':
obtains (le) "x ≤ y" | (gt) "x > y"
by force
lemma monoI_comp[intro]:
assumes "mono f" "mono g"
shows "mono (f ∘ g)"
using assms by (intro monoI, auto dest: monoD)
lemma strict_monoI_comp[intro]:
assumes "strict_mono f" "strict_mono g"
shows "strict_mono (f ∘ g)"
using assms by (intro strict_monoI, auto dest: strict_monoD)
lemma eq_le_absorb[simp]:
fixes x y :: "'a :: order"
shows "x = y ∧ x ≤ y ⟷ x = y" "x ≤ y ∧ x = y ⟷ x = y"
by auto
lemma INFM_Suc[simp]: "(∃⇩∞ i. P (Suc i)) ⟷ (∃⇩∞ i. P i)"
unfolding INFM_nat using Suc_lessE less_Suc_eq by metis
lemma INFM_plus[simp]: "(∃⇩∞ i. P (i + n :: nat)) ⟷ (∃⇩∞ i. P i)"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
have "(∃⇩∞ i. P (i + Suc n)) ⟷ (∃⇩∞ i. P (Suc i + n))" by simp
also have "… ⟷ (∃⇩∞ i. P (i + n))" using INFM_Suc by this
also have "… ⟷ (∃⇩∞ i. P i)" using Suc by this
finally show ?case by this
qed
lemma INFM_minus[simp]: "(∃⇩∞ i. P (i - n :: nat)) ⟷ (∃⇩∞ i. P i)"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
have "(∃⇩∞ i. P (i - Suc n)) ⟷ (∃⇩∞ i. P (Suc i - Suc n))" using INFM_Suc by meson
also have "… ⟷ (∃⇩∞ i. P (i - n))" by simp
also have "… ⟷ (∃⇩∞ i. P i)" using Suc by this
finally show ?case by this
qed
subsection ‹Constants›
definition const :: "'a ⇒ 'b ⇒ 'a"
where "const x ≡ λ _. x"
definition const2 :: "'a ⇒ 'b ⇒ 'c ⇒ 'a"
where "const2 x ≡ λ _ _. x"
definition const3 :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'a"
where "const3 x ≡ λ _ _ _. x"
definition const4 :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'a"
where "const4 x ≡ λ _ _ _ _. x"
definition const5 :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'f ⇒ 'a"
where "const5 x ≡ λ _ _ _ _ _. x"
lemma const_apply[simp]: "const x y = x" unfolding const_def by rule
lemma const2_apply[simp]: "const2 x y z = x" unfolding const2_def by rule
lemma const3_apply[simp]: "const3 x y z u = x" unfolding const3_def by rule
lemma const4_apply[simp]: "const4 x y z u v = x" unfolding const4_def by rule
lemma const5_apply[simp]: "const5 x y z u v w = x" unfolding const5_def by rule
definition zip_fun :: "('a ⇒ 'b) ⇒ ('a ⇒ 'c) ⇒ 'a ⇒ 'b × 'c" (infixr "∥" 51)
where "f ∥ g ≡ λ x. (f x, g x)"
lemma zip_fun_simps[simp]:
"(f ∥ g) x = (f x, g x)"
"fst ∘ (f ∥ g) = f"
"snd ∘ (f ∥ g) = g"
"fst ∘ h ∥ snd ∘ h = h"
"fst ` range (f ∥ g) = range f"
"snd ` range (f ∥ g) = range g"
unfolding zip_fun_def by force+
lemma zip_fun_eq[dest]:
assumes "f ∥ g = h ∥ i"
shows "f = h" "g = i"
using assms unfolding zip_fun_def by (auto dest: fun_cong)
lemma zip_fun_range_subset[intro, simp]: "range (f ∥ g) ⊆ range f × range g"
unfolding zip_fun_def by blast
lemma zip_fun_range_finite[elim]:
assumes "finite (range (f ∥ g))"
obtains "finite (range f)" "finite (range g)"
proof
show "finite (range f)" using finite_imageI [OF assms(1), of fst]
by (simp add: image_image)
show "finite (range g)" using finite_imageI [OF assms(1), of snd]
by (simp add: image_image)
qed
lemma zip_fun_split:
obtains f g
where "h = f ∥ g"
proof
show "h = fst ∘ h ∥ snd ∘ h" by simp
qed
abbreviation "None_None ≡ (None, None)"
abbreviation "None_Some ≡ λ (y). (None, Some y)"
abbreviation "Some_None ≡ λ (x). (Some x, None)"
abbreviation "Some_Some ≡ λ (x, y). (Some x, Some y)"
abbreviation "None_None_None ≡ (None, None, None)"
abbreviation "None_None_Some ≡ λ (z). (None, None, Some z)"
abbreviation "None_Some_None ≡ λ (y). (None, Some y, None)"
abbreviation "None_Some_Some ≡ λ (y, z). (None, Some y, Some z)"
abbreviation "Some_None_None ≡ λ (x). (Some x, None, None)"
abbreviation "Some_None_Some ≡ λ (x, z). (Some x, None, Some z)"
abbreviation "Some_Some_None ≡ λ (x, y). (Some x, Some y, None)"
abbreviation "Some_Some_Some ≡ λ (x, y, z). (Some x, Some y, Some z)"
lemma inj_Some2[simp, intro]:
"inj None_Some"
"inj Some_None"
"inj Some_Some"
by (rule injI, force)+
lemma inj_Some3[simp, intro]:
"inj None_None_Some"
"inj None_Some_None"
"inj None_Some_Some"
"inj Some_None_None"
"inj Some_None_Some"
"inj Some_Some_None"
"inj Some_Some_Some"
by (rule injI, force)+
definition swap :: "'a × 'b ⇒ 'b × 'a"
where "swap x ≡ (snd x, fst x)"
lemma swap_simps[simp]: "swap (a, b) = (b, a)" unfolding swap_def by simp
lemma swap_inj[intro, simp]: "inj swap" by (rule injI, auto)
lemma swap_surj[intro, simp]: "surj swap" by (rule surjI[where ?f = swap], auto)
lemma swap_bij[intro, simp]: "bij swap" by (rule bijI, auto)
definition push :: "('a × 'b) × 'c ⇒ 'a × 'b × 'c"
where "push x ≡ (fst (fst x), snd (fst x), snd x)"
definition pull :: "'a × 'b × 'c ⇒ ('a × 'b) × 'c"
where "pull x ≡ ((fst x, fst (snd x)), snd (snd x))"
lemma push_simps[simp]: "push ((x, y), z) = (x, y, z)" unfolding push_def by simp
lemma pull_simps[simp]: "pull (x, y, z) = ((x, y), z)" unfolding pull_def by simp
definition label :: "'vertex × 'label × 'vertex ⇒ 'label"
where "label ≡ fst ∘ snd"
lemma label_select[simp]: "label (p, a, q) = a" unfolding label_def by simp
subsection ‹Theorems for @term{curry} and @term{split}›
lemma curry_split[simp]: "curry ∘ case_prod = id" by auto
lemma split_curry[simp]: "case_prod ∘ curry = id" by auto
lemma curry_le[simp]: "curry f ≤ curry g ⟷ f ≤ g" unfolding le_fun_def by force
lemma split_le[simp]: "case_prod f ≤ case_prod g ⟷ f ≤ g" unfolding le_fun_def by force
lemma mono_curry_left[simp]: "mono (curry ∘ h) ⟷ mono h"
unfolding mono_def by fastforce
lemma mono_split_left[simp]: "mono (case_prod ∘ h) ⟷ mono h"
unfolding mono_def by fastforce
lemma mono_curry_right[simp]: "mono (h ∘ curry) ⟷ mono h"
unfolding mono_def split_le[symmetric] by bestsimp
lemma mono_split_right[simp]: "mono (h ∘ case_prod) ⟷ mono h"
unfolding mono_def curry_le[symmetric] by bestsimp
lemma Collect_curry[simp]: "{x. P (curry x)} = case_prod ` {x. P x}" using image_Collect by fastforce
lemma Collect_split[simp]: "{x. P (case_prod x)} = curry ` {x. P x}" using image_Collect by force
lemma gfp_split_curry[simp]: "gfp (case_prod ∘ f ∘ curry) = case_prod (gfp f)"
proof -
have "gfp (case_prod ∘ f ∘ curry) = Sup {u. u ≤ case_prod (f (curry u))}" unfolding gfp_def by simp
also have "… = Sup {u. curry u ≤ curry (case_prod (f (curry u)))}" unfolding curry_le by simp
also have "… = Sup {u. curry u ≤ f (curry u)}" by simp
also have "… = Sup (case_prod ` {u. u ≤ f u})" unfolding Collect_curry[of "λ u. u ≤ f u"] by simp
also have "… = case_prod (Sup {u. u ≤ f u})" by (force simp add: image_comp)
also have "… = case_prod (gfp f)" unfolding gfp_def by simp
finally show ?thesis by this
qed
lemma gfp_curry_split[simp]: "gfp (curry ∘ f ∘ case_prod) = curry (gfp f)"
proof -
have "gfp (curry ∘ f ∘ case_prod) = Sup {u. u ≤ curry (f (case_prod u))}" unfolding gfp_def by simp
also have "… = Sup {u. case_prod u ≤ case_prod (curry (f (case_prod u)))}" unfolding split_le by simp
also have "… = Sup {u. case_prod u ≤ f (case_prod u)}" by simp
also have "… = Sup (curry ` {u. u ≤ f u})" unfolding Collect_split[of "λ u. u ≤ f u"] by simp
also have "… = curry (Sup {u. u ≤ f u})" by (force simp add: image_comp)
also have "… = curry (gfp f)" unfolding gfp_def by simp
finally show ?thesis by this
qed
lemma not_someI:
assumes "⋀ x. P x ⟹ False"
shows "¬ P (SOME x. P x)"
using assms by blast
lemma some_ccontr:
assumes "(⋀ x. ¬ P x) ⟹ False"
shows "P (SOME x. P x)"
using assms someI_ex ccontr by metis
end