Theory EvenOdd

Up to index of Isabelle/HOL/IMPP

(*  Title:      HOL/IMPP/EvenOdd.thy
    ID:         $Id: EvenOdd.thy,v 1.13 1999/11/24 13:48:19 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1999 TUM

Example of mutually recursive procedures verified with Hoare logic
*)

EvenOdd = Hoare +

constdefs even :: nat => bool
  "even n == 2 dvd n"

consts
  Even, Odd :: pname
rules 
  Even_neq_Odd "Even ~= Odd"

constdefs
  evn :: com
 "evn == IF (%s. s<Arg>=0)
         THEN Loc Res:==(%s. 0)
         ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
              Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
              Loc Res:==(%s. s<Res> * s<Arg>))"
  odd :: com
 "odd == IF (%s. s<Arg>=0)
         THEN Loc Res:==(%s. 1)
         ELSE(Loc Res:=CALL Even (%s. s<Arg> -1))"

rules
  body_Even "body Even = evn"
  body_Odd  "body Odd  = odd"
  
consts
  Z_eq_Arg_plus   :: nat => nat assn ("Z=Arg+_" [50]50)
 "even_Z=(Res=0)" ::        nat assn ("Res'_ok")
defs
  Z_eq_Arg_plus_def "Z=Arg+n == %Z s.      Z =  s<Arg>+n"
  Res_ok_def       "Res_ok   == %Z s. even Z = (s<Res>=0)"

end

even

theorem even_0:

  even 0

theorem not_even_1:

  even 1 = False

theorem even_step:

  even (Suc (Suc n)) = even n

Arg, Res

theorem Z_eq_Arg_plus_def2:

  (Z=Arg+n) Z s = (Z = s<Arg> + n)

theorem Res_ok_def2:

  Res_ok Z s = (even Z = (s<Res> = 0))

verification

theorem Odd_lemma:

  {{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+1}. body Odd .{Res_ok}

theorem Even_lemma:

  {{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. body Even .{Res_ok}

theorem Even_ok_N:

  {}|-{Z=Arg+0}. BODY Even .{Res_ok}

theorem Even_ok_S:

  {}|-{Z=Arg+0}. BODY Even .{Res_ok}