substantial simplification restores code generation
authorhaftmann
Tue Nov 10 16:11:43 2009 +0100 (2009-11-10)
changeset 335957264824baf66
parent 33594 357f74e0090c
child 33596 27c5023ee818
substantial simplification restores code generation
src/HOL/Record.thy
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Record.thy	Tue Nov 10 16:11:39 2009 +0100
     1.2 +++ b/src/HOL/Record.thy	Tue Nov 10 16:11:43 2009 +0100
     1.3 @@ -3,15 +3,386 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5      Author:     Norbert Schirmer, TU Muenchen
     1.6      Author:     Thomas Sewell, NICTA
     1.7 +    Author:     Florian Haftmann, TU Muenchen
     1.8  *)
     1.9  
    1.10  header {* Extensible records with structural subtyping *}
    1.11  
    1.12  theory Record
    1.13 -imports Product_Type
    1.14 +imports Datatype
    1.15  uses ("Tools/record.ML")
    1.16  begin
    1.17  
    1.18 +subsection {* Introduction *}
    1.19 +
    1.20 +text {*
    1.21 +  Records are isomorphic to compound tuple types. To implement
    1.22 +  efficient records, we make this isomorphism explicit. Consider the
    1.23 +  record access/update simplification @{text "alpha (beta_update f
    1.24 +  rec) = alpha rec"} for distinct fields alpha and beta of some record
    1.25 +  rec with n fields. There are @{text "n ^ 2"} such theorems, which
    1.26 +  prohibits storage of all of them for large n. The rules can be
    1.27 +  proved on the fly by case decomposition and simplification in O(n)
    1.28 +  time. By creating O(n) isomorphic-tuple types while defining the
    1.29 +  record, however, we can prove the access/update simplification in
    1.30 +  @{text "O(log(n)^2)"} time.
    1.31 +
    1.32 +  The O(n) cost of case decomposition is not because O(n) steps are
    1.33 +  taken, but rather because the resulting rule must contain O(n) new
    1.34 +  variables and an O(n) size concrete record construction. To sidestep
    1.35 +  this cost, we would like to avoid case decomposition in proving
    1.36 +  access/update theorems.
    1.37 +
    1.38 +  Record types are defined as isomorphic to tuple types. For instance,
    1.39 +  a record type with fields @{text "'a"}, @{text "'b"}, @{text "'c"}
    1.40 +  and @{text "'d"} might be introduced as isomorphic to @{text "'a \<times>
    1.41 +  ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to @{text "('a \<times>
    1.42 +  'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to the
    1.43 +  underlying type then using O(log(n)) fst or snd operations.
    1.44 +  Updators can be defined similarly, if we introduce a @{text
    1.45 +  "fst_update"} and @{text "snd_update"} function. Furthermore, we can
    1.46 +  prove the access/update theorem in O(log(n)) steps by using simple
    1.47 +  rewrites on fst, snd, @{text "fst_update"} and @{text "snd_update"}.
    1.48 +
    1.49 +  The catch is that, although O(log(n)) steps were taken, the
    1.50 +  underlying type we converted to is a tuple tree of size
    1.51 +  O(n). Processing this term type wastes performance. We avoid this
    1.52 +  for large n by taking each subtree of size K and defining a new type
    1.53 +  isomorphic to that tuple subtree. A record can now be defined as
    1.54 +  isomorphic to a tuple tree of these O(n/K) new types, or, if @{text
    1.55 +  "n > K*K"}, we can repeat the process, until the record can be
    1.56 +  defined in terms of a tuple tree of complexity less than the
    1.57 +  constant K.
    1.58 +
    1.59 +  If we prove the access/update theorem on this type with the
    1.60 +  analagous steps to the tuple tree, we consume @{text "O(log(n)^2)"}
    1.61 +  time as the intermediate terms are @{text "O(log(n))"} in size and
    1.62 +  the types needed have size bounded by K.  To enable this analagous
    1.63 +  traversal, we define the functions seen below: @{text
    1.64 +  "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"}
    1.65 +  and @{text "istuple_snd_update"}. These functions generalise tuple
    1.66 +  operations by taking a parameter that encapsulates a tuple
    1.67 +  isomorphism.  The rewrites needed on these functions now need an
    1.68 +  additional assumption which is that the isomorphism works.
    1.69 +
    1.70 +  These rewrites are typically used in a structured way. They are here
    1.71 +  presented as the introduction rule @{text "isomorphic_tuple.intros"}
    1.72 +  rather than as a rewrite rule set. The introduction form is an
    1.73 +  optimisation, as net matching can be performed at one term location
    1.74 +  for each step rather than the simplifier searching the term for
    1.75 +  possible pattern matches. The rule set is used as it is viewed
    1.76 +  outside the locale, with the locale assumption (that the isomorphism
    1.77 +  is valid) left as a rule assumption. All rules are structured to aid
    1.78 +  net matching, using either a point-free form or an encapsulating
    1.79 +  predicate.
    1.80 +*}
    1.81 +
    1.82 +subsection {* Operators and lemmas for types isomorphic to tuples *}
    1.83 +
    1.84 +datatype ('a, 'b, 'c) tuple_isomorphism = TupleIsomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
    1.85 +
    1.86 +primrec repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where
    1.87 +  "repr (TupleIsomorphism r a) = r"
    1.88 +
    1.89 +primrec abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
    1.90 +  "abst (TupleIsomorphism r a) = a"
    1.91 +
    1.92 +definition istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.93 +  "istuple_fst isom = fst \<circ> repr isom"
    1.94 +
    1.95 +definition istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.96 +  "istuple_snd isom = snd \<circ> repr isom"
    1.97 +
    1.98 +definition istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    1.99 +  "istuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
   1.100 +
   1.101 +definition istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
   1.102 +  "istuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
   1.103 +
   1.104 +definition istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
   1.105 +  "istuple_cons isom = curry (abst isom)"
   1.106 +
   1.107 +
   1.108 +subsection {* Logical infrastructure for records *}
   1.109 +
   1.110 +definition istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   1.111 +  "istuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
   1.112 +
   1.113 +definition istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   1.114 +  "istuple_update_accessor_cong_assist upd acc \<longleftrightarrow> 
   1.115 +     (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
   1.116 +
   1.117 +definition istuple_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
   1.118 +  "istuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow>
   1.119 +     upd f v = v' \<and> acc v = x \<and> istuple_update_accessor_cong_assist upd acc"
   1.120 +
   1.121 +lemma update_accessor_congruence_foldE:
   1.122 +  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   1.123 +  and       r: "r = r'" and v: "acc r' = v'"
   1.124 +  and       f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
   1.125 +  shows        "upd f r = upd f' r'"
   1.126 +  using uac r v [symmetric]
   1.127 +  apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
   1.128 +   apply (simp add: istuple_update_accessor_cong_assist_def)
   1.129 +  apply (simp add: f)
   1.130 +  done
   1.131 +
   1.132 +lemma update_accessor_congruence_unfoldE:
   1.133 +  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> r = r' \<Longrightarrow> acc r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v)
   1.134 +     \<Longrightarrow> upd f r = upd f' r'"
   1.135 +  apply (erule(2) update_accessor_congruence_foldE)
   1.136 +  apply simp
   1.137 +  done
   1.138 +
   1.139 +lemma istuple_update_accessor_cong_assist_id:
   1.140 +  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
   1.141 +  by rule (simp add: istuple_update_accessor_cong_assist_def)
   1.142 +
   1.143 +lemma update_accessor_noopE:
   1.144 +  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   1.145 +      and acc: "f (acc x) = acc x"
   1.146 +  shows        "upd f x = x"
   1.147 +using uac by (simp add: acc istuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
   1.148 +  cong: update_accessor_congruence_unfoldE [OF uac])
   1.149 +
   1.150 +lemma update_accessor_noop_compE:
   1.151 +  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   1.152 +  assumes acc: "f (acc x) = acc x"
   1.153 +  shows      "upd (g \<circ> f) x = upd g x"
   1.154 +  by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
   1.155 +
   1.156 +lemma update_accessor_cong_assist_idI:
   1.157 +  "istuple_update_accessor_cong_assist id id"
   1.158 +  by (simp add: istuple_update_accessor_cong_assist_def)
   1.159 +
   1.160 +lemma update_accessor_cong_assist_triv:
   1.161 +  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   1.162 +  by assumption
   1.163 +
   1.164 +lemma update_accessor_accessor_eqE:
   1.165 +  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> acc v = x"
   1.166 +  by (simp add: istuple_update_accessor_eq_assist_def)
   1.167 +
   1.168 +lemma update_accessor_updator_eqE:
   1.169 +  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> upd f v = v'"
   1.170 +  by (simp add: istuple_update_accessor_eq_assist_def)
   1.171 +
   1.172 +lemma istuple_update_accessor_eq_assist_idI:
   1.173 +  "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
   1.174 +  by (simp add: istuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
   1.175 +
   1.176 +lemma istuple_update_accessor_eq_assist_triv:
   1.177 +  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
   1.178 +  by assumption
   1.179 +
   1.180 +lemma istuple_update_accessor_cong_from_eq:
   1.181 +  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   1.182 +  by (simp add: istuple_update_accessor_eq_assist_def)
   1.183 +
   1.184 +lemma o_eq_dest:
   1.185 +  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
   1.186 +  apply (clarsimp simp: o_def)
   1.187 +  apply (erule fun_cong)
   1.188 +  done
   1.189 +
   1.190 +lemma o_eq_elim:
   1.191 +  "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
   1.192 +  apply (erule meta_mp)
   1.193 +  apply (erule o_eq_dest)
   1.194 +  done
   1.195 +
   1.196 +lemma istuple_surjective_proof_assistI:
   1.197 +  "f x = y \<Longrightarrow> istuple_surjective_proof_assist x y f"
   1.198 +  by (simp add: istuple_surjective_proof_assist_def)
   1.199 +
   1.200 +lemma istuple_surjective_proof_assist_idE:
   1.201 +  "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   1.202 +  by (simp add: istuple_surjective_proof_assist_def)
   1.203 +
   1.204 +locale isomorphic_tuple =
   1.205 +  fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
   1.206 +    and repr and abst
   1.207 +  defines "repr \<equiv> Record.repr isom"
   1.208 +  defines "abst \<equiv> Record.abst isom"
   1.209 +  assumes repr_inv: "\<And>x. abst (repr x) = x"
   1.210 +  assumes abst_inv: "\<And>y. repr (abst y) = y"
   1.211 +begin
   1.212 +
   1.213 +lemma repr_inj:
   1.214 +  "repr x = repr y \<longleftrightarrow> x = y"
   1.215 +  apply (rule iffI, simp_all)
   1.216 +  apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
   1.217 +  done
   1.218 +
   1.219 +lemma abst_inj:
   1.220 +  "abst x = abst y \<longleftrightarrow> x = y"
   1.221 +  apply (rule iffI, simp_all)
   1.222 +  apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
   1.223 +  done
   1.224 +
   1.225 +lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj repr_def [symmetric] abst_def [symmetric]
   1.226 +
   1.227 +lemma istuple_access_update_fst_fst:
   1.228 +  "f o h g = j o f \<Longrightarrow>
   1.229 +    (f o istuple_fst isom) o (istuple_fst_update isom o h) g
   1.230 +          = j o (f o istuple_fst isom)"
   1.231 +  by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
   1.232 +             intro!: ext elim!: o_eq_elim)
   1.233 +
   1.234 +lemma istuple_access_update_snd_snd:
   1.235 +  "f o h g = j o f \<Longrightarrow>
   1.236 +    (f o istuple_snd isom) o (istuple_snd_update isom o h) g
   1.237 +          = j o (f o istuple_snd isom)"
   1.238 +  by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
   1.239 +             intro!: ext elim!: o_eq_elim)
   1.240 +
   1.241 +lemma istuple_access_update_fst_snd:
   1.242 +  "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
   1.243 +          = id o (f o istuple_fst isom)"
   1.244 +  by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
   1.245 +             intro!: ext elim!: o_eq_elim)
   1.246 +
   1.247 +lemma istuple_access_update_snd_fst:
   1.248 +  "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
   1.249 +          = id o (f o istuple_snd isom)"
   1.250 +  by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
   1.251 +             intro!: ext elim!: o_eq_elim)
   1.252 +
   1.253 +lemma istuple_update_swap_fst_fst:
   1.254 +  "h f o j g = j g o h f \<Longrightarrow>
   1.255 +    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   1.256 +          = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
   1.257 +  by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
   1.258 +
   1.259 +lemma istuple_update_swap_snd_snd:
   1.260 +  "h f o j g = j g o h f \<Longrightarrow>
   1.261 +    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   1.262 +          = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
   1.263 +  by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
   1.264 +
   1.265 +lemma istuple_update_swap_fst_snd:
   1.266 +  "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
   1.267 +          = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
   1.268 +  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
   1.269 +
   1.270 +lemma istuple_update_swap_snd_fst:
   1.271 +  "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
   1.272 +          = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
   1.273 +  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
   1.274 +
   1.275 +lemma istuple_update_compose_fst_fst:
   1.276 +  "h f o j g = k (f o g) \<Longrightarrow>
   1.277 +    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   1.278 +          = (istuple_fst_update isom o k) (f o g)"
   1.279 +  by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
   1.280 +
   1.281 +lemma istuple_update_compose_snd_snd:
   1.282 +  "h f o j g = k (f o g) \<Longrightarrow>
   1.283 +    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   1.284 +          = (istuple_snd_update isom o k) (f o g)"
   1.285 +  by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
   1.286 +
   1.287 +lemma istuple_surjective_proof_assist_step:
   1.288 +  "istuple_surjective_proof_assist v a (istuple_fst isom o f) \<Longrightarrow>
   1.289 +     istuple_surjective_proof_assist v b (istuple_snd isom o f)
   1.290 +      \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
   1.291 +  by (clarsimp simp: istuple_surjective_proof_assist_def simps
   1.292 +    istuple_fst_def istuple_snd_def istuple_cons_def)
   1.293 +
   1.294 +lemma istuple_fst_update_accessor_cong_assist:
   1.295 +  assumes "istuple_update_accessor_cong_assist f g"
   1.296 +  shows "istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
   1.297 +proof -
   1.298 +  from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
   1.299 +  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   1.300 +    istuple_fst_update_def istuple_fst_def)
   1.301 +qed
   1.302 +
   1.303 +lemma istuple_snd_update_accessor_cong_assist:
   1.304 +  assumes "istuple_update_accessor_cong_assist f g"
   1.305 +  shows "istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
   1.306 +proof -
   1.307 +  from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
   1.308 +  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   1.309 +    istuple_snd_update_def istuple_snd_def)
   1.310 +qed
   1.311 +
   1.312 +lemma istuple_fst_update_accessor_eq_assist:
   1.313 +  assumes "istuple_update_accessor_eq_assist f g a u a' v"
   1.314 +  shows "istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
   1.315 +    (istuple_cons isom a b) u (istuple_cons isom a' b) v"
   1.316 +proof -
   1.317 +  from assms have "f id = id"
   1.318 +    by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
   1.319 +  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
   1.320 +    istuple_fst_update_def istuple_fst_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   1.321 +qed
   1.322 +
   1.323 +lemma istuple_snd_update_accessor_eq_assist:
   1.324 +  assumes "istuple_update_accessor_eq_assist f g b u b' v"
   1.325 +  shows "istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
   1.326 +    (istuple_cons isom a b) u (istuple_cons isom a b') v"
   1.327 +proof -
   1.328 +  from assms have "f id = id"
   1.329 +    by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
   1.330 +  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
   1.331 +    istuple_snd_update_def istuple_snd_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   1.332 +qed
   1.333 +
   1.334 +lemma istuple_cons_conj_eqI:
   1.335 +  "a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
   1.336 +    istuple_cons isom a b = istuple_cons isom c d \<and> P \<longleftrightarrow> Q"
   1.337 +  by (clarsimp simp: istuple_cons_def simps)
   1.338 +
   1.339 +lemmas intros =
   1.340 +    istuple_access_update_fst_fst
   1.341 +    istuple_access_update_snd_snd
   1.342 +    istuple_access_update_fst_snd
   1.343 +    istuple_access_update_snd_fst
   1.344 +    istuple_update_swap_fst_fst
   1.345 +    istuple_update_swap_snd_snd
   1.346 +    istuple_update_swap_fst_snd
   1.347 +    istuple_update_swap_snd_fst
   1.348 +    istuple_update_compose_fst_fst
   1.349 +    istuple_update_compose_snd_snd
   1.350 +    istuple_surjective_proof_assist_step
   1.351 +    istuple_fst_update_accessor_eq_assist
   1.352 +    istuple_snd_update_accessor_eq_assist
   1.353 +    istuple_fst_update_accessor_cong_assist
   1.354 +    istuple_snd_update_accessor_cong_assist
   1.355 +    istuple_cons_conj_eqI
   1.356 +
   1.357 +end
   1.358 +
   1.359 +lemma isomorphic_tuple_intro:
   1.360 +  fixes repr abst
   1.361 +  assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
   1.362 +     and abst_inv: "\<And>z. repr (abst z) = z"
   1.363 +  assumes v: "v \<equiv> TupleIsomorphism repr abst"
   1.364 +  shows "isomorphic_tuple v"
   1.365 +  apply (rule isomorphic_tuple.intro)
   1.366 +  apply (simp_all add: abst_inv v)
   1.367 +  apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
   1.368 +  apply (simp add: abst_inv)
   1.369 +  done
   1.370 +
   1.371 +definition
   1.372 +  "tuple_istuple \<equiv> TupleIsomorphism id id"
   1.373 +
   1.374 +lemma tuple_istuple:
   1.375 +  "isomorphic_tuple tuple_istuple"
   1.376 +  by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_istuple_def)
   1.377 +
   1.378 +lemma refl_conj_eq:
   1.379 +  "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   1.380 +  by simp
   1.381 +
   1.382 +lemma istuple_UNIV_I: "x \<in> UNIV \<equiv> True"
   1.383 +  by simp
   1.384 +
   1.385 +lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   1.386 +  by simp
   1.387 +
   1.388  lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
   1.389    by simp
   1.390  
   1.391 @@ -22,14 +393,11 @@
   1.392    "a o b = c \<Longrightarrow> a (b v) = c v"
   1.393    by clarsimp
   1.394  
   1.395 -lemma id_o_refl:
   1.396 -  "id o f = f o id"
   1.397 -  by simp
   1.398 -
   1.399  lemma o_eq_id_dest:
   1.400    "a o b = id o c \<Longrightarrow> a (b v) = c v"
   1.401    by clarsimp
   1.402  
   1.403 +
   1.404  subsection {* Concrete record syntax *}
   1.405  
   1.406  nonterminals
   1.407 @@ -63,400 +431,15 @@
   1.408    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   1.409    "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
   1.410  
   1.411 -subsection {* Operators and lemmas for types isomorphic to tuples *}
   1.412  
   1.413 -text {*
   1.414 -Records are isomorphic to compound tuple types. To implement efficient
   1.415 -records, we make this isomorphism explicit. Consider the record
   1.416 -access/update simplification @{text "alpha (beta_update f rec) = alpha rec"} for
   1.417 -distinct fields alpha and beta of some record rec with n fields. There
   1.418 -are @{text "n ^ 2"} such theorems, which prohibits storage of all of them for
   1.419 -large n. The rules can be proved on the fly by case decomposition and
   1.420 -simplification in O(n) time. By creating O(n) isomorphic-tuple types
   1.421 -while defining the record, however, we can prove the access/update
   1.422 -simplification in @{text "O(log(n)^2)"} time.
   1.423 -
   1.424 -The O(n) cost of case decomposition is not because O(n) steps are taken,
   1.425 -but rather because the resulting rule must contain O(n) new variables and
   1.426 -an O(n) size concrete record construction. To sidestep this cost, we would
   1.427 -like to avoid case decomposition in proving access/update theorems.
   1.428 -
   1.429 -Record types are defined as isomorphic to tuple types. For instance, a
   1.430 -record type with fields 'a, 'b, 'c and 'd might be introduced as
   1.431 -isomorphic to @{text "'a \<times> ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to
   1.432 -@{text "('a \<times> 'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to
   1.433 -the underlying type then using O(log(n)) fst or snd operations.
   1.434 -Updators can be defined similarly, if we introduce a @{text "fst_update"} and
   1.435 -@{text "snd_update"} function. Furthermore, we can prove the access/update
   1.436 -theorem in O(log(n)) steps by using simple rewrites on fst, snd,
   1.437 -@{text "fst_update"} and @{text "snd_update"}.
   1.438 -
   1.439 -The catch is that, although O(log(n)) steps were taken, the underlying
   1.440 -type we converted to is a tuple tree of size O(n). Processing this term
   1.441 -type wastes performance. We avoid this for large n by taking each
   1.442 -subtree of size K and defining a new type isomorphic to that tuple
   1.443 -subtree. A record can now be defined as isomorphic to a tuple tree
   1.444 -of these O(n/K) new types, or, if @{text "n > K*K"}, we can repeat the process,
   1.445 -until the record can be defined in terms of a tuple tree of complexity
   1.446 -less than the constant K.
   1.447 -
   1.448 -If we prove the access/update theorem on this type with the analagous
   1.449 -steps to the tuple tree, we consume @{text "O(log(n)^2)"} time as the intermediate
   1.450 -terms are O(log(n)) in size and the types needed have size bounded by K.
   1.451 -To enable this analagous traversal, we define the functions seen below:
   1.452 -@{text "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"}
   1.453 -and @{text "istuple_snd_update"}. These functions generalise tuple
   1.454 -operations by taking a parameter that encapsulates a tuple isomorphism.
   1.455 -The rewrites needed on these functions now need an additional assumption
   1.456 -which is that the isomorphism works.
   1.457 -
   1.458 -These rewrites are typically used in a structured way. They are here
   1.459 -presented as the introduction rule @{text "isomorphic_tuple.intros"} rather than
   1.460 -as a rewrite rule set. The introduction form is an optimisation, as net
   1.461 -matching can be performed at one term location for each step rather than
   1.462 -the simplifier searching the term for possible pattern matches. The rule
   1.463 -set is used as it is viewed outside the locale, with the locale assumption
   1.464 -(that the isomorphism is valid) left as a rule assumption. All rules are
   1.465 -structured to aid net matching, using either a point-free form or an
   1.466 -encapsulating predicate.
   1.467 -*}
   1.468 -
   1.469 -typedef ('a, 'b, 'c) tuple_isomorphism
   1.470 -  = "UNIV :: (('a \<Rightarrow> ('b \<times> 'c)) \<times> (('b \<times> 'c) \<Rightarrow> 'a)) set"
   1.471 -  by simp
   1.472 -
   1.473 -definition
   1.474 -  "TupleIsomorphism repr abst = Abs_tuple_isomorphism (repr, abst)"
   1.475 -
   1.476 -definition
   1.477 -  istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b"
   1.478 -where
   1.479 - "istuple_fst isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in fst \<circ> repr"
   1.480 -
   1.481 -definition
   1.482 -  istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c"
   1.483 -where
   1.484 - "istuple_snd isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in snd \<circ> repr"
   1.485 -
   1.486 -definition
   1.487 -  istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)"
   1.488 -where
   1.489 - "istuple_fst_update isom \<equiv>
   1.490 -     let (repr, abst) = Rep_tuple_isomorphism isom in
   1.491 -        (\<lambda>f v. abst (f (fst (repr v)), snd (repr v)))"
   1.492 -
   1.493 -definition
   1.494 -  istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)"
   1.495 -where
   1.496 - "istuple_snd_update isom \<equiv>
   1.497 -     let (repr, abst) = Rep_tuple_isomorphism isom in
   1.498 -        (\<lambda>f v. abst (fst (repr v), f (snd (repr v))))"
   1.499 -
   1.500 -definition
   1.501 -  istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a"
   1.502 -where
   1.503 - "istuple_cons isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in curry abst"
   1.504 -
   1.505 -text {*
   1.506 -These predicates are used in the introduction rule set to constrain
   1.507 -matching appropriately. The elimination rules for them produce the
   1.508 -desired theorems once they are proven. The final introduction rules are
   1.509 -used when no further rules from the introduction rule set can apply.
   1.510 -*}
   1.511 -
   1.512 -definition
   1.513 -  istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   1.514 -where
   1.515 - "istuple_surjective_proof_assist x y f \<equiv> (f x = y)"
   1.516 -
   1.517 -definition
   1.518 -  istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a))
   1.519 -                              \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   1.520 -where
   1.521 - "istuple_update_accessor_cong_assist upd acc
   1.522 -    \<equiv> (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v)
   1.523 -       \<and> (\<forall>v. upd id v = v)"
   1.524 -
   1.525 -definition
   1.526 -  istuple_update_accessor_eq_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b)
   1.527 -                              \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   1.528 -where
   1.529 - "istuple_update_accessor_eq_assist upd acc v f v' x
   1.530 -    \<equiv> upd f v = v' \<and> acc v = x
   1.531 -      \<and> istuple_update_accessor_cong_assist upd acc"
   1.532 -
   1.533 -lemma update_accessor_congruence_foldE:
   1.534 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   1.535 -  and       r: "r = r'" and v: "acc r' = v'"
   1.536 -  and       f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
   1.537 -  shows        "upd f r = upd f' r'"
   1.538 -  using uac r v[symmetric]
   1.539 -  apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
   1.540 -   apply (simp add: istuple_update_accessor_cong_assist_def)
   1.541 -  apply (simp add: f)
   1.542 -  done
   1.543 -
   1.544 -lemma update_accessor_congruence_unfoldE:
   1.545 -  "\<lbrakk> istuple_update_accessor_cong_assist upd acc;
   1.546 -     r = r'; acc r' = v'; \<And>v. v = v' \<Longrightarrow> f v = f' v \<rbrakk>
   1.547 -     \<Longrightarrow> upd f r = upd f' r'"
   1.548 -  apply (erule(2) update_accessor_congruence_foldE)
   1.549 -  apply simp
   1.550 -  done
   1.551 -
   1.552 -lemma istuple_update_accessor_cong_assist_id:
   1.553 -  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
   1.554 -  by (rule ext, simp add: istuple_update_accessor_cong_assist_def)
   1.555 -
   1.556 -lemma update_accessor_noopE:
   1.557 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   1.558 -      and acc: "f (acc x) = acc x"
   1.559 -  shows        "upd f x = x"
   1.560 -  using uac
   1.561 -  by (simp add: acc istuple_update_accessor_cong_assist_id[OF uac, unfolded id_def]
   1.562 -          cong: update_accessor_congruence_unfoldE[OF uac])
   1.563 -
   1.564 -lemma update_accessor_noop_compE:
   1.565 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   1.566 -  assumes acc: "f (acc x) = acc x"
   1.567 -  shows      "upd (g \<circ> f) x = upd g x"
   1.568 -  by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
   1.569 -
   1.570 -lemma update_accessor_cong_assist_idI:
   1.571 -  "istuple_update_accessor_cong_assist id id"
   1.572 -  by (simp add: istuple_update_accessor_cong_assist_def)
   1.573 -
   1.574 -lemma update_accessor_cong_assist_triv:
   1.575 -  "istuple_update_accessor_cong_assist upd acc
   1.576 -       \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   1.577 -  by assumption
   1.578 -
   1.579 -lemma update_accessor_accessor_eqE:
   1.580 -  "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> acc v = x"
   1.581 -  by (simp add: istuple_update_accessor_eq_assist_def)
   1.582 -
   1.583 -lemma update_accessor_updator_eqE:
   1.584 -  "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> upd f v = v'"
   1.585 -  by (simp add: istuple_update_accessor_eq_assist_def)
   1.586 -
   1.587 -lemma istuple_update_accessor_eq_assist_idI:
   1.588 -  "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
   1.589 -  by (simp add: istuple_update_accessor_eq_assist_def
   1.590 -                update_accessor_cong_assist_idI)
   1.591 -
   1.592 -lemma istuple_update_accessor_eq_assist_triv:
   1.593 -  "istuple_update_accessor_eq_assist upd acc v f v' x
   1.594 -     \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
   1.595 -  by assumption
   1.596 -
   1.597 -lemma istuple_update_accessor_cong_from_eq:
   1.598 -  "istuple_update_accessor_eq_assist upd acc v f v' x
   1.599 -     \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   1.600 -  by (simp add: istuple_update_accessor_eq_assist_def)
   1.601 -
   1.602 -lemma o_eq_dest:
   1.603 -  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
   1.604 -  apply (clarsimp simp: o_def)
   1.605 -  apply (erule fun_cong)
   1.606 -  done
   1.607 -
   1.608 -lemma o_eq_elim:
   1.609 -  "\<lbrakk> a o b = c o d; \<lbrakk> \<And>v. a (b v) = c (d v) \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
   1.610 -  apply (erule meta_mp)
   1.611 -  apply (erule o_eq_dest)
   1.612 -  done
   1.613 -
   1.614 -lemma istuple_surjective_proof_assistI:
   1.615 -  "f x = y \<Longrightarrow>
   1.616 -     istuple_surjective_proof_assist x y f"
   1.617 -  by (simp add: istuple_surjective_proof_assist_def)
   1.618 -
   1.619 -lemma istuple_surjective_proof_assist_idE:
   1.620 -  "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   1.621 -  by (simp add: istuple_surjective_proof_assist_def)
   1.622 -
   1.623 -locale isomorphic_tuple =
   1.624 -  fixes isom :: "('a, 'b, 'c) tuple_isomorphism" 
   1.625 -       and repr and abst
   1.626 -  defines "repr \<equiv> fst (Rep_tuple_isomorphism isom)"
   1.627 -  defines "abst \<equiv> snd (Rep_tuple_isomorphism isom)"
   1.628 -  assumes repr_inv: "\<And>x. abst (repr x) = x"
   1.629 -  assumes abst_inv: "\<And>y. repr (abst y) = y"
   1.630 -
   1.631 -begin
   1.632 -
   1.633 -lemma repr_inj:
   1.634 -  "(repr x = repr y) = (x = y)"
   1.635 -  apply (rule iffI, simp_all)
   1.636 -  apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
   1.637 -  done
   1.638 -
   1.639 -lemma abst_inj:
   1.640 -  "(abst x = abst y) = (x = y)"
   1.641 -  apply (rule iffI, simp_all)
   1.642 -  apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
   1.643 -  done
   1.644 -
   1.645 -lemma split_Rep:
   1.646 -  "split f (Rep_tuple_isomorphism isom)
   1.647 -     = f repr abst"
   1.648 -  by (simp add: split_def repr_def abst_def)
   1.649 -
   1.650 -lemmas simps = Let_def split_Rep repr_inv abst_inv repr_inj abst_inj
   1.651 -
   1.652 -lemma istuple_access_update_fst_fst:
   1.653 -  "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
   1.654 -    (f o istuple_fst isom) o (istuple_fst_update isom o h) g
   1.655 -          = j o (f o istuple_fst isom)"
   1.656 -  by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
   1.657 -             intro!: ext elim!: o_eq_elim)
   1.658 -
   1.659 -lemma istuple_access_update_snd_snd:
   1.660 -  "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
   1.661 -    (f o istuple_snd isom) o (istuple_snd_update isom o h) g
   1.662 -          = j o (f o istuple_snd isom)"
   1.663 -  by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
   1.664 -             intro!: ext elim!: o_eq_elim)
   1.665 -
   1.666 -lemma istuple_access_update_fst_snd:
   1.667 -  "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
   1.668 -          = id o (f o istuple_fst isom)"
   1.669 -  by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
   1.670 -             intro!: ext elim!: o_eq_elim)
   1.671 -
   1.672 -lemma istuple_access_update_snd_fst:
   1.673 -  "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
   1.674 -          = id o (f o istuple_snd isom)"
   1.675 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
   1.676 -             intro!: ext elim!: o_eq_elim)
   1.677 -
   1.678 -lemma istuple_update_swap_fst_fst:
   1.679 -  "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
   1.680 -    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   1.681 -          = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
   1.682 -  by (clarsimp simp: istuple_fst_update_def simps
   1.683 -             intro!: ext elim!: o_eq_elim)
   1.684 -
   1.685 -lemma istuple_update_swap_snd_snd:
   1.686 -  "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
   1.687 -    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   1.688 -          = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
   1.689 -  by (clarsimp simp: istuple_snd_update_def simps
   1.690 -             intro!: ext elim!: o_eq_elim)
   1.691 -
   1.692 -lemma istuple_update_swap_fst_snd:
   1.693 -  "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
   1.694 -          = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
   1.695 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
   1.696 -             intro!: ext elim!: o_eq_elim)
   1.697 -
   1.698 -lemma istuple_update_swap_snd_fst:
   1.699 -  "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
   1.700 -          = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
   1.701 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
   1.702 -             intro!: ext elim!: o_eq_elim)
   1.703 -
   1.704 -lemma istuple_update_compose_fst_fst:
   1.705 -  "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
   1.706 -    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   1.707 -          = (istuple_fst_update isom o k) (f o g)"
   1.708 -  by (fastsimp simp: istuple_fst_update_def simps
   1.709 -             intro!: ext elim!: o_eq_elim dest: fun_cong)
   1.710 -
   1.711 -lemma istuple_update_compose_snd_snd:
   1.712 -  "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
   1.713 -    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   1.714 -          = (istuple_snd_update isom o k) (f o g)"
   1.715 -  by (fastsimp simp: istuple_snd_update_def simps
   1.716 -             intro!: ext elim!: o_eq_elim dest: fun_cong)
   1.717 -
   1.718 -lemma istuple_surjective_proof_assist_step:
   1.719 -  "\<lbrakk> istuple_surjective_proof_assist v a (istuple_fst isom o f);
   1.720 -     istuple_surjective_proof_assist v b (istuple_snd isom o f) \<rbrakk>
   1.721 -      \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
   1.722 -  by (clarsimp simp: istuple_surjective_proof_assist_def simps
   1.723 -                     istuple_fst_def istuple_snd_def istuple_cons_def)
   1.724 -
   1.725 -lemma istuple_fst_update_accessor_cong_assist:
   1.726 -  "istuple_update_accessor_cong_assist f g \<Longrightarrow>
   1.727 -      istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
   1.728 -  by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   1.729 -                     istuple_fst_update_def istuple_fst_def)
   1.730 -
   1.731 -lemma istuple_snd_update_accessor_cong_assist:
   1.732 -  "istuple_update_accessor_cong_assist f g \<Longrightarrow>
   1.733 -      istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
   1.734 -  by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   1.735 -                     istuple_snd_update_def istuple_snd_def)
   1.736 -
   1.737 -lemma istuple_fst_update_accessor_eq_assist:
   1.738 -  "istuple_update_accessor_eq_assist f g a u a' v \<Longrightarrow>
   1.739 -      istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
   1.740 -              (istuple_cons isom a b) u (istuple_cons isom a' b) v"
   1.741 -  by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def
   1.742 -                     istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   1.743 -
   1.744 -lemma istuple_snd_update_accessor_eq_assist:
   1.745 -  "istuple_update_accessor_eq_assist f g b u b' v \<Longrightarrow>
   1.746 -      istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
   1.747 -              (istuple_cons isom a b) u (istuple_cons isom a b') v"
   1.748 -  by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def
   1.749 -                     istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   1.750 -
   1.751 -lemma istuple_cons_conj_eqI:
   1.752 -  "\<lbrakk> (a = c \<and> b = d \<and> P) = Q \<rbrakk> \<Longrightarrow>
   1.753 -    (istuple_cons isom a b = istuple_cons isom c d \<and> P) = Q"
   1.754 -  by (clarsimp simp: istuple_cons_def simps)
   1.755 -
   1.756 -lemmas intros =
   1.757 -    istuple_access_update_fst_fst
   1.758 -    istuple_access_update_snd_snd
   1.759 -    istuple_access_update_fst_snd
   1.760 -    istuple_access_update_snd_fst
   1.761 -    istuple_update_swap_fst_fst
   1.762 -    istuple_update_swap_snd_snd
   1.763 -    istuple_update_swap_fst_snd
   1.764 -    istuple_update_swap_snd_fst
   1.765 -    istuple_update_compose_fst_fst
   1.766 -    istuple_update_compose_snd_snd
   1.767 -    istuple_surjective_proof_assist_step
   1.768 -    istuple_fst_update_accessor_eq_assist
   1.769 -    istuple_snd_update_accessor_eq_assist
   1.770 -    istuple_fst_update_accessor_cong_assist
   1.771 -    istuple_snd_update_accessor_cong_assist
   1.772 -    istuple_cons_conj_eqI
   1.773 -
   1.774 -end
   1.775 -
   1.776 -lemma isomorphic_tuple_intro:
   1.777 -  assumes repr_inj: "\<And>x y. (repr x = repr y) = (x = y)"
   1.778 -     and abst_inv: "\<And>z. repr (abst z) = z"
   1.779 -  shows "v \<equiv> TupleIsomorphism repr abst \<Longrightarrow> isomorphic_tuple v"
   1.780 -  apply (rule isomorphic_tuple.intro,
   1.781 -         simp_all add: TupleIsomorphism_def Abs_tuple_isomorphism_inverse
   1.782 -                       tuple_isomorphism_def abst_inv)
   1.783 -  apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
   1.784 -  apply (simp add: abst_inv)
   1.785 -  done
   1.786 -
   1.787 -definition
   1.788 - "tuple_istuple \<equiv> TupleIsomorphism id id"
   1.789 -
   1.790 -lemma tuple_istuple:
   1.791 -  "isomorphic_tuple tuple_istuple"
   1.792 -  by (simp add: isomorphic_tuple_intro[OF _ _ reflexive] tuple_istuple_def)
   1.793 -
   1.794 -lemma refl_conj_eq:
   1.795 -  "Q = R \<Longrightarrow> (P \<and> Q) = (P \<and> R)"
   1.796 -  by simp
   1.797 -
   1.798 -lemma istuple_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
   1.799 -  by simp
   1.800 -
   1.801 -lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   1.802 -  by simp
   1.803 +subsection {* Record package *}
   1.804  
   1.805  use "Tools/record.ML"
   1.806  setup Record.setup
   1.807  
   1.808 +hide (open) const TupleIsomorphism repr abst istuple_fst istuple_snd
   1.809 +  istuple_fst_update istuple_snd_update istuple_cons
   1.810 +  istuple_surjective_proof_assist istuple_update_accessor_cong_assist
   1.811 +  istuple_update_accessor_eq_assist tuple_istuple
   1.812 +
   1.813  end
     2.1 --- a/src/HOL/Tools/record.ML	Tue Nov 10 16:11:39 2009 +0100
     2.2 +++ b/src/HOL/Tools/record.ML	Tue Nov 10 16:11:43 2009 +0100
     2.3 @@ -150,7 +150,8 @@
     2.4      val thm_thy =
     2.5        cdef_thy
     2.6        |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (isom_name, istuple))
     2.7 -      |> Sign.parent_path;
     2.8 +      |> Sign.parent_path
     2.9 +      |> Code.add_default_eqn isom_def;
    2.10    in
    2.11      ((isom, cons $ isom), thm_thy)
    2.12    end;