# HG changeset patch
# User haftmann
# Date 1261380742 -3600
# Node ID 5da0f7abbe291fc9afc0ccd6eb99bfa05dbd1a07
# Parent  a0efb4754cb7390c40e1f0fd5f4c3c94d927dc06# Parent  8e5b596d8c73a812428108f30821d92bcb8aff79
merged

diff -r a0efb4754cb7 -r 5da0f7abbe29 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat Dec 19 09:07:04 2009 -0800
+++ b/src/HOL/Fun.thy	Mon Dec 21 08:32:22 2009 +0100
@@ -74,6 +74,14 @@
 lemma o_id [simp]: "f o id = f"
 by (simp add: comp_def)
 
+lemma o_eq_dest:
+  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
+  by (simp only: o_def) (fact fun_cong)
+
+lemma o_eq_elim:
+  "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
+  by (erule meta_mp) (fact o_eq_dest) 
+
 lemma image_compose: "(f o g) ` r = f`(g`r)"
 by (simp add: comp_def, blast)
 
diff -r a0efb4754cb7 -r 5da0f7abbe29 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Sat Dec 19 09:07:04 2009 -0800
+++ b/src/HOL/Record.thy	Mon Dec 21 08:32:22 2009 +0100
@@ -59,8 +59,8 @@
   time as the intermediate terms are @{text "O(log(n))"} in size and
   the types needed have size bounded by K.  To enable this analagous
   traversal, we define the functions seen below: @{text
-  "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"}
-  and @{text "istuple_snd_update"}. These functions generalise tuple
+  "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"}
+  and @{text "iso_tuple_snd_update"}. These functions generalise tuple
   operations by taking a parameter that encapsulates a tuple
   isomorphism.  The rewrites needed on these functions now need an
   additional assumption which is that the isomorphism works.
@@ -79,278 +79,259 @@
 
 subsection {* Operators and lemmas for types isomorphic to tuples *}
 
