src/HOL/Record.thy
author haftmann
Fri Nov 27 08:41:10 2009 +0100 (2009-11-27)
changeset 33963 977b94b64905
parent 33595 7264824baf66
child 34151 8d57ce46b3f7
permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
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@22817
     9
header {* Extensible records with structural subtyping *}
wenzelm@22817
    10
nipkow@15131
    11
theory Record
haftmann@33595
    12
imports Datatype
tsewell@32744
    13
uses ("Tools/record.ML")
nipkow@15131
    14
begin
wenzelm@4870
    15
haftmann@33595
    16
subsection {* Introduction *}
haftmann@33595
    17
haftmann@33595
    18
text {*
haftmann@33595
    19
  Records are isomorphic to compound tuple types. To implement
haftmann@33595
    20
  efficient records, we make this isomorphism explicit. Consider the
haftmann@33595
    21
  record access/update simplification @{text "alpha (beta_update f
haftmann@33595
    22
  rec) = alpha rec"} for distinct fields alpha and beta of some record
haftmann@33595
    23
  rec with n fields. There are @{text "n ^ 2"} such theorems, which
haftmann@33595
    24
  prohibits storage of all of them for large n. The rules can be
haftmann@33595
    25
  proved on the fly by case decomposition and simplification in O(n)
haftmann@33595
    26
  time. By creating O(n) isomorphic-tuple types while defining the
haftmann@33595
    27
  record, however, we can prove the access/update simplification in
haftmann@33595
    28
  @{text "O(log(n)^2)"} time.
haftmann@33595
    29
haftmann@33595
    30
  The O(n) cost of case decomposition is not because O(n) steps are
haftmann@33595
    31
  taken, but rather because the resulting rule must contain O(n) new
haftmann@33595
    32
  variables and an O(n) size concrete record construction. To sidestep
haftmann@33595
    33
  this cost, we would like to avoid case decomposition in proving
haftmann@33595
    34
  access/update theorems.
haftmann@33595
    35
haftmann@33595
    36
  Record types are defined as isomorphic to tuple types. For instance,
haftmann@33595
    37
  a record type with fields @{text "'a"}, @{text "'b"}, @{text "'c"}
haftmann@33595
    38
  and @{text "'d"} might be introduced as isomorphic to @{text "'a \<times>
haftmann@33595
    39
  ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to @{text "('a \<times>
haftmann@33595
    40
  'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to the
haftmann@33595
    41
  underlying type then using O(log(n)) fst or snd operations.
haftmann@33595
    42
  Updators can be defined similarly, if we introduce a @{text
haftmann@33595
    43
  "fst_update"} and @{text "snd_update"} function. Furthermore, we can
haftmann@33595
    44
  prove the access/update theorem in O(log(n)) steps by using simple
haftmann@33595
    45
  rewrites on fst, snd, @{text "fst_update"} and @{text "snd_update"}.
haftmann@33595
    46
haftmann@33595
    47
  The catch is that, although O(log(n)) steps were taken, the
haftmann@33595
    48
  underlying type we converted to is a tuple tree of size
haftmann@33595
    49
  O(n). Processing this term type wastes performance. We avoid this
haftmann@33595
    50
  for large n by taking each subtree of size K and defining a new type
haftmann@33595
    51
  isomorphic to that tuple subtree. A record can now be defined as
haftmann@33595
    52
  isomorphic to a tuple tree of these O(n/K) new types, or, if @{text
haftmann@33595
    53
  "n > K*K"}, 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
haftmann@33595
    58
  analagous steps to the tuple tree, we consume @{text "O(log(n)^2)"}
haftmann@33595
    59
  time as the intermediate terms are @{text "O(log(n))"} in size and
haftmann@33595
    60
  the types needed have size bounded by K.  To enable this analagous
haftmann@33595
    61
  traversal, we define the functions seen below: @{text
haftmann@33595
    62
  "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"}
haftmann@33595
    63
  and @{text "istuple_snd_update"}. These functions generalise tuple
haftmann@33595
    64
  operations by taking a parameter that encapsulates a tuple
haftmann@33595
    65
  isomorphism.  The rewrites needed on these functions now need an
haftmann@33595
    66
  additional assumption which is that the isomorphism works.
haftmann@33595
    67
haftmann@33595
    68
  These rewrites are typically used in a structured way. They are here
haftmann@33595
    69
  presented as the introduction rule @{text "isomorphic_tuple.intros"}
haftmann@33595
    70
  rather than as a rewrite rule set. The introduction form is an
haftmann@33595
    71
  optimisation, as net matching can be performed at one term location
haftmann@33595
    72
  for each step rather than the simplifier searching the term for
haftmann@33595
    73
  possible pattern matches. The rule set is used as it is viewed
haftmann@33595
    74
  outside the locale, with the locale assumption (that the isomorphism
haftmann@33595
    75
  is valid) left as a rule assumption. All rules are structured to aid
haftmann@33595
    76
  net matching, using either a point-free form or an encapsulating
haftmann@33595
    77
  predicate.
haftmann@33595
    78
*}
haftmann@33595
    79
haftmann@33595
    80
subsection {* Operators and lemmas for types isomorphic to tuples *}
haftmann@33595
    81
haftmann@33595
    82
datatype ('a, 'b, 'c) tuple_isomorphism = TupleIsomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
haftmann@33595
    83
haftmann@33595
    84
primrec repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where
haftmann@33595
    85
  "repr (TupleIsomorphism r a) = r"
haftmann@33595
    86
haftmann@33595
    87
primrec abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
haftmann@33595
    88
  "abst (TupleIsomorphism r a) = a"
haftmann@33595
    89
haftmann@33595
    90
definition istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
haftmann@33595
    91
  "istuple_fst isom = fst \<circ> repr isom"
haftmann@33595
    92
haftmann@33595
    93
definition istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
haftmann@33595
    94
  "istuple_snd isom = snd \<circ> repr isom"
haftmann@33595
    95
haftmann@33595
    96
definition istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
haftmann@33595
    97
  "istuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
haftmann@33595
    98
haftmann@33595
    99
definition istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
haftmann@33595
   100
  "istuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
haftmann@33595
   101
haftmann@33595
   102
definition istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
haftmann@33595
   103
  "istuple_cons isom = curry (abst isom)"
haftmann@33595
   104
haftmann@33595
   105
haftmann@33595
   106
subsection {* Logical infrastructure for records *}
haftmann@33595
   107
haftmann@33595
   108
definition istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
haftmann@33595
   109
  "istuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
haftmann@33595
   110
haftmann@33595
   111
definition istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
haftmann@33595
   112
  "istuple_update_accessor_cong_assist upd acc \<longleftrightarrow> 
haftmann@33595
   113
     (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
haftmann@33595
   114
haftmann@33595
   115
definition istuple_update_accessor_eq_assist :: "(('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@33595
   116
  "istuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow>
haftmann@33595
   117
     upd f v = v' \<and> acc v = x \<and> istuple_update_accessor_cong_assist upd acc"
haftmann@33595
   118
haftmann@33595
   119
lemma update_accessor_congruence_foldE:
haftmann@33595
   120
  assumes uac: "istuple_update_accessor_cong_assist upd acc"
haftmann@33595
   121
  and       r: "r = r'" and v: "acc r' = v'"
haftmann@33595
   122
  and       f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
haftmann@33595
   123
  shows        "upd f r = upd f' r'"
haftmann@33595
   124
  using uac r v [symmetric]
haftmann@33595
   125
  apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
haftmann@33595
   126
   apply (simp add: istuple_update_accessor_cong_assist_def)
haftmann@33595
   127
  apply (simp add: f)
haftmann@33595
   128
  done
haftmann@33595
   129
haftmann@33595
   130
lemma update_accessor_congruence_unfoldE:
haftmann@33595
   131
  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> r = r' \<Longrightarrow> acc r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v)
haftmann@33595
   132
     \<Longrightarrow> upd f r = upd f' r'"
haftmann@33595
   133
  apply (erule(2) update_accessor_congruence_foldE)
haftmann@33595
   134
  apply simp
haftmann@33595
   135
  done
haftmann@33595
   136
haftmann@33595
   137
lemma istuple_update_accessor_cong_assist_id:
haftmann@33595
   138
  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
haftmann@33595
   139
  by rule (simp add: istuple_update_accessor_cong_assist_def)
haftmann@33595
   140
haftmann@33595
   141
lemma update_accessor_noopE:
haftmann@33595
   142
  assumes uac: "istuple_update_accessor_cong_assist upd acc"
haftmann@33595
   143
      and acc: "f (acc x) = acc x"
haftmann@33595
   144
  shows        "upd f x = x"
haftmann@33595
   145
using uac by (simp add: acc istuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
haftmann@33595
   146
  cong: update_accessor_congruence_unfoldE [OF uac])
haftmann@33595
   147
haftmann@33595
   148
lemma update_accessor_noop_compE:
haftmann@33595
   149
  assumes uac: "istuple_update_accessor_cong_assist upd acc"
haftmann@33595
   150
  assumes acc: "f (acc x) = acc x"
haftmann@33595
   151
  shows      "upd (g \<circ> f) x = upd g x"
haftmann@33595
   152
  by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
haftmann@33595
   153
haftmann@33595
   154
lemma update_accessor_cong_assist_idI:
haftmann@33595
   155
  "istuple_update_accessor_cong_assist id id"
haftmann@33595
   156
  by (simp add: istuple_update_accessor_cong_assist_def)
haftmann@33595
   157
haftmann@33595
   158
lemma update_accessor_cong_assist_triv:
haftmann@33595
   159
  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
haftmann@33595
   160
  by assumption
haftmann@33595
   161
haftmann@33595
   162
lemma update_accessor_accessor_eqE:
haftmann@33595
   163
  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> acc v = x"
haftmann@33595
   164
  by (simp add: istuple_update_accessor_eq_assist_def)
haftmann@33595
   165
haftmann@33595
   166
lemma update_accessor_updator_eqE:
haftmann@33595
   167
  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> upd f v = v'"
haftmann@33595
   168
  by (simp add: istuple_update_accessor_eq_assist_def)
haftmann@33595
   169
haftmann@33595
   170
lemma istuple_update_accessor_eq_assist_idI:
haftmann@33595
   171
  "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
haftmann@33595
   172
  by (simp add: istuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
haftmann@33595
   173
haftmann@33595
   174
lemma istuple_update_accessor_eq_assist_triv:
haftmann@33595
   175
  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
haftmann@33595
   176
  by assumption
haftmann@33595
   177
haftmann@33595
   178
lemma istuple_update_accessor_cong_from_eq:
haftmann@33595
   179
  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
haftmann@33595
   180
  by (simp add: istuple_update_accessor_eq_assist_def)
haftmann@33595
   181
haftmann@33595
   182
lemma o_eq_dest:
haftmann@33595
   183
  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
haftmann@33595
   184
  apply (clarsimp simp: o_def)
haftmann@33595
   185
  apply (erule fun_cong)
haftmann@33595
   186
  done
haftmann@33595
   187
haftmann@33595
   188
lemma o_eq_elim:
haftmann@33595
   189
  "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
haftmann@33595
   190
  apply (erule meta_mp)
haftmann@33595
   191
  apply (erule o_eq_dest)
haftmann@33595
   192
  done
haftmann@33595
   193
haftmann@33595
   194
lemma istuple_surjective_proof_assistI:
haftmann@33595
   195
  "f x = y \<Longrightarrow> istuple_surjective_proof_assist x y f"
haftmann@33595
   196
  by (simp add: istuple_surjective_proof_assist_def)
haftmann@33595
   197
haftmann@33595
   198
lemma istuple_surjective_proof_assist_idE:
haftmann@33595
   199
  "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
haftmann@33595
   200
  by (simp add: istuple_surjective_proof_assist_def)
haftmann@33595
   201
haftmann@33595
   202
locale isomorphic_tuple =
haftmann@33595
   203
  fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
haftmann@33595
   204
    and repr and abst
haftmann@33595
   205
  defines "repr \<equiv> Record.repr isom"
haftmann@33595
   206
  defines "abst \<equiv> Record.abst isom"
haftmann@33595
   207
  assumes repr_inv: "\<And>x. abst (repr x) = x"
haftmann@33595
   208
  assumes abst_inv: "\<And>y. repr (abst y) = y"
haftmann@33595
   209
begin
haftmann@33595
   210
haftmann@33595
   211
lemma repr_inj:
haftmann@33595
   212
  "repr x = repr y \<longleftrightarrow> x = y"
haftmann@33595
   213
  apply (rule iffI, simp_all)
haftmann@33595
   214
  apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
haftmann@33595
   215
  done
haftmann@33595
   216
haftmann@33595
   217
lemma abst_inj:
haftmann@33595
   218
  "abst x = abst y \<longleftrightarrow> x = y"
haftmann@33595
   219
  apply (rule iffI, simp_all)
haftmann@33595
   220
  apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
haftmann@33595
   221
  done
haftmann@33595
   222
haftmann@33595
   223
lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj repr_def [symmetric] abst_def [symmetric]
haftmann@33595
   224
haftmann@33595
   225
lemma istuple_access_update_fst_fst:
haftmann@33595
   226
  "f o h g = j o f \<Longrightarrow>
haftmann@33595
   227
    (f o istuple_fst isom) o (istuple_fst_update isom o h) g
haftmann@33595
   228
          = j o (f o istuple_fst isom)"
haftmann@33595
   229
  by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
haftmann@33595
   230
             intro!: ext elim!: o_eq_elim)
haftmann@33595
   231
haftmann@33595
   232
lemma istuple_access_update_snd_snd:
haftmann@33595
   233
  "f o h g = j o f \<Longrightarrow>
haftmann@33595
   234
    (f o istuple_snd isom) o (istuple_snd_update isom o h) g
haftmann@33595
   235
          = j o (f o istuple_snd isom)"
haftmann@33595
   236
  by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
haftmann@33595
   237
             intro!: ext elim!: o_eq_elim)
haftmann@33595
   238
haftmann@33595
   239
lemma istuple_access_update_fst_snd:
haftmann@33595
   240
  "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
haftmann@33595
   241
          = id o (f o istuple_fst isom)"
haftmann@33595
   242
  by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
haftmann@33595
   243
             intro!: ext elim!: o_eq_elim)
haftmann@33595
   244
haftmann@33595
   245
lemma istuple_access_update_snd_fst:
haftmann@33595
   246
  "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
haftmann@33595
   247
          = id o (f o istuple_snd isom)"
haftmann@33595
   248
  by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
haftmann@33595
   249
             intro!: ext elim!: o_eq_elim)
haftmann@33595
   250
haftmann@33595
   251
lemma istuple_update_swap_fst_fst:
haftmann@33595
   252
  "h f o j g = j g o h f \<Longrightarrow>
haftmann@33595
   253
    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
haftmann@33595
   254
          = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
haftmann@33595
   255
  by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
haftmann@33595
   256
haftmann@33595
   257
lemma istuple_update_swap_snd_snd:
haftmann@33595
   258
  "h f o j g = j g o h f \<Longrightarrow>
haftmann@33595
   259
    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
haftmann@33595
   260
          = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
haftmann@33595
   261
  by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
haftmann@33595
   262
haftmann@33595
   263
lemma istuple_update_swap_fst_snd:
haftmann@33595
   264
  "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
haftmann@33595
   265
          = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
haftmann@33595
   266
  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
haftmann@33595
   267
haftmann@33595
   268
lemma istuple_update_swap_snd_fst:
haftmann@33595
   269
  "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
haftmann@33595
   270
          = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
haftmann@33595
   271
  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
haftmann@33595
   272
haftmann@33595
   273
lemma istuple_update_compose_fst_fst:
haftmann@33595
   274
  "h f o j g = k (f o g) \<Longrightarrow>
haftmann@33595
   275
    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
haftmann@33595
   276
          = (istuple_fst_update isom o k) (f o g)"
haftmann@33595
   277
  by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
haftmann@33595
   278
haftmann@33595
   279
lemma istuple_update_compose_snd_snd:
haftmann@33595
   280
  "h f o j g = k (f o g) \<Longrightarrow>
haftmann@33595
   281
    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
haftmann@33595
   282
          = (istuple_snd_update isom o k) (f o g)"
haftmann@33595
   283
  by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
haftmann@33595
   284
haftmann@33595
   285
lemma istuple_surjective_proof_assist_step:
haftmann@33595
   286
  "istuple_surjective_proof_assist v a (istuple_fst isom o f) \<Longrightarrow>
haftmann@33595
   287
     istuple_surjective_proof_assist v b (istuple_snd isom o f)
haftmann@33595
   288
      \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
haftmann@33595
   289
  by (clarsimp simp: istuple_surjective_proof_assist_def simps
haftmann@33595
   290
    istuple_fst_def istuple_snd_def istuple_cons_def)
haftmann@33595
   291
haftmann@33595
   292
lemma istuple_fst_update_accessor_cong_assist:
haftmann@33595
   293
  assumes "istuple_update_accessor_cong_assist f g"
haftmann@33595
   294
  shows "istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
haftmann@33595
   295
proof -
haftmann@33595
   296
  from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
haftmann@33595
   297
  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
haftmann@33595
   298
    istuple_fst_update_def istuple_fst_def)
