author | tsewell@rubicon.NSW.bigpond.net.au |
Thu, 27 Aug 2009 00:40:53 +1000 | |
changeset 32743 | c4e9a48bc50e |
parent 31723 | f5cafe803b55 |
child 32744 | 50406c4951d9 |
permissions | -rw-r--r-- |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Record.thy |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
2 |
ID: $Id: Record.thy,v 1.33 2007/12/19 15:32:12 schirmer Exp $ |
16114 | 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 | 6 |
header {* Extensible records with structural subtyping *} |
7 |
||
15131 | 8 |
theory Record |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
9 |
imports Product_Type IsTuple |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
10 |
uses ("Tools/record_package.ML") |
15131 | 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 | 15 |
|
25705 | 16 |
lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" |
17 |
by (simp add: comp_def) |
|
11821 | 18 |
|
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
19 |
lemma meta_iffD2: |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
20 |
"\<lbrakk> PROP P \<equiv> PROP Q; PROP Q \<rbrakk> \<Longrightarrow> PROP P" |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
21 |
by simp |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
22 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
23 |
lemma o_eq_dest_lhs: |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
24 |
"a o b = c \<Longrightarrow> a (b v) = c v" |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
25 |
by clarsimp |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
26 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
27 |
lemma id_o_refl: |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
28 |
"id o f = f o id" |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
29 |
by simp |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
30 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
31 |
lemma o_eq_id_dest: |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
32 |
"a o b = id o c \<Longrightarrow> a (b v) = c v" |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
33 |
by clarsimp |
22817 | 34 |
|
11833 | 35 |
subsection {* Concrete record syntax *} |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
36 |
|
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
37 |
nonterminals |
5198 | 38 |
ident field_type field_types field fields update updates |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
39 |
syntax |
11821 | 40 |
"_constify" :: "id => ident" ("_") |
41 |
"_constify" :: "longid => ident" ("_") |
|
5198 | 42 |
|
11821 | 43 |
"_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)") |
44 |
"" :: "field_type => field_types" ("_") |
|
45 |
"_field_types" :: "[field_type, field_types] => field_types" ("_,/ _") |
|
46 |
"_record_type" :: "field_types => type" ("(3'(| _ |'))") |
|
10093 | 47 |
"_record_type_scheme" :: "[field_types, type] => type" ("(3'(| _,/ (2... ::/ _) |'))") |
5198 | 48 |
|
11821 | 49 |
"_field" :: "[ident, 'a] => field" ("(2_ =/ _)") |
50 |
"" :: "field => fields" ("_") |
|
51 |
"_fields" :: "[field, fields] => fields" ("_,/ _") |
|
52 |
"_record" :: "fields => 'a" ("(3'(| _ |'))") |
|
10093 | 53 |
"_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2... =/ _) |'))") |
5198 | 54 |
|
10641 | 55 |
"_update_name" :: idt |
11821 | 56 |
"_update" :: "[ident, 'a] => update" ("(2_ :=/ _)") |
57 |
"" :: "update => updates" ("_") |
|
58 |
"_updates" :: "[update, updates] => updates" ("_,/ _") |
|
10093 | 59 |
"_record_update" :: "['a, updates] => 'b" ("_/(3'(| _ |'))" [900,0] 900) |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
60 |
|
10331 | 61 |
syntax (xsymbols) |
11821 | 62 |
"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)") |
10093 | 63 |
"_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
64 |
"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
|
65 |
"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
|
66 |
"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
|
9729 | 67 |
|
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
68 |
use "Tools/record_package.ML" |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
69 |
setup RecordPackage.setup |
10641 | 70 |
|
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
71 |
end |