src/HOL/Record.thy
author tsewell@rubicon.NSW.bigpond.net.au
Wed Sep 23 19:17:48 2009 +1000 (2009-09-23)
changeset 32752 f65d74a264dd
parent 32745 192d58483fdf
child 32756 fb32a99a7689
permissions -rw-r--r--
Initial response to feedback from Norbert, Makarius on record patch

As Norbert recommended, the IsTuple.thy and istuple_support.ML files
have been integrated into Record.thy and record.ML. I haven't merged
the structures - record.ML now contains Record and IsTupleSupport.

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