theory week12B_demo
imports
  AutoCorres
begin



-- -------------------------------------------------
section {* Invariants *}
-- -------------------------------------------------


text {* 

Find postconditions and invariants (informally / pen&paper) for:

f1(a,b):
{
    while (b > 0) {
        a += 1;
        b -= 1;
    }
    return a;
}

f2(a,b):
{  
  b=1;
  while (a<>0) {
    b=b*a
    a--
  }
}

f3(n):
{
  res=0;
  i=1;
  while (i<>n) {
     res=res+i;
     i++;
  }
  return res;
}

f4(n):
{
   if (n < 2)
     return 0;
   i = 2;
   while (n % i != 0) {
     i++;
   }
   return (i == n);
}

f5(p,q) (from week08B)
(precondition: {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and> size Qs \<le> size Ps})
(postcondition: {List next p (splice Ps Qs)} )
(for invariant, can use (Path next p Xs pp))
{ 
   pp=p;
   while (q<>Null){
      qq = q->next;
      q->next = pp->next; 
      pp->next = q; 
      pp := q->next; 
      q := qq
   }
}
   
  

    

*}

text {* Answers:
 
f1(A,B): a + b = A + B

f2(A,B): b * fac a = fac A"

f3(N): 2*res = i*(i-1)

f4(m):  (\<forall>m. 2 \<le> m \<and> m < i \<longrightarrow> n mod m \<noteq> 0) 
        \<and> 2 \<le> i \<and> i \<le> n 
  (postcondition: prime n \<longleftrightarrow> (i = n) )      
        
  
f5(p,q): (\<exists>As Bs Cs. Path next p As pp \<and> List next pp Bs \<and> List next q Cs \<and>
           splice Ps Qs = As @ splice Bs Cs)
    (plus extra conditions on distinctness)    
           
 
 *}


-- -------------------------------------------------
section {* Autocorres and VCG *}
-- -------------------------------------------------


