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