Theory Semantics

theory Semantics
imports Main
begin

section ‹The Language›

subsection ‹Variables and Values›

type_synonym vname = string ― ‹names for variables›

datatype val
  = Bool bool      ― ‹Boolean value›
  | Intg int       ― ‹integer value› 

abbreviation "true == Bool True"
abbreviation "false == Bool False"



subsection ‹Expressions and Commands›

datatype bop = Eq | And | Less | Add | Sub     ― ‹names of binary operations›

datatype expr
  = Val val                                          ― ‹value›
  | Var vname                                        ― ‹local variable›
  | BinOp expr bop expr    (‹_ «_» _› [80,0,81] 80)  ― ‹binary operation›


text ‹Note: we assume that only type correct expressions are regarded
  as later proofs fail if expressions evaluate to None due to type errors.
  However there is [yet] no typing system›

fun binop :: "bop ⇒ val ⇒ val ⇒ val option"
where "binop Eq v1 v2               = Some(Bool(v1 = v2))"
  | "binop And (Bool b1) (Bool b2)  = Some(Bool(b1 ∧ b2))"
  | "binop Less (Intg i1) (Intg i2) = Some(Bool(i1 < i2))"
  | "binop Add (Intg i1) (Intg i2)  = Some(Intg(i1 + i2))"
  | "binop Sub (Intg i1) (Intg i2)  = Some(Intg(i1 - i2))"

  | "binop bop v1 v2                = Some(Intg(0))"


datatype com
  = Skip
  | LAss vname expr        (‹_:=_› [70,70] 70)  ― ‹local assignment›
  | Seq com com            (‹_;;/ _› [61,60] 60)
  | Cond expr com com      (‹if '(_') _/ else _› [80,79,79] 70)
  | While expr com         (‹while '(_') _› [80,79] 70)


fun fv :: "expr ⇒ vname set" ― ‹free variables in an expression›
where
  FVc: "fv (Val V) = {}"
  | FVv: "fv (Var V) = {V}"
  | FVe: "fv (e1 «bop» e2) = fv e1 ∪ fv e2"


subsection ‹State›

type_synonym state = "vname ⇀ val"


text ‹‹interpret› silently assumes type correct expressions, 
  i.e. no expression evaluates to None›

fun "interpret" :: "expr ⇒ state ⇒ val option" (‹⟦_⟧_›)
where Val: "⟦Val v⟧ s = Some v"
  | Var: "⟦Var V⟧ s = s V"
  | BinOp: "⟦e1«bop»e2⟧ s = (case ⟦e1⟧ s of None ⇒ None
    | Some v1 ⇒ (case ⟦e2⟧ s of None ⇒ None
                           | Some v2 ⇒ binop bop v1 v2))"

subsection ‹Small Step Semantics›

inductive red :: "com * state ⇒ com * state ⇒ bool"
and red' :: "com ⇒ state ⇒ com ⇒ state ⇒ bool"
   (‹((1⟨_,/_⟩) →/ (1⟨_,/_⟩))› [0,0,0,0] 81)
where
  "⟨c1,s1⟩ → ⟨c2,s2⟩ == red (c1,s1) (c2,s2)" |
  RedLAss:
  "⟨V:=e,s⟩ → ⟨Skip,s(V:=(⟦e⟧ s))⟩"

  | SeqRed:
  "⟨c1,s⟩ → ⟨c1',s'⟩ ⟹ ⟨c1;;c2,s⟩ → ⟨c1';;c2,s'⟩"

  | RedSeq:
  "⟨Skip;;c2,s⟩ → ⟨c2,s⟩"

  | RedCondTrue:
  "⟦b⟧ s = Some true ⟹ ⟨if (b) c1 else c2,s⟩ → ⟨c1,s⟩"

  | RedCondFalse:
  "⟦b⟧ s = Some false ⟹ ⟨if (b) c1 else c2,s⟩ → ⟨c2,s⟩"

  | RedWhileTrue:
  "⟦b⟧ s = Some true ⟹ ⟨while (b) c,s⟩ → ⟨c;;while (b) c,s⟩"

  | RedWhileFalse:
  "⟦b⟧ s = Some false ⟹ ⟨while (b) c,s⟩ → ⟨Skip,s⟩"

