src/HOL/Record.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 34151 8d57ce46b3f7
child 35132 d137efecf793
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     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   "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"}
    63   and @{text "iso_tuple_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 = Tuple_Isomorphism "'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 (Tuple_Isomorphism r a) = r"
    86 
    87 primrec abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
    88   "abst (Tuple_Isomorphism r a) = a"
    89 
    90 definition iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
    91   "iso_tuple_fst isom = fst \<circ> repr isom"
    92 
    93 definition iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
    94   "iso_tuple_snd isom = snd \<circ> repr isom"
    95 
    96 definition iso_tuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    97   "iso_tuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
    98 
    99 definition iso_tuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
   100   "iso_tuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
   101 
   102 definition iso_tuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
   103   "iso_tuple_cons isom = curry (abst isom)"
   104 
   105 
   106 subsection {* Logical infrastructure for records *}
   107 
   108 definition iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   109   "iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
   110 
   111 definition iso_tuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   112   "iso_tuple_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 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
   116   "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow>
   117      upd f v = v' \<and> acc v = x \<and> iso_tuple_update_accessor_cong_assist upd acc"
   118 
   119 lemma update_accessor_congruence_foldE:
   120   assumes uac: "iso_tuple_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: iso_tuple_update_accessor_cong_assist_def)
   127   apply (simp add: f)
   128   done
   129 
   130 lemma update_accessor_congruence_unfoldE:
   131   "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)
   132      \<Longrightarrow> upd f r = upd f' r'"
   133   apply (erule(2) update_accessor_congruence_foldE)
   134   apply simp
   135   done
   136 
   137 lemma iso_tuple_update_accessor_cong_assist_id:
   138   "iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
   139   by rule (simp add: iso_tuple_update_accessor_cong_assist_def)
   140 
   141 lemma update_accessor_noopE:
   142   assumes uac: "iso_tuple_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 iso_tuple_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: "iso_tuple_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   "iso_tuple_update_accessor_cong_assist id id"
   156   by (simp add: iso_tuple_update_accessor_cong_assist_def)
   157 
   158 lemma update_accessor_cong_assist_triv:
   159   "iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> iso_tuple_update_accessor_cong_assist upd acc"
   160   by assumption
   161 
   162 lemma update_accessor_accessor_eqE:
   163   "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> acc v = x"
   164   by (simp add: iso_tuple_update_accessor_eq_assist_def)
   165 
   166 lemma update_accessor_updator_eqE:
   167   "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> upd f v = v'"
   168   by (simp add: iso_tuple_update_accessor_eq_assist_def)
   169 
   170 lemma iso_tuple_update_accessor_eq_assist_idI:
   171   "v' = f v \<Longrightarrow> iso_tuple_update_accessor_eq_assist id id v f v' v"
   172   by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
   173 
   174 lemma iso_tuple_update_accessor_eq_assist_triv:
   175   "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"
   176   by assumption
   177 
   178 lemma iso_tuple_update_accessor_cong_from_eq:
   179   "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> iso_tuple_update_accessor_cong_assist upd acc"
   180   by (simp add: iso_tuple_update_accessor_eq_assist_def)
   181 
   182 lemma iso_tuple_surjective_proof_assistI:
   183   "f x = y \<Longrightarrow> iso_tuple_surjective_proof_assist x y f"
   184   by (simp add: iso_tuple_surjective_proof_assist_def)
   185 
   186 lemma iso_tuple_surjective_proof_assist_idE:
   187   "iso_tuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   188   by (simp add: iso_tuple_surjective_proof_assist_def)
   189 
   190 locale isomorphic_tuple =
   191   fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
   192   assumes repr_inv: "\<And>x. abst isom (repr isom x) = x"
   193   assumes abst_inv: "\<And>y. repr isom (abst isom y) = y"
   194 begin
   195 
   196 lemma repr_inj:
   197   "repr isom x = repr isom y \<longleftrightarrow> x = y"
   198   by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"] simp add: repr_inv)
   199 
   200 lemma abst_inj:
   201   "abst isom x = abst isom y \<longleftrightarrow> x = y"
   202   by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"] simp add: abst_inv)
   203 
   204 lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj
   205 
   206 lemma iso_tuple_access_update_fst_fst:
   207   "f o h g = j o f \<Longrightarrow>
   208     (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g
   209           = j o (f o iso_tuple_fst isom)"
   210   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps
   211              intro!: ext elim!: o_eq_elim)
   212 
   213 lemma iso_tuple_access_update_snd_snd:
   214   "f o h g = j o f \<Longrightarrow>
   215     (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g
   216           = j o (f o iso_tuple_snd isom)"
   217   by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps
   218              intro!: ext elim!: o_eq_elim)
   219 
   220 lemma iso_tuple_access_update_fst_snd:
   221   "(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g
   222           = id o (f o iso_tuple_fst isom)"
   223   by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps
   224              intro!: ext elim!: o_eq_elim)
   225 
   226 lemma iso_tuple_access_update_snd_fst:
   227   "(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g
   228           = id o (f o iso_tuple_snd isom)"
   229   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps
   230              intro!: ext elim!: o_eq_elim)
   231 
   232 lemma iso_tuple_update_swap_fst_fst:
   233   "h f o j g = j g o h f \<Longrightarrow>
   234     (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g
   235           = (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f"
   236   by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
   237 
   238 lemma iso_tuple_update_swap_snd_snd:
   239   "h f o j g = j g o h f \<Longrightarrow>
   240     (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g
   241           = (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f"
   242   by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
   243 
   244 lemma iso_tuple_update_swap_fst_snd:
   245   "(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g
   246           = (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f"
   247   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext)
   248 
   249 lemma iso_tuple_update_swap_snd_fst:
   250   "(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g
   251           = (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f"
   252   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext)
   253 
   254 lemma iso_tuple_update_compose_fst_fst:
   255   "h f o j g = k (f o g) \<Longrightarrow>
   256     (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g
   257           = (iso_tuple_fst_update isom o k) (f o g)"
   258   by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
   259 
   260 lemma iso_tuple_update_compose_snd_snd:
   261   "h f o j g = k (f o g) \<Longrightarrow>
   262     (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g
   263           = (iso_tuple_snd_update isom o k) (f o g)"
   264   by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
   265 
   266 lemma iso_tuple_surjective_proof_assist_step:
   267   "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \<Longrightarrow>
   268      iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f)
   269       \<Longrightarrow> iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f"
   270   by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps
   271     iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def)
   272 
   273 lemma iso_tuple_fst_update_accessor_cong_assist:
   274   assumes "iso_tuple_update_accessor_cong_assist f g"
   275   shows "iso_tuple_update_accessor_cong_assist (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)"
   276 proof -
   277   from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id)
   278   with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
   279     iso_tuple_fst_update_def iso_tuple_fst_def)
   280 qed
   281 
   282 lemma iso_tuple_snd_update_accessor_cong_assist:
   283   assumes "iso_tuple_update_accessor_cong_assist f g"
   284   shows "iso_tuple_update_accessor_cong_assist (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)"
   285 proof -
   286   from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id)
   287   with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
   288     iso_tuple_snd_update_def iso_tuple_snd_def)
   289 qed
   290 
   291 lemma iso_tuple_fst_update_accessor_eq_assist:
   292   assumes "iso_tuple_update_accessor_eq_assist f g a u a' v"
   293   shows "iso_tuple_update_accessor_eq_assist (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)
   294     (iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v"
   295 proof -
   296   from assms have "f id = id"
   297     by (auto simp add: iso_tuple_update_accessor_eq_assist_def intro: iso_tuple_update_accessor_cong_assist_id)
   298   with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
   299     iso_tuple_fst_update_def iso_tuple_fst_def iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
   300 qed
   301 
   302 lemma iso_tuple_snd_update_accessor_eq_assist:
   303   assumes "iso_tuple_update_accessor_eq_assist f g b u b' v"
   304   shows "iso_tuple_update_accessor_eq_assist (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)
   305     (iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v"
   306 proof -
   307   from assms have "f id = id"
   308     by (auto simp add: iso_tuple_update_accessor_eq_assist_def intro: iso_tuple_update_accessor_cong_assist_id)
   309   with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
   310     iso_tuple_snd_update_def iso_tuple_snd_def iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
   311 qed
   312 
   313 lemma iso_tuple_cons_conj_eqI:
   314   "a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
   315     iso_tuple_cons isom a b = iso_tuple_cons isom c d \<and> P \<longleftrightarrow> Q"
   316   by (clarsimp simp: iso_tuple_cons_def simps)
   317 
   318 lemmas intros =
   319     iso_tuple_access_update_fst_fst
   320     iso_tuple_access_update_snd_snd
   321     iso_tuple_access_update_fst_snd
   322     iso_tuple_access_update_snd_fst
   323     iso_tuple_update_swap_fst_fst
   324     iso_tuple_update_swap_snd_snd
   325     iso_tuple_update_swap_fst_snd
   326     iso_tuple_update_swap_snd_fst
   327     iso_tuple_update_compose_fst_fst
   328     iso_tuple_update_compose_snd_snd
   329     iso_tuple_surjective_proof_assist_step
   330     iso_tuple_fst_update_accessor_eq_assist
   331     iso_tuple_snd_update_accessor_eq_assist
   332     iso_tuple_fst_update_accessor_cong_assist
   333     iso_tuple_snd_update_accessor_cong_assist
   334     iso_tuple_cons_conj_eqI
   335 
   336 end
   337 
   338 lemma isomorphic_tuple_intro:
   339   fixes repr abst
   340   assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
   341      and abst_inv: "\<And>z. repr (abst z) = z"
   342   assumes v: "v \<equiv> Tuple_Isomorphism repr abst"
   343   shows "isomorphic_tuple v"
   344 proof
   345   have "\<And>x. repr (abst (repr x)) = repr x"
   346     by (simp add: abst_inv)
   347   then show "\<And>x. Record.abst v (Record.repr v x) = x"
   348     by (simp add: v repr_inj)
   349   show P: "\<And>y. Record.repr v (Record.abst v y) = y"
   350     by (simp add: v) (fact abst_inv)
   351 qed
   352 
   353 definition
   354   "tuple_iso_tuple \<equiv> Tuple_Isomorphism id id"
   355 
   356 lemma tuple_iso_tuple:
   357   "isomorphic_tuple tuple_iso_tuple"
   358   by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def)
   359 
   360 lemma refl_conj_eq:
   361   "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   362   by simp
   363 
   364 lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
   365   by simp
   366 
   367 lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   368   by simp
   369 
   370 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
   371   by simp
   372 
   373 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" 
   374   by (simp add: comp_def)
   375 
   376 lemma o_eq_dest_lhs:
   377   "a o b = c \<Longrightarrow> a (b v) = c v"
   378   by clarsimp
   379 
   380 lemma o_eq_id_dest:
   381   "a o b = id o c \<Longrightarrow> a (b v) = c v"
   382   by clarsimp
   383 
   384 
   385 subsection {* Concrete record syntax *}
   386 
   387 nonterminals
   388   ident field_type field_types field fields update updates
   389 syntax
   390   "_constify"           :: "id => ident"                        ("_")
   391   "_constify"           :: "longid => ident"                    ("_")
   392 
   393   "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
   394   ""                    :: "field_type => field_types"          ("_")
   395   "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
   396   "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
   397   "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
   398 
   399   "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
   400   ""                    :: "field => fields"                    ("_")
   401   "_fields"             :: "[field, fields] => fields"          ("_,/ _")
   402   "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
   403   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
   404 
   405   "_update_name"        :: idt
   406   "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
   407   ""                    :: "update => updates"                  ("_")
   408   "_updates"            :: "[update, updates] => updates"       ("_,/ _")
   409   "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
   410 
   411 syntax (xsymbols)
   412   "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
   413   "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
   414   "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
   415   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   416   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
   417 
   418 
   419 subsection {* Record package *}
   420 
   421 use "Tools/record.ML"
   422 setup Record.setup
   423 
   424 hide (open) const Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   425   iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
   426   iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
   427   iso_tuple_update_accessor_eq_assist tuple_iso_tuple
   428 
   429 end