Theory Language

section ‹Language and Semantics›

text ‹In this file, we formalize concepts from section 3:
- Program states and programming language (definition 1)
- Big-step semantics (figure 2)
- Extended states (definition 2)
- Extended semantics (definition 4) and some useful properties (lemma 1)›

theory Language
  imports Main
begin

subsection Language

text ‹Definition 1›

type_synonym ('var, 'val) pstate = "'var ⇒ 'val"

type_synonym ('var, 'val) bexp = "('var, 'val) pstate ⇒ bool"
type_synonym ('var, 'val) exp = "('var, 'val) pstate ⇒ 'val"


datatype ('var, 'val) stmt = 
  Assign 'var "('var, 'val) exp"
  | Seq "('var, 'val) stmt" "('var, 'val) stmt"  (infixl ‹;;› 60)
  | If "('var, 'val) stmt" "('var, 'val) stmt"                    ―‹Non-deterministic choice›
  | Skip
  | Havoc 'var                                                    ―‹Non-deterministic assignment›
  | Assume "('var, 'val) bexp"
  | While "('var, 'val) stmt"                                     ―‹Non-deterministic loop›

subsection Semantics

text ‹Figure 2›

inductive single_sem :: "('var, 'val) stmt ⇒ ('var, 'val) pstate ⇒ ('var, 'val) pstate ⇒ bool"
  (‹⟨_, _⟩ → _› [51,0] 81)
  where
  SemSkip: "⟨Skip, σ⟩ → σ"
| SemAssign: "⟨Assign var e, σ⟩ → σ(var := (e σ))"
| SemSeq: "⟦ ⟨C1, σ⟩ → σ1; ⟨C2, σ1⟩ → σ2 ⟧ ⟹ ⟨Seq C1 C2, σ⟩ → σ2"
| SemIf1: "⟨C1, σ⟩ → σ1 ⟹ ⟨If C1 C2, σ⟩ → σ1"
| SemIf2: "⟨C2, σ⟩ → σ2 ⟹ ⟨If C1 C2, σ⟩ → σ2"
| SemHavoc: "⟨Havoc var, σ⟩ → σ(var := v)"
| SemAssume: "b σ ⟹ ⟨Assume b, σ⟩ → σ"
| SemWhileIter: "⟦ ⟨C, σ⟩ → σ' ; ⟨While C, σ'⟩ → σ'' ⟧ ⟹ ⟨While C, σ⟩ → σ''"
| SemWhileExit: "⟨While C, σ⟩ → σ"

inductive_cases single_sem_Seq_elim[elim!]: "⟨Seq C1 C2, σ⟩ → σ'"
inductive_cases single_sem_Skip_elim[elim!]: "⟨Skip, σ⟩ → σ'"
inductive_cases single_sem_While_elim: "⟨While C, σ⟩ → σ'"
inductive_cases single_sem_If_elim[elim!]: "⟨If C1 C2, σ⟩ → σ'"
inductive_cases single_sem_Assume_elim[elim!]: "⟨Assume b, σ⟩ → σ'"
inductive_cases single_sem_Assign_elim[elim!]: "⟨Assign x e, σ⟩ → σ'"
inductive_cases single_sem_Havoc_elim[elim!]: "⟨Havoc x, σ⟩ → σ'"


subsection ‹Extended States and Extended Semantics›

text ‹Definition 2: Extended states›
type_synonym ('lvar, 'lval, 'pvar, 'pval) state = "('lvar ⇒ 'lval) × ('pvar, 'pval) pstate"

text ‹Definition 4: Extended semantics›
definition sem :: "('pvar, 'pval) stmt ⇒ ('lvar, 'lval, 'pvar, 'pval) state set ⇒ ('lvar, 'lval, 'pvar, 'pval) state set" where
  "sem C S = { (l, σ') |σ' σ l. (l, σ) ∈ S ∧ ⟨C, σ⟩ → σ' }"

lemma in_sem:
  "φ ∈ sem C S ⟷ (∃σ. (fst φ, σ) ∈ S ∧ single_sem C σ (snd φ))" (is "?A ⟷ ?B")
proof
  assume ?A
  then obtain σ' σ l where "φ = (l, σ')" "(l, σ) ∈ S ∧ ⟨C, σ⟩ → σ'"
    using sem_def[of C S] by auto
  then show ?B
    by auto
next
  show "?B ⟹ ?A"
    by (metis (mono_tags, lifting) CollectI prod.collapse sem_def)
qed

text ‹Lemma 1: Useful properties of the extended semantics›