text {*

Example: Write a C function calculating the product of two numbers only using addition
         and prove it correct using Autocorres or/and VCG (partial correctness).


General reminder about VCG and Autocorres:

  - Write myfile.c defining myfunction (a1, ..., an) (run gcc to check)
  
  - Start new Isabelle file importing AutoCorres
  
  - Run C-parser:  install_C_file "myfile.c"
    This defines myfile_global_addresses.myfunction_body_def
  
  - Then work in the context of this file: "context myfile begin ... end"
    
  - Using just VCG:       
    -- state the lemma: 
     
      lemma 
        "\<Gamma> \<turnstile> {s. a1_' s = a1  \<and>  ...  \<and> an_' s = an  \<and> Precond s a1 ... an }
               \<acute>ret__unsigned :== PROC myfunction (a1,...,an)
             {t.  Postcond t a1 ... an (ret__unsigned_' t) }"
     
           (or   Call my_function_'proc )
           
           (NB: use \<Gamma> \<turnstile>\<^sub>t ... if you want to also show termination)
           
     -- then vcg_step  (not full vcg as we haven;t given any while loop invariant...)
     -- then whileAnno_def once to remove the implicit 'undefined' invariant
     -- then whileAnno_def again with the right invariant (and measure)
     -- then vcg
     -- then solve the goals
  
  - with Autocorres
    -- Run autocorres:  autocorres [ts_rules = nondet] "myfile.c"
       This defines myfile.myfunction'_def
       
    -- Then state lemma:
    
     lemma "\<lbrace> \<lambda>s. Precond a1 .. an s \<rbrace> 
            myfunction' a1 .. an 
            \<lbrace> \<lambda>r s. Postcond a1 .. an r s \<rbrace>"
            
        (NB: use \<lbrace>...\<rbrace> _ \<lbrace>...\<rbrace>!  if you want to also show termination)
            
    -- Then unfold definition
    -- Then whileLoop_add_inv to specify the invariant (and measure)
    -- Then wp
    -- then solve the goals    
    
*}
    
    
    
-- -------------------------------------------------
section "recursive functions"
-- -------------------------------------------------

text {* see http://isabelle.in.tum.de/dist/Isabelle2013/doc/functions.pdf *}


text {* 

Question: What is needed for a recursive function to be defined in Isabelle? Why?)

Question: What are the 3 ways of defining recursive functions?  

Question: When should each one be used? Give examples (eg app, fib, sum)*}

text {* 

Answer: We need to prove termination for all recursive functions we define.
        This is because all Isabelle function need to be total.
        (and this is to avoid inconsistencies, eg if f(n) = f(n) + 1 we could prove
         0 = 1 by subtracting f(n) on both sides)

Answer: primrec, fun and function

Answer: 

= WAY 1: primrec = 

     > to be used when one parameter is a datatype and the recursion
       is "primitive" (each recursive call peels off a datatype
       constructor from one of the arguments; thus recursion always
       terminates, i.e. the function is total)

     Namely, each equation should be of the form:

        f x1 ... xm (C y1 ...yk) z1 ...zn = rhs
 
     where
        - C is one of the datatype constructor 
        - all recursive occurrences of f in rhs are of the form f ... yi ... for some i
        - at most one reduction rule for each constructor can be given

     Example: 
*}


primrec app
where
  "app [] ys = ys "
| "app (x#xs) ys =  x#(app xs ys) "


text {*

= WAY 2: fun =

     > to be used for more complicated pattern matching, but
       "obvious" termination

   Example:
*}

fun fib :: "nat \<Rightarrow> nat" 
where
"fib 0 = 1"
| "fib (Suc 0) = 1"
| "fib (Suc (Suc n)) = fib n + fib (Suc n)"


fun sep:: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  "sep a (x # y # zs) = x # a # sep a (y # zs)" 
| "sep a xs = xs"

text {* Note that equations are read sequentially: if patterns
overlap, the order of the equations is taken into account. In sep, the
second equation is only meant for the cases where the first one does
not match.
*}

text {*

= WAY 3: function = 

   > any set of equations
     BUT need to prove that
        (a) equations are disjoint and complete
             > use "pat_completeness" method
             > may want to use (sequential) attribute if overlapping
               patterns
        (b) the function terminates (separate proof. If not there,
            partial rules only)
             > use "relation r" method
             > may want to use the "measure f" function that turns a
               function on natural numbers in a relation

                    apply (relation "measure ..") 

               relation takes a relation of type ('a \<times> 'a) set, where
               'a is the argument type of the function (if the
               function has 2 arguments of type say 'b and 'c
               resp. then we use tuples: 'a would be ('b x 'c)).

               measure :: ('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set constructs a
               wellfounded relation from a mapping into the natural
               numbers

            > we must prove that (a) the relation we supplied is
              wellfounded, and (b) that the arguments of recursive
              calls indeed decrease with respect to the relation

  Note: 

       fun f:: \<tau>
       where 
         <equations>

  is equivalent to 

       function (sequential) f :: \<tau>
       where 
        <equations>
       by pat_completeness auto

       termination by lexicographic_order

   Example: Write a function quicksort:: "nat list \<Rightarrow> nat list" sorting
            a list using the standard quick sort algorithm. 

            Hint: use the function filter:: ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a
            list and less_Suc_eq_le*}


fun quicksort
where
 "quicksort [] = []"
|"quicksort (x#xs) = (quicksort (filter (\<lambda>y. y\<le>x) xs)) @[x]@ (quicksort (filter (\<lambda>y. y>x) xs))"

text {* actually fun worked here! Let's try with function anyway *}

function (sequential) quicksort2 :: "nat list \<Rightarrow> nat list"
where
  "quicksort2 [] = []"
| "quicksort2 (x#xs) =
     quicksort2 [y \<leftarrow> xs. y \<le> x] @ [x] @ quicksort2 [y \<leftarrow> xs. x < y]"
  -- "need to prove distinctness and completeness of patterns"
     apply pat_completeness
    apply simp
   apply simp
  apply simp
  done

-- "get only partial simp and induction rules"
thm quicksort.psimps
thm quicksort.pinduct

termination quicksort2
  apply (relation "measure length") 
    thm less_Suc_eq_le
    apply (auto simp: less_Suc_eq_le)
  done


-- "now have full induction and simp available"
print_theorems

text {* 

  Other example: write a function "sum i N" which sums up natural
                 numbers up to N, using a counter i:
                     sum 0 N = 0+1+2+...+N

*}


function sum
where
"sum i N = (if i<N then sum (Suc i) N else 0)"
by auto

termination sum
  apply (relation "measure (\<lambda>(i,N). N-i)")
   apply simp
  apply simp
done


    
end