Initial response to feedback from Norbert, Makarius on record patch
authortsewell@rubicon.NSW.bigpond.net.au
Wed Sep 23 19:17:48 2009 +1000 (2009-09-23)
changeset 32752f65d74a264dd
parent 32751 5b65449d7669
child 32753 5fae12e4679c
Initial response to feedback from Norbert, Makarius on record patch

As Norbert recommended, the IsTuple.thy and istuple_support.ML files
have been integrated into Record.thy and record.ML. I haven't merged
the structures - record.ML now contains Record and IsTupleSupport.

Some of the cosmetic changes Makarius requested have been made,
including renaming variables with camel-case and run-together names
and removing the tab character from the Author: line. Constants are
defined with definition rather than constdefs. The split_ex_prf
inner function has been cleaned up.
src/HOL/IsTuple.thy
src/HOL/Record.thy
src/HOL/Tools/istuple_support.ML
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/IsTuple.thy	Tue Sep 22 13:52:19 2009 +1000
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,389 +0,0 @@
     1.4 -(*  Title:      HOL/IsTuple.thy
     1.5 -    Author:     Thomas Sewell, NICTA
     1.6 -*)
     1.7 -
     1.8 -header {* Operators on types isomorphic to tuples *}
     1.9 -
    1.10 -theory IsTuple imports Product_Type
    1.11 -
    1.12 -uses ("Tools/istuple_support.ML")
    1.13 -
    1.14 -begin
    1.15 -
    1.16 -text {*
    1.17 -This module provides operators and lemmas for types isomorphic to tuples.
    1.18 -These types are used in defining efficient records. Consider the record
    1.19 -access/update simplification "alpha (beta_update f rec) = alpha rec" for
    1.20 -distinct fields alpha and beta of some record rec with n fields. There
    1.21 -are n^2 such theorems, which prohibits storage of all of them for
    1.22 -large n. The rules can be proved on the fly by case decomposition and
    1.23 -simplification in O(n) time. By creating O(n) isomorphic-tuple types
    1.24 -while defining the record, however, we can prove the access/update
    1.25 -simplification in O(log(n)^2) time.
    1.26 -
    1.27 -The O(n) cost of case decomposition is not because O(n) steps are taken,
    1.28 -but rather because the resulting rule must contain O(n) new variables and
    1.29 -an O(n) size concrete record construction. To sidestep this cost, we would
    1.30 -like to avoid case decomposition in proving access/update theorems.
    1.31 -
    1.32 -Record types are defined as isomorphic to tuple types. For instance, a
    1.33 -record type with fields 'a, 'b, 'c and 'd might be introduced as
    1.34 -isomorphic to 'a \<times> ('b \<times> ('c \<times> 'd)). If we balance the tuple tree to
    1.35 -('a \<times> 'b) \<times> ('c \<times> 'd) then accessors can be defined by converting to
    1.36 -the underlying type then using O(log(n)) fst or snd operations.
    1.37 -Updators can be defined similarly, if we introduce a fst_update and
    1.38 -snd_update function. Furthermore, we can prove the access/update
    1.39 -theorem in O(log(n)) steps by using simple rewrites on fst, snd,
    1.40 -fst_update and snd_update.
    1.41 -
    1.42 -The catch is that, although O(log(n)) steps were taken, the underlying
    1.43 -type we converted to is a tuple tree of size O(n). Processing this term
    1.44 -type wastes performance. We avoid this for large n by taking each
    1.45 -subtree of size K and defining a new type isomorphic to that tuple
    1.46 -subtree. The record can now be defined as isomorphic to a tuple tree
    1.47 -of these O(n/K) new types, or, if n > K*K, we can repeat the process,
    1.48 -until the record can be defined in terms of a tuple tree of complexity
    1.49 -less than the constant K.
    1.50 -
    1.51 -If we prove the access/update theorem on this type with the analagous
    1.52 -steps to the tuple tree, we consume O(log(n)^2) time as the intermediate
    1.53 -terms are O(log(n)) in size and the types needed have size bounded by K.
    1.54 -To enable this analagous traversal, we define the functions seen below:
    1.55 -istuple_fst, istuple_snd, istuple_fst_update and istuple_snd_update.
    1.56 -These functions generalise tuple operations by taking a parameter that
    1.57 -encapsulates a tuple isomorphism. The rewrites needed on these functions
    1.58 -now need an additional assumption which is that the isomorphism works.
    1.59 -
    1.60 -These rewrites are typically used in a structured way. They are here
    1.61 -presented as the introduction rule isomorphic_tuple.intros rather than
    1.62 -as a rewrite rule set. The introduction form is an optimisation, as net
    1.63 -matching can be performed at one term location for each step rather than
    1.64 -the simplifier searching the term for possible pattern matches. The rule
    1.65 -set is used as it is viewed outside the locale, with the locale assumption
    1.66 -(that the isomorphism is valid) left as rule assumption. All rules are
    1.67 -structured to aid net matching, using either a point-free form or an
    1.68 -encapsulating predicate.
    1.69 -*}
    1.70 -
    1.71 -typedef ('a, 'b, 'c) tuple_isomorphism
    1.72 -  = "UNIV :: (('a \<Rightarrow> ('b \<times> 'c)) \<times> (('b \<times> 'c) \<Rightarrow> 'a)) set"
    1.73 -  by simp
    1.74 -
    1.75 -constdefs
    1.76 -  "TupleIsomorphism repr abst \<equiv> Abs_tuple_isomorphism (repr, abst)"
    1.77 -
    1.78 -constdefs
    1.79 -  istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b"
    1.80 - "istuple_fst isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in fst \<circ> repr"
    1.81 -  istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c"
    1.82 - "istuple_snd isom \<equiv>  let (repr, abst) = Rep_tuple_isomorphism isom in snd \<circ> repr"
    1.83 -  istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)"
    1.84 - "istuple_fst_update isom \<equiv>
    1.85 -     let (repr, abst) = Rep_tuple_isomorphism isom in
    1.86 -        (\<lambda>f v. abst (f (fst (repr v)), snd (repr v)))"
    1.87 -  istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)"
    1.88 - "istuple_snd_update isom \<equiv>
    1.89 -     let (repr, abst) = Rep_tuple_isomorphism isom in
    1.90 -        (\<lambda>f v. abst (fst (repr v), f (snd (repr v))))"
    1.91 -  istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a"
    1.92 - "istuple_cons isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in curry abst"
    1.93 -
    1.94 -text {*
    1.95 -These predicates are used in the introduction rule set to constrain
    1.96 -matching appropriately. The elimination rules for them produce the
    1.97 -desired theorems once they are proven. The final introduction rules are
    1.98 -used when no further rules from the introduction rule set can apply.
    1.99 -*}
   1.100 -
   1.101 -constdefs
   1.102 -  istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   1.103 - "istuple_surjective_proof_assist x y f \<equiv> f x = y"
   1.104 -  istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a))
   1.105 -                              \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   1.106 - "istuple_update_accessor_cong_assist upd acc
   1.107 -    \<equiv> (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v)
   1.108 -       \<and> (\<forall>v. upd id v = v)"
   1.109 -  istuple_update_accessor_eq_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b)
   1.110 -                              \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   1.111 - "istuple_update_accessor_eq_assist upd acc v f v' x
   1.112 -    \<equiv> upd f v = v' \<and> acc v = x
   1.113 -      \<and> istuple_update_accessor_cong_assist upd acc"
   1.114 -
   1.115 -lemma update_accessor_congruence_foldE:
   1.116 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   1.117 -  and       r: "r = r'" and v: "acc r' = v'"
   1.118 -  and       f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
   1.119 -  shows        "upd f r = upd f' r'"
   1.120 -  using uac r v[symmetric]
   1.121 -  apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
   1.122 -   apply (simp add: istuple_update_accessor_cong_assist_def)
   1.123 -  apply (simp add: f)
   1.124 -  done
   1.125 -
   1.126 -lemma update_accessor_congruence_unfoldE:
   1.127 -  "\<lbrakk> istuple_update_accessor_cong_assist upd acc;
   1.128 -     r = r'; acc r' = v'; \<And>v. v = v' \<Longrightarrow> f v = f' v \<rbrakk>
   1.129 -     \<Longrightarrow> upd f r = upd f' r'"
   1.130 -  apply (erule(2) update_accessor_congruence_foldE)
   1.131 -  apply simp
   1.132 -  done
   1.133 -
   1.134 -lemma istuple_update_accessor_cong_assist_id:
   1.135 -  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
   1.136 -  by (rule ext, simp add: istuple_update_accessor_cong_assist_def)
   1.137 -
   1.138 -lemma update_accessor_noopE:
   1.139 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   1.140 -      and acc: "f (acc x) = acc x"
   1.141 -  shows        "upd f x = x"
   1.142 -  using uac
   1.143 -  by (simp add: acc istuple_update_accessor_cong_assist_id[OF uac, unfolded id_def]
   1.144 -          cong: update_accessor_congruence_unfoldE[OF uac])
   1.145 -
   1.146 -lemma update_accessor_noop_compE:
   1.147 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   1.148 -  assumes acc: "f (acc x) = acc x"
   1.149 -  shows      "upd (g \<circ> f) x = upd g x"
   1.150 -  by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
   1.151 -
   1.152 -lemma update_accessor_cong_assist_idI:
   1.153 -  "istuple_update_accessor_cong_assist id id"
   1.154 -  by (simp add: istuple_update_accessor_cong_assist_def)
   1.155 -
   1.156 -lemma update_accessor_cong_assist_triv:
   1.157 -  "istuple_update_accessor_cong_assist upd acc
   1.158 -       \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   1.159 -  by assumption
   1.160 -
   1.161 -lemma update_accessor_accessor_eqE:
   1.162 -  "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> acc v = x"
   1.163 -  by (simp add: istuple_update_accessor_eq_assist_def)
   1.164 -
   1.165 -lemma update_accessor_updator_eqE:
   1.166 -  "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> upd f v = v'"
   1.167 -  by (simp add: istuple_update_accessor_eq_assist_def)
   1.168 -
   1.169 -lemma istuple_update_accessor_eq_assist_idI:
   1.170 -  "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
   1.171 -  by (simp add: istuple_update_accessor_eq_assist_def
   1.172 -                update_accessor_cong_assist_idI)
   1.173 -
   1.174 -lemma istuple_update_accessor_eq_assist_triv:
   1.175 -  "istuple_update_accessor_eq_assist upd acc v f v' x
   1.176 -     \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
   1.177 -  by assumption
   1.178 -
   1.179 -lemma istuple_update_accessor_cong_from_eq:
   1.180 -  "istuple_update_accessor_eq_assist upd acc v f v' x
   1.181 -     \<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 -  "\<lbrakk> a o b = c o d; \<lbrakk> \<And>v. a (b v) = c (d v) \<rbrakk> \<Longrightarrow> R \<rbrakk> \<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>
   1.198 -     istuple_surjective_proof_assist x y f"
   1.199 -  by (simp add: istuple_surjective_proof_assist_def)
   1.200 -
   1.201 -lemma istuple_surjective_proof_assist_idE:
   1.202 -  "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   1.203 -  by (simp add: istuple_surjective_proof_assist_def)
   1.204 -
   1.205 -locale isomorphic_tuple =
   1.206 -  fixes isom :: "('a, 'b, 'c) tuple_isomorphism" 
   1.207 -       and repr and abst
   1.208 -  defines "repr \<equiv> fst (Rep_tuple_isomorphism isom)"
   1.209 -  defines "abst \<equiv> snd (Rep_tuple_isomorphism isom)"
   1.210 -  assumes repr_inv: "\<And>x. abst (repr x) = x"
   1.211 -  assumes abst_inv: "\<And>y. repr (abst y) = y"
   1.212 -
   1.213 -begin
   1.214 -
   1.215 -lemma repr_inj:
   1.216 -  "(repr x = repr y) = (x = y)"
   1.217 -  apply (rule iffI, simp_all)
   1.218 -  apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
   1.219 -  done
   1.220 -
   1.221 -lemma abst_inj:
   1.222 -  "(abst x = abst y) = (x = y)"
   1.223 -  apply (rule iffI, simp_all)
   1.224 -  apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
   1.225 -  done
   1.226 -
   1.227 -lemma split_Rep:
   1.228 -  "split f (Rep_tuple_isomorphism isom)
   1.229 -     = f repr abst"
   1.230 -  by (simp add: split_def repr_def abst_def)
   1.231 -
   1.232 -lemmas simps = Let_def split_Rep repr_inv abst_inv repr_inj abst_inj
   1.233 -
   1.234 -lemma istuple_access_update_fst_fst:
   1.235 -  "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
   1.236 -    (f o istuple_fst isom) o (istuple_fst_update isom o h) g
   1.237 -          = j o (f o istuple_fst isom)"
   1.238 -  by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
   1.239 -             intro!: ext elim!: o_eq_elim)
   1.240 -
   1.241 -lemma istuple_access_update_snd_snd:
   1.242 -  "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
   1.243 -    (f o istuple_snd isom) o (istuple_snd_update isom o h) g
   1.244 -          = j o (f o istuple_snd isom)"
   1.245 -  by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
   1.246 -             intro!: ext elim!: o_eq_elim)
   1.247 -
   1.248 -lemma istuple_access_update_fst_snd:
   1.249 -  "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
   1.250 -          = id o (f o istuple_fst isom)"
   1.251 -  by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
   1.252 -             intro!: ext elim!: o_eq_elim)
   1.253 -
   1.254 -lemma istuple_access_update_snd_fst:
   1.255 -  "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
   1.256 -          = id o (f o istuple_snd isom)"
   1.257 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
   1.258 -             intro!: ext elim!: o_eq_elim)
   1.259 -
   1.260 -lemma istuple_update_swap_fst_fst:
   1.261 -  "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
   1.262 -    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   1.263 -          = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
   1.264 -  by (clarsimp simp: istuple_fst_update_def simps
   1.265 -             intro!: ext elim!: o_eq_elim)
   1.266 -
   1.267 -lemma istuple_update_swap_snd_snd:
   1.268 -  "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
   1.269 -    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   1.270 -          = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
   1.271 -  by (clarsimp simp: istuple_snd_update_def simps
   1.272 -             intro!: ext elim!: o_eq_elim)
   1.273 -
   1.274 -lemma istuple_update_swap_fst_snd:
   1.275 -  "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
   1.276 -          = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
   1.277 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
   1.278 -             intro!: ext elim!: o_eq_elim)
   1.279 -
   1.280 -lemma istuple_update_swap_snd_fst:
   1.281 -  "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
   1.282 -          = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
   1.283 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
   1.284 -             intro!: ext elim!: o_eq_elim)
   1.285 -
   1.286 -lemma istuple_update_compose_fst_fst:
   1.287 -  "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
   1.288 -    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   1.289 -          = (istuple_fst_update isom o k) (f o g)"
   1.290 -  by (fastsimp simp: istuple_fst_update_def simps
   1.291 -             intro!: ext elim!: o_eq_elim dest: fun_cong)
   1.292 -
   1.293 -lemma istuple_update_compose_snd_snd:
   1.294 -  "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
   1.295 -    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   1.296 -          = (istuple_snd_update isom o k) (f o g)"
   1.297 -  by (fastsimp simp: istuple_snd_update_def simps
   1.298 -             intro!: ext elim!: o_eq_elim dest: fun_cong)
   1.299 -
   1.300 -lemma istuple_surjective_proof_assist_step:
   1.301 -  "\<lbrakk> istuple_surjective_proof_assist v a (istuple_fst isom o f);
   1.302 -     istuple_surjective_proof_assist v b (istuple_snd isom o f) \<rbrakk>
   1.303 -      \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
   1.304 -  by (clarsimp simp: istuple_surjective_proof_assist_def simps
   1.305 -                     istuple_fst_def istuple_snd_def istuple_cons_def)
   1.306 -
   1.307 -lemma istuple_fst_update_accessor_cong_assist:
   1.308 -  "istuple_update_accessor_cong_assist f g \<Longrightarrow>
   1.309 -      istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
   1.310 -  by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   1.311 -                     istuple_fst_update_def istuple_fst_def)
   1.312 -
   1.313 -lemma istuple_snd_update_accessor_cong_assist:
   1.314 -  "istuple_update_accessor_cong_assist f g \<Longrightarrow>
   1.315 -      istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
   1.316 -  by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   1.317 -                     istuple_snd_update_def istuple_snd_def)
   1.318 -
   1.319 -lemma istuple_fst_update_accessor_eq_assist:
   1.320 -  "istuple_update_accessor_eq_assist f g a u a' v \<Longrightarrow>
   1.321 -      istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
   1.322 -              (istuple_cons isom a b) u (istuple_cons isom a' b) v"
   1.323 -  by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def
   1.324 -                     istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   1.325 -
   1.326 -lemma istuple_snd_update_accessor_eq_assist:
   1.327 -  "istuple_update_accessor_eq_assist f g b u b' v \<Longrightarrow>
   1.328 -      istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
   1.329 -              (istuple_cons isom a b) u (istuple_cons isom a b') v"
   1.330 -  by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def
   1.331 -                     istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   1.332 -
   1.333 -lemma istuple_cons_conj_eqI:
   1.334 -  "\<lbrakk> (a = c \<and> b = d \<and> P) = Q \<rbrakk> \<Longrightarrow>
   1.335 -    (istuple_cons isom a b = istuple_cons isom c d \<and> P) = Q"
   1.336 -  by (clarsimp simp: istuple_cons_def simps)
   1.337 -
   1.338 -lemmas intros =
   1.339 -    istuple_access_update_fst_fst
   1.340 -    istuple_access_update_snd_snd
   1.341 -    istuple_access_update_fst_snd
   1.342 -    istuple_access_update_snd_fst
   1.343 -    istuple_update_swap_fst_fst
   1.344 -    istuple_update_swap_snd_snd
   1.345 -    istuple_update_swap_fst_snd
   1.346 -    istuple_update_swap_snd_fst
   1.347 -    istuple_update_compose_fst_fst
   1.348 -    istuple_update_compose_snd_snd
   1.349 -    istuple_surjective_proof_assist_step
   1.350 -    istuple_fst_update_accessor_eq_assist
   1.351 -    istuple_snd_update_accessor_eq_assist
   1.352 -    istuple_fst_update_accessor_cong_assist
   1.353 -    istuple_snd_update_accessor_cong_assist
   1.354 -    istuple_cons_conj_eqI
   1.355 -
   1.356 -end
   1.357 -
   1.358 -lemma isomorphic_tuple_intro:
   1.359 -  assumes repr_inj: "\<And>x y. (repr x = repr y) = (x = y)"
   1.360 -     and abst_inv: "\<And>z. repr (abst z) = z"
   1.361 -  shows "v \<equiv> TupleIsomorphism repr abst \<Longrightarrow> isomorphic_tuple v"
   1.362 -  apply (rule isomorphic_tuple.intro,
   1.363 -         simp_all add: TupleIsomorphism_def Abs_tuple_isomorphism_inverse
   1.364 -                       tuple_isomorphism_def abst_inv)
   1.365 -  apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
   1.366 -  apply (simp add: abst_inv)
   1.367 -  done
   1.368 -
   1.369 -constdefs
   1.370 - "tuple_istuple \<equiv> TupleIsomorphism id id"
   1.371 -
   1.372 -lemma tuple_istuple:
   1.373 -  "isomorphic_tuple tuple_istuple"
   1.374 -  by (simp add: isomorphic_tuple_intro[OF _ _ reflexive] tuple_istuple_def)
   1.375 -
   1.376 -lemma refl_conj_eq:
   1.377 -  "Q = R \<Longrightarrow> (P \<and> Q) = (P \<and> R)"
   1.378 -  by simp
   1.379 -
   1.380 -lemma meta_all_sameI:
   1.381 -  "(\<And>x. PROP P x \<equiv> PROP Q x) \<Longrightarrow> (\<And>x. PROP P x) \<equiv> (\<And>x. PROP Q x)"
   1.382 -  by simp
   1.383 -
   1.384 -lemma istuple_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
   1.385 -  by simp
   1.386 -
   1.387 -lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   1.388 -  by simp
   1.389 -
   1.390 -use "Tools/istuple_support.ML";
   1.391 -
   1.392 -end
     2.1 --- a/src/HOL/Record.thy	Tue Sep 22 13:52:19 2009 +1000
     2.2 +++ b/src/HOL/Record.thy	Wed Sep 23 19:17:48 2009 +1000
     2.3 @@ -1,11 +1,12 @@
     2.4  (*  Title:      HOL/Record.thy
     2.5 -    Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
     2.6 +    Authors:    Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
     2.7 +                Thomas Sewell, NICTA
     2.8  *)
     2.9  
    2.10  header {* Extensible records with structural subtyping *}
    2.11  
    2.12  theory Record
    2.13 -imports Product_Type IsTuple
    2.14 +imports Product_Type
    2.15  uses ("Tools/record.ML")
    2.16  begin
    2.17  
    2.18 @@ -64,6 +65,402 @@
    2.19    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
    2.20    "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
    2.21  
    2.22 +subsection {* Operators and lemmas for types isomorphic to tuples *}
    2.23 +
    2.24 +text {*
    2.25 +Records are isomorphic to compound tuple types. To implement efficient
    2.26 +records, we make this isomorphism explicit. Consider the record
    2.27 +access/update simplification "alpha (beta_update f rec) = alpha rec" for
    2.28 +distinct fields alpha and beta of some record rec with n fields. There
    2.29 +are n^2 such theorems, which prohibits storage of all of them for
    2.30 +large n. The rules can be proved on the fly by case decomposition and
    2.31 +simplification in O(n) time. By creating O(n) isomorphic-tuple types
    2.32 +while defining the record, however, we can prove the access/update
    2.33 +simplification in O(log(n)^2) time.
    2.34 +
    2.35 +The O(n) cost of case decomposition is not because O(n) steps are taken,
    2.36 +but rather because the resulting rule must contain O(n) new variables and
    2.37 +an O(n) size concrete record construction. To sidestep this cost, we would
    2.38 +like to avoid case decomposition in proving access/update theorems.
    2.39 +
    2.40 +Record types are defined as isomorphic to tuple types. For instance, a
    2.41 +record type with fields 'a, 'b, 'c and 'd might be introduced as
    2.42 +isomorphic to 'a \<times> ('b \<times> ('c \<times> 'd)). If we balance the tuple tree to
    2.43 +('a \<times> 'b) \<times> ('c \<times> 'd) then accessors can be defined by converting to
    2.44 +the underlying type then using O(log(n)) fst or snd operations.
    2.45 +Updators can be defined similarly, if we introduce a fst_update and
    2.46 +snd_update function. Furthermore, we can prove the access/update
    2.47 +theorem in O(log(n)) steps by using simple rewrites on fst, snd,
    2.48 +fst_update and snd_update.
    2.49 +
    2.50 +The catch is that, although O(log(n)) steps were taken, the underlying
    2.51 +type we converted to is a tuple tree of size O(n). Processing this term
    2.52 +type wastes performance. We avoid this for large n by taking each
    2.53 +subtree of size K and defining a new type isomorphic to that tuple
    2.54 +subtree. A record can now be defined as isomorphic to a tuple tree
    2.55 +of these O(n/K) new types, or, if n > K*K, we can repeat the process,
    2.56 +until the record can be defined in terms of a tuple tree of complexity
    2.57 +less than the constant K.
    2.58 +
    2.59 +If we prove the access/update theorem on this type with the analagous
    2.60 +steps to the tuple tree, we consume O(log(n)^2) time as the intermediate
    2.61 +terms are O(log(n)) in size and the types needed have size bounded by K.
    2.62 +To enable this analagous traversal, we define the functions seen below:
    2.63 +istuple_fst, istuple_snd, istuple_fst_update and istuple_snd_update.
    2.64 +These functions generalise tuple operations by taking a parameter that
    2.65 +encapsulates a tuple isomorphism. The rewrites needed on these functions
    2.66 +now need an additional assumption which is that the isomorphism works.
    2.67 +
    2.68 +These rewrites are typically used in a structured way. They are here
    2.69 +presented as the introduction rule isomorphic_tuple.intros rather than
    2.70 +as a rewrite rule set. The introduction form is an optimisation, as net
    2.71 +matching can be performed at one term location for each step rather than
    2.72 +the simplifier searching the term for possible pattern matches. The rule
    2.73 +set is used as it is viewed outside the locale, with the locale assumption
    2.74 +(that the isomorphism is valid) left as a rule assumption. All rules are
    2.75 +structured to aid net matching, using either a point-free form or an
    2.76 +encapsulating predicate.
    2.77 +*}
    2.78 +
    2.79 +typedef ('a, 'b, 'c) tuple_isomorphism
    2.80 +  = "UNIV :: (('a \<Rightarrow> ('b \<times> 'c)) \<times> (('b \<times> 'c) \<Rightarrow> 'a)) set"
    2.81 +  by simp
    2.82 +
    2.83 +definition
    2.84 +  "TupleIsomorphism repr abst = Abs_tuple_isomorphism (repr, abst)"
    2.85 +
    2.86 +definition
    2.87 +  istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b"
    2.88 +where
    2.89 + "istuple_fst isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in fst \<circ> repr"
    2.90 +
    2.91 +definition
    2.92 +  istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c"
    2.93 +where
    2.94 + "istuple_snd isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in snd \<circ> repr"
    2.95 +
    2.96 +definition
    2.97 +  istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)"
    2.98 +where
    2.99 + "istuple_fst_update isom \<equiv>
   2.100 +     let (repr, abst) = Rep_tuple_isomorphism isom in
   2.101 +        (\<lambda>f v. abst (f (fst (repr v)), snd (repr v)))"
   2.102 +
   2.103 +definition
   2.104 +  istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)"
   2.105 +where
   2.106 + "istuple_snd_update isom \<equiv>
   2.107 +     let (repr, abst) = Rep_tuple_isomorphism isom in
   2.108 +        (\<lambda>f v. abst (fst (repr v), f (snd (repr v))))"
   2.109 +
   2.110 +definition
   2.111 +  istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a"
   2.112 +where
   2.113 + "istuple_cons isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in curry abst"
   2.114 +
   2.115 +text {*
   2.116 +These predicates are used in the introduction rule set to constrain
   2.117 +matching appropriately. The elimination rules for them produce the
   2.118 +desired theorems once they are proven. The final introduction rules are
   2.119 +used when no further rules from the introduction rule set can apply.
   2.120 +*}
   2.121 +
   2.122 +definition
   2.123 +  istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   2.124 +where
   2.125 + "istuple_surjective_proof_assist x y f \<equiv> (f x = y)"
   2.126 +
   2.127 +definition
   2.128 +  istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a))
   2.129 +                              \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   2.130 +where
   2.131 + "istuple_update_accessor_cong_assist upd acc
   2.132 +    \<equiv> (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v)
   2.133 +       \<and> (\<forall>v. upd id v = v)"
   2.134 +
   2.135 +definition
   2.136 +  istuple_update_accessor_eq_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b)
   2.137 +                              \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   2.138 +where
   2.139 + "istuple_update_accessor_eq_assist upd acc v f v' x
   2.140 +    \<equiv> upd f v = v' \<and> acc v = x
   2.141 +      \<and> istuple_update_accessor_cong_assist upd acc"
   2.142 +
   2.143 +lemma update_accessor_congruence_foldE:
   2.144 +  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   2.145 +  and       r: "r = r'" and v: "acc r' = v'"
   2.146 +  and       f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
   2.147 +  shows        "upd f r = upd f' r'"
   2.148 +  using uac r v[symmetric]
   2.149 +  apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
   2.150 +   apply (simp add: istuple_update_accessor_cong_assist_def)
   2.151 +  apply (simp add: f)
   2.152 +  done
   2.153 +
   2.154 +lemma update_accessor_congruence_unfoldE:
   2.155 +  "\<lbrakk> istuple_update_accessor_cong_assist upd acc;
   2.156 +     r = r'; acc r' = v'; \<And>v. v = v' \<Longrightarrow> f v = f' v \<rbrakk>
   2.157 +     \<Longrightarrow> upd f r = upd f' r'"
   2.158 +  apply (erule(2) update_accessor_congruence_foldE)
   2.159 +  apply simp
   2.160 +  done
   2.161 +
   2.162 +lemma istuple_update_accessor_cong_assist_id:
   2.163 +  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
   2.164 +  by (rule ext, simp add: istuple_update_accessor_cong_assist_def)
   2.165 +
   2.166 +lemma update_accessor_noopE:
   2.167 +  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   2.168 +      and acc: "f (acc x) = acc x"
   2.169 +  shows        "upd f x = x"
   2.170 +  using uac
   2.171 +  by (simp add: acc istuple_update_accessor_cong_assist_id[OF uac, unfolded id_def]
   2.172 +          cong: update_accessor_congruence_unfoldE[OF uac])
   2.173 +
   2.174 +lemma update_accessor_noop_compE:
   2.175 +  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   2.176 +  assumes acc: "f (acc x) = acc x"
   2.177 +  shows      "upd (g \<circ> f) x = upd g x"
   2.178 +  by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
   2.179 +
   2.180 +lemma update_accessor_cong_assist_idI:
   2.181 +  "istuple_update_accessor_cong_assist id id"
   2.182 +  by (simp add: istuple_update_accessor_cong_assist_def)
   2.183 +
   2.184 +lemma update_accessor_cong_assist_triv:
   2.185 +  "istuple_update_accessor_cong_assist upd acc
   2.186 +       \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   2.187 +  by assumption
   2.188 +
   2.189 +lemma update_accessor_accessor_eqE:
   2.190 +  "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> acc v = x"
   2.191 +  by (simp add: istuple_update_accessor_eq_assist_def)
   2.192 +
   2.193 +lemma update_accessor_updator_eqE:
   2.194 +  "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> upd f v = v'"
   2.195 +  by (simp add: istuple_update_accessor_eq_assist_def)
   2.196 +
   2.197 +lemma istuple_update_accessor_eq_assist_idI:
   2.198 +  "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
   2.199 +  by (simp add: istuple_update_accessor_eq_assist_def
   2.200 +                update_accessor_cong_assist_idI)
   2.201 +
   2.202 +lemma istuple_update_accessor_eq_assist_triv:
   2.203 +  "istuple_update_accessor_eq_assist upd acc v f v' x
   2.204 +     \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
   2.205 +  by assumption
   2.206 +
   2.207 +lemma istuple_update_accessor_cong_from_eq:
   2.208 +  "istuple_update_accessor_eq_assist upd acc v f v' x
   2.209 +     \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   2.210 +  by (simp add: istuple_update_accessor_eq_assist_def)
   2.211 +
   2.212 +lemma o_eq_dest:
   2.213 +  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
   2.214 +  apply (clarsimp simp: o_def)
   2.215 +  apply (erule fun_cong)
   2.216 +  done
   2.217 +
   2.218 +lemma o_eq_elim:
   2.219 +  "\<lbrakk> a o b = c o d; \<lbrakk> \<And>v. a (b v) = c (d v) \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
   2.220 +  apply (erule meta_mp)
   2.221 +  apply (erule o_eq_dest)
   2.222 +  done
   2.223 +
   2.224 +lemma istuple_surjective_proof_assistI:
   2.225 +  "f x = y \<Longrightarrow>
   2.226 +     istuple_surjective_proof_assist x y f"
   2.227 +  by (simp add: istuple_surjective_proof_assist_def)
   2.228 +
   2.229 +lemma istuple_surjective_proof_assist_idE:
   2.230 +  "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   2.231 +  by (simp add: istuple_surjective_proof_assist_def)
   2.232 +
   2.233 +locale isomorphic_tuple =
   2.234 +  fixes isom :: "('a, 'b, 'c) tuple_isomorphism" 
   2.235 +       and repr and abst
   2.236 +  defines "repr \<equiv> fst (Rep_tuple_isomorphism isom)"
   2.237 +  defines "abst \<equiv> snd (Rep_tuple_isomorphism isom)"
   2.238 +  assumes repr_inv: "\<And>x. abst (repr x) = x"
   2.239 +  assumes abst_inv: "\<And>y. repr (abst y) = y"
   2.240 +
   2.241 +begin
   2.242 +
   2.243 +lemma repr_inj:
   2.244 +  "(repr x = repr y) = (x = y)"
   2.245 +  apply (rule iffI, simp_all)
   2.246 +  apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
   2.247 +  done
   2.248 +
   2.249 +lemma abst_inj:
   2.250 +  "(abst x = abst y) = (x = y)"
   2.251 +  apply (rule iffI, simp_all)
   2.252 +  apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
   2.253 +  done
   2.254 +
   2.255 +lemma split_Rep:
   2.256 +  "split f (Rep_tuple_isomorphism isom)
   2.257 +     = f repr abst"
   2.258 +  by (simp add: split_def repr_def abst_def)
   2.259 +
   2.260 +lemmas simps = Let_def split_Rep repr_inv abst_inv repr_inj abst_inj
   2.261 +
   2.262 +lemma istuple_access_update_fst_fst:
   2.263 +  "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
   2.264 +    (f o istuple_fst isom) o (istuple_fst_update isom o h) g
   2.265 +          = j o (f o istuple_fst isom)"
   2.266 +  by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
   2.267 +             intro!: ext elim!: o_eq_elim)
   2.268 +
   2.269 +lemma istuple_access_update_snd_snd:
   2.270 +  "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
   2.271 +    (f o istuple_snd isom) o (istuple_snd_update isom o h) g
   2.272 +          = j o (f o istuple_snd isom)"
   2.273 +  by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
   2.274 +             intro!: ext elim!: o_eq_elim)
   2.275 +
   2.276 +lemma istuple_access_update_fst_snd:
   2.277 +  "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
   2.278 +          = id o (f o istuple_fst isom)"
   2.279 +  by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
   2.280 +             intro!: ext elim!: o_eq_elim)
   2.281 +
   2.282 +lemma istuple_access_update_snd_fst:
   2.283 +  "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
   2.284 +          = id o (f o istuple_snd isom)"
   2.285 +  by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
   2.286 +             intro!: ext elim!: o_eq_elim)
   2.287 +
   2.288 +lemma istuple_update_swap_fst_fst:
   2.289 +  "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
   2.290 +    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   2.291 +          = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
   2.292 +  by (clarsimp simp: istuple_fst_update_def simps
   2.293 +             intro!: ext elim!: o_eq_elim)
   2.294 +
   2.295 +lemma istuple_update_swap_snd_snd:
   2.296 +  "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
   2.297 +    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   2.298 +          = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
   2.299 +  by (clarsimp simp: istuple_snd_update_def simps
   2.300 +             intro!: ext elim!: o_eq_elim)
   2.301 +
   2.302 +lemma istuple_update_swap_fst_snd:
   2.303 +  "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
   2.304 +          = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
   2.305 +  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
   2.306 +             intro!: ext elim!: o_eq_elim)
   2.307 +
   2.308 +lemma istuple_update_swap_snd_fst:
   2.309 +  "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
   2.310 +          = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
   2.311 +  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
   2.312 +             intro!: ext elim!: o_eq_elim)
   2.313 +
   2.314 +lemma istuple_update_compose_fst_fst:
   2.315 +  "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
   2.316 +    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   2.317 +          = (istuple_fst_update isom o k) (f o g)"
   2.318 +  by (fastsimp simp: istuple_fst_update_def simps
   2.319 +             intro!: ext elim!: o_eq_elim dest: fun_cong)
   2.320 +
   2.321 +lemma istuple_update_compose_snd_snd:
   2.322 +  "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
   2.323 +    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   2.324 +          = (istuple_snd_update isom o k) (f o g)"
   2.325 +  by (fastsimp simp: istuple_snd_update_def simps
   2.326 +             intro!: ext elim!: o_eq_elim dest: fun_cong)
   2.327 +
   2.328 +lemma istuple_surjective_proof_assist_step:
   2.329 +  "\<lbrakk> istuple_surjective_proof_assist v a (istuple_fst isom o f);
   2.330 +     istuple_surjective_proof_assist v b (istuple_snd isom o f) \<rbrakk>
   2.331 +      \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
   2.332 +  by (clarsimp simp: istuple_surjective_proof_assist_def simps
   2.333 +                     istuple_fst_def istuple_snd_def istuple_cons_def)
   2.334 +
   2.335 +lemma istuple_fst_update_accessor_cong_assist:
   2.336 +  "istuple_update_accessor_cong_assist f g \<Longrightarrow>
   2.337 +      istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
   2.338 +  by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   2.339 +                     istuple_fst_update_def istuple_fst_def)
   2.340 +
   2.341 +lemma istuple_snd_update_accessor_cong_assist:
   2.342 +  "istuple_update_accessor_cong_assist f g \<Longrightarrow>
   2.343 +      istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
   2.344 +  by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   2.345 +                     istuple_snd_update_def istuple_snd_def)
   2.346 +
   2.347 +lemma istuple_fst_update_accessor_eq_assist:
   2.348 +  "istuple_update_accessor_eq_assist f g a u a' v \<Longrightarrow>
   2.349 +      istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
   2.350 +              (istuple_cons isom a b) u (istuple_cons isom a' b) v"
   2.351 +  by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def
   2.352 +                     istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   2.353 +
   2.354 +lemma istuple_snd_update_accessor_eq_assist:
   2.355 +  "istuple_update_accessor_eq_assist f g b u b' v \<Longrightarrow>
   2.356 +      istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
   2.357 +              (istuple_cons isom a b) u (istuple_cons isom a b') v"
   2.358 +  by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def
   2.359 +                     istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   2.360 +
   2.361 +lemma istuple_cons_conj_eqI:
   2.362 +  "\<lbrakk> (a = c \<and> b = d \<and> P) = Q \<rbrakk> \<Longrightarrow>
   2.363 +    (istuple_cons isom a b = istuple_cons isom c d \<and> P) = Q"
   2.364 +  by (clarsimp simp: istuple_cons_def simps)
   2.365 +
   2.366 +lemmas intros =
   2.367 +    istuple_access_update_fst_fst
   2.368 +    istuple_access_update_snd_snd
   2.369 +    istuple_access_update_fst_snd
   2.370 +    istuple_access_update_snd_fst
   2.371 +    istuple_update_swap_fst_fst
   2.372 +    istuple_update_swap_snd_snd
   2.373 +    istuple_update_swap_fst_snd
   2.374 +    istuple_update_swap_snd_fst
   2.375 +    istuple_update_compose_fst_fst
   2.376 +    istuple_update_compose_snd_snd
   2.377 +    istuple_surjective_proof_assist_step
   2.378 +    istuple_fst_update_accessor_eq_assist
   2.379 +    istuple_snd_update_accessor_eq_assist
   2.380 +    istuple_fst_update_accessor_cong_assist
   2.381 +    istuple_snd_update_accessor_cong_assist
   2.382 +    istuple_cons_conj_eqI
   2.383 +
   2.384 +end
   2.385 +
   2.386 +lemma isomorphic_tuple_intro:
   2.387 +  assumes repr_inj: "\<And>x y. (repr x = repr y) = (x = y)"
   2.388 +     and abst_inv: "\<And>z. repr (abst z) = z"
   2.389 +  shows "v \<equiv> TupleIsomorphism repr abst \<Longrightarrow> isomorphic_tuple v"
   2.390 +  apply (rule isomorphic_tuple.intro,
   2.391 +         simp_all add: TupleIsomorphism_def Abs_tuple_isomorphism_inverse
   2.392 +                       tuple_isomorphism_def abst_inv)
   2.393 +  apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
   2.394 +  apply (simp add: abst_inv)
   2.395 +  done
   2.396 +
   2.397 +definition
   2.398 + "tuple_istuple \<equiv> TupleIsomorphism id id"
   2.399 +
   2.400 +lemma tuple_istuple:
   2.401 +  "isomorphic_tuple tuple_istuple"
   2.402 +  by (simp add: isomorphic_tuple_intro[OF _ _ reflexive] tuple_istuple_def)
   2.403 +
   2.404 +lemma refl_conj_eq:
   2.405 +  "Q = R \<Longrightarrow> (P \<and> Q) = (P \<and> R)"
   2.406 +  by simp
   2.407 +
   2.408 +lemma meta_all_sameI:
   2.409 +  "(\<And>x. PROP P x \<equiv> PROP Q x) \<Longrightarrow> (\<And>x. PROP P x) \<equiv> (\<And>x. PROP Q x)"
   2.410 +  by simp
   2.411 +
   2.412 +lemma istuple_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
   2.413 +  by simp
   2.414 +
   2.415 +lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   2.416 +  by simp
   2.417 +
   2.418  use "Tools/record.ML"
   2.419  setup Record.setup
   2.420  
     3.1 --- a/src/HOL/Tools/istuple_support.ML	Tue Sep 22 13:52:19 2009 +1000
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,149 +0,0 @@
     3.4 -(*  Title:	HOL/Tools/ntuple_support.ML
     3.5 -    Author:	Thomas Sewell, NICTA
     3.6 -
     3.7 -Support for defining instances of tuple-like types and supplying
     3.8 -introduction rules needed by the record package.
     3.9 -*)
    3.10 -
    3.11 -
    3.12 -signature ISTUPLE_SUPPORT =
    3.13 -sig
    3.14 -  val add_istuple_type: bstring * string list -> (typ * typ) -> theory ->
    3.15 -            (term * term * theory);
    3.16 -
    3.17 -  val mk_cons_tuple: term * term -> term;
    3.18 -  val dest_cons_tuple: term -> term * term;
    3.19 -
    3.20 -  val istuple_intros_tac: theory -> int -> tactic;
    3.21 -
    3.22 -  val named_cterm_instantiate: (string * cterm) list -> thm -> thm;
    3.23 -end;
    3.24 -
    3.25 -structure IsTupleSupport : ISTUPLE_SUPPORT =
    3.26 -struct
    3.27 -
    3.28 -val isomN = "_TupleIsom";
    3.29 -val defN = "_def";
    3.30 -
    3.31 -val istuple_UNIV_I = @{thm "istuple_UNIV_I"};
    3.32 -val istuple_True_simp = @{thm "istuple_True_simp"};
    3.33 -
    3.34 -val istuple_intro = @{thm "isomorphic_tuple_intro"};
    3.35 -val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"});
    3.36 -
    3.37 -val constname = fst o dest_Const;
    3.38 -val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple});
    3.39 -
    3.40 -val istuple_constN = constname @{term isomorphic_tuple};
    3.41 -val istuple_consN = constname @{term istuple_cons};
    3.42 -
    3.43 -val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"});
    3.44 -
    3.45 -fun named_cterm_instantiate values thm = let
    3.46 -    fun match name (Var ((name', _), _)) = name = name'
    3.47 -      | match name _ = false;
    3.48 -    fun getvar name = case (find_first (match name)
    3.49 -                                    (OldTerm.term_vars (prop_of thm)))
    3.50 -      of SOME var => cterm_of (theory_of_thm thm) var
    3.51 -       | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
    3.52 -  in
    3.53 -    cterm_instantiate (map (apfst getvar) values) thm
    3.54 -  end;
    3.55 -
    3.56 -structure IsTupleThms = TheoryDataFun
    3.57 -(
    3.58 -  type T = thm Symtab.table;
    3.59 -  val empty = Symtab.make [tuple_istuple];
    3.60 -  val copy = I;
    3.61 -  val extend = I;
    3.62 -  val merge = K (Symtab.merge Thm.eq_thm_prop);
    3.63 -);
    3.64 -
    3.65 -fun do_typedef name repT alphas thy =
    3.66 -  let
    3.67 -    fun get_thms thy name =
    3.68 -      let
    3.69 -        val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT,
    3.70 -          Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name;
    3.71 -        val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp];
    3.72 -      in (map rewrite_rule [rep_inject, abs_inverse],
    3.73 -            Const (absN, repT --> absT), absT) end;
    3.74 -  in
    3.75 -    thy
    3.76 -    |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
    3.77 -    |-> (fn (name, _) => `(fn thy => get_thms thy name))
    3.78 -  end;
    3.79 -
    3.80 -fun mk_cons_tuple (left, right) = let
    3.81 -    val (leftT, rightT) = (fastype_of left, fastype_of right);
    3.82 -    val prodT           = HOLogic.mk_prodT (leftT, rightT);
    3.83 -    val isomT           = Type (tup_isom_typeN, [prodT, leftT, rightT]);
    3.84 -  in
    3.85 -    Const (istuple_consN, isomT --> leftT --> rightT --> prodT)
    3.86 -      $ Const (fst tuple_istuple, isomT) $ left $ right
    3.87 -  end;
    3.88 -
    3.89 -fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right)
    3.90 -  = if ic = istuple_consN then (left, right)
    3.91 -    else raise TERM ("dest_cons_tuple", [v])
    3.92 -  | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]);
    3.93 -
    3.94 -fun add_istuple_type (name, alphas) (leftT, rightT) thy =
    3.95 -let
    3.96 -  val repT = HOLogic.mk_prodT (leftT, rightT);
    3.97 -
    3.98 -  val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
    3.99 -    thy
   3.100 -    |> do_typedef name repT alphas
   3.101 -    ||> Sign.add_path name;
   3.102 -
   3.103 -  (* construct a type and body for the isomorphism constant by
   3.104 -     instantiating the theorem to which the definition will be applied *)
   3.105 -  val intro_inst = rep_inject RS
   3.106 -                   (named_cterm_instantiate [("abst", cterm_of typ_thy absC)]
   3.107 -                        istuple_intro);
   3.108 -  val (_, body)  = Logic.dest_equals (List.last (prems_of intro_inst));
   3.109 -  val isomT      = fastype_of body;
   3.110 -  val isomBind   = Binding.name (name ^ isomN);
   3.111 -  val isom       = Const (Sign.full_name typ_thy isomBind, isomT);
   3.112 -  val isom_spec  = (name ^ isomN ^ defN, Logic.mk_equals (isom, body));
   3.113 -
   3.114 -  val ([isom_def], cdef_thy) =
   3.115 -    typ_thy
   3.116 -    |> Sign.add_consts_i [Syntax.no_syn (isomBind, isomT)]
   3.117 -    |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
   3.118 -
   3.119 -  val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
   3.120 -  val cons    = Const (istuple_consN, isomT --> leftT --> rightT --> absT)
   3.121 -
   3.122 -  val thm_thy =
   3.123 -    cdef_thy
   3.124 -    |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop
   3.125 -                           (constname isom, istuple))
   3.126 -    |> Sign.parent_path;
   3.127 -in
   3.128 -  (isom, cons $ isom, thm_thy)
   3.129 -end;
   3.130 -
   3.131 -fun istuple_intros_tac thy = let
   3.132 -    val isthms  = IsTupleThms.get thy;
   3.133 -    fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
   3.134 -    val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let
   3.135 -        val goal' = Envir.beta_eta_contract goal;
   3.136 -        val isom  = case goal' of (Const tp $ (Const pr $ Const is))
   3.137 -                    => if fst tp = "Trueprop" andalso fst pr = istuple_constN
   3.138 -                       then Const is
   3.139 -                       else err "unexpected goal predicate" goal'
   3.140 -            | _ => err "unexpected goal format" goal';
   3.141 -        val isthm = case Symtab.lookup isthms (constname isom) of
   3.142 -                    SOME isthm => isthm
   3.143 -                  | NONE => err "no thm found for constant" isom;
   3.144 -      in rtac isthm n end);
   3.145 -  in
   3.146 -    fn n => resolve_from_net_tac istuple_intros n
   3.147 -            THEN use_istuple_thm_tac n
   3.148 -  end;
   3.149 -
   3.150 -end;
   3.151 -
   3.152 -
     4.1 --- a/src/HOL/Tools/record.ML	Tue Sep 22 13:52:19 2009 +1000
     4.2 +++ b/src/HOL/Tools/record.ML	Wed Sep 23 19:17:48 2009 +1000
     4.3 @@ -52,6 +52,146 @@
     4.4  end;
     4.5  
     4.6  
     4.7 +signature ISTUPLE_SUPPORT =
     4.8 +sig
     4.9 +  val add_istuple_type: bstring * string list -> (typ * typ) -> theory ->
    4.10 +            (term * term * theory);
    4.11 +
    4.12 +  val mk_cons_tuple: term * term -> term;
    4.13 +  val dest_cons_tuple: term -> term * term;
    4.14 +
    4.15 +  val istuple_intros_tac: theory -> int -> tactic;
    4.16 +
    4.17 +  val named_cterm_instantiate: (string * cterm) list -> thm -> thm;
    4.18 +end;
    4.19 +
    4.20 +structure IsTupleSupport : ISTUPLE_SUPPORT =
    4.21 +struct
    4.22 +
    4.23 +val isomN = "_TupleIsom";
    4.24 +val defN = "_def";
    4.25 +
    4.26 +val istuple_UNIV_I = @{thm "istuple_UNIV_I"};
    4.27 +val istuple_True_simp = @{thm "istuple_True_simp"};
    4.28 +
    4.29 +val istuple_intro = @{thm "isomorphic_tuple_intro"};
    4.30 +val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"});
    4.31 +
    4.32 +val constname = fst o dest_Const;
    4.33 +val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple});
    4.34 +
    4.35 +val istuple_constN = constname @{term isomorphic_tuple};
    4.36 +val istuple_consN = constname @{term istuple_cons};
    4.37 +
    4.38 +val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"});
    4.39 +
    4.40 +fun named_cterm_instantiate values thm = let
    4.41 +    fun match name (Var ((name', _), _)) = name = name'
    4.42 +      | match name _ = false;
    4.43 +    fun getvar name = case (find_first (match name)
    4.44 +                                    (OldTerm.term_vars (prop_of thm)))
    4.45 +      of SOME var => cterm_of (theory_of_thm thm) var
    4.46 +       | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
    4.47 +  in
    4.48 +    cterm_instantiate (map (apfst getvar) values) thm
    4.49 +  end;
    4.50 +
    4.51 +structure IsTupleThms = TheoryDataFun
    4.52 +(
    4.53 +  type T = thm Symtab.table;
    4.54 +  val empty = Symtab.make [tuple_istuple];
    4.55 +  val copy = I;
    4.56 +  val extend = I;
    4.57 +  val merge = K (Symtab.merge Thm.eq_thm_prop);
    4.58 +);
    4.59 +
    4.60 +fun do_typedef name repT alphas thy =
    4.61 +  let
    4.62 +    fun get_thms thy name =
    4.63 +      let
    4.64 +        val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT,
    4.65 +          Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name;
    4.66 +        val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp];
    4.67 +      in (map rewrite_rule [rep_inject, abs_inverse],
    4.68 +            Const (absN, repT --> absT), absT) end;
    4.69 +  in
    4.70 +    thy
    4.71 +    |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
    4.72 +    |-> (fn (name, _) => `(fn thy => get_thms thy name))
    4.73 +  end;
    4.74 +
    4.75 +fun mk_cons_tuple (left, right) = let
    4.76 +    val (leftT, rightT) = (fastype_of left, fastype_of right);
    4.77 +    val prodT           = HOLogic.mk_prodT (leftT, rightT);
    4.78 +    val isomT           = Type (tup_isom_typeN, [prodT, leftT, rightT]);
    4.79 +  in
    4.80 +    Const (istuple_consN, isomT --> leftT --> rightT --> prodT)
    4.81 +      $ Const (fst tuple_istuple, isomT) $ left $ right
    4.82 +  end;
    4.83 +
    4.84 +fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right)
    4.85 +  = if ic = istuple_consN then (left, right)
    4.86 +    else raise TERM ("dest_cons_tuple", [v])
    4.87 +  | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]);
    4.88 +
    4.89 +fun add_istuple_type (name, alphas) (leftT, rightT) thy =
    4.90 +let
    4.91 +  val repT = HOLogic.mk_prodT (leftT, rightT);
    4.92 +
    4.93 +  val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
    4.94 +    thy
    4.95 +    |> do_typedef name repT alphas
    4.96 +    ||> Sign.add_path name;
    4.97 +
    4.98 +  (* construct a type and body for the isomorphism constant by
    4.99 +     instantiating the theorem to which the definition will be applied *)
   4.100 +  val intro_inst = rep_inject RS
   4.101 +                   (named_cterm_instantiate [("abst", cterm_of typ_thy absC)]
   4.102 +                        istuple_intro);
   4.103 +  val (_, body)  = Logic.dest_equals (List.last (prems_of intro_inst));
   4.104 +  val isomT      = fastype_of body;
   4.105 +  val isom_bind  = Binding.name (name ^ isomN);
   4.106 +  val isom       = Const (Sign.full_name typ_thy isom_bind, isomT);
   4.107 +  val isom_spec  = (name ^ isomN ^ defN, Logic.mk_equals (isom, body));
   4.108 +
   4.109 +  val ([isom_def], cdef_thy) =
   4.110 +    typ_thy
   4.111 +    |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
   4.112 +    |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
   4.113 +
   4.114 +  val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
   4.115 +  val cons    = Const (istuple_consN, isomT --> leftT --> rightT --> absT)
   4.116 +
   4.117 +  val thm_thy =
   4.118 +    cdef_thy
   4.119 +    |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop
   4.120 +                           (constname isom, istuple))
   4.121 +    |> Sign.parent_path;
   4.122 +in
   4.123 +  (isom, cons $ isom, thm_thy)
   4.124 +end;
   4.125 +
   4.126 +fun istuple_intros_tac thy = let
   4.127 +    val isthms  = IsTupleThms.get thy;
   4.128 +    fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
   4.129 +    val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let
   4.130 +        val goal' = Envir.beta_eta_contract goal;
   4.131 +        val isom  = case goal' of (Const tp $ (Const pr $ Const is))
   4.132 +                    => if fst tp = "Trueprop" andalso fst pr = istuple_constN
   4.133 +                       then Const is
   4.134 +                       else err "unexpected goal predicate" goal'
   4.135 +            | _ => err "unexpected goal format" goal';
   4.136 +        val isthm = case Symtab.lookup isthms (constname isom) of
   4.137 +                    SOME isthm => isthm
   4.138 +                  | NONE => err "no thm found for constant" isom;
   4.139 +      in rtac isthm n end);
   4.140 +  in
   4.141 +    fn n => resolve_from_net_tac istuple_intros n
   4.142 +            THEN use_istuple_thm_tac n
   4.143 +  end;
   4.144 +
   4.145 +end;
   4.146 +
   4.147  structure Record: RECORD =
   4.148  struct
   4.149  
   4.150 @@ -68,6 +208,7 @@
   4.151  val o_assoc = @{thm "o_assoc"};
   4.152  val id_apply = @{thm id_apply};
   4.153  val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
   4.154 +val Not_eq_iff = @{thm Not_eq_iff};
   4.155  
   4.156  val refl_conj_eq = thm "refl_conj_eq";
   4.157  val meta_all_sameI = thm "meta_all_sameI";
   4.158 @@ -966,14 +1107,14 @@
   4.159      val T = range_type (fastype_of f);
   4.160    in mk_comp (Const ("Fun.id", T --> T)) f end;
   4.161  
   4.162 -fun get_updfuns (upd $ _ $ t) = upd :: get_updfuns t
   4.163 -  | get_updfuns _             = [];
   4.164 +fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
   4.165 +  | get_upd_funs _             = [];
   4.166  
   4.167  fun get_accupd_simps thy term defset intros_tac = let
   4.168      val (acc, [body]) = strip_comb term;
   4.169      val recT          = domain_type (fastype_of acc);
   4.170 -    val updfuns       = sort_distinct TermOrd.fast_term_ord
   4.171 -                           (get_updfuns body);
   4.172 +    val upd_funs      = sort_distinct TermOrd.fast_term_ord
   4.173 +                           (get_upd_funs body);
   4.174      fun get_simp upd  = let
   4.175          val T    = domain_type (fastype_of upd);
   4.176          val lhs  = mk_comp acc (upd $ Free ("f", T));
   4.177 @@ -987,7 +1128,7 @@
   4.178          val dest = if is_sel_upd_pair thy acc upd
   4.179                     then o_eq_dest else o_eq_id_dest;
   4.180        in standard (othm RS dest) end;
   4.181 -  in map get_simp updfuns end;
   4.182 +  in map get_simp upd_funs end;
   4.183  
   4.184  structure SymSymTab = Table(type key = string * string
   4.185                              val ord = prod_ord fast_string_ord fast_string_ord);
   4.186 @@ -1009,26 +1150,26 @@
   4.187  
   4.188  fun get_updupd_simps thy term defset intros_tac = let
   4.189      val recT          = fastype_of term;
   4.190 -    val updfuns       = get_updfuns term;
   4.191 +    val upd_funs      = get_upd_funs term;
   4.192      val cname         = fst o dest_Const;
   4.193      fun getswap u u'  = get_updupd_simp thy defset intros_tac u u'
   4.194                                (cname u = cname u');
   4.195 -    fun buildswapstoeq upd [] swaps = swaps
   4.196 -      | buildswapstoeq upd (u::us) swaps = let
   4.197 +    fun build_swaps_to_eq upd [] swaps = swaps
   4.198 +      | build_swaps_to_eq upd (u::us) swaps = let
   4.199               val key      = (cname u, cname upd);
   4.200               val newswaps = if SymSymTab.defined swaps key then swaps
   4.201                              else SymSymTab.insert (K true)
   4.202                                       (key, getswap u upd) swaps;
   4.203            in if cname u = cname upd then newswaps
   4.204 -             else buildswapstoeq upd us newswaps end;
   4.205 -    fun swapsneeded []      prev seen swaps = map snd (SymSymTab.dest swaps)
   4.206 -      | swapsneeded (u::us) prev seen swaps =
   4.207 +             else build_swaps_to_eq upd us newswaps end;
   4.208 +    fun swaps_needed []      prev seen swaps = map snd (SymSymTab.dest swaps)
   4.209 +      | swaps_needed (u::us) prev seen swaps =
   4.210             if Symtab.defined seen (cname u)
   4.211 -           then swapsneeded us prev seen
   4.212 -                   (buildswapstoeq u prev swaps)
   4.213 -           else swapsneeded us (u::prev)
   4.214 +           then swaps_needed us prev seen
   4.215 +                   (build_swaps_to_eq u prev swaps)
   4.216 +           else swaps_needed us (u::prev)
   4.217                     (Symtab.insert (K true) (cname u, ()) seen) swaps;
   4.218 -  in swapsneeded updfuns [] Symtab.empty SymSymTab.empty end;
   4.219 +  in swaps_needed upd_funs [] Symtab.empty SymSymTab.empty end;
   4.220  
   4.221  val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
   4.222  
   4.223 @@ -2222,14 +2363,13 @@
   4.224  
   4.225      fun split_ex_prf () =
   4.226        let
   4.227 -        val ss   = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1];
   4.228 -        val [Pv] = OldTerm.term_vars (prop_of split_object);
   4.229 -        val cPv  = cterm_of defs_thy Pv;
   4.230 -        val cP   = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
   4.231 -        val so3  = cterm_instantiate ([(cPv, cP)]) split_object;
   4.232 -        val so4  = simplify ss so3;
   4.233 +        val ss    = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff];
   4.234 +        val P_nm  = fst (dest_Free P);
   4.235 +        val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
   4.236 +        val so'   = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
   4.237 +        val so''  = simplify ss so';
   4.238        in
   4.239 -        prove_standard [] split_ex_prop (fn prems => resolve_tac [so4] 1)
   4.240 +        prove_standard [] split_ex_prop (fn prems => resolve_tac [so''] 1)
   4.241        end;
   4.242      val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
   4.243