Theory Probabilistic_Timed_Automata.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