isabelle: src/HOL/IMP/Com.thy@578a51fae383 (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
42174 d0be2722ce9f modernized specifications; wenzelm parents: 41589 diff changeset	14	type_synonym val = nat -- "or anything else, @{text nat} used in examples"
d0be2722ce9f modernized specifications; wenzelm parents: 41589 diff changeset	15	type_synonym state = "loc \<Rightarrow> val"
d0be2722ce9f modernized specifications; wenzelm parents: 41589 diff changeset	16	type_synonym aexp = "state \<Rightarrow> val"
d0be2722ce9f modernized specifications; wenzelm parents: 41589 diff changeset	17	type_synonym bexp = "state \<Rightarrow> bool"
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	18	-- "arithmetic and boolean expressions are not modelled explicitly here,"
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	19	-- "they are just functions on states"
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	20
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	21	datatype
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	22	com = SKIP
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	23	\| Assign loc aexp ("_ :== _ " 60)
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	24	\| Semi com com ("_; _" [60, 60] 10)
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	25	\| Cond bexp com com ("IF _ THEN _ ELSE _" 60)
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	26	\| While bexp com ("WHILE _ DO _" 60)
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	27
27362 a6dc1769fdda modernized specifications; wenzelm parents: 16417 diff changeset	28	notation (latex)
a6dc1769fdda modernized specifications; wenzelm parents: 16417 diff changeset	29	SKIP ("\<SKIP>") and
a6dc1769fdda modernized specifications; wenzelm parents: 16417 diff changeset	30	Cond ("\<IF> _ \<THEN> _ \<ELSE> _" 60) and
a6dc1769fdda modernized specifications; wenzelm parents: 16417 diff changeset	31	While ("\<WHILE> _ \<DO> _" 60)
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	32
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	33	end

author	wenzelm
	Tue, 05 Apr 2011 14:25:18 +0200
changeset 42224	578a51fae383
parent 42174	d0be2722ce9f
child 43141	11fce8564415
permissions	-rw-r--r--