-datatype ('a, 'b, 'c) tuple_isomorphism = TupleIsomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
+datatype ('a, 'b, 'c) tuple_isomorphism = Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
 
 primrec repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where
-  "repr (TupleIsomorphism r a) = r"
+  "repr (Tuple_Isomorphism r a) = r"
 
 primrec abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
-  "abst (TupleIsomorphism r a) = a"
+  "abst (Tuple_Isomorphism r a) = a"
 
-definition istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
-  "istuple_fst isom = fst \<circ> repr isom"
+definition iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
+  "iso_tuple_fst isom = fst \<circ> repr isom"
 
-definition istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
-  "istuple_snd isom = snd \<circ> repr isom"
+definition iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
+  "iso_tuple_snd isom = snd \<circ> repr isom"
 
-definition istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
-  "istuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
+definition iso_tuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
+  "iso_tuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
 
-definition istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
-  "istuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
+definition iso_tuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
+  "iso_tuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
 
-definition istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
-  "istuple_cons isom = curry (abst isom)"
+definition iso_tuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
+  "iso_tuple_cons isom = curry (abst isom)"
 
 
 subsection {* Logical infrastructure for records *}
 
-definition istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
-  "istuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
+definition iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
+  "iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
 
-definition istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
-  "istuple_update_accessor_cong_assist upd acc \<longleftrightarrow> 
+definition iso_tuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
+  "iso_tuple_update_accessor_cong_assist upd acc \<longleftrightarrow> 
      (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
 
-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
-  "istuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow>
-     upd f v = v' \<and> acc v = x \<and> istuple_update_accessor_cong_assist upd acc"
+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
+  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow>
+     upd f v = v' \<and> acc v = x \<and> iso_tuple_update_accessor_cong_assist upd acc"
 
 lemma update_accessor_congruence_foldE:
-  assumes uac: "istuple_update_accessor_cong_assist upd acc"
+  assumes uac: "iso_tuple_update_accessor_cong_assist upd acc"
   and       r: "r = r'" and v: "acc r' = v'"
   and       f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
   shows        "upd f r = upd f' r'"
   using uac r v [symmetric]
   apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
-   apply (simp add: istuple_update_accessor_cong_assist_def)
+   apply (simp add: iso_tuple_update_accessor_cong_assist_def)
   apply (simp add: f)
   done
 
 lemma update_accessor_congruence_unfoldE:
-  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> r = r' \<Longrightarrow> acc r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v)
+  "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)
      \<Longrightarrow> upd f r = upd f' r'"
   apply (erule(2) update_accessor_congruence_foldE)
   apply simp
   done
 
-lemma istuple_update_accessor_cong_assist_id:
-  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
-  by rule (simp add: istuple_update_accessor_cong_assist_def)
+lemma iso_tuple_update_accessor_cong_assist_id:
+  "iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
+  by rule (simp add: iso_tuple_update_accessor_cong_assist_def)
 
 lemma update_accessor_noopE:
-  assumes uac: "istuple_update_accessor_cong_assist upd acc"
+  assumes uac: "iso_tuple_update_accessor_cong_assist upd acc"
       and acc: "f (acc x) = acc x"
   shows        "upd f x = x"
-using uac by (simp add: acc istuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
+using uac by (simp add: acc iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
   cong: update_accessor_congruence_unfoldE [OF uac])
 
 lemma update_accessor_noop_compE:
-  assumes uac: "istuple_update_accessor_cong_assist upd acc"
+  assumes uac: "iso_tuple_update_accessor_cong_assist upd acc"
   assumes acc: "f (acc x) = acc x"
   shows      "upd (g \<circ> f) x = upd g x"
   by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
 
 lemma update_accessor_cong_assist_idI:
-  "istuple_update_accessor_cong_assist id id"
-  by (simp add: istuple_update_accessor_cong_assist_def)
+  "iso_tuple_update_accessor_cong_assist id id"
+  by (simp add: iso_tuple_update_accessor_cong_assist_def)
 
 lemma update_accessor_cong_assist_triv:
-  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
+  "iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> iso_tuple_update_accessor_cong_assist upd acc"
   by assumption
 
 lemma update_accessor_accessor_eqE:
-  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> acc v = x"
-  by (simp add: istuple_update_accessor_eq_assist_def)
+  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> acc v = x"
+  by (simp add: iso_tuple_update_accessor_eq_assist_def)
 
 lemma update_accessor_updator_eqE:
-  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> upd f v = v'"
-  by (simp add: istuple_update_accessor_eq_assist_def)
+  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> upd f v = v'"
+  by (simp add: iso_tuple_update_accessor_eq_assist_def)
 
-lemma istuple_update_accessor_eq_assist_idI:
-  "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
-  by (simp add: istuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
+lemma iso_tuple_update_accessor_eq_assist_idI:
+  "v' = f v \<Longrightarrow> iso_tuple_update_accessor_eq_assist id id v f v' v"
+  by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
 
-lemma istuple_update_accessor_eq_assist_triv:
-  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
+lemma iso_tuple_update_accessor_eq_assist_triv:
+  "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"
   by assumption
 
-lemma istuple_update_accessor_cong_from_eq:
-  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
-  by (simp add: istuple_update_accessor_eq_assist_def)
-
-lemma o_eq_dest:
-  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
-  apply (clarsimp simp: o_def)
-  apply (erule fun_cong)
-  done
+lemma iso_tuple_update_accessor_cong_from_eq:
+  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> iso_tuple_update_accessor_cong_assist upd acc"
+  by (simp add: iso_tuple_update_accessor_eq_assist_def)
 
-lemma o_eq_elim:
-  "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
-  apply (erule meta_mp)
-  apply (erule o_eq_dest)
-  done
+lemma iso_tuple_surjective_proof_assistI:
+  "f x = y \<Longrightarrow> iso_tuple_surjective_proof_assist x y f"
+  by (simp add: iso_tuple_surjective_proof_assist_def)
 
-lemma istuple_surjective_proof_assistI:
-  "f x = y \<Longrightarrow> istuple_surjective_proof_assist x y f"
-  by (simp add: istuple_surjective_proof_assist_def)
-
-lemma istuple_surjective_proof_assist_idE:
-  "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
-  by (simp add: istuple_surjective_proof_assist_def)
+lemma iso_tuple_surjective_proof_assist_idE:
+  "iso_tuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
+  by (simp add: iso_tuple_surjective_proof_assist_def)
 
 locale isomorphic_tuple =
   fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
-    and repr and abst
-  defines "repr \<equiv> Record.repr isom"
-  defines "abst \<equiv> Record.abst isom"
-  assumes repr_inv: "\<And>x. abst (repr x) = x"
-  assumes abst_inv: "\<And>y. repr (abst y) = y"
+  assumes repr_inv: "\<And>x. abst isom (repr isom x) = x"
+  assumes abst_inv: "\<And>y. repr isom (abst isom y) = y"
 begin
 
 lemma repr_inj:
-  "repr x = repr y \<longleftrightarrow> x = y"
-  apply (rule iffI, simp_all)
-  apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
-  done
+  "repr isom x = repr isom y \<longleftrightarrow> x = y"
+  by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"] simp add: repr_inv)
 
 lemma abst_inj:
-  "abst x = abst y \<longleftrightarrow> x = y"
-  apply (rule iffI, simp_all)
-  apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
-  done
+  "abst isom x = abst isom y \<longleftrightarrow> x = y"
+  by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"] simp add: abst_inv)
+
+lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj
 
-lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj repr_def [symmetric] abst_def [symmetric]
-
-lemma istuple_access_update_fst_fst:
+lemma iso_tuple_access_update_fst_fst:
   "f o h g = j o f \<Longrightarrow>
-    (f o istuple_fst isom) o (istuple_fst_update isom o h) g
-          = j o (f o istuple_fst isom)"
-  by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
+    (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g
+          = j o (f o iso_tuple_fst isom)"
+  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps
              intro!: ext elim!: o_eq_elim)
 
-lemma istuple_access_update_snd_snd:
+lemma iso_tuple_access_update_snd_snd:
   "f o h g = j o f \<Longrightarrow>
-    (f o istuple_snd isom) o (istuple_snd_update isom o h) g
-          = j o (f o istuple_snd isom)"
-  by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
+    (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g
+          = j o (f o iso_tuple_snd isom)"
+  by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps
              intro!: ext elim!: o_eq_elim)
 
-lemma istuple_access_update_fst_snd:
-  "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
-          = id o (f o istuple_fst isom)"
-  by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
+lemma iso_tuple_access_update_fst_snd:
+  "(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g
+          = id o (f o iso_tuple_fst isom)"
+  by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps
              intro!: ext elim!: o_eq_elim)
 
-lemma istuple_access_update_snd_fst:
-  "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
-          = id o (f o istuple_snd isom)"
-  by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
+lemma iso_tuple_access_update_snd_fst:
+  "(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g
+          = id o (f o iso_tuple_snd isom)"
+  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps
              intro!: ext elim!: o_eq_elim)
 
-lemma istuple_update_swap_fst_fst:
+lemma iso_tuple_update_swap_fst_fst:
   "h f o j g = j g o h f \<Longrightarrow>
-    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
-          = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
-  by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
+    (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g
+          = (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f"
+  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
 
-lemma istuple_update_swap_snd_snd:
+lemma iso_tuple_update_swap_snd_snd:
   "h f o j g = j g o h f \<Longrightarrow>
-    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
-          = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
-  by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
+    (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g
+          = (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f"
+  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
 
-lemma istuple_update_swap_fst_snd:
-  "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
-          = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
-  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
+lemma iso_tuple_update_swap_fst_snd:
+  "(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g
+          = (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f"
+  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext)
 
-lemma istuple_update_swap_snd_fst:
-  "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
-          = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
-  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
+lemma iso_tuple_update_swap_snd_fst:
+  "(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g
+          = (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f"
+  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext)
 
-lemma istuple_update_compose_fst_fst:
+lemma iso_tuple_update_compose_fst_fst:
   "h f o j g = k (f o g) \<Longrightarrow>
-    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
-          = (istuple_fst_update isom o k) (f o g)"
-  by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
+    (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g
+          = (iso_tuple_fst_update isom o k) (f o g)"
+  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
 
-lemma istuple_update_compose_snd_snd:
+lemma iso_tuple_update_compose_snd_snd:
   "h f o j g = k (f o g) \<Longrightarrow>
-    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
-          = (istuple_snd_update isom o k) (f o g)"
-  by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
+    (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g
+          = (iso_tuple_snd_update isom o k) (f o g)"
+  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
 
-lemma istuple_surjective_proof_assist_step:
-  "istuple_surjective_proof_assist v a (istuple_fst isom o f) \<Longrightarrow>
-     istuple_surjective_proof_assist v b (istuple_snd isom o f)
-      \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
-  by (clarsimp simp: istuple_surjective_proof_assist_def simps
-    istuple_fst_def istuple_snd_def istuple_cons_def)
+lemma iso_tuple_surjective_proof_assist_step:
+  "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \<Longrightarrow>
+     iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f)
+      \<Longrightarrow> iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f"
+  by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps
+    iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def)
 
-lemma istuple_fst_update_accessor_cong_assist:
-  assumes "istuple_update_accessor_cong_assist f g"
-  shows "istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
+lemma iso_tuple_fst_update_accessor_cong_assist:
+  assumes "iso_tuple_update_accessor_cong_assist f g"
+  shows "iso_tuple_update_accessor_cong_assist (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)"
 proof -
-  from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
-  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
-    istuple_fst_update_def istuple_fst_def)
+  from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id)
+  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
+    iso_tuple_fst_update_def iso_tuple_fst_def)
 qed
 
-lemma istuple_snd_update_accessor_cong_assist:
-  assumes "istuple_update_accessor_cong_assist f g"
-  shows "istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
+lemma iso_tuple_snd_update_accessor_cong_assist:
+  assumes "iso_tuple_update_accessor_cong_assist f g"
+  shows "iso_tuple_update_accessor_cong_assist (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)"
 proof -
-  from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
-  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
-    istuple_snd_update_def istuple_snd_def)
+  from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id)
+  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
+    iso_tuple_snd_update_def iso_tuple_snd_def)
 qed
 
-lemma istuple_fst_update_accessor_eq_assist:
-  assumes "istuple_update_accessor_eq_assist f g a u a' v"
-  shows "istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
-    (istuple_cons isom a b) u (istuple_cons isom a' b) v"
+lemma iso_tuple_fst_update_accessor_eq_assist:
+  assumes "iso_tuple_update_accessor_eq_assist f g a u a' v"
+  shows "iso_tuple_update_accessor_eq_assist (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)
+    (iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v"
 proof -
   from assms have "f id = id"
-    by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
-  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
-    istuple_fst_update_def istuple_fst_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
+    by (auto simp add: iso_tuple_update_accessor_eq_assist_def intro: iso_tuple_update_accessor_cong_assist_id)
+  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
+    iso_tuple_fst_update_def iso_tuple_fst_def iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
 qed
 
-lemma istuple_snd_update_accessor_eq_assist:
-  assumes "istuple_update_accessor_eq_assist f g b u b' v"
-  shows "istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
-    (istuple_cons isom a b) u (istuple_cons isom a b') v"
+lemma iso_tuple_snd_update_accessor_eq_assist:
+  assumes "iso_tuple_update_accessor_eq_assist f g b u b' v"
+  shows "iso_tuple_update_accessor_eq_assist (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)
+    (iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v"
 proof -
   from assms have "f id = id"
-    by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
-  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
-    istuple_snd_update_def istuple_snd_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
+    by (auto simp add: iso_tuple_update_accessor_eq_assist_def intro: iso_tuple_update_accessor_cong_assist_id)
+  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
+    iso_tuple_snd_update_def iso_tuple_snd_def iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
 qed
 
-lemma istuple_cons_conj_eqI:
+lemma iso_tuple_cons_conj_eqI:
   "a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
-    istuple_cons isom a b = istuple_cons isom c d \<and> P \<longleftrightarrow> Q"
-  by (clarsimp simp: istuple_cons_def simps)
+    iso_tuple_cons isom a b = iso_tuple_cons isom c d \<and> P \<longleftrightarrow> Q"
+  by (clarsimp simp: iso_tuple_cons_def simps)
 
 lemmas intros =
-    istuple_access_update_fst_fst
-    istuple_access_update_snd_snd
-    istuple_access_update_fst_snd
-    istuple_access_update_snd_fst
-    istuple_update_swap_fst_fst
-    istuple_update_swap_snd_snd
-    istuple_update_swap_fst_snd
-    istuple_update_swap_snd_fst
-    istuple_update_compose_fst_fst
-    istuple_update_compose_snd_snd
-    istuple_surjective_proof_assist_step
-    istuple_fst_update_accessor_eq_assist
-    istuple_snd_update_accessor_eq_assist
-    istuple_fst_update_accessor_cong_assist
-    istuple_snd_update_accessor_cong_assist
-    istuple_cons_conj_eqI
+    iso_tuple_access_update_fst_fst
+    iso_tuple_access_update_snd_snd
+    iso_tuple_access_update_fst_snd
+    iso_tuple_access_update_snd_fst
+    iso_tuple_update_swap_fst_fst
+    iso_tuple_update_swap_snd_snd
+    iso_tuple_update_swap_fst_snd
+    iso_tuple_update_swap_snd_fst
+    iso_tuple_update_compose_fst_fst
+    iso_tuple_update_compose_snd_snd
+    iso_tuple_surjective_proof_assist_step
+    iso_tuple_fst_update_accessor_eq_assist
+    iso_tuple_snd_update_accessor_eq_assist
+    iso_tuple_fst_update_accessor_cong_assist
+    iso_tuple_snd_update_accessor_cong_assist
+    iso_tuple_cons_conj_eqI
 
 end
 
@@ -358,29 +339,32 @@
   fixes repr abst
   assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
      and abst_inv: "\<And>z. repr (abst z) = z"
-  assumes v: "v \<equiv> TupleIsomorphism repr abst"
+  assumes v: "v \<equiv> Tuple_Isomorphism repr abst"
   shows "isomorphic_tuple v"
-  apply (rule isomorphic_tuple.intro)
-  apply (simp_all add: abst_inv v)
-  apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
-  apply (simp add: abst_inv)
-  done
+proof
+  have "\<And>x. repr (abst (repr x)) = repr x"
+    by (simp add: abst_inv)
+  then show "\<And>x. Record.abst v (Record.repr v x) = x"
+    by (simp add: v repr_inj)
+  show P: "\<And>y. Record.repr v (Record.abst v y) = y"
+    by (simp add: v) (fact abst_inv)
+qed
 
 definition
-  "tuple_istuple \<equiv> TupleIsomorphism id id"
+  "tuple_iso_tuple \<equiv> Tuple_Isomorphism id id"
 
-lemma tuple_istuple:
-  "isomorphic_tuple tuple_istuple"
-  by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_istuple_def)
+lemma tuple_iso_tuple:
+  "isomorphic_tuple tuple_iso_tuple"
+  by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def)
 
 lemma refl_conj_eq:
   "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   by simp
 
-lemma istuple_UNIV_I: "x \<in> UNIV \<equiv> True"
+lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
   by simp
 
-lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
+lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   by simp
 
 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
@@ -437,9 +421,9 @@
 use "Tools/record.ML"
 setup Record.setup
 
-hide (open) const TupleIsomorphism repr abst istuple_fst istuple_snd
-  istuple_fst_update istuple_snd_update istuple_cons
-  istuple_surjective_proof_assist istuple_update_accessor_cong_assist
-  istuple_update_accessor_eq_assist tuple_istuple
+hide (open) const Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
+  iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
+  iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
+  iso_tuple_update_accessor_eq_assist tuple_iso_tuple
 
 end
diff -r a0efb4754cb7 -r 5da0f7abbe29 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Dec 19 09:07:04 2009 -0800
+++ b/src/HOL/Tools/record.ML	Mon Dec 21 08:32:22 2009 +0100
@@ -50,24 +50,24 @@
 end;
 
 
-signature ISTUPLE_SUPPORT =
+signature ISO_TUPLE_SUPPORT =
 sig
-  val add_istuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
+  val add_iso_tuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
   val mk_cons_tuple: term * term -> term
   val dest_cons_tuple: term -> term * term
-  val istuple_intros_tac: int -> tactic
+  val iso_tuple_intros_tac: int -> tactic
   val named_cterm_instantiate: (string * cterm) list -> thm -> thm
 end;
 
-structure IsTupleSupport: ISTUPLE_SUPPORT =
+structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
 struct
 
-val isomN = "_TupleIsom";
-
-val istuple_intro = @{thm isomorphic_tuple_intro};
-val istuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
-
-val tuple_istuple = (@{const_name tuple_istuple}, @{thm tuple_istuple});
+val isoN = "_Tuple_Iso";
+
+val iso_tuple_intro = @{thm isomorphic_tuple_intro};
+val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
+
+val tuple_iso_tuple = (@{const_name tuple_iso_tuple}, @{thm tuple_iso_tuple});
 
 fun named_cterm_instantiate values thm =
   let
@@ -81,10 +81,10 @@
     cterm_instantiate (map (apfst getvar) values) thm
   end;
 
-structure IsTupleThms = Theory_Data
+structure Iso_Tuple_Thms = Theory_Data
 (
   type T = thm Symtab.table;
-  val empty = Symtab.make [tuple_istuple];
+  val empty = Symtab.make [tuple_iso_tuple];
   val extend = I;
   fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
 );
@@ -96,7 +96,7 @@
         val SOME {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
           Abs_inverse = abs_inverse, ...} = Typedef.get_info thy name;
         val rewrite_rule =
-          MetaSimplifier.rewrite_rule [@{thm istuple_UNIV_I}, @{thm istuple_True_simp}];
+          MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
       in
         (map rewrite_rule [rep_inject, abs_inverse], Const (absN, repT --> absT), absT)
       end;
@@ -112,14 +112,14 @@
     val prodT = HOLogic.mk_prodT (leftT, rightT);
     val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
   in
-    Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> prodT) $
-      Const (fst tuple_istuple, isomT) $ left $ right
+    Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
+      Const (fst tuple_iso_tuple, isomT) $ left $ right
   end;
 
-fun dest_cons_tuple (Const (@{const_name istuple_cons}, _) $ Const _ $ t $ u) = (t, u)
+fun dest_cons_tuple (Const (@{const_name iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
   | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
 
-fun add_istuple_type (name, alphas) (leftT, rightT) thy =
+fun add_iso_tuple_type (name, alphas) (leftT, rightT) thy =
   let
     val repT = HOLogic.mk_prodT (leftT, rightT);
 
@@ -131,39 +131,39 @@
     (*construct a type and body for the isomorphism constant by
       instantiating the theorem to which the definition will be applied*)
     val intro_inst =
-      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] istuple_intro;
+      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
     val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
     val isomT = fastype_of body;
-    val isom_bind = Binding.name (name ^ isomN);
+    val isom_bind = Binding.name (name ^ isoN);
     val isom_name = Sign.full_name typ_thy isom_bind;
     val isom = Const (isom_name, isomT);
-    val isom_spec = (Thm.def_name (name ^ isomN), Logic.mk_equals (isom, body));
+    val isom_spec = (Thm.def_name (name ^ isoN), Logic.mk_equals (isom, body));
 
     val ([isom_def], cdef_thy) =
       typ_thy
       |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
       |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
 
-    val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
-    val cons = Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> absT);
+    val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
+    val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
 
     val thm_thy =
       cdef_thy
-      |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (isom_name, istuple))
+      |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
       |> Sign.parent_path
       |> Code.add_default_eqn isom_def;
   in
     ((isom, cons $ isom), thm_thy)
   end;
 
-val istuple_intros_tac = resolve_from_net_tac istuple_intros THEN'
+val iso_tuple_intros_tac = resolve_from_net_tac iso_tuple_intros THEN'
   CSUBGOAL (fn (cgoal, i) =>
     let
       val thy = Thm.theory_of_cterm cgoal;
       val goal = Thm.term_of cgoal;
 
-      val isthms = IsTupleThms.get thy;
-      fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
+      val isthms = Iso_Tuple_Thms.get thy;
+      fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);
 
       val goal' = Envir.beta_eta_contract goal;
       val is =
@@ -197,13 +197,13 @@
 
 val refl_conj_eq = @{thm refl_conj_eq};
 
-val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
-val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
+val surject_assistI = @{thm "iso_tuple_surjective_proof_assistI"};
+val surject_assist_idE = @{thm "iso_tuple_surjective_proof_assist_idE"};
 
 val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"};
 val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"};
-val updacc_eq_idI = @{thm "istuple_update_accessor_eq_assist_idI"};
-val updacc_eq_triv = @{thm "istuple_update_accessor_eq_assist_triv"};
+val updacc_eq_idI = @{thm "iso_tuple_update_accessor_eq_assist_idI"};
+val updacc_eq_triv = @{thm "iso_tuple_update_accessor_eq_assist_triv"};
 
 val updacc_foldE = @{thm "update_accessor_congruence_foldE"};
 val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"};
@@ -211,7 +211,7 @@
 val updacc_noop_compE = @{thm "update_accessor_noop_compE"};
 val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"};
 val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"};
-val updacc_cong_from_eq = @{thm "istuple_update_accessor_cong_from_eq"};
+val updacc_cong_from_eq = @{thm "iso_tuple_update_accessor_cong_from_eq"};
 
 val o_eq_dest = @{thm o_eq_dest};
 val o_eq_id_dest = @{thm o_eq_id_dest};
@@ -1066,7 +1066,7 @@
           Goal.prove (ProofContext.init thy) [] [] prop
             (fn _ =>
               simp_tac defset 1 THEN
-              REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
+              REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
               TRY (simp_tac (HOL_ss addsimps id_o_apps) 1));
         val dest =
           if is_sel_upd_pair thy acc upd
@@ -1089,7 +1089,7 @@
       Goal.prove (ProofContext.init thy) [] [] prop
         (fn _ =>
           simp_tac defset 1 THEN
-          REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
+          REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
           TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
     val dest = if comp then o_eq_dest_lhs else o_eq_dest;
   in Drule.standard (othm RS dest) end;
@@ -1117,7 +1117,7 @@
           else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
   in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
 
-val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
+val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate;
 
 fun prove_unfold_defs thy ex_simps ex_simprs prop =
   let
@@ -1222,7 +1222,7 @@
     Goal.prove (ProofContext.init thy) [] [] prop
       (fn _ =>
         simp_tac simpset 1 THEN
-        REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
+        REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
         TRY (resolve_tac [updacc_cong_idI] 1))
   end;
 
@@ -1612,22 +1612,22 @@
     (*before doing anything else, create the tree of new types
       that will back the record extension*)
 
-    val mktreeV = Balanced_Tree.make IsTupleSupport.mk_cons_tuple;
-
-    fun mk_istuple (left, right) (thy, i) =
+    val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
+
+    fun mk_iso_tuple (left, right) (thy, i) =
       let
         val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
         val nm = suffix suff (Long_Name.base_name name);
         val ((_, cons), thy') =
-          IsTupleSupport.add_istuple_type
+          Iso_Tuple_Support.add_iso_tuple_type
             (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
       in
         (cons $ left $ right, (thy', i + 1))
       end;
 
-    (*trying to create a 1-element istuple will fail, and is pointless anyway*)
-    fun mk_even_istuple [arg] = pair arg
-      | mk_even_istuple args = mk_istuple (IsTupleSupport.dest_cons_tuple (mktreeV args));
+    (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*)
+    fun mk_even_iso_tuple [arg] = pair arg
+      | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args));
 
     fun build_meta_tree_type i thy vars more =
       let val len = length vars in
@@ -1637,12 +1637,12 @@
             fun group16 [] = []
               | group16 xs = take 16 xs :: group16 (drop 16 xs);
             val vars' = group16 vars;
-            val (composites, (thy', i')) = fold_map mk_even_istuple vars' (thy, i);
+            val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i);
           in
             build_meta_tree_type i' thy' composites more
           end
         else
-          let val (term, (thy', _)) = mk_istuple (mktreeV vars, more) (thy, 0)
+          let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0)
           in (term, thy') end
       end;
 
@@ -1712,7 +1712,7 @@
             simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
             REPEAT_DETERM
               (rtac refl_conj_eq 1 ORELSE
-                IsTupleSupport.istuple_intros_tac 1 ORELSE
+                Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
                 rtac refl 1)));
 
     val inject = timeit_msg "record extension inject proof:" inject_prf;
@@ -1730,7 +1730,7 @@
         val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
         val tactic1 =
           simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
-          REPEAT_ALL_NEW IsTupleSupport.istuple_intros_tac 1;
+          REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
         val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
         val [halfway] = Seq.list_of (tactic1 start);
         val [surject] = Seq.list_of (tactic2 (Drule.standard halfway));
@@ -1954,7 +1954,7 @@
 
     val ext_defs = ext_def :: map #extdef parents;
 
-    (*Theorems from the istuple intros.
+    (*Theorems from the iso_tuple intros.
       This is complex enough to deserve a full comment.
       By unfolding ext_defs from r_rec0 we create a tree of constructor
       calls (many of them Pair, but others as well). The introduction
@@ -1979,7 +1979,7 @@
         val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
         val tactic =
           simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
-          REPEAT (IsTupleSupport.istuple_intros_tac 1 ORELSE terminal);
+          REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
         val updaccs = Seq.list_of (tactic init_thm);
       in
         (updaccs RL [updacc_accessor_eqE],
@@ -2207,7 +2207,7 @@
              [rtac surject_assist_idE 1,
               simp_tac init_ss 1,
               REPEAT
-                (IsTupleSupport.istuple_intros_tac 1 ORELSE
+                (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
                   (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
       end;
     val surjective = timeit_msg "record surjective proof:" surjective_prf;
diff -r a0efb4754cb7 -r 5da0f7abbe29 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Sat Dec 19 09:07:04 2009 -0800
+++ b/src/Tools/Code/code_printer.ML	Mon Dec 21 08:32:22 2009 +0100
@@ -59,16 +59,16 @@
   val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
 
   type tyco_syntax
+  type simple_const_syntax
+  type proto_const_syntax
   type const_syntax
-  type proto_const_syntax
   val parse_infix: ('a -> 'b) -> lrx * int -> string
     -> int * ((fixity -> 'b -> Pretty.T)
     -> fixity -> 'a list -> Pretty.T)
   val parse_syntax: ('a -> 'b) -> OuterParse.token list
     -> (int * ((fixity -> 'b -> Pretty.T)
     -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
-  val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
-    -> fixity -> (iterm * itype) list -> Pretty.T)) option -> proto_const_syntax option
+  val simple_const_syntax: simple_const_syntax -> proto_const_syntax
   val activate_const_syntax: theory -> literals
     -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
   val gen_print_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
@@ -219,15 +219,17 @@
 
 type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
   -> fixity -> itype list -> Pretty.T);
-type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
-  -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+
+type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
+  -> fixity -> (iterm * itype) list -> Pretty.T);
 type proto_const_syntax = int * (string list * (literals -> string list
   -> (var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
+type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
+  -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
 
-fun simple_const_syntax (SOME (n, f)) = SOME (n,
-      ([], (fn _ => fn _ => fn print => fn thm => fn vars => f (print vars))))
-  | simple_const_syntax NONE = NONE;
+val simple_const_syntax =
+  apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars))));
 
 fun activate_const_syntax thy literals (n, (cs, f)) naming =
   fold_map (Code_Thingol.ensure_declared_const thy) cs naming
@@ -307,7 +309,7 @@
 
 fun parse_syntax prep_arg xs =
   Scan.option ((
-      ((OuterParse.$$$ infixK  >> K X)
+      ((OuterParse.$$$ infixK >> K X)
         || (OuterParse.$$$ infixlK >> K L)
         || (OuterParse.$$$ infixrK >> K R))
         -- OuterParse.nat >> parse_infix prep_arg
diff -r a0efb4754cb7 -r 5da0f7abbe29 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sat Dec 19 09:07:04 2009 -0800
+++ b/src/Tools/Code/code_target.ML	Mon Dec 21 08:32:22 2009 +0100
@@ -6,9 +6,8 @@
 
 signature CODE_TARGET =
 sig
-  include CODE_PRINTER
-
   type serializer
+  type literals = Code_Printer.literals
   val add_target: string * (serializer * literals) -> theory -> theory
   val extend_target: string *
       (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
@@ -39,6 +38,8 @@
   val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
 
   val allow_abort: string -> theory -> theory
+  type tyco_syntax = Code_Printer.tyco_syntax
+  type proto_const_syntax = Code_Printer.proto_const_syntax
   val add_syntax_class: string -> class -> string option -> theory -> theory
   val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
   val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
@@ -51,7 +52,11 @@
 struct
 
 open Basic_Code_Thingol;
-open Code_Printer;
+
+type literals = Code_Printer.literals;
+type tyco_syntax = Code_Printer.tyco_syntax;
+type proto_const_syntax = Code_Printer.proto_const_syntax;
+
 
 (** basics **)
 
@@ -78,8 +83,8 @@
 datatype name_syntax_table = NameSyntaxTable of {
   class: string Symtab.table,
   instance: unit Symreltab.table,
-  tyco: tyco_syntax Symtab.table,
-  const: proto_const_syntax Symtab.table
+  tyco: Code_Printer.tyco_syntax Symtab.table,
+  const: Code_Printer.proto_const_syntax Symtab.table
 };
 
 fun mk_name_syntax_table ((class, instance), (tyco, const)) =
@@ -103,14 +108,14 @@
   -> (string * Pretty.T) list           (*includes*)
   -> (string -> string option)          (*module aliasses*)
   -> (string -> string option)          (*class syntax*)
-  -> (string -> tyco_syntax option)
-  -> (string -> const_syntax option)
+  -> (string -> Code_Printer.tyco_syntax option)
+  -> (string -> Code_Printer.const_syntax option)
   -> ((Pretty.T -> string) * (Pretty.T -> unit))
   -> Code_Thingol.program
   -> string list                        (*selected statements*)
   -> serialization;
 
-datatype serializer_entry = Serializer of serializer * literals
+datatype serializer_entry = Serializer of serializer * Code_Printer.literals
   | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
 
 datatype target = Target of {
@@ -273,7 +278,7 @@
     serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
       (Symtab.lookup module_alias) (Symtab.lookup class')
       (Symtab.lookup tyco') (Symtab.lookup const')
-      (string_of_pretty width, writeln_pretty width)
+      (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
       program4 names2
   end;
 
@@ -396,32 +401,32 @@
 fun read_inst thy (raw_tyco, raw_class) =
   (read_class thy raw_class, read_tyco thy raw_tyco);
 
-fun gen_add_syntax upd del mapp check_x get_check_syn prep target raw_x some_syn thy =
+fun gen_add_syntax upd del mapp check_x check_raw_syn prep_syn prep_x target raw_x some_raw_syn thy =
   let
-    val x = prep thy raw_x;
-    fun check_syn thy syn = ();
-  in case some_syn
-   of SOME syn => (map_name_syntax target o mapp) (upd (x, (check_x thy x; check_syn thy syn; syn))) thy
+    val x = prep_x thy raw_x |> tap (check_x thy);
+    fun prep_check raw_syn = prep_syn (raw_syn |> tap (check_raw_syn thy target));
+  in case some_raw_syn
+   of SOME raw_syn => (map_name_syntax target o mapp) (upd (x, prep_check raw_syn)) thy
     | NONE => (map_name_syntax target o mapp) (del x) thy
   end;
 
-fun gen_add_syntax_class prep =
-  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) I prep;
+fun gen_add_syntax_class prep_class =
+  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) ((K o K o K) ()) I prep_class;
 
-fun gen_add_syntax_inst prep =
-  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) I prep;
+fun gen_add_syntax_inst prep_inst =
+  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) ((K o K o K) ()) I prep_inst;
 
-fun gen_add_syntax_tyco prep =
+fun gen_add_syntax_tyco prep_tyco =
   gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apfst)
     (fn thy => fn tyco => fn (n, _) => if n <> Sign.arity_number thy tyco
       then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
-      else ()) I prep;
+      else ()) ((K o K o K) ()) I prep_tyco;
 
-fun gen_add_syntax_const prep =
+fun gen_add_syntax_const prep_const check_raw_syn prep_syn =
   gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apsnd)
     (fn thy => fn c => fn (n, _) => if n > Code.args_number thy c
       then error ("Too many arguments in syntax for constant " ^ quote c)
-      else ()) I prep;
+      else ()) check_raw_syn prep_syn prep_const;
 
 fun add_reserved target =
   let
@@ -438,7 +443,7 @@
               then warning ("Overwriting existing include " ^ name)
               else ();
             val cs = map (read_const thy) raw_cs;
-          in Symtab.update (name, (str content, cs)) incls end
+          in Symtab.update (name, (Code_Printer.str content, cs)) incls end
       | add (name, NONE) incls = Symtab.delete name incls;
   in map_includes target (add args) thy end;
 
@@ -460,12 +465,6 @@
     val c = prep_const thy raw_c;
   in thy |> (CodeTargetData.map o apfst o apsnd) (insert (op =) c) end;
 
-fun zip_list (x::xs) f g =
-  f
-  #-> (fn y =>
-    fold_map (fn x => g |-- f >> pair x) xs
-    #-> (fn xys => pair ((x, y) :: xys)));
-
 
 (* concrete syntax *)
 
@@ -474,6 +473,12 @@
 structure P = OuterParse
 and K = OuterKeyword
 
+fun zip_list (x::xs) f g =
+  f
+  #-> (fn y =>
+    fold_map (fn x => g |-- f >> pair x) xs
+    #-> (fn xys => pair ((x, y) :: xys)));
+
 fun parse_multi_syntax parse_thing parse_syntax =
   P.and_list1 parse_thing
   #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
@@ -484,7 +489,8 @@
 val add_syntax_class = gen_add_syntax_class cert_class;
 val add_syntax_inst = gen_add_syntax_inst cert_inst;
 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
-val add_syntax_const = gen_add_syntax_const (K I);
+val add_syntax_const_simple = gen_add_syntax_const (K I) ((K o K o K) ()) Code_Printer.simple_const_syntax;
+val add_syntax_const = gen_add_syntax_const (K I) ((K o K o K) ()) I;
 val allow_abort = gen_allow_abort (K I);
 val add_reserved = add_reserved;
 val add_include = add_include;
@@ -492,7 +498,9 @@
 val add_syntax_class_cmd = gen_add_syntax_class read_class;
 val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
-val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
+val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) Code_Printer.simple_const_syntax;
+val add_syntax_const_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) I;
+
 val allow_abort_cmd = gen_allow_abort Code.read_const;
 
 fun parse_args f args =
@@ -524,25 +532,23 @@
 
 val _ =
   OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
-    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
-      (Scan.option (P.minus >> K ()))
+    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) (Scan.option (P.minus >> K ()))
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
           fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
   );
 
 val _ =
   OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
-    parse_multi_syntax P.xname (parse_syntax I)
+    parse_multi_syntax P.xname (Code_Printer.parse_syntax I)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
           fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
   );
 
 val _ =
   OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
-    parse_multi_syntax P.term_group (parse_syntax fst)
+    parse_multi_syntax P.term_group (Code_Printer.parse_syntax fst)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
-      fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const
-        (Code_Printer.simple_const_syntax syn)) syns)
+      fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
   );
 
 val _ =