isabelle: src/HOL/IMPP/EvenOdd.thy@340c466c9605 (annotated)

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

author	wenzelm
	Fri, 05 May 2006 21:59:41 +0200
changeset 19573	340c466c9605
parent 17477	ceb42ea2f223
child 19803	aa2581752afb
permissions	-rw-r--r--