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 v₁ v₂ = Some(Bool(v₁ = v₂))"
  | "binop And (Bool b₁) (Bool b₂) = Some(Bool(b₁ ∧ b₂))"
  | "binop Less (Intg i₁) (Intg i₂) = Some(Bool(i₁ < i₂))"
  | "binop Add (Intg i₁) (Intg i₂) = Some(Intg(i₁ + i₂))"
  | "binop Sub (Intg i₁) (Intg i₂) = Some(Intg(i₁ - i₂))"

  | "binop bop v₁ v₂ = 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: "[e₁«bop¬e₂] s = (case [e₁] s of None → None
    | Some v₁ → (case [e₂] s of None → None
                           | Some v₂ → binop bop v₁ v₂))"

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:
  "⟨c₁,s⟩ → ⟨c₁',s'⟩ ==> ⟨c₁;;c₂,s⟩ → ⟨c₁';;c₂,s'⟩"

  | RedSeq:
  "⟨Skip;;c₂,s⟩ → ⟨c₂,s⟩"

  | RedCondTrue:
  "[b] s = Some true ==> ⟨if (b) c₁ else c₂,s⟩ → ⟨c₁,s⟩"

  | RedCondFalse:
  "[b] s = Some false ==> ⟨if (b) c₁ else c₂,s⟩ → ⟨c₂,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;;c₂,s⟩ →* ⟨Skip,s'⟩ ==> ⟨c₂,s⟩ →* ⟨Skip,s'⟩"
by(induct c=="Skip;;c₂" s rule:converse_rtranclp_induct2)(auto elim:red.cases)

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


lemma Cond_True_or_False:
  "⟨if (b) c₁ else c₂,s⟩ →* ⟨Skip,s'⟩ ==> [b] s = Some true ∨ [b] s = Some false"
by(induct c=="if (b) c₁ else c₂" s rule:converse_rtranclp_induct2)(auto elim:red.cases)

lemma CondTrue_reds:
  "⟨if (b) c₁ else c₂,s⟩ →* ⟨Skip,s'⟩ ==> [b] s = Some true ==> ⟨c₁,s⟩ →* ⟨Skip,s'⟩"
by(induct c=="if (b) c₁ else c₂" s rule:converse_rtranclp_induct2)(auto elim:red.cases)

lemma CondFalse_reds:
  "⟨if (b) c₁ else c₂,s⟩ →* ⟨Skip,s'⟩ ==> [b] s = Some false ==> ⟨c₂,s⟩ →* ⟨Skip,s'⟩"
