theory week10B_demo 
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 := 2 { B = 2 }"
  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 }"
  apply vcg_simp
  apply (simp add: left_distrib)
done


lemma factorial_sound:
  "VARS A B
  { A = n}
  B := 1;
  WHILE A \<noteq> 0 INV { B * fac A = fac n } DO
    B := B * A;
    A := A - 1
  OD
  { B = fac n }"
  apply vcg_simp
   apply (case_tac A, simp)
   apply clarsimp
   apply (metis  mult_Suc nat_mult_assoc nat_mult_commute)
  apply clarsimp
done

  

-- "Arrays"
  

lemma 
 "VARS I L 
 { True }
  I := 0;
  WHILE I < length L \<and> L!I \<noteq> key 
  INV { \<forall>j<I. L!j \<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_simp
   apply (intro allI impI)
   apply (case_tac "j<I")
    apply clarsimp
   apply (subgoal_tac "j=I")
    apply clarsimp
   apply clarsimp
  apply (simp add: in_set_conv_nth)
done




-- "Pointers"

thm List_def

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




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 { True (* TODO *)}
  DO qq := q^.tl; q^.tl := pp^.tl; pp^.tl := q; pp := q^.tl; q := qq OD
  {List tl p (splice Ps Qs)}"
thm splice.simps
thm Path.simps
oops
 
end