src/HOL/Record.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 47893 4cf901b1089a
child 48891 c0eafbd55de3
permissions -rw-r--r--
tuned proofs;
     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 Plain Quickcheck_Narrowing
    13 keywords "record" :: thy_decl
    14 uses ("Tools/record.ML")
    15 begin
    16 
    17 subsection {* Introduction *}
    18 
    19 text {*
    20   Records are isomorphic to compound tuple types. To implement
    21   efficient records, we make this isomorphism explicit. Consider the
    22   record access/update simplification @{text "alpha (beta_update f
    23   rec) = alpha rec"} for distinct fields alpha and beta of some record
    24   rec with n fields. There are @{text "n ^ 2"} such theorems, which
    25   prohibits storage of all of them for large n. The rules can be
    26   proved on the fly by case decomposition and simplification in O(n)
    27   time. By creating O(n) isomorphic-tuple types while defining the
    28   record, however, we can prove the access/update simplification in
    29   @{text "O(log(n)^2)"} time.
    30 
    31   The O(n) cost of case decomposition is not because O(n) steps are
    32   taken, but rather because the resulting rule must contain O(n) new
    33   variables and an O(n) size concrete record construction. To sidestep
    34   this cost, we would like to avoid case decomposition in proving
    35   access/update theorems.
    36 
    37   Record types are defined as isomorphic to tuple types. For instance,
    38   a record type with fields @{text "'a"}, @{text "'b"}, @{text "'c"}
    39   and @{text "'d"} might be introduced as isomorphic to @{text "'a \<times>
    40   ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to @{text "('a \<times>
    41   'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to the
    42   underlying type then using O(log(n)) fst or snd operations.
    43   Updators can be defined similarly, if we introduce a @{text
    44   "fst_update"} and @{text "snd_update"} function. Furthermore, we can
    45   prove the access/update theorem in O(log(n)) steps by using simple
    46   rewrites on fst, snd, @{text "fst_update"} and @{text "snd_update"}.
    47 
    48   The catch is that, although O(log(n)) steps were taken, the
    49   underlying type we converted to is a tuple tree of size
    50   O(n). Processing this term type wastes performance. We avoid this
    51   for large n by taking each subtree of size K and defining a new type
    52   isomorphic to that tuple subtree. A record can now be defined as
    53   isomorphic to a tuple tree of these O(n/K) new types, or, if @{text
    54   "n > K*K"}, we can repeat the process, until the record can be
    55   defined in terms of a tuple tree of complexity less than the
    56   constant K.
    57 
    58   If we prove the access/update theorem on this type with the
    59   analogous steps to the tuple tree, we consume @{text "O(log(n)^2)"}
    60   time as the intermediate terms are @{text "O(log(n))"} in size and
    61   the types needed have size bounded by K.  To enable this analogous
    62   traversal, we define the functions seen below: @{text
    63   "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"}
    64   and @{text "iso_tuple_snd_update"}. These functions generalise tuple
    65   operations by taking a parameter that encapsulates a tuple
    66   isomorphism.  The rewrites needed on these functions now need an
    67   additional assumption which is that the isomorphism works.
    68 
    69   These rewrites are typically used in a structured way. They are here
    70   presented as the introduction rule @{text "isomorphic_tuple.intros"}
    71   rather than as a rewrite rule set. The introduction form is an
    72   optimisation, as net matching can be performed at one term location
    73   for each step rather than the simplifier searching the term for
    74   possible pattern matches. The rule set is used as it is viewed
    75   outside the locale, with the locale assumption (that the isomorphism
    76   is valid) left as a rule assumption. All rules are structured to aid
    77   net matching, using either a point-free form or an encapsulating
    78   predicate.
    79 *}
    80 
    81 subsection {* Operators and lemmas for types isomorphic to tuples *}
    82 
    83 datatype ('a, 'b, 'c) tuple_isomorphism =
    84   Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
    85 
    86 primrec
    87   repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where
    88   "repr (Tuple_Isomorphism r a) = r"
    89 
    90 primrec
    91   abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
    92   "abst (Tuple_Isomorphism r a) = a"
    93 
    94 definition
    95   iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
    96   "iso_tuple_fst isom = fst \<circ> repr isom"
    97 
    98 definition
    99   iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
   100   "iso_tuple_snd isom = snd \<circ> repr isom"
   101 
   102 definition
   103   iso_tuple_fst_update ::
   104     "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
   105   "iso_tuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
   106 
   107 definition
   108   iso_tuple_snd_update ::
   109     "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
   110   "iso_tuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
   111 
   112 definition
   113   iso_tuple_cons ::
   114     "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
   115   "iso_tuple_cons isom = curry (abst isom)"
   116 
   117 
   118 subsection {* Logical infrastructure for records *}
   119 
   120 definition
   121   iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   122   "iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
   123 
   124 definition
   125   iso_tuple_update_accessor_cong_assist ::
   126     "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   127   "iso_tuple_update_accessor_cong_assist upd ac \<longleftrightarrow>
   128      (\<forall>f v. upd (\<lambda>x. f (ac v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
   129 
   130 definition
   131   iso_tuple_update_accessor_eq_assist ::
   132     "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
   133   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<longleftrightarrow>
   134      upd f v = v' \<and> ac v = x \<and> iso_tuple_update_accessor_cong_assist upd ac"
   135 
   136 lemma update_accessor_congruence_foldE:
   137   assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
   138     and r: "r = r'" and v: "ac r' = v'"
   139     and f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
   140   shows "upd f r = upd f' r'"
   141   using uac r v [symmetric]
   142   apply (subgoal_tac "upd (\<lambda>x. f (ac r')) r' = upd (\<lambda>x. f' (ac r')) r'")
   143    apply (simp add: iso_tuple_update_accessor_cong_assist_def)
   144   apply (simp add: f)
   145   done
   146 
   147 lemma update_accessor_congruence_unfoldE:
   148   "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
   149     r = r' \<Longrightarrow> ac r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v) \<Longrightarrow>
   150     upd f r = upd f' r'"
   151   apply (erule(2) update_accessor_congruence_foldE)
   152   apply simp
   153   done
   154 
   155 lemma iso_tuple_update_accessor_cong_assist_id:
   156   "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow> upd id = id"
   157   by rule (simp add: iso_tuple_update_accessor_cong_assist_def)
   158 
   159 lemma update_accessor_noopE:
   160   assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
   161     and ac: "f (ac x) = ac x"
   162   shows "upd f x = x"
   163   using uac
   164   by (simp add: ac iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
   165     cong: update_accessor_congruence_unfoldE [OF uac])
   166 
   167 lemma update_accessor_noop_compE:
   168   assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
   169     and ac: "f (ac x) = ac x"
   170   shows "upd (g \<circ> f) x = upd g x"
   171   by (simp add: ac cong: update_accessor_congruence_unfoldE[OF uac])
   172 
   173 lemma update_accessor_cong_assist_idI:
   174   "iso_tuple_update_accessor_cong_assist id id"
   175   by (simp add: iso_tuple_update_accessor_cong_assist_def)
   176 
   177 lemma update_accessor_cong_assist_triv:
   178   "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
   179     iso_tuple_update_accessor_cong_assist upd ac"
   180   by assumption
   181 
   182 lemma update_accessor_accessor_eqE:
   183   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> ac v = x"
   184   by (simp add: iso_tuple_update_accessor_eq_assist_def)
   185 
   186 lemma update_accessor_updator_eqE:
   187   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> upd f v = v'"
   188   by (simp add: iso_tuple_update_accessor_eq_assist_def)
   189 
   190 lemma iso_tuple_update_accessor_eq_assist_idI:
   191   "v' = f v \<Longrightarrow> iso_tuple_update_accessor_eq_assist id id v f v' v"
   192   by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
   193 
   194 lemma iso_tuple_update_accessor_eq_assist_triv:
   195   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
   196     iso_tuple_update_accessor_eq_assist upd ac v f v' x"
   197   by assumption
   198 
   199 lemma iso_tuple_update_accessor_cong_from_eq:
   200   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
   201     iso_tuple_update_accessor_cong_assist upd ac"
   202   by (simp add: iso_tuple_update_accessor_eq_assist_def)
   203 
   204 lemma iso_tuple_surjective_proof_assistI:
   205   "f x = y \<Longrightarrow> iso_tuple_surjective_proof_assist x y f"
   206   by (simp add: iso_tuple_surjective_proof_assist_def)
   207 
   208 lemma iso_tuple_surjective_proof_assist_idE:
   209   "iso_tuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   210   by (simp add: iso_tuple_surjective_proof_assist_def)
   211 
   212 locale isomorphic_tuple =
   213   fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
   214   assumes repr_inv: "\<And>x. abst isom (repr isom x) = x"
   215     and abst_inv: "\<And>y. repr isom (abst isom y) = y"
   216 begin
   217 
   218 lemma repr_inj: "repr isom x = repr isom y \<longleftrightarrow> x = y"
   219   by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"]
   220     simp add: repr_inv)
   221 
   222 lemma abst_inj: "abst isom x = abst isom y \<longleftrightarrow> x = y"
   223   by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"]
   224     simp add: abst_inv)
   225 
   226 lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj
   227 
   228 lemma iso_tuple_access_update_fst_fst:
   229   "f o h g = j o f \<Longrightarrow>
   230     (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g =
   231       j o (f o iso_tuple_fst isom)"
   232   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps
   233     fun_eq_iff)
   234 
   235 lemma iso_tuple_access_update_snd_snd:
   236   "f o h g = j o f \<Longrightarrow>
   237     (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g =
   238       j o (f o iso_tuple_snd isom)"
   239   by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps
   240     fun_eq_iff)
   241 
   242 lemma iso_tuple_access_update_fst_snd:
   243   "(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g =
   244     id o (f o iso_tuple_fst isom)"
   245   by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps
   246     fun_eq_iff)
   247 
   248 lemma iso_tuple_access_update_snd_fst:
   249   "(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g =
   250     id o (f o iso_tuple_snd isom)"
   251   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps
   252     fun_eq_iff)
   253 
   254 lemma iso_tuple_update_swap_fst_fst:
   255   "h f o j g = j g o h f \<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 j) g o (iso_tuple_fst_update isom o h) f"
   258   by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)
   259 
   260 lemma iso_tuple_update_swap_snd_snd:
   261   "h f o j g = j g o h f \<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 j) g o (iso_tuple_snd_update isom o h) f"
   264   by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)
   265 
   266 lemma iso_tuple_update_swap_fst_snd:
   267   "(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g =
   268     (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f"
   269   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def
   270     simps fun_eq_iff)
   271 
   272 lemma iso_tuple_update_swap_snd_fst:
   273   "(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g =
   274     (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f"
   275   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps
   276     fun_eq_iff)
   277 
   278 lemma iso_tuple_update_compose_fst_fst:
   279   "h f o j g = k (f o g) \<Longrightarrow>
   280     (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g =
   281       (iso_tuple_fst_update isom o k) (f o g)"
   282   by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)
   283 
   284 lemma iso_tuple_update_compose_snd_snd:
   285   "h f o j g = k (f o g) \<Longrightarrow>
   286     (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g =
   287       (iso_tuple_snd_update isom o k) (f o g)"
   288   by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)
   289 
   290 lemma iso_tuple_surjective_proof_assist_step:
   291   "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \<Longrightarrow>
   292     iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f) \<Longrightarrow>
   293     iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f"
   294   by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps
   295     iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def)
   296 
   297 lemma iso_tuple_fst_update_accessor_cong_assist:
   298   assumes "iso_tuple_update_accessor_cong_assist f g"
   299   shows "iso_tuple_update_accessor_cong_assist
   300     (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)"
   301 proof -
   302   from assms have "f id = id"
   303     by (rule iso_tuple_update_accessor_cong_assist_id)
   304   with assms show ?thesis
   305     by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
   306       iso_tuple_fst_update_def iso_tuple_fst_def)
   307 qed
   308 
   309 lemma iso_tuple_snd_update_accessor_cong_assist:
   310   assumes "iso_tuple_update_accessor_cong_assist f g"
   311   shows "iso_tuple_update_accessor_cong_assist
   312     (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)"
   313 proof -
   314   from assms have "f id = id"
   315     by (rule iso_tuple_update_accessor_cong_assist_id)
   316   with assms show ?thesis
   317     by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
   318       iso_tuple_snd_update_def iso_tuple_snd_def)
   319 qed
   320 
   321 lemma iso_tuple_fst_update_accessor_eq_assist:
   322   assumes "iso_tuple_update_accessor_eq_assist f g a u a' v"
   323   shows "iso_tuple_update_accessor_eq_assist
   324     (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)
   325     (iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v"
   326 proof -
   327   from assms have "f id = id"
   328     by (auto simp add: iso_tuple_update_accessor_eq_assist_def
   329       intro: iso_tuple_update_accessor_cong_assist_id)
   330   with assms show ?thesis
   331     by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
   332       iso_tuple_fst_update_def iso_tuple_fst_def
   333       iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
   334 qed
   335 
   336 lemma iso_tuple_snd_update_accessor_eq_assist:
   337   assumes "iso_tuple_update_accessor_eq_assist f g b u b' v"
   338   shows "iso_tuple_update_accessor_eq_assist
   339     (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)
   340     (iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v"
   341 proof -
   342   from assms have "f id = id"
   343     by (auto simp add: iso_tuple_update_accessor_eq_assist_def
   344       intro: iso_tuple_update_accessor_cong_assist_id)
   345   with assms show ?thesis
   346     by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
   347       iso_tuple_snd_update_def iso_tuple_snd_def
   348       iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
   349 qed
   350 
   351 lemma iso_tuple_cons_conj_eqI:
   352   "a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
   353     iso_tuple_cons isom a b = iso_tuple_cons isom c d \<and> P \<longleftrightarrow> Q"
   354   by (clarsimp simp: iso_tuple_cons_def simps)
   355 
   356 lemmas intros =
   357   iso_tuple_access_update_fst_fst
   358   iso_tuple_access_update_snd_snd
   359   iso_tuple_access_update_fst_snd
   360   iso_tuple_access_update_snd_fst
   361   iso_tuple_update_swap_fst_fst
   362   iso_tuple_update_swap_snd_snd
   363   iso_tuple_update_swap_fst_snd
   364   iso_tuple_update_swap_snd_fst
   365   iso_tuple_update_compose_fst_fst
   366   iso_tuple_update_compose_snd_snd
   367   iso_tuple_surjective_proof_assist_step
   368   iso_tuple_fst_update_accessor_eq_assist
   369   iso_tuple_snd_update_accessor_eq_assist
   370   iso_tuple_fst_update_accessor_cong_assist
   371   iso_tuple_snd_update_accessor_cong_assist
   372   iso_tuple_cons_conj_eqI
   373 
   374 end
   375 
   376 lemma isomorphic_tuple_intro:
   377   fixes repr abst
   378   assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
   379     and abst_inv: "\<And>z. repr (abst z) = z"
   380     and v: "v \<equiv> Tuple_Isomorphism repr abst"
   381   shows "isomorphic_tuple v"
   382 proof
   383   fix x have "repr (abst (repr x)) = repr x"
   384     by (simp add: abst_inv)
   385   then show "Record.abst v (Record.repr v x) = x"
   386     by (simp add: v repr_inj)
   387 next
   388   fix y
   389   show "Record.repr v (Record.abst v y) = y"
   390     by (simp add: v) (fact abst_inv)
   391 qed
   392 
   393 definition
   394   "tuple_iso_tuple \<equiv> Tuple_Isomorphism id id"
   395 
   396 lemma tuple_iso_tuple:
   397   "isomorphic_tuple tuple_iso_tuple"
   398   by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def)
   399 
   400 lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   401   by simp
   402 
   403 lemma iso_tuple_UNIV_I [no_atp]: "x \<in> UNIV \<equiv> True"
   404   by simp
   405 
   406 lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   407   by simp
   408 
   409 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
   410   by simp
   411 
   412 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
   413   by (simp add: comp_def)
   414 
   415 lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
   416   by clarsimp
   417 
   418 lemma o_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"
   419   by clarsimp
   420 
   421 
   422 subsection {* Concrete record syntax *}
   423 
   424 nonterminal
   425   ident and
   426   field_type and
   427   field_types and
   428   field and
   429   fields and
   430   field_update and
   431   field_updates
   432 
   433 syntax
   434   "_constify"           :: "id => ident"                        ("_")
   435   "_constify"           :: "longid => ident"                    ("_")
   436 
   437   "_field_type"         :: "ident => type => field_type"        ("(2_ ::/ _)")
   438   ""                    :: "field_type => field_types"          ("_")
   439   "_field_types"        :: "field_type => field_types => field_types"    ("_,/ _")
   440   "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
   441   "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
   442 
   443   "_field"              :: "ident => 'a => field"               ("(2_ =/ _)")
   444   ""                    :: "field => fields"                    ("_")
   445   "_fields"             :: "field => fields => fields"          ("_,/ _")
   446   "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
   447   "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
   448 
   449   "_field_update"       :: "ident => 'a => field_update"        ("(2_ :=/ _)")
   450   ""                    :: "field_update => field_updates"      ("_")
   451   "_field_updates"      :: "field_update => field_updates => field_updates"  ("_,/ _")
   452   "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
   453 
   454 syntax (xsymbols)
   455   "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
   456   "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
   457   "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
   458   "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   459   "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
   460 
   461 
   462 subsection {* Record package *}
   463 
   464 use "Tools/record.ML" setup Record.setup
   465 
   466 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   467   iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
   468   iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
   469   iso_tuple_update_accessor_eq_assist tuple_iso_tuple
   470 
   471 end