wenzelm@4870: (*  Title:      HOL/Record.thy
wenzelm@32763:     Author:     Wolfgang Naraschewski, TU Muenchen
wenzelm@32763:     Author:     Markus Wenzel, TU Muenchen
wenzelm@32763:     Author:     Norbert Schirmer, TU Muenchen
wenzelm@32763:     Author:     Thomas Sewell, NICTA
haftmann@33595:     Author:     Florian Haftmann, TU Muenchen
wenzelm@4870: *)
wenzelm@4870: 
wenzelm@22817: header {* Extensible records with structural subtyping *}
wenzelm@22817: 
nipkow@15131: theory Record
blanchet@56048: imports Quickcheck_Exhaustive
wenzelm@46950: keywords "record" :: thy_decl
nipkow@15131: begin
wenzelm@4870: 
haftmann@33595: subsection {* Introduction *}
haftmann@33595: 
haftmann@33595: text {*
haftmann@33595:   Records are isomorphic to compound tuple types. To implement
haftmann@33595:   efficient records, we make this isomorphism explicit. Consider the
haftmann@33595:   record access/update simplification @{text "alpha (beta_update f
haftmann@33595:   rec) = alpha rec"} for distinct fields alpha and beta of some record
haftmann@33595:   rec with n fields. There are @{text "n ^ 2"} such theorems, which
haftmann@33595:   prohibits storage of all of them for large n. The rules can be
haftmann@33595:   proved on the fly by case decomposition and simplification in O(n)
haftmann@33595:   time. By creating O(n) isomorphic-tuple types while defining the
haftmann@33595:   record, however, we can prove the access/update simplification in
haftmann@33595:   @{text "O(log(n)^2)"} time.
haftmann@33595: 
haftmann@33595:   The O(n) cost of case decomposition is not because O(n) steps are
haftmann@33595:   taken, but rather because the resulting rule must contain O(n) new
haftmann@33595:   variables and an O(n) size concrete record construction. To sidestep
haftmann@33595:   this cost, we would like to avoid case decomposition in proving
haftmann@33595:   access/update theorems.
haftmann@33595: 
haftmann@33595:   Record types are defined as isomorphic to tuple types. For instance,
haftmann@33595:   a record type with fields @{text "'a"}, @{text "'b"}, @{text "'c"}
haftmann@33595:   and @{text "'d"} might be introduced as isomorphic to @{text "'a \<times>
haftmann@33595:   ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to @{text "('a \<times>
haftmann@33595:   'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to the
haftmann@33595:   underlying type then using O(log(n)) fst or snd operations.
haftmann@33595:   Updators can be defined similarly, if we introduce a @{text
haftmann@33595:   "fst_update"} and @{text "snd_update"} function. Furthermore, we can
haftmann@33595:   prove the access/update theorem in O(log(n)) steps by using simple
haftmann@33595:   rewrites on fst, snd, @{text "fst_update"} and @{text "snd_update"}.
haftmann@33595: 
haftmann@33595:   The catch is that, although O(log(n)) steps were taken, the
haftmann@33595:   underlying type we converted to is a tuple tree of size
haftmann@33595:   O(n). Processing this term type wastes performance. We avoid this
haftmann@33595:   for large n by taking each subtree of size K and defining a new type
haftmann@33595:   isomorphic to that tuple subtree. A record can now be defined as
haftmann@33595:   isomorphic to a tuple tree of these O(n/K) new types, or, if @{text
haftmann@33595:   "n > K*K"}, we can repeat the process, until the record can be
haftmann@33595:   defined in terms of a tuple tree of complexity less than the
haftmann@33595:   constant K.
haftmann@33595: 
haftmann@33595:   If we prove the access/update theorem on this type with the
huffman@44922:   analogous steps to the tuple tree, we consume @{text "O(log(n)^2)"}
haftmann@33595:   time as the intermediate terms are @{text "O(log(n))"} in size and
huffman@44922:   the types needed have size bounded by K.  To enable this analogous
haftmann@33595:   traversal, we define the functions seen below: @{text
haftmann@34151:   "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"}
haftmann@34151:   and @{text "iso_tuple_snd_update"}. These functions generalise tuple
haftmann@33595:   operations by taking a parameter that encapsulates a tuple
haftmann@33595:   isomorphism.  The rewrites needed on these functions now need an
haftmann@33595:   additional assumption which is that the isomorphism works.
haftmann@33595: 
haftmann@33595:   These rewrites are typically used in a structured way. They are here
haftmann@33595:   presented as the introduction rule @{text "isomorphic_tuple.intros"}
haftmann@33595:   rather than as a rewrite rule set. The introduction form is an
haftmann@33595:   optimisation, as net matching can be performed at one term location
haftmann@33595:   for each step rather than the simplifier searching the term for
haftmann@33595:   possible pattern matches. The rule set is used as it is viewed
haftmann@33595:   outside the locale, with the locale assumption (that the isomorphism
haftmann@33595:   is valid) left as a rule assumption. All rules are structured to aid
haftmann@33595:   net matching, using either a point-free form or an encapsulating
haftmann@33595:   predicate.
haftmann@33595: *}
haftmann@33595: 
haftmann@33595: subsection {* Operators and lemmas for types isomorphic to tuples *}
haftmann@33595: 
wenzelm@35132: datatype ('a, 'b, 'c) tuple_isomorphism =
wenzelm@35132:   Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
haftmann@33595: 
wenzelm@35132: primrec
wenzelm@35132:   repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where
haftmann@34151:   "repr (Tuple_Isomorphism r a) = r"
haftmann@33595: 
wenzelm@35132: primrec
wenzelm@35132:   abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
haftmann@34151:   "abst (Tuple_Isomorphism r a) = a"
haftmann@33595: 
wenzelm@35132: definition
wenzelm@35132:   iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
haftmann@34151:   "iso_tuple_fst isom = fst \<circ> repr isom"
haftmann@33595: 
wenzelm@35132: definition
wenzelm@35132:   iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
haftmann@34151:   "iso_tuple_snd isom = snd \<circ> repr isom"
haftmann@33595: 
wenzelm@35132: definition
wenzelm@35132:   iso_tuple_fst_update ::
wenzelm@35132:     "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
haftmann@34151:   "iso_tuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
haftmann@33595: 
wenzelm@35132: definition
wenzelm@35132:   iso_tuple_snd_update ::
wenzelm@35132:     "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
haftmann@34151:   "iso_tuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
haftmann@33595: 
wenzelm@35132: definition
wenzelm@35132:   iso_tuple_cons ::
wenzelm@35132:     "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
haftmann@34151:   "iso_tuple_cons isom = curry (abst isom)"
haftmann@33595: 
haftmann@33595: 
haftmann@33595: subsection {* Logical infrastructure for records *}
haftmann@33595: 
wenzelm@35132: definition
wenzelm@35132:   iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
haftmann@34151:   "iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
haftmann@33595: 
wenzelm@35132: definition
wenzelm@35132:   iso_tuple_update_accessor_cong_assist ::
wenzelm@35132:     "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
haftmann@38394:   "iso_tuple_update_accessor_cong_assist upd ac \<longleftrightarrow>
haftmann@38394:      (\<forall>f v. upd (\<lambda>x. f (ac v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
haftmann@33595: 
wenzelm@35132: definition
wenzelm@35132:   iso_tuple_update_accessor_eq_assist ::
wenzelm@35132:     "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
haftmann@38394:   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<longleftrightarrow>
haftmann@38394:      upd f v = v' \<and> ac v = x \<and> iso_tuple_update_accessor_cong_assist upd ac"
haftmann@33595: 
haftmann@33595: lemma update_accessor_congruence_foldE:
haftmann@38394:   assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
haftmann@38394:     and r: "r = r'" and v: "ac r' = v'"
wenzelm@35132:     and f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
wenzelm@35132:   shows "upd f r = upd f' r'"
haftmann@33595:   using uac r v [symmetric]
haftmann@38394:   apply (subgoal_tac "upd (\<lambda>x. f (ac r')) r' = upd (\<lambda>x. f' (ac r')) r'")
haftmann@34151:    apply (simp add: iso_tuple_update_accessor_cong_assist_def)
haftmann@33595:   apply (simp add: f)
haftmann@33595:   done
haftmann@33595: 
haftmann@33595: lemma update_accessor_congruence_unfoldE:
haftmann@38394:   "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
haftmann@38394:     r = r' \<Longrightarrow> ac r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v) \<Longrightarrow>
wenzelm@35132:     upd f r = upd f' r'"
haftmann@33595:   apply (erule(2) update_accessor_congruence_foldE)
haftmann@33595:   apply simp
haftmann@33595:   done
haftmann@33595: 
haftmann@34151: lemma iso_tuple_update_accessor_cong_assist_id:
haftmann@38394:   "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow> upd id = id"
haftmann@34151:   by rule (simp add: iso_tuple_update_accessor_cong_assist_def)
haftmann@33595: 
haftmann@33595: lemma update_accessor_noopE:
haftmann@38394:   assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
haftmann@38394:     and ac: "f (ac x) = ac x"
wenzelm@35132:   shows "upd f x = x"
wenzelm@35132:   using uac
haftmann@38394:   by (simp add: ac iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
wenzelm@35132:     cong: update_accessor_congruence_unfoldE [OF uac])
haftmann@33595: 
haftmann@33595: lemma update_accessor_noop_compE:
haftmann@38394:   assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
haftmann@38394:     and ac: "f (ac x) = ac x"
wenzelm@35132:   shows "upd (g \<circ> f) x = upd g x"
haftmann@38394:   by (simp add: ac cong: update_accessor_congruence_unfoldE[OF uac])
haftmann@33595: 
haftmann@33595: lemma update_accessor_cong_assist_idI:
haftmann@34151:   "iso_tuple_update_accessor_cong_assist id id"
haftmann@34151:   by (simp add: iso_tuple_update_accessor_cong_assist_def)
haftmann@33595: 
haftmann@33595: lemma update_accessor_cong_assist_triv:
haftmann@38394:   "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
haftmann@38394:     iso_tuple_update_accessor_cong_assist upd ac"
haftmann@33595:   by assumption
haftmann@33595: 
haftmann@33595: lemma update_accessor_accessor_eqE:
haftmann@38394:   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> ac v = x"
haftmann@34151:   by (simp add: iso_tuple_update_accessor_eq_assist_def)
haftmann@33595: 
haftmann@33595: lemma update_accessor_updator_eqE:
haftmann@38394:   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> upd f v = v'"
haftmann@34151:   by (simp add: iso_tuple_update_accessor_eq_assist_def)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_update_accessor_eq_assist_idI:
haftmann@34151:   "v' = f v \<Longrightarrow> iso_tuple_update_accessor_eq_assist id id v f v' v"
haftmann@34151:   by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_update_accessor_eq_assist_triv:
haftmann@38394:   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
haftmann@38394:     iso_tuple_update_accessor_eq_assist upd ac v f v' x"
haftmann@33595:   by assumption
haftmann@33595: 
haftmann@34151: lemma iso_tuple_update_accessor_cong_from_eq:
haftmann@38394:   "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
haftmann@38394:     iso_tuple_update_accessor_cong_assist upd ac"
haftmann@34151:   by (simp add: iso_tuple_update_accessor_eq_assist_def)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_surjective_proof_assistI:
haftmann@34151:   "f x = y \<Longrightarrow> iso_tuple_surjective_proof_assist x y f"
haftmann@34151:   by (simp add: iso_tuple_surjective_proof_assist_def)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_surjective_proof_assist_idE:
haftmann@34151:   "iso_tuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
haftmann@34151:   by (simp add: iso_tuple_surjective_proof_assist_def)
haftmann@33595: 
haftmann@33595: locale isomorphic_tuple =
haftmann@33595:   fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
haftmann@34151:   assumes repr_inv: "\<And>x. abst isom (repr isom x) = x"
wenzelm@35132:     and abst_inv: "\<And>y. repr isom (abst isom y) = y"
haftmann@33595: begin
haftmann@33595: 
wenzelm@35132: lemma repr_inj: "repr isom x = repr isom y \<longleftrightarrow> x = y"
wenzelm@35132:   by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"]
wenzelm@35132:     simp add: repr_inv)
haftmann@33595: 
wenzelm@35132: lemma abst_inj: "abst isom x = abst isom y \<longleftrightarrow> x = y"
wenzelm@35132:   by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"]
wenzelm@35132:     simp add: abst_inv)
haftmann@34151: 
haftmann@34151: lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj
haftmann@33595: 
haftmann@34151: lemma iso_tuple_access_update_fst_fst:
haftmann@33595:   "f o h g = j o f \<Longrightarrow>
wenzelm@35132:     (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g =
wenzelm@35132:       j o (f o iso_tuple_fst isom)"
haftmann@34151:   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps
huffman@44922:     fun_eq_iff)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_access_update_snd_snd:
haftmann@33595:   "f o h g = j o f \<Longrightarrow>
wenzelm@35132:     (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g =
wenzelm@35132:       j o (f o iso_tuple_snd isom)"
haftmann@34151:   by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps
huffman@44922:     fun_eq_iff)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_access_update_fst_snd:
wenzelm@35132:   "(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g =
wenzelm@35132:     id o (f o iso_tuple_fst isom)"
haftmann@34151:   by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps
huffman@44922:     fun_eq_iff)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_access_update_snd_fst:
wenzelm@35132:   "(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g =
wenzelm@35132:     id o (f o iso_tuple_snd isom)"
haftmann@34151:   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps
huffman@44922:     fun_eq_iff)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_update_swap_fst_fst:
haftmann@33595:   "h f o j g = j g o h f \<Longrightarrow>
wenzelm@35132:     (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g =
wenzelm@35132:       (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f"
huffman@44922:   by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_update_swap_snd_snd:
haftmann@33595:   "h f o j g = j g o h f \<Longrightarrow>
wenzelm@35132:     (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g =
wenzelm@35132:       (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f"
huffman@44922:   by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_update_swap_fst_snd:
wenzelm@35132:   "(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g =
wenzelm@35132:     (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f"
wenzelm@35132:   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def
huffman@44922:     simps fun_eq_iff)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_update_swap_snd_fst:
wenzelm@35132:   "(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g =
wenzelm@35132:     (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f"
huffman@44922:   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps
huffman@44922:     fun_eq_iff)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_update_compose_fst_fst:
haftmann@33595:   "h f o j g = k (f o g) \<Longrightarrow>
wenzelm@35132:     (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g =
wenzelm@35132:       (iso_tuple_fst_update isom o k) (f o g)"
huffman@44922:   by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_update_compose_snd_snd:
haftmann@33595:   "h f o j g = k (f o g) \<Longrightarrow>
wenzelm@35132:     (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g =
wenzelm@35132:       (iso_tuple_snd_update isom o k) (f o g)"
huffman@44922:   by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_surjective_proof_assist_step:
haftmann@34151:   "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \<Longrightarrow>
wenzelm@35132:     iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f) \<Longrightarrow>
wenzelm@35132:     iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f"
haftmann@34151:   by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps
haftmann@34151:     iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def)
haftmann@33595: 
haftmann@34151: lemma iso_tuple_fst_update_accessor_cong_assist:
haftmann@34151:   assumes "iso_tuple_update_accessor_cong_assist f g"
wenzelm@35132:   shows "iso_tuple_update_accessor_cong_assist
wenzelm@35132:     (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)"
haftmann@33595: proof -
wenzelm@35132:   from assms have "f id = id"
wenzelm@35132:     by (rule iso_tuple_update_accessor_cong_assist_id)
wenzelm@35132:   with assms show ?thesis
wenzelm@35132:     by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
wenzelm@35132:       iso_tuple_fst_update_def iso_tuple_fst_def)
haftmann@33595: qed
haftmann@33595: 
haftmann@34151: lemma iso_tuple_snd_update_accessor_cong_assist:
haftmann@34151:   assumes "iso_tuple_update_accessor_cong_assist f g"
wenzelm@35132:   shows "iso_tuple_update_accessor_cong_assist
wenzelm@35132:     (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)"
haftmann@33595: proof -
wenzelm@35132:   from assms have "f id = id"
wenzelm@35132:     by (rule iso_tuple_update_accessor_cong_assist_id)
wenzelm@35132:   with assms show ?thesis
wenzelm@35132:     by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
wenzelm@35132:       iso_tuple_snd_update_def iso_tuple_snd_def)
haftmann@33595: qed
haftmann@33595: 
haftmann@34151: lemma iso_tuple_fst_update_accessor_eq_assist:
haftmann@34151:   assumes "iso_tuple_update_accessor_eq_assist f g a u a' v"
wenzelm@35132:   shows "iso_tuple_update_accessor_eq_assist
wenzelm@35132:     (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)
haftmann@34151:     (iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v"
haftmann@33595: proof -
haftmann@33595:   from assms have "f id = id"
wenzelm@35132:     by (auto simp add: iso_tuple_update_accessor_eq_assist_def
wenzelm@35132:       intro: iso_tuple_update_accessor_cong_assist_id)
wenzelm@35132:   with assms show ?thesis
wenzelm@35132:     by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
wenzelm@35132:       iso_tuple_fst_update_def iso_tuple_fst_def
wenzelm@35132:       iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
haftmann@33595: qed
haftmann@33595: 
haftmann@34151: lemma iso_tuple_snd_update_accessor_eq_assist:
haftmann@34151:   assumes "iso_tuple_update_accessor_eq_assist f g b u b' v"
wenzelm@35132:   shows "iso_tuple_update_accessor_eq_assist
wenzelm@35132:     (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)
haftmann@34151:     (iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v"
haftmann@33595: proof -
haftmann@33595:   from assms have "f id = id"
wenzelm@35132:     by (auto simp add: iso_tuple_update_accessor_eq_assist_def
wenzelm@35132:       intro: iso_tuple_update_accessor_cong_assist_id)
wenzelm@35132:   with assms show ?thesis
wenzelm@35132:     by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
wenzelm@35132:       iso_tuple_snd_update_def iso_tuple_snd_def
wenzelm@35132:       iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
haftmann@33595: qed
haftmann@33595: 
haftmann@34151: lemma iso_tuple_cons_conj_eqI:
haftmann@33595:   "a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
haftmann@34151:     iso_tuple_cons isom a b = iso_tuple_cons isom c d \<and> P \<longleftrightarrow> Q"
haftmann@34151:   by (clarsimp simp: iso_tuple_cons_def simps)
haftmann@33595: 
haftmann@33595: lemmas intros =
wenzelm@35132:   iso_tuple_access_update_fst_fst
wenzelm@35132:   iso_tuple_access_update_snd_snd
wenzelm@35132:   iso_tuple_access_update_fst_snd
wenzelm@35132:   iso_tuple_access_update_snd_fst
wenzelm@35132:   iso_tuple_update_swap_fst_fst
wenzelm@35132:   iso_tuple_update_swap_snd_snd
wenzelm@35132:   iso_tuple_update_swap_fst_snd
wenzelm@35132:   iso_tuple_update_swap_snd_fst
wenzelm@35132:   iso_tuple_update_compose_fst_fst
wenzelm@35132:   iso_tuple_update_compose_snd_snd
wenzelm@35132:   iso_tuple_surjective_proof_assist_step
wenzelm@35132:   iso_tuple_fst_update_accessor_eq_assist
wenzelm@35132:   iso_tuple_snd_update_accessor_eq_assist
wenzelm@35132:   iso_tuple_fst_update_accessor_cong_assist
wenzelm@35132:   iso_tuple_snd_update_accessor_cong_assist
wenzelm@35132:   iso_tuple_cons_conj_eqI
haftmann@33595: 
haftmann@33595: end
haftmann@33595: 
haftmann@33595: lemma isomorphic_tuple_intro:
haftmann@33595:   fixes repr abst
haftmann@33595:   assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
wenzelm@35132:     and abst_inv: "\<And>z. repr (abst z) = z"
wenzelm@35132:     and v: "v \<equiv> Tuple_Isomorphism repr abst"
haftmann@33595:   shows "isomorphic_tuple v"
haftmann@34151: proof
wenzelm@35132:   fix x have "repr (abst (repr x)) = repr x"
haftmann@34151:     by (simp add: abst_inv)
wenzelm@35132:   then show "Record.abst v (Record.repr v x) = x"
haftmann@34151:     by (simp add: v repr_inj)
wenzelm@35132: next
wenzelm@35132:   fix y
wenzelm@35132:   show "Record.repr v (Record.abst v y) = y"
haftmann@34151:     by (simp add: v) (fact abst_inv)
haftmann@34151: qed
haftmann@33595: 
haftmann@33595: definition
haftmann@34151:   "tuple_iso_tuple \<equiv> Tuple_Isomorphism id id"
haftmann@33595: 
haftmann@34151: lemma tuple_iso_tuple:
haftmann@34151:   "isomorphic_tuple tuple_iso_tuple"
haftmann@34151:   by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def)
haftmann@33595: 
wenzelm@35132: lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
haftmann@33595:   by simp
haftmann@33595: 
blanchet@54147: lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
haftmann@33595:   by simp
haftmann@33595: 
haftmann@34151: lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
haftmann@33595:   by simp
haftmann@33595: 
schirmer@14700: lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
schirmer@14700:   by simp
wenzelm@11826: 
wenzelm@35132: lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
schirmer@25705:   by (simp add: comp_def)
wenzelm@11821: 
haftmann@33595: 
wenzelm@11833: subsection {* Concrete record syntax *}
wenzelm@4870: 
wenzelm@41229: nonterminal
wenzelm@41229:   ident and
wenzelm@41229:   field_type and
wenzelm@41229:   field_types and
wenzelm@41229:   field and
wenzelm@41229:   fields and
wenzelm@41229:   field_update and
wenzelm@41229:   field_updates
wenzelm@41229: 
wenzelm@4870: syntax
wenzelm@11821:   "_constify"           :: "id => ident"                        ("_")
wenzelm@11821:   "_constify"           :: "longid => ident"                    ("_")
wenzelm@5198: 
wenzelm@35144:   "_field_type"         :: "ident => type => field_type"        ("(2_ ::/ _)")
wenzelm@11821:   ""                    :: "field_type => field_types"          ("_")
wenzelm@35144:   "_field_types"        :: "field_type => field_types => field_types"    ("_,/ _")
wenzelm@11821:   "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
wenzelm@35144:   "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
wenzelm@5198: 
wenzelm@35144:   "_field"              :: "ident => 'a => field"               ("(2_ =/ _)")
wenzelm@11821:   ""                    :: "field => fields"                    ("_")
wenzelm@35144:   "_fields"             :: "field => fields => fields"          ("_,/ _")
wenzelm@11821:   "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
wenzelm@35144:   "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
wenzelm@5198: 
wenzelm@35146:   "_field_update"       :: "ident => 'a => field_update"        ("(2_ :=/ _)")
wenzelm@35146:   ""                    :: "field_update => field_updates"      ("_")
wenzelm@35146:   "_field_updates"      :: "field_update => field_updates => field_updates"  ("_,/ _")
wenzelm@35146:   "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
wenzelm@4870: 
wenzelm@10331: syntax (xsymbols)
wenzelm@11821:   "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
wenzelm@35132:   "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
wenzelm@35132:   "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
wenzelm@35132:   "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
wenzelm@35146:   "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
wenzelm@9729: 
tsewell@32752: 
haftmann@33595: subsection {* Record package *}
tsewell@32752: 
wenzelm@56732: ML_file "Tools/record.ML"
wenzelm@10641: 
wenzelm@36176: hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
haftmann@34151:   iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
haftmann@34151:   iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
haftmann@34151:   iso_tuple_update_accessor_eq_assist tuple_iso_tuple
haftmann@33595: 
wenzelm@4870: end