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