# Theory ExamplesAbort

Up to index of Isabelle/HOL/Hoare

theory ExamplesAbort
imports HoareAbort
begin

    (*  Title:      HOL/Hoare/ExamplesAbort.thy
        ID:         $Id: ExamplesAbort.thy,v 1.5 2005/07/07 10:39:32 nipkow Exp $
        Author:     Tobias Nipkow
        Copyright   1998 TUM

    Some small examples for programs that may abort.
    *)

    theory ExamplesAbort imports HoareAbort begin

    lemma "VARS x y z::nat
     {y = z & z ≠ 0} z ≠ 0 -> x := y div z {x = 1}"
    by vcg_simp

    lemma
     "VARS a i j
     {k <= length a & i < k & j < k} j < length a -> a[i] := a!j {True}"
    apply vcg_simp
    done

    lemma "VARS (a::int list) i
     {True}
     i := 0;
     WHILE i < length a
     INV {i <= length a}
     DO a[i] := 7; i := i+1 OD
     {True}"
    apply vcg_simp
    done

    end

lemma

      {y = z ∧ z ≠ 0}
       z ≠ 0 -> x := y div z
       {x = 1}

lemma

      {k ≤ length a ∧ i < k ∧ j < k}
       j < length a -> i < length a -> a := a[i := a ! j]
       {True}

lemma

      {True}
       i := 0;
       WHILE i < length a INV {i ≤ length a}
        DO i < length a -> a := a[i := 7]; i := i + 1 OD
       {True}