Quelle  Basis.thy

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

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

text‹

  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
  "\<not>a ≡ λs. ¬a s"

abbreviation (input)
  pred_conj :: "('a ==> bool) ==> ('a ==> bool) ==> 'a ==> bool" (infixr ‹\∧› 35) where
  "a \<and> b ≡ λs. a s ∧ b s"

abbreviation (input)
  pred_implies :: "('a ==> bool) ==> ('a ==> bool) ==> 'a ==> bool" (infixr ‹\⟶› 25) where
  "a \<longrightarrow> 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 \<in> b ≡ λs. a s ∈ b s"

abbreviation (input)
  pred_neq :: "('a ==> 'b) ==> ('a ==> 'b) ==> 'a ==> bool" (infix ‹\≠› 40) where
  "a \<noteq> 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 \<le> 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 \<bowtie> g ≡ λx. (f x, g x)"

abbreviation (input)
  pred_all :: "('b ==> 'a ==> bool) ==> 'a ==> bool" (binder ‹\∀› 10) where
  "\<forall>x. P x ≡ λs. ∀x. P x s"

abbreviation (input)
  pred_ex :: "('b ==> 'a ==> bool) ==> 'a ==> bool" (binder ‹\∃› 10) where
  "\<exists>x. P x ≡ λs. ∃x. P x s"

section‹ ``Monoidal'' Hoare logic ›

text‹

  the absence of a general-purpose development of Hoare Logic for
  correctness in Isabelle/HOL\footnote{At the time of writing the
  contains several for partial correctness, and one for
  correctness over a language with restricted expressions. SIMPL
 cite‹"DBLP:journals/afp/Schirmer08"›) is overkill for our present
 .}, we adopt the following syntactic contrivance that eases
  multiple assertions about function results. ``Programs''
  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‹

  that the @{thm[source] assignI} rule applies to all state
 , 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‹

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

  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‹

  parameters ‹lambda› and ‹mu› must exist by the
  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‹

  ease further reasoning, we define a new locale that fixes @{term
 lambda"} and @{term "mu"}, and assume these properties hold. We then
  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
(*>*)