Theory HOL_Basis
theory HOL_Basis
imports
"tools/Strengthen"
"HOL-Library.Complete_Partial_Order2"
"HOL-Library.Monad_Syntax"
"Coinductive.TLList"
"HOL-Library.BNF_Corec"
begin
section‹ Extra HOL ›
declare [[coercion_enabled = false]]
hide_const (open) BNF_Cardinal_Order_Relation.stable
hide_const (open) Topological_Spaces.incseq
hide_const (open) Topological_Spaces.decseq
no_notation Binomial.binomial (infixl "choose" 65)
no_notation Sublist.parallel (infixl "∥" 50)
consts parallel :: "'a ⇒ 'a ⇒ 'a" (infixr "∥" 53)
consts Parallel :: "'a set ⇒ ('a ⇒ 'b) ⇒ 'b"
syntax
"_PAR1" :: "pttrns ⇒ 'a set ⇒ 'b" ("(3‖_./ _)" [0, 10] 10)
"_PAR" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b" ("(3‖_∈_./ _)" [0, 0, 10] 10)
translations
"‖x y. f" ⇌ "‖x. ‖y. f"
"‖x. f" ⇌ "CONST Parallel CONST UNIV (λx. f)"
"‖x∈A. f" ⇌ "CONST Parallel A (λx. f)"
lemmas conj_explode = conj_imp_eq_imp_imp
lemma If_Not[simp]:
shows "(if ¬P then Q else R) = (if P then R else Q)"
by simp
lemma Let_distrib:
shows "f (let x = a in e x) = (let x = a in f (e x))"
by simp
lemma stronger_disjE:
assumes "P ∨ Q"
assumes "P ⟹ R"
assumes "⟦¬P; Q⟧ ⟹ R"
shows "R"
using assms by blast
abbreviation (input) Collect2 :: "('a ⇒ 'b ⇒ bool) ⇒ ('a × 'b) set" where
"Collect2 P ≡ Collect (case_prod P)"
lemma mono_Set_bind:
shows "mono (λX. Set.bind X f)"
unfolding Set.bind_def by (rule monoI) fast
lemma
minus_False[simp]: "-{False} = {True}"
and minus_True[simp]: "-{True} = {False}"
by blast+
lemma
shows Collect_True[simp]: "{x. x} = {True}"
and Collect_bot[simp]: "Collect ⊥ = {}"
and Collect_Not[simp]: "Collect Not = {False}"
by blast+
lemma const_image_conv:
shows "(λ_. c) ` X ⊆ Y ⟷ (c ∉ Y ⟶ X = {})"
by blast
lemma inv_vimage:
assumes "surj f"
shows "inv f -` f -` x = x"
using assms by (metis image_comp image_f_inv_f surj_iff surj_image_vimage_eq vimage_comp)
lemma Union_singleton:
shows "⋃{{x} |x. x ∈ X} = X"
by blast
lemma UNIV_minus_uminus[simp]:
shows "UNIV - X = -X"
by auto
lemmas insert_Image = Un_Image[where R="{r}", simplified] for r
lemma Image_UNIV:
fixes R :: "('a × 'b) set"
shows "R `` UNIV = snd ` R"
by force
lemma insert_Diff_UNIV:
shows "insert x (- {x}) = UNIV"
and "insert x (UNIV - {x}) = UNIV"
by blast+
lemmas eq_commute_conv = HOL.eq_iff_swap
lemma inf_commute_conv:
fixes x :: "_::semilattice_inf"
assumes "x ⊓ y = z"
shows "y ⊓ x = z"
by (simp add: assms inf_commute)
abbreviation (input) uncurry :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a × 'b ⇒ 'c" where "uncurry ≡ case_prod"
lemmas fun_eqI = ext
lemma override_on_cong[cong]:
assumes "A = A'"
assumes "⋀x. x ∉ A' ⟹ f x = f' x"
assumes "⋀x. x ∈ A' ⟹ g x = g' x"
shows "override_on f g A = override_on f' g' A'"
using assms by (simp add: override_on_def fun_eq_iff)
lemma override_on_comp:
shows "h ∘ override_on f g A = override_on (h ∘ f) (h ∘ g) A"
by (simp_all add: override_on_def fun_eq_iff)
lemma refine_compose:
assumes "∀x y. f x = f y ⟶ g x = g y"
obtains h where "g = h ∘ f"
proof atomize_elim
from assms have "g = (g ∘ inv f) ∘ f"
unfolding o_def inv_def by (metis (mono_tags, lifting) someI_ex)
then show "∃h. g = h ∘ f" by blast
qed
lemma inj_Not[iff]:
shows "inj Not"
by (simp add: inj_def)
lemma bij_Not[iff]:
shows "bij Not"
unfolding bij_def by blast
lemma bij_inv_eq_iff:
assumes "bij p"
shows "x = inv p y ⟷ p x = y"
and "inv p y = x ⟷ p x = y"
by (simp_all add: assms bij_inv_eq_iff eq_commute_conv[OF bij_inv_eq_iff])
lemma bij_inv:
assumes "bij f"
shows "f (inv f x) = x"
and "f ∘ inv f = id"
by (simp_all add: assms fun_eq_iff flip: bij_inv_eq_iff)
lemma image_image_set_diff_singleton:
assumes "inj f"
shows "f ` A - {f a} = f ` (A - {a})"
by (simp add: assms image_set_diff)
lemma image_Inter_subseteq:
shows "f ` ⋂A ⊆ ⋂{f ` x |x. x ∈ A}"
by blast
lemma fst_image:
shows "fst ` Collect (λx. ∃s. x = (v, s, s)) = {v}"
by force
lemma Least_equality:
fixes x :: "_::order"
assumes "P x"
assumes "⋀y. P y ⟹ x ≤ y"
shows "Least P = x"
and "x = Least P"
using Least_equality assms by blast+
declare map_prod.id[simp]
declare map_prod.compositionality[simp]
lemma map_prod_image_Collect:
fixes f :: "'a ⇒ 'b"
fixes g :: "'c ⇒ 'd"
shows "map_prod f g ` Collect P = {(f x, g y) |x y. P (x, y)}"
by blast
lemma range_map_prod:
shows "range (map_prod f g) = range f × range g"
by blast
declare unit.case_cong_weak[cong del]
lemma lambda_unit_futzery:
shows "(λ_. P) = (λ(). P)"
by auto
lemma fun_unit_id:
shows "(f :: unit ⇒ unit) = id"
by (simp add: fun_eq_iff)
lemma surj_unit_range[iff]:
shows "surj (f :: _ ⇒ unit)"
unfolding surj_def by simp
lemma split_pairs:
shows "((x, y) = z) ⟷ (fst z = x ∧ snd z = y)"
and "(z = (x, y)) ⟷ (fst z = x ∧ snd z = y)"
by auto
lemma eq_split_pair:
shows "(=) (x, y) = (λp. fst p = x ∧ snd p = y)"
by fastforce
lemma map_prod_conv:
shows "(x, y) = map_prod f g z ⟷ (∃a b. z = (a, b) ∧ x = f a ∧ y = g b)"
and "map_prod f g z = (x, y) ⟷ (∃a b. z = (a, b) ∧ x = f a ∧ y = g b)"
by (case_tac [!] z) auto
lemma map_prod_image_Times:
shows "map_prod f g ` (F × G) = f ` F × g ` G"
by blast
lemma map_prod_vimage_Times:
shows "map_prod f g -` (F × G) = f -` F × g -` G"
by fastforce
lemma vimage_range:
shows "f -` range f = UNIV"
by blast
lemma Pair_image:
shows "Pair x ` F = {x} × F"
by fast
lemma fst_image_map_prod:
shows "fst ` map_prod f g ` X = f ` fst ` X"
unfolding image_def by force
lemma snd_image_map_prod:
shows "snd ` map_prod f g ` X = g ` snd ` X"
unfolding image_def by force
lemma Times_Un_distrib2:
shows "A × (B ∪ C) = A × B ∪ A × C"
by fast
lemma Times_insert_distrib1:
shows "insert x X × Y = {x} × Y ∪ X × Y"
by fast
lemma map_prod_apfst[simp]:
shows "map_prod f g (apfst h x) = map_prod (f ∘ h) g x"
and "apfst f (map_prod h g x) = map_prod (f ∘ h) g x"
by (simp_all add: apfst_def)
lemma map_prod_apsnd[simp]:
shows "map_prod f g (apsnd h x) = map_prod f (g ∘ h) x"
and "apsnd g (map_prod f h x) = map_prod f (g ∘ h) x"
by (simp_all add: apsnd_def)
lemma map_prod_const_image:
shows "map_prod (λx. c) g ` X = {c} × g ` snd ` X"
and "map_prod f (λx. c) ` X = f ` fst ` X × {c}"
by force+
type_synonym 'a relp = "'a ⇒ 'a ⇒ bool"
definition Diag :: "('a ⇒ bool) ⇒ 'a rel" where
"Diag P = Restr Id (Collect P)"
abbreviation Pre :: "('s ⇒ bool) ⇒ 's rel" where
"Pre P ≡ Collect P × UNIV"
abbreviation Post :: "('v ⇒ 's ⇒ bool) ⇒ 'v ⇒ 's rel" where
"Post Q v ≡ UNIV × Collect (Q v)"
lemma member_Diag[simp]:
shows "(x, y) ∈ Diag P ⟷ x = y ∧ P x"
by (fastforce simp: Diag_def)
lemma Diag_Id_le[iff]:
shows "Diag P ⊆ Id"
by (fastforce simp: Diag_def)
lemma mono_Diag:
shows "mono Diag"
by (fastforce simp: Diag_def intro: monoI)
lemmas strengthen_Diag[strg] = st_monotone[OF mono_Diag]
lemma Diag_bot[iff]:
shows "Diag ⊥ = {}"
and "Diag (λ_. False) = {}"
by (simp_all add: Diag_def)
lemma Diag_top[iff]:
shows "Diag ⊤ = Id"
and "Diag (λ_. True) = Id"
by (auto simp: Diag_def)
lemma Diag_Sup:
shows "Diag (⨆X) = ⨆(Diag ` X)"
unfolding Diag_def by blast
declare refl_Id[iff]
lemma Id_not_empty[iff]:
shows "Id ≠ {}"
by fast
lemma refl_alt_def:
shows "refl r ⟷ Id ⊆ r"
unfolding refl_on_def by auto
lemma mono_Image:
shows "mono (Image r)"
by (rule monoI) auto
lemma Image_comp:
shows "(``) R ∘ (``) S = (``) (S O R)"
by fastforce
lemmas refl_INTER = refl_on_INTER[where A="λx. UNIV" and S=UNIV, simplified, rule_format]
lemma refl_UnionI:
assumes "r ∈ R"
assumes "refl r"
shows "refl (⋃R)"
using assms unfolding refl_on_def by fast
lemma refl_UNIV[iff]:
shows "refl UNIV"
unfolding refl_on_def by simp
lemma trans_UNIV[iff]:
shows "trans UNIV"
unfolding trans_def by simp
lemma refl_on_intI:
assumes "refl_on A r"
assumes "refl_on A s"
shows "refl_on A (r ∩ s)"
using assms unfolding refl_on_def by blast
lemma refl_inter_conv:
shows "refl (r ∩ s) ⟷ refl r ∧ refl s"
unfolding refl_on_def by auto
lemma map_prod_image_Image:
fixes X :: "('a × 'b) set"
fixes Y :: "'c set"
fixes f :: "'a ⇒ 'c"
fixes g :: "'b ⇒ 'd"
shows "(map_prod f g ` X) `` Y = g ` X `` f -` Y"
by (force simp add: Image_iff image_iff)
lemma equiv_closed:
assumes "equiv A r"
assumes "B ⊆ A"
shows "r `` r `` B = r `` B"
using assms unfolding equiv_def by (auto elim: transE dest: refl_onD)
lemma sym_trans_refl_on:
assumes "sym r"
assumes "trans r"
shows "refl_on (Domain r) r"
using assms by (force intro: refl_onI elim: symE transE)
declare bot_unique[simp]
declare subset_refl[iff]
declare trans_rtrancl[iff]
declare refl_rtrancl[iff]
declare le_bool_def[simp del]
declare transp_le[intro!]
declare List.null_def[simp]
lemma split_list_Ex:
shows "(∃xxs. P xxs) ⟷ (P [] ∨ (∃x xs. P (x # xs)))"
by (metis neq_Nil_conv)
lemma append_Nil[simp]:
shows "(@) [] = id"
by fastforce
lemma case_list_cancel:
shows "(case xs of [] ⇒ f | _ ⇒ f) = f"
by (simp split: list.splits)
lemma rev_induct2[consumes 1, case_names Nil snoc]:
assumes "length xs = length ys"
assumes "P [] []"
assumes "⋀x xs y ys. length xs = length ys ⟹ P xs ys ⟹ P (xs @ [x]) (ys @ [y])"
shows "P xs ys"
proof -
have "P (rev (rev xs)) (rev (rev ys))"
by (rule list_induct2[of "rev xs" "rev ys"]) (simp_all add: assms)
then show ?thesis by simp
qed
lemma Image_set_map_filter:
shows "set xs `` X = set (map snd (filter (λx. fst x ∈ X) xs))"
by (induct xs) auto
lemma case_list_snoc:
shows "case_list n c (xs @ [x]) = c (hd (xs @ [x])) (tl (xs @ [x]))"
by (simp split: list.splits)
lemma sorted_wrt_set_last:
assumes "x ∈ set xs"
assumes "sorted_wrt r xs"
assumes "reflp r"
assumes "transp r"
shows "r x (last xs)"
using assms by (induct xs) (auto elim: reflpE)
lemma append_eq_conv_conj:
shows "(zs = xs @ ys) = (xs = take (length xs) zs ∧ ys = drop (length xs) zs)"
and "(xs @ ys = zs) = (xs = take (length xs) zs ∧ ys = drop (length xs) zs)"
by (rule eq_commute_conv) (simp_all add: append_eq_conv_conj)
lemma drop_eq_Cons_length_conv:
shows "(∃y ys. drop i xs = y # ys) ⟷ i < length xs"
using neq_Nil_conv by fastforce
lemma drop_eq_Cons_lengthD:
assumes "drop i xs = y # ys"
shows "i < length xs"
by (meson assms drop_eq_Cons_length_conv)
lemma filter_weaken_cong:
assumes "filter P xs = filter P ys"
assumes "∀x. Q x ⟶ P x"
shows "filter Q xs = filter Q ys"
using assms(1)
proof(induct xs arbitrary: ys)
case Nil with assms(2) show ?case by (auto simp: empty_filter_conv)
next
case (Cons x xs) from assms(2) Cons.prems show ?case
by (auto 4 3 simp: Cons_eq_filter_iff filter_empty_conv dest!: Cons.hyps split: if_splits)
qed
lemma filter_eq_ConsE:
assumes "filter P xs = y # ys"
obtains us vs where "xs = us @ y # vs" and "∀u∈set us. ¬ P u" and "P y" and "ys = filter P vs"
using iffD1[OF filter_eq_Cons_iff assms] by blast
lemma Cons_eq_filterE:
assumes "y # ys = filter P xs"
obtains us vs where "xs = us @ y # vs" and "∀u∈set us. ¬ P u" and "P y" and "ys = filter P vs"
using filter_eq_ConsE[OF sym[OF assms]] .
lemma filter_eq_appendE:
assumes "filter P xs = ys @ zs"
obtains us vs where "xs = us @ vs" and "filter P us = ys" and "filter P vs = zs"
apply atomize_elim
using assms
proof(induct xs arbitrary: ys)
case (Cons x xs ys) then show ?case
by (clarsimp simp: Cons_eq_append_conv split: if_split_asm; metis filter.simps)
qed simp
lemma append_eq_filterE:
assumes "ys @ zs = filter P xs"
obtains us vs where "xs = us @ vs" and "filter P us = ys" and "filter P vs = zs"
using assms by (metis filter_eq_appendE)
lemma filter_eq_append_conv:
shows "filter P xs = ys @ zs ⟷ (∃us vs. xs = us @ vs ∧ filter P us = ys ∧ filter P vs = zs)" (is ?thesis1)
and "ys @ zs = filter P xs ⟷ (∃us vs. xs = us @ vs ∧ filter P us = ys ∧ filter P vs = zs)" (is ?thesis2)
proof -
show ?thesis1 by (meson filter_append filter_eq_appendE)
then show ?thesis2 by (rule eq_commute_conv)
qed
lemma fold_fun:
shows "fold (λx. (∘) (f x)) xs g s = fold f xs (g s)"
by (induct xs arbitrary: s g) simp_all
lemma last_Pair_const:
shows "last ((a, b) # map (λx. (a, snd x)) xs) = (a, last (b # map snd xs))"
by (induct xs) auto
lemma mono_nth_Suc_aux:
fixes xs :: "_::linorder list"
assumes "∀i < length xs - Suc 0. xs ! i ≤ xs ! Suc i"
assumes "j < length xs"
assumes "i ≤ j"
shows "xs ! i ≤ xs ! j"
using assms
proof(induct j)
case (Suc j) then show ?case
by (fastforce dest: iffD1[OF le_eq_less_or_eq] spec[where x="j"])
qed simp
lemma mono_nth_Suc:
fixes xs :: "_::linorder list"
shows "(∀j < length xs. ∀i ≤ j. xs ! i ≤ xs ! j) ⟷ (∀i < length xs - 1. xs!i ≤ xs ! Suc i)"
by (auto intro: mono_nth_Suc_aux)
lemma sorted_nth_monoI2:
assumes "⋀i. i < length xs - 1 ⟹ xs ! i ≤ xs ! Suc i"
shows "sorted xs"
by (meson assms mono_nth_Suc sorted_iff_nth_mono)
lemma bij_map_prod:
shows "bij (map_prod f g) ⟷ bij f ∧ bij g"
unfolding bij_def surj_def inj_def by auto
lemma bij_inv_map_prod:
assumes "bij f"
assumes "bij g"
shows "inv (map_prod f g) = map_prod (inv f) (inv g)"
by (simp add: assms fun_eq_iff bij_inv_eq_iff bij_map_prod bij_inv)
lemma surj_map_conv:
shows "surj (map f) ⟷ surj f"
by (auto simp flip: lists_UNIV lists_image) (metis Cons_in_lists_iff UNIV_I lists_UNIV)
lemma bij_map_conv:
shows "bij (map f) ⟷ bij f"
by (simp add: bij_betw_def surj_map_conv)
lemma inv_map:
assumes "bij f"
shows "inv (map f) xs = map (inv f) xs"
by (simp add: assms bij_inv_eq_iff(2)[OF iffD2[OF bij_map_conv]] bij_inv)
lemma set_singleton_conv:
shows "set xs = {x} ⟷ (∃i. xs = replicate (Suc i) x)" (is ?thesis1)
and "{x} = set xs ⟷ (∃i. xs = replicate (Suc i) x)" (is ?thesis2)
proof -
show ?thesis1
by (metis length_Cons neq_Nil_conv replicate_length_same set_empty2 set_replicate_Suc singletonD)
then show ?thesis2
by (rule eq_commute_conv)
qed
lemma nths_singleton_le:
assumes "i < length xs"
shows "nths xs {i} = [xs ! i]"
using assms
by (induct xs rule: rev_induct)
(auto simp: nths_def nth_append not_less filter_empty_conv elim: in_set_zipE)
lemma nths_empty_conv:
shows "nths xs A = [] ⟷ xs = [] ∨ (∀i∈A. length xs ≤ i)" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
have "length xs ≤ i" if "∀j<length xs. j ∉ A" and "xs ≠ []" and "i ∈ A" for i
using that leI by blast
then show "?lhs ⟹ ?rhs"
by (fastforce dest: arg_cong[where f=set] simp: set_nths)
show "?rhs ⟹ ?lhs"
by (auto simp: nths_def filter_empty_conv elim!: in_set_zipE)
qed
lemma nths_singleton_eq_conv:
shows "nths xs {i} = (if i < length xs then [xs ! i] else [])"
by (simp add: nths_empty_conv nths_singleton_le)
lemma prefix_append_strict_prefix:
shows "prefix xs (ys @ zs) ⟷ strict_prefix xs ys ∨ (∃us. xs = ys @ us ∧ prefix us zs)"
using prefix_append prefix_code(1) prefix_order.le_less by blast
lemma prefix_append_not_Nil:
shows "prefix xs (ys @ zs) ⟷ prefix xs ys ∨ (∃us. xs = ys @ us ∧ us ≠ [] ∧ prefix us zs)"
by (fastforce simp: prefix_append)
lemma prefix_append_not_NilE[consumes 1, case_names incomplete continue]:
assumes "prefix xs (ys @ zs)"
assumes "prefix xs ys ⟹ R"
assumes "⋀us. ⟦xs = ys @ us; us ≠ []; prefix us zs⟧ ⟹ R"
shows R
using assms prefix_append_not_Nil by blast
lemma subseq_Cons_right:
shows "subseq xs (y # ys)
⟷ (case xs of [] ⇒ True | x' # xs' ⇒ (x' = y ∧ subseq xs' ys) ∨ subseq xs ys)"
by (auto elim: subseq_Cons' split: list.splits)
lemma take_is_strict_prefix[intro!]:
assumes "n < length xs"
shows "strict_prefix (take n xs) xs"
by (meson assms leD prefix_order.le_neq_trans take_all_iff take_is_prefix)
lemma wfP_strict_prefix:
shows "wfP (strict_prefix :: 'a list ⇒ 'a list ⇒ bool)"
proof -
have "∃z∈Q. ∀y. strict_prefix y z ⟶ y ∉ Q" if "x ∈ Q" for x :: "'a list" and Q
using that by (induct x rule: length_induct) (blast dest: prefix_length_less)
then show ?thesis
unfolding wfP_def by (auto intro!: wfI_min)
qed
lemma set_subseq:
assumes "subseq xs ys"
shows "set xs ⊆ set ys"
using assms by (metis notin_set_nthsI subseq_conv_nths subsetI)
lemma subseq_filter_alt:
assumes "subseq xs ys"
assumes "∀x∈set xs. P x ⟶ Q x"
shows "subseq (filter P xs) (filter Q ys)"
using assms by induct auto
lemma lists_not_eq:
assumes "xs ≠ ys"
assumes "length xs = length ys"
obtains ps x y xs' ys'
where "x ≠ y" and "xs = ps @ x # xs'" and "ys = ps @ y # ys'"
using same_length_different[OF assms] by clarsimp
lemmas prefix_map_rightD = prefix_map_rightE
lemma prefix_map_rightE:
assumes "prefix xs (map f ys)"
obtains xs' where "prefix xs' ys" and "xs = map f xs'"
by (meson assms prefix_map_rightD)
lemma prefix_filter_rightE:
assumes "prefix xs (filter P ys)"
obtains xs' where "prefix xs' ys" and "xs = filter P xs'"
by (metis assms filter_eq_appendE prefix_def)
lemma prefix_induct[case_names Nil snoc]:
assumes "P []"
assumes "⋀xs' x. ⟦prefix (xs' @ [x]) xs; P xs'⟧ ⟹ P (xs' @ [x])"
shows "P xs"
proof -
have "P xs'" if "prefix xs' xs" for xs'
using that by (induct xs' rule: rev_induct) (auto simp: prefix_def assms)
then show ?thesis by simp
qed
declare map_option.id[simp]
declare map_option.id[unfolded id_def, simp]
declare map_option.compositionality[simp]
lemma not_None_eq2[simp]:
shows "(None ≠ x) = (∃y. x = Some y)"
by (metis not_Some_eq)
lemmas map_option_eq_Some[simp] =
Option.map_option_eq_Some
eq_commute_conv[OF Option.map_option_eq_Some]
lemma inj_map_option:
shows "inj (map_option f) ⟷ inj f"
by (simp add: inj_def split_option_all)
lemma surj_map_option:
shows "surj (map_option f) ⟷ surj f"
by (simp add: surj_def split_option_ex split_option_all)
lemma bij_map_option:
shows "bij (map_option f) ⟷ bij f"
by (simp add: bij_def inj_map_option surj_map_option)
lemma inv_map_option:
assumes "bij f"
shows "inv (map_option f) x = map_option (inv f) x"
by (simp add: assms bij_inv_eq_iff bij_map_option bij_inv)
lemma case_option_cancel:
shows "case_option f (λ_. f) opt = f"
by (simp split: option.splits)
lemma option_bind_alt_def:
shows "Option.bind = (λopt f. case_option None f opt)"
by (simp add: fun_eq_iff split: option.split)
lemma option_bind_eq_None_conv:
shows "Option.bind a f = None ⟷ a = None ∨ f (the a) = None"
and "None = Option.bind a f ⟷ a = None ∨ f (the a) = None"
by (intro Option.bind_eq_None_conv eq_commute_conv)+
overloading
pfunpow ≡ "compow :: nat ⇒ ('a ⇒ 'a option) ⇒ ('a ⇒ 'a option)"
begin
primrec pfunpow :: "nat ⇒ ('a ⇀ 'a) ⇒ 'a ⇀ 'a" where
"pfunpow 0 f = Some"
| "pfunpow (Suc n) f = (λx. Option.bind (f x) (pfunpow n f))"
end
lemma pfunpow_0[simp]:
shows "(f ^^ 0) x = Some x"
by simp
lemma pfunpow_Suc_right:
shows "f ^^ Suc n = (λx. Option.bind ((f ^^ n) x) f)"
proof (induct n)
case 0 show ?case by simp
next
case (Suc n) show ?case by (simp flip: Suc)
qed
lemmas pfunpow_simps_right = pfunpow.simps(1) pfunpow_Suc_right
text ‹For code generation.›
context
begin
qualified definition pfunpow :: "nat ⇒ ('a ⇒ 'a option) ⇒ 'a ⇒ 'a option" where
pfunpow_code_def[code_abbrev]: "pfunpow = compow"
lemma pfunpow_code[code]:
shows "pfunpow (Suc n) f = (λx. (Option.bind (f x)) (pfunpow n f))"
and "pfunpow 0 f = Some"
by (simp_all add: pfunpow_code_def fun_eq_iff)
end
lemma pfunpow_add:
shows "f ^^ (m + n) = (λx. Option.bind ((f ^^ m) x) (f ^^ n))"
by (induct m) simp_all
lemma pfunpow_mult:
fixes f :: "'a ⇒ 'a option"
shows "(f ^^ m) ^^ n = f ^^ (m * n)"
by (induct n) (simp_all add: pfunpow_add)
lemma pfunpow_swap1:
fixes f :: "'a ⇒ 'a option"
shows "((f ^^ n) x) ⤜ f = f x ⤜ (f ^^ n)"
by (rule fun_cong[OF trans[OF pfunpow.simps(2)[symmetric] pfunpow_Suc_right], symmetric])
lemma Some_pfunpow[simp]:
shows "Some ^^ n = Some"
by (induct n) simp_all
lemma (in linorder) split_asm_min:
shows "P (min i j) ⟷ ¬ (i ≤ j ∧ ¬ P i ∨ ¬ i ≤ j ∧ ¬ P j)"
by (simp add: min_def)
lemma (in linorder) split_asm_max:
shows "P (max i j) ⟷ ¬ (i ≤ j ∧ ¬ P j ∨ ¬ i ≤ j ∧ ¬ P i)"
by (simp add: max_def)
lemmas case_sum_cancel = case_sum_KK
lemma sum_In_conv:
shows Inl_conv: "Inl a ∈ A <+> B ⟷ a ∈ A"
and Inr_conv: "Inr b ∈ A <+> B ⟷ b ∈ B"
by blast+
lemma restrict_map_UNIV[simp]:
shows "m |` UNIV = m"
by fastforce
lemma finite_distinct_conv:
shows "finite X ⟷ finite {xs . set xs ⊆ X ∧ distinct xs}" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
assume ?lhs show ?rhs
by (rule rev_finite_subset[OF finite_lists_length_le[OF ‹?lhs›, where n="card X"]])
(fastforce dest: card_mono[OF ‹?lhs›] distinct_card)
next
have *: "X ⊆ ⋃(set ` {xs. set xs ⊆ X ∧ distinct xs})" by (clarsimp simp: exI[where x="[x]" for x])
show "?rhs ⟹ ?lhs"
by (blast intro: rev_finite_subset[OF finite_UN_I *])
qed
lemma Min_plus:
fixes X :: "nat set"
assumes "finite X"
assumes "finite Y"
assumes "X ≠ {}"
assumes "Y ≠ {}"
shows "Min X + Min Y = Min {x + y |x y. x ∈ X ∧ y ∈ Y}"
using assms by (force simp: finite_image_set2 add_mono intro: Min_in sym[OF Min_eqI])
lemma always_eventually_pigeonhole:
"(∀i. ∃n≥i. ∃m≤k. P m n) ⟷ (∃m≤k::nat. ∀i::nat. ∃n≥i. P m n)"
proof(induct k)
case (Suc k) then show ?case
by (auto 8 0 dest: le_SucI) (metis order.trans le_SucE linorder_linear)
qed simp
lemma refl_trans_rtrancl:
assumes "refl r"
assumes "trans r"
shows "r⇧* = r"
using assms by (simp add: refl_alt_def rtrancl_trancl_reflcl subset_antisym)
lemma refl_trans_rtrancl_conv:
shows "r⇧* = r ⟷ refl r ∧ trans r"
by (metis refl_rtrancl refl_trans_rtrancl trans_rtrancl)
lemma order_rtrancl: "{(x::_::order, y). x ≤ y}⇧* = {(x, y). x ≤ y}"
by (auto intro!: refl_trans_rtrancl reflI transI)
subsection‹ Inverse image under a function ›
lemma inv_image_alt_def:
shows "inv_image r f = map_prod f f -` r"
unfolding inv_image_def by fastforce
lemma inv_image_id[simp]:
shows "inv_image r id = r"
unfolding inv_image_def by simp
lemma inv_image_union:
shows "inv_image (X ∪ Y) f = inv_image X f ∪ inv_image Y f"
unfolding inv_image_def by fast
lemma inv_image_inter:
shows "inv_image (X ∩ Y) f = inv_image X f ∩ inv_image Y f"
unfolding inv_image_def by fast
subsection‹ Identity relation under a projection\label{sec:id_on_proj} ›
definition Id_on_proj :: "('a ⇒ 'b) ⇒ 'a rel" ("Id⇘_⇙") where
"Id⇘f⇙ = {(s, s'). f s = f s'}"
lemma member_Id_on_proj[simp]:
shows "(x, y) ∈ Id⇘f⇙ ⟷ f x = f y"
unfolding Id_on_proj_def by simp
lemma Id_on_proj_const:
shows "Id⇘λ_. c⇙ = UNIV"
by (simp add: Id_on_proj_def)
lemma Id_on_proj_id:
shows "Id⇘id⇙ = Id"
by (auto simp: Id_on_proj_def Id_def)
lemma Id_weaken[iff]:
shows "Id⇘f⇙ ⊆ Id⇘λs. g (f s)⇙"
and "(λx y. (x, y) ∈ Id⇘f⇙) ≤ (λx y. (x, y) ∈ Id⇘λs. g (f s)⇙)"
by (auto simp: Id_on_proj_def)
lemma refl_Id_on_proj[iff]:
shows "refl Id⇘f⇙"
by (simp add: Id_on_proj_def refl_on_def)
lemma sym_Id_on_proj[iff]:
shows "sym Id⇘f⇙"
by (simp add: Id_on_proj_def sym_def)
lemma trans_Id_on_proj[iff]:
shows "trans Id⇘f⇙"
by (simp add: Id_on_proj_def trans_def)
lemma equiv_Id_on_proj[iff]:
shows "equiv UNIV Id⇘f⇙"
by (simp add: equiv_def)
lemma Id_on_proj_pred_pair:
shows "Id⇘λx. (f x, g x)⇙ = Id⇘f⇙ ∩ Id⇘g⇙"
by (auto simp: Id_on_proj_def)
lemma Id_on_proj_Inf:
shows "(⋂x∈X. Id⇘f x⇙) = Id⇘λs. (λx. (x, f x s)) ` X⇙"
by (fastforce simp: Id_on_proj_def)
subsection‹ Ordering under a projection ›
definition less_eq_on_proj :: "('s ⇒ 'a::ord) ⇒ 's rel" ("❙≤⇘_⇙") where
"❙≤⇘f⇙ = {(s, s'). f s' ≤ f s}"
lemma less_eq_on_proj[simp]:
shows "(x, y) ∈ ❙≤⇘f⇙ ⟷ f y ≤ f x"
unfolding less_eq_on_proj_def by simp
lemma refl_less_eq_on_proj[iff]:
fixes f :: "_ ⇒ _::preorder"
shows "refl (❙≤⇘f⇙)"
by (auto intro: refl_onI)
lemma trans_less_eq_on_proj[iff]:
fixes f :: "_ ⇒ _::preorder"
shows "trans (❙≤⇘f⇙)"
unfolding trans_def by (fastforce elim: order_trans)
subsection‹ Monotonicity ›
lemma mono_inf:
assumes "mono (f::_⇒_::semilattice_inf)"
assumes "mono g"
shows "mono (λx. f x ⊓ g x)"
using assms by (simp add: monotone_def le_infI1 le_infI2)
declare mono2mono_inf[partial_function_mono]
declare mono2mono_sup[cont_intro, partial_function_mono]
lemmas mono2mono_conj[cont_intro, partial_function_mono] = mono2mono_inf[where 'a=bool, simplified inf_bool_def]
lemma monotone_const:
assumes "ordb c c"
shows "monotone orda ordb (λ_. c)"
using assms by (simp add: monotone_def reflpD)
lemma monotone_domain_empty[cont_intro]:
shows "monotone (λx y. False) ordb f"
unfolding monotone_def by blast
lemma monotone_domain_Id:
assumes "reflp ordb"
shows "monotone (λx y. (x, y) ∈ Id) ordb f"
using assms by (simp add: monotone_def reflpD)
lemma monotone_domain_UNIV:
assumes "reflp ordb"
assumes "antisymp ordb"
shows "monotone (λx y. True) ordb f ⟷ (∃c. f = (λ_. c))"
using assms by (auto 7 0 simp: monotone_def reflp_def antisymp_def)
lemma antimono_monotone_domain:
shows "antimono monotone"
unfolding monotone_def by blast
lemma monotone_monotone:
assumes "monotone orda ordb f"
assumes "orda' ≤ orda"
assumes "ordb ≤ ordb'"
shows "monotone orda' ordb' f"
using assms unfolding monotone_def by blast
lemma monotone_domain_infI:
assumes "monotone r ordb f"
shows "monotone (r ⊓ s) ordb f"
and "monotone (s ⊓ r) ordb f"
using assms unfolding monotone_def by blast+
lemma monotone_domain_supD:
assumes "monotone (r ⊔ s) ordb f"
shows "monotone r ordb f"
and "monotone s ordb f"
using assms unfolding monotone_def by blast+
lemma monotone_Id_on_proj:
assumes "⋀v. monotone (λx y. (x, y) ∈ Id⇘f⇙) ordb (P v)"
shows "monotone (λx y. (x, y) ∈ Id⇘f⇙) ordb (λs. P (f s) s)"
using assms unfolding monotone_def Id_on_proj_def by simp
lemma monotone_Id_on_proj':
assumes "reflp ordb"
shows "monotone (λx y. (x, y) ∈ Id⇘f⇙) ordb (λs. P (f s))"
unfolding monotone_def Id_on_proj_def using assms by (simp add: reflpD)
lemma monotone_Inf[cont_intro, partial_function_mono]:
fixes orda :: "'c relp"
fixes F :: "'b ⇒ 'c ⇒ 'a::complete_lattice"
assumes "⋀x. monotone orda (≤) (λy. F x y)"
shows "monotone orda (≤) (λy. ⨅x∈X. F x y)"
using assms by (simp add: INF_mono' monotone_def)
lemma monotone_comp:
fixes f :: "'b ⇒ 'c"
fixes g :: "'a ⇒ 'b"
assumes "monotone ordb ordc f"
assumes "monotone orda ordb g"
shows "monotone orda ordc (f ∘ g)"
using assms unfolding monotone_def by simp
lemma monotone_case_sum:
fixes v :: "'a + 'b"
fixes left :: "'s ⇒ 'a ⇒ bool"
fixes right :: "'s ⇒ 'b ⇒ bool"
assumes "⋀v. monotone orda ordb (λx. left x v)"
assumes "⋀v. monotone orda ordb (λx. right x v)"
shows "monotone orda ordb (λx. case_sum (left x) (right x) v)"
using assms unfolding monotone_def by (simp split: sum.splits)
lemma monotone_case_option:
fixes v :: "'a option"
fixes none :: "'s ⇒ bool"
fixes some :: "'s ⇒ 'a ⇒ bool"
assumes "monotone orda ordb (λs. none s)"
assumes "⋀v. monotone orda ordb (λs. some s v)"
shows "monotone orda ordb (λs. case_option (none s) (some s) v)"
using assms unfolding monotone_def by (simp split: option.splits)
subsection‹ Cartesian product of relations ›
text‹
A set version of \<^const>‹rel_prod› and corresponding projections.
›
definition relprod :: "('a × 'b) set ⇒ ('c × 'd) set ⇒ (('a × 'c) × ('b × 'd)) set" (infixr "×⇩R" 75) where
"relprod P Q = {((a, c), (b, d)) |a b c d. (a, b) ∈ P ∧ (c, d) ∈ Q}"
definition relfst :: "(('a × 'c) × ('b × 'd)) set ⇒ ('a × 'b) set" where
"relfst R = map_prod fst fst ` R"
definition relsnd :: "(('a × 'c) × ('b × 'd)) set ⇒ ('c × 'd) set" where
"relsnd R = map_prod snd snd ` R"
lemma member_relprod[simp]:
shows "(x, y) ∈ P ×⇩R Q ⟷ (fst x, fst y) ∈ P ∧ (snd x, snd y) ∈ Q"
unfolding relprod_def by force
lemma map_prod_image_relprod:
fixes P :: "('a × 'b) set"
fixes Q :: "('c × 'd) set"
fixes f :: "'a × 'c ⇒ 'e"
fixes g :: "'b × 'd ⇒ 'f"
shows "map_prod f g ` (P ×⇩R Q) = {(f (a, c), g (b, d)) |a b c d. (a, b) ∈ P ∧ (c, d) ∈ Q}"
unfolding map_prod_def relprod_def image_def by auto
lemma map_prod_vimage_relprod:
fixes P :: "('a × 'b) set"
fixes Q :: "('c × 'd) set"
fixes f :: "'e ⇒ 'a × 'c"
fixes g :: "'f ⇒ 'b × 'd"
shows "map_prod f g -` (P ×⇩R Q) = {(x, y). (fst (f x), fst (g y)) ∈ P ∧ (snd (f x), snd (g y)) ∈ Q}"
by fastforce
lemma relprod_mono:
assumes "P ⊆ P'"
assumes "Q ⊆ Q'"
shows "P ×⇩R Q ⊆ P' ×⇩R Q'"
unfolding relprod_def using assms by blast
lemma strengthen_relprod[strg]:
assumes "st_ord F P P'"
assumes "st_ord F Q Q'"
shows "st_ord F (P ×⇩R Q) (P' ×⇩R Q')"
using assms by (cases F) auto
lemma mono_relprod:
shows "mono (λx. relprod x Q)"
and "mono (λx. relprod P x)"
unfolding relprod_def by (rule monoI; blast)+
lemma mono_relfst:
shows "mono relfst"
unfolding relfst_def by (rule monoI) blast
lemma mono_relsnd:
shows "mono relsnd"
unfolding relsnd_def by (rule monoI) blast
lemma relfst_subseteq_conv[simp]:
shows "relfst X ⊆ Y ⟷ X ⊆ Y ×⇩R UNIV"
unfolding relfst_def by fastforce
lemma relsnd_subseteq_conv[simp]:
shows "relsnd X ⊆ Y ⟷ X ⊆ UNIV ×⇩R Y"
unfolding relsnd_def by fastforce
lemma relprod_Id[simp]:
shows "Id ×⇩R Id = Id"
unfolding relprod_def by auto
lemma relprod_UNIV[simp]:
shows "UNIV ×⇩R UNIV = UNIV"
unfolding relprod_def by auto
lemma relprod_inter_Id:
shows "Id ∩ UNIV ×⇩R Id = Id"
and "UNIV ×⇩R Id ⊓ Id = Id"
by auto
lemma reflcl_relprod:
shows "(r ×⇩R s)⇧= ⊆ r⇧= ×⇩R s⇧="
unfolding relprod_def by auto
lemma inv_image_fst:
shows "inv_image r fst = r ×⇩R UNIV"
unfolding relprod_def inv_image_def by fastforce
lemma inv_image_snd:
shows "inv_image r snd = UNIV ×⇩R r"
unfolding relprod_def inv_image_def by fastforce
lemma relprod_inter:
shows "r ×⇩R s ∩ r' ×⇩R s' = (r ∩ r') ×⇩R (s ∩ s')"
unfolding relprod_def by blast
lemma relprod_union_subseteq:
shows "r ×⇩R s ∪ r' ×⇩R s' ⊆ (r ∪ r') ×⇩R (s ∪ s')"
unfolding relprod_def by blast
lemma relprod_empty[simp]:
shows "r ×⇩R {} = {}"
and "{} ×⇩R r = {}"
unfolding relprod_def by simp_all
lemma relprod_empty_conv:
shows "r ×⇩R s = {} ⟷ r = {} ∨ s = {}"
unfolding relprod_def by fast
lemma relfst_empty[simp]:
shows "relfst {} = {}"
unfolding relfst_def by simp
lemma relsnd_empty[simp]:
shows "relsnd {} = {}"
unfolding relsnd_def by simp
lemma relprod_relfst_relsnd_subseteq:
shows "P ⊆ relfst P ×⇩R relsnd P"
unfolding relfst_def relsnd_def relprod_def by force
lemma relfst_relprod:
assumes "Q ≠ {}"
shows "relfst (P ×⇩R Q) = P"
unfolding relfst_def relprod_def using assms by force
lemma relsnd_relprod:
assumes "P ≠ {}"
shows "relsnd (P ×⇩R Q) = Q"
unfolding relsnd_def relprod_def using assms by force
lemma relfst_Id[simp]:
shows "relfst Id = Id"
unfolding relfst_def by force
lemma relsnd_Id[simp]:
shows "relsnd Id = Id"
unfolding relsnd_def by force
lemma relfst_UNIV[simp]:
shows "relfst UNIV = UNIV"
unfolding relfst_def by (rule map_prod_surj[OF range_fst range_fst])
lemma relsnd_UNIV[simp]:
shows "relsnd UNIV = UNIV"
unfolding relsnd_def by (rule map_prod_surj[OF range_snd range_snd])
lemma relfst_union:
shows "relfst (R ∪ S) = relfst R ∪ relfst S"
unfolding relfst_def by blast
lemma relsnd_union:
shows "relsnd (R ∪ S) = relsnd R ∪ relsnd S"
unfolding relsnd_def by blast
lemma relprod_unionL:
shows "(P ∪ R) ×⇩R S = P ×⇩R S ∪ R ×⇩R S"
unfolding relprod_def by blast
lemma relprod_unionR:
shows "P ×⇩R (R ∪ S) = P ×⇩R R ∪ P ×⇩R S"
unfolding relprod_def by blast
lemma Id_on_proj_fst:
shows "Id⇘fst⇙ = Id ×⇩R UNIV"
unfolding Id_on_proj_def by force
lemma Id_on_proj_snd:
shows "Id⇘snd⇙ = UNIV ×⇩R Id"
unfolding Id_on_proj_def by force
lemma refl_on_relprodI:
assumes "refl_on A r"
assumes "refl_on B s"
shows "refl_on (A × B) (r ×⇩R s)"
using assms unfolding relprod_def refl_on_def by auto
lemma refl_relprod_conv:
shows "refl (r ×⇩R s) ⟷ refl r ∧ refl s"
unfolding relprod_def refl_on_def by simp
lemma trans_relprod[intro]:
assumes "trans r"
assumes "trans s"
shows "trans (r ×⇩R s)"
using assms unfolding relprod_def trans_def by fast
lemma map_prod_snd_snd_image_Id:
shows "map_prod snd snd ` Id = Id"
by (metis relsnd_Id relsnd_def)
lemma map_prod_fst_fst_vimage:
shows "map_prod fst fst -` X = X ×⇩R UNIV"
by fastforce
lemma map_prod_snd_snd_vimage:
shows "map_prod snd snd -` X = UNIV ×⇩R X"
by fastforce
lemma map_prod_map_prod_vimage_Id:
shows "map_prod (map_prod f g) (map_prod f g) -` Id = map_prod f f -` Id ×⇩R map_prod g g -` Id"
by fastforce
lemma Id_le_relprod_conv:
shows "Id ⊆ r ×⇩R s ⟷ Id ⊆ r ∧ Id ⊆ s"
by fastforce
subsection‹ More transfer ›
context
includes lifting_syntax
begin
lemma antimono_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_total A"
assumes [transfer_rule]: "(A ===> A ===> (=)) (≤) (≤)"
assumes [transfer_rule]: "(B ===> B ===> (=)) (≤) (≤)"
shows "((A ===> B) ===> (=)) antimono antimono"
unfolding antimono_def by transfer_prover
end
paragraph‹ More \<^theory>‹Coinductive.Coinductive_List› and \<^theory>‹Coinductive.TLList› ›
lemmas tset_tmap = TLList.tllist.set_map
lemma not_is_TNil:
shows "¬ is_TNil y ⟷ (∃x xs. y = TCons x xs)"
by (cases y) simp_all
lemma lmap_repeat:
shows "lmap f (repeat x) = repeat (f x)"
by coinduction simp
lemma tlength_0_conv:
shows "tlength xs = 0 ⟷ (∃b. xs = TNil b)"
by (cases xs) simp_all
lemma tfinite_tlength_conv:
shows "tfinite xs ⟷ (∃n. tlength xs = enat n)"
by (simp add: lfinite_conv_llength_enat)
lemma tdropn_eq_TNil_conv:
shows "tdropn i xs = TNil b ⟷ b = terminal xs ∧ tlength xs ≤ enat i" (is ?thesis1)
and "TNil b = tdropn i xs ⟷ b = terminal xs ∧ tlength xs ≤ enat i" (is ?thesis2)
proof -
show ?thesis1
proof(induct i arbitrary: xs)
case (0 xs) show ?case
by (cases xs) (auto simp: enat_0)
next
case (Suc i xs) then show ?case
by (cases xs) (auto simp flip: eSuc_enat)
qed
then show ?thesis2
by (rule eq_commute_conv)
qed
lemma tdropn_eq_TCons_tlength_conv:
shows "(∃y ys. tdropn i xs = TCons y ys) ⟷ (enat i < tlength xs)"
by (metis leI tdropn_Suc_conv_tdropn tdropn_eq_TNil_conv(1) tllist.distinct(1))
lemma tdropn_eq_TCons_tlengthD:
assumes "tdropn i xs = TCons y ys"
shows "enat i < tlength xs"
using assms by (simp flip: tdropn_eq_TCons_tlength_conv)
lemma tdropn_tlength:
assumes "tlength xs ≤ enat i"
shows "tdropn i xs = TNil (terminal xs)"
by (simp add: assms tdropn_eq_TNil_conv)
lemma terminal_tdropn[simp]:
shows "terminal (tdropn i xs) = terminal xs"
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case by (cases xs) simp_all
qed simp
lemma in_tset_tdropnD:
assumes "x ∈ tset (tdropn i xs)"
shows "x ∈ tset xs"
using assms
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case by (cases xs) simp_all
qed simp
paragraph‹ New constants ›
definition trepeat :: "'a ⇒ ('a, 'b) tllist" where
"trepeat x = tllist_of_llist undefined (Coinductive_List.repeat x)"
primrec treplicate :: "nat ⇒ 'a ⇒ 'b ⇒ ('a, 'b) tllist" where
"treplicate 0 x v = TNil v"
| "treplicate (Suc i) x v = TCons x (treplicate i x v)"
primrec tshift :: "'a list ⇒ ('a, 'b) tllist ⇒ ('a, 'b) tllist" where
"tshift [] ys = ys"
| "tshift (x # xs) ys = TCons x (tshift xs ys)"
primrec ttake :: "nat ⇒ ('a, 'b) tllist ⇒ 'a list × 'b option" where
"ttake 0 xs = ([], None)"
| "ttake (Suc i) xs = (case xs of TNil b ⇒ ([], Some b) | TCons x xs ⇒ apfst ((#) x) (ttake i xs))"
definition tshift2 :: "'a list × 'b option ⇒ ('a, 'b) tllist ⇒ ('a, 'b) tllist" where
"tshift2 xsv ys = tshift (fst xsv) (case_option ys TNil (snd xsv))"
lemma trepeat_unfold:
shows "trepeat x = TCons x (trepeat x)"
using iterates by (fastforce simp add: trepeat_def simp flip: tllist_of_llist_LCons)
lemma not_finite_trepeat[iff]:
shows "¬tfinite (trepeat x)"
by (simp add: trepeat_def)
lemma trepeat_simps[simp]:
shows "thd (trepeat x) = x"
and "ttl (trepeat x) = trepeat x"
and "tset (trepeat x) = {x}"
and "trepeat x ≠ TNil b"
and "TNil b ≠ trepeat x"
by (simp_all add: trepeat_def lnull_iterates[unfolded lnull_def])
lemma case_tllist_trepeat:
shows "case_tllist tnil tcons (trepeat x) = tcons x (trepeat x)"
by (subst trepeat_unfold) simp
lemma trepeat_eq_TCons_conv:
shows "trepeat x = TCons y ys ⟷ x = y ∧ ys = trepeat x"
and "TCons y ys = trepeat x ⟷ x = y ∧ ys = trepeat x"
by (subst trepeat_unfold; fast)+
lemma tmap_trepeat:
shows "tmap sf vf (trepeat s) = trepeat (sf s)"
by (simp add: trepeat_def lmap_repeat tmap_tllist_of_llist)
lemma tdropn_trepeat:
shows "tdropn i (trepeat x) = trepeat x"
proof(induct i)
case (Suc i) then show ?case by (subst trepeat_unfold) simp
qed simp
lemma ttake_trepeat:
shows "ttake i (trepeat x) = (List.replicate i x, None)"
by (induct i) (simp_all add: trepeat_eq_TCons_conv split: tllist.split)
lemma terminal_treplicate:
shows "terminal (treplicate i x v) = v"
by (induct i) simp_all
lemma finite_treplicate[iff]:
shows "tfinite (treplicate i x v)"
by (induct i) simp_all
lemma tset_treplicate:
shows "tset (treplicate i x v) = (case i of 0 ⇒ {} | Suc _ ⇒ {x})"
by (induct i) (simp_all split: nat.split)
lemma tlength_treplicate:
shows "tlength (treplicate i x v) = enat i"
by (induct i) (simp_all add: enat_0 eSuc_enat)
lemma tmap_treplicate:
shows "tmap f g (treplicate i x v) = treplicate i (f x) (g v)"
by (induct i) simp_all
lemma tdropn_treplicate:
shows "tdropn i (treplicate j x v) = treplicate (j - i) x v"
proof(induct j arbitrary: i)
case (Suc j i) then show ?case by (cases i) simp_all
qed simp
lemma ttake_treplicate:
shows "ttake i (treplicate j x v) = (replicate (min i j) x, if i ≤ j then None else Some v)"
proof(induct j arbitrary: i)
case (0 i) then show ?case by (cases i) simp_all
next
case (Suc j i) then show ?case by (cases i) simp_all
qed
lemmas treplicate_simps[simp] =
terminal_treplicate
tset_treplicate
tlength_treplicate
tmap_treplicate
tdropn_treplicate
ttake_treplicate
lemma tshift_sel[simp]:
shows "thd (tshift xs ys) = (if List.null xs then thd ys else hd xs)"
and "ttl (tshift xs ys) = (if List.null xs then ttl ys else tshift (tl xs) ys)"
by (case_tac [!] xs) simp_all
lemma tfinite_tshift[simp]:
shows "tfinite (tshift xs ys) ⟷ tfinite ys"
by (induct xs) simp_all
lemma tlength_tshift:
shows "tlength (tshift xs ys) = enat (length xs) + tlength ys"
by (induct xs) (simp_all add: enat_0 eSuc_plus flip: eSuc_enat)
lemma tmap_tshift:
shows "tmap f g (tshift xs ys) = tshift (map f xs) (tmap f g ys)"
by (induct xs) simp_all
lemma tshift_append:
shows "tshift (xs @ ys) zs = tshift xs (tshift ys zs)"
by (induct xs) simp_all
lemma tshift_same_conv[simp]:
shows "tshift xs ys = tshift xs zs ⟷ ys = zs"
by (induct xs) simp_all
lemma tset_tshift:
shows "tset (tshift xs ys) = set xs ∪ tset ys"
by (induct xs) simp_all
lemma terminal_tshift:
shows "terminal (tshift xs ys) = terminal ys"
by (induct xs) simp_all
lemma tdropn_tshift:
shows "tdropn i (tshift xs ys) = tshift (drop i xs) (tdropn (i - length xs) ys)"
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case
by (cases xs) simp_all
qed simp
lemma tshift_drop:
shows "tshift (drop i xs) ys = tdropn (min i (length xs)) (tshift xs ys)"
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case
by (cases xs) simp_all
qed simp
lemma tshift_fst_ttake_tdropn_id[simp]:
shows "tshift (fst (ttake i xs)) (tdropn i xs) = xs"
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case
by (cases xs) simp_all
qed simp
lemma tshift_eq_TNil_conv:
shows "tshift ys zs = TNil v ⟷ ys = [] ∧ zs = TNil v" (is ?thesis1)
and "TNil v = tshift ys zs ⟷ ys = [] ∧ zs = TNil v" (is ?thesis2)
proof -
show ?thesis1 by (cases ys) simp_all
then show ?thesis2 by (rule eq_commute_conv)
qed
lemma tshift_eq_TCons_conv:
shows "tshift ys zs = TCons x xs ⟷ (ys = [] ∧ zs = TCons x xs ∨ (∃ys'. ys = x # ys' ∧ tshift ys' zs = xs))" (is ?thesis1)
and "TCons x xs = tshift ys zs ⟷ (ys = [] ∧ zs = TCons x xs ∨ (∃ys'. ys = x # ys' ∧ tshift ys' zs = xs))" (is ?thesis2)
proof -
show ?thesis1 by (cases ys) simp_all
then show ?thesis2 by (rule eq_commute_conv)
qed
lemma tmap_eq_tshift_conv:
shows "tmap f g xs = tshift ys zs ⟷ (∃us vs. xs = tshift us vs ∧ ys = map f us ∧ zs = tmap f g vs)" (is ?thesis1)
and "tshift ys zs = tmap f g xs ⟷ (∃us vs. xs = tshift us vs ∧ ys = map f us ∧ zs = tmap f g vs)" (is ?thesis2)
proof -
show ?thesis1
proof(induct ys arbitrary: xs zs)
case (Cons y ys xs zs) then show ?case
by (cases xs) (auto simp: Cons_eq_map_conv tshift_eq_TNil_conv tshift_eq_TCons_conv)
qed auto
then show ?thesis2 by (rule eq_commute_conv)
qed
lemma ttake_tshift:
shows "ttake i (tshift xs ys)
= (if i ≤ length xs then (take i xs, None) else apfst ((@) xs) (ttake (i - length xs) ys))"
proof(induct i arbitrary: xs)
case (Suc i) then show ?case
by (cases xs; cases ys) (simp_all add: apfst_compose)
qed simp
lemma tshift_eq_trepeat_conv:
shows "tshift xs ys = trepeat x ⟷ set xs ⊆ {x} ∧ ys = trepeat x" (is ?thesis1)
and "trepeat x = tshift xs ys ⟷ set xs ⊆ {x} ∧ ys = trepeat x" (is ?thesis2)
proof -
show ?thesis1 by (induct xs arbitrary: ys) (auto simp: trepeat_eq_TCons_conv)
then show ?thesis2 by (rule eq_commute_conv)
qed
lemma tshift_eq_tshift_conv2:
shows "tshift xs ys = tshift zs ts
⟷ (∃us. xs = zs @ us ∧ tshift us ys = ts ∨ xs @ us = zs ∧ ys = tshift us ts)"
proof(induct xs arbitrary: ys zs ts)
case (Cons x xs) show ?case
by (auto simp: tshift_append tshift_eq_TCons_conv Cons_eq_append_conv eq_commute_conv[OF Cons])
qed auto
lemma tshift2_simps[simp]:
shows "tshift2 (xs, Some v) ys = tshift xs (TNil v)"
and "tshift2 (xs, None) ys = tshift xs ys"
and "tshift2 (x # xs, w) ys = TCons x (tshift2 (xs, w) ys)"
and "tshift2 (apfst ((#) x) zs) ys = TCons x (tshift2 zs ys)"
by (simp_all add: tshift2_def)
lemma tlength_tshift2:
shows "tlength (tshift2 xsv ys)
= enat (length (fst xsv)) + (case_option (tlength ys) (λ_. 0) (snd xsv))"
by (simp add: tshift2_def tlength_tshift split: option.split)
lemma tfinite_tshift2[simp]:
shows "tfinite (tshift2 xsv ys) ⟷ (snd xsv = None ⟶ tfinite ys)"
by (simp add: tshift2_def split: option.split)
lemma tdropn_tshift2:
shows "tdropn i (tshift2 xsv ys) = tshift2 (apfst (drop i) xsv) (tdropn (i - length (fst xsv)) ys)"
by (simp add: tshift2_def tdropn_tshift split: option.split)
lemma ttake_TNil:
shows "ttake i (TNil b) = ([], case i of 0 ⇒ None | Suc _ ⇒ Some b)"
by (cases i) simp_all
lemma ttake_tmap:
shows "ttake i (tmap f g xs) = map_prod (map f) (map_option g) (ttake i xs)"
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case
by (cases xs) (simp_all add: comp_def)
qed simp
lemma in_set_ttakeD:
assumes "x ∈ set (fst (ttake i xs))"
shows "x ∈ tset xs"
using assms
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case
by (cases xs) auto
qed simp
lemma length_ttake:
shows "length (fst (ttake i xs)) = min i (case tlength xs of ∞ ⇒ i | enat j ⇒ j)"
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case
by (cases xs; clarsimp split: enat.split simp: eSuc_enat)
qed (simp split: enat.split)
lemma ttake_eq_None_conv:
shows "snd (ttake i xs) = None ⟷ enat i ≤ tlength xs" (is ?thesis1)
and "None = snd (ttake i xs) ⟷ enat i ≤ tlength xs" (is ?thesis2)
proof -
show ?thesis1
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case
by (cases xs) (simp_all add: Suc_ile_eq enat_0_iff)
qed (simp add: enat_0)
then show ?thesis2
by (rule eq_commute_conv)
qed
lemma ttake_eq_Some_conv:
shows "snd (ttake i xs) = Some b ⟷ b = terminal xs ∧ tlength xs < enat i" (is ?thesis1)
and "Some b = snd (ttake i xs) ⟷ b = terminal xs ∧ tlength xs < enat i" (is ?thesis2)
proof -
show ?thesis1
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case
by (cases xs) (auto simp flip: eSuc_enat)
qed (simp add: enat_0)
then show ?thesis2
by (rule eq_commute_conv)
qed
lemma ttake_eq_Nil_conv:
shows "fst (ttake i xs) = [] ⟷ i = 0 ∨ is_TNil xs" (is ?thesis1)
and "[] = fst (ttake i xs) ⟷ i = 0 ∨ is_TNil xs" (is ?thesis2)
proof -
show ?thesis1
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case
by (cases xs) simp_all
qed simp
then show ?thesis2
by (rule eq_commute_conv)
qed
lemma take_fst_ttake:
shows "take i (fst (ttake j xs)) = fst (ttake (min i j) xs)"
proof(induct j arbitrary: xs i)
case (Suc j xs i) then show ?case
by (cases xs; cases i) simp_all
qed simp
lemma tshift2_ttake_shorter:
assumes "tlength xs < enat i"
shows "tshift2 (ttake i xs) ys = xs"
using assms
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case
by (cases xs) (simp_all flip: eSuc_enat)
qed (simp add: enat_0)
lemma tshift2_ttake_tdropn_id:
shows "tshift2 (ttake i xs) (tdropn i xs) = xs"
by (simp add: tshift2_def ttake_eq_Some_conv flip: tdropn_tlength[where i=i] split: option.split)
lemma ttake_tshift2:
shows "ttake i (tshift2 xsv ys)
= (if i ≤ length (fst xsv) then (take i (fst xsv), None) else apfst ((@) (fst xsv)) (ttake (i - length (fst xsv)) (case_option ys TNil (snd xsv))))"
by (simp add: tshift2_def ttake_tshift)
lemma tfinite_ttake_all:
assumes "tfinite xs"
obtains j where "tshift2 (ttake j xs) ys = xs"
apply atomize_elim
using assms
proof(induct rule: tfinite_induct)
case (TCons x xs)
from TCons(2) obtain j where "tshift2 (ttake j xs) ys = xs" ..
then show ?case by (simp add: tshift2_def exI[where x="Suc j"])
qed (simp add: exI[where x=1])
lemma fst_ttake_flat:
assumes "tlength xs ≤ enat i"
assumes "i ≤ j"
shows "fst (ttake i xs) = fst (ttake j xs)"
by (metis assms enat.simps(4) enat_ile enat_ord_simps(1) length_ttake min.absorb1 min.absorb2 take_all_iff take_fst_ttake)
lemma snd_ttake_flat:
assumes "tlength xs < enat i"
assumes "i ≤ j"
shows "snd (ttake i xs) = snd (ttake j xs)"
by (metis assms order.trans enat_ord_simps(1) option.collapse ttake_eq_None_conv(2) ttake_eq_Some_conv(2))
lemma ttake_flat:
assumes "tlength xs < enat i"
assumes "i ≤ j"
shows "ttake i xs = ttake j xs"
by (simp add: assms fst_ttake_flat snd_ttake_flat order_less_imp_le prod.expand)
lemma ttake_add:
shows "ttake (i + j) xs
= (let xsv = ttake i xs in
case snd xsv of None ⇒ apfst ((@) (fst xsv)) (ttake j (tdropn i xs)) | Some _ ⇒ xsv)"
by (induct i arbitrary: xs) (auto simp: Let_def prod.expand split: option.splits tllist.splits)
lemma nth_ttake:
assumes "i <j"
assumes "enat i < tlength xs"
shows "fst (ttake j xs) ! i = tnth xs i"
using assms
proof(induct j arbitrary: xs i)
case (Suc j xs i) then show ?case
by (cases i) (auto simp: Suc_ile_eq split: tllist.split)
qed simp
lemma ttake_eq_imp_eq:
assumes "⋀i. ttake i xs = ttake i ys"
shows "xs = ys"
using assms
proof(coinduction arbitrary: xs ys)
case (Eq_tllist xs ys) show ?case
proof(intro conjI impI allI exI)
from spec[OF Eq_tllist, where x=1] show "is_TNil xs ⟷ is_TNil ys"
by (simp split: tllist.split_asm)
from spec[OF Eq_tllist, where x=1] show "terminal xs = terminal ys" if "is_TNil xs" and "is_TNil ys"
using that by (simp split: tllist.split_asm)
from spec[OF Eq_tllist, where x=1] show "thd xs = thd ys" if "¬is_TNil xs" and "¬is_TNil ys"
using that by (simp split: tllist.split_asm)
show "ttake i (ttl xs) = ttake i (ttl ys)" if "¬is_TNil xs" and "¬is_TNil ys" for i
using spec[OF Eq_tllist, where x="Suc i"] that
by (simp add: apfst_def map_prod_def split_def prod.expand split: tllist.split_asm)
qed simp_all
qed
end