lemmas red_induct = red.induct[split_format (complete)]

abbreviation reds ::"com ⇒ state ⇒ com ⇒ state ⇒ bool" 
   (‹((1⟨_,/_⟩) →*/ (1⟨_,/_⟩))› [0,0,0,0] 81) where
  "⟨c,s⟩ →* ⟨c',s'⟩ ==  red** (c,s) (c',s')"

lemma Skip_reds:
  "⟨Skip,s⟩ →* ⟨c',s'⟩ ⟹ s = s' ∧ c' = Skip"
by(blast elim:converse_rtranclpE red.cases)

lemma LAss_reds:
  "⟨V:=e,s⟩ →* ⟨Skip,s'⟩ ⟹ s' = s(V:=⟦e⟧ s)"
proof(induct "V:=e" s rule:converse_rtranclp_induct2)
  case (step s c'' s'')
  hence "c'' = Skip" and "s'' = s(V:=(⟦e⟧ s))" by(auto elim:red.cases)
  with ‹⟨c'',s''⟩ →* ⟨Skip,s'⟩› show ?case by(auto dest:Skip_reds)
qed

lemma Seq2_reds:
  "⟨Skip;;c2,s⟩ →* ⟨Skip,s'⟩ ⟹ ⟨c2,s⟩ →* ⟨Skip,s'⟩"
by(induct c=="Skip;;c2" s rule:converse_rtranclp_induct2)(auto elim:red.cases)

lemma Seq_reds:
  assumes "⟨c1;;c2,s⟩ →* ⟨Skip,s'⟩"
  obtains s'' where "⟨c1,s⟩ →* ⟨Skip,s''⟩" and "⟨c2,s''⟩ →* ⟨Skip,s'⟩"
