Theory Big_StepT

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
to 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"} ?
That @{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,
blast and friends (but not simp!) to use it automatically; [elim!] means that
it is applied eagerly.

Similarly 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