theory Demo13 imports Hoare begin

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

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

lemma "\<turnstile> \<lbrace> True \<rbrace> \<acute>B := 2 \<lbrace> \<acute>B = 2 \<rbrace>"
  apply hoare
  done
  
lemma mult_by_add:
  "\<turnstile> \<lbrace> \<acute>A = 0 \<and> \<acute>B = 0 \<rbrace>
    WHILE \<acute>A \<noteq> a
    INV \<lbrace> \<acute>B = \<acute>A * b \<rbrace> DO 
      \<acute>B := \<acute>B + b; 
      \<acute>A := \<acute>A + 1
    OD
    \<lbrace>\<acute>B = a * b \<rbrace>"
  apply hoare
  apply auto
  done
  

  

lemma factorial_sound:
  "\<turnstile> \<lbrace> \<acute>A = n \<rbrace>
  \<acute>B := 1;
  WHILE \<acute>A \<noteq> 0 INV \<lbrace> \<acute>B * fac \<acute>A = fac n \<rbrace> DO
    \<acute>B := \<acute>B * \<acute>A;
    \<acute>A := \<acute>A - 1
  OD
  \<lbrace> \<acute>B = fac n \<rbrace>"
  apply hoare
    apply simp
   apply clarsimp
   apply (case_tac "A s")
    apply simp
   apply (simp add: ring_simps)
  apply clarsimp
  done
  

-- "Arrays"

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


lemma zero_search: 
 "\<turnstile> \<lbrace> True \<rbrace>
  \<acute>I := 0;
  WHILE \<acute>I < length \<acute>L \<and> \<acute>L!\<acute>I \<noteq> key 
  INV \<lbrace> \<forall>j < \<acute>I. \<acute>L!j \<noteq> key \<rbrace> DO
    \<acute>I := \<acute>I+1 
  OD
  \<lbrace> (\<acute>I < length \<acute>L \<longrightarrow> \<acute>L!\<acute>I = key) \<and>
    (\<acute>I = length \<acute>L \<longrightarrow> key \<notin> set \<acute>L) \<rbrace>"
  apply hoare
    apply simp
   apply clarsimp
   apply (case_tac "j < I s")
    apply fastsimp
   apply (subgoal_tac "j = I s")
    apply simp
   apply simp
  apply clarsimp
  apply (drule all_nth_imp_all_set, assumption)
  apply simp
  done



end
