Theory CIMP_vcg_rules

(*<*)
(*
 * Copyright 2015, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory CIMP_vcg_rules
imports
  CIMP_vcg
begin

(*>*)
subsubsection‹ VCG rules \label{sec:cimp:vcg_rules} ›

text‹

We can develop some (but not all) of the familiar Hoare rules; see
\<^citet>‹"DBLP:journals/acta/Lamport80"› and the
seL4/l4.verified lemma buckets for inspiration. We avoid many of the
issues Lamport mentions as we only treat basic (atomic) commands.

›

context
  fixes coms :: "('answer, 'location, 'proc, 'question, 'state) programs"
  fixes p :: "'proc"
  fixes aft :: "('answer, 'location, 'question, 'state) loc_comp"
begin

abbreviation
  valid_syn :: "('answer, 'location, 'proc, 'question, 'state) state_pred
             ⇒ ('answer, 'location, 'question, 'state) com
             ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred ⇒ bool" where
  "valid_syn P c Q ≡ coms, p, aft ⊢ ⦃P⦄ c ⦃Q⦄"
notation valid_syn (‹⦃_⦄/ _/ ⦃_⦄›)

abbreviation
  valid_inv_syn :: "('answer, 'location, 'proc, 'question, 'state) state_pred
                  ⇒ ('answer, 'location, 'question, 'state) com ⇒ bool" where
  "valid_inv_syn P c ≡ ⦃P⦄ c ⦃P⦄"
notation valid_inv_syn (‹⦃_⦄/ _›)

lemma vcg_True:
  "⦃P⦄ c ⦃⟨True⟩⦄"
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_conj:
  "⟦ ⦃I⦄ c ⦃Q⦄; ⦃I⦄ c ⦃R⦄ ⟧ ⟹ ⦃I⦄ c ⦃Q ❙∧ R⦄"
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_pre_imp:
  "⟦ ⋀s. P s ⟹ Q s; ⦃Q⦄ c ⦃R⦄ ⟧ ⟹ ⦃P⦄ c ⦃R⦄"
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemmas vcg_pre = vcg_pre_imp[rotated]

lemma vcg_post_imp:
  "⟦ ⋀s. Q s ⟹ R s; ⦃P⦄ c ⦃Q⦄ ⟧ ⟹ ⦃P⦄ c ⦃R⦄"
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_prop[intro]:
  "⦃⟨P⟩⦄ c"
by (cases c) (fastforce intro: vcg.intros)+

lemma vcg_drop_imp:
  assumes "⦃P⦄ c ⦃Q⦄"
  shows "⦃P⦄ c ⦃R ❙⟶ Q⦄"
using assms
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_conj_lift:
  assumes x: "⦃P⦄ c ⦃Q⦄"
  assumes y: "⦃P'⦄ c ⦃Q'⦄"
  shows      "⦃P ❙∧ P'⦄ c ⦃Q ❙∧ Q'⦄"
apply (rule vcg_conj)
 apply (rule vcg_pre[OF x], simp)
apply (rule vcg_pre[OF y], simp)
done

lemma vcg_disj_lift:
  assumes x: "⦃P⦄  c ⦃Q⦄"
  assumes y: "⦃P'⦄ c ⦃Q'⦄"
  shows      "⦃P ❙∨ P'⦄ c ⦃Q ❙∨ Q'⦄"
using assms
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_imp_lift:
  assumes "⦃P'⦄ c ⦃❙¬ P⦄"
  assumes "⦃Q'⦄ c ⦃Q⦄"
  shows "⦃P' ❙∨ Q'⦄ c ⦃P ❙⟶ Q⦄"
by (simp only: imp_conv_disj vcg_disj_lift[OF assms])

lemma vcg_ex_lift:
  assumes "⋀x. ⦃P x⦄ c ⦃Q x⦄"
  shows "⦃λs. ∃x. P x s⦄ c ⦃λs. ∃x. Q x s⦄"
using assms
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_all_lift:
  assumes "⋀x. ⦃P x⦄ c ⦃Q x⦄"
  shows "⦃λs. ∀x. P x s⦄ c ⦃λs. ∀x. Q x s⦄"
using assms
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_name_pre_state:
  assumes "⋀s. P s ⟹ ⦃(=) s⦄ c ⦃Q⦄"
  shows "⦃P⦄ c ⦃Q⦄"
using assms
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_lift_comp:
  assumes f: "⋀P. ⦃λs. P (f s :: 'a :: type)⦄ c"
  assumes P: "⋀x. ⦃Q x⦄ c ⦃P x⦄"
  shows "⦃λs. Q (f s) s⦄ c ⦃λs. P (f s) s⦄"
apply (rule vcg_name_pre_state)
apply (rename_tac s)
apply (rule vcg_pre)
 apply (rule vcg_post_imp[rotated])
  apply (rule vcg_conj_lift)
   apply (rule_tac x="f s" in P)
  apply (rule_tac P="λfs. fs = f s" in f)
 apply simp
apply simp
done


subsubsection‹Cheap non-interference rules›

text‹

These rules magically construct VCG lifting rules from the easier to
prove ‹eq_imp› facts. We don't actually use these in the GC,
but we do derive @{const "fun_upd"} equations using the same
mechanism. Thanks to Thomas Sewell for the requisite syntax magic.

As these ‹eq_imp› facts do not usefully compose, we make the
definition asymmetric (i.e., ‹g› does not get a bundle of
parameters).

Note that these are effectively parametricity rules.

›

definition eq_imp :: "('a ⇒ 'b ⇒ 'c) ⇒ ('b ⇒ 'e) ⇒ bool" where
  "eq_imp f g ≡ (∀s s'. (∀x. f x s = f x s') ⟶ (g s = g s'))"

lemma eq_impD:
  "⟦ eq_imp f g; ∀x. f x s = f x s' ⟧ ⟹ g s = g s'"
by (simp add: eq_imp_def)

lemma eq_imp_vcg:
  assumes g: "eq_imp f g"
  assumes f: "∀x P. ⦃P ∘ (f x)⦄ c"
  shows "⦃P ∘ g⦄ c"
apply (rule vcg_name_pre_state)
apply (rename_tac s)
apply (rule vcg_pre)
 apply (rule vcg_post_imp[rotated])
  apply (rule vcg_all_lift[where 'a='a])
  apply (rule_tac x=x and P="λfs. fs = f x s" in f[rule_format])
 apply simp
 apply (frule eq_impD[where f=f, OF g])
 apply simp
apply simp
done

lemma eq_imp_vcg_LST:
  assumes g: "eq_imp f g"
  assumes f: "∀x P. ⦃P ∘ (f x) ∘ LST⦄ c"
  shows "⦃P ∘ g ∘ LST⦄ c"
apply (rule vcg_name_pre_state)
apply (rename_tac s)
apply (rule vcg_pre)
 apply (rule vcg_post_imp[rotated])
  apply (rule vcg_all_lift[where 'a='a])
  apply (rule_tac x=x and P="λfs. fs = f x s↓" in f[rule_format])
 apply simp
 apply (frule eq_impD[where f=f, OF g])
 apply simp
apply simp
done

lemma eq_imp_fun_upd:
  assumes g: "eq_imp f g"
  assumes f: "∀x. f x (s(fld := val)) = f x s"
  shows "g (s(fld := val)) = g s"
apply (rule eq_impD[OF g])
apply (rule f)
done

lemma curry_forall_eq:
  "(∀f. P f) = (∀f. P (case_prod f))"
by (metis case_prod_curry)

lemma pres_tuple_vcg:
  "(∀P. ⦃P ∘ (λs. (f s, g s))⦄ c)
    ⟷ ((∀P. ⦃P ∘ f⦄ c) ∧ (∀P. ⦃P ∘ g⦄ c))"
apply (simp add: curry_forall_eq o_def)
apply safe
  apply fast
 apply fast
apply (rename_tac P)
apply (rule_tac f="f" and P="λfs s. P fs (g s)" in vcg_lift_comp; simp)
done

lemma pres_tuple_vcg_LST:
  "(∀P. ⦃P ∘ (λs. (f s, g s)) ∘ LST⦄ c)
    ⟷ ((∀P. ⦃P ∘ f ∘ LST⦄ c) ∧ (∀P. ⦃P ∘ g ∘ LST⦄ c))"
apply (simp add: curry_forall_eq o_def)
apply safe
  apply fast
 apply fast
apply (rename_tac P)
apply (rule_tac f="λs. f s↓" and P="λfs s. P fs (g s)" for g in vcg_lift_comp; simp)
done

no_notation valid_syn (‹⦃_⦄/ _/ ⦃_⦄›)

end

(*<*)

end
(*>*)