theory week12B_demo

imports "~~/src/HOL/Hoare/Hoare_Logic"

begin


-- -------------------------------------------------
section "recursive functions"
-- -------------------------------------------------

text {* see http://isabelle.in.tum.de/dist/Isabelle2012/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 in natural numbers in a relation

                    apply (relation "measure ..") 

               relation takes a relation of type ('a × '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 × '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





-- -------------------------------------------------
section "functional correctness"
-- -------------------------------------------------


text {*

Goal: prove correctness of following program

    VARS k m d t
    {(*TODO*)}
    k := K;
    m := M;
    WHILE m \<noteq> 0
    INV { (*TODO*)} DO
      t := m;
      m := k mod m;
      k := t
    OD; 
    d := k
    { d= gcd(K,M) }"


Question: what is this program computing?

Question: write the standard definition in Isabelle of a postcondition
          for this program (i.e. functional version of this program)

Question: write a precondition and an invariant

Question: find another definition of the postcondition that would make
          the reasoning of the invariant easier, and prove its
          equivalent to the standard one.

Question: prove the correctness of the program

*}

text {* standard definition of gcd *}
definition gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
  "gcd k m \<equiv> THE d. d dvd k \<and> d dvd m \<and> (\<forall> d'. d' dvd k \<and> d' dvd m \<longrightarrow> d' \<le> d)"

text {* other definition of gcd, usingsame algorithm than our program *}
fun gcd2 ::  "nat \<Rightarrow> nat \<Rightarrow> nat" where
  "gcd2 k 0 = k" |
  "gcd2 k m = gcd2 m (k mod m)"

text {* gcd2 is a common divisor *}
lemma gcd2_common_divisor:
  "gcd2 k m dvd k \<and> gcd2 k m dvd m"
  apply(induct k m rule: gcd2.induct)
   apply simp
  apply clarsimp
  apply (erule (1) dvd_mod_imp_dvd)
  done

text {*gcd2 is the greatest *}
lemma gcd2_bounds_common_divisors:
  "k \<noteq> 0 \<or> m \<noteq> 0 \<Longrightarrow> x dvd k \<and> x dvd m \<Longrightarrow> x \<le> gcd2 k m"
  apply(induct k m arbitrary: x rule: gcd2.induct)
   apply (fastforce elim: dvd_imp_le)
  apply (fastforce intro: dvd_mod)
  done

text {*gcd2 is the greatest common divisor *}
lemma greatest_common_divisor_is_gcd2:
  assumes a: "k \<noteq> 0 \<or> m \<noteq> 0"
  assumes b: "d dvd k \<and> d dvd m \<and> (\<forall>d'. d' dvd k \<and> d' dvd m \<longrightarrow> d' \<le> d)"
  shows "d = gcd2 k m"
  proof(rule le_antisym)
  from a b show "d \<le> gcd2 k m" 
   by (fastforce intro: gcd2_bounds_common_divisors)
  from a b gcd2_common_divisor show "gcd2 k m \<le> d" by auto
  qed

text {* gcd2 is equivalent to gcd*}
lemma gcd_gcd2:
  "\<lbrakk>k \<noteq> 0 \<or> m \<noteq> 0\<rbrakk> \<Longrightarrow> gcd k m = gcd2 k m"
  apply(simp add: gcd_def)
  apply(rule the_equality)
   using gcd2_common_divisor gcd2_bounds_common_divisors greatest_common_divisor_is_gcd2 by auto


text {* correctness of the program *}
lemma "
    VARS k m d t
    {K \<noteq> 0 \<or> M \<noteq> 0}
    k := K;
    m := M;
    WHILE m \<noteq> 0
    INV { gcd k m = gcd K M \<and> (k \<noteq> 0 \<or> m \<noteq> 0)} DO
      t := m;
      m := k mod m;
      k := t
    OD; 
    d := k
    { d = gcd K M }"
  apply (vcg_simp)
   apply clarsimp
   apply (simp add: gcd_gcd2)
   apply (case_tac m, clarsimp)
   apply clarsimp apply clarsimp
  apply (clarsimp simp: gcd_gcd2)
  done



-- -------------------------------------------------
section "playing with numbers"
-- -------------------------------------------------
 

text {* 

Question: define a tree type containing elements of type "int" in the
          nodes (including leaves)

Question: define a function sum_nodes:: "tree \<Rightarrow> nat" computing the sum
          of all elements. Try on some examples 

*}

datatype tree
  = Leaf int
  | Node tree int tree

primrec sum_node:: "tree \<Rightarrow> nat"
where
 "sum_node (Leaf i) = (nat i)"
|"sum_node (Node t1 i t2) = (nat i) + sum_node t1 + sum_node t2"

value "nat (-1)"
term nat

value "sum_node (Node (Leaf 3) 6 (Leaf 1))"
value "sum_node (Node (Node (Leaf 3) 6 (Leaf 1)) 14 (Leaf 0)) "

end