lemma sem_seq:
  "sem (Seq C1 C2) S = sem C2 (sem C1 S)" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof
    fix x2 assume "x2 ∈ ?A"
    then obtain x0 where "(fst x2, x0) ∈ S" "single_sem (Seq C1 C2) x0 (snd x2)"
      by (metis in_sem)
    then obtain x1 where "single_sem C1 x0 x1" "single_sem C2 x1 (snd x2)"
      using single_sem_Seq_elim[of C1 C2 x0 "snd x2"]
      by blast
    then show "x2 ∈ ?B"
      by (metis ‹(fst x2, x0) ∈ S› fst_conv in_sem snd_conv)
  qed
  show "?B ⊆ ?A"
  proof
    fix x2 assume "x2 ∈ ?B"
    then obtain x1 where "(fst x2, x1) ∈ sem C1 S" "single_sem C2 x1 (snd x2)"
      by (metis in_sem)
    then obtain x0 where "(fst x2, x0) ∈ S" "single_sem C1 x0 x1"
      by (metis fst_conv in_sem snd_conv)
    then have "single_sem (Seq C1 C2) x0 (snd x2)"
      by (simp add: SemSeq ‹⟨C2, x1⟩ → snd x2›)
    then show "x2 ∈ ?A"
      by (meson ‹(fst x2, x0) ∈ S› in_sem)
  qed
qed

lemma sem_skip:
  "sem Skip S = S"
  using single_sem_Skip_elim SemSkip in_sem[of _ Skip S]
  by fastforce

lemma sem_union:
  "sem C (S1 ∪ S2) = sem C S1 ∪ sem C S2" (is "?A = ?B")
proof
  show "?A ⊆ ?B" 
  proof
    fix x assume "x ∈ ?A"
    then obtain y where "(fst x, y) ∈ S1 ∪ S2" "single_sem C y (snd x)"
      using in_sem by blast
    then show "x ∈ ?B"
      by (metis Un_iff in_sem)
  qed
  show "?B ⊆ ?A"
  proof
    fix x assume "x ∈ ?B"
    show "x ∈ ?A"
    proof (cases "x ∈ sem C S1")
      case True
      then show ?thesis
        by (metis IntD2 Un_Int_eq(3) in_sem)
    next
      case False
      then show ?thesis
        by (metis Un_iff ‹x ∈ sem C S1 ∪ sem C S2› in_sem)
    qed
  qed
qed

lemma sem_union_general:
  "sem C (⋃x. f x) = (⋃x. sem C (f x))" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof
    fix b assume "b ∈ ?A"
    then obtain a where "a ∈ (⋃x. f x)" "fst a = fst b" "single_sem C (snd a) (snd b)"
      by (metis fst_conv in_sem snd_conv)
    then obtain x where "a ∈ f x" by blast
    then have "b ∈ sem C (f x)"
      by (metis ‹⟨C, snd a⟩ → snd b› ‹fst a = fst b› in_sem surjective_pairing)
    then show "b ∈ ?B"
      by blast
  qed
  show "?B ⊆ ?A"
  proof
    fix y assume "y ∈ ?B"
    then obtain x where "y ∈ sem C (f x)"
      by blast
    then show "y ∈ ?A"
      by (meson UN_I in_sem iso_tuple_UNIV_I)
  qed
qed

lemma sem_monotonic:
  assumes "S ⊆ S'"
  shows "sem C S ⊆ sem C S'"
  by (metis assms sem_union subset_Un_eq)

lemma subsetPairI:
  assumes "⋀l σ. (l, σ) ∈ A ⟹ (l, σ) ∈ B"
  shows "A ⊆ B"
  by (simp add: assms subrelI)


lemma sem_if:
  "sem (If C1 C2) S = sem C1 S ∪ sem C2 S" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof (rule subsetPairI)
    fix l y assume "(l, y) ∈ ?A"
    then obtain x where "(l, x) ∈ S" "single_sem (If C1 C2) x y"
      by (metis fst_conv in_sem snd_conv)
    then show "(l, y) ∈ ?B" using single_sem_If_elim
      UnI1 UnI2 in_sem
      by (metis fst_conv snd_conv)
  qed
  show "?B ⊆ ?A"
    using SemIf1 SemIf2 in_sem
    by (metis (no_types, lifting) Un_subset_iff subsetI)
qed

lemma sem_assume:
  "sem (Assume b) S = { (l, σ) |l σ. (l, σ) ∈ S ∧ b σ }" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof (rule subsetPairI)
    fix l y assume "(l, y) ∈ ?A" then obtain x where "(l, x) ∈ S" "single_sem (Assume b) x y"
      using in_sem
      by (metis fst_conv snd_conv)
    then show "(l, y) ∈ ?B" using single_sem_Assume_elim by blast
  qed
  show "?B ⊆ ?A"
  proof (rule subsetPairI)
    fix l σ assume asm0: "(l, σ) ∈ {(l, σ) |l σ. (l, σ) ∈ S ∧ b σ}"
    then have "(l, σ) ∈ S" "b σ" by simp_all
    then show "(l, σ) ∈ sem (Assume b) S"
      by (metis SemAssume fst_eqD in_sem snd_eqD)
  qed
qed

lemma while_then_reaches:
  assumes "(single_sem C)⇧*⇧* σ σ''"
  shows "single_sem (While C) σ σ''"
  using assms
proof (induct rule: converse_rtranclp_induct)
  case base
  then show ?case
    by (simp add: SemWhileExit)
next
  case (step y z)
  then show ?case
    using SemWhileIter by blast
qed

