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

4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	1	(* Title: HOL/Record.thy
16114 8d453f906e43 tuned; wenzelm parents: 15140 diff changeset	2	Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	3	*)
cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	4
22817 9dfadec17cc4 added header; wenzelm parents: 22759 diff changeset	5	header {* Extensible records with structural subtyping *}
9dfadec17cc4 added header; wenzelm parents: 22759 diff changeset	6
15131 c69542757a4d New theory header syntax. nipkow parents: 14701 diff changeset	7	theory Record
15140 322485b816ac import -> imports nipkow parents: 15131 diff changeset	8	imports Product_Type
31723 f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 25705 diff changeset	9	uses ("Tools/record.ML")
15131 c69542757a4d New theory header syntax. nipkow parents: 14701 diff changeset	10	begin
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	11
14700 2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	12	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	13	by simp
11826 2203c7f9ec40 proper setup for abstract product types; wenzelm parents: 11821 diff changeset	14
14700 2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	15	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	16	by simp
11826 2203c7f9ec40 proper setup for abstract product types; wenzelm parents: 11821 diff changeset	17
14700 2f885b7e5ba7 reimplementation of HOL records; only one type is created for schirmer parents: 14080 diff changeset	18	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	19	by simp
14080 9a50427d7165 Added split_paired_All rule for splitting variables bound by berghofe parents: 13421 diff changeset	20
25705 45a2ffc5911e replaced K_record by lambda term %x. c schirmer parents: 22817 diff changeset	21	lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
45a2ffc5911e replaced K_record by lambda term %x. c schirmer parents: 22817 diff changeset	22	by (simp add: comp_def)
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	23
22817 9dfadec17cc4 added header; wenzelm parents: 22759 diff changeset	24
11833 475f772ab643 tuned; wenzelm parents: 11826 diff changeset	25	subsection {* Concrete record syntax *}
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	26
cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	27	nonterminals
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	28	ident field_type field_types field fields update updates
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	29	syntax
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	30	"_constify" :: "id => ident" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	31	"_constify" :: "longid => ident" ("_")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	32
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	33	"_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	34	"" :: "field_type => field_types" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	35	"_field_types" :: "[field_type, field_types] => field_types" ("_,/ _")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	36	"_record_type" :: "field_types => type" ("(3'(\| _ \|'))")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	37	"_record_type_scheme" :: "[field_types, type] => type" ("(3'(\| _,/ (2... ::/ _) \|'))")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	38
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	39	"_field" :: "[ident, 'a] => field" ("(2_ =/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	40	"" :: "field => fields" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	41	"_fields" :: "[field, fields] => fields" ("_,/ _")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	42	"_record" :: "fields => 'a" ("(3'(\| _ \|'))")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	43	"_record_scheme" :: "[fields, 'a] => 'a" ("(3'(\| _,/ (2... =/ _) \|'))")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	44
10641 d1533f63c738 added "_update_name" and parse_translation; wenzelm parents: 10331 diff changeset	45	"_update_name" :: idt
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	46	"_update" :: "[ident, 'a] => update" ("(2_ :=/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	47	"" :: "update => updates" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	48	"_updates" :: "[update, updates] => updates" ("_,/ _")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	49	"_record_update" :: "['a, updates] => 'b" ("_/(3'(\| _ \|'))" [900,0] 900)
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	50
10331 7411e4659d4a more "xsymbols" syntax; wenzelm parents: 10309 diff changeset	51	syntax (xsymbols)
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	52	"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	53	"_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	54	"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	55	"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	56	"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
9729 40cfc3dd27da \<dots> syntax; wenzelm parents: 7357 diff changeset	57
31723 f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 25705 diff changeset	58	use "Tools/record.ML"
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 25705 diff changeset	59	setup Record.setup
10641 d1533f63c738 added "_update_name" and parse_translation; wenzelm parents: 10331 diff changeset	60
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	61	end

author	nipkow
	Sat, 20 Jun 2009 13:34:54 +0200
changeset 31730	d74830dc3e4a
parent 31723	f5cafe803b55
child 32743	c4e9a48bc50e
permissions	-rw-r--r--