src/HOL/IMPP/EvenOdd.thy
author wenzelm
Sat Sep 17 20:14:30 2005 +0200 (2005-09-17)
changeset 17477 ceb42ea2f223
parent 15354 9234f5765d9c
child 19803 aa2581752afb
permissions -rw-r--r--
converted to Isar theory format;
oheimb@8177
     1
(*  Title:      HOL/IMPP/EvenOdd.thy
oheimb@8177
     2
    ID:         $Id$
oheimb@8177
     3
    Author:     David von Oheimb
oheimb@8177
     4
    Copyright   1999 TUM
oheimb@8177
     5
*)
oheimb@8177
     6
wenzelm@17477
     7
header {* Example of mutually recursive procedures verified with Hoare logic *}
oheimb@8177
     8
wenzelm@17477
     9
theory EvenOdd
wenzelm@17477
    10
imports Misc
wenzelm@17477
    11
begin
wenzelm@17477
    12
wenzelm@17477
    13
constdefs
wenzelm@17477
    14
  even :: "nat => bool"
wenzelm@11704
    15
  "even n == 2 dvd n"
oheimb@8177
    16
oheimb@8177
    17
consts
wenzelm@17477
    18
  Even :: pname
wenzelm@17477
    19
  Odd :: pname
wenzelm@17477
    20
axioms
wenzelm@17477
    21
  Even_neq_Odd: "Even ~= Odd"
wenzelm@17477
    22
  Arg_neq_Res:  "Arg  ~= Res"
oheimb@8177
    23
oheimb@8177
    24
constdefs
oheimb@8177
    25
  evn :: com
nipkow@15354
    26
 "evn == IF (%s. s<Arg> = 0)
oheimb@8177
    27
         THEN Loc Res:==(%s. 0)
oheimb@8177
    28
         ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
oheimb@8177
    29
              Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
oheimb@8177
    30
              Loc Res:==(%s. s<Res> * s<Arg>))"
oheimb@8177
    31
  odd :: com
nipkow@15354
    32
 "odd == IF (%s. s<Arg> = 0)
oheimb@8177
    33
         THEN Loc Res:==(%s. 1)
wenzelm@11701
    34
         ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))"
oheimb@8177
    35
oheimb@8177
    36
defs
wenzelm@17477
    37
  bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
wenzelm@17477
    38
oheimb@8177
    39
consts
wenzelm@17477
    40
  Z_eq_Arg_plus   :: "nat => nat assn" ("Z=Arg+_" [50]50)
wenzelm@17477
    41
 "even_Z=(Res=0)" ::        "nat assn" ("Res'_ok")
oheimb@8177
    42
defs
wenzelm@17477
    43
  Z_eq_Arg_plus_def: "Z=Arg+n == %Z s.      Z =  s<Arg>+n"
wenzelm@17477
    44
  Res_ok_def:       "Res_ok   == %Z s. even Z = (s<Res> = 0)"
wenzelm@17477
    45
wenzelm@17477
    46
ML {* use_legacy_bindings (the_context ()) *}
oheimb@8177
    47
oheimb@8177
    48
end