lemma in_closure_then_while:
  assumes "single_sem C' σ σ''"
  shows "⋀C. C' = While C ⟹ (single_sem C)⇧*⇧* σ σ''"
  using assms
proof (induct rule: single_sem.induct)
  case (SemWhileIter σ C' σ' σ'')
  then show ?case
    by (metis (no_types, lifting) rtranclp.rtrancl_into_rtrancl rtranclp.rtrancl_refl rtranclp_trans stmt.inject(6))
next
  case (SemWhileExit σ C')
  then show ?case
    by blast
qed (auto)

theorem loop_equiv:
  "single_sem (While C) σ σ' ⟷ (single_sem C)⇧*⇧* σ σ'"
  using in_closure_then_while while_then_reaches by blast


fun iterate_sem where
  "iterate_sem 0 _ S = S"
| "iterate_sem (Suc n) C S = sem C (iterate_sem n C S)"

lemma in_iterate_then_in_trans:
  assumes "(l, σ'') ∈ iterate_sem n C S"
  shows "∃σ. (l, σ) ∈ S ∧ (single_sem C)⇧*⇧* σ σ''"
  using assms
proof (induct n arbitrary: σ'' S)
  case 0
  then show ?case
    using iterate_sem.simps(1) by blast
next
  case (Suc n)
  then show ?case
    using in_sem rtranclp.rtrancl_into_rtrancl
    by (metis (mono_tags, lifting) fst_conv iterate_sem.simps(2) snd_conv)
qed

lemma reciprocal:
  assumes "(single_sem C)⇧*⇧* σ σ''"
      and "(l, σ) ∈ S"
    shows "∃n. (l, σ'') ∈ iterate_sem n C S"
  using assms
proof (induct rule: rtranclp_induct)
  case base
  then show ?case
    using iterate_sem.simps(1) by blast
next
  case (step y z)
  then obtain n where "(l, y) ∈ iterate_sem n C S" by blast
  then show ?case
    using in_sem iterate_sem.simps(2) step.hyps(2)
    by (metis fst_eqD snd_eqD)
qed

lemma union_iterate_sem_trans:
  "(l, σ'') ∈ (⋃n. iterate_sem n C S) ⟷ (∃σ. (l, σ) ∈ S ∧ (single_sem C)⇧*⇧* σ σ'')" (is "?A ⟷ ?B")
  using in_iterate_then_in_trans reciprocal by auto

lemma sem_while:
  "sem (While C) S = (⋃n. iterate_sem n C S)" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof (rule subsetPairI)
    fix l y assume "(l, y) ∈ ?A"
    then obtain x where x_def: "(l, x) ∈ S" "(single_sem C)⇧*⇧* x y"
      using in_closure_then_while in_sem
      by (metis fst_eqD snd_conv)
    then have "single_sem (While C) x y"
      using while_then_reaches by blast
    then show "(l, y) ∈ ?B"
      by (metis x_def union_iterate_sem_trans)
  qed
  show "?B ⊆ ?A"
  proof (rule subsetPairI)
    fix l y assume "(l, y) ∈ ?B"
    then obtain x where "(l, x) ∈ S" "(single_sem C)⇧*⇧* x y"
      using union_iterate_sem_trans by blast
    then show "(l, y) ∈ ?A"
      using in_sem while_then_reaches by fastforce
  qed
qed


lemma assume_sem:
  "sem (Assume b) S = Set.filter (b ∘ snd) S" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof (rule subsetPairI)
    fix l σ
    assume asm0: "(l, σ) ∈ sem (Assume b) S"
    then show "(l, σ) ∈ Set.filter (b ∘ snd) S"
      by (metis comp_apply fst_conv in_sem member_filter single_sem_Assume_elim snd_conv)
  qed
  show "?B ⊆ ?A"
    by (metis (mono_tags, opaque_lifting) SemAssume comp_apply in_sem member_filter prod.collapse subsetI)
qed

lemma sem_split_general:
  "sem C (⋃x. F x) = (⋃x. sem C (F x))" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof (rule subsetPairI)
    fix l σ'
    assume asm0: "(l, σ') ∈ sem C (⋃ (range F))"
    then obtain x σ where "(l, σ) ∈ F x" "single_sem C σ σ'"
      by (metis (no_types, lifting) UN_iff fst_conv in_sem snd_conv)
    then show "(l, σ') ∈ (⋃x. sem C (F x))"
      using asm0 sem_union_general by blast
  qed
  show "?B ⊆ ?A"
    by (simp add: SUP_least Sup_upper sem_monotonic)
qed

fun written_vars where
  "written_vars (Assign x _) = {x}"
| "written_vars (Havoc x) = {x}"
| "written_vars (C1;; C2) = written_vars C1 ∪ written_vars C2"
| "written_vars (If C1 C2) = written_vars C1 ∪ written_vars C2"
| "written_vars (While C) = written_vars C"
| "written_vars _ = {}"

lemma written_vars_not_modified:
  assumes "single_sem C φ φ'"
    and "x ∉ written_vars C"
    shows "φ x = φ' x"
  using assms
  by (induct rule: single_sem.induct) auto

end