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