# Theory Lib

theory Lib
imports Complex_Main
```theory "Lib"
imports
Complex_Main
begin
section ‹Generic Mathematical Background Lemmas›

lemma finite_subset [simp]: "finite M ⟹ finite {x∈M. P x}"
by simp

lemma finite_powerset [simp]: "finite M ⟹ finite {S. S⊆M}"
by simp

definition fst_proj:: "('a*'b) set ⇒ 'a set"
where "fst_proj M ≡ {A. ∃B. (A,B)∈M}"

definition snd_proj:: "('a*'b) set ⇒ 'b set"
where "snd_proj M ≡ {B. ∃A. (A,B)∈M}"

lemma fst_proj_mem [simp]: "(A ∈ fst_proj M) = (∃B. (A,B)∈M)"
unfolding fst_proj_def by auto

lemma snd_proj_mem [simp]: "(B ∈ snd_proj M) = (∃A. (A,B)∈M)"
unfolding snd_proj_def by auto

lemma fst_proj_prop: "∀x∈fst_proj {(A,B)| A B. P A ∧ R A B}. P(x)"
unfolding fst_proj_def by auto

lemma snd_proj_prop: "∀x∈snd_proj {(A,B) | A B. P B ∧ R A B}. P(x)"
unfolding snd_proj_def by auto

lemma map_cons: "map f (Cons x xs) = Cons (f x) (map f xs)"
by (rule List.list.map)
lemma map_append: "map f (append xs ys) = append (map f xs) (map f ys)"
by simp

text‹Lockstep induction schema for two simultaneous least fixpoints.
If the successor step and supremum step of two least fixpoint inflations
preserve a relation, then that relation holds of the two respective least fixpoints.›

lemma lfp_lockstep_induct [case_names monof monog step union]:
fixes f :: "'a::complete_lattice ⇒ 'a"
and g :: "'b::complete_lattice ⇒ 'b"
assumes monof: "mono f"
and monog: "mono g"
and R_step: "⋀A B. A ≤ lfp(f) ⟹ B ≤ lfp(g) ⟹ R A B ⟹ R (f(A)) (g(B))"
and R_Union: "⋀M::('a*'b) set. (∀(A,B)∈M. R A B) ⟹ R (Sup (fst_proj M)) (Sup (snd_proj M))"
shows "R (lfp f) (lfp g)"
proof-
(*using idea of proof of "Inductive.thy:lfp_ordinal_induct"*)
let ?M = "{(A,B). A ≤ lfp f ∧ B ≤ lfp g ∧ R A B}"
from R_Union have supdoes: "R (Sup (fst_proj ?M)) (Sup (snd_proj ?M))" by simp
also have "Sup (fst_proj ?M) = lfp f" and "Sup (snd_proj ?M) = lfp g"
proof (rule antisym)
show fle: "Sup (fst_proj ?M) ≤ lfp f"
using fst_proj_prop Sup_le_iff by fastforce
then have "f (Sup (fst_proj ?M)) ≤ f (lfp f)"
by (rule monof [THEN monoD])
then have fsup: "f (Sup (fst_proj ?M)) ≤ lfp f"
using monof [THEN lfp_unfold] by simp

have gle: "Sup (snd_proj ?M) ≤ lfp g"
using snd_proj_prop Sup_le_iff by fastforce
then have "g (Sup (snd_proj ?M)) ≤ g (lfp g)"
by (rule monog [THEN monoD])
then have gsup: "g (Sup (snd_proj ?M)) ≤ lfp g"
using monog [THEN lfp_unfold] by simp

from fsup and gsup have fgsup: "(f(Sup(fst_proj ?M)), g(Sup(snd_proj ?M))) ∈ ?M"
using R_Union R_step Sup_le_iff
using calculation fle gle by blast

from fgsup have "f (Sup (fst_proj ?M)) ≤ Sup (fst_proj ?M)"
using Sup_upper by (metis (mono_tags, lifting) fst_proj_def mem_Collect_eq)
then show fge: "lfp f ≤ Sup (fst_proj ?M)"
by (rule lfp_lowerbound)
show "Sup (snd_proj ?M) = lfp g"
proof (rule antisym)
show "Sup (snd_proj ?M) ≤ lfp g" by (rule gle)
from fgsup have "g (Sup (snd_proj ?M)) ≤ Sup (snd_proj ?M)"
using Sup_upper by (metis (mono_tags, lifting) snd_proj_def mem_Collect_eq)
then show gge: "lfp g ≤ Sup (snd_proj ?M)"
by (rule lfp_lowerbound)
qed
qed
then show ?thesis using supdoes by simp
qed

lemma sup_eq_all: "(⋀A. (A∈M ⟹ f(A)=g(A)))
⟹ Sup {f(A) | A. A∈M} = Sup {g(A) | A. A∈M}"
by metis

lemma sup_corr_eq_chain: "⋀M::('a::complete_lattice*'a) set. (∀(A,B)∈M. f(A)=g(B)) ⟹ (Sup {f(A) | A. A∈fst_proj M} = Sup {g(B) | B. B∈snd_proj M})"
by (metis (mono_tags, lifting) case_prod_conv fst_proj_mem snd_proj_mem)

end```