(*<*) theory a7 = Hoare: (*>*)

section {* Beweise in Hoare-Logik *}

text {* Gegeben ist das folgende imperative Programm, das 
in einem Array @{text a} das minimale Element @{text min}
berechnet. 

Weisen Sie die Korrektheit dieses Programms nach, indem Sie zeigen,
daß die Nachbedingung gilt. Entwickeln Sie dazu eine geeignete
Invariante und beweisen Sie anschließend die durch den
Verifikationsbedingungs-Generator erzeugten Aussagen.  *}

lemma min_find: "
  VARS i (min::nat) a n
  {length a = n \<and> 0 < n}
  i := 0;
  min := a ! 0;
  WHILE i < n
  INV {True}
  DO
    IF (a ! i) < min THEN min := (a ! i) ELSE SKIP FI;
    i := i + 1
  OD
  {\<forall> v \<in> set a. min \<le> v}"
apply vcg
oops

(*<*) end (*>*)