Theory VeriComp.Semantics

section ‹The Dynamic Representation of a Language›

theory Semantics
  imports Main Behaviour Inf Transfer_Extras begin

text ‹
The definition of programming languages is separated into two parts: an abstract semantics and a concrete program representation.
›

definition finished :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool" where
  "finished r x = (∄y. r x y)"

lemma finished_star:
  assumes "finished r x"
  shows "r⇧^*⇧^* x y ⟹ x = y"
proof (induction y rule: rtranclp_induct)
  case base
  then show ?case by simp
next
  case (step y z)
  then show ?case
    using assms by (auto simp: finished_def)
qed

locale semantics =
  fixes
    step :: "'state ⇒ 'state ⇒ bool" (infix ‹→› 50) and
    final :: "'state ⇒ bool"
  assumes
    final_finished: "final s ⟹ finished step s"
begin

text ‹
The semantics locale represents the semantics as an abstract machine.
It is expressed by a transition system with a transition relation @{term step}---usually written as an infix @{text →} arrow---and final states @{term final}.
›

lemma finished_step:
  "step s s' ⟹ ¬finished step s"
by (auto simp add: finished_def)

abbreviation eval :: "'state ⇒ 'state ⇒ bool" (infix ‹→⇧^*› 50) where
  "eval ≡ step⇧^*⇧^*"

abbreviation inf_step :: "'state ⇒ bool" where
  "inf_step ≡ inf step"

notation
  inf_step (‹'(→⇧^∞')› [] 50) and
  inf_step (‹_ →⇧^∞› [55] 50)

lemma inf_not_finished: "s →⇧^∞ ⟹ ¬ finished step s"
  using inf.cases finished_step by metis

lemma eval_deterministic:
  assumes
    deterministic: "⋀x y z. step x y ⟹ step x z ⟹ y = z" and
    "s1 →⇧^* s2" and "s1 →⇧^* s3" and "finished step s2" and "finished step s3"
  shows "s2 = s3"
proof -
  have "right_unique step"
    using deterministic by (auto intro: right_uniqueI)
  with assms show ?thesis
    by (auto simp: finished_def intro: rtranclp_complete_run_right_unique)
qed

lemma step_converges_or_diverges: "(∃s'. s →⇧^* s' ∧ finished step s') ∨ s →⇧^∞"
  by (smt (verit, del_insts) finished_def inf.coinduct rtranclp.intros(2) rtranclp.rtrancl_refl)

subsection ‹Behaviour of a dynamic execution›

inductive state_behaves :: "'state ⇒ 'state behaviour ⇒ bool" (infix ‹↓› 50) where
  state_terminates:
    "s1 →⇧^* s2 ⟹ finished step s2 ⟹ final s2 ⟹ s1 ↓ (Terminates s2)" |
  state_diverges:
    "s1 →⇧^∞ ⟹ s1 ↓ Diverges" |
  state_goes_wrong:
    "s1 →⇧^* s2 ⟹ finished step s2 ⟹ ¬ final s2 ⟹ s1 ↓ (Goes_wrong s2)"


text ‹
Even though the @{term step} transition relation in the @{locale semantics} locale need not be deterministic, if it happens to be, then the behaviour of a program becomes deterministic too.
›

lemma right_unique_state_behaves:
  assumes
    "right_unique (→)"
  shows "right_unique (↓)"
proof (rule right_uniqueI)
  fix s b1 b2
  assume "s ↓ b1" "s ↓ b2"
  thus "b1 = b2"
    by (auto simp: finished_def simp del: not_ex
        elim!: state_behaves.cases
        dest: rtranclp_complete_run_right_unique[OF ‹right_unique (→)›, of s]
        dest: final_finished star_inf[OF ‹right_unique (→)›, THEN inf_not_finished])
qed

lemma left_total_state_behaves: "left_total (↓)"
proof (rule left_totalI)
  fix s
  show "∃b. s ↓ b"
    using step_converges_or_diverges[of s]
  proof (elim disjE exE conjE)
    fix s'
    assume "s →⇧^* s'" and "finished (→) s'"
    thus "∃b. s ↓ b"
      by (cases "final s'") (auto intro: state_terminates state_goes_wrong)
  next
    assume "s →⇧^∞"
    thus "∃b. s ↓ b"
      by (auto intro: state_diverges)
  qed
qed

subsection ‹Safe states›

definition safe where
  "safe s ⟷ (∀s'. step⇧^*⇧^* s s' ⟶ final s' ∨ (∃s''. step s' s''))"

lemma final_safeI: "final s ⟹ safe s"
  by (metis final_finished finished_star safe_def)

lemma step_safe: "step s s' ⟹ safe s ⟹ safe s'"
  by (simp add: converse_rtranclp_into_rtranclp safe_def)

lemma steps_safe: "step⇧^*⇧^* s s' ⟹ safe s ⟹ safe s'"
  by (meson rtranclp_trans safe_def)

lemma safe_state_behaves_not_wrong:
  assumes "safe s" and "s ↓ b"
  shows "¬ is_wrong b"
  using ‹s ↓ b›
proof (cases rule: state_behaves.cases)
  case (state_goes_wrong s2)
  then show ?thesis
    using ‹safe s› by (auto simp: safe_def finished_def)
qed simp_all

end

end