author | haftmann |
Fri, 22 Jan 2010 13:38:29 +0100 | |
changeset 34945 | 478f31081a78 |
parent 34151 | 8d57ce46b3f7 |
child 35132 | d137efecf793 |
permissions | -rw-r--r-- |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Record.thy |
32763 | 2 |
Author: Wolfgang Naraschewski, TU Muenchen |
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
Author: Norbert Schirmer, TU Muenchen |
|
5 |
Author: Thomas Sewell, NICTA |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
6 |
Author: Florian Haftmann, TU Muenchen |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
7 |
*) |
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
8 |
|
22817 | 9 |
header {* Extensible records with structural subtyping *} |
10 |
||
15131 | 11 |
theory Record |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
12 |
imports Datatype |
32744
50406c4951d9
Record patch imported and working.
Thomas Sewell <tsewell@nicta.com.au>
parents:
32743
diff
changeset
|
13 |
uses ("Tools/record.ML") |
15131 | 14 |
begin |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
15 |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
16 |
subsection {* Introduction *} |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
17 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
18 |
text {* |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
19 |
Records are isomorphic to compound tuple types. To implement |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
20 |
efficient records, we make this isomorphism explicit. Consider the |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
21 |
record access/update simplification @{text "alpha (beta_update f |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
22 |
rec) = alpha rec"} for distinct fields alpha and beta of some record |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
23 |
rec with n fields. There are @{text "n ^ 2"} such theorems, which |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
24 |
prohibits storage of all of them for large n. The rules can be |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
25 |
proved on the fly by case decomposition and simplification in O(n) |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
26 |
time. By creating O(n) isomorphic-tuple types while defining the |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
27 |
record, however, we can prove the access/update simplification in |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
28 |
@{text "O(log(n)^2)"} time. |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
29 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
30 |
The O(n) cost of case decomposition is not because O(n) steps are |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
31 |
taken, but rather because the resulting rule must contain O(n) new |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
32 |
variables and an O(n) size concrete record construction. To sidestep |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
33 |
this cost, we would like to avoid case decomposition in proving |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
34 |
access/update theorems. |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
35 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
36 |
Record types are defined as isomorphic to tuple types. For instance, |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
37 |
a record type with fields @{text "'a"}, @{text "'b"}, @{text "'c"} |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
38 |
and @{text "'d"} might be introduced as isomorphic to @{text "'a \<times> |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
39 |
('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to @{text "('a \<times> |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
40 |
'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to the |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
41 |
underlying type then using O(log(n)) fst or snd operations. |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
42 |
Updators can be defined similarly, if we introduce a @{text |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
43 |
"fst_update"} and @{text "snd_update"} function. Furthermore, we can |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
44 |
prove the access/update theorem in O(log(n)) steps by using simple |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
45 |
rewrites on fst, snd, @{text "fst_update"} and @{text "snd_update"}. |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
46 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
47 |
The catch is that, although O(log(n)) steps were taken, the |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
48 |
underlying type we converted to is a tuple tree of size |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
49 |
O(n). Processing this term type wastes performance. We avoid this |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
50 |
for large n by taking each subtree of size K and defining a new type |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
51 |
isomorphic to that tuple subtree. A record can now be defined as |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
52 |
isomorphic to a tuple tree of these O(n/K) new types, or, if @{text |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
53 |
"n > K*K"}, we can repeat the process, until the record can be |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
54 |
defined in terms of a tuple tree of complexity less than the |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
55 |
constant K. |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
56 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
57 |
If we prove the access/update theorem on this type with the |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
58 |
analagous steps to the tuple tree, we consume @{text "O(log(n)^2)"} |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
59 |
time as the intermediate terms are @{text "O(log(n))"} in size and |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
60 |
the types needed have size bounded by K. To enable this analagous |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
61 |
traversal, we define the functions seen below: @{text |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
62 |
"iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"} |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
63 |
and @{text "iso_tuple_snd_update"}. These functions generalise tuple |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
64 |
operations by taking a parameter that encapsulates a tuple |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
65 |
isomorphism. The rewrites needed on these functions now need an |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
66 |
additional assumption which is that the isomorphism works. |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
67 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
68 |
These rewrites are typically used in a structured way. They are here |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
69 |
presented as the introduction rule @{text "isomorphic_tuple.intros"} |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
70 |
rather than as a rewrite rule set. The introduction form is an |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
71 |
optimisation, as net matching can be performed at one term location |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
72 |
for each step rather than the simplifier searching the term for |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
73 |
possible pattern matches. The rule set is used as it is viewed |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
74 |
outside the locale, with the locale assumption (that the isomorphism |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
75 |
is valid) left as a rule assumption. All rules are structured to aid |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
76 |
net matching, using either a point-free form or an encapsulating |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
77 |
predicate. |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
78 |
*} |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
79 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
80 |
subsection {* Operators and lemmas for types isomorphic to tuples *} |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
81 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
82 |
datatype ('a, 'b, 'c) tuple_isomorphism = Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
83 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
84 |
primrec repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
85 |
"repr (Tuple_Isomorphism r a) = r" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
86 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
87 |
primrec abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
88 |
"abst (Tuple_Isomorphism r a) = a" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
89 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
90 |
definition iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
91 |
"iso_tuple_fst isom = fst \<circ> repr isom" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
92 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
93 |
definition iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
94 |
"iso_tuple_snd isom = snd \<circ> repr isom" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
95 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
96 |
definition iso_tuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
97 |
"iso_tuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
98 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
99 |
definition iso_tuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
100 |
"iso_tuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
101 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
102 |
definition iso_tuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
103 |
"iso_tuple_cons isom = curry (abst isom)" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
104 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
105 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
106 |
subsection {* Logical infrastructure for records *} |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
107 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
108 |
definition iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
109 |
"iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
110 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
111 |
definition iso_tuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
112 |
"iso_tuple_update_accessor_cong_assist upd acc \<longleftrightarrow> |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
113 |
(\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v) \<and> (\<forall>v. upd id v = v)" |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
114 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
115 |
definition iso_tuple_update_accessor_eq_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
116 |
"iso_tuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow> |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
117 |
upd f v = v' \<and> acc v = x \<and> iso_tuple_update_accessor_cong_assist upd acc" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
118 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
119 |
lemma update_accessor_congruence_foldE: |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
120 |
assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
121 |
and r: "r = r'" and v: "acc r' = v'" |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
122 |
and f: "\<And>v. v' = v \<Longrightarrow> f v = f' v" |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
123 |
shows "upd f r = upd f' r'" |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
124 |
using uac r v [symmetric] |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
125 |
apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'") |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
126 |
apply (simp add: iso_tuple_update_accessor_cong_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
127 |
apply (simp add: f) |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
128 |
done |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
129 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
130 |
lemma update_accessor_congruence_unfoldE: |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
131 |
"iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> r = r' \<Longrightarrow> acc r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
132 |
\<Longrightarrow> upd f r = upd f' r'" |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
133 |
apply (erule(2) update_accessor_congruence_foldE) |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
134 |
apply simp |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
135 |
done |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
136 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
137 |
lemma iso_tuple_update_accessor_cong_assist_id: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
138 |
"iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
139 |
by rule (simp add: iso_tuple_update_accessor_cong_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
140 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
141 |
lemma update_accessor_noopE: |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
142 |
assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
143 |
and acc: "f (acc x) = acc x" |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
144 |
shows "upd f x = x" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
145 |
using uac by (simp add: acc iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def] |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
146 |
cong: update_accessor_congruence_unfoldE [OF uac]) |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
147 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
148 |
lemma update_accessor_noop_compE: |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
149 |
assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
150 |
assumes acc: "f (acc x) = acc x" |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
151 |
shows "upd (g \<circ> f) x = upd g x" |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
152 |
by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac]) |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
153 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
154 |
lemma update_accessor_cong_assist_idI: |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
155 |
"iso_tuple_update_accessor_cong_assist id id" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
156 |
by (simp add: iso_tuple_update_accessor_cong_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
157 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
158 |
lemma update_accessor_cong_assist_triv: |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
159 |
"iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> iso_tuple_update_accessor_cong_assist upd acc" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
160 |
by assumption |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
161 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
162 |
lemma update_accessor_accessor_eqE: |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
163 |
"iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> acc v = x" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
164 |
by (simp add: iso_tuple_update_accessor_eq_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
165 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
166 |
lemma update_accessor_updator_eqE: |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
167 |
"iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> upd f v = v'" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
168 |
by (simp add: iso_tuple_update_accessor_eq_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
169 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
170 |
lemma iso_tuple_update_accessor_eq_assist_idI: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
171 |
"v' = f v \<Longrightarrow> iso_tuple_update_accessor_eq_assist id id v f v' v" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
172 |
by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
173 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
174 |
lemma iso_tuple_update_accessor_eq_assist_triv: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
175 |
"iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> iso_tuple_update_accessor_eq_assist upd acc v f v' x" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
176 |
by assumption |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
177 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
178 |
lemma iso_tuple_update_accessor_cong_from_eq: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
179 |
"iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> iso_tuple_update_accessor_cong_assist upd acc" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
180 |
by (simp add: iso_tuple_update_accessor_eq_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
181 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
182 |
lemma iso_tuple_surjective_proof_assistI: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
183 |
"f x = y \<Longrightarrow> iso_tuple_surjective_proof_assist x y f" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
184 |
by (simp add: iso_tuple_surjective_proof_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
185 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
186 |
lemma iso_tuple_surjective_proof_assist_idE: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
187 |
"iso_tuple_surjective_proof_assist x y id \<Longrightarrow> x = y" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
188 |
by (simp add: iso_tuple_surjective_proof_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
189 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
190 |
locale isomorphic_tuple = |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
191 |
fixes isom :: "('a, 'b, 'c) tuple_isomorphism" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
192 |
assumes repr_inv: "\<And>x. abst isom (repr isom x) = x" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
193 |
assumes abst_inv: "\<And>y. repr isom (abst isom y) = y" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
194 |
begin |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
195 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
196 |
lemma repr_inj: |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
197 |
"repr isom x = repr isom y \<longleftrightarrow> x = y" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
198 |
by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"] simp add: repr_inv) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
199 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
200 |
lemma abst_inj: |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
201 |
"abst isom x = abst isom y \<longleftrightarrow> x = y" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
202 |
by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"] simp add: abst_inv) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
203 |
|
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
204 |
lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
205 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
206 |
lemma iso_tuple_access_update_fst_fst: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
207 |
"f o h g = j o f \<Longrightarrow> |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
208 |
(f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
209 |
= j o (f o iso_tuple_fst isom)" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
210 |
by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
211 |
intro!: ext elim!: o_eq_elim) |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
212 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
213 |
lemma iso_tuple_access_update_snd_snd: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
214 |
"f o h g = j o f \<Longrightarrow> |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
215 |
(f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
216 |
= j o (f o iso_tuple_snd isom)" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
217 |
by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
218 |
intro!: ext elim!: o_eq_elim) |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
219 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
220 |
lemma iso_tuple_access_update_fst_snd: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
221 |
"(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
222 |
= id o (f o iso_tuple_fst isom)" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
223 |
by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
224 |
intro!: ext elim!: o_eq_elim) |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
225 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
226 |
lemma iso_tuple_access_update_snd_fst: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
227 |
"(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
228 |
= id o (f o iso_tuple_snd isom)" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
229 |
by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
230 |
intro!: ext elim!: o_eq_elim) |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
231 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
232 |
lemma iso_tuple_update_swap_fst_fst: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
233 |
"h f o j g = j g o h f \<Longrightarrow> |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
234 |
(iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
235 |
= (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
236 |
by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
237 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
238 |
lemma iso_tuple_update_swap_snd_snd: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
239 |
"h f o j g = j g o h f \<Longrightarrow> |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
240 |
(iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
241 |
= (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
242 |
by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
243 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
244 |
lemma iso_tuple_update_swap_fst_snd: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
245 |
"(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
246 |
= (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
247 |
by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
248 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
249 |
lemma iso_tuple_update_swap_snd_fst: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
250 |
"(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
251 |
= (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
252 |
by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
253 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
254 |
lemma iso_tuple_update_compose_fst_fst: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
255 |
"h f o j g = k (f o g) \<Longrightarrow> |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
256 |
(iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
257 |
= (iso_tuple_fst_update isom o k) (f o g)" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
258 |
by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
259 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
260 |
lemma iso_tuple_update_compose_snd_snd: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
261 |
"h f o j g = k (f o g) \<Longrightarrow> |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
262 |
(iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
263 |
= (iso_tuple_snd_update isom o k) (f o g)" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
264 |
by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
265 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
266 |
lemma iso_tuple_surjective_proof_assist_step: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
267 |
"iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \<Longrightarrow> |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
268 |
iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
269 |
\<Longrightarrow> iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
270 |
by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
271 |
iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
272 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
273 |
lemma iso_tuple_fst_update_accessor_cong_assist: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
274 |
assumes "iso_tuple_update_accessor_cong_assist f g" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
275 |
shows "iso_tuple_update_accessor_cong_assist (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
276 |
proof - |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
277 |
from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
278 |
with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
279 |
iso_tuple_fst_update_def iso_tuple_fst_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
280 |
qed |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
281 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
282 |
lemma iso_tuple_snd_update_accessor_cong_assist: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
283 |
assumes "iso_tuple_update_accessor_cong_assist f g" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
284 |
shows "iso_tuple_update_accessor_cong_assist (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
285 |
proof - |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
286 |
from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
287 |
with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
288 |
iso_tuple_snd_update_def iso_tuple_snd_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
289 |
qed |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
290 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
291 |
lemma iso_tuple_fst_update_accessor_eq_assist: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
292 |
assumes "iso_tuple_update_accessor_eq_assist f g a u a' v" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
293 |
shows "iso_tuple_update_accessor_eq_assist (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
294 |
(iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
295 |
proof - |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
296 |
from assms have "f id = id" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
297 |
by (auto simp add: iso_tuple_update_accessor_eq_assist_def intro: iso_tuple_update_accessor_cong_assist_id) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
298 |
with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
299 |
iso_tuple_fst_update_def iso_tuple_fst_def iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
300 |
qed |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
301 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
302 |
lemma iso_tuple_snd_update_accessor_eq_assist: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
303 |
assumes "iso_tuple_update_accessor_eq_assist f g b u b' v" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
304 |
shows "iso_tuple_update_accessor_eq_assist (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
305 |
(iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
306 |
proof - |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
307 |
from assms have "f id = id" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
308 |
by (auto simp add: iso_tuple_update_accessor_eq_assist_def intro: iso_tuple_update_accessor_cong_assist_id) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
309 |
with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
310 |
iso_tuple_snd_update_def iso_tuple_snd_def iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
311 |
qed |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
312 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
313 |
lemma iso_tuple_cons_conj_eqI: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
314 |
"a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow> |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
315 |
iso_tuple_cons isom a b = iso_tuple_cons isom c d \<and> P \<longleftrightarrow> Q" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
316 |
by (clarsimp simp: iso_tuple_cons_def simps) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
317 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
318 |
lemmas intros = |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
319 |
iso_tuple_access_update_fst_fst |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
320 |
iso_tuple_access_update_snd_snd |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
321 |
iso_tuple_access_update_fst_snd |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
322 |
iso_tuple_access_update_snd_fst |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
323 |
iso_tuple_update_swap_fst_fst |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
324 |
iso_tuple_update_swap_snd_snd |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
325 |
iso_tuple_update_swap_fst_snd |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
326 |
iso_tuple_update_swap_snd_fst |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
327 |
iso_tuple_update_compose_fst_fst |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
328 |
iso_tuple_update_compose_snd_snd |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
329 |
iso_tuple_surjective_proof_assist_step |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
330 |
iso_tuple_fst_update_accessor_eq_assist |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
331 |
iso_tuple_snd_update_accessor_eq_assist |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
332 |
iso_tuple_fst_update_accessor_cong_assist |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
333 |
iso_tuple_snd_update_accessor_cong_assist |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
334 |
iso_tuple_cons_conj_eqI |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
335 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
336 |
end |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
337 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
338 |
lemma isomorphic_tuple_intro: |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
339 |
fixes repr abst |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
340 |
assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y" |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
341 |
and abst_inv: "\<And>z. repr (abst z) = z" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
342 |
assumes v: "v \<equiv> Tuple_Isomorphism repr abst" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
343 |
shows "isomorphic_tuple v" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
344 |
proof |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
345 |
have "\<And>x. repr (abst (repr x)) = repr x" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
346 |
by (simp add: abst_inv) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
347 |
then show "\<And>x. Record.abst v (Record.repr v x) = x" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
348 |
by (simp add: v repr_inj) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
349 |
show P: "\<And>y. Record.repr v (Record.abst v y) = y" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
350 |
by (simp add: v) (fact abst_inv) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
351 |
qed |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
352 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
353 |
definition |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
354 |
"tuple_iso_tuple \<equiv> Tuple_Isomorphism id id" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
355 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
356 |
lemma tuple_iso_tuple: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
357 |
"isomorphic_tuple tuple_iso_tuple" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
358 |
by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
359 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
360 |
lemma refl_conj_eq: |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
361 |
"Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R" |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
362 |
by simp |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
363 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
364 |
lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
365 |
by simp |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
366 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
367 |
lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
368 |
by simp |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
369 |
|
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14080
diff
changeset
|
370 |
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
|
371 |
by simp |
11826 | 372 |
|
25705 | 373 |
lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" |
374 |
by (simp add: comp_def) |
|
11821 | 375 |
|
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
376 |
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
|
377 |
"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
|
378 |
by clarsimp |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
379 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
380 |
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
|
381 |
"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
|
382 |
by clarsimp |
22817 | 383 |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
384 |
|
11833 | 385 |
subsection {* Concrete record syntax *} |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
386 |
|
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
387 |
nonterminals |
5198 | 388 |
ident field_type field_types field fields update updates |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
389 |
syntax |
11821 | 390 |
"_constify" :: "id => ident" ("_") |
391 |
"_constify" :: "longid => ident" ("_") |
|
5198 | 392 |
|
11821 | 393 |
"_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)") |
394 |
"" :: "field_type => field_types" ("_") |
|
395 |
"_field_types" :: "[field_type, field_types] => field_types" ("_,/ _") |
|
396 |
"_record_type" :: "field_types => type" ("(3'(| _ |'))") |
|
10093 | 397 |
"_record_type_scheme" :: "[field_types, type] => type" ("(3'(| _,/ (2... ::/ _) |'))") |
5198 | 398 |
|
11821 | 399 |
"_field" :: "[ident, 'a] => field" ("(2_ =/ _)") |
400 |
"" :: "field => fields" ("_") |
|
401 |
"_fields" :: "[field, fields] => fields" ("_,/ _") |
|
402 |
"_record" :: "fields => 'a" ("(3'(| _ |'))") |
|
10093 | 403 |
"_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2... =/ _) |'))") |
5198 | 404 |
|
10641 | 405 |
"_update_name" :: idt |
11821 | 406 |
"_update" :: "[ident, 'a] => update" ("(2_ :=/ _)") |
407 |
"" :: "update => updates" ("_") |
|
408 |
"_updates" :: "[update, updates] => updates" ("_,/ _") |
|
10093 | 409 |
"_record_update" :: "['a, updates] => 'b" ("_/(3'(| _ |'))" [900,0] 900) |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
410 |
|
10331 | 411 |
syntax (xsymbols) |
11821 | 412 |
"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)") |
10093 | 413 |
"_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
414 |
"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
|
415 |
"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
|
416 |
"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
|
9729 | 417 |
|
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
418 |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
419 |
subsection {* Record package *} |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
420 |
|
32744
50406c4951d9
Record patch imported and working.
Thomas Sewell <tsewell@nicta.com.au>
parents:
32743
diff
changeset
|
421 |
use "Tools/record.ML" |
50406c4951d9
Record patch imported and working.
Thomas Sewell <tsewell@nicta.com.au>
parents:
32743
diff
changeset
|
422 |
setup Record.setup |
10641 | 423 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
424 |
hide (open) const Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
425 |
iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
426 |
iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
427 |
iso_tuple_update_accessor_eq_assist tuple_iso_tuple |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
428 |
|
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
429 |
end |