(* Author: Gerwin Klein, Tobias Nipkow *)

theory Big_Step imports Com begin

subsection "Big-Step Semantics of Commands"

text ‹
  big-step semantics is a straight-forward inductive definition
  concrete syntax. Note that the first parameter is a tuple,
  the syntax becomes ‹(c,s) → s'›.
 ›

inductive
  big_step :: "com × state → state → bool" (infix ‹→› 55)
where
Skip: "(SKIP,s) → s" |
Assign: "(x ::= a,s) → s(x := aval a s)" |
Seq: "[ (c₁,s₁) → s₂; (c₂,s₂) → s₃ ] ==> (c₁;;c₂, s₁) → s₃" |
IfTrue: "[ bval b s; (c₁,s) → t ] ==> (IF b THEN c₁ ELSE c₂, s) → t" |
IfFalse: "[ ¬bval b s; (c₂,s) → t ] ==> (IF b THEN c₁ ELSE c₂, s) → t" |
WhileFalse: "¬bval b s ==> (WHILE b DO c,s) → s" |
WhileTrue:
"[ bval b s₁; (c,s₁) → s₂; (WHILE b DO c, s₂) → s₃ ]
\<Longrightarrow> (WHILE b DO c, s₁) → s₃"

text‹We want to execute the big-step rules:›

code_pred big_step .

text‹For inductive definitions we need command
 \texttt{values} instead of \texttt{value}.›

values "{t. (SKIP, λ_. 0) → t}"

text‹We need to translate the result state into a list
  display it.›

values "{map t [''x''] |t. (SKIP, <''x'' := 42>) → t}"

values "{map t [''x''] |t. (''x'' ::= N 2, <''x'' := 42>) → t}"

values "{map t [''x'',''y''] |t.
  (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
   <''x'' := 0, ''y'' := 13>) → t}"


text‹Proof automation:›

text ‹The introduction rules are good for automatically
  small program executions. The recursive cases
  require backtracking, so we declare the set as unsafe
  rules.›
declare big_step.intros [intro]

text‹The standard induction rule
 {thm [display] big_step.induct [no_vars]}›

thm big_step.induct

text‹
  induction schema is almost perfect for our purposes, but
  trick for reusing the tuple syntax means that the induction
  has two parameters instead of the ‹c›, ‹s›,
  ‹s'› that we are likely to encounter. Splitting
  tuple parameter fixes this:
 ›
lemmas big_step_induct = big_step.induct[split_format(complete)]
thm big_step_induct
text ‹
 {thm [display] big_step_induct [no_vars]}
 ›


subsection "Rule inversion"

text‹What can we deduce from @{prop "(SKIP,s) → t"} ?
  @{prop "s = t"}. This is how we can automatically prove it:›

inductive_cases SkipE[elim!]: "(SKIP,s) → t"
thm SkipE

text‹This is an \emph{elimination rule}. The [elim] attribute tells auto,
  and friends (but not simp!) to use it automatically; [elim!] means that
  is applied eagerly.

  for the other commands:›

inductive_cases AssignE[elim!]: "(x ::= a,s) → t"
thm AssignE
inductive_cases SeqE[elim!]: "(c1;;c2,s1) → s3"
thm SeqE
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) → t"
thm IfE

inductive_cases WhileE[elim]: "(WHILE b DO c,s) → t"
thm WhileE
text‹Only [elim]: [elim!] would not terminate.›

text‹An automatic example:›

lemma "(IF b THEN SKIP ELSE SKIP, s) → t ==> t = s"
by blast

text‹Rule inversion by hand via the ``cases'' method:›

lemma assumes "(IF b THEN SKIP ELSE SKIP, s) → t"
shows "t = s"
proof-
  from assms show ?thesis
  proof cases  ― ‹inverting assms›
    case IfTrue thm IfTrue
    thus ?thesis by blast
  next
    case IfFalse thus ?thesis by blast
  qed
qed

(* Using rule inversion to prove simplification rules: *)
lemma assign_simp:
  "(x ::= a,s) → s' ⟷ (s' = s(x := aval a s))"
  by auto

text ‹An example combining rule inversion and derivations›
lemma Seq_assoc:
  "(c1;; c2;; c3, s) → s' ⟷ (c1;; (c2;; c3), s) → s'"
proof
  assume "(c1;; c2;; c3, s) → s'"
  then obtain s1 s2 where
    c1: "(c1, s) → s1" and
    c2: "(c2, s1) → s2" and
    c3: "(c3, s2) → s'" by auto
  from c2 c3
  have "(c2;; c3, s1) → s'" by (rule Seq)
  with c1
  show "(c1;; (c2;; c3), s) → s'" by (rule Seq)
next
  ― ‹The other direction is analogous›
  assume "(c1;; (c2;; c3), s) → s'"
  thus "(c1;; c2;; c3, s) → s'" by auto
qed


subsection "Command Equivalence"

text ‹
 We call two statements ‹c› and ‹c'› equivalent wrt.\ the
 big-step semantics when \emph{‹c› started in ‹s› terminates
 in ‹s'› iff ‹c'› started in the same ‹s› also terminates
 in the same ‹s'›}. Formally:
 ›
abbreviation
  equiv_c :: "com → com → bool" (infix ‹∼› 50) where
  "c ∼ c' ≡ (∀s t. (c,s) → t = (c',s) → t)"


text ‹
 : ‹∼› is the symbol written \verb!\ < s i m >! (without spaces).

 As an example, we show that loop unfolding is an equivalence
 transformation on programs:
 ›
lemma unfold_while:
  "(WHILE b DO c) ∼ (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w ∼ ?iw")