proof -
  have "∃s''. ⟨c1,s⟩ →* ⟨Skip,s''⟩ ∧ ⟨c2,s''⟩ →* ⟨Skip,s'⟩"
  proof -
    { fix c c'
      assume "⟨c,s⟩ →* ⟨c',s'⟩" and "c = c1;;c2" and "c' = Skip"
      hence "∃s''. ⟨c1,s⟩ →* ⟨Skip,s''⟩ ∧ ⟨c2,s''⟩ →* ⟨Skip,s'⟩"
      proof(induct arbitrary:c1 rule:converse_rtranclp_induct2)
        case refl thus ?case by simp
      next
        case (step c s c'' s'')
        note IH = ‹⋀c1. ⟦c'' = c1;;c2; c' = Skip⟧ 
          ⟹ ∃sx. ⟨c1,s''⟩ →* ⟨Skip,sx⟩ ∧ ⟨c2,sx⟩ →* ⟨Skip,s'⟩›
        from step
        have "⟨c1;;c2,s⟩ → ⟨c'',s''⟩" by simp
        hence "(c1 = Skip ∧ c'' = c2 ∧ s = s'') ∨ 
          (∃c1'. ⟨c1,s⟩ → ⟨c1',s''⟩ ∧ c'' = c1';;c2)"
          by(auto elim:red.cases)
        thus ?case
        proof
          assume "c1 = Skip ∧ c'' = c2 ∧ s = s''"
          with ‹⟨c'',s''⟩ →* ⟨c',s'⟩› ‹c' = Skip›
          show ?thesis by auto
        next
          assume "∃c1'. ⟨c1,s⟩ → ⟨c1',s''⟩ ∧ c'' = c1';;c2"
          then obtain c1' where "⟨c1,s⟩ → ⟨c1',s''⟩" and "c'' = c1';;c2" by blast
          from IH[OF ‹c'' = c1';;c2› ‹c' = Skip›]
          obtain sx where "⟨c1',s''⟩ →* ⟨Skip,sx⟩" and "⟨c2,sx⟩ →* ⟨Skip,s'⟩"
            by blast
          from ‹⟨c1,s⟩ → ⟨c1',s''⟩› ‹⟨c1',s''⟩ →* ⟨Skip,sx⟩›
          have "⟨c1,s⟩ →* ⟨Skip,sx⟩" by(auto intro:converse_rtranclp_into_rtranclp)
          with ‹⟨c2,sx⟩ →* ⟨Skip,s'⟩› show ?thesis by auto
        qed
      qed }
    with ‹⟨c1;;c2,s⟩ →* ⟨Skip,s'⟩› show ?thesis by simp
  qed
  with that show ?thesis by blast
qed


lemma Cond_True_or_False:
  "⟨if (b) c1 else c2,s⟩ →* ⟨Skip,s'⟩ ⟹ ⟦b⟧ s = Some true ∨ ⟦b⟧ s = Some false"
by(induct c=="if (b) c1 else c2" s rule:converse_rtranclp_induct2)(auto elim:red.cases)

lemma CondTrue_reds:
  "⟨if (b) c1 else c2,s⟩ →* ⟨Skip,s'⟩ ⟹ ⟦b⟧ s = Some true ⟹ ⟨c1,s⟩ →* ⟨Skip,s'⟩"
by(induct c=="if (b) c1 else c2" s rule:converse_rtranclp_induct2)(auto elim:red.cases)

lemma CondFalse_reds:
  "⟨if (b) c1 else c2,s⟩ →* ⟨Skip,s'⟩ ⟹ ⟦b⟧ s = Some false ⟹ ⟨c2,s⟩ →* ⟨Skip,s'⟩"
by(induct c=="if (b) c1 else c2" s rule:converse_rtranclp_induct2)(auto elim:red.cases)

lemma WhileFalse_reds: 
  "⟨while (b) cx,s⟩ →* ⟨Skip,s'⟩ ⟹ ⟦b⟧ s = Some false ⟹ s = s'"
proof(induct "while (b) cx" s rule:converse_rtranclp_induct2)
  case step thus ?case by(auto elim:red.cases dest: Skip_reds)
qed

lemma WhileTrue_reds: 
  "⟨while (b) cx,s⟩ →* ⟨Skip,s'⟩ ⟹ ⟦b⟧ s = Some true
  ⟹ ∃sx. ⟨cx,s⟩ →* ⟨Skip,sx⟩ ∧ ⟨while (b) cx,sx⟩ →* ⟨Skip,s'⟩"
proof(induct "while (b) cx" s rule:converse_rtranclp_induct2)
  case (step s c'' s'')
  hence "c'' = cx;;while (b) cx ∧ s'' = s" by(auto elim:red.cases)
  with ‹⟨c'',s''⟩ →* ⟨Skip,s'⟩› show ?case by(auto dest:Seq_reds)
qed

lemma While_True_or_False:
  "⟨while (b) com,s⟩ →* ⟨Skip,s'⟩ ⟹ ⟦b⟧ s = Some true ∨ ⟦b⟧ s = Some false"
by(induct c=="while (b) com" s rule:converse_rtranclp_induct2)(auto elim:red.cases)


inductive red_n :: "com ⇒ state ⇒ nat ⇒ com ⇒ state ⇒ bool"
   (‹((1⟨_,/_⟩) →⇗_⇖ (1⟨_,/_⟩))› [0,0,0,0,0] 81)
where red_n_Base: "⟨c,s⟩ →⇗0⇖ ⟨c,s⟩"
     | red_n_Rec: "⟦⟨c,s⟩ → ⟨c'',s''⟩; ⟨c'',s''⟩ →⇗n⇖ ⟨c',s'⟩⟧ ⟹ ⟨c,s⟩ →⇗Suc n⇖ ⟨c',s'⟩"


lemma Seq_red_nE: assumes "⟨c1;;c2,s⟩ →⇗n⇖ ⟨Skip,s'⟩"
  obtains i j s'' where "⟨c1,s⟩ →⇗i⇖ ⟨Skip,s''⟩" and "⟨c2,s''⟩ →⇗j⇖ ⟨Skip,s'⟩"
  and "n = i + j + 1"
proof -
  from ‹⟨c1;;c2,s⟩ →⇗n⇖ ⟨Skip,s'⟩› 
  have "∃i j s''. ⟨c1,s⟩ →⇗i⇖ ⟨Skip,s''⟩ ∧ ⟨c2,s''⟩ →⇗j⇖ ⟨Skip,s'⟩ ∧ n = i + j + 1"
  proof(induct "c1;;c2" s n "Skip" s' arbitrary:c1 rule:red_n.induct)
    case (red_n_Rec s c'' s'' n s')
    note IH = ‹⋀c1. c'' = c1;;c2
      ⟹ ∃i j sx. ⟨c1,s''⟩ →⇗i⇖ ⟨Skip,sx⟩ ∧ ⟨c2,sx⟩ →⇗j⇖ ⟨Skip,s'⟩ ∧ n = i + j + 1›
    from ‹⟨c1;;c2,s⟩ → ⟨c'',s''⟩›
    have "(c1 = Skip ∧ c'' = c2 ∧ s = s'') ∨ 
      (∃c1'. c'' = c1';;c2 ∧ ⟨c1,s⟩ → ⟨c1',s''⟩)"
      by(induct "c1;;c2" _ _ _ rule:red_induct) auto
    thus ?case
    proof
      assume "c1 = Skip ∧ c'' = c2 ∧ s = s''"
      hence "c1 = Skip" and "c'' = c2" and "s = s''" by simp_all
      from ‹c1 = Skip› have "⟨c1,s⟩ →⇗0⇖ ⟨Skip,s⟩" by(fastforce intro:red_n_Base)
      with ‹⟨c'',s''⟩ →⇗n⇖ ⟨Skip,s'⟩› ‹c'' = c2› ‹s = s''›
      show ?thesis by(rule_tac x="0" in exI) auto
    next
      assume "∃c1'. c'' = c1';;c2 ∧ ⟨c1,s⟩ → ⟨c1',s''⟩"
      then obtain c1' where "c'' = c1';;c2" and "⟨c1,s⟩ → ⟨c1',s''⟩" by blast
      from IH[OF ‹c'' = c1';;c2›] obtain i j sx
        where "⟨c1',s''⟩ →⇗i⇖ ⟨Skip,sx⟩" and "⟨c2,sx⟩ →⇗j⇖ ⟨Skip,s'⟩"
        and "n = i + j + 1" by blast
      from ‹⟨c1,s⟩ → ⟨c1',s''⟩› ‹⟨c1',s''⟩ →⇗i⇖ ⟨Skip,sx⟩›
      have "⟨c1,s⟩ →⇗Suc i⇖ ⟨Skip,sx⟩" by(rule red_n.red_n_Rec)
      with ‹⟨c2,sx⟩ →⇗j⇖ ⟨Skip,s'⟩› ‹n = i + j + 1› show ?thesis
        by(rule_tac x="Suc i" in exI) auto
    qed
  qed
  with that show ?thesis by blast
qed


lemma while_red_nE:
  "⟨while (b) cx,s⟩ →⇗n⇖ ⟨Skip,s'⟩ 
  ⟹ (⟦b⟧ s = Some false ∧ s = s' ∧ n = 1) ∨
     (∃i j s''. ⟦b⟧ s = Some true ∧ ⟨cx,s⟩ →⇗i⇖ ⟨Skip,s''⟩ ∧ 
                ⟨while (b) cx,s''⟩ →⇗j⇖ ⟨Skip,s'⟩ ∧ n = i + j + 2)"
proof(induct "while (b) cx" s n "Skip" s' rule:red_n.induct)
  case (red_n_Rec s c'' s'' n s')
  from ‹⟨while (b) cx,s⟩ → ⟨c'',s''⟩›
  have "(⟦b⟧ s = Some false ∧ c'' = Skip ∧ s'' = s) ∨
    (⟦b⟧ s = Some true ∧ c'' = cx;;while (b) cx ∧ s'' = s)"
    by(induct "while (b) cx" _ _ _ rule:red_induct) auto
  thus ?case
  proof
    assume "⟦b⟧ s = Some false ∧ c'' = Skip ∧ s'' = s"
    hence "⟦b⟧ s = Some false" and "c'' = Skip" and "s'' = s" by simp_all
    with ‹⟨c'',s''⟩ →⇗n⇖ ⟨Skip,s'⟩› have "s = s'" and "n = 0"
      by(induct _ _ Skip _ rule:red_n.induct,auto elim:red.cases)
    with ‹⟦b⟧ s = Some false› show ?thesis by fastforce
  next
    assume "⟦b⟧ s = Some true ∧ c'' = cx;;while (b) cx ∧ s'' = s"
    hence "⟦b⟧ s = Some true" and "c'' = cx;;while (b) cx" 
      and "s'' = s" by simp_all
    with ‹⟨c'',s''⟩ →⇗n⇖ ⟨Skip,s'⟩›
    obtain i j sx where "⟨cx,s⟩ →⇗i⇖ ⟨Skip,sx⟩" and "⟨while (b) cx,sx⟩ →⇗j⇖ ⟨Skip,s'⟩"
      and "n = i + j + 1" by(fastforce elim:Seq_red_nE)
    with ‹⟦b⟧ s = Some true› show ?thesis by fastforce
  qed
qed


lemma while_red_n_induct [consumes 1, case_names false true]:
  assumes major: "⟨while (b) cx,s⟩ →⇗n⇖ ⟨Skip,s'⟩"
  and IHfalse:"⋀s.  ⟦b⟧ s = Some false ⟹ P s s"
  and IHtrue:"⋀s i j s''. ⟦  ⟦b⟧ s = Some true; ⟨cx,s⟩ →⇗i⇖ ⟨Skip,s''⟩; 
                            ⟨while (b) cx,s''⟩ →⇗j⇖ ⟨Skip,s'⟩; P s'' s'⟧ ⟹ P s s'"
  shows "P s s'"
using major
proof(induct n arbitrary:s rule:nat_less_induct)
  fix n s
  assume IHall:"∀m<n. ∀x. ⟨while (b) cx,x⟩ →⇗m⇖ ⟨Skip,s'⟩ ⟶ P x s'"
    and  "⟨while (b) cx,s⟩ →⇗n⇖ ⟨Skip,s'⟩"
  from ‹⟨while (b) cx,s⟩ →⇗n⇖ ⟨Skip,s'⟩›
  have "(⟦b⟧ s = Some false ∧ s = s' ∧ n = 1) ∨
     (∃i j s''. ⟦b⟧ s = Some true ∧ ⟨cx,s⟩ →⇗i⇖ ⟨Skip,s''⟩ ∧ 
                ⟨while (b) cx,s''⟩ →⇗j⇖ ⟨Skip,s'⟩ ∧ n = i + j + 2)" 
    by(rule while_red_nE)
  thus "P s s'"
  proof
    assume "⟦b⟧ s = Some false ∧ s = s' ∧ n = 1"
    hence "⟦b⟧ s = Some false" and "s = s'" by auto
    from IHfalse[OF ‹⟦b⟧ s = Some false›] have "P s s" .
    with ‹s = s'› show ?thesis by simp
  next
    assume "∃i j s''. ⟦b⟧ s = Some true ∧ ⟨cx,s⟩ →⇗i⇖ ⟨Skip,s''⟩ ∧ 
                      ⟨while (b) cx,s''⟩ →⇗j⇖ ⟨Skip,s'⟩ ∧ n = i + j + 2"
    then obtain i j s'' where "⟦b⟧ s = Some true"
      and "⟨cx,s⟩ →⇗i⇖ ⟨Skip,s''⟩" and "⟨while (b) cx,s''⟩ →⇗j⇖ ⟨Skip,s'⟩"
      and "n = i + j + 2" by blast
    with IHall have "P s'' s'"
      apply(erule_tac x="j" in allE) apply clarsimp done
    from IHtrue[OF ‹⟦b⟧ s = Some true› ‹⟨cx,s⟩ →⇗i⇖ ⟨Skip,s''⟩› 
      ‹⟨while (b) cx,s''⟩ →⇗j⇖ ⟨Skip,s'⟩› this] show ?thesis .
  qed
qed


lemma reds_to_red_n:"⟨c,s⟩ →* ⟨c',s'⟩ ⟹ ∃n. ⟨c,s⟩ →⇗n⇖ ⟨c',s'⟩"
by(induct rule:converse_rtranclp_induct2,auto intro:red_n.intros)


lemma red_n_to_reds:"⟨c,s⟩ →⇗n⇖ ⟨c',s'⟩ ⟹ ⟨c,s⟩ →* ⟨c',s'⟩"
by(induct rule:red_n.induct,auto intro:converse_rtranclp_into_rtranclp)


lemma while_reds_induct[consumes 1, case_names false true]:
  "⟦⟨while (b) cx,s⟩ →* ⟨Skip,s'⟩; ⋀s. ⟦b⟧ s = Some false ⟹ P s s;
    ⋀s s''. ⟦ ⟦b⟧ s = Some true; ⟨cx,s⟩ →* ⟨Skip,s''⟩; 
             ⟨while (b) cx,s''⟩ →* ⟨Skip,s'⟩; P s'' s'⟧ ⟹ P s s'⟧
  ⟹ P s s'"
apply(drule reds_to_red_n,clarsimp)
apply(erule while_red_n_induct,clarsimp)
by(auto dest:red_n_to_reds)


lemma red_det:
  "⟦⟨c,s⟩ → ⟨c1,s1⟩; ⟨c,s⟩ → ⟨c2,s2⟩⟧ ⟹ c1 = c2 ∧ s1 = s2"
proof(induct arbitrary:c2 rule:red_induct)
  case (SeqRed c1 s c1' s' c2')
  note IH = ‹⋀c2. ⟨c1,s⟩ → ⟨c2,s2⟩ ⟹ c1' = c2 ∧ s' = s2›
  from ‹⟨c1;;c2',s⟩ → ⟨c2,s2⟩› have "c1 = Skip ∨ (∃cx. c2 = cx;;c2' ∧ ⟨c1,s⟩ → ⟨cx,s2⟩)"
    by(fastforce elim:red.cases)
  thus ?case
  proof
    assume "c1 = Skip"
    with ‹⟨c1,s⟩ → ⟨c1',s'⟩› have False by(fastforce elim:red.cases)
    thus ?thesis by simp
  next
    assume "∃cx. c2 = cx;;c2' ∧ ⟨c1,s⟩ → ⟨cx,s2⟩"
    then obtain cx where "c2 = cx;;c2'" and "⟨c1,s⟩ → ⟨cx,s2⟩" by blast
    from IH[OF ‹⟨c1,s⟩ → ⟨cx,s2⟩›] have "c1' = cx ∧ s' = s2" .
    with ‹c2 = cx;;c2'› show ?thesis by simp
  qed
qed (fastforce elim:red.cases)+


theorem reds_det:
  "⟦⟨c,s⟩ →* ⟨Skip,s1⟩; ⟨c,s⟩ →* ⟨Skip,s2⟩⟧ ⟹ s1 = s2"
proof(induct rule:converse_rtranclp_induct2)
  case refl
  from ‹⟨Skip,s1⟩ →* ⟨Skip,s2⟩› show ?case
    by -(erule converse_rtranclpE,auto elim:red.cases)
next
  case (step c'' s'' c' s')
  note IH = ‹⟨c',s'⟩ →* ⟨Skip,s2⟩ ⟹ s1 = s2›
  from step have "⟨c'',s''⟩ → ⟨c',s'⟩"
    by simp
  from ‹⟨c'',s''⟩ →* ⟨Skip,s2⟩› this have "⟨c',s'⟩ →* ⟨Skip,s2⟩"
    by -(erule converse_rtranclpE,auto elim:red.cases dest:red_det)
  from IH[OF this] show ?thesis .
qed


end