# Theory Basic

```(* Author: Julian Brunner *)
(* This is originally a part of the CAVA model checker *)
theory Basic
imports
Main
begin

abbreviation (input) "const x ≡ λ _. x"

lemma infinite_subset[trans]: "infinite A ⟹ A ⊆ B ⟹ infinite B" using infinite_super by this
lemma finite_subset[trans]: "A ⊆ B ⟹ finite B ⟹ finite A" using finite_subset by this

declare infinite_coinduct[case_names infinite, coinduct pred: infinite]
lemma infinite_psubset_coinduct[case_names infinite, consumes 1]:
assumes "R A"
assumes "⋀ A. R A ⟹ ∃ B ⊂ A. R B"
shows "infinite A"
proof
assume "finite A"
then show "False" using assms by (induct rule: finite_psubset_induct) (auto)
qed

lemma GreatestI:
fixes k :: nat
assumes "P k" "⋀ k. P k ⟹ k ≤ l"
shows "P (GREATEST k. P k)"
proof (rule GreatestI_nat)
show "P k" using assms(1) by this
show "k ≤ l" if "P k" for k using assms(2) that by force
qed
lemma Greatest_le:
fixes k :: nat
assumes "P k" "⋀ k. P k ⟹ k ≤ l"
shows "k ≤ (GREATEST k. P k)"
proof (rule Greatest_le_nat)
show "P k" using assms(1) by this
show "k ≤ l" if "P k" for k using assms(2) that by force
qed
lemma Greatest_not_less:
fixes k :: nat
assumes "k > (GREATEST k. P k)" "⋀ k. P k ⟹ k ≤ l"
shows "¬ P k"
proof
assume 1: "P k"
have 2: "k ≤ (GREATEST k. P k)" using Greatest_le 1 assms(2) by this
show "False" using assms(1) 2 by auto
qed

lemma finite_set_of_finite_maps':
assumes "finite A" "finite B"
shows "finite {m. dom m ⊆ A ∧ ran m ⊆ B}"
proof -
have "{m. dom m ⊆ A ∧ ran m ⊆ B} = (⋃ 𝒜 ∈ Pow A. {m. dom m = 𝒜 ∧ ran m ⊆ B})" by auto
also have "finite …" using finite_subset assms by (auto intro: finite_set_of_finite_maps)
finally show ?thesis by this
qed

primrec alternate :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ nat ⇒ ('a ⇒ 'a)" where
"alternate f g 0 = id" | "alternate f g (Suc k) = alternate g f k ∘ f"

lemma alternate_Suc[simp]: "alternate f g (Suc k) = (if even k then f else g) ∘ alternate f g k"
proof (induct k arbitrary: f g)
case (0)
show ?case by simp
next
case (Suc k)
have "alternate f g (Suc (Suc k)) = alternate g f (Suc k) ∘ f" by auto
also have "… = (if even k then g else f) ∘ (alternate g f k ∘ f)" unfolding Suc by auto
also have "… = (if even (Suc k) then f else g) ∘ alternate f g (Suc k)" by auto
finally show ?case by this
qed

declare alternate.simps(2)[simp del]

lemma alternate_antimono:
assumes "⋀ x. f x ≤ x" "⋀ x. g x ≤ x"
shows "antimono (alternate f g)"
proof
fix k l :: nat
assume 1: "k ≤ l"
obtain n where 2: "l = k + n" using le_Suc_ex 1 by auto
have 3: "alternate f g (k + n) ≤ alternate f g k"
proof (induct n)
case (0)
show ?case by simp
next
case (Suc n)
have "alternate f g (k + Suc n) ≤ alternate f g (k + n)" using assms by (auto intro: le_funI)
also have "… ≤ alternate f g k" using Suc by this
finally show ?case by this
qed
show "alternate f g l ≤ alternate f g k" using 3 unfolding 2 by this
qed

end
```