src/HOL/Record.thy
author haftmann
Fri Nov 27 08:41:10 2009 +0100 (2009-11-27)
changeset 33963 977b94b64905
parent 33595 7264824baf66
child 34151 8d57ce46b3f7
permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
     1 (*  Title:      HOL/Record.thy
     2     Author:     Wolfgang Naraschewski, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
     4     Author:     Norbert Schirmer, TU Muenchen
     5     Author:     Thomas Sewell, NICTA
     6     Author:     Florian Haftmann, TU Muenchen
     7 *)
     8 
     9 header {* Extensible records with structural subtyping *}
    10 
    11 theory Record
    12 imports Datatype
    13 uses ("Tools/record.ML")
    14 begin
    15 
    16 subsection {* Introduction *}
    17 
    18 text {*
    19   Records are isomorphic to compound tuple types. To implement
    20   efficient records, we make this isomorphism explicit. Consider the
    21   record access/update simplification @{text "alpha (beta_update f
    22   rec) = alpha rec"} for distinct fields alpha and beta of some record
    23   rec with n fields. There are @{text "n ^ 2"} such theorems, which
    24   prohibits storage of all of them for large n. The rules can be
    25   proved on the fly by case decomposition and simplification in O(n)
    26   time. By creating O(n) isomorphic-tuple types while defining the
    27   record, however, we can prove the access/update simplification in
    28   @{text "O(log(n)^2)"} time.
    29 
    30   The O(n) cost of case decomposition is not because O(n) steps are
    31   taken, but rather because the resulting rule must contain O(n) new
    32   variables and an O(n) size concrete record construction. To sidestep
    33   this cost, we would like to avoid case decomposition in proving
    34   access/update theorems.
    35 
    36   Record types are defined as isomorphic to tuple types. For instance,
    37   a record type with fields @{text "'a"}, @{text "'b"}, @{text "'c"}
    38   and @{text "'d"} might be introduced as isomorphic to @{text "'a \<times>
    39   ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to @{text "('a \<times>
    40   'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to the
    41   underlying type then using O(log(n)) fst or snd operations.
    42   Updators can be defined similarly, if we introduce a @{text
    43   "fst_update"} and @{text "snd_update"} function. Furthermore, we can
    44   prove the access/update theorem in O(log(n)) steps by using simple
    45   rewrites on fst, snd, @{text "fst_update"} and @{text "snd_update"}.
    46 
    47   The catch is that, although O(log(n)) steps were taken, the
    48   underlying type we converted to is a tuple tree of size
    49   O(n). Processing this term type wastes performance. We avoid this
    50   for large n by taking each subtree of size K and defining a new type
    51   isomorphic to that tuple subtree. A record can now be defined as
    52   isomorphic to a tuple tree of these O(n/K) new types, or, if @{text
    53   "n > K*K"}, we can repeat the process, until the record can be
    54   defined in terms of a tuple tree of complexity less than the
    55   constant K.
    56 
    57   If we prove the access/update theorem on this type with the
    58   analagous steps to the tuple tree, we consume @{text "O(log(n)^2)"}
    59   time as the intermediate terms are @{text "O(log(n))"} in size and
    60   the types needed have size bounded by K.  To enable this analagous
    61   traversal, we define the functions seen below: @{text
    62   "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"}
    63   and @{text "istuple_snd_update"}. These functions generalise tuple
    64   operations by taking a parameter that encapsulates a tuple
    65   isomorphism.  The rewrites needed on these functions now need an
    66   additional assumption which is that the isomorphism works.
    67 
    68   These rewrites are typically used in a structured way. They are here
    69   presented as the introduction rule @{text "isomorphic_tuple.intros"}
    70   rather than as a rewrite rule set. The introduction form is an
    71   optimisation, as net matching can be performed at one term location
    72   for each step rather than the simplifier searching the term for
    73   possible pattern matches. The rule set is used as it is viewed
    74   outside the locale, with the locale assumption (that the isomorphism
    75   is valid) left as a rule assumption. All rules are structured to aid
    76   net matching, using either a point-free form or an encapsulating
    77   predicate.
    78 *}
    79 
    80 subsection {* Operators and lemmas for types isomorphic to tuples *}
    81 
    82 datatype ('a, 'b, 'c) tuple_isomorphism = TupleIsomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
    83 
    84 primrec repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where
    85   "repr (TupleIsomorphism r a) = r"
    86 
    87 primrec abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
    88   "abst (TupleIsomorphism r a) = a"
    89 
    90 definition istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
    91   "istuple_fst isom = fst \<circ> repr isom"
    92 
    93 definition istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
    94   "istuple_snd isom = snd \<circ> repr isom"
    95 
    96 definition istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    97   "istuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
    98 
    99 definition istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
   100   "istuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
   101 
   102 definition istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
   103   "istuple_cons isom = curry (abst isom)"
   104 
   105 
   106 subsection {* Logical infrastructure for records *}
   107 
   108 definition istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   109   "istuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
   110 
   111 definition istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   112   "istuple_update_accessor_cong_assist upd acc \<longleftrightarrow> 
   113      (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
   114 
   115 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
   116   "istuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow>
   117      upd f v = v' \<and> acc v = x \<and> istuple_update_accessor_cong_assist upd acc"
   118 
   119 lemma update_accessor_congruence_foldE:
   120   assumes uac: "istuple_update_accessor_cong_assist upd acc"
   121   and       r: "r = r'" and v: "acc r' = v'"
   122   and       f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
   123   shows        "upd f r = upd f' r'"
   124   using uac r v [symmetric]
   125   apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
   126    apply (simp add: istuple_update_accessor_cong_assist_def)
   127   apply (simp add: f)
   128   done
   129 
   130 lemma update_accessor_congruence_unfoldE:
   131   "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> r = r' \<Longrightarrow> acc r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v)
   132      \<Longrightarrow> upd f r = upd f' r'"
   133   apply (erule(2) update_accessor_congruence_foldE)
   134   apply simp
   135   done
   136 
   137 lemma istuple_update_accessor_cong_assist_id:
   138   "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
   139   by rule (simp add: istuple_update_accessor_cong_assist_def)
   140 
   141 lemma update_accessor_noopE:
   142   assumes uac: "istuple_update_accessor_cong_assist upd acc"
   143       and acc: "f (acc x) = acc x"
   144   shows        "upd f x = x"
   145 using uac by (simp add: acc istuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
   146   cong: update_accessor_congruence_unfoldE [OF uac])
   147 
   148 lemma update_accessor_noop_compE:
   149   assumes uac: "istuple_update_accessor_cong_assist upd acc"
   150   assumes acc: "f (acc x) = acc x"
   151   shows      "upd (g \<circ> f) x = upd g x"
   152   by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
   153 
   154 lemma update_accessor_cong_assist_idI:
   155   "istuple_update_accessor_cong_assist id id"
   156   by (simp add: istuple_update_accessor_cong_assist_def)
   157 
   158 lemma update_accessor_cong_assist_triv:
   159   "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   160   by assumption
   161 
   162 lemma update_accessor_accessor_eqE:
   163   "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> acc v = x"
   164   by (simp add: istuple_update_accessor_eq_assist_def)
   165 
   166 lemma update_accessor_updator_eqE:
   167   "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> upd f v = v'"
   168   by (simp add: istuple_update_accessor_eq_assist_def)
   169 
   170 lemma istuple_update_accessor_eq_assist_idI:
   171   "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
   172   by (simp add: istuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
   173 
   174 lemma istuple_update_accessor_eq_assist_triv:
   175   "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
   176   by assumption
   177 
   178 lemma istuple_update_accessor_cong_from_eq:
   179   "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   180   by (simp add: istuple_update_accessor_eq_assist_def)
   181 
   182 lemma o_eq_dest:
   183   "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
   184   apply (clarsimp simp: o_def)
   185   apply (erule fun_cong)
   186   done
   187 
   188 lemma o_eq_elim:
   189   "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
   190   apply (erule meta_mp)
   191   apply (erule o_eq_dest)
   192   done
   193 
   194 lemma istuple_surjective_proof_assistI:
   195   "f x = y \<Longrightarrow> istuple_surjective_proof_assist x y f"
   196   by (simp add: istuple_surjective_proof_assist_def)
   197 
   198 lemma istuple_surjective_proof_assist_idE:
   199   "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   200   by (simp add: istuple_surjective_proof_assist_def)
   201 
   202 locale isomorphic_tuple =
   203   fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
   204     and repr and abst
   205   defines "repr \<equiv> Record.repr isom"
   206   defines "abst \<equiv> Record.abst isom"
   207   assumes repr_inv: "\<And>x. abst (repr x) = x"
   208   assumes abst_inv: "\<And>y. repr (abst y) = y"
   209 begin
   210 
   211 lemma repr_inj:
   212   "repr x = repr y \<longleftrightarrow> x = y"
   213   apply (rule iffI, simp_all)
   214   apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
   215   done
   216 
   217 lemma abst_inj:
   218   "abst x = abst y \<longleftrightarrow> x = y"
   219   apply (rule iffI, simp_all)
   220   apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
   221   done
   222 
   223 lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj repr_def [symmetric] abst_def [symmetric]
   224 
   225 lemma istuple_access_update_fst_fst:
   226   "f o h g = j o f \<Longrightarrow>
   227     (f o istuple_fst isom) o (istuple_fst_update isom o h) g
   228           = j o (f o istuple_fst isom)"
   229   by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
   230              intro!: ext elim!: o_eq_elim)
   231 
   232 lemma istuple_access_update_snd_snd:
   233   "f o h g = j o f \<Longrightarrow>
   234     (f o istuple_snd isom) o (istuple_snd_update isom o h) g
   235           = j o (f o istuple_snd isom)"
   236   by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
   237              intro!: ext elim!: o_eq_elim)
   238 
   239 lemma istuple_access_update_fst_snd:
   240   "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
   241           = id o (f o istuple_fst isom)"
   242   by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
   243              intro!: ext elim!: o_eq_elim)
   244 
   245 lemma istuple_access_update_snd_fst:
   246   "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
   247           = id o (f o istuple_snd isom)"
   248   by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
   249              intro!: ext elim!: o_eq_elim)
   250 
   251 lemma istuple_update_swap_fst_fst:
   252   "h f o j g = j g o h f \<Longrightarrow>
   253     (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   254           = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
   255   by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
   256 
   257 lemma istuple_update_swap_snd_snd:
   258   "h f o j g = j g o h f \<Longrightarrow>
   259     (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   260           = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
   261   by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
   262 
   263 lemma istuple_update_swap_fst_snd:
   264   "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
   265           = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
   266   by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
   267 
   268 lemma istuple_update_swap_snd_fst:
   269   "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
   270           = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
   271   by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
   272 
   273 lemma istuple_update_compose_fst_fst:
   274   "h f o j g = k (f o g) \<Longrightarrow>
   275     (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   276           = (istuple_fst_update isom o k) (f o g)"
   277   by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
   278 
   279 lemma istuple_update_compose_snd_snd:
   280   "h f o j g = k (f o g) \<Longrightarrow>
   281     (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   282           = (istuple_snd_update isom o k) (f o g)"
   283   by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
   284 
   285 lemma istuple_surjective_proof_assist_step:
   286   "istuple_surjective_proof_assist v a (istuple_fst isom o f) \<Longrightarrow>
   287      istuple_surjective_proof_assist v b (istuple_snd isom o f)
   288       \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
   289   by (clarsimp simp: istuple_surjective_proof_assist_def simps
   290     istuple_fst_def istuple_snd_def istuple_cons_def)
   291 
   292 lemma istuple_fst_update_accessor_cong_assist:
   293   assumes "istuple_update_accessor_cong_assist f g"
   294   shows "istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
   295 proof -
   296   from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
   297   with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   298     istuple_fst_update_def istuple_fst_def)
   299 qed
   300 
   301 lemma istuple_snd_update_accessor_cong_assist:
   302   assumes "istuple_update_accessor_cong_assist f g"
   303   shows "istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
   304 proof -
   305   from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
   306   with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   307     istuple_snd_update_def istuple_snd_def)
   308 qed
   309 
   310 lemma istuple_fst_update_accessor_eq_assist:
   311   assumes "istuple_update_accessor_eq_assist f g a u a' v"
   312   shows "istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
   313     (istuple_cons isom a b) u (istuple_cons isom a' b) v"
   314 proof -
   315   from assms have "f id = id"
   316     by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
   317   with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
   318     istuple_fst_update_def istuple_fst_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   319 qed
   320 
   321 lemma istuple_snd_update_accessor_eq_assist:
   322   assumes "istuple_update_accessor_eq_assist f g b u b' v"
   323   shows "istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
   324     (istuple_cons isom a b) u (istuple_cons isom a b') v"
   325 proof -
   326   from assms have "f id = id"
   327     by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
   328   with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
   329     istuple_snd_update_def istuple_snd_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   330 qed
   331 
   332 lemma istuple_cons_conj_eqI:
   333   "a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
   334     istuple_cons isom a b = istuple_cons isom c d \<and> P \<longleftrightarrow> Q"
   335   by (clarsimp simp: istuple_cons_def simps)
   336 
   337 lemmas intros =
   338     istuple_access_update_fst_fst
   339     istuple_access_update_snd_snd
   340     istuple_access_update_fst_snd
   341     istuple_access_update_snd_fst
   342     istuple_update_swap_fst_fst
   343     istuple_update_swap_snd_snd
   344     istuple_update_swap_fst_snd
   345     istuple_update_swap_snd_fst
   346     istuple_update_compose_fst_fst
   347     istuple_update_compose_snd_snd
   348     istuple_surjective_proof_assist_step
   349     istuple_fst_update_accessor_eq_assist
   350     istuple_snd_update_accessor_eq_assist
   351     istuple_fst_update_accessor_cong_assist
   352     istuple_snd_update_accessor_cong_assist
   353     istuple_cons_conj_eqI
   354 
   355 end
   356 
   357 lemma isomorphic_tuple_intro:
   358   fixes repr abst
   359   assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
   360      and abst_inv: "\<And>z. repr (abst z) = z"
   361   assumes v: "v \<equiv> TupleIsomorphism repr abst"
   362   shows "isomorphic_tuple v"
   363   apply (rule isomorphic_tuple.intro)
   364   apply (simp_all add: abst_inv v)
   365   apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
   366   apply (simp add: abst_inv)
   367   done
   368 
   369 definition
   370   "tuple_istuple \<equiv> TupleIsomorphism id id"
   371 
   372 lemma tuple_istuple:
   373   "isomorphic_tuple tuple_istuple"
   374   by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_istuple_def)
   375 
   376 lemma refl_conj_eq:
   377   "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   378   by simp
   379 
   380 lemma istuple_UNIV_I: "x \<in> UNIV \<equiv> True"
   381   by simp
   382 
   383 lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   384   by simp
   385 
   386 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
   387   by simp
   388 
   389 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" 
   390   by (simp add: comp_def)
   391 
   392 lemma o_eq_dest_lhs:
   393   "a o b = c \<Longrightarrow> a (b v) = c v"
   394   by clarsimp
   395 
   396 lemma o_eq_id_dest:
   397   "a o b = id o c \<Longrightarrow> a (b v) = c v"
   398   by clarsimp
   399 
   400 
   401 subsection {* Concrete record syntax *}
   402 
   403 nonterminals
   404   ident field_type field_types field fields update updates
   405 syntax
   406   "_constify"           :: "id => ident"                        ("_")
   407   "_constify"           :: "longid => ident"                    ("_")
   408 
   409   "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
   410   ""                    :: "field_type => field_types"          ("_")
   411   "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
   412   "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
   413   "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
   414 
   415   "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
   416   ""                    :: "field => fields"                    ("_")
   417   "_fields"             :: "[field, fields] => fields"          ("_,/ _")
   418   "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
   419   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
   420 
   421   "_update_name"        :: idt
   422   "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
   423   ""                    :: "update => updates"                  ("_")
   424   "_updates"            :: "[update, updates] => updates"       ("_,/ _")
   425   "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
   426 
   427 syntax (xsymbols)
   428   "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
   429   "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
   430   "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
   431   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   432   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
   433 
   434 
   435 subsection {* Record package *}
   436 
   437 use "Tools/record.ML"
   438 setup Record.setup
   439 
   440 hide (open) const TupleIsomorphism repr abst istuple_fst istuple_snd
   441   istuple_fst_update istuple_snd_update istuple_cons
   442   istuple_surjective_proof_assist istuple_update_accessor_cong_assist
   443   istuple_update_accessor_eq_assist tuple_istuple
   444 
   445 end