isabelle: src/HOL/Record.thy@4c57e850e8d5 (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
15131 c69542757a4d New theory header syntax. nipkow parents: 14701 diff changeset	6	theory Record
15140 322485b816ac import -> imports nipkow parents: 15131 diff changeset	7	imports Product_Type
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 16114 diff changeset	8	uses ("Tools/record_package.ML")
15131 c69542757a4d New theory header syntax. nipkow parents: 14701 diff changeset	9	begin
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	10
14700 2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	11	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	12	by simp
11826 2203c7f9ec40 proper setup for abstract product types; wenzelm parents: 11821 diff changeset	13
14700 2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	14	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	15	by simp
11826 2203c7f9ec40 proper setup for abstract product types; wenzelm parents: 11821 diff changeset	16
14700 2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	17	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	18	by simp
14080 9a50427d7165 Added split_paired_All rule for splitting variables bound by berghofe parents: 13421 diff changeset	19
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	20
11833 475f772ab643 tuned; wenzelm parents: 11826 diff changeset	21	subsection {* Concrete record syntax *}
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	22
cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	23	nonterminals
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	24	ident field_type field_types field fields update updates
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	25	syntax
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	26	"_constify" :: "id => ident" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	27	"_constify" :: "longid => ident" ("_")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	28
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	29	"_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	30	"" :: "field_type => field_types" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	31	"_field_types" :: "[field_type, field_types] => field_types" ("_,/ _")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	32	"_record_type" :: "field_types => type" ("(3'(\| _ \|'))")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	33	"_record_type_scheme" :: "[field_types, type] => type" ("(3'(\| _,/ (2... ::/ _) \|'))")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	34
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	35	"_field" :: "[ident, 'a] => field" ("(2_ =/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	36	"" :: "field => fields" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	37	"_fields" :: "[field, fields] => fields" ("_,/ _")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	38	"_record" :: "fields => 'a" ("(3'(\| _ \|'))")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	39	"_record_scheme" :: "[fields, 'a] => 'a" ("(3'(\| _,/ (2... =/ _) \|'))")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	40
10641 d1533f63c738 added "_update_name" and parse_translation; wenzelm parents: 10331 diff changeset	41	"_update_name" :: idt
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	42	"_update" :: "[ident, 'a] => update" ("(2_ :=/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	43	"" :: "update => updates" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	44	"_updates" :: "[update, updates] => updates" ("_,/ _")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	45	"_record_update" :: "['a, updates] => 'b" ("_/(3'(\| _ \|'))" [900,0] 900)
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	46
10331 7411e4659d4a more "xsymbols" syntax; wenzelm parents: 10309 diff changeset	47	syntax (xsymbols)
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	48	"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	49	"_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	50	"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	51	"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	52	"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
9729 40cfc3dd27da \<dots> syntax; wenzelm parents: 7357 diff changeset	53
16114 8d453f906e43 tuned; wenzelm parents: 15140 diff changeset	54	use "Tools/record_package.ML"
8d453f906e43 tuned; wenzelm parents: 15140 diff changeset	55	setup RecordPackage.setup
10641 d1533f63c738 added "_update_name" and parse_translation; wenzelm parents: 10331 diff changeset	56
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	57	end
14700 2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	58

author	wenzelm
	Wed, 26 Jul 2006 00:44:44 +0200
changeset 20207	4c57e850e8d5
parent 17957	d31acb64aa9a
child 21226	a607ae87ee81
permissions	-rw-r--r--