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