by(induct c=="if (b) c₁ else c₂" 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⟩ → ⟨c,s⟩"
     | red_n_Rec: "[⟨c,s⟩ → ⟨c'',s''⟩; ⟨c'',s''⟩ → ⟨c',s'⟩] ==> ⟨c,s⟩ → ⁿ ⟨c',s'⟩"


lemma Seq_red_nE: assumes "⟨c₁;;c₂,s⟩ → ⟨Skip,s'⟩"
  obtains i j s'' where "⟨c₁,s⟩ → ⟨Skip,s''⟩" and "⟨c₂,s''⟩ → ⟨Skip,s'⟩"
  and "n = i + j + 1"
proof -
  from ‹⟨c₁;;c₂,s⟩ → ⟨Skip,s'⟩›
  have "∃i j s''. ⟨c₁,s⟩ → ⟨Skip,s''⟩ ∧ ⟨c₂,s''⟩ → ⟨Skip,s'⟩ ∧ n = i + j + 1"
  proof(induct "c₁;;c₂" s n "Skip" s' arbitrary:c₁ rule:red_n.induct)
    case (red_n_Rec s c'' s'' n s')
    note IH = ‹∧c₁. c'' = c₁;;c₂
 ==> ∃i j sx. ⟨c₁,s''⟩ → ⟨Skip,sx⟩ ∧ ⟨c₂,sx⟩ → ⟨Skip,s'⟩ ∧ n = i + j + 1›
    from ‹⟨c₁;;c₂,s⟩ → ⟨c'',s''⟩›
    have "(c₁ = Skip ∧ c'' = c₂ ∧ s = s'') ∨
      (∃c₁'. c'' = c₁';;c₂ ∧ ⟨c₁,s⟩ → ⟨c₁',s''⟩)"
      by(induct "c₁;;c₂" _ _ _ rule:red_induct) auto
    thus ?case
    proof
      assume "c₁ = Skip ∧ c'' = c₂ ∧ s = s''"
      hence "c₁ = Skip" and "c'' = c₂" and "s = s''" by simp_all
      from ‹c₁ = Skip› have "⟨c₁,s⟩ → ⟨Skip,s⟩" by(fastforce intro:red_n_Base)
      with ‹⟨c'',s''⟩ → ⟨Skip,s'⟩› ‹c'' = c₂› ‹s = s''›
      show ?thesis by(rule_tac x="0" in exI) auto
    next
      assume "∃c₁'. c'' = c₁';;c₂ ∧ ⟨c₁,s⟩ → ⟨c₁',s''⟩"
      then obtain c₁' where "c'' = c₁';;c₂" and "⟨c₁,s⟩ → ⟨c₁',s''⟩" by blast
      from IH[OF ‹c'' = c₁';;c₂›] obtain i j sx
        where "⟨c₁',s''⟩ → ⟨Skip,sx⟩" and "⟨c₂,sx⟩ → ⟨Skip,s'⟩"
        and "n = i + j + 1" by blast
      from ‹⟨c₁,s⟩ → ⟨c₁',s''⟩› ‹⟨c₁',s''⟩ → ⟨Skip,sx⟩›
      have "⟨c₁,s⟩ → ⁱ ⟨Skip,sx⟩" by(rule red_n.red_n_Rec)
      with ‹⟨c₂,sx⟩ → ⟨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⟩ → ⟨Skip,s'⟩
  ==> ([b] s = Some false ∧ s = s' ∧ n = 1) ∨
     (∃i j s''. [b] s = Some true ∧ ⟨cx,s⟩ → ⟨Skip,s''⟩ ∧
                ⟨while (b) cx,s''⟩ → ⟨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''⟩ → ⟨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''⟩ → ⟨Skip,s'⟩›
    obtain i j sx where "⟨cx,s⟩ → ⟨Skip,sx⟩" and "⟨while (b) cx,sx⟩ → ⟨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⟩ → ⟨Skip,s'⟩"
  and IHfalse:"∧s. [b] s = Some false ==> P s s"
  and IHtrue:"∧s i j s''. [ [b] s = Some true; ⟨cx,s⟩ → ⟨Skip,s''⟩;
                            ⟨while (b) cx,s''⟩ → ⟨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⟩ → ⟨Skip,s'⟩ ⟶ P x s'"
    and  "⟨while (b) cx,s⟩ → ⟨Skip,s'⟩"
  from ‹⟨while (b) cx,s⟩ → ⟨Skip,s'⟩›
  have "([b] s = Some false ∧ s = s' ∧ n = 1) ∨
     (∃i j s''. [b] s = Some true ∧ ⟨cx,s⟩ → ⟨Skip,s''⟩ ∧
                ⟨while (b) cx,s''⟩ → ⟨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⟩ → ⟨Skip,s''⟩ ∧
                      ⟨while (b) cx,s''⟩ → ⟨Skip,s'⟩ ∧ n = i + j + 2"
    then obtain i j s'' where "[b] s = Some true"
      and "⟨cx,s⟩ → ⟨Skip,s''⟩" and "⟨while (b) cx,s''⟩ → ⟨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⟩ → ⟨Skip,s''⟩›
      ‹⟨while (b) cx,s''⟩ → ⟨Skip,s'⟩› this] show ?thesis .
  qed
qed


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


lemma red_n_to_reds:"⟨c,s⟩ → ⟨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⟩ → ⟨c₁,s₁⟩; ⟨c,s⟩ → ⟨c₂,s₂⟩] ==> c₁ = c₂ ∧ s₁ = s₂"
proof(induct arbitrary:c₂ rule:red_induct)
  case (SeqRed c₁ s c₁' s' c₂')
  note IH = ‹∧c₂. ⟨c₁,s⟩ → ⟨c₂,s₂⟩ ==> c₁' = c₂ ∧ s' = s₂›
  from ‹⟨c₁;;c₂',s⟩ → ⟨c₂,s₂⟩› have "c₁ = Skip ∨ (∃cx. c₂ = cx;;c₂' ∧ ⟨c₁,s⟩ → ⟨cx,s₂⟩)"
    by(fastforce elim:red.cases)
  thus ?case
  proof
    assume "c₁ = Skip"
    with ‹⟨c₁,s⟩ → ⟨c₁',s'⟩› have False by(fastforce elim:red.cases)
    thus ?thesis by simp
  next
    assume "∃cx. c₂ = cx;;c₂' ∧ ⟨c₁,s⟩ → ⟨cx,s₂⟩"
    then obtain cx where "c₂ = cx;;c₂'" and "⟨c₁,s⟩ → ⟨cx,s₂⟩" by blast
    from IH[OF ‹⟨c₁,s⟩ → ⟨cx,s₂⟩›] have "c₁' = cx ∧ s' = s₂" .
    with ‹c₂ = cx;;c₂'› show ?thesis by simp
  qed
qed (fastforce elim:red.cases)+


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


end