haftmann@33595
   299
qed
haftmann@33595
   300
haftmann@33595
   301
lemma istuple_snd_update_accessor_cong_assist:
haftmann@33595
   302
  assumes "istuple_update_accessor_cong_assist f g"
haftmann@33595
   303
  shows "istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
haftmann@33595
   304
proof -
haftmann@33595
   305
  from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
haftmann@33595
   306
  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
haftmann@33595
   307
    istuple_snd_update_def istuple_snd_def)
haftmann@33595
   308
qed
haftmann@33595
   309
haftmann@33595
   310
lemma istuple_fst_update_accessor_eq_assist:
haftmann@33595
   311
  assumes "istuple_update_accessor_eq_assist f g a u a' v"
haftmann@33595
   312
  shows "istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
haftmann@33595
   313
    (istuple_cons isom a b) u (istuple_cons isom a' b) v"
haftmann@33595
   314
proof -
haftmann@33595
   315
  from assms have "f id = id"
haftmann@33595
   316
    by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
haftmann@33595
   317
  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
haftmann@33595
   318
    istuple_fst_update_def istuple_fst_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
haftmann@33595
   319
qed
haftmann@33595
   320
haftmann@33595
   321
lemma istuple_snd_update_accessor_eq_assist:
haftmann@33595
   322
  assumes "istuple_update_accessor_eq_assist f g b u b' v"
haftmann@33595
   323
  shows "istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
haftmann@33595
   324
    (istuple_cons isom a b) u (istuple_cons isom a b') v"
haftmann@33595
   325
proof -
haftmann@33595
   326
  from assms have "f id = id"
haftmann@33595
   327
    by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
haftmann@33595
   328
  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
haftmann@33595
   329
    istuple_snd_update_def istuple_snd_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
haftmann@33595
   330
qed
haftmann@33595
   331
haftmann@33595
   332
lemma istuple_cons_conj_eqI:
haftmann@33595
   333
  "a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
haftmann@33595
   334
    istuple_cons isom a b = istuple_cons isom c d \<and> P \<longleftrightarrow> Q"
haftmann@33595
   335
  by (clarsimp simp: istuple_cons_def simps)
haftmann@33595
   336
haftmann@33595
   337
lemmas intros =
haftmann@33595
   338
    istuple_access_update_fst_fst
haftmann@33595
   339
    istuple_access_update_snd_snd
haftmann@33595
   340
    istuple_access_update_fst_snd
haftmann@33595
   341
    istuple_access_update_snd_fst
haftmann@33595
   342
    istuple_update_swap_fst_fst
haftmann@33595
   343
    istuple_update_swap_snd_snd
haftmann@33595
   344
    istuple_update_swap_fst_snd
haftmann@33595
   345
    istuple_update_swap_snd_fst
haftmann@33595
   346
    istuple_update_compose_fst_fst
haftmann@33595
   347
    istuple_update_compose_snd_snd
haftmann@33595
   348
    istuple_surjective_proof_assist_step
haftmann@33595
   349
    istuple_fst_update_accessor_eq_assist
haftmann@33595
   350
    istuple_snd_update_accessor_eq_assist
haftmann@33595
   351
    istuple_fst_update_accessor_cong_assist
haftmann@33595
   352
    istuple_snd_update_accessor_cong_assist
haftmann@33595
   353
    istuple_cons_conj_eqI
haftmann@33595
   354
haftmann@33595
   355
end
haftmann@33595
   356
haftmann@33595
   357
lemma isomorphic_tuple_intro:
haftmann@33595
   358
  fixes repr abst
haftmann@33595
   359
  assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
haftmann@33595
   360
     and abst_inv: "\<And>z. repr (abst z) = z"
haftmann@33595
   361
  assumes v: "v \<equiv> TupleIsomorphism repr abst"
haftmann@33595
   362
  shows "isomorphic_tuple v"
haftmann@33595
   363
  apply (rule isomorphic_tuple.intro)
haftmann@33595
   364
  apply (simp_all add: abst_inv v)
haftmann@33595
   365
  apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
haftmann@33595
   366
  apply (simp add: abst_inv)
haftmann@33595
   367
  done
haftmann@33595
   368
haftmann@33595
   369
definition
haftmann@33595
   370
  "tuple_istuple \<equiv> TupleIsomorphism id id"
haftmann@33595
   371
haftmann@33595
   372
lemma tuple_istuple:
haftmann@33595
   373
  "isomorphic_tuple tuple_istuple"
haftmann@33595
   374
  by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_istuple_def)
haftmann@33595
   375
haftmann@33595
   376
lemma refl_conj_eq:
haftmann@33595
   377
  "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
haftmann@33595
   378
  by simp
haftmann@33595
   379
haftmann@33595
   380
lemma istuple_UNIV_I: "x \<in> UNIV \<equiv> True"
haftmann@33595
   381
  by simp
haftmann@33595
   382
haftmann@33595
   383
lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
haftmann@33595
   384
  by simp
haftmann@33595
   385
schirmer@14700
   386
lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
schirmer@14700
   387
  by simp
wenzelm@11826
   388
schirmer@25705
   389
lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" 
schirmer@25705
   390
  by (simp add: comp_def)
wenzelm@11821
   391
tsewell@32743
   392
lemma o_eq_dest_lhs:
tsewell@32743
   393
  "a o b = c \<Longrightarrow> a (b v) = c v"
tsewell@32743
   394
  by clarsimp
tsewell@32743
   395
tsewell@32743
   396
lemma o_eq_id_dest:
tsewell@32743
   397
  "a o b = id o c \<Longrightarrow> a (b v) = c v"
tsewell@32743
   398
  by clarsimp
wenzelm@22817
   399
haftmann@33595
   400
wenzelm@11833
   401
subsection {* Concrete record syntax *}
wenzelm@4870
   402
wenzelm@4870
   403
nonterminals
wenzelm@5198
   404
  ident field_type field_types field fields update updates
wenzelm@4870
   405
syntax
wenzelm@11821
   406
  "_constify"           :: "id => ident"                        ("_")
wenzelm@11821
   407
  "_constify"           :: "longid => ident"                    ("_")
wenzelm@5198
   408
wenzelm@11821
   409
  "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
wenzelm@11821
   410
  ""                    :: "field_type => field_types"          ("_")
wenzelm@11821
   411
  "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
wenzelm@11821
   412
  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
wenzelm@10093
   413
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
wenzelm@5198
   414
wenzelm@11821
   415
  "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
wenzelm@11821
   416
  ""                    :: "field => fields"                    ("_")
wenzelm@11821
   417
  "_fields"             :: "[field, fields] => fields"          ("_,/ _")
wenzelm@11821
   418
  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
wenzelm@10093
   419
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
wenzelm@5198
   420
wenzelm@10641
   421
  "_update_name"        :: idt
wenzelm@11821
   422
  "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
wenzelm@11821
   423
  ""                    :: "update => updates"                  ("_")
wenzelm@11821
   424
  "_updates"            :: "[update, updates] => updates"       ("_,/ _")
wenzelm@10093
   425
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
wenzelm@4870
   426
wenzelm@10331
   427
syntax (xsymbols)
wenzelm@11821
   428
  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
wenzelm@10093
   429
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
wenzelm@10093
   430
  "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
wenzelm@10093
   431
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
wenzelm@10093
   432
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
wenzelm@9729
   433
tsewell@32752
   434
haftmann@33595
   435
subsection {* Record package *}
tsewell@32752
   436
tsewell@32744
   437
use "Tools/record.ML"
tsewell@32744
   438
setup Record.setup
wenzelm@10641
   439
haftmann@33595
   440
hide (open) const TupleIsomorphism repr abst istuple_fst istuple_snd
haftmann@33595
   441
  istuple_fst_update istuple_snd_update istuple_cons
haftmann@33595
   442
  istuple_surjective_proof_assist istuple_update_accessor_cong_assist
haftmann@33595
   443
  istuple_update_accessor_eq_assist tuple_istuple
haftmann@33595
   444
wenzelm@4870
   445
end