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 9section \<open>Extensible records with structural subtyping\<close> 10 11theory Record 12imports Quickcheck_Exhaustive 13keywords 14 "record" :: thy_defn and 15 "print_record" :: diag 16begin 17 18subsection \<open>Introduction\<close> 19 20text \<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 79subsection \<open>Operators and lemmas for types isomorphic to tuples\<close> 80 81datatype (dead 'a, dead 'b, dead 'c) tuple_isomorphism = 82 Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a" 83 84primrec 85 repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where 86 "repr (Tuple_Isomorphism r a) = r" 87 88primrec 89 abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where 90 "abst (Tuple_Isomorphism r a) = a" 91 92definition 93 iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where 94 "iso_tuple_fst isom = fst \<circ> repr isom" 95 96definition 97 iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where 98 "iso_tuple_snd isom = snd \<circ> repr isom" 99 100definition 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 105definition 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 110definition 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 116subsection \<open>Logical infrastructure for records\<close> 117 118definition 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 122definition 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 128definition 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 134lemma 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 145lemma 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 153lemma 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 157lemma 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 165lemma 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 171lemma 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 175lemma 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 180lemma 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 184lemma 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 188lemma 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 192lemma 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 197lemma 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 202lemma 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 206lemma 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 210locale 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" 214begin 215 216lemma 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 220lemma 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 224lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj 225 226lemma 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 233lemma 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 240lemma 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 246lemma 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 252lemma 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 258lemma 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 264lemma 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 270lemma 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 276lemma 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 282lemma 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 288lemma 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 295lemma 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)" 299proof - 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) 305qed 306 307lemma 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)" 311proof - 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) 317qed 318 319lemma 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" 324proof - 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) 332qed 333 334lemma 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" 339proof - 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) 347qed 348 349lemma 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 354lemmas 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 372end 373 374lemma 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" 380proof 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) 385next 386 fix y 387 show "Record.repr v (Record.abst v y) = y" 388 by (simp add: v) (fact abst_inv) 389qed 390 391definition 392 "tuple_iso_tuple \<equiv> Tuple_Isomorphism id id" 393 394lemma tuple_iso_tuple: 395 "isomorphic_tuple tuple_iso_tuple" 396 by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def) 397 398lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R" 399 by simp 400 401lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True" 402 by simp 403 404lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 405 by simp 406 407lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s" 408 by simp 409 410lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" 411 by (simp add: comp_def) 412 413 414subsection \<open>Concrete record syntax\<close> 415 416nonterminal 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 425syntax 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 446syntax (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 454subsection \<open>Record package\<close> 455 456ML_file \<open>Tools/record.ML\<close> 457 458hide_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 463end 464