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