isabelle: src/HOL/IMP/VC.thy@b6456ccd9e3e (annotated)

1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1451 diff changeset	1	(* Title: HOL/IMP/VC.thy
1447 bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1451 diff changeset	3	Author: Tobias Nipkow
1447 bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	4	Copyright 1996 TUM
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	5
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	6	acom: annotated commands
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	7	vc: verification-conditions
2810 c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	8	awp: weakest (liberal) precondition
1447 bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	9	*)
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	10
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	11	VC = Hoare +
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	12
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	13	datatype acom = Askip
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	14	\| Aass loc aexp
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	15	\| Asemi acom acom
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	16	\| Aif bexp acom acom
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	17	\| Awhile bexp assn acom
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	18
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	19	consts
2810 c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	20	vc,awp :: acom => assn => assn
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	21	vcawp :: "acom => assn => assn * assn"
1447 bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	22	astrip :: acom => com
bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	23
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 4897 diff changeset	24	primrec
2810 c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	25	"awp Askip Q = Q"
4897 be11be0b6ea1 Changed [/] to [:=] and removed actual definition. nipkow parents: 3842 diff changeset	26	"awp (Aass x a) Q = (%s. Q(s[x:=a s]))"
2810 c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	27	"awp (Asemi c d) Q = awp c (awp d Q)"
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	28	"awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	29	"awp (Awhile b I c) Q = I"
1447 bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	30
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 4897 diff changeset	31	primrec
3842 b55686a7b22c fixed dots; wenzelm parents: 2810 diff changeset	32	"vc Askip Q = (%s. True)"
b55686a7b22c fixed dots; wenzelm parents: 2810 diff changeset	33	"vc (Aass x a) Q = (%s. True)"
2810 c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	34	"vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
1900 c7a869229091 Simplified primrec definitions. berghofe parents: 1696 diff changeset	35	"vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)"
c7a869229091 Simplified primrec definitions. berghofe parents: 1696 diff changeset	36	"vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
2810 c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	37	(I s & b s --> awp c I s) & vc c I s)"
1447 bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	38
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 4897 diff changeset	39	primrec
1900 c7a869229091 Simplified primrec definitions. berghofe parents: 1696 diff changeset	40	"astrip Askip = SKIP"
c7a869229091 Simplified primrec definitions. berghofe parents: 1696 diff changeset	41	"astrip (Aass x a) = (x:=a)"
c7a869229091 Simplified primrec definitions. berghofe parents: 1696 diff changeset	42	"astrip (Asemi c d) = (astrip c;astrip d)"
c7a869229091 Simplified primrec definitions. berghofe parents: 1696 diff changeset	43	"astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
c7a869229091 Simplified primrec definitions. berghofe parents: 1696 diff changeset	44	"astrip (Awhile b I c) = (WHILE b DO astrip c)"
1451 6803ecb9b198 Added vcwp nipkow parents: 1447 diff changeset	45
2810 c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	46	(* simultaneous computation of vc and awp: *)
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 4897 diff changeset	47	primrec
3842 b55686a7b22c fixed dots; wenzelm parents: 2810 diff changeset	48	"vcawp Askip Q = (%s. True, Q)"
4897 be11be0b6ea1 Changed [/] to [:=] and removed actual definition. nipkow parents: 3842 diff changeset	49	"vcawp (Aass x a) Q = (%s. True, %s. Q(s[x:=a s]))"
2810 c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	50	"vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	51	(vcc,wpc) = vcawp c wpd
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	52	in (%s. vcc s & vcd s, wpc))"
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	53	"vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	54	(vcc,wpc) = vcawp c Q
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	55	in (%s. vcc s & vcd s,
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	56	%s.(b s --> wpc s) & (~b s --> wpd s)))"
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	57	"vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	58	in (%s. (I s & ~b s --> Q s) &
c4e16b36bc57 Added wp_while. nipkow parents: 1900 diff changeset	59	(I s & b s --> wpc s) & vcc s, I))"
1451 6803ecb9b198 Added vcwp nipkow parents: 1447 diff changeset	60
1447 bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: diff changeset	61	end

author	paulson
	Thu, 01 Oct 1998 18:30:05 +0200
changeset 5601	b6456ccd9e3e
parent 5183	89f162de39cf
child 9241	f961c1fdff50
permissions	-rw-r--r--