isabelle: src/HOL/IMP/Com.thy@6d736d983d5c (annotated)

12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	1	(* Title: HOL/IMP/Com.thy
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	2	Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
41589 bbd861837ebc tuned headers; wenzelm parents: 27362 diff changeset	3	Author: Gerwin Klein
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	4	*)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	5
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	6	header "Syntax of Commands"
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	7
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 12431 diff changeset	8	theory Com imports Main begin
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	9
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	10	typedecl loc
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	11	-- "an unspecified (arbitrary) type of locations
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	12	(adresses/names) for variables"
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	13
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	14	types
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	15	val = nat -- "or anything else, @{text nat} used in examples"
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	16	state = "loc \<Rightarrow> val"
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	17	aexp = "state \<Rightarrow> val"
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	18	bexp = "state \<Rightarrow> bool"
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	19	-- "arithmetic and boolean expressions are not modelled explicitly here,"
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	20	-- "they are just functions on states"
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	21
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	22	datatype
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	23	com = SKIP
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	24	\| Assign loc aexp ("_ :== _ " 60)
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	25	\| Semi com com ("_; _" [60, 60] 10)
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	26	\| Cond bexp com com ("IF _ THEN _ ELSE _" 60)
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	27	\| While bexp com ("WHILE _ DO _" 60)
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	28
27362 a6dc1769fdda modernized specifications; wenzelm parents: 16417 diff changeset	29	notation (latex)
a6dc1769fdda modernized specifications; wenzelm parents: 16417 diff changeset	30	SKIP ("\<SKIP>") and
a6dc1769fdda modernized specifications; wenzelm parents: 16417 diff changeset	31	Cond ("\<IF> _ \<THEN> _ \<ELSE> _" 60) and
a6dc1769fdda modernized specifications; wenzelm parents: 16417 diff changeset	32	While ("\<WHILE> _ \<DO> _" 60)
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	33
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	34	end

author	wenzelm
	Sun, 30 Jan 2011 13:02:18 +0100
changeset 41648	6d736d983d5c
parent 41589	bbd861837ebc
child 42174	d0be2722ce9f
permissions	-rw-r--r--