isabelle: src/HOL/MicroJava/J/Decl.thy@8ba39d2d9d0b (annotated)

8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	1	(* Title: HOL/MicroJava/J/Decl.thy
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	2	ID: $Id$
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	3	Author: David von Oheimb
11372 648795477bb5 corrected xsymbol/HTML syntax oheimb parents: 11070 diff changeset	4	Copyright 1999 Technische Universitaet Muenchen
11070 cc421547e744 improved document (added headers etc) oheimb parents: 11026 diff changeset	5	*)
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	6
12911 704713ca07ea new document kleing parents: 12517 diff changeset	7	header {* \isaheader{Class Declarations and Programs} *}
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	8
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 14134 diff changeset	9	theory Decl imports Type begin
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	10
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	11	types
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	12	fdecl = "vname \<times> ty" -- "field declaration, cf. 8.3 (, 9.3)"
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	13
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	14	sig = "mname \<times> ty list" -- "signature of a method, cf. 8.4.2"
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	15
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	16	'c mdecl = "sig \<times> ty \<times> 'c" -- "method declaration in a class"
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	17
18551 be0705186ff5 class now an keyword, quoted where necessary haftmann parents: 16417 diff changeset	18	'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list"
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	19	-- "class = superclass, fields, methods"
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	20
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	21	'c cdecl = "cname \<times> 'c class" -- "class declaration, cf. 8.1"
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	22
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	23	'c prog = "'c cdecl list" -- "program"
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	24
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	25
10613 78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	26	translations
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 10925 diff changeset	27	"fdecl" <= (type) "vname \<times> ty"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 10925 diff changeset	28	"sig" <= (type) "mname \<times> ty list"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 10925 diff changeset	29	"mdecl c" <= (type) "sig \<times> ty \<times> c"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 10925 diff changeset	30	"class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 10925 diff changeset	31	"cdecl c" <= (type) "cname \<times> (c class)"
10613 78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	32	"prog c" <= (type) "(c cdecl) list"
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	33
9346 297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast oheimb parents: 8011 diff changeset	34
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	35	constdefs
18551 be0705186ff5 class now an keyword, quoted where necessary haftmann parents: 16417 diff changeset	36	"class" :: "'c prog => (cname \<rightharpoonup> 'c class)"
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	37	"class \<equiv> map_of"
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	38
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	39	is_class :: "'c prog => cname => bool"
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	40	"is_class G C \<equiv> class G C \<noteq> None"
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	41
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 10925 diff changeset	42
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 10925 diff changeset	43	lemma finite_is_class: "finite {C. is_class G C}"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 10925 diff changeset	44	apply (unfold is_class_def class_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 10925 diff changeset	45	apply (fold dom_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 10925 diff changeset	46	apply (rule finite_dom_map_of)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 10925 diff changeset	47	done
9346 297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast oheimb parents: 8011 diff changeset	48
10613 78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	49	consts
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	50	is_type :: "'c prog => ty => bool"
9346 297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast oheimb parents: 8011 diff changeset	51	primrec
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	52	"is_type G (PrimT pt) = True"
360e3215f029 exception merge, cleanup, tuned kleing parents: 11372 diff changeset	53	"is_type G (RefT t) = (case t of NullT => True \| ClassT C => is_class G C)"
9346 297dcbf64526 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast oheimb parents: 8011 diff changeset	54
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	55	end

author	nipkow
	Tue, 13 Nov 2007 13:51:12 +0100
changeset 25427	8ba39d2d9d0b
parent 18551	be0705186ff5
child 35416	d8d7d1b785af
permissions	-rw-r--r--