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