Quelle  Semantics.thy

section ‹The Dynamic Representation of a Language›

theory Semantics
  imports Main Behaviour Inf Transfer_Extras begin

text ‹
  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 ‹
  semantics locale represents the semantics as an abstract machine.
  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 →^\<infinity> ==> ¬ 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 →^\<infinity>"
  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 →^\<infinity> ==> s1 ↓ Diverges" |
  state_goes_wrong:
    "s1 →^* s2 ==> finished step s2 ==> ¬ final s2 ==> s1 ↓ (Goes_wrong s2)"


text ‹
  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 →^\<infinity>"
    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