Theory Basis

(*<*)
theory Basis
imports
  "HOL-Library.While_Combinator"
begin

(*>*)
section‹ Point-free notation ›

text‹

We adopt point-free notation for our assertions over program states.

›

abbreviation (input)
  pred_K :: "'b ⇒ 'a ⇒ 'b" (‹⟨_⟩›) where
  "⟨f⟩ ≡ λs. f"

abbreviation (input)
  pred_not :: "('a ⇒ bool) ⇒ 'a ⇒ bool" (‹❙¬›) where
  "❙¬a ≡ λs. ¬a s"

abbreviation (input)
  pred_conj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" (infixr ‹❙∧› 35) where
  "a ❙∧ b ≡ λs. a s ∧ b s"

abbreviation (input)
  pred_implies :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" (infixr ‹❙⟶› 25) where
  "a ❙⟶ b ≡ λs. a s ⟶ b s"

abbreviation (input)
  pred_eq :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ bool" (infix ‹❙=› 40) where
  "a ❙= b ≡ λs. a s = b s"

abbreviation (input)
  pred_member :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b set) ⇒ 'a ⇒ bool" (infix ‹❙∈› 40) where
  "a ❙∈ b ≡ λs. a s ∈ b s"

abbreviation (input)
  pred_neq :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ bool" (infix ‹❙≠› 40) where
  "a ❙≠ b ≡ λs. a s ≠ b s"

abbreviation (input)
  pred_If :: "('a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" (‹(❙if (_)/ ❙then (_)/ ❙else (_))› [0, 0, 10] 10) where
  "❙if P ❙then x ❙else y ≡ λs. if P s then x s else y s"

abbreviation (input)
  pred_less :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ bool" (infix ‹❙<› 40) where
  "a ❙< b ≡ λs. a s < b s"

abbreviation (input)
  pred_le :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ bool" (infix ‹❙≤› 40) where
  "a ❙≤ b ≡ λs. a s ≤ b s"

abbreviation (input)
  pred_plus :: "('a ⇒ 'b::plus) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixl ‹❙+› 65) where
  "a ❙+ b ≡ λs. a s + b s"

abbreviation (input)
  pred_minus :: "('a ⇒ 'b::minus) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixl ‹❙-› 65) where
  "a ❙- b ≡ λs. a s - b s"

abbreviation (input)
  fun_fanout :: "('a ⇒ 'b) ⇒ ('a ⇒ 'c) ⇒ 'a ⇒ 'b × 'c" (infix ‹❙⨝› 35) where
  "f ❙⨝ g ≡ λx. (f x, g x)"

abbreviation (input)
  pred_all :: "('b ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool" (binder ‹❙∀› 10) where
  "❙∀x. P x ≡ λs. ∀x. P x s"

abbreviation (input)
  pred_ex :: "('b ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool" (binder ‹❙∃› 10) where
  "❙∃x. P x ≡ λs. ∃x. P x s"

section‹ ``Monoidal'' Hoare logic ›

text‹

In the absence of a general-purpose development of Hoare Logic for
total correctness in Isabelle/HOL\footnote{At the time of writing the
distribution contains several for partial correctness, and one for
total correctness over a language with restricted expressions.  SIMPL
(\<^cite>‹"DBLP:journals/afp/Schirmer08"›) is overkill for our present
purposes.}, we adopt the following syntactic contrivance that eases
making multiple assertions about function results. ``Programs''
consist of the state-transformer semantics of statements.

›

definition valid :: "('s ⇒ bool) ⇒ ('s ⇒ 's) ⇒ ('s ⇒ bool) ⇒ bool" (‹⦃_⦄/ _/ ⦃_⦄›) where
  "⦃P⦄ c ⦃Q⦄ ≡ ∀s. P s ⟶ Q (c s)"

notation (input) id (‹SKIP›)
notation fcomp (infixl ‹;;› 60)

named_theorems wp_intro "weakest precondition intro rules"

lemma seqI[wp_intro]:
  assumes "⦃Q⦄ d ⦃R⦄"
  assumes "⦃P⦄ c ⦃Q⦄"
  shows "⦃P⦄ c ;; d ⦃R⦄"
using assms by (simp add: valid_def)

lemma iteI[wp_intro]:
  assumes "⦃P'⦄ x ⦃Q⦄"
  assumes "⦃P''⦄ y ⦃Q⦄"
  shows "⦃❙if b ❙then P' ❙else P''⦄ ❙if b ❙then x ❙else y ⦃Q⦄"
using assms by (simp add: valid_def)

lemma assignI[wp_intro]:
  shows "⦃Q ∘ f⦄ f ⦃Q⦄"
by (simp add: valid_def)

lemma whileI:
  assumes "⦃I'⦄ c ⦃I⦄"
  assumes "⋀s. I s ⟹ if b s then I' s else Q s"
  assumes "wf r"
  assumes "⋀s. ⟦ I s; b s ⟧ ⟹ (c s, s) ∈ r"
  shows "⦃I⦄ while b c ⦃Q⦄"
using assms by (simp add: while_rule valid_def)

lemma hoare_pre:
  assumes "⦃R⦄ f ⦃Q⦄"
  assumes "⋀s. P s ⟹ R s"
  shows "⦃P⦄ f ⦃Q⦄"
using assms by (simp add: valid_def)

lemma hoare_post_imp:
  assumes "⦃P⦄ a ⦃Q⦄"
  assumes "⋀s. Q s ⟹ R s"
  shows "⦃P⦄ a ⦃R⦄"
using assms by (simp add: valid_def)

