src/HOL/Record.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 48891 c0eafbd55de3
child 51112 da97167e03f7
permissions -rw-r--r--
introduce order topology
     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 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   analogous 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 analogous
    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 =
    83   Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
    84 
    85 primrec
    86   repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where
    87   "repr (Tuple_Isomorphism r a) = r"
    88 
    89 primrec
    90   abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
    91   "abst (Tuple_Isomorphism r a) = a"
    92 
    93 definition
    94   iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
    95   "iso_tuple_fst isom = fst \<circ> repr isom"
    96 
    97 definition
    98   iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
    99   "iso_tuple_snd isom = snd \<circ> repr isom"
   100 
   101 definition
   102   iso_tuple_fst_update ::
   103     "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
   104   "iso_tuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
   105 
   106 definition
   107   iso_tuple_snd_update ::
   108     "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
   109   "iso_tuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
   110 
   111 definition
   112   iso_tuple_cons ::
   113     "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
   114   "iso_tuple_cons isom = curry (abst isom)"
   115 
   116 
   117 subsection {* Logical infrastructure for records *}
   118 
   119 definition
   120   iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   121   "iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
   122 
   123 definition
   124   iso_tuple_update_accessor_cong_assist ::
   125     "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   126   "iso_tuple_update_accessor_cong_assist upd ac \<longleftrightarrow>
   127      (\<forall>f v. upd (\<lambda>x. f (ac v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
   128 
   129 definition
   130   iso_tuple_update_accessor_eq_assist ::
   131     "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
   132   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<longleftrightarrow>
   133      upd f v = v' \<and> ac v = x \<and> iso_tuple_update_accessor_cong_assist upd ac"
   134 
   135 lemma update_accessor_congruence_foldE:
   136   assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
   137     and r: "r = r'" and v: "ac r' = v'"
   138     and f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
   139   shows "upd f r = upd f' r'"
   140   using uac r v [symmetric]
   141   apply (subgoal_tac "upd (\<lambda>x. f (ac r')) r' = upd (\<lambda>x. f' (ac r')) r'")
   142    apply (simp add: iso_tuple_update_accessor_cong_assist_def)
   143   apply (simp add: f)
   144   done
   145 
   146 lemma update_accessor_congruence_unfoldE:
   147   "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
   148     r = r' \<Longrightarrow> ac r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v) \<Longrightarrow>
   149     upd f r = upd f' r'"
   150   apply (erule(2) update_accessor_congruence_foldE)
   151   apply simp
   152   done
   153 
   154 lemma iso_tuple_update_accessor_cong_assist_id:
   155   "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow> upd id = id"
   156   by rule (simp add: iso_tuple_update_accessor_cong_assist_def)
   157 
   158 lemma update_accessor_noopE:
   159   assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
   160     and ac: "f (ac x) = ac x"
   161   shows "upd f x = x"
   162   using uac
   163   by (simp add: ac iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
   164     cong: update_accessor_congruence_unfoldE [OF uac])
   165 
   166 lemma update_accessor_noop_compE:
   167   assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
   168     and ac: "f (ac x) = ac x"
   169   shows "upd (g \<circ> f) x = upd g x"
   170   by (simp add: ac cong: update_accessor_congruence_unfoldE[OF uac])
   171 
   172 lemma update_accessor_cong_assist_idI:
   173   "iso_tuple_update_accessor_cong_assist id id"
   174   by (simp add: iso_tuple_update_accessor_cong_assist_def)
   175 
   176 lemma update_accessor_cong_assist_triv:
   177   "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
   178     iso_tuple_update_accessor_cong_assist upd ac"
   179   by assumption
   180 
   181 lemma update_accessor_accessor_eqE:
   182   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> ac v = x"
   183   by (simp add: iso_tuple_update_accessor_eq_assist_def)
   184 
   185 lemma update_accessor_updator_eqE:
   186   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> upd f v = v'"
   187   by (simp add: iso_tuple_update_accessor_eq_assist_def)
   188 
   189 lemma iso_tuple_update_accessor_eq_assist_idI:
   190   "v' = f v \<Longrightarrow> iso_tuple_update_accessor_eq_assist id id v f v' v"
   191   by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
   192 
   193 lemma iso_tuple_update_accessor_eq_assist_triv:
   194   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
   195     iso_tuple_update_accessor_eq_assist upd ac v f v' x"
   196   by assumption
   197 
   198 lemma iso_tuple_update_accessor_cong_from_eq:
   199   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
   200     iso_tuple_update_accessor_cong_assist upd ac"
   201   by (simp add: iso_tuple_update_accessor_eq_assist_def)
   202 
   203 lemma iso_tuple_surjective_proof_assistI:
   204   "f x = y \<Longrightarrow> iso_tuple_surjective_proof_assist x y f"
   205   by (simp add: iso_tuple_surjective_proof_assist_def)
   206 
   207 lemma iso_tuple_surjective_proof_assist_idE:
   208   "iso_tuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   209   by (simp add: iso_tuple_surjective_proof_assist_def)
   210 
   211 locale isomorphic_tuple =
   212   fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
   213   assumes repr_inv: "\<And>x. abst isom (repr isom x) = x"
   214     and abst_inv: "\<And>y. repr isom (abst isom y) = y"
   215 begin
   216 
   217 lemma repr_inj: "repr isom x = repr isom y \<longleftrightarrow> x = y"
   218   by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"]
   219     simp add: repr_inv)
   220 
   221 lemma abst_inj: "abst isom x = abst isom y \<longleftrightarrow> x = y"
   222   by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"]
   223     simp add: abst_inv)
   224 
   225 lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj
   226 
   227 lemma iso_tuple_access_update_fst_fst:
   228   "f o h g = j o f \<Longrightarrow>
   229     (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g =
   230       j o (f o iso_tuple_fst isom)"
   231   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps
   232     fun_eq_iff)
   233 
   234 lemma iso_tuple_access_update_snd_snd:
   235   "f o h g = j o f \<Longrightarrow>
   236     (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g =
   237       j o (f o iso_tuple_snd isom)"
   238   by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps
   239     fun_eq_iff)
   240 
   241 lemma iso_tuple_access_update_fst_snd:
   242   "(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g =
   243     id o (f o iso_tuple_fst isom)"
   244   by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps
   245     fun_eq_iff)
   246 
   247 lemma iso_tuple_access_update_snd_fst:
   248   "(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g =
   249     id o (f o iso_tuple_snd isom)"
   250   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps
   251     fun_eq_iff)
   252 
   253 lemma iso_tuple_update_swap_fst_fst:
   254   "h f o j g = j g o h f \<Longrightarrow>
   255     (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g =
   256       (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f"
   257   by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)
   258 
   259 lemma iso_tuple_update_swap_snd_snd:
   260   "h f o j g = j g o h f \<Longrightarrow>
   261     (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g =
   262       (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f"
   263   by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)
   264 
   265 lemma iso_tuple_update_swap_fst_snd:
   266   "(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g =
   267     (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f"
   268   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def
   269     simps fun_eq_iff)
   270 
   271 lemma iso_tuple_update_swap_snd_fst:
   272   "(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g =
   273     (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f"
   274   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps
   275     fun_eq_iff)
   276 
   277 lemma iso_tuple_update_compose_fst_fst:
   278   "h f o j g = k (f o g) \<Longrightarrow>
   279     (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g =
   280       (iso_tuple_fst_update isom o k) (f o g)"
   281   by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)
   282 
   283 lemma iso_tuple_update_compose_snd_snd:
   284   "h f o j g = k (f o g) \<Longrightarrow>
   285     (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g =
   286       (iso_tuple_snd_update isom o k) (f o g)"
   287   by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)
   288 
   289 lemma iso_tuple_surjective_proof_assist_step:
   290   "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \<Longrightarrow>
   291     iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f) \<Longrightarrow>
   292     iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f"
   293   by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps
   294     iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def)
   295 
   296 lemma iso_tuple_fst_update_accessor_cong_assist:
   297   assumes "iso_tuple_update_accessor_cong_assist f g"
   298   shows "iso_tuple_update_accessor_cong_assist
   299     (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)"
   300 proof -
   301   from assms have "f id = id"
   302     by (rule iso_tuple_update_accessor_cong_assist_id)
   303   with assms show ?thesis
   304     by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
   305       iso_tuple_fst_update_def iso_tuple_fst_def)
   306 qed
   307 
   308 lemma iso_tuple_snd_update_accessor_cong_assist:
   309   assumes "iso_tuple_update_accessor_cong_assist f g"
   310   shows "iso_tuple_update_accessor_cong_assist
   311     (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)"
   312 proof -
   313   from assms have "f id = id"
   314     by (rule iso_tuple_update_accessor_cong_assist_id)
   315   with assms show ?thesis
   316     by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
   317       iso_tuple_snd_update_def iso_tuple_snd_def)
   318 qed
   319 
   320 lemma iso_tuple_fst_update_accessor_eq_assist:
   321   assumes "iso_tuple_update_accessor_eq_assist f g a u a' v"
   322   shows "iso_tuple_update_accessor_eq_assist
   323     (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)
   324     (iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v"
   325 proof -
   326   from assms have "f id = id"
   327     by (auto simp add: iso_tuple_update_accessor_eq_assist_def
   328       intro: iso_tuple_update_accessor_cong_assist_id)
   329   with assms show ?thesis
   330     by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
   331       iso_tuple_fst_update_def iso_tuple_fst_def
   332       iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
   333 qed
   334 
   335 lemma iso_tuple_snd_update_accessor_eq_assist:
   336   assumes "iso_tuple_update_accessor_eq_assist f g b u b' v"
   337   shows "iso_tuple_update_accessor_eq_assist
   338     (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)
   339     (iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v"
   340 proof -
   341   from assms have "f id = id"
   342     by (auto simp add: iso_tuple_update_accessor_eq_assist_def
   343       intro: iso_tuple_update_accessor_cong_assist_id)
   344   with assms show ?thesis
   345     by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
   346       iso_tuple_snd_update_def iso_tuple_snd_def
   347       iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
   348 qed
   349 
   350 lemma iso_tuple_cons_conj_eqI:
   351   "a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
   352     iso_tuple_cons isom a b = iso_tuple_cons isom c d \<and> P \<longleftrightarrow> Q"
   353   by (clarsimp simp: iso_tuple_cons_def simps)
   354 
   355 lemmas intros =
   356   iso_tuple_access_update_fst_fst
   357   iso_tuple_access_update_snd_snd
   358   iso_tuple_access_update_fst_snd
   359   iso_tuple_access_update_snd_fst
   360   iso_tuple_update_swap_fst_fst
   361   iso_tuple_update_swap_snd_snd
   362   iso_tuple_update_swap_fst_snd
   363   iso_tuple_update_swap_snd_fst
   364   iso_tuple_update_compose_fst_fst
   365   iso_tuple_update_compose_snd_snd
   366   iso_tuple_surjective_proof_assist_step
   367   iso_tuple_fst_update_accessor_eq_assist
   368   iso_tuple_snd_update_accessor_eq_assist
   369   iso_tuple_fst_update_accessor_cong_assist
   370   iso_tuple_snd_update_accessor_cong_assist
   371   iso_tuple_cons_conj_eqI
   372 
   373 end
   374 
   375 lemma isomorphic_tuple_intro:
   376   fixes repr abst
   377   assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
   378     and abst_inv: "\<And>z. repr (abst z) = z"
   379     and v: "v \<equiv> Tuple_Isomorphism repr abst"
   380   shows "isomorphic_tuple v"
   381 proof
   382   fix x have "repr (abst (repr x)) = repr x"
   383     by (simp add: abst_inv)
   384   then show "Record.abst v (Record.repr v x) = x"
   385     by (simp add: v repr_inj)
   386 next
   387   fix y
   388   show "Record.repr v (Record.abst v y) = y"
   389     by (simp add: v) (fact abst_inv)
   390 qed
   391 
   392 definition
   393   "tuple_iso_tuple \<equiv> Tuple_Isomorphism id id"
   394 
   395 lemma tuple_iso_tuple:
   396   "isomorphic_tuple tuple_iso_tuple"
   397   by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def)
   398 
   399 lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   400   by simp
   401 
   402 lemma iso_tuple_UNIV_I [no_atp]: "x \<in> UNIV \<equiv> True"
   403   by simp
   404 
   405 lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   406   by simp
   407 
   408 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
   409   by simp
   410 
   411 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
   412   by (simp add: comp_def)
   413 
   414 lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
   415   by clarsimp
   416 
   417 lemma o_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"
   418   by clarsimp
   419 
   420 
   421 subsection {* Concrete record syntax *}
   422 
   423 nonterminal
   424   ident and
   425   field_type and
   426   field_types and
   427   field and
   428   fields and
   429   field_update and
   430   field_updates
   431 
   432 syntax
   433   "_constify"           :: "id => ident"                        ("_")
   434   "_constify"           :: "longid => ident"                    ("_")
   435 
   436   "_field_type"         :: "ident => type => field_type"        ("(2_ ::/ _)")
   437   ""                    :: "field_type => field_types"          ("_")
   438   "_field_types"        :: "field_type => field_types => field_types"    ("_,/ _")
   439   "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
   440   "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
   441 
   442   "_field"              :: "ident => 'a => field"               ("(2_ =/ _)")
   443   ""                    :: "field => fields"                    ("_")
   444   "_fields"             :: "field => fields => fields"          ("_,/ _")
   445   "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
   446   "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
   447 
   448   "_field_update"       :: "ident => 'a => field_update"        ("(2_ :=/ _)")
   449   ""                    :: "field_update => field_updates"      ("_")
   450   "_field_updates"      :: "field_update => field_updates => field_updates"  ("_,/ _")
   451   "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
   452 
   453 syntax (xsymbols)
   454   "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
   455   "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
   456   "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
   457   "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   458   "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
   459 
   460 
   461 subsection {* Record package *}
   462 
   463 ML_file "Tools/record.ML" setup Record.setup
   464 
   465 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   466   iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
   467   iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
   468   iso_tuple_update_accessor_eq_assist tuple_iso_tuple
   469 
   470 end