author | wenzelm |
Mon, 28 Dec 2015 01:26:34 +0100 | |
changeset 61944 | 5d06ecfdb472 |
parent 61799 | 4cf66f21b764 |
child 61955 | e96292f32c3c |
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 |
|
60758 | 9 |
section \<open>Extensible records with structural subtyping\<close> |
22817 | 10 |
|
15131 | 11 |
theory Record |
56048
d311c6377e08
moved 'Quickcheck_Narrowing' further down the theory graph
blanchet
parents:
56047
diff
changeset
|
12 |
imports Quickcheck_Exhaustive |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
44922
diff
changeset
|
13 |
keywords "record" :: thy_decl |
15131 | 14 |
begin |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
15 |
|
60758 | 16 |
subsection \<open>Introduction\<close> |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
17 |
|
60758 | 18 |
text \<open> |
33595
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 |
61799 | 21 |
record access/update simplification \<open>alpha (beta_update f |
22 |
rec) = alpha rec\<close> for distinct fields alpha and beta of some record |
|
23 |
rec with n fields. There are \<open>n ^ 2\<close> such theorems, which |
|
33595
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 |
61799 | 28 |
\<open>O(log(n)^2)\<close> time. |
33595
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, |
61799 | 37 |
a record type with fields \<open>'a\<close>, \<open>'b\<close>, \<open>'c\<close> |
38 |
and \<open>'d\<close> might be introduced as isomorphic to \<open>'a \<times> |
|
39 |
('b \<times> ('c \<times> 'd))\<close>. If we balance the tuple tree to \<open>('a \<times> |
|
40 |
'b) \<times> ('c \<times> 'd)\<close> then accessors can be defined by converting to the |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
41 |
underlying type then using O(log(n)) fst or snd operations. |
61799 | 42 |
Updators can be defined similarly, if we introduce a \<open>fst_update\<close> and \<open>snd_update\<close> function. Furthermore, we can |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
43 |
prove the access/update theorem in O(log(n)) steps by using simple |
61799 | 44 |
rewrites on fst, snd, \<open>fst_update\<close> and \<open>snd_update\<close>. |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
45 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
46 |
The catch is that, although O(log(n)) steps were taken, the |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
47 |
underlying type we converted to is a tuple tree of size |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
48 |
O(n). Processing this term type wastes performance. We avoid this |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
49 |
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
|
50 |
isomorphic to that tuple subtree. A record can now be defined as |
61799 | 51 |
isomorphic to a tuple tree of these O(n/K) new types, or, if \<open>n > K*K\<close>, we can repeat the process, until the record can be |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
52 |
defined in terms of a tuple tree of complexity less than the |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
53 |
constant K. |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
54 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
55 |
If we prove the access/update theorem on this type with the |
61799 | 56 |
analogous steps to the tuple tree, we consume \<open>O(log(n)^2)\<close> |
57 |
time as the intermediate terms are \<open>O(log(n))\<close> in size and |
|
44922 | 58 |
the types needed have size bounded by K. To enable this analogous |
61799 | 59 |
traversal, we define the functions seen below: \<open>iso_tuple_fst\<close>, \<open>iso_tuple_snd\<close>, \<open>iso_tuple_fst_update\<close> |
60 |
and \<open>iso_tuple_snd_update\<close>. These functions generalise tuple |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
61 |
operations by taking a parameter that encapsulates a tuple |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
62 |
isomorphism. The rewrites needed on these functions now need an |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
63 |
additional assumption which is that the isomorphism works. |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
64 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
65 |
These rewrites are typically used in a structured way. They are here |
61799 | 66 |
presented as the introduction rule \<open>isomorphic_tuple.intros\<close> |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
67 |
rather than as a rewrite rule set. The introduction form is an |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
68 |
optimisation, as net matching can be performed at one term location |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
69 |
for each step rather than the simplifier searching the term for |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
70 |
possible pattern matches. The rule set is used as it is viewed |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
71 |
outside the locale, with the locale assumption (that the isomorphism |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
72 |
is valid) left as a rule assumption. All rules are structured to aid |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
73 |
net matching, using either a point-free form or an encapsulating |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
74 |
predicate. |
60758 | 75 |
\<close> |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
76 |
|
60758 | 77 |
subsection \<open>Operators and lemmas for types isomorphic to tuples\<close> |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
78 |
|
58310 | 79 |
datatype (dead 'a, dead 'b, dead 'c) tuple_isomorphism = |
35132 | 80 |
Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
81 |
|
35132 | 82 |
primrec |
83 |
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
|
84 |
"repr (Tuple_Isomorphism r a) = r" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
85 |
|
35132 | 86 |
primrec |
87 |
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 |
|
35132 | 90 |
definition |
91 |
iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
92 |
"iso_tuple_fst isom = fst \<circ> repr isom" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
93 |
|
35132 | 94 |
definition |
95 |
iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
96 |
"iso_tuple_snd isom = snd \<circ> repr isom" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
97 |
|
35132 | 98 |
definition |
99 |
iso_tuple_fst_update :: |
|
100 |
"('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
101 |
"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
|
102 |
|
35132 | 103 |
definition |
104 |
iso_tuple_snd_update :: |
|
105 |
"('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
106 |
"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
|
107 |
|
35132 | 108 |
definition |
109 |
iso_tuple_cons :: |
|
110 |
"('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
111 |
"iso_tuple_cons isom = curry (abst isom)" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
112 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
113 |
|
60758 | 114 |
subsection \<open>Logical infrastructure for records\<close> |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
115 |
|
35132 | 116 |
definition |
117 |
iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
118 |
"iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
119 |
|
35132 | 120 |
definition |
121 |
iso_tuple_update_accessor_cong_assist :: |
|
122 |
"(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where |
|
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
123 |
"iso_tuple_update_accessor_cong_assist upd ac \<longleftrightarrow> |
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
124 |
(\<forall>f v. upd (\<lambda>x. f (ac v)) v = upd f v) \<and> (\<forall>v. upd id v = v)" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
125 |
|
35132 | 126 |
definition |
127 |
iso_tuple_update_accessor_eq_assist :: |
|
128 |
"(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where |
|
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
129 |
"iso_tuple_update_accessor_eq_assist upd ac v f v' x \<longleftrightarrow> |
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
130 |
upd f v = v' \<and> ac v = x \<and> iso_tuple_update_accessor_cong_assist upd ac" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
131 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
132 |
lemma update_accessor_congruence_foldE: |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
133 |
assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" |
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
134 |
and r: "r = r'" and v: "ac r' = v'" |
35132 | 135 |
and f: "\<And>v. v' = v \<Longrightarrow> f v = f' v" |
136 |
shows "upd f r = upd f' r'" |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
137 |
using uac r v [symmetric] |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
138 |
apply (subgoal_tac "upd (\<lambda>x. f (ac r')) r' = upd (\<lambda>x. f' (ac r')) r'") |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
139 |
apply (simp add: iso_tuple_update_accessor_cong_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
140 |
apply (simp add: f) |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
141 |
done |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
142 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
143 |
lemma update_accessor_congruence_unfoldE: |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
144 |
"iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow> |
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
145 |
r = r' \<Longrightarrow> ac r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v) \<Longrightarrow> |
35132 | 146 |
upd f r = upd f' r'" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
147 |
apply (erule(2) update_accessor_congruence_foldE) |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
148 |
apply simp |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
149 |
done |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
150 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
151 |
lemma iso_tuple_update_accessor_cong_assist_id: |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
152 |
"iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow> upd id = id" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
153 |
by rule (simp add: iso_tuple_update_accessor_cong_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
154 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
155 |
lemma update_accessor_noopE: |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
156 |
assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" |
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
157 |
and ac: "f (ac x) = ac x" |
35132 | 158 |
shows "upd f x = x" |
159 |
using uac |
|
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
160 |
by (simp add: ac iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def] |
35132 | 161 |
cong: update_accessor_congruence_unfoldE [OF uac]) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
162 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
163 |
lemma update_accessor_noop_compE: |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
164 |
assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" |
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
165 |
and ac: "f (ac x) = ac x" |
35132 | 166 |
shows "upd (g \<circ> f) x = upd g x" |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
167 |
by (simp add: ac cong: update_accessor_congruence_unfoldE[OF uac]) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
168 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
169 |
lemma update_accessor_cong_assist_idI: |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
170 |
"iso_tuple_update_accessor_cong_assist id id" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
171 |
by (simp add: iso_tuple_update_accessor_cong_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
172 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
173 |
lemma update_accessor_cong_assist_triv: |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
174 |
"iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow> |
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
175 |
iso_tuple_update_accessor_cong_assist upd ac" |
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 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
178 |
lemma update_accessor_accessor_eqE: |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
179 |
"iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> ac v = x" |
34151
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 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
182 |
lemma update_accessor_updator_eqE: |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
183 |
"iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> upd f v = v'" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
184 |
by (simp add: iso_tuple_update_accessor_eq_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_update_accessor_eq_assist_idI: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
187 |
"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
|
188 |
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
|
189 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
190 |
lemma iso_tuple_update_accessor_eq_assist_triv: |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
191 |
"iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> |
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
192 |
iso_tuple_update_accessor_eq_assist upd ac v f v' x" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
193 |
by assumption |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
194 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
195 |
lemma iso_tuple_update_accessor_cong_from_eq: |
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
196 |
"iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> |
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
36176
diff
changeset
|
197 |
iso_tuple_update_accessor_cong_assist upd ac" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
198 |
by (simp add: iso_tuple_update_accessor_eq_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
199 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
200 |
lemma iso_tuple_surjective_proof_assistI: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
201 |
"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
|
202 |
by (simp add: iso_tuple_surjective_proof_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
203 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
204 |
lemma iso_tuple_surjective_proof_assist_idE: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
205 |
"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
|
206 |
by (simp add: iso_tuple_surjective_proof_assist_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
207 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
208 |
locale isomorphic_tuple = |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
209 |
fixes isom :: "('a, 'b, 'c) tuple_isomorphism" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
210 |
assumes repr_inv: "\<And>x. abst isom (repr isom x) = x" |
35132 | 211 |
and abst_inv: "\<And>y. repr isom (abst isom y) = y" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
212 |
begin |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
213 |
|
35132 | 214 |
lemma repr_inj: "repr isom x = repr isom y \<longleftrightarrow> x = y" |
215 |
by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"] |
|
216 |
simp add: repr_inv) |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
217 |
|
35132 | 218 |
lemma abst_inj: "abst isom x = abst isom y \<longleftrightarrow> x = y" |
219 |
by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"] |
|
220 |
simp add: abst_inv) |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
221 |
|
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
222 |
lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
223 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
224 |
lemma iso_tuple_access_update_fst_fst: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
225 |
"f o h g = j o f \<Longrightarrow> |
35132 | 226 |
(f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g = |
227 |
j o (f o iso_tuple_fst isom)" |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
228 |
by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps |
44922 | 229 |
fun_eq_iff) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
230 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
231 |
lemma iso_tuple_access_update_snd_snd: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
232 |
"f o h g = j o f \<Longrightarrow> |
35132 | 233 |
(f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g = |
234 |
j o (f o iso_tuple_snd isom)" |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
235 |
by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps |
44922 | 236 |
fun_eq_iff) |
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_access_update_fst_snd: |
35132 | 239 |
"(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g = |
240 |
id o (f o iso_tuple_fst isom)" |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
241 |
by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps |
44922 | 242 |
fun_eq_iff) |
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_access_update_snd_fst: |
35132 | 245 |
"(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g = |
246 |
id o (f o iso_tuple_snd isom)" |
|
34151
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_def simps |
44922 | 248 |
fun_eq_iff) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
249 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
250 |
lemma iso_tuple_update_swap_fst_fst: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
251 |
"h f o j g = j g o h f \<Longrightarrow> |
35132 | 252 |
(iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g = |
253 |
(iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f" |
|
44922 | 254 |
by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
255 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
256 |
lemma iso_tuple_update_swap_snd_snd: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
257 |
"h f o j g = j g o h f \<Longrightarrow> |
35132 | 258 |
(iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g = |
259 |
(iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f" |
|
44922 | 260 |
by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
261 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
262 |
lemma iso_tuple_update_swap_fst_snd: |
35132 | 263 |
"(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g = |
264 |
(iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f" |
|
265 |
by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def |
|
44922 | 266 |
simps fun_eq_iff) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
267 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
268 |
lemma iso_tuple_update_swap_snd_fst: |
35132 | 269 |
"(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g = |
270 |
(iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f" |
|
44922 | 271 |
by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps |
272 |
fun_eq_iff) |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
273 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
274 |
lemma iso_tuple_update_compose_fst_fst: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
275 |
"h f o j g = k (f o g) \<Longrightarrow> |
35132 | 276 |
(iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g = |
277 |
(iso_tuple_fst_update isom o k) (f o g)" |
|
44922 | 278 |
by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
279 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
280 |
lemma iso_tuple_update_compose_snd_snd: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
281 |
"h f o j g = k (f o g) \<Longrightarrow> |
35132 | 282 |
(iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g = |
283 |
(iso_tuple_snd_update isom o k) (f o g)" |
|
44922 | 284 |
by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
285 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
286 |
lemma iso_tuple_surjective_proof_assist_step: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
287 |
"iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \<Longrightarrow> |
35132 | 288 |
iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f) \<Longrightarrow> |
289 |
iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f" |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
290 |
by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
291 |
iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
292 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
293 |
lemma iso_tuple_fst_update_accessor_cong_assist: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
294 |
assumes "iso_tuple_update_accessor_cong_assist f g" |
35132 | 295 |
shows "iso_tuple_update_accessor_cong_assist |
296 |
(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
|
297 |
proof - |
35132 | 298 |
from assms have "f id = id" |
299 |
by (rule iso_tuple_update_accessor_cong_assist_id) |
|
300 |
with assms show ?thesis |
|
301 |
by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps |
|
302 |
iso_tuple_fst_update_def iso_tuple_fst_def) |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
303 |
qed |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
304 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
305 |
lemma iso_tuple_snd_update_accessor_cong_assist: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
306 |
assumes "iso_tuple_update_accessor_cong_assist f g" |
35132 | 307 |
shows "iso_tuple_update_accessor_cong_assist |
308 |
(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
|
309 |
proof - |
35132 | 310 |
from assms have "f id = id" |
311 |
by (rule iso_tuple_update_accessor_cong_assist_id) |
|
312 |
with assms show ?thesis |
|
313 |
by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps |
|
314 |
iso_tuple_snd_update_def iso_tuple_snd_def) |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
315 |
qed |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
316 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
317 |
lemma iso_tuple_fst_update_accessor_eq_assist: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
318 |
assumes "iso_tuple_update_accessor_eq_assist f g a u a' v" |
35132 | 319 |
shows "iso_tuple_update_accessor_eq_assist |
320 |
(iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom) |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
321 |
(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
|
322 |
proof - |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
323 |
from assms have "f id = id" |
35132 | 324 |
by (auto simp add: iso_tuple_update_accessor_eq_assist_def |
325 |
intro: iso_tuple_update_accessor_cong_assist_id) |
|
326 |
with assms show ?thesis |
|
327 |
by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def |
|
328 |
iso_tuple_fst_update_def iso_tuple_fst_def |
|
329 |
iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps) |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
330 |
qed |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
331 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
332 |
lemma iso_tuple_snd_update_accessor_eq_assist: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
333 |
assumes "iso_tuple_update_accessor_eq_assist f g b u b' v" |
35132 | 334 |
shows "iso_tuple_update_accessor_eq_assist |
335 |
(iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom) |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
336 |
(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
|
337 |
proof - |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
338 |
from assms have "f id = id" |
35132 | 339 |
by (auto simp add: iso_tuple_update_accessor_eq_assist_def |
340 |
intro: iso_tuple_update_accessor_cong_assist_id) |
|
341 |
with assms show ?thesis |
|
342 |
by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def |
|
343 |
iso_tuple_snd_update_def iso_tuple_snd_def |
|
344 |
iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps) |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
345 |
qed |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
346 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
347 |
lemma iso_tuple_cons_conj_eqI: |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
348 |
"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
|
349 |
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
|
350 |
by (clarsimp simp: iso_tuple_cons_def simps) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
351 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
352 |
lemmas intros = |
35132 | 353 |
iso_tuple_access_update_fst_fst |
354 |
iso_tuple_access_update_snd_snd |
|
355 |
iso_tuple_access_update_fst_snd |
|
356 |
iso_tuple_access_update_snd_fst |
|
357 |
iso_tuple_update_swap_fst_fst |
|
358 |
iso_tuple_update_swap_snd_snd |
|
359 |
iso_tuple_update_swap_fst_snd |
|
360 |
iso_tuple_update_swap_snd_fst |
|
361 |
iso_tuple_update_compose_fst_fst |
|
362 |
iso_tuple_update_compose_snd_snd |
|
363 |
iso_tuple_surjective_proof_assist_step |
|
364 |
iso_tuple_fst_update_accessor_eq_assist |
|
365 |
iso_tuple_snd_update_accessor_eq_assist |
|
366 |
iso_tuple_fst_update_accessor_cong_assist |
|
367 |
iso_tuple_snd_update_accessor_cong_assist |
|
368 |
iso_tuple_cons_conj_eqI |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
369 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
370 |
end |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
371 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
372 |
lemma isomorphic_tuple_intro: |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
373 |
fixes repr abst |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
374 |
assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y" |
35132 | 375 |
and abst_inv: "\<And>z. repr (abst z) = z" |
376 |
and v: "v \<equiv> Tuple_Isomorphism repr abst" |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
377 |
shows "isomorphic_tuple v" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
378 |
proof |
35132 | 379 |
fix x have "repr (abst (repr x)) = repr x" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
380 |
by (simp add: abst_inv) |
35132 | 381 |
then show "Record.abst v (Record.repr v x) = x" |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
382 |
by (simp add: v repr_inj) |
35132 | 383 |
next |
384 |
fix y |
|
385 |
show "Record.repr v (Record.abst v y) = y" |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
386 |
by (simp add: v) (fact abst_inv) |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
387 |
qed |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
388 |
|
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
389 |
definition |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
390 |
"tuple_iso_tuple \<equiv> Tuple_Isomorphism id id" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
391 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
392 |
lemma tuple_iso_tuple: |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
393 |
"isomorphic_tuple tuple_iso_tuple" |
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
394 |
by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def) |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
395 |
|
35132 | 396 |
lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
397 |
by simp |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
398 |
|
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
51112
diff
changeset
|
399 |
lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
400 |
by simp |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
401 |
|
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
402 |
lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
403 |
by simp |
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
404 |
|
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14080
diff
changeset
|
405 |
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
|
406 |
by simp |
11826 | 407 |
|
35132 | 408 |
lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" |
25705 | 409 |
by (simp add: comp_def) |
11821 | 410 |
|
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
411 |
|
60758 | 412 |
subsection \<open>Concrete record syntax\<close> |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
413 |
|
41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
38539
diff
changeset
|
414 |
nonterminal |
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
38539
diff
changeset
|
415 |
ident and |
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
38539
diff
changeset
|
416 |
field_type and |
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
38539
diff
changeset
|
417 |
field_types and |
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
38539
diff
changeset
|
418 |
field and |
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
38539
diff
changeset
|
419 |
fields and |
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
38539
diff
changeset
|
420 |
field_update and |
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
38539
diff
changeset
|
421 |
field_updates |
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
38539
diff
changeset
|
422 |
|
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
423 |
syntax |
11821 | 424 |
"_constify" :: "id => ident" ("_") |
425 |
"_constify" :: "longid => ident" ("_") |
|
5198 | 426 |
|
35144 | 427 |
"_field_type" :: "ident => type => field_type" ("(2_ ::/ _)") |
11821 | 428 |
"" :: "field_type => field_types" ("_") |
35144 | 429 |
"_field_types" :: "field_type => field_types => field_types" ("_,/ _") |
11821 | 430 |
"_record_type" :: "field_types => type" ("(3'(| _ |'))") |
35144 | 431 |
"_record_type_scheme" :: "field_types => type => type" ("(3'(| _,/ (2... ::/ _) |'))") |
5198 | 432 |
|
35144 | 433 |
"_field" :: "ident => 'a => field" ("(2_ =/ _)") |
11821 | 434 |
"" :: "field => fields" ("_") |
35144 | 435 |
"_fields" :: "field => fields => fields" ("_,/ _") |
11821 | 436 |
"_record" :: "fields => 'a" ("(3'(| _ |'))") |
35144 | 437 |
"_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))") |
5198 | 438 |
|
35146 | 439 |
"_field_update" :: "ident => 'a => field_update" ("(2_ :=/ _)") |
440 |
"" :: "field_update => field_updates" ("_") |
|
441 |
"_field_updates" :: "field_update => field_updates => field_updates" ("_,/ _") |
|
442 |
"_record_update" :: "'a => field_updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900) |
|
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
443 |
|
10331 | 444 |
syntax (xsymbols) |
11821 | 445 |
"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)") |
35132 | 446 |
"_record_type_scheme" :: "field_types => type => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
447 |
"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
|
448 |
"_record_scheme" :: "fields => 'a => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
|
35146 | 449 |
"_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900) |
9729 | 450 |
|
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
451 |
|
60758 | 452 |
subsection \<open>Record package\<close> |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
453 |
|
56732 | 454 |
ML_file "Tools/record.ML" |
10641 | 455 |
|
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
35146
diff
changeset
|
456 |
hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd |
34151
8d57ce46b3f7
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann
parents:
33595
diff
changeset
|
457 |
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
|
458 |
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
|
459 |
iso_tuple_update_accessor_eq_assist tuple_iso_tuple |
33595
7264824baf66
substantial simplification restores code generation
haftmann
parents:
32799
diff
changeset
|
460 |
|
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
461 |
end |