(* 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