text‹

Note that the @{thm[source] assignI} rule applies to all state
transformers, and therefore the order in which we attempt to use the
@{thm[source] wp_intro} rules matters.

›


section‹ Properties of iterated functions on finite sets ›

text‹

We begin by fixing the @{term "f"} and @{term "x0"} under
consideration in a locale, and establishing Knuth's properties.

The sequence is modelled as a function ‹seq :: nat
⇒ 'a› in the obvious way.

›

locale fx0 =
  fixes f :: "'a::finite ⇒ 'a"
  fixes x0 :: "'a"
begin

definition seq' :: "'a ⇒ nat ⇒ 'a" where
  "seq' x i ≡ (f ^^ i) x"

abbreviation "seq ≡ seq' x0"
(*<*)

declare (in -) fx0.seq'_def[code]

lemma seq'_simps[simp]:
  "seq' x 0 = x"
  "seq' x (Suc i) = f (seq' x i)"
  "seq' (f x) i ∈ range (seq' x)"
by (auto intro: range_eqI[where x="Suc i"] simp: seq'_def funpow_swap1)

lemma seq_inj:
  "⟦ seq' x i = seq' x j; p = i + n; q = j + n ⟧ ⟹ seq' x p = seq' x q"
apply hypsubst_thin
by (induct n) simp_all
(*>*)
text‹

The parameters ‹lambda› and ‹mu› must exist by the
pigeonhole principle.

›

lemma seq'_not_inj_on_card_UNIV:
  shows "¬inj_on (seq' x) {0 .. card (UNIV::'a set)}"
by (simp add: inj_on_iff_eq_card)
   (metis UNIV_I card_mono finite lessI not_less subsetI)

definition properties :: "nat ⇒ nat ⇒ bool" where
  "properties lambda mu ≡
     0 < lambda
   ∧ inj_on seq {0 ..< mu + lambda}
   ∧ (∀i≥mu. ∀j. seq (i + j * lambda) = seq i)"

lemma properties_existence:
  obtains lambda mu
  where "properties lambda mu"
proof -
  obtain l where l: "inj_on seq {0..l} ∧ ¬inj_on seq {0..Suc l}"
    using ex_least_nat_less[where P="λub. ¬inj_on seq {0..ub}" and n="card (UNIV :: 'a set)"]
          seq'_not_inj_on_card_UNIV
    by fastforce
  moreover
  from l obtain mu where mu: "mu ≤ l ∧ seq (Suc l) = seq mu"
    by (fastforce simp: atLeastAtMostSuc_conv)
  moreover
  define lambda where "lambda = l - mu + 1"
  have "seq (i + j * lambda) = seq i" if "mu ≤ i" for i j
  using that proof (induct j)
    case (Suc j)
    from l mu have F: "seq (l + j + 1) = seq (mu + j)" for j
      by (fastforce elim: seq_inj)
    from mu Suc F[where j="i + j * lambda - mu"] show ?case
      by (simp add: lambda_def field_simps)
  qed simp
  ultimately have "properties lambda mu"
    by (auto simp: properties_def lambda_def atLeastLessThanSuc_atLeastAtMost)
  then show thesis ..
qed

end

text‹

To ease further reasoning, we define a new locale that fixes @{term
"lambda"} and @{term "mu"}, and assume these properties hold. We then
derive further rules that are easy to apply.

›

locale properties = fx0 +
  fixes lambda mu :: "nat"
  assumes P: "properties lambda mu"
begin

lemma properties_lambda_gt_0:
  shows "0 < lambda"
using P by (simp add: properties_def)

lemma properties_loop:
  assumes "mu ≤ i"
  shows "seq (i + j * lambda) = seq i"
using P assms by (simp add: properties_def)

lemma properties_mod_lambda:
  assumes "mu ≤ i"
  shows "seq i = seq (mu + (i - mu) mod lambda)"
using properties_loop[where i="mu + (i - mu) mod lambda" and j="(i - mu) div lambda"] assms
by simp

lemma properties_distinct:
  assumes "j ∈ {0 <..< lambda}"
  shows "seq (i + j) ≠ seq i"
proof(cases "mu ≤ i")
  case True
  from assms have A: "(i + j) mod lambda ≠ i mod lambda" for i
    by (auto simp add: mod_eq_dvd_iff_nat)
  from ‹mu ≤ i›
  have "seq (i + j) = seq (mu + (i + j - mu) mod lambda)"
       "seq i = seq (mu + (i - mu) mod lambda)"
    by (auto intro: properties_mod_lambda)
  with P ‹mu ≤ i› assms A[where i="i-mu"] show ?thesis
    by (clarsimp simp: properties_def inj_on_eq_iff)
next
  case False with P assms show ?thesis
    by (clarsimp simp: properties_def inj_on_eq_iff)
qed

lemma properties_distinct_contrapos:
  assumes "seq (i + j) = seq i"
  shows "j ∉ {0 <..< lambda}"
using assms by (rule contrapos_pp) (simp add: properties_distinct)

lemma properties_loops_ge_mu:
  assumes "seq (i + j) = seq i"
  assumes "0 < j"
  shows "mu ≤ i"
proof(rule classical)
  assume X: "¬?thesis" show ?thesis
  proof(cases "mu ≤ i + j")
    case True with P X assms show ?thesis
      by (fastforce simp: properties_def inj_on_eq_iff
                    dest: properties_mod_lambda)
  next
    case False with P assms show ?thesis
      by (fastforce simp add: properties_def inj_on_eq_iff)
  qed
qed

end
(*<*)

end
(*>*)