Quelle  Big_StepT.thy

section "Big Step Semantics with Time"
theory Big_StepT imports Big_Step begin

subsection "Big-Step with Time Semantics of Commands"

inductive
  big_step_t :: "com × state ==> nat ==> state ==> bool"  (‹_ ==> _ ⇓ _› 55)
where
Skip: "(SKIP,s) ==> Suc 0 ⇓ s" |
Assign: "(x ::= a,s) ==> Suc 0 ⇓ s(x := aval a s)" |
Seq: "[ (c1,s1) ==> x ⇓ s2; (c2,s2) ==> y ⇓ s3 ; z=x+y ] ==> (c1;;c2, s1) ==> z ⇓ s3" |
IfTrue: "[ bval b s; (c1,s) ==> x ⇓ t; y=x+1 ] ==> (IF b THEN c1 ELSE c2, s) ==> y ⇓ t" |
IfFalse: "[ ¬bval b s; (c2,s) ==> x ⇓ t; y=x+1 ] ==> (IF b THEN c1 ELSE c2, s) ==> y ⇓ t" |
WhileFalse: "[ ¬bval b s ] ==> (WHILE b DO c,s) ==> Suc 0 ⇓ s" |
WhileTrue: "[ bval b s1; (c,s1) ==> x ⇓ s2; (WHILE b DO c, s2) ==> y ⇓ s3; 1+x+y=z ]
    ==> (WHILE b DO c, s1) ==> z ⇓ s3"


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

code_pred big_step_t .

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

values "{(t, x). (SKIP, λ_. 0) ==> x ⇓ t}"

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

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

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

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


text‹Proof automation:›
 
declare big_step_t.intros [intro]
  
lemmas big_step_t_induct = big_step_t.induct[split_format(complete)]

subsection "Rule inversion"

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

inductive_cases Skip_tE[elim!]: "(SKIP,s) ==> x ⇓ t"
thm Skip_tE

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 Assign_tE[elim!]: "(x ::= a,s) ==> p ⇓ t"
thm Assign_tE
inductive_cases Seq_tE[elim!]: "(c1;;c2,s1) ==> p ⇓ s3"
thm Seq_tE
inductive_cases If_tE[elim!]: "(IF b THEN c1 ELSE c2,s) ==> x ⇓ t"
thm If_tE

inductive_cases While_tE[elim]: "(WHILE b DO c,s) ==> x ⇓ t"
thm While_tE
text‹Only [elim]: [elim!] would not terminate.›

text‹An automatic example:›

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

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

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

(* Using rule inversion to prove simplification rules: *)
lemma assign_t_simp:
  "(x ::= a,s) ==> Suc 0 ⇓ s' ⟷ (s' = s(x := aval a s))"
  by (auto)

text ‹An example combining rule inversion and derivations›
lemma Seq_t_assoc:
  "((c1;; c2;; c3, s) ==> p ⇓ s') ⟷ ((c1;; (c2;; c3), s) ==> p ⇓ s')"
proof
  assume "(c1;; c2;; c3, s) ==> p ⇓ s'"
  then obtain s1 s2 p1 p2 p3 where
    c1: "(c1, s) ==> p1 ⇓ s1" and
    c2: "(c2, s1) ==> p2 ⇓ s2" and
    c3: "(c3, s2) ==> p3 ⇓ s'" and
    p: "p = p1 + (p2 + p3)" by auto
  from c2 c3
  have "(c2;; c3, s1) ==> p2 + p3 ⇓ s'" apply (rule Seq) by simp
  with c1
  show "(c1;; (c2;; c3), s) ==> p ⇓ s'" unfolding p apply (rule Seq) by simp
next
  ― ‹The other direction is analogous›
  assume "(c1;; (c2;; c3), s) ==> p ⇓ s'"
  then obtain s1 s2 p1 p2 p3 where
    c1: "(c1, s) ==> p1 ⇓ s1" and
    c2: "(c2, s1) ==> p2 ⇓ s2" and
    c3: "(c3, s2) ==> p3 ⇓ s'" and
    p: "p = (p1 + p2) + p3" by auto
  from c1 c2
  have "(c1;; c2, s) ==> p1 + p2 ⇓ s2" apply (rule Seq) by simp
  from this c3
  show "(c1;; c2;; c3, s) ==> p ⇓ s'" unfolding p apply (rule Seq) by simp
qed


subsection "Relation to Big-Step Semantics"

lemma "(∃p. ((c, s) ==> p ⇓ s')) = ((c, s) ==> s')"
proof 
    assume "∃p. (c, s) ==> p ⇓ s'"
    then obtain p where "(c, s) ==> p ⇓ s'"
by blast
    then show "((c, s) ==> s')"
      apply(induct c s p s' rule: big_step_t_induct)
        prefer 2 apply(rule Big_Step.Assign)
        apply(auto) done
next
  assume "((c, s) ==> s')"
  then show "(∃p. ((c, s) ==> p ⇓ s'))"
    apply(induct c s s' rule: big_step_induct)
      by blast+
qed

 
subsection "Execution is deterministic"

text ‹This proof is automatic.›

theorem big_step_t_determ: "[ (c,s) ==> p ⇓ t; (c,s) ==> q ⇓ u ] ==> u = t"
  apply (induction arbitrary: u q rule: big_step_t.induct)
  apply blast+ done
 

theorem big_step_t_determ2: "[ (c,s) ==> p ⇓ t; (c,s) ==> q ⇓ u ] ==> (u = t ∧ p=q)"
  apply  (induction arbitrary: u q rule: big_step_t_induct) 
    apply(elim Skip_tE) apply(simp)
    apply(elim Assign_tE) apply(simp)
  apply blast
    apply(elim If_tE) apply(simp) apply blast
    apply(elim If_tE)  apply blast apply(simp)
    apply(erule While_tE) apply(simp) apply blast
    proof (goal_cases)
      case 1
      from 1(7) show ?case apply(safe) 
        apply(erule While_tE)
          using 1(1-6) apply fast
          using 1(1-6) apply (simp)
        apply(erule While_tE)
          using 1(1-6) apply fast
          using 1(1-6) by (simp)
     qed
         
       
lemma bigstep_det: "(c1, s) ==> p1 ⇓ t1 ==> (c1, s) ==> p ⇓ t ==> p1=p ∧ t1=t"
  using big_step_t_determ2 by simp


lemma bigstep_progress: "(c, s) ==> p ⇓ t ==> p > 0"
apply(induct rule: big_step_t.induct, auto) done

abbreviation terminates (‹↓›) where "terminates cs ≡ (∃n a. (cs ==> n ⇓ a))"
abbreviation thestate (‹↓_s›) where "thestate cs ≡ (THE a. ∃n. (cs ==> n ⇓ a))" 
abbreviation thetime (‹↓_t›) where "thetime cs ≡ (THE n. ∃a. (cs ==> n ⇓ a))"  
            
  
lemma bigstepT_the_cost: "(c, s) ==> t ⇓ s' ==> ↓_t(c, s) = t"
  using bigstep_det by blast 

lemma bigstepT_the_state: "(c, s) ==> t ⇓ s' ==> ↓_s(c, s) = s'"
  using bigstep_det by blast 


lemma SKIPnot: "(¬ (SKIP, s) ==> p ⇓ t) = (s≠t ∨ p≠Suc 0)" by blast

 
lemma SKIPp: "↓_t(SKIP,s) = Suc 0"
  apply(rule the_equality)
  apply fast
  apply auto done 

lemma SKIPt: "↓_s(SKIP,s) = s"
  apply(rule the_equality)
  apply fast
  apply auto done 


lemma ASSp: "(THE p. Ex (big_step_t (x ::= e, s) p)) = Suc 0"
  apply(rule the_equality)
  apply fast
  apply auto done 

lemma ASSt: "(THE t. ∃p. (x ::= e, s) ==> p ⇓ t) = s(x := aval e s)"
  apply(rule the_equality)
  apply fast
  apply auto done 

lemma ASSnot: "( ¬ (x ::= e, s) ==> p ⇓ t ) = (p≠Suc 0 ∨ t≠s(x := aval e s))"
  apply auto done
       
    
    
lemma If_THE_True: "Suc (THE n. ∃a. (c1, s) ==> n ⇓ a) = (THE n. ∃a. (IF b THEN c1 ELSE c2, s) ==> n ⇓ a)"
     if T: "bval b s" and c1_t: "terminates (c1,s)" for s l
proof -
  from c1_t obtain p t where a: "(c1, s) ==> p ⇓ t" by blast
  with T have b: "(IF b THEN c1 ELSE c2, s) ==> p+1 ⇓ t"  using IfTrue by simp
  from a bigstepT_the_cost have "(THE n. ∃a. (c1, s) ==> n ⇓ a) = p" by simp
moreover    
  from b bigstepT_the_cost have "(THE n. ∃a. (IF b THEN c1 ELSE c2, s) ==> n ⇓ a) = p+1" by simp
ultimately
  show ?thesis by simp
qed

lemma If_THE_False: "Suc (THE n. ∃a. (c2, s) ==> n ⇓ a) = (THE n. ∃a. (IF b THEN c1 ELSE c2, s) ==> n ⇓ a)"
     if T: "¬bval b s" and c2_t: "↓ (c2,s)" for s l
proof -
  from c2_t obtain p t where a: "(c2, s) ==> p ⇓ t"  by blast
  with T have b: "(IF b THEN c1 ELSE c2, s) ==> p+1 ⇓ t"  using IfFalse by simp
  from a bigstepT_the_cost have "(THE n. ∃a. (c2, s) ==> n ⇓ a) = p" by simp
moreover    
  from b bigstepT_the_cost have "(THE n. ∃a. (IF b THEN c1 ELSE c2, s) ==> n ⇓ a) = p+1" by simp
ultimately
  show ?thesis by simp
qed
    
  
end