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

author	krauss
	Sat, 27 Dec 2008 17:49:15 +0100
changeset 29183	f1648e009dc1
parent 27362	a6dc1769fdda
child 41589	bbd861837ebc
permissions	-rw-r--r--