isabelle: src/HOL/Record.thy@b2267a9e9e28 (annotated)

4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	1	(* Title: HOL/Record.thy
cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	2	ID: $Id$
16114 8d453f906e43 tuned; wenzelm parents: 15140 diff changeset	3	Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	4	*)
cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	5
22817 9dfadec17cc4 added header; wenzelm parents: 22759 diff changeset	6	header {* Extensible records with structural subtyping *}
9dfadec17cc4 added header; wenzelm parents: 22759 diff changeset	7
15131 c69542757a4d New theory header syntax. nipkow parents: 14701 diff changeset	8	theory Record
15140 322485b816ac import -> imports nipkow parents: 15131 diff changeset	9	imports Product_Type
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 16114 diff changeset	10	uses ("Tools/record_package.ML")
15131 c69542757a4d New theory header syntax. nipkow parents: 14701 diff changeset	11	begin
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	12
14700 2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	13	lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	14	by simp
11826 2203c7f9ec40 proper setup for abstract product types; wenzelm parents: 11821 diff changeset	15
14700 2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	16	lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	17	by simp
11826 2203c7f9ec40 proper setup for abstract product types; wenzelm parents: 11821 diff changeset	18
14700 2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	19	lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	20	by simp
14080 9a50427d7165 Added split_paired_All rule for splitting variables bound by berghofe parents: 13421 diff changeset	21
22759 e4a3f49eb924 reverted to classical syntax for K_record haftmann parents: 22744 diff changeset	22	constdefs
22744 5cbe966d67a2 Isar definitions are now added explicitly to code theorem table haftmann parents: 21226 diff changeset	23	K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
22759 e4a3f49eb924 reverted to classical syntax for K_record haftmann parents: 22744 diff changeset	24	K_record_apply [simp, code func]: "K_record c x \<equiv> c"
21226 a607ae87ee81 field-update in records is generalised to take a function on the field schirmer parents: 17957 diff changeset	25
a607ae87ee81 field-update in records is generalised to take a function on the field schirmer parents: 17957 diff changeset	26	lemma K_record_comp [simp]: "(K_record c \<circ> f) = K_record c"
a607ae87ee81 field-update in records is generalised to take a function on the field schirmer parents: 17957 diff changeset	27	by (rule ext) (simp add: K_record_apply comp_def)
a607ae87ee81 field-update in records is generalised to take a function on the field schirmer parents: 17957 diff changeset	28
a607ae87ee81 field-update in records is generalised to take a function on the field schirmer parents: 17957 diff changeset	29	lemma K_record_cong [cong]: "K_record c x = K_record c x"
a607ae87ee81 field-update in records is generalised to take a function on the field schirmer parents: 17957 diff changeset	30	by (rule refl)
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	31
22817 9dfadec17cc4 added header; wenzelm parents: 22759 diff changeset	32
11833 475f772ab643 tuned; wenzelm parents: 11826 diff changeset	33	subsection {* Concrete record syntax *}
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	34
cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	35	nonterminals
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	36	ident field_type field_types field fields update updates
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	37	syntax
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	38	"_constify" :: "id => ident" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	39	"_constify" :: "longid => ident" ("_")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	40
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	41	"_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	42	"" :: "field_type => field_types" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	43	"_field_types" :: "[field_type, field_types] => field_types" ("_,/ _")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	44	"_record_type" :: "field_types => type" ("(3'(\| _ \|'))")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	45	"_record_type_scheme" :: "[field_types, type] => type" ("(3'(\| _,/ (2... ::/ _) \|'))")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	46
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	47	"_field" :: "[ident, 'a] => field" ("(2_ =/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	48	"" :: "field => fields" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	49	"_fields" :: "[field, fields] => fields" ("_,/ _")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	50	"_record" :: "fields => 'a" ("(3'(\| _ \|'))")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	51	"_record_scheme" :: "[fields, 'a] => 'a" ("(3'(\| _,/ (2... =/ _) \|'))")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	52
10641 d1533f63c738 added "_update_name" and parse_translation; wenzelm parents: 10331 diff changeset	53	"_update_name" :: idt
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	54	"_update" :: "[ident, 'a] => update" ("(2_ :=/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	55	"" :: "update => updates" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	56	"_updates" :: "[update, updates] => updates" ("_,/ _")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	57	"_record_update" :: "['a, updates] => 'b" ("_/(3'(\| _ \|'))" [900,0] 900)
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	58
10331 7411e4659d4a more "xsymbols" syntax; wenzelm parents: 10309 diff changeset	59	syntax (xsymbols)
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	60	"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	61	"_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	62	"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	63	"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	64	"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
9729 40cfc3dd27da \<dots> syntax; wenzelm parents: 7357 diff changeset	65
16114 8d453f906e43 tuned; wenzelm parents: 15140 diff changeset	66	use "Tools/record_package.ML"
8d453f906e43 tuned; wenzelm parents: 15140 diff changeset	67	setup RecordPackage.setup
10641 d1533f63c738 added "_update_name" and parse_translation; wenzelm parents: 10331 diff changeset	68
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	69	end

author	wenzelm
	Thu, 21 Jun 2007 15:42:12 +0200
changeset 23458	b2267a9e9e28
parent 22817	9dfadec17cc4
child 25705	45a2ffc5911e
permissions	-rw-r--r--