proof -
  ― ‹to show the equivalence, we look at the derivation tree for›
  ― ‹each side and from that construct a derivation tree for the other side›
  { fix s t assume "(?w, s) → t"
    ― ‹as a first thing we note that, if @{text b} is @{text False} in state @{text s},›
    ― ‹then both statements do nothing:›
    { assume "¬bval b s"
      hence "t = s" using ‹(?w,s) → t› by blast
      hence "(?iw, s) → t" using ‹¬bval b s› by blast
    }
    moreover
    ― ‹on the other hand, if @{text b} is @{text True} in state @{text s},›
    ― ‹then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) → t"}›
    { assume "bval b s"
      with ‹(?w, s) → t› obtain s' where
        "(c, s) → s'" and "(?w, s') → t" by auto
      ― ‹now we can build a derivation tree for the @{text IF}›
      ― ‹first, the body of the True-branch:›
      hence "(c;; ?w, s) → t" by (rule Seq)
      ― ‹then the whole @{text IF}›
      with ‹bval b s› have "(?iw, s) → t" by (rule IfTrue)
    }
    ultimately
    ― ‹both cases together give us what we want:›
    have "(?iw, s) → t" by blast
  }
  moreover
  ― ‹now the other direction:›
  { fix s t assume "(?iw, s) → t"
    ― ‹again, if @{text b} is @{text False} in state @{text s}, then the False-branch›
    ― ‹of the @{text IF} is executed, and both statements do nothing:›
    { assume "¬bval b s"
      hence "s = t" using ‹(?iw, s) → t› by blast
      hence "(?w, s) → t" using ‹¬bval b s› by blast
    }
    moreover
    ― ‹on the other hand, if @{text b} is @{text True} in state @{text s},›
    ― ‹then this time only the @{text IfTrue} rule can have be used›
    { assume "bval b s"
      with ‹(?iw, s) → t› have "(c;; ?w, s) → t" by auto
      ― ‹and for this, only the Seq-rule is applicable:›
      then obtain s' where
        "(c, s) → s'" and "(?w, s') → t" by auto
      ― ‹with this information, we can build a derivation tree for the @{text WHILE}›
      with ‹bval b s›
      have "(?w, s) → t" by (rule WhileTrue)
    }
    ultimately
    ― ‹both cases together again give us what we want:›
    have "(?w, s) → t" by blast
  }
  ultimately
  show ?thesis by blast
qed

text ‹Luckily, such lengthy proofs are seldom necessary. Isabelle can
  many such facts automatically.›

lemma while_unfold:
  "(WHILE b DO c) ∼ (IF b THEN c;; WHILE b DO c ELSE SKIP)"
by blast

lemma triv_if:
  "(IF b THEN c ELSE c) ∼ c"
by blast

lemma commute_if:
  "(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2)
   ∼
   (IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
by blast

lemma sim_while_cong_aux:
  "(WHILE b DO c,s) → t ==> c ∼ c' ==> (WHILE b DO c',s) → t"
apply(induction "WHILE b DO c" s t arbitrary: b c rule: big_step_induct)
 apply blast
apply blast
done

lemma sim_while_cong: "c ∼ c' ==> WHILE b DO c ∼ WHILE b DO c'"
by (metis sim_while_cong_aux)

text ‹Command equivalence is an equivalence relation, i.e.\ it is
 , symmetric, and transitive. Because we used an abbreviation
 , Isabelle derives this automatically.›

lemma sim_refl:  "c ∼ c" by simp
lemma sim_sym:   "(c ∼ c') = (c' ∼ c)" by auto
lemma sim_trans: "c ∼ c' ==> c' ∼ c'' ==> c ∼ c''" by auto

subsection "Execution is deterministic"

text ‹This proof is automatic.›

theorem big_step_determ: "[ (c,s) → t; (c,s) → u ] ==> u = t"
  by (induction arbitrary: u rule: big_step.induct) blast+

text ‹
 This is the proof as you might present it in a lecture. The remaining
 cases are simple enough to be proved automatically:
 ›

theorem
  "(c,s) → t ==> (c,s) → t' ==> t' = t"
proof (induction arbitrary: t' rule: big_step.induct)
  ― ‹the only interesting case, @{text WhileTrue}:›
  fix b c s s₁ t t'
  ― ‹The assumptions of the rule:›
  assume "bval b s" and "(c,s) → s₁" and "(WHILE b DO c,s₁) → t"
  ― ‹Ind.Hyp; note the @{text"∧"} because of arbitrary:›
  assume IHc: "∧t'. (c,s) → t' ==> t' = s₁"
  assume IHw: "∧t'. (WHILE b DO c,s₁) → t' ==> t' = t"
  ― ‹Premise of implication:›
  assume "(WHILE b DO c,s) → t'"
  with ‹bval b s› obtain s₁' where
      c: "(c,s) → s₁'" and
      w: "(WHILE b DO c,s₁') → t'"
    by auto
  from c IHc have "s₁' = s₁" by blast
  with w IHw show "t' = t" by blast
qed blast+ ― ‹prove the rest automatically›

end