Theory Big_Step

theory Big_Step
imports Com
(* Author: Gerwin Klein, Tobias Nipkow *)theory Big_Step imports Com beginsubsection "Big-Step Semantics of Commands"text {*The big-step semantics is a straight-forward inductive definitionwith concrete syntax. Note that the first paramenter is a tuple,so the syntax becomes @{text "(c,s) => s'"}.*}text_raw{*\snip{BigStepdef}{0}{1}{% *}inductive  big_step :: "com × state => state => bool" (infix "=>" 55)whereSkip: "(SKIP,s) => s" |Assign: "(x ::= a,s) => s(x := aval a s)" |Seq: "[| (c⇩1,s⇩1) => s⇩2;  (c⇩2,s⇩2) => s⇩3 |] ==> (c⇩1;;c⇩2, s⇩1) => s⇩3" |IfTrue: "[| bval b s;  (c⇩1,s) => t |] ==> (IF b THEN c⇩1 ELSE c⇩2, s) => t" |IfFalse: "[| ¬bval b s;  (c⇩2,s) => t |] ==> (IF b THEN c⇩1 ELSE c⇩2, s) => t" |WhileFalse: "¬bval b s ==> (WHILE b DO c,s) => s" |WhileTrue:"[| bval b s⇩1;  (c,s⇩1) => s⇩2;  (WHILE b DO c, s⇩2) => s⇩3 |] ==> (WHILE b DO c, s⇩1) => s⇩3"text_raw{*}%endsnip*}text_raw{*\snip{BigStepEx}{1}{2}{% *}schematic_lemma ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) => ?t"apply(rule Seq)apply(rule Assign)apply simpapply(rule Assign)donetext_raw{*}%endsnip*}thm ex[simplified]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 listto 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 automaticallyconstruction small program executions. The recursive casesmay require backtracking, so we declare the set as unsafeintro rules. *}declare big_step.intros [intro]text{* The standard induction rule @{thm [display] big_step.induct [no_vars]} *}thm big_step.inducttext{*This induction schema is almost perfect for our purposes, butour trick for reusing the tuple syntax means that the inductionschema has two parameters instead of the @{text c}, @{text s},and @{text s'} that we are likely to encounter. Splittingthe tuple parameter fixes this:*}lemmas big_step_induct = big_step.induct[split_format(complete)]thm big_step_inducttext {*@{thm [display] big_step_induct [no_vars]}*}subsection "Rule inversion"text{* What can we deduce from @{prop "(SKIP,s) => t"} ?That @{prop "s = t"}. This is how we can automatically prove it: *}inductive_cases SkipE[elim!]: "(SKIP,s) => t"thm SkipEtext{* This is an \emph{elimination rule}. The [elim] attribute tells auto,blast and friends (but not simp!) to use it automatically; [elim!] means thatit is applied eagerly.Similarly for the other commands: *}inductive_cases AssignE[elim!]: "(x ::= a,s) => t"thm AssignEinductive_cases SeqE[elim!]: "(c1;;c2,s1) => s3"thm SeqEinductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) => t"thm IfEinductive_cases WhileE[elim]: "(WHILE b DO c,s) => t"thm WhileEtext{* Only [elim]: [elim!] would not terminate. *}text{* An automatic example: *}lemma "(IF b THEN SKIP ELSE SKIP, s) => t ==> t = s"by blasttext{* 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  qedqed(* Using rule inversion to prove simplification rules: *)lemma assign_simp:  "(x ::= a,s) => s' <-> (s' = s(x := aval a s))"  by autotext {* 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 autoqedsubsection "Command Equivalence"text {*  We call two statements @{text c} and @{text c'} equivalent wrt.\ the  big-step semantics when \emph{@{text c} started in @{text s} terminates  in @{text s'} iff @{text c'} started in the same @{text s} also terminates  in the same @{text s'}}. Formally:*}text_raw{*\snip{BigStepEquiv}{0}{1}{% *}abbreviation  equiv_c :: "com => com => bool" (infix "∼" 50) where  "c ∼ c' ≡ (∀s t. (c,s) => t  =  (c',s) => t)"text_raw{*}%endsnip*}text {*Warning: @{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 blastqedtext {* Luckily, such lengthy proofs are seldom necessary.  Isabelle canprove many such facts automatically.  *}lemma while_unfold:  "(WHILE b DO c) ∼ (IF b THEN c;; WHILE b DO c ELSE SKIP)"by blastlemma triv_if:  "(IF b THEN c ELSE c) ∼ c"by blastlemma 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 blastlemma 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 blastapply blastdonelemma 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 isreflexive, symmetric, and transitive. Because we used an abbreviationabove, Isabelle derives this automatically. *}lemma sim_refl:  "c ∼ c" by simplemma sim_sym:   "(c ∼ c') = (c' ∼ c)" by autolemma sim_trans: "c ∼ c' ==> c' ∼ c'' ==> c ∼ c''" by autosubsection "Execution is deterministic"text {* This proof is automatic. *}text_raw{*\snip{BigStepDeterministic}{0}{1}{% *}theorem big_step_determ: "[| (c,s) => t; (c,s) => u |] ==> u = t"  by (induction arbitrary: u rule: big_step.induct) blast+text_raw{*}%endsnip*}text {*  This is the proof as you might present it in a lecture. The remaining  cases are simple enough to be proved automatically:*}text_raw{*\snip{BigStepDetLong}{0}{2}{% *}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⇩1 t t'  -- "The assumptions of the rule:"  assume "bval b s" and "(c,s) => s⇩1" and "(WHILE b DO c,s⇩1) => t"  -- {* Ind.Hyp; note the @{text"!!"} because of arbitrary: *}  assume IHc: "!!t'. (c,s) => t' ==> t' = s⇩1"  assume IHw: "!!t'. (WHILE b DO c,s⇩1) => t' ==> t' = t"  -- "Premise of implication:"  assume "(WHILE b DO c,s) => t'"  with bval b s obtain s⇩1' where      c: "(c,s) => s⇩1'" and      w: "(WHILE b DO c,s⇩1') => t'"    by auto  from c IHc have "s⇩1' = s⇩1" by blast  with w IHw show "t' = t" by blastqed blast+ -- "prove the rest automatically"text_raw{*}%endsnip*}end