(* Title: HOL/IMPP/EvenOdd.thy ID: $Id: EvenOdd.thy,v 1.6 2005/09/17 18:14:30 wenzelm Exp $ Author: David von Oheimb Copyright 1999 TUM *) header {* Example of mutually recursive procedures verified with Hoare logic *} theory EvenOdd imports Misc begin constdefs even :: "nat => bool" "even n == 2 dvd n" consts Even :: pname Odd :: pname axioms Even_neq_Odd: "Even ~= Odd" Arg_neq_Res: "Arg ~= Res" 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))" defs bodies_def: "bodies == [(Even,evn),(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)" ML {* use_legacy_bindings (the_context ()) *} end
theorem even_0:
EvenOdd.even 0
theorem not_even_1:
EvenOdd.even (Suc 0) = False
theorem even_step:
EvenOdd.even (Suc (Suc n)) = EvenOdd.even n
theorem Z_eq_Arg_plus_def2:
(Z=Arg+n) Z s = (Z = s<Arg> + n)
theorem Res_ok_def2:
Res_ok Z s = (EvenOdd.even Z = (s<Res> = 0))
theorem body_Odd:
body Odd = Some odd
theorem body_Even:
body Even = Some evn
theorem Odd_lemma:
{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}
theorem Even_lemma:
{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}
theorem Even_ok_N:
{}|-{Z=Arg+0}. BODY Even .{Res_ok}
theorem Even_ok_S:
{}|-{Z=Arg+0}. BODY Even .{Res_ok}