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