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

lemma
  "VARS (A::int) B 
   { True }
    A:=0;
    B:=0;
    WHILE A \<noteq> a
    INV { B = A * b } DO
      B := B + b; 
      A := A + 1
    OD
    {B = a * b }"
  apply vcg 
    apply simp 
  (*sledgehammer*)
   apply (smt semiring_normalization_rules(3))
  apply simp
  done

lemma
  "VARS (A::int) B 
   { a\<ge>0 }
    A:=0;
    B:=0;
    WHILE A < a
    INV { B = A * b \<and> A\<le>a  } DO
      B := B + b; 
      A := A + 1
    OD
    {B = a * b }"
  apply vcg
    apply simp
   (*sledgehammer*)
   apply (simp add: int_distrib(1))
  sledgehammer
  by force

lemma
  "VARS (A::nat) (B::int) 
   { b\<ge>0 }
    A:=a;
    B:=1;
    WHILE A \<noteq> 0
    INV { B = (b^(a-A)) \<and>A\<le>a} DO
      B := B * b; 
      A := A - 1
    OD
    {B = (b^a) }"
  apply vcg 
    apply simp 
   (*sledgehammer*)
   using Suc_diff_le apply auto[1]
 (*sledgehammer*)
  using Suc_diff_le by auto
(* Note: if you forget A\<le>a then you get an unsolvable goal; 
   you can try nitpick which will find a counterexample.
   The added condition is required to use the theorem 
       thm Suc_diff_le
*)


lemma
  "VARS (X::int list) (Y::int list) 
   { True }
    X:=x;
    Y:=[];
    WHILE X \<noteq> []
    INV { (rev X)@Y = rev x } DO
      Y := (hd X # Y); 
      X := tl X
    OD
    {Y = rev x }"
  apply vcg 
    apply simp 
   (*sledgehammer*)
   apply (metis append.left_neutral append_eq_append_conv2 list.collapse rev.simps(2) rev_append rev_rev_ident)
  apply clarsimp
  done
  (* NB: can also use  INV { x = rev Y @ X } *)

lemma
  "VARS (A::int) (B::nat) (C::int)
   { a\<ge>0 }
    A:=a;
    B:=b;
    C:=1;
    WHILE B \<noteq> 0
    INV { a^b = C*A^B} DO
      WHILE ((B mod 2) = 0) 
      INV {a^b = C*A^B} DO
        A:=A*A;
        B:=B div 2
      OD;
      C := C * A; 
      B := B - 1
    OD
    {C = (a^b) }"
  apply vcg 
      apply simp_all
   (*sledgehammer*)
   apply (metis dvd_eq_mod_eq_0 dvd_mult_div_cancel semiring_normalization_rules(30) semiring_normalization_rules(36)) 
  (*sledgehammer*)
  by (metis One_nat_def dvd_imp_mod_0 odd_Suc_minus_one one_neq_zero power_Suc)





text \<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 *)

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

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. Path nxt p Ps (Ref X) }
  DO p := p^.nxt OD
  {  p = Ref X }"
  apply vcg 
  (* try find_theorems "_\<in>_" "_@_" *)
  (* sledghammer also works *)
    apply (simp add: in_set_conv_decomp)
    apply clarsimp
    apply (simp add: List_app)
    apply blast
   apply auto
  done




(* 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