isabelle: src/HOL/Record.thy@20f43e0e0958 (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
25705 45a2ffc5911e replaced K_record by lambda term %x. c schirmer parents: 22817 diff changeset	22	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	23	by (simp add: comp_def)
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	24
22817 9dfadec17cc4 added header; wenzelm parents: 22759 diff changeset	25
11833 475f772ab643 tuned; wenzelm parents: 11826 diff changeset	26	subsection {* Concrete record syntax *}
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	27
cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	28	nonterminals
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	29	ident field_type field_types field fields update updates
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	30	syntax
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	31	"_constify" :: "id => ident" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	32	"_constify" :: "longid => ident" ("_")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	33
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	34	"_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	35	"" :: "field_type => field_types" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	36	"_field_types" :: "[field_type, field_types] => field_types" ("_,/ _")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	37	"_record_type" :: "field_types => type" ("(3'(\| _ \|'))")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	38	"_record_type_scheme" :: "[field_types, type] => type" ("(3'(\| _,/ (2... ::/ _) \|'))")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	39
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	40	"_field" :: "[ident, 'a] => field" ("(2_ =/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	41	"" :: "field => fields" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	42	"_fields" :: "[field, fields] => fields" ("_,/ _")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	43	"_record" :: "fields => 'a" ("(3'(\| _ \|'))")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	44	"_record_scheme" :: "[fields, 'a] => 'a" ("(3'(\| _,/ (2... =/ _) \|'))")
5198 b1adae4f8b90 added type and update syntax; wenzelm parents: 5032 diff changeset	45
10641 d1533f63c738 added "_update_name" and parse_translation; wenzelm parents: 10331 diff changeset	46	"_update_name" :: idt
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	47	"_update" :: "[ident, 'a] => update" ("(2_ :=/ _)")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	48	"" :: "update => updates" ("_")
ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	49	"_updates" :: "[update, updates] => updates" ("_,/ _")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	50	"_record_update" :: "['a, updates] => 'b" ("_/(3'(\| _ \|'))" [900,0] 900)
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	51
10331 7411e4659d4a more "xsymbols" syntax; wenzelm parents: 10309 diff changeset	52	syntax (xsymbols)
11821 ad32c92435db abstract product types; wenzelm parents: 11489 diff changeset	53	"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)")
10093 44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	54	"_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	55	"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	56	"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input"); wenzelm parents: 9729 diff changeset	57	"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
9729 40cfc3dd27da \<dots> syntax; wenzelm parents: 7357 diff changeset	58
16114 8d453f906e43 tuned; wenzelm parents: 15140 diff changeset	59	use "Tools/record_package.ML"
8d453f906e43 tuned; wenzelm parents: 15140 diff changeset	60	setup RecordPackage.setup
10641 d1533f63c738 added "_update_name" and parse_translation; wenzelm parents: 10331 diff changeset	61
4870 cc36acb5b114 Extensible records with structural subtyping in HOL. See wenzelm parents: diff changeset	62	end

author	wenzelm
	Sun, 30 Nov 2008 14:43:29 +0100
changeset 28917	20f43e0e0958
parent 25705	45a2ffc5911e
child 31723	f5cafe803b55
permissions	-rw-r--r--