prefer prefix "iso" over potentially misleading "is"; tuned
authorhaftmann
Mon Dec 21 08:32:04 2009 +0100 (2009-12-21)
changeset 341518d57ce46b3f7
parent 34150 22acb8b38639
child 34152 8e5b596d8c73
prefer prefix "iso" over potentially misleading "is"; tuned
src/HOL/Record.thy
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Record.thy	Mon Dec 21 08:32:03 2009 +0100
     1.2 +++ b/src/HOL/Record.thy	Mon Dec 21 08:32:04 2009 +0100
     1.3 @@ -59,8 +59,8 @@
     1.4    time as the intermediate terms are @{text "O(log(n))"} in size and
     1.5    the types needed have size bounded by K.  To enable this analagous
     1.6    traversal, we define the functions seen below: @{text
     1.7 -  "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"}
     1.8 -  and @{text "istuple_snd_update"}. These functions generalise tuple
     1.9 +  "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"}
    1.10 +  and @{text "iso_tuple_snd_update"}. These functions generalise tuple
    1.11    operations by taking a parameter that encapsulates a tuple
    1.12    isomorphism.  The rewrites needed on these functions now need an
    1.13    additional assumption which is that the isomorphism works.
    1.14 @@ -79,278 +79,259 @@
    1.15  
    1.16  subsection {* Operators and lemmas for types isomorphic to tuples *}
    1.17  
    1.18 -datatype ('a, 'b, 'c) tuple_isomorphism = TupleIsomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
    1.19 +datatype ('a, 'b, 'c) tuple_isomorphism = Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
    1.20  
    1.21  primrec repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where
    1.22 -  "repr (TupleIsomorphism r a) = r"
    1.23 +  "repr (Tuple_Isomorphism r a) = r"
    1.24  
    1.25  primrec abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
    1.26 -  "abst (TupleIsomorphism r a) = a"
    1.27 +  "abst (Tuple_Isomorphism r a) = a"
    1.28  
    1.29 -definition istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.30 -  "istuple_fst isom = fst \<circ> repr isom"
    1.31 +definition iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.32 +  "iso_tuple_fst isom = fst \<circ> repr isom"
    1.33  
    1.34 -definition istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.35 -  "istuple_snd isom = snd \<circ> repr isom"
    1.36 +definition iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.37 +  "iso_tuple_snd isom = snd \<circ> repr isom"
    1.38  
    1.39 -definition istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    1.40 -  "istuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
    1.41 +definition iso_tuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    1.42 +  "iso_tuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
    1.43  
    1.44 -definition istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    1.45 -  "istuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
    1.46 +definition iso_tuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    1.47 +  "iso_tuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
    1.48  
    1.49 -definition istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
    1.50 -  "istuple_cons isom = curry (abst isom)"
    1.51 +definition iso_tuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
    1.52 +  "iso_tuple_cons isom = curry (abst isom)"
    1.53  
    1.54  
    1.55  subsection {* Logical infrastructure for records *}
    1.56  
    1.57 -definition istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
    1.58 -  "istuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
    1.59 +definition iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
    1.60 +  "iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
    1.61  
    1.62 -definition istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
    1.63 -  "istuple_update_accessor_cong_assist upd acc \<longleftrightarrow> 
    1.64 +definition iso_tuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
    1.65 +  "iso_tuple_update_accessor_cong_assist upd acc \<longleftrightarrow> 
    1.66       (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
    1.67  
    1.68 -definition istuple_update_accessor_eq_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
    1.69 -  "istuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow>
    1.70 -     upd f v = v' \<and> acc v = x \<and> istuple_update_accessor_cong_assist upd acc"
    1.71 +definition iso_tuple_update_accessor_eq_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
    1.72 +  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow>
    1.73 +     upd f v = v' \<and> acc v = x \<and> iso_tuple_update_accessor_cong_assist upd acc"
    1.74  
    1.75  lemma update_accessor_congruence_foldE:
    1.76 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
    1.77 +  assumes uac: "iso_tuple_update_accessor_cong_assist upd acc"
    1.78    and       r: "r = r'" and v: "acc r' = v'"
    1.79    and       f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
    1.80    shows        "upd f r = upd f' r'"
    1.81    using uac r v [symmetric]
    1.82    apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
    1.83 -   apply (simp add: istuple_update_accessor_cong_assist_def)
    1.84 +   apply (simp add: iso_tuple_update_accessor_cong_assist_def)
    1.85    apply (simp add: f)
    1.86    done
    1.87  
    1.88  lemma update_accessor_congruence_unfoldE:
    1.89 -  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> r = r' \<Longrightarrow> acc r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v)
    1.90 +  "iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> r = r' \<Longrightarrow> acc r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v)
    1.91       \<Longrightarrow> upd f r = upd f' r'"
    1.92    apply (erule(2) update_accessor_congruence_foldE)
    1.93    apply simp
    1.94    done
    1.95  
    1.96 -lemma istuple_update_accessor_cong_assist_id:
    1.97 -  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
    1.98 -  by rule (simp add: istuple_update_accessor_cong_assist_def)
    1.99 +lemma iso_tuple_update_accessor_cong_assist_id:
   1.100 +  "iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
   1.101 +  by rule (simp add: iso_tuple_update_accessor_cong_assist_def)
   1.102  
   1.103  lemma update_accessor_noopE:
   1.104 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   1.105 +  assumes uac: "iso_tuple_update_accessor_cong_assist upd acc"
   1.106        and acc: "f (acc x) = acc x"
   1.107    shows        "upd f x = x"
   1.108 -using uac by (simp add: acc istuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
   1.109 +using uac by (simp add: acc iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
   1.110    cong: update_accessor_congruence_unfoldE [OF uac])
   1.111  
   1.112  lemma update_accessor_noop_compE:
   1.113 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   1.114 +  assumes uac: "iso_tuple_update_accessor_cong_assist upd acc"
   1.115    assumes acc: "f (acc x) = acc x"
   1.116    shows      "upd (g \<circ> f) x = upd g x"
   1.117    by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
   1.118  
   1.119  lemma update_accessor_cong_assist_idI:
   1.120 -  "istuple_update_accessor_cong_assist id id"
   1.121 -  by (simp add: istuple_update_accessor_cong_assist_def)
   1.122 +  "iso_tuple_update_accessor_cong_assist id id"
   1.123 +  by (simp add: iso_tuple_update_accessor_cong_assist_def)
   1.124  
   1.125  lemma update_accessor_cong_assist_triv:
   1.126 -  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   1.127 +  "iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> iso_tuple_update_accessor_cong_assist upd acc"
   1.128    by assumption
   1.129  
   1.130  lemma update_accessor_accessor_eqE:
   1.131 -  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> acc v = x"
   1.132 -  by (simp add: istuple_update_accessor_eq_assist_def)
   1.133 +  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> acc v = x"
   1.134 +  by (simp add: iso_tuple_update_accessor_eq_assist_def)
   1.135  
   1.136  lemma update_accessor_updator_eqE:
   1.137 -  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> upd f v = v'"
   1.138 -  by (simp add: istuple_update_accessor_eq_assist_def)
   1.139 +  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> upd f v = v'"
   1.140 +  by (simp add: iso_tuple_update_accessor_eq_assist_def)
   1.141  
   1.142 -lemma istuple_update_accessor_eq_assist_idI:
   1.143 -  "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
   1.144 -  by (simp add: istuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
   1.145 +lemma iso_tuple_update_accessor_eq_assist_idI:
   1.146 +  "v' = f v \<Longrightarrow> iso_tuple_update_accessor_eq_assist id id v f v' v"
   1.147 +  by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
   1.148  
   1.149 -lemma istuple_update_accessor_eq_assist_triv:
   1.150 -  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
   1.151 +lemma iso_tuple_update_accessor_eq_assist_triv:
   1.152 +  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> iso_tuple_update_accessor_eq_assist upd acc v f v' x"
   1.153    by assumption
   1.154  
   1.155 -lemma istuple_update_accessor_cong_from_eq:
   1.156 -  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   1.157 -  by (simp add: istuple_update_accessor_eq_assist_def)
   1.158 -
   1.159 -lemma o_eq_dest:
   1.160 -  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
   1.161 -  apply (clarsimp simp: o_def)
   1.162 -  apply (erule fun_cong)
   1.163 -  done
   1.164 +lemma iso_tuple_update_accessor_cong_from_eq:
   1.165 +  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> iso_tuple_update_accessor_cong_assist upd acc"
   1.166 +  by (simp add: iso_tuple_update_accessor_eq_assist_def)
   1.167  
   1.168 -lemma o_eq_elim:
   1.169 -  "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
   1.170 -  apply (erule meta_mp)
   1.171 -  apply (erule o_eq_dest)
   1.172 -  done
   1.173 +lemma iso_tuple_surjective_proof_assistI:
   1.174 +  "f x = y \<Longrightarrow> iso_tuple_surjective_proof_assist x y f"
   1.175 +  by (simp add: iso_tuple_surjective_proof_assist_def)
   1.176  
   1.177 -lemma istuple_surjective_proof_assistI:
   1.178 -  "f x = y \<Longrightarrow> istuple_surjective_proof_assist x y f"
   1.179 -  by (simp add: istuple_surjective_proof_assist_def)
   1.180 -
   1.181 -lemma istuple_surjective_proof_assist_idE:
   1.182 -  "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   1.183 -  by (simp add: istuple_surjective_proof_assist_def)
   1.184 +lemma iso_tuple_surjective_proof_assist_idE:
   1.185 +  "iso_tuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   1.186 +  by (simp add: iso_tuple_surjective_proof_assist_def)
   1.187  
   1.188  locale isomorphic_tuple =
   1.189    fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
   1.190 -    and repr and abst
   1.191 -  defines "repr \<equiv> Record.repr isom"
   1.192 -  defines "abst \<equiv> Record.abst isom"
   1.193 -  assumes repr_inv: "\<And>x. abst (repr x) = x"
   1.194 -  assumes abst_inv: "\<And>y. repr (abst y) = y"
   1.195 +  assumes repr_inv: "\<And>x. abst isom (repr isom x) = x"
   1.196 +  assumes abst_inv: "\<And>y. repr isom (abst isom y) = y"
   1.197  begin
   1.198  
   1.199  lemma repr_inj:
   1.200 -  "repr x = repr y \<longleftrightarrow> x = y"
   1.201 -  apply (rule iffI, simp_all)
   1.202 -  apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
   1.203 -  done
   1.204 +  "repr isom x = repr isom y \<longleftrightarrow> x = y"
   1.205 +  by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"] simp add: repr_inv)
   1.206  
   1.207  lemma abst_inj:
   1.208 -  "abst x = abst y \<longleftrightarrow> x = y"
   1.209 -  apply (rule iffI, simp_all)
   1.210 -  apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
   1.211 -  done
   1.212 +  "abst isom x = abst isom y \<longleftrightarrow> x = y"
   1.213 +  by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"] simp add: abst_inv)
   1.214 +
   1.215 +lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj
   1.216  
   1.217 -lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj repr_def [symmetric] abst_def [symmetric]
   1.218 -
   1.219 -lemma istuple_access_update_fst_fst:
   1.220 +lemma iso_tuple_access_update_fst_fst:
   1.221    "f o h g = j o f \<Longrightarrow>
   1.222 -    (f o istuple_fst isom) o (istuple_fst_update isom o h) g
   1.223 -          = j o (f o istuple_fst isom)"
   1.224 -  by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
   1.225 +    (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g
   1.226 +          = j o (f o iso_tuple_fst isom)"
   1.227 +  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps
   1.228               intro!: ext elim!: o_eq_elim)
   1.229  
   1.230 -lemma istuple_access_update_snd_snd:
   1.231 +lemma iso_tuple_access_update_snd_snd:
   1.232    "f o h g = j o f \<Longrightarrow>
   1.233 -    (f o istuple_snd isom) o (istuple_snd_update isom o h) g
   1.234 -          = j o (f o istuple_snd isom)"
   1.235 -  by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
   1.236 +    (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g
   1.237 +          = j o (f o iso_tuple_snd isom)"
   1.238 +  by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps
   1.239               intro!: ext elim!: o_eq_elim)
   1.240  
   1.241 -lemma istuple_access_update_fst_snd:
   1.242 -  "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
   1.243 -          = id o (f o istuple_fst isom)"
   1.244 -  by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
   1.245 +lemma iso_tuple_access_update_fst_snd:
   1.246 +  "(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g
   1.247 +          = id o (f o iso_tuple_fst isom)"
   1.248 +  by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps
   1.249               intro!: ext elim!: o_eq_elim)
   1.250  
   1.251 -lemma istuple_access_update_snd_fst:
   1.252 -  "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
   1.253 -          = id o (f o istuple_snd isom)"
   1.254 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
   1.255 +lemma iso_tuple_access_update_snd_fst:
   1.256 +  "(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g
   1.257 +          = id o (f o iso_tuple_snd isom)"
   1.258 +  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps
   1.259               intro!: ext elim!: o_eq_elim)
   1.260  
   1.261 -lemma istuple_update_swap_fst_fst:
   1.262 +lemma iso_tuple_update_swap_fst_fst:
   1.263    "h f o j g = j g o h f \<Longrightarrow>
   1.264 -    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   1.265 -          = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
   1.266 -  by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
   1.267 +    (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g
   1.268 +          = (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f"
   1.269 +  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
   1.270  
   1.271 -lemma istuple_update_swap_snd_snd:
   1.272 +lemma iso_tuple_update_swap_snd_snd:
   1.273    "h f o j g = j g o h f \<Longrightarrow>
   1.274 -    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   1.275 -          = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
   1.276 -  by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
   1.277 +    (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g
   1.278 +          = (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f"
   1.279 +  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
   1.280  
   1.281 -lemma istuple_update_swap_fst_snd:
   1.282 -  "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
   1.283 -          = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
   1.284 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
   1.285 +lemma iso_tuple_update_swap_fst_snd:
   1.286 +  "(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g
   1.287 +          = (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f"
   1.288 +  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext)
   1.289  
   1.290 -lemma istuple_update_swap_snd_fst:
   1.291 -  "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
   1.292 -          = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
   1.293 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
   1.294 +lemma iso_tuple_update_swap_snd_fst:
   1.295 +  "(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g
   1.296 +          = (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f"
   1.297 +  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext)
   1.298  
   1.299 -lemma istuple_update_compose_fst_fst:
   1.300 +lemma iso_tuple_update_compose_fst_fst:
   1.301    "h f o j g = k (f o g) \<Longrightarrow>
   1.302 -    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   1.303 -          = (istuple_fst_update isom o k) (f o g)"
   1.304 -  by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
   1.305 +    (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g
   1.306 +          = (iso_tuple_fst_update isom o k) (f o g)"
   1.307 +  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
   1.308  
   1.309 -lemma istuple_update_compose_snd_snd:
   1.310 +lemma iso_tuple_update_compose_snd_snd:
   1.311    "h f o j g = k (f o g) \<Longrightarrow>
   1.312 -    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   1.313 -          = (istuple_snd_update isom o k) (f o g)"
   1.314 -  by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
   1.315 +    (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g
   1.316 +          = (iso_tuple_snd_update isom o k) (f o g)"
   1.317 +  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
   1.318  
   1.319 -lemma istuple_surjective_proof_assist_step:
   1.320 -  "istuple_surjective_proof_assist v a (istuple_fst isom o f) \<Longrightarrow>
   1.321 -     istuple_surjective_proof_assist v b (istuple_snd isom o f)
   1.322 -      \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
   1.323 -  by (clarsimp simp: istuple_surjective_proof_assist_def simps
   1.324 -    istuple_fst_def istuple_snd_def istuple_cons_def)
   1.325 +lemma iso_tuple_surjective_proof_assist_step:
   1.326 +  "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \<Longrightarrow>
   1.327 +     iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f)
   1.328 +      \<Longrightarrow> iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f"
   1.329 +  by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps
   1.330 +    iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def)
   1.331  
   1.332 -lemma istuple_fst_update_accessor_cong_assist:
   1.333 -  assumes "istuple_update_accessor_cong_assist f g"
   1.334 -  shows "istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
   1.335 +lemma iso_tuple_fst_update_accessor_cong_assist:
   1.336 +  assumes "iso_tuple_update_accessor_cong_assist f g"
   1.337 +  shows "iso_tuple_update_accessor_cong_assist (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)"
   1.338  proof -
   1.339 -  from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
   1.340 -  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   1.341 -    istuple_fst_update_def istuple_fst_def)
   1.342 +  from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id)
   1.343 +  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
   1.344 +    iso_tuple_fst_update_def iso_tuple_fst_def)
   1.345  qed
   1.346  
   1.347 -lemma istuple_snd_update_accessor_cong_assist:
   1.348 -  assumes "istuple_update_accessor_cong_assist f g"
   1.349 -  shows "istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
   1.350 +lemma iso_tuple_snd_update_accessor_cong_assist:
   1.351 +  assumes "iso_tuple_update_accessor_cong_assist f g"
   1.352 +  shows "iso_tuple_update_accessor_cong_assist (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)"
   1.353  proof -
   1.354 -  from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
   1.355 -  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   1.356 -    istuple_snd_update_def istuple_snd_def)
   1.357 +  from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id)
   1.358 +  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
   1.359 +    iso_tuple_snd_update_def iso_tuple_snd_def)
   1.360  qed
   1.361  
   1.362 -lemma istuple_fst_update_accessor_eq_assist:
   1.363 -  assumes "istuple_update_accessor_eq_assist f g a u a' v"
   1.364 -  shows "istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
   1.365 -    (istuple_cons isom a b) u (istuple_cons isom a' b) v"
   1.366 +lemma iso_tuple_fst_update_accessor_eq_assist:
   1.367 +  assumes "iso_tuple_update_accessor_eq_assist f g a u a' v"
   1.368 +  shows "iso_tuple_update_accessor_eq_assist (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)
   1.369 +    (iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v"
   1.370  proof -
   1.371    from assms have "f id = id"
   1.372 -    by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
   1.373 -  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
   1.374 -    istuple_fst_update_def istuple_fst_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   1.375 +    by (auto simp add: iso_tuple_update_accessor_eq_assist_def intro: iso_tuple_update_accessor_cong_assist_id)
   1.376 +  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
   1.377 +    iso_tuple_fst_update_def iso_tuple_fst_def iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
   1.378  qed
   1.379  
   1.380 -lemma istuple_snd_update_accessor_eq_assist:
   1.381 -  assumes "istuple_update_accessor_eq_assist f g b u b' v"
   1.382 -  shows "istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
   1.383 -    (istuple_cons isom a b) u (istuple_cons isom a b') v"
   1.384 +lemma iso_tuple_snd_update_accessor_eq_assist:
   1.385 +  assumes "iso_tuple_update_accessor_eq_assist f g b u b' v"
   1.386 +  shows "iso_tuple_update_accessor_eq_assist (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)
   1.387 +    (iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v"
   1.388  proof -
   1.389    from assms have "f id = id"
   1.390 -    by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
   1.391 -  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
   1.392 -    istuple_snd_update_def istuple_snd_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   1.393 +    by (auto simp add: iso_tuple_update_accessor_eq_assist_def intro: iso_tuple_update_accessor_cong_assist_id)
   1.394 +  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
   1.395 +    iso_tuple_snd_update_def iso_tuple_snd_def iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
   1.396  qed
   1.397  
   1.398 -lemma istuple_cons_conj_eqI:
   1.399 +lemma iso_tuple_cons_conj_eqI:
   1.400    "a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
   1.401 -    istuple_cons isom a b = istuple_cons isom c d \<and> P \<longleftrightarrow> Q"
   1.402 -  by (clarsimp simp: istuple_cons_def simps)
   1.403 +    iso_tuple_cons isom a b = iso_tuple_cons isom c d \<and> P \<longleftrightarrow> Q"
   1.404 +  by (clarsimp simp: iso_tuple_cons_def simps)
   1.405  
   1.406  lemmas intros =
   1.407 -    istuple_access_update_fst_fst
   1.408 -    istuple_access_update_snd_snd
   1.409 -    istuple_access_update_fst_snd
   1.410 -    istuple_access_update_snd_fst
   1.411 -    istuple_update_swap_fst_fst
   1.412 -    istuple_update_swap_snd_snd
   1.413 -    istuple_update_swap_fst_snd
   1.414 -    istuple_update_swap_snd_fst
   1.415 -    istuple_update_compose_fst_fst
   1.416 -    istuple_update_compose_snd_snd
   1.417 -    istuple_surjective_proof_assist_step
   1.418 -    istuple_fst_update_accessor_eq_assist
   1.419 -    istuple_snd_update_accessor_eq_assist
   1.420 -    istuple_fst_update_accessor_cong_assist
   1.421 -    istuple_snd_update_accessor_cong_assist
   1.422 -    istuple_cons_conj_eqI
   1.423 +    iso_tuple_access_update_fst_fst
   1.424 +    iso_tuple_access_update_snd_snd
   1.425 +    iso_tuple_access_update_fst_snd
   1.426 +    iso_tuple_access_update_snd_fst
   1.427 +    iso_tuple_update_swap_fst_fst
   1.428 +    iso_tuple_update_swap_snd_snd
   1.429 +    iso_tuple_update_swap_fst_snd
   1.430 +    iso_tuple_update_swap_snd_fst
   1.431 +    iso_tuple_update_compose_fst_fst
   1.432 +    iso_tuple_update_compose_snd_snd
   1.433 +    iso_tuple_surjective_proof_assist_step
   1.434 +    iso_tuple_fst_update_accessor_eq_assist
   1.435 +    iso_tuple_snd_update_accessor_eq_assist
   1.436 +    iso_tuple_fst_update_accessor_cong_assist
   1.437 +    iso_tuple_snd_update_accessor_cong_assist
   1.438 +    iso_tuple_cons_conj_eqI
   1.439  
   1.440  end
   1.441  
   1.442 @@ -358,29 +339,32 @@
   1.443    fixes repr abst
   1.444    assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
   1.445       and abst_inv: "\<And>z. repr (abst z) = z"
   1.446 -  assumes v: "v \<equiv> TupleIsomorphism repr abst"
   1.447 +  assumes v: "v \<equiv> Tuple_Isomorphism repr abst"
   1.448    shows "isomorphic_tuple v"
   1.449 -  apply (rule isomorphic_tuple.intro)
   1.450 -  apply (simp_all add: abst_inv v)
   1.451 -  apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
   1.452 -  apply (simp add: abst_inv)
   1.453 -  done
   1.454 +proof
   1.455 +  have "\<And>x. repr (abst (repr x)) = repr x"
   1.456 +    by (simp add: abst_inv)
   1.457 +  then show "\<And>x. Record.abst v (Record.repr v x) = x"
   1.458 +    by (simp add: v repr_inj)
   1.459 +  show P: "\<And>y. Record.repr v (Record.abst v y) = y"
   1.460 +    by (simp add: v) (fact abst_inv)
   1.461 +qed
   1.462  
   1.463  definition
   1.464 -  "tuple_istuple \<equiv> TupleIsomorphism id id"
   1.465 +  "tuple_iso_tuple \<equiv> Tuple_Isomorphism id id"
   1.466  
   1.467 -lemma tuple_istuple:
   1.468 -  "isomorphic_tuple tuple_istuple"
   1.469 -  by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_istuple_def)
   1.470 +lemma tuple_iso_tuple:
   1.471 +  "isomorphic_tuple tuple_iso_tuple"
   1.472 +  by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def)
   1.473  
   1.474  lemma refl_conj_eq:
   1.475    "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   1.476    by simp
   1.477  
   1.478 -lemma istuple_UNIV_I: "x \<in> UNIV \<equiv> True"
   1.479 +lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
   1.480    by simp
   1.481  
   1.482 -lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   1.483 +lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   1.484    by simp
   1.485  
   1.486  lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
   1.487 @@ -437,9 +421,9 @@
   1.488  use "Tools/record.ML"
   1.489  setup Record.setup
   1.490  
   1.491 -hide (open) const TupleIsomorphism repr abst istuple_fst istuple_snd
   1.492 -  istuple_fst_update istuple_snd_update istuple_cons
   1.493 -  istuple_surjective_proof_assist istuple_update_accessor_cong_assist
   1.494 -  istuple_update_accessor_eq_assist tuple_istuple
   1.495 +hide (open) const Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   1.496 +  iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
   1.497 +  iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
   1.498 +  iso_tuple_update_accessor_eq_assist tuple_iso_tuple
   1.499  
   1.500  end
     2.1 --- a/src/HOL/Tools/record.ML	Mon Dec 21 08:32:03 2009 +0100
     2.2 +++ b/src/HOL/Tools/record.ML	Mon Dec 21 08:32:04 2009 +0100
     2.3 @@ -50,24 +50,24 @@
     2.4  end;
     2.5  
     2.6  
     2.7 -signature ISTUPLE_SUPPORT =
     2.8 +signature ISO_TUPLE_SUPPORT =
     2.9  sig
    2.10 -  val add_istuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
    2.11 +  val add_iso_tuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
    2.12    val mk_cons_tuple: term * term -> term
    2.13    val dest_cons_tuple: term -> term * term
    2.14 -  val istuple_intros_tac: int -> tactic
    2.15 +  val iso_tuple_intros_tac: int -> tactic
    2.16    val named_cterm_instantiate: (string * cterm) list -> thm -> thm
    2.17  end;
    2.18  
    2.19 -structure IsTupleSupport: ISTUPLE_SUPPORT =
    2.20 +structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
    2.21  struct
    2.22  
    2.23 -val isomN = "_TupleIsom";
    2.24 -
    2.25 -val istuple_intro = @{thm isomorphic_tuple_intro};
    2.26 -val istuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
    2.27 -
    2.28 -val tuple_istuple = (@{const_name tuple_istuple}, @{thm tuple_istuple});
    2.29 +val isoN = "_Tuple_Iso";
    2.30 +
    2.31 +val iso_tuple_intro = @{thm isomorphic_tuple_intro};
    2.32 +val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
    2.33 +
    2.34 +val tuple_iso_tuple = (@{const_name tuple_iso_tuple}, @{thm tuple_iso_tuple});
    2.35  
    2.36  fun named_cterm_instantiate values thm =
    2.37    let
    2.38 @@ -81,10 +81,10 @@
    2.39      cterm_instantiate (map (apfst getvar) values) thm
    2.40    end;
    2.41  
    2.42 -structure IsTupleThms = Theory_Data
    2.43 +structure Iso_Tuple_Thms = Theory_Data
    2.44  (
    2.45    type T = thm Symtab.table;
    2.46 -  val empty = Symtab.make [tuple_istuple];
    2.47 +  val empty = Symtab.make [tuple_iso_tuple];
    2.48    val extend = I;
    2.49    fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
    2.50  );
    2.51 @@ -96,7 +96,7 @@
    2.52          val SOME {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
    2.53            Abs_inverse = abs_inverse, ...} = Typedef.get_info thy name;
    2.54          val rewrite_rule =
    2.55 -          MetaSimplifier.rewrite_rule [@{thm istuple_UNIV_I}, @{thm istuple_True_simp}];
    2.56 +          MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
    2.57        in
    2.58          (map rewrite_rule [rep_inject, abs_inverse], Const (absN, repT --> absT), absT)
    2.59        end;
    2.60 @@ -112,14 +112,14 @@
    2.61      val prodT = HOLogic.mk_prodT (leftT, rightT);
    2.62      val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
    2.63    in
    2.64 -    Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> prodT) $
    2.65 -      Const (fst tuple_istuple, isomT) $ left $ right
    2.66 +    Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
    2.67 +      Const (fst tuple_iso_tuple, isomT) $ left $ right
    2.68    end;
    2.69  
    2.70 -fun dest_cons_tuple (Const (@{const_name istuple_cons}, _) $ Const _ $ t $ u) = (t, u)
    2.71 +fun dest_cons_tuple (Const (@{const_name iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
    2.72    | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
    2.73  
    2.74 -fun add_istuple_type (name, alphas) (leftT, rightT) thy =
    2.75 +fun add_iso_tuple_type (name, alphas) (leftT, rightT) thy =
    2.76    let
    2.77      val repT = HOLogic.mk_prodT (leftT, rightT);
    2.78  
    2.79 @@ -131,39 +131,39 @@
    2.80      (*construct a type and body for the isomorphism constant by
    2.81        instantiating the theorem to which the definition will be applied*)
    2.82      val intro_inst =
    2.83 -      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] istuple_intro;
    2.84 +      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
    2.85      val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
    2.86      val isomT = fastype_of body;
    2.87 -    val isom_bind = Binding.name (name ^ isomN);
    2.88 +    val isom_bind = Binding.name (name ^ isoN);
    2.89      val isom_name = Sign.full_name typ_thy isom_bind;
    2.90      val isom = Const (isom_name, isomT);
    2.91 -    val isom_spec = (Thm.def_name (name ^ isomN), Logic.mk_equals (isom, body));
    2.92 +    val isom_spec = (Thm.def_name (name ^ isoN), Logic.mk_equals (isom, body));
    2.93  
    2.94      val ([isom_def], cdef_thy) =
    2.95        typ_thy
    2.96        |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
    2.97        |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
    2.98  
    2.99 -    val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
   2.100 -    val cons = Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> absT);
   2.101 +    val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
   2.102 +    val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
   2.103  
   2.104      val thm_thy =
   2.105        cdef_thy
   2.106 -      |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (isom_name, istuple))
   2.107 +      |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
   2.108        |> Sign.parent_path
   2.109        |> Code.add_default_eqn isom_def;
   2.110    in
   2.111      ((isom, cons $ isom), thm_thy)
   2.112    end;
   2.113  
   2.114 -val istuple_intros_tac = resolve_from_net_tac istuple_intros THEN'
   2.115 +val iso_tuple_intros_tac = resolve_from_net_tac iso_tuple_intros THEN'
   2.116    CSUBGOAL (fn (cgoal, i) =>
   2.117      let
   2.118        val thy = Thm.theory_of_cterm cgoal;
   2.119        val goal = Thm.term_of cgoal;
   2.120  
   2.121 -      val isthms = IsTupleThms.get thy;
   2.122 -      fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
   2.123 +      val isthms = Iso_Tuple_Thms.get thy;
   2.124 +      fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);
   2.125  
   2.126        val goal' = Envir.beta_eta_contract goal;
   2.127        val is =
   2.128 @@ -197,13 +197,13 @@
   2.129  
   2.130  val refl_conj_eq = @{thm refl_conj_eq};
   2.131  
   2.132 -val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
   2.133 -val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
   2.134 +val surject_assistI = @{thm "iso_tuple_surjective_proof_assistI"};
   2.135 +val surject_assist_idE = @{thm "iso_tuple_surjective_proof_assist_idE"};
   2.136  
   2.137  val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"};
   2.138  val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"};
   2.139 -val updacc_eq_idI = @{thm "istuple_update_accessor_eq_assist_idI"};
   2.140 -val updacc_eq_triv = @{thm "istuple_update_accessor_eq_assist_triv"};
   2.141 +val updacc_eq_idI = @{thm "iso_tuple_update_accessor_eq_assist_idI"};
   2.142 +val updacc_eq_triv = @{thm "iso_tuple_update_accessor_eq_assist_triv"};
   2.143  
   2.144  val updacc_foldE = @{thm "update_accessor_congruence_foldE"};
   2.145  val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"};
   2.146 @@ -211,7 +211,7 @@
   2.147  val updacc_noop_compE = @{thm "update_accessor_noop_compE"};
   2.148  val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"};
   2.149  val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"};
   2.150 -val updacc_cong_from_eq = @{thm "istuple_update_accessor_cong_from_eq"};
   2.151 +val updacc_cong_from_eq = @{thm "iso_tuple_update_accessor_cong_from_eq"};
   2.152  
   2.153  val o_eq_dest = @{thm o_eq_dest};
   2.154  val o_eq_id_dest = @{thm o_eq_id_dest};
   2.155 @@ -1066,7 +1066,7 @@
   2.156            Goal.prove (ProofContext.init thy) [] [] prop
   2.157              (fn _ =>
   2.158                simp_tac defset 1 THEN
   2.159 -              REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   2.160 +              REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   2.161                TRY (simp_tac (HOL_ss addsimps id_o_apps) 1));
   2.162          val dest =
   2.163            if is_sel_upd_pair thy acc upd
   2.164 @@ -1089,7 +1089,7 @@
   2.165        Goal.prove (ProofContext.init thy) [] [] prop
   2.166          (fn _ =>
   2.167            simp_tac defset 1 THEN
   2.168 -          REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   2.169 +          REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   2.170            TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
   2.171      val dest = if comp then o_eq_dest_lhs else o_eq_dest;
   2.172    in Drule.standard (othm RS dest) end;
   2.173 @@ -1117,7 +1117,7 @@
   2.174            else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
   2.175    in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
   2.176  
   2.177 -val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
   2.178 +val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate;
   2.179  
   2.180  fun prove_unfold_defs thy ex_simps ex_simprs prop =
   2.181    let
   2.182 @@ -1222,7 +1222,7 @@
   2.183      Goal.prove (ProofContext.init thy) [] [] prop
   2.184        (fn _ =>
   2.185          simp_tac simpset 1 THEN
   2.186 -        REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   2.187 +        REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   2.188          TRY (resolve_tac [updacc_cong_idI] 1))
   2.189    end;
   2.190  
   2.191 @@ -1612,22 +1612,22 @@
   2.192      (*before doing anything else, create the tree of new types
   2.193        that will back the record extension*)
   2.194  
   2.195 -    val mktreeV = Balanced_Tree.make IsTupleSupport.mk_cons_tuple;
   2.196 -
   2.197 -    fun mk_istuple (left, right) (thy, i) =
   2.198 +    val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
   2.199 +
   2.200 +    fun mk_iso_tuple (left, right) (thy, i) =
   2.201        let
   2.202          val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
   2.203          val nm = suffix suff (Long_Name.base_name name);
   2.204          val ((_, cons), thy') =
   2.205 -          IsTupleSupport.add_istuple_type
   2.206 +          Iso_Tuple_Support.add_iso_tuple_type
   2.207              (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
   2.208        in
   2.209          (cons $ left $ right, (thy', i + 1))
   2.210        end;
   2.211  
   2.212 -    (*trying to create a 1-element istuple will fail, and is pointless anyway*)
   2.213 -    fun mk_even_istuple [arg] = pair arg
   2.214 -      | mk_even_istuple args = mk_istuple (IsTupleSupport.dest_cons_tuple (mktreeV args));
   2.215 +    (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*)
   2.216 +    fun mk_even_iso_tuple [arg] = pair arg
   2.217 +      | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args));
   2.218  
   2.219      fun build_meta_tree_type i thy vars more =
   2.220        let val len = length vars in
   2.221 @@ -1637,12 +1637,12 @@
   2.222              fun group16 [] = []
   2.223                | group16 xs = take 16 xs :: group16 (drop 16 xs);
   2.224              val vars' = group16 vars;
   2.225 -            val (composites, (thy', i')) = fold_map mk_even_istuple vars' (thy, i);
   2.226 +            val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i);
   2.227            in
   2.228              build_meta_tree_type i' thy' composites more
   2.229            end
   2.230          else
   2.231 -          let val (term, (thy', _)) = mk_istuple (mktreeV vars, more) (thy, 0)
   2.232 +          let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0)
   2.233            in (term, thy') end
   2.234        end;
   2.235  
   2.236 @@ -1712,7 +1712,7 @@
   2.237              simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
   2.238              REPEAT_DETERM
   2.239                (rtac refl_conj_eq 1 ORELSE
   2.240 -                IsTupleSupport.istuple_intros_tac 1 ORELSE
   2.241 +                Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
   2.242                  rtac refl 1)));
   2.243  
   2.244      val inject = timeit_msg "record extension inject proof:" inject_prf;
   2.245 @@ -1730,7 +1730,7 @@
   2.246          val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
   2.247          val tactic1 =
   2.248            simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
   2.249 -          REPEAT_ALL_NEW IsTupleSupport.istuple_intros_tac 1;
   2.250 +          REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
   2.251          val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
   2.252          val [halfway] = Seq.list_of (tactic1 start);
   2.253          val [surject] = Seq.list_of (tactic2 (Drule.standard halfway));
   2.254 @@ -1954,7 +1954,7 @@
   2.255  
   2.256      val ext_defs = ext_def :: map #extdef parents;
   2.257  
   2.258 -    (*Theorems from the istuple intros.
   2.259 +    (*Theorems from the iso_tuple intros.
   2.260        This is complex enough to deserve a full comment.
   2.261        By unfolding ext_defs from r_rec0 we create a tree of constructor
   2.262        calls (many of them Pair, but others as well). The introduction
   2.263 @@ -1979,7 +1979,7 @@
   2.264          val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
   2.265          val tactic =
   2.266            simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
   2.267 -          REPEAT (IsTupleSupport.istuple_intros_tac 1 ORELSE terminal);
   2.268 +          REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
   2.269          val updaccs = Seq.list_of (tactic init_thm);
   2.270        in
   2.271          (updaccs RL [updacc_accessor_eqE],
   2.272 @@ -2207,7 +2207,7 @@
   2.273               [rtac surject_assist_idE 1,
   2.274                simp_tac init_ss 1,
   2.275                REPEAT
   2.276 -                (IsTupleSupport.istuple_intros_tac 1 ORELSE
   2.277 +                (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
   2.278                    (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
   2.279        end;
   2.280      val surjective = timeit_msg "record surjective proof:" surjective_prf;