Theory IMP2_from_IMP

section ‹Introduction to IMP2-VCG, based on IMP›
theory IMP2_from_IMP
imports "../IMP2"
begin

  text ‹This document briefly introduces the extensions of IMP2 over IMP.›

  subsection ‹Fancy Syntax›
  
  text ‹Standard Syntax›
  definition "exp_count_up1 ≡ 
    ''a'' ::= N 1;;
    ''c'' ::= N 0;;
    WHILE Cmpop (<) (V ''c'') (V ''n'') DO (
      ''a'' ::= Binop (*) (N 2) (V ''a'');; 
      ''c'' ::= Binop (+) (V ''c'') (N 1))"

  (* Type \ < ^ imp > \open \close , without the spaces.
  
    for ‹…›, there is an autocompletion if you type a quote (")
    
    for ― ‹›, type \comment and use autocompletion
    
  *)
  text ‹Fancy Syntax›
  definition "exp_count_up2 ≡ imp‹
    ― ‹Initialization›
    a = 1;
    c = 0;
    while (c<n) { ― ‹Iterate until ‹c› has reached ‹n››
      a=2*a; ― ‹Double ‹a››
      c=c+1  ― ‹Increment ‹c››
    }
  ›"    
      
  lemma "exp_count_up1 = exp_count_up2"
    unfolding exp_count_up1_def exp_count_up2_def ..
  
  

  subsection ‹Operators and Arrays›

  text ‹We reflect arbitrary Isabelle functions into the syntax: ›
  value "bval (Cmpop (≤) (Binop (+) (Unop uminus (V ''x'')) (N 42)) (N 50)) <''x'':=(λ_. -5)> "
    
  thm aval.simps bval.simps

  text ‹Every variable is an array, indexed by integers, no bounds.
    Syntax shortcuts to access index 0.
  ›  

  term ‹Vidx ''a'' (i::aexp)› ― ‹Array access at index ‹i››
  lemma "V ''x'' = Vidx ''x'' (N 0)" .. ― ‹Shortcut for access at index ‹0››
  
  text ‹New commands:›
  term ‹AssignIdx ''a'' (i::aexp) (v::aexp)› ― ‹Assign at index. Replaces assign.›
  term ‹''a''[i] ::= v›  ― ‹Standard syntax›
  term ‹imp‹ a[i] = v ›› ― ‹Fancy syntax›
  
  lemma ‹Assign ''x'' v = AssignIdx ''x'' (N 0) v› .. ― ‹Shortcut for assignment to index ‹0››
  term ‹''x'' ::= v› term ‹imp‹x = v+1››
  
  text ‹Note: In fancy syntax, assignment between variables is always parsed as array copy.
    This is no problem unless a variable is used as both, array and plain value, 
    which should be avoided anyway.
  ›
    
  term ‹ArrayCpy ''d'' ''s''› ― ‹Copy whole array. Both operands are variable names.›
  term ‹''d''[] ::= ''s''› term ‹imp‹d = s››
  
  term ‹ArrayClear ''a''› ― ‹Initialize array to all zeroes.›
  term ‹CLEAR ''a''[]› term ‹imp‹clear a[]››

  text ‹Semantics of these is straightforward›
  thm big_step.AssignIdx big_step.ArrayCpy big_step.ArrayClear
  
  subsection ‹Local and Global Variables›
  term ‹is_global› term ‹is_local› ― ‹Partitions variable names›
  term ‹<s1|s2>› ― ‹State with locals from ‹s1› and globals from ‹s2››
  
  term ‹SCOPE c› term ‹imp‹scope { skip }››    ― ‹Execute ‹c› with fresh set of local variables›
  thm big_step.Scope
  
  subsubsection ‹Parameter Passing›
  text ‹Parameters and return values by global variables: This is syntactic sugar only:›
  context fixes f :: com begin
  term ‹imp‹ (r1,r2) = f(x1,x2,x3)››
  end
  
  
  subsection ‹Recursive procedures›
  term ‹PCall ''name''› 
  thm big_step.PCall
  
  subsubsection ‹Procedure Scope›
  text ‹Execute command with local set of procedures›
  term ‹PScope π c›
  thm big_step.PScope
  
  subsubsection ‹Syntactic sugar for procedure call with parameters›
  term ‹imp‹(r1,r2) = rec name(x1,x2,x3)››
  
  subsection ‹More Readable VCs›
  lemmas nat_distribs = nat_add_distrib nat_diff_distrib Suc_diff_le nat_mult_distrib nat_div_distrib
  
  lemma "s0 ''n'' 0 ≥ 0 ⟹ wlp π exp_count_up1 (λs. s ''a'' 0 = 2^nat (s0 ''n'' 0)) s0"
    unfolding exp_count_up1_def
    apply (subst annotate_whileI[where 
          I="λs. s ''n'' 0 = s0 ''n'' 0 ∧  s ''a'' 0 = 2 ^ nat (s ''c'' 0) ∧ 0 ≤ s ''c'' 0 ∧ s ''c'' 0 ≤ s0 ''n'' 0" 
        ])
    apply (i_vcg_preprocess; i_vcg_gen; clarsimp)
    text ‹The postprocessor converts from states applied to string names to actual variables›
    apply i_vcg_postprocess
    by (auto simp: algebra_simps nat_distribs)
        
  lemma "s0 ''n'' 0 ≥ 0 ⟹ wlp π exp_count_up1 (λs. s ''a'' 0 = 2^nat (s0 ''n'' 0)) s0"
    unfolding exp_count_up1_def
    apply (subst annotate_whileI[where 
          I="λs. s ''n'' 0 = s0 ''n'' 0 ∧  s ''a'' 0 = 2 ^ nat (s ''c'' 0) ∧ 0 ≤ s ''c'' 0 ∧ s ''c'' 0 ≤ s0 ''n'' 0" 
        ])
    text ‹The postprocessor is invoked by default›    
    apply vcg
    oops
    
    
  subsection ‹Specification Commands›    
  
  text ‹IMP2 provides a set of commands to simplify specification and annotation of programs.›

  text ‹Old way of proving a specification: ›  
  lemma "let n = s0 ''n'' 0 in n ≥ 0 
    ⟹ wlp π exp_count_up1 (λs. let a = s ''a'' 0; n0 = s0 ''n'' 0 in a = 2^nat (n0)) s0"
    unfolding exp_count_up1_def
    apply (subst annotate_whileI[where 
          I="λs. s ''n'' 0 = s0 ''n'' 0 ∧  s ''a'' 0 = 2 ^ nat (s ''c'' 0) ∧ 0 ≤ s ''c'' 0 ∧ s ''c'' 0 ≤ s0 ''n'' 0" 
          (* Similar for invar! *)
        ])
    apply vcg
    apply (auto simp: algebra_simps nat_distribs)
    done
  
  lemma "VAR (s x) P = (let v=s x in P v)" unfolding VAR_def by simp 

  text ‹IMP2 specification commands›
  program_spec (partial) exp_count_up
    assumes "0≤n"               ― ‹Precondition. Use variable names of program.›
    ensures "a = 2^nat n0"       ― ‹Postcondition. Use variable names of programs. 
                                      Suffix with ‹⋅0› to refer to initial state›
    defines                     ― ‹Program›
    ‹
      a = 1;
      c = 0;
      while (c<n) 
        @invariant ‹n=n0 ∧ a=2^nat c ∧ 0≤c ∧ c≤n› ― ‹
            Invar annotation. Variable names and suffix ‹⋅0› for variables from initial state.›
      {
        a=2*a;
        c=c+1
      }
    ›
    apply vcg
    by (auto simp: algebra_simps nat_distribs)

  thm exp_count_up_spec  
  thm exp_count_up_def
      
  (* 
    We can also annotate 
      @variant ‹measure-expression› 
        (interpreted over variables (v) and variables at program start (v0) 
        
    or, both @variant ‹…› and @relation ‹R›:
      R :: 'a rel, and variant produces an 'a
      
  *)
          
  
  procedure_spec exp_count_up_proc(n) returns a
    assumes "0≤n"               
    ensures "a = 2^nat n0"      
    defines                     
    ‹
      a = 1;
      c = 0;
      while (c<n) 
        @invariant ‹n=n0 ∧ a=2^nat c ∧ 0≤c ∧ c≤n› 
        @variant ‹n-c›
      {
        a=2*a;
        c=c+1
      }
    ›
    apply vcg
    by (auto simp: algebra_simps nat_distribs)
  
  text ‹Simple Recursion›
  recursive_spec 
    exp_rec(n) returns a assumes "0≤n" ensures "a=2^nat n0" variant "n"
    defines ‹if (n==0) a=1 else {t=rec exp_rec(n-1); a=2*t}›
    apply vcg
      apply (auto simp: algebra_simps nat_distribs)
    by (metis Suc_le_D diff_Suc_Suc dvd_1_left dvd_imp_le minus_nat.diff_0 nat_0_iff nat_int neq0_conv of_nat_0 order_class.order.antisym pos_int_cases power_Suc zless_nat_eq_int_zless)
    
  text ‹Mutual Recursion: See Examples›
        

end