theory week09A_demo_sol 
imports "~~/src/HOL/Hoare/HeapSyntax" 
begin


primrec
  fac :: "nat \<Rightarrow> nat"
where
  "fac 0 = 1"
| "fac (Suc n) = (Suc n) * fac n"


lemma "VARS B { True } B := x { B = x  }"
  apply vcg
  done
  
lemma 
  " VARS (x::nat) y r 
    {True} 
    IF x>y THEN r:=x ELSE r:=y FI
    {r\<ge>x \<and> r \<ge>y \<and> (r=x \<or> r=y)}"
  apply vcg
  apply simp
  done
  
lemma
  "VARS (A::int) B 
   { A = 0 \<and> B = 0 }
    WHILE A \<noteq> a
    INV { B = A * b } DO
      B := B + b; 
      A := A + 1
    OD
    {B = a * b }"
  by (vcg; simp add: distrib_right)
  
lemma factorial_sound:
  "VARS A B
  { A = n}
  B := 1;
  WHILE A \<noteq> 0 INV { fac n = B * fac A } DO
    B := B * A;
    A := A - 1
  OD
  { B = fac n }"
  apply (vcg; clarsimp)
  apply (case_tac A; clarsimp)
  done


\<comment> \<open>----------------------------------------------------------------------------------\<close>

\<comment> \<open>Arrays\<close>

(* define a program that looks for a key in an array *)
(*think about the loop invariant *)
lemma 
 "VARS I L 
 { True }
  I := 0;
  WHILE I < length L \<and> L!I \<noteq> key 
  INV { \<forall>i<I. L ! i \<noteq> key } DO
    I := I+1 
  OD
  { (I < length L \<longrightarrow> L!I = key) \<and> (I=length L \<longrightarrow> key \<notin> set L)}"
  apply (vcg; clarsimp)
  using less_antisym apply blast
  by (meson in_set_conv_nth)

(* another version done in the class *)
term take
lemma
 "VARS I L 
 { True }
  I := 0;
  WHILE I < length L \<and> L!I \<noteq> key 
  INV { key \<notin> set (take I L)  } DO
    I := I+1 
  OD
  { (I < length L \<longrightarrow> L!I = key) \<and> (I=length L \<longrightarrow> key \<notin> set L)}"
  apply vcg
    apply simp
  defer
   apply clarsimp
  apply clarsimp
  using take_Suc_conv_app_nth by fastforce


\<comment> \<open>Pointers\<close>
thm List_def Path.simps

(* "List nxt p Ps" represents a linked list, starting
    at pointer p, with 'nxt' being the function to find
    the next pointer, and Ps the list of all the content
    of the linked list *)

(* define a function that takes X, p and nxt function,
   assuming that X in the set of the linked list,
   then it returns the pointer to that element *)

(* think about its loop invariant *)

(* because we are updating p itself, it is hard to state that X is not
   in the set of the path segment that we have already looked at. Instead
   we state the existence of the remaining segment that should include X *)

lemma
 "VARS nxt p
  { List nxt p Ps \<and> X \<in> set Ps }
  WHILE p \<noteq> Null \<and> p \<noteq> Ref X
  INV { \<exists>Ps. List nxt p Ps \<and> X \<in> set Ps }
  DO p := p^.nxt OD
  {  p = Ref X }"
  apply vcg
  apply auto
  done

(* if we don't assume that X is in the set of the linked list, we need
   to change the the invariant and postconditions as follows *)

lemma "VARS nxt p
  { List nxt p Ps }
  WHILE p \<noteq> Null \<and> p \<noteq> Ref X
  INV {  \<exists>ls ls'. Ps = ls @ ls' \<and> List nxt p ls' \<and> X \<notin> set ls }
  DO p := p^.nxt OD
  { ( X \<in> set Ps \<longrightarrow> p = Ref X) \<and> (\<not>  X \<in> set Ps \<longrightarrow> p = Null) }"
  apply vcg
  by fastforce+


(* define a function that "splices" 2 disjoint linked lists together *)

(* think about its loop invariant *)

lemma "VARS tl p q pp qq
  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> size Qs \<le> size Ps}
  pp := p;
  WHILE q \<noteq> Null
  INV {\<exists>as bs qs.
    distinct as \<and> Path tl p as pp \<and> List tl pp bs \<and> List tl q qs \<and>
    set bs \<inter> set qs = {} \<and> set as \<inter> (set bs \<union> set qs) = {} \<and>
    size qs \<le> size bs \<and> splice Ps Qs = as @ splice bs qs}
  DO qq := q^.tl; q^.tl := pp^.tl; pp^.tl := q; pp := q^.tl; q := qq OD
  {List tl p (splice Ps Qs)}"
  apply (vcg; simp)
    apply(rule_tac x = "[]" in exI)
    apply fastforce
   apply clarsimp
   apply(rename_tac y bs qqs)
   apply(case_tac bs; clarsimp)
   apply(rename_tac x bbs)
   apply(rule_tac x = "as @ [x,y]" in exI)
   apply simp
   apply(rule_tac x = "bbs" in exI)
   apply simp
   apply(rule_tac x = "qqs" in exI)
   apply simp
  apply (fastforce simp: List_app)
  done


end