Simplification of various aspects of the IsTuple component
authorThomas Sewell <tsewell@nicta.com.au>
Thu Sep 10 16:38:18 2009 +1000 (2009-09-10)
changeset 32745192d58483fdf
parent 32744 50406c4951d9
child 32746 2f1701a6d4e8
Simplification of various aspects of the IsTuple component
of the new record package. Extensive documentation added in
IsTuple.thy - it should now be possible to figure out what's
going on from the sources supplied.
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	Thu Sep 10 15:18:43 2009 +1000
     1.2 +++ b/src/HOL/IsTuple.thy	Thu Sep 10 16:38:18 2009 +1000
     1.3 @@ -1,20 +1,95 @@
     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 type with n fields. There
    1.21 +are n^2 such theorems, which is 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. These
    1.56 +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. With a little
    1.61 +thinking they can be presented as an introduction rule set rather than
    1.62 +a rewrite rule set. This is an optimisation, as net matching can be
    1.63 +performed at one term location for each step rather than the simplifier
    1.64 +searching the term for possible applications.
    1.65 +*}
    1.66 +
    1.67 +typedef ('a, 'b, 'c) tuple_isomorphism
    1.68 +  = "UNIV :: (('a \<Rightarrow> ('b \<times> 'c)) \<times> (('b \<times> 'c) \<Rightarrow> 'a)) set"
    1.69 +  by simp
    1.70 +
    1.71  constdefs
    1.72 -  istuple_fst :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.73 - "istuple_fst isom \<equiv> (fst \<circ> isom)"
    1.74 -  istuple_snd :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.75 - "istuple_snd isom \<equiv> (snd \<circ> isom)"
    1.76 -  istuple_fst_update :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> (('b \<times> 'c) \<Rightarrow> 'a)
    1.77 -                           \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)"
    1.78 - "istuple_fst_update isom inv \<equiv> \<lambda>f v. inv (f (fst (isom v)), snd (isom v))"
    1.79 -  istuple_snd_update :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> (('b \<times> 'c) \<Rightarrow> 'a)
    1.80 -                           \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)"
    1.81 - "istuple_snd_update isom inv \<equiv> \<lambda>f v. inv (fst (isom v), f (snd (isom v)))"
    1.82 +  "TupleIsomorphism repr abst \<equiv> Abs_tuple_isomorphism (repr, abst)"
    1.83 +
    1.84 +constdefs
    1.85 +  istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b"
    1.86 + "istuple_fst isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in fst \<circ> repr"
    1.87 +  istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c"
    1.88 + "istuple_snd isom \<equiv>  let (repr, abst) = Rep_tuple_isomorphism isom in snd \<circ> repr"
    1.89 +  istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)"
    1.90 + "istuple_fst_update isom \<equiv>
    1.91 +     let (repr, abst) = Rep_tuple_isomorphism isom in
    1.92 +        (\<lambda>f v. abst (f (fst (repr v)), snd (repr v)))"
    1.93 +  istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)"
    1.94 + "istuple_snd_update isom \<equiv>
    1.95 +     let (repr, abst) = Rep_tuple_isomorphism isom in
    1.96 +        (\<lambda>f v. abst (fst (repr v), f (snd (repr v))))"
    1.97 +  istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a"
    1.98 + "istuple_cons isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in curry abst"
    1.99 +
   1.100 +text {*
   1.101 +These predicates are used in the introduction rule set to constrain
   1.102 +matching appropriately. The elimination rules for them produce the
   1.103 +desired theorems once they are proven. The final introduction rules are
   1.104 +used when no further rules from the introduction rule set can apply.
   1.105 +*}
   1.106  
   1.107  constdefs
   1.108    istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   1.109 @@ -121,129 +196,137 @@
   1.110    by (simp add: istuple_surjective_proof_assist_def)
   1.111  
   1.112  locale isomorphic_tuple =
   1.113 -  fixes isom :: "'a \<Rightarrow> ('b \<times> 'c)" and inv :: "('b \<times> 'c) \<Rightarrow> 'a"
   1.114 -    and cons :: "'b \<Rightarrow> 'c \<Rightarrow> 'a"
   1.115 -  assumes isom_eq: "(isom x = isom y) = (x = y)"
   1.116 -  and inverse_inv: "isom (inv v) = v"
   1.117 -  and cons_def: "cons \<equiv> curry inv"
   1.118 +  fixes isom :: "('a, 'b, 'c) tuple_isomorphism" 
   1.119 +       and repr and abst
   1.120 +  defines "repr \<equiv> fst (Rep_tuple_isomorphism isom)"
   1.121 +  defines "abst \<equiv> snd (Rep_tuple_isomorphism isom)"
   1.122 +  assumes repr_inv: "\<And>x. abst (repr x) = x"
   1.123 +  assumes abst_inv: "\<And>y. repr (abst y) = y"
   1.124  
   1.125  begin
   1.126  
   1.127 -lemma inverse_isom:
   1.128 -  "(inv (isom v)) = v"
   1.129 -  by (rule iffD1 [OF isom_eq], simp add: inverse_inv)
   1.130 -
   1.131 -lemma inv_eq:
   1.132 -  "(inv x = inv y) = (x = y)"
   1.133 -  apply (rule iffI)
   1.134 -   apply (drule arg_cong[where f=isom])
   1.135 -   apply (simp add: inverse_inv)
   1.136 -  apply simp
   1.137 +lemma repr_inj:
   1.138 +  "(repr x = repr y) = (x = y)"
   1.139 +  apply (rule iffI, simp_all)
   1.140 +  apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
   1.141    done
   1.142  
   1.143 -lemmas simps = isom_eq inv_eq inverse_inv inverse_isom cons_def
   1.144 +lemma abst_inj:
   1.145 +  "(abst x = abst y) = (x = y)"
   1.146 +  apply (rule iffI, simp_all)
   1.147 +  apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
   1.148 +  done
   1.149 +
   1.150 +lemma split_Rep:
   1.151 +  "split f (Rep_tuple_isomorphism isom)
   1.152 +     = f repr abst"
   1.153 +  by (simp add: split_def repr_def abst_def)
   1.154 +
   1.155 +lemmas simps = Let_def split_Rep repr_inv abst_inv repr_inj abst_inj
   1.156  
   1.157  lemma istuple_access_update_fst_fst:
   1.158    "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
   1.159 -    (f o istuple_fst isom) o (istuple_fst_update isom inv o h) g
   1.160 +    (f o istuple_fst isom) o (istuple_fst_update isom o h) g
   1.161            = j o (f o istuple_fst isom)"
   1.162    by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
   1.163               intro!: ext elim!: o_eq_elim)
   1.164  
   1.165  lemma istuple_access_update_snd_snd:
   1.166    "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
   1.167 -    (f o istuple_snd isom) o (istuple_snd_update isom inv o h) g
   1.168 +    (f o istuple_snd isom) o (istuple_snd_update isom o h) g
   1.169            = j o (f o istuple_snd isom)"
   1.170    by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
   1.171               intro!: ext elim!: o_eq_elim)
   1.172  
   1.173  lemma istuple_access_update_fst_snd:
   1.174 -  "(f o istuple_fst isom) o (istuple_snd_update isom inv o h) g
   1.175 +  "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
   1.176            = id o (f o istuple_fst isom)"
   1.177    by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
   1.178               intro!: ext elim!: o_eq_elim)
   1.179  
   1.180  lemma istuple_access_update_snd_fst:
   1.181 -  "(f o istuple_snd isom) o (istuple_fst_update isom inv o h) g
   1.182 +  "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
   1.183            = id o (f o istuple_snd isom)"
   1.184    by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
   1.185               intro!: ext elim!: o_eq_elim)
   1.186  
   1.187  lemma istuple_update_swap_fst_fst:
   1.188    "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
   1.189 -    (istuple_fst_update isom inv o h) f o (istuple_fst_update isom inv o j) g
   1.190 -          = (istuple_fst_update isom inv o j) g o (istuple_fst_update isom inv o h) f"
   1.191 +    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   1.192 +          = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
   1.193    by (clarsimp simp: istuple_fst_update_def simps
   1.194               intro!: ext elim!: o_eq_elim)
   1.195  
   1.196  lemma istuple_update_swap_snd_snd:
   1.197    "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
   1.198 -    (istuple_snd_update isom inv o h) f o (istuple_snd_update isom inv o j) g
   1.199 -          = (istuple_snd_update isom inv o j) g o (istuple_snd_update isom inv o h) f"
   1.200 +    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   1.201 +          = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
   1.202    by (clarsimp simp: istuple_snd_update_def simps
   1.203               intro!: ext elim!: o_eq_elim)
   1.204  
   1.205  lemma istuple_update_swap_fst_snd:
   1.206 -  "(istuple_snd_update isom inv o h) f o (istuple_fst_update isom inv o j) g
   1.207 -          = (istuple_fst_update isom inv o j) g o (istuple_snd_update isom inv o h) f"
   1.208 +  "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
   1.209 +          = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
   1.210    by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
   1.211               intro!: ext elim!: o_eq_elim)
   1.212  
   1.213  lemma istuple_update_swap_snd_fst:
   1.214 -  "(istuple_fst_update isom inv o h) f o (istuple_snd_update isom inv o j) g
   1.215 -          = (istuple_snd_update isom inv o j) g o (istuple_fst_update isom inv o h) f"
   1.216 +  "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
   1.217 +          = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
   1.218    by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
   1.219               intro!: ext elim!: o_eq_elim)
   1.220  
   1.221  lemma istuple_update_compose_fst_fst:
   1.222    "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
   1.223 -    (istuple_fst_update isom inv o h) f o (istuple_fst_update isom inv o j) g
   1.224 -          = (istuple_fst_update isom inv o k) (f o g)"
   1.225 +    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   1.226 +          = (istuple_fst_update isom o k) (f o g)"
   1.227    by (fastsimp simp: istuple_fst_update_def simps
   1.228               intro!: ext elim!: o_eq_elim dest: fun_cong)
   1.229  
   1.230  lemma istuple_update_compose_snd_snd:
   1.231    "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
   1.232 -    (istuple_snd_update isom inv o h) f o (istuple_snd_update isom inv o j) g
   1.233 -          = (istuple_snd_update isom inv o k) (f o g)"
   1.234 +    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   1.235 +          = (istuple_snd_update isom o k) (f o g)"
   1.236    by (fastsimp simp: istuple_snd_update_def simps
   1.237               intro!: ext elim!: o_eq_elim dest: fun_cong)
   1.238  
   1.239  lemma istuple_surjective_proof_assist_step:
   1.240    "\<lbrakk> istuple_surjective_proof_assist v a (istuple_fst isom o f);
   1.241       istuple_surjective_proof_assist v b (istuple_snd isom o f) \<rbrakk>
   1.242 -      \<Longrightarrow> istuple_surjective_proof_assist v (cons a b) f"
   1.243 +      \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
   1.244    by (clarsimp simp: istuple_surjective_proof_assist_def simps
   1.245 -                     istuple_fst_def istuple_snd_def)
   1.246 +                     istuple_fst_def istuple_snd_def istuple_cons_def)
   1.247  
   1.248  lemma istuple_fst_update_accessor_cong_assist:
   1.249    "istuple_update_accessor_cong_assist f g \<Longrightarrow>
   1.250 -      istuple_update_accessor_cong_assist (istuple_fst_update isom inv o f) (g o istuple_fst isom)"
   1.251 -  by (simp add: istuple_update_accessor_cong_assist_def istuple_fst_update_def istuple_fst_def simps)
   1.252 +      istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
   1.253 +  by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   1.254 +                     istuple_fst_update_def istuple_fst_def)
   1.255  
   1.256  lemma istuple_snd_update_accessor_cong_assist:
   1.257    "istuple_update_accessor_cong_assist f g \<Longrightarrow>
   1.258 -      istuple_update_accessor_cong_assist (istuple_snd_update isom inv o f) (g o istuple_snd isom)"
   1.259 -  by (simp add: istuple_update_accessor_cong_assist_def istuple_snd_update_def istuple_snd_def simps)
   1.260 +      istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
   1.261 +  by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   1.262 +                     istuple_snd_update_def istuple_snd_def)
   1.263  
   1.264  lemma istuple_fst_update_accessor_eq_assist:
   1.265    "istuple_update_accessor_eq_assist f g a u a' v \<Longrightarrow>
   1.266 -      istuple_update_accessor_eq_assist (istuple_fst_update isom inv o f) (g o istuple_fst isom)
   1.267 -              (cons a b) u (cons a' b) v"
   1.268 -  by (simp add: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def simps
   1.269 -                istuple_update_accessor_cong_assist_def)
   1.270 +      istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
   1.271 +              (istuple_cons isom a b) u (istuple_cons isom a' b) v"
   1.272 +  by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def
   1.273 +                     istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   1.274  
   1.275  lemma istuple_snd_update_accessor_eq_assist:
   1.276    "istuple_update_accessor_eq_assist f g b u b' v \<Longrightarrow>
   1.277 -      istuple_update_accessor_eq_assist (istuple_snd_update isom inv o f) (g o istuple_snd isom)
   1.278 -              (cons a b) u (cons a b') v"
   1.279 -  by (simp add: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def simps
   1.280 -                istuple_update_accessor_cong_assist_def)
   1.281 +      istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
   1.282 +              (istuple_cons isom a b) u (istuple_cons isom a b') v"
   1.283 +  by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def
   1.284 +                     istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   1.285  
   1.286 -lemma cons_conj_eqI:
   1.287 +lemma istuple_cons_conj_eqI:
   1.288    "\<lbrakk> (a = c \<and> b = d \<and> P) = Q \<rbrakk> \<Longrightarrow>
   1.289 -    (cons a b = cons c d \<and> P) = Q"
   1.290 -  by (simp add: simps)
   1.291 +    (istuple_cons isom a b = istuple_cons isom c d \<and> P) = Q"
   1.292 +  by (clarsimp simp: istuple_cons_def simps)
   1.293  
   1.294  lemmas intros =
   1.295      istuple_access_update_fst_fst
   1.296 @@ -261,12 +344,27 @@
   1.297      istuple_snd_update_accessor_eq_assist
   1.298      istuple_fst_update_accessor_cong_assist
   1.299      istuple_snd_update_accessor_cong_assist
   1.300 -    cons_conj_eqI
   1.301 +    istuple_cons_conj_eqI
   1.302  
   1.303  end
   1.304  
   1.305 -interpretation tuple_automorphic: isomorphic_tuple "id" "id" "Pair"
   1.306 -  by (unfold_locales, simp_all add: curry_def)
   1.307 +lemma isomorphic_tuple_intro:
   1.308 +  assumes repr_inj: "\<And>x y. (repr x = repr y) = (x = y)"
   1.309 +     and abst_inv: "\<And>z. repr (abst z) = z"
   1.310 +  shows "v \<equiv> TupleIsomorphism repr abst \<Longrightarrow> isomorphic_tuple v"
   1.311 +  apply (rule isomorphic_tuple.intro,
   1.312 +         simp_all add: TupleIsomorphism_def Abs_tuple_isomorphism_inverse
   1.313 +                       tuple_isomorphism_def abst_inv)
   1.314 +  apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
   1.315 +  apply (simp add: abst_inv)
   1.316 +  done
   1.317 +
   1.318 +constdefs
   1.319 + "tuple_istuple \<equiv> TupleIsomorphism id id"
   1.320 +
   1.321 +lemma tuple_istuple:
   1.322 +  "isomorphic_tuple tuple_istuple"
   1.323 +  by (simp add: isomorphic_tuple_intro[OF _ _ reflexive] tuple_istuple_def)
   1.324  
   1.325  lemma refl_conj_eq:
   1.326    "Q = R \<Longrightarrow> (P \<and> Q) = (P \<and> R)"
     2.1 --- a/src/HOL/Record.thy	Thu Sep 10 15:18:43 2009 +1000
     2.2 +++ b/src/HOL/Record.thy	Thu Sep 10 16:38:18 2009 +1000
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/Record.thy
     2.5 -    ID:         $Id: Record.thy,v 1.33 2007/12/19 15:32:12 schirmer Exp $
     2.6      Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
     2.7  *)
     2.8  
     3.1 --- a/src/HOL/Tools/istuple_support.ML	Thu Sep 10 15:18:43 2009 +1000
     3.2 +++ b/src/HOL/Tools/istuple_support.ML	Thu Sep 10 16:38:18 2009 +1000
     3.3 @@ -1,7 +1,7 @@
     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 extracting
     3.8 +Support for defining instances of tuple-like types and supplying
     3.9  introduction rules needed by the record package.
    3.10  *)
    3.11  
    3.12 @@ -9,82 +9,56 @@
    3.13  signature ISTUPLE_SUPPORT =
    3.14  sig
    3.15    val add_istuple_type: bstring * string list -> (typ * typ) -> theory ->
    3.16 -            (term * theory);
    3.17 -  type tagged_net = ((string * int) * thm) Net.net;
    3.18 -
    3.19 -  val get_istuple_intros: theory -> tagged_net;
    3.20 +            (term * term * theory);
    3.21  
    3.22 -  val build_tagged_net: string -> thm list -> tagged_net;
    3.23 -  val resolve_from_tagged_net: tagged_net -> int -> tactic;
    3.24 -  val tag_thm_trace: thm list ref;
    3.25 -  val merge_tagged_nets: (tagged_net * tagged_net) -> tagged_net;
    3.26 +  val mk_cons_tuple: term * term -> term;
    3.27 +  val dest_cons_tuple: term -> term * term;
    3.28 +
    3.29 +  val istuple_intros_tac: theory -> int -> tactic;
    3.30 +
    3.31 +  val named_cterm_instantiate: (string * cterm) list -> thm -> thm;
    3.32  end;
    3.33  
    3.34  structure IsTupleSupport : ISTUPLE_SUPPORT =
    3.35  struct
    3.36  
    3.37 -val consN = "_NTupleCons";
    3.38 +val isomN = "_TupleIsom";
    3.39  val defN = "_def";
    3.40  
    3.41 -val istuple_UNIV_I = thm "istuple_UNIV_I";
    3.42 -val istuple_True_simp = thm "istuple_True_simp";
    3.43 +val istuple_UNIV_I = @{thm "istuple_UNIV_I"};
    3.44 +val istuple_True_simp = @{thm "istuple_True_simp"};
    3.45  
    3.46 -val istuple_intro = thm "isomorphic_tuple.intro";
    3.47 -val istuple_intros = thms "isomorphic_tuple.intros";
    3.48 -
    3.49 -val init_intros = thms "tuple_automorphic.intros";
    3.50 -
    3.51 -type tagged_net = ((string * int) * thm) Net.net;
    3.52 +val istuple_intro = @{thm "isomorphic_tuple_intro"};
    3.53 +val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"});
    3.54  
    3.55 -(* broadly similar to the use of nets in Tactic.resolve_from_net_tac.
    3.56 -   the tag strings identify which group of theorems a theorem in the
    3.57 -   net belongs to. *)
    3.58 -fun build_tagged_net tag thms = let
    3.59 -    fun add_to_net thm (i, net) =
    3.60 -        (i + 1, Net.insert_term (K false) (concl_of thm, ((tag, i), thm)) net);
    3.61 -    val (n, net) = fold add_to_net thms (0, Net.empty);
    3.62 -  in net end;
    3.63 +val constname = fst o dest_Const;
    3.64 +val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple});
    3.65  
    3.66 -val tag_thm_trace = ref ([] : thm list);
    3.67 +val istuple_constN = constname @{term isomorphic_tuple};
    3.68 +val istuple_consN = constname @{term istuple_cons};
    3.69 +
    3.70 +val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"});
    3.71  
    3.72 -(* we check here that only theorems from a single group are being
    3.73 -   selected for unification, and that there are no duplicates. this
    3.74 -   is a good test that the net is doing its job, picking exactly the
    3.75 -   appropriate rules rather than overapproximating. *)
    3.76 -fun tagged_thms_check t xs = let
    3.77 -    val tags = sort_distinct string_ord (map (fst o fst) xs);
    3.78 -    val ids  = sort_distinct int_ord (map (snd o fst) xs);
    3.79 -    val thms = map snd xs;
    3.80 -in
    3.81 -   if length tags > 1
    3.82 -   then (tag_thm_trace := t :: thms;
    3.83 -     raise THM ("tag mismatch " ^ hd tags ^ ", " ^ nth tags 1, 1, t :: thms))
    3.84 -   else if length ids < length xs
    3.85 -   then (tag_thm_trace := t :: thms;
    3.86 -     raise THM ("tag match duplicate id ", 1, t :: thms))
    3.87 -   else ()
    3.88 -end;
    3.89 +fun named_cterm_instantiate values thm = let
    3.90 +    fun match name (Var ((name', _), _)) = name = name'
    3.91 +      | match name _ = false;
    3.92 +    fun getvar name = case (find_first (match name)
    3.93 +                                    (OldTerm.term_vars (prop_of thm)))
    3.94 +      of SOME var => cterm_of (theory_of_thm thm) var
    3.95 +       | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
    3.96 +  in
    3.97 +    cterm_instantiate (map (apfst getvar) values) thm
    3.98 +  end;
    3.99  
   3.100 -fun resolve_from_tagged_net net i t =
   3.101 -  SUBGOAL (fn (prem, i) => let
   3.102 -      val options = Net.unify_term net (Logic.strip_assums_concl prem);
   3.103 -      val sorted  = sort (int_ord o pairself (snd o fst)) options;
   3.104 -      val check   = tagged_thms_check t sorted;
   3.105 -    in resolve_tac (map snd sorted) i end) i t;
   3.106 -
   3.107 -val merge_tagged_nets = Net.merge (Thm.eq_thm_prop o pairself snd);
   3.108 -
   3.109 -structure IsTupleIntros = TheoryDataFun
   3.110 +structure IsTupleThms = TheoryDataFun
   3.111  (
   3.112 -  type T = tagged_net;
   3.113 -  val empty = build_tagged_net "initial introduction rules" init_intros;
   3.114 +  type T = thm Symtab.table;
   3.115 +  val empty = Symtab.make [tuple_istuple];
   3.116    val copy = I;
   3.117    val extend = I;
   3.118 -  val merge = K merge_tagged_nets;
   3.119 +  val merge = K (Symtab.merge Thm.eq_thm_prop);
   3.120  );
   3.121  
   3.122 -val get_istuple_intros = IsTupleIntros.get;
   3.123 -
   3.124  fun do_typedef name repT alphas thy =
   3.125    let
   3.126      fun get_thms thy name =
   3.127 @@ -93,52 +67,83 @@
   3.128            Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name;
   3.129          val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp];
   3.130        in (map rewrite_rule [rep_inject, abs_inverse],
   3.131 -            Const (absN, repT --> absT)) end;
   3.132 +            Const (absN, repT --> absT), absT) end;
   3.133    in
   3.134      thy
   3.135      |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
   3.136      |-> (fn (name, _) => `(fn thy => get_thms thy name))
   3.137    end;
   3.138  
   3.139 -(* copied from earlier version of HOLogic *)
   3.140 -fun mk_curry t =
   3.141 -  (case Term.fastype_of t of
   3.142 -    T as (Type ("fun", [Type ("*", [A, B]), C])) =>
   3.143 -      Const ("curry", T --> A --> B --> C) $ t
   3.144 -  | _ => raise TERM ("mk_curry: bad body type", [t]));
   3.145 +fun mk_cons_tuple (left, right) = let
   3.146 +    val (leftT, rightT) = (fastype_of left, fastype_of right);
   3.147 +    val prodT           = HOLogic.mk_prodT (leftT, rightT);
   3.148 +    val isomT           = Type (tup_isom_typeN, [prodT, leftT, rightT]);
   3.149 +  in
   3.150 +    Const (istuple_consN, isomT --> leftT --> rightT --> prodT)
   3.151 +      $ Const (fst tuple_istuple, isomT) $ left $ right
   3.152 +  end;
   3.153  
   3.154 -fun add_istuple_type (name, alphas) (left, right) thy =
   3.155 +fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right)
   3.156 +  = if ic = istuple_consN then (left, right)
   3.157 +    else raise TERM ("dest_cons_tuple", [v])
   3.158 +  | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]);
   3.159 +
   3.160 +fun add_istuple_type (name, alphas) (leftT, rightT) thy =
   3.161  let
   3.162 -  val repT = HOLogic.mk_prodT (left, right);
   3.163 +  val repT = HOLogic.mk_prodT (leftT, rightT);
   3.164  
   3.165 -  val (([rep_inject, abs_inverse], abs), typ_thy) =
   3.166 +  val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
   3.167      thy
   3.168      |> do_typedef name repT alphas
   3.169      ||> Sign.add_path name;
   3.170  
   3.171 -  val abs_curry = mk_curry abs;
   3.172 -  val consT     = fastype_of abs_curry;
   3.173 -  val consBind  = Binding.name (name ^ consN);
   3.174 -  val cons      = Const (Sign.full_name typ_thy consBind, consT);
   3.175 -  val cons_spec = (name ^ consN ^ defN, Logic.mk_equals (cons, abs_curry));
   3.176 +  (* construct a type and body for the isomorphism constant by
   3.177 +     instantiating the theorem to which the definition will be applied *)
   3.178 +  val intro_inst = rep_inject RS
   3.179 +                   (named_cterm_instantiate [("abst", cterm_of typ_thy absC)]
   3.180 +                        istuple_intro);
   3.181 +  val (_, body)  = Logic.dest_equals (List.last (prems_of intro_inst));
   3.182 +  val isomT      = fastype_of body;
   3.183 +  val isomBind   = Binding.name (name ^ isomN);
   3.184 +  val isom       = Const (Sign.full_name typ_thy isomBind, isomT);
   3.185 +  val isom_spec  = (name ^ isomN ^ defN, Logic.mk_equals (isom, body));
   3.186  
   3.187 -  val ([cons_def], cdef_thy) =
   3.188 +  val ([isom_def], cdef_thy) =
   3.189      typ_thy
   3.190 -    |> Sign.add_consts_i [Syntax.no_syn (consBind, consT)]
   3.191 -    |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name cons_spec)];
   3.192 +    |> Sign.add_consts_i [Syntax.no_syn (isomBind, isomT)]
   3.193 +    |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
   3.194  
   3.195 -  val istuple = [abs_inverse, cons_def] MRS (rep_inject RS istuple_intro);
   3.196 -  val intros = [istuple] RL istuple_intros;
   3.197 -  val intro_net = build_tagged_net name intros;
   3.198 +  val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
   3.199 +  val cons    = Const (istuple_consN, isomT --> leftT --> rightT --> absT)
   3.200  
   3.201    val thm_thy =
   3.202      cdef_thy
   3.203 -    |> IsTupleIntros.map (curry merge_tagged_nets intro_net)
   3.204 +    |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop
   3.205 +                           (constname isom, istuple))
   3.206      |> Sign.parent_path;
   3.207  in
   3.208 -  (cons, thm_thy)
   3.209 +  (isom, cons $ isom, thm_thy)
   3.210  end;
   3.211  
   3.212 +fun istuple_intros_tac thy = let
   3.213 +    val isthms  = IsTupleThms.get thy;
   3.214 +    fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
   3.215 +    val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let
   3.216 +        val goal' = Envir.beta_eta_contract goal;
   3.217 +        val isom  = case goal' of (Const tp $ (Const pr $ Const is))
   3.218 +                    => if fst tp = "Trueprop" andalso fst pr = istuple_constN
   3.219 +                       then Const is
   3.220 +                       else err "unexpected goal predicate" goal'
   3.221 +            | _ => err "unexpected goal format" goal';
   3.222 +        val isthm = case Symtab.lookup isthms (constname isom) of
   3.223 +                    SOME isthm => isthm
   3.224 +                  | NONE => err "no thm found for constant" isom;
   3.225 +      in rtac isthm n end);
   3.226 +  in
   3.227 +    fn n => resolve_from_net_tac istuple_intros n
   3.228 +            THEN use_istuple_thm_tac n
   3.229 +  end;
   3.230 +
   3.231  end;
   3.232  
   3.233  
     4.1 --- a/src/HOL/Tools/record.ML	Thu Sep 10 15:18:43 2009 +1000
     4.2 +++ b/src/HOL/Tools/record.ML	Thu Sep 10 16:38:18 2009 +1000
     4.3 @@ -1,5 +1,6 @@
     4.4  (*  Title:      HOL/Tools/record.ML
     4.5 -    Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
     4.6 +    Authors:    Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
     4.7 +                Thomas Sewell, NICTA
     4.8  
     4.9  Extensible records with structural subtyping in HOL.
    4.10  *)
    4.11 @@ -1029,22 +1030,12 @@
    4.12                     (Symtab.insert (K true) (cname u, ()) seen) swaps;
    4.13    in swapsneeded updfuns [] Symtab.empty SymSymTab.empty end;
    4.14  
    4.15 -fun named_cterm_instantiate values thm = let
    4.16 -    fun match name (Var ((name', _), _)) = name = name'
    4.17 -      | match name _ = false;
    4.18 -    fun getvar name = case (find_first (match name)
    4.19 -                                    (OldTerm.term_vars (prop_of thm)))
    4.20 -      of SOME var => cterm_of (theory_of_thm thm) var
    4.21 -       | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
    4.22 -  in
    4.23 -    cterm_instantiate (map (apfst getvar) values) thm
    4.24 -  end;
    4.25 +val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
    4.26  
    4.27  fun prove_unfold_defs thy ss T ex_simps ex_simprs prop =
    4.28    let
    4.29      val defset = get_sel_upd_defs thy;
    4.30 -    val intros = IsTupleSupport.get_istuple_intros thy;
    4.31 -    val in_tac = IsTupleSupport.resolve_from_tagged_net intros;
    4.32 +    val in_tac = IsTupleSupport.istuple_intros_tac thy;
    4.33      val prop'  = Envir.beta_eta_contract prop;
    4.34      val (lhs, rhs)   = Logic.dest_equals (Logic.strip_assums_concl prop');
    4.35      val (head, args) = strip_comb lhs;
    4.36 @@ -1136,8 +1127,7 @@
    4.37        | _ => NONE));
    4.38  
    4.39  fun get_upd_acc_cong_thm upd acc thy simpset = let
    4.40 -    val intros = IsTupleSupport.get_istuple_intros thy;
    4.41 -    val in_tac = IsTupleSupport.resolve_from_tagged_net intros;
    4.42 +    val in_tac = IsTupleSupport.istuple_intros_tac thy;
    4.43  
    4.44      val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)]
    4.45      val prop  = concl_of (named_cterm_instantiate insts updacc_cong_triv);
    4.46 @@ -1567,14 +1557,14 @@
    4.47        val left  = List.take (xs, half);
    4.48        val right = List.drop (xs, half);
    4.49      in
    4.50 -      HOLogic.mk_prod (mktreeV left, mktreeV right)
    4.51 +      IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right)
    4.52      end;
    4.53  
    4.54      fun mk_istuple ((thy, i), (left, rght)) =
    4.55      let
    4.56        val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i);
    4.57        val nm   = suffix suff (Long_Name.base_name name);
    4.58 -      val (cons, thy') = IsTupleSupport.add_istuple_type
    4.59 +      val (isom, cons, thy') = IsTupleSupport.add_istuple_type
    4.60                 (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
    4.61      in
    4.62        ((thy', i + 1), cons $ left $ rght)
    4.63 @@ -1585,7 +1575,7 @@
    4.64      fun mk_even_istuple ((thy, i), [arg]) =
    4.65          ((thy, i), arg)
    4.66        | mk_even_istuple ((thy, i), args) =
    4.67 -        mk_istuple ((thy, i), HOLogic.dest_prod (mktreeV args));
    4.68 +        mk_istuple ((thy, i), IsTupleSupport.dest_cons_tuple (mktreeV args));
    4.69  
    4.70      fun build_meta_tree_type i thy vars more =
    4.71      let
    4.72 @@ -1645,8 +1635,7 @@
    4.73      val w     = Free (wN, extT);
    4.74      val P = Free (Name.variant variants "P", extT-->HOLogic.boolT);
    4.75      val C = Free (Name.variant variants "C", HOLogic.boolT);
    4.76 -    val intros = IsTupleSupport.get_istuple_intros defs_thy;
    4.77 -    val intros_tac = IsTupleSupport.resolve_from_tagged_net intros;
    4.78 +    val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy;
    4.79  
    4.80      val inject_prop =
    4.81        let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
    4.82 @@ -1934,8 +1923,7 @@
    4.83          (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
    4.84  
    4.85      val ext_defs = ext_def :: map #extdef parents;
    4.86 -    val intros = IsTupleSupport.get_istuple_intros extension_thy;
    4.87 -    val intros_tac = IsTupleSupport.resolve_from_tagged_net intros;
    4.88 +    val intros_tac = IsTupleSupport.istuple_intros_tac extension_thy;
    4.89  
    4.90      (* Theorems from the istuple intros.
    4.91         This is complex enough to deserve a full comment.