theory Demo13_2 imports "./Pointers"
begin




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

record vars =
  A :: "nat"
  B :: "nat"


lemma "VARS B { True } B := 2 { B = 2 }"
  apply vcg_simp
  done

lemma 
  " VARS (x::nat) y r 
    {True} 
    IF x>y THEN r:=x ELSE r:=y FI
    { (r=x\<or> r=y) \<and> r\<ge>x \<and> r\<ge>y} "
  apply vcg_simp
  done


lemma mult_by_add:
  "VARS A 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 }"
  oops

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 }"
  oops

  

-- "Arrays"
  
record vars2 =
  I :: "nat"
  L :: "nat list"


lemma zero_search: 
 "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 clarsimp
   apply (case_tac "j < I")
    apply fastsimp
   apply (subgoal_tac "j = I")
    apply simp
   apply simp
  apply clarsimp thm all_nth_imp_all_set
  apply (drule all_nth_imp_all_set, assumption)
  apply simp
  done 


-- Pointers

record vars3 = vars2 +
  nxt :: "nat \<Rightarrow> nat ref"
  p :: "nat ref"

lemma element_search:
 "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_simp
    apply blast
   apply clarsimp
  apply clarsimp
  done
   
end