(*  Title:      HOL/Record.thy
    Author:     Wolfgang Naraschewski, TU Muenchen
    Author:     Markus Wenzel, TU Muenchen
    Author:     Norbert Schirmer, TU Muenchen
    Author:     Thomas Sewell, NICTA
    Author:     Florian Haftmann, TU Muenchen
*)

section ‹Extensible records with structural subtyping›

theory Record
imports Quickcheck_Exhaustive
keywords
  "record" :: thy_defn and
  "print_record" :: diag
begin

subsection ‹Introduction›

text ‹
 Records are isomorphic to compound tuple types. To implement
 efficient records, we make this isomorphism explicit. Consider the
 record access/update simplification ‹alpha (beta_update f
 rec) = alpha rec› for distinct fields alpha and beta of some record
 rec with n fields. There are ‹n ^ 2› such theorems, which
 prohibits storage of all of them for large n. The rules can be
 proved on the fly by case decomposition and simplification in O(n)
 time. By creating O(n) isomorphic-tuple types while defining the
 record, however, we can prove the access/update simplification in
 ‹O(log(n)^2)› time.

 The O(n) cost of case decomposition is not because O(n) steps are
 taken, but rather because the resulting rule must contain O(n) new
 variables and an O(n) size concrete record construction. To sidestep
 this cost, we would like to avoid case decomposition in proving
 access/update theorems.

 Record types are defined as isomorphic to tuple types. For instance,
 a record type with fields ‹'a›, ‹'b›, ‹'c›
 and ‹'d› might be introduced as isomorphic to ‹'a ×
 ('b × ('c × 'd))›. If we balance the tuple tree to ‹('a ×
 'b) × ('c × 'd)› then accessors can be defined by converting to the
 underlying type then using O(log(n)) fst or snd operations.
 Updators can be defined similarly, if we introduce a ‹fst_update› and ‹snd_update› function. Furthermore, we can
 prove the access/update theorem in O(log(n)) steps by using simple
 rewrites on fst, snd, ‹fst_update› and ‹snd_update›.

 The catch is that, although O(log(n)) steps were taken, the
 underlying type we converted to is a tuple tree of size
 O(n). Processing this term type wastes performance. We avoid this
 for large n by taking each subtree of size K and defining a new type
 isomorphic to that tuple subtree. A record can now be defined as
 isomorphic to a tuple tree of these O(n/K) new types, or, if ‹n > K*K›, we can repeat the process, until the record can be
 defined in terms of a tuple tree of complexity less than the
 constant K.

 If we prove the access/update theorem on this type with the
 analogous steps to the tuple tree, we consume ‹O(log(n)^2)›
 time as the intermediate terms are ‹O(log(n))› in size and
 the types needed have size bounded by K. To enable this analogous
 traversal, we define the functions seen below: ‹iso_tuple_fst›, ‹iso_tuple_snd›, ‹iso_tuple_fst_update›
 and ‹iso_tuple_snd_update›. These functions generalise tuple
 operations by taking a parameter that encapsulates a tuple
 isomorphism. The rewrites needed on these functions now need an
 additional assumption which is that the isomorphism works.

 These rewrites are typically used in a structured way. They are here
 presented as the introduction rule ‹isomorphic_tuple.intros›
 rather than as a rewrite rule set. The introduction form is an
 optimisation, as net matching can be performed at one term location
 for each step rather than the simplifier searching the term for
 possible pattern matches. The rule set is used as it is viewed
 outside the locale, with the locale assumption (that the isomorphism
 is valid) left as a rule assumption. All rules are structured to aid
 net matching, using either a point-free form or an encapsulating
 predicate.
 ›

subsection ‹Operators and lemmas for types isomorphic to tuples›

datatype (dead 'a, dead 'b, dead 'c) tuple_isomorphism =
  Tuple_Isomorphism "'a → 'b × 'c" "'b × 'c → 'a"

primrec
  repr :: "('a, 'b, 'c) tuple_isomorphism → 'a → 'b × 'c" where
  "repr (Tuple_Isomorphism r a) = r"

primrec
  abst :: "('a, 'b, 'c) tuple_isomorphism → 'b × 'c → 'a" where
  "abst (Tuple_Isomorphism r a) = a"

definition
  iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism → 'a → 'b" where
  "iso_tuple_fst isom = fst ∘ repr isom"

definition
  iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism → 'a → 'c" where
  "iso_tuple_snd isom = snd ∘ repr isom"

definition
  iso_tuple_fst_update ::
    "('a, 'b, 'c) tuple_isomorphism → ('b → 'b) → ('a → 'a)" where
  "iso_tuple_fst_update isom f = abst isom ∘ apfst f ∘ repr isom"

definition
  iso_tuple_snd_update ::
    "('a, 'b, 'c) tuple_isomorphism → ('c → 'c) → ('a → 'a)" where
  "iso_tuple_snd_update isom f = abst isom ∘ apsnd f ∘ repr isom"

definition
  iso_tuple_cons ::
    "('a, 'b, 'c) tuple_isomorphism → 'b → 'c → 'a" where
  "iso_tuple_cons isom = curry (abst isom)"


subsection ‹Logical infrastructure for records›

definition
  iso_tuple_surjective_proof_assist :: "'a → 'b → ('a → 'b) → bool" where
  "iso_tuple_surjective_proof_assist x y f ⟷ f x = y"

definition
  iso_tuple_update_accessor_cong_assist ::
    "(('b → 'b) → ('a → 'a)) → ('a → 'b) → bool" where
  "iso_tuple_update_accessor_cong_assist upd ac ⟷
     (∀f v. upd (λx. f (ac v)) v = upd f v) ∧ (∀v. upd id v = v)"

definition
  iso_tuple_update_accessor_eq_assist ::
    "(('b → 'b) → ('a → 'a)) → ('a → 'b) → 'a → ('b → 'b) → 'a → 'b → bool" where
  "iso_tuple_update_accessor_eq_assist upd ac v f v' x ⟷
     upd f v = v' ∧ ac v = x ∧ iso_tuple_update_accessor_cong_assist upd ac"

lemma update_accessor_congruence_foldE:
  assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
    and r: "r = r'" and v: "ac r' = v'"
    and f: "∧v. v' = v ==> f v = f' v"
  shows "upd f r = upd f' r'"
  using uac r v [symmetric]
  apply (subgoal_tac "upd (λx. f (ac r')) r' = upd (λx. f' (ac r')) r'")
   apply (simp add: iso_tuple_update_accessor_cong_assist_def)
  apply (simp add: f)
  done

lemma update_accessor_congruence_unfoldE:
  "iso_tuple_update_accessor_cong_assist upd ac ==>
    r = r' ==> ac r' = v' ==> (∧v. v = v' ==> f v = f' v) ==>
    upd f r = upd f' r'"
  apply (erule(2) update_accessor_congruence_foldE)
  apply simp
  done

lemma iso_tuple_update_accessor_cong_assist_id:
  "iso_tuple_update_accessor_cong_assist upd ac ==> upd id = id"
  by rule (simp add: iso_tuple_update_accessor_cong_assist_def)

lemma update_accessor_noopE:
  assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
    and ac: "f (ac x) = ac x"
  shows "upd f x = x"
  using uac
  by (simp add: ac iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
    cong: update_accessor_congruence_unfoldE [OF uac])

lemma update_accessor_noop_compE:
  assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
    and ac: "f (ac x) = ac x"
  shows "upd (g ∘ f) x = upd g x"
  by (simp add: ac cong: update_accessor_congruence_unfoldE[OF uac])

lemma update_accessor_cong_assist_idI:
  "iso_tuple_update_accessor_cong_assist id id"
  by (simp add: iso_tuple_update_accessor_cong_assist_def)

lemma update_accessor_cong_assist_triv:
  "iso_tuple_update_accessor_cong_assist upd ac ==>
    iso_tuple_update_accessor_cong_assist upd ac"
  by assumption

lemma update_accessor_accessor_eqE:
  "iso_tuple_update_accessor_eq_assist upd ac v f v' x ==> ac v = x"
  by (simp add: iso_tuple_update_accessor_eq_assist_def)

lemma update_accessor_updator_eqE:
  "iso_tuple_update_accessor_eq_assist upd ac v f v' x ==> upd f v = v'"
  by (simp add: iso_tuple_update_accessor_eq_assist_def)

lemma iso_tuple_update_accessor_eq_assist_idI:
  "v' = f v ==> iso_tuple_update_accessor_eq_assist id id v f v' v"
  by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)

lemma iso_tuple_update_accessor_eq_assist_triv:
  "iso_tuple_update_accessor_eq_assist upd ac v f v' x ==>
    iso_tuple_update_accessor_eq_assist upd ac v f v' x"
  by assumption

lemma iso_tuple_update_accessor_cong_from_eq:
  "iso_tuple_update_accessor_eq_assist upd ac v f v' x ==>
    iso_tuple_update_accessor_cong_assist upd ac"
  by (simp add: iso_tuple_update_accessor_eq_assist_def)

lemma iso_tuple_surjective_proof_assistI:
  "f x = y ==> iso_tuple_surjective_proof_assist x y f"
  by (simp add: iso_tuple_surjective_proof_assist_def)

lemma iso_tuple_surjective_proof_assist_idE:
  "iso_tuple_surjective_proof_assist x y id ==> x = y"
  by (simp add: iso_tuple_surjective_proof_assist_def)

locale isomorphic_tuple =
  fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
  assumes repr_inv: "∧x. abst isom (repr isom x) = x"
    and abst_inv: "∧y. repr isom (abst isom y) = y"
begin

lemma repr_inj: "repr isom x = repr isom y ⟷ x = y"
  by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"]
    simp add: repr_inv)

lemma abst_inj: "abst isom x = abst isom y ⟷ x = y"
  by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"]
    simp add: abst_inv)

lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj

lemma iso_tuple_access_update_fst_fst:
  "f ∘ h g = j ∘ f ==>
    (f ∘ iso_tuple_fst isom) ∘ (iso_tuple_fst_update isom ∘ h) g =
      j ∘ (f ∘ iso_tuple_fst isom)"
  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps
    fun_eq_iff)

lemma iso_tuple_access_update_snd_snd:
  "f ∘ h g = j ∘ f ==>
    (f ∘ iso_tuple_snd isom) ∘ (iso_tuple_snd_update isom ∘ h) g =
      j ∘ (f ∘ iso_tuple_snd isom)"
  by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps
    fun_eq_iff)

lemma iso_tuple_access_update_fst_snd:
  "(f ∘ iso_tuple_fst isom) ∘ (iso_tuple_snd_update isom ∘ h) g =
    id ∘ (f ∘ iso_tuple_fst isom)"
  by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps
    fun_eq_iff)

lemma iso_tuple_access_update_snd_fst:
  "(f ∘ iso_tuple_snd isom) ∘ (iso_tuple_fst_update isom ∘ h) g =
    id ∘ (f ∘ iso_tuple_snd isom)"
  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps
    fun_eq_iff)

lemma iso_tuple_update_swap_fst_fst:
  "h f ∘ j g = j g ∘ h f ==>
    (iso_tuple_fst_update isom ∘ h) f ∘ (iso_tuple_fst_update isom ∘ j) g =
      (iso_tuple_fst_update isom ∘ j) g ∘ (iso_tuple_fst_update isom ∘ h) f"
  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)

lemma iso_tuple_update_swap_snd_snd:
  "h f ∘ j g = j g ∘ h f ==>
    (iso_tuple_snd_update isom ∘ h) f ∘ (iso_tuple_snd_update isom ∘ j) g =
      (iso_tuple_snd_update isom ∘ j) g ∘ (iso_tuple_snd_update isom ∘ h) f"
  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)

lemma iso_tuple_update_swap_fst_snd:
  "(iso_tuple_snd_update isom ∘ h) f ∘ (iso_tuple_fst_update isom ∘ j) g =
    (iso_tuple_fst_update isom ∘ j) g ∘ (iso_tuple_snd_update isom ∘ h) f"
  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def
    simps fun_eq_iff)

lemma iso_tuple_update_swap_snd_fst:
  "(iso_tuple_fst_update isom ∘ h) f ∘ (iso_tuple_snd_update isom ∘ j) g =
    (iso_tuple_snd_update isom ∘ j) g ∘ (iso_tuple_fst_update isom ∘ h) f"
  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps
    fun_eq_iff)

lemma iso_tuple_update_compose_fst_fst:
  "h f ∘ j g = k (f ∘ g) ==>
    (iso_tuple_fst_update isom ∘ h) f ∘ (iso_tuple_fst_update isom ∘ j) g =
      (iso_tuple_fst_update isom ∘ k) (f ∘ g)"
  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)

lemma iso_tuple_update_compose_snd_snd:
  "h f ∘ j g = k (f ∘ g) ==>
    (iso_tuple_snd_update isom ∘ h) f ∘ (iso_tuple_snd_update isom ∘ j) g =
      (iso_tuple_snd_update isom ∘ k) (f ∘ g)"
  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)

lemma iso_tuple_surjective_proof_assist_step:
  "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom ∘ f) ==>
    iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom ∘ f) ==>
    iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f"
  by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps
    iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def)

lemma iso_tuple_fst_update_accessor_cong_assist:
  assumes "iso_tuple_update_accessor_cong_assist f g"
  shows "iso_tuple_update_accessor_cong_assist
    (iso_tuple_fst_update isom ∘ f) (g ∘ iso_tuple_fst isom)"
proof -
  from assms have "f id = id"
    by (rule iso_tuple_update_accessor_cong_assist_id)
  with assms show ?thesis
    by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
      iso_tuple_fst_update_def iso_tuple_fst_def)
qed

lemma iso_tuple_snd_update_accessor_cong_assist:
  assumes "iso_tuple_update_accessor_cong_assist f g"
  shows "iso_tuple_update_accessor_cong_assist
    (iso_tuple_snd_update isom ∘ f) (g ∘ iso_tuple_snd isom)"
proof -
  from assms have "f id = id"
    by (rule iso_tuple_update_accessor_cong_assist_id)
  with assms show ?thesis
    by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
      iso_tuple_snd_update_def iso_tuple_snd_def)
qed

lemma iso_tuple_fst_update_accessor_eq_assist:
  assumes "iso_tuple_update_accessor_eq_assist f g a u a' v"
  shows "iso_tuple_update_accessor_eq_assist
    (iso_tuple_fst_update isom ∘ f) (g ∘ iso_tuple_fst isom)
    (iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v"
proof -
  from assms have "f id = id"
    by (auto simp add: iso_tuple_update_accessor_eq_assist_def
      intro: iso_tuple_update_accessor_cong_assist_id)
  with assms show ?thesis
    by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
      iso_tuple_fst_update_def iso_tuple_fst_def
      iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
qed

lemma iso_tuple_snd_update_accessor_eq_assist:
  assumes "iso_tuple_update_accessor_eq_assist f g b u b' v"
  shows "iso_tuple_update_accessor_eq_assist
    (iso_tuple_snd_update isom ∘ f) (g ∘ iso_tuple_snd isom)
    (iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v"
proof -
  from assms have "f id = id"
    by (auto simp add: iso_tuple_update_accessor_eq_assist_def
      intro: iso_tuple_update_accessor_cong_assist_id)
  with assms show ?thesis
    by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
      iso_tuple_snd_update_def iso_tuple_snd_def
      iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
qed

lemma iso_tuple_cons_conj_eqI:
  "a = c ∧ b = d ∧ P ⟷ Q ==>
    iso_tuple_cons isom a b = iso_tuple_cons isom c d ∧ P ⟷ Q"
  by (clarsimp simp: iso_tuple_cons_def simps)

lemmas intros =
  iso_tuple_access_update_fst_fst
  iso_tuple_access_update_snd_snd
  iso_tuple_access_update_fst_snd
  iso_tuple_access_update_snd_fst
  iso_tuple_update_swap_fst_fst
  iso_tuple_update_swap_snd_snd
  iso_tuple_update_swap_fst_snd
  iso_tuple_update_swap_snd_fst
  iso_tuple_update_compose_fst_fst
  iso_tuple_update_compose_snd_snd
  iso_tuple_surjective_proof_assist_step
  iso_tuple_fst_update_accessor_eq_assist
  iso_tuple_snd_update_accessor_eq_assist
  iso_tuple_fst_update_accessor_cong_assist
  iso_tuple_snd_update_accessor_cong_assist
  iso_tuple_cons_conj_eqI

end

lemma isomorphic_tuple_intro:
  fixes repr abst
  assumes repr_inj: "∧x y. repr x = repr y ⟷ x = y"
    and abst_inv: "∧z. repr (abst z) = z"
    and v: "v ≡ Tuple_Isomorphism repr abst"
  shows "isomorphic_tuple v"
proof
  fix x have "repr (abst (repr x)) = repr x"
    by (simp add: abst_inv)
  then show "Record.abst v (Record.repr v x) = x"
    by (simp add: v repr_inj)
next
  fix y
  show "Record.repr v (Record.abst v y) = y"
    by (simp add: v) (fact abst_inv)
qed

definition
  "tuple_iso_tuple ≡ Tuple_Isomorphism id id"

lemma tuple_iso_tuple:
  "isomorphic_tuple tuple_iso_tuple"
  by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def)

lemma refl_conj_eq: "Q = R ==> P ∧ Q ⟷ P ∧ R"
  by simp

lemma iso_tuple_UNIV_I: "x ∈ UNIV ≡ True"
  by simp

lemma iso_tuple_True_simp: "(True ==> PROP P) ≡ PROP P"
  by simp

lemma prop_subst: "s = t ==> PROP P t ==> PROP P s"
  by simp

lemma K_record_comp: "(λx. c) ∘ f = (λx. c)"
  by (simp add: comp_def)


subsection ‹Concrete record syntax›

nonterminal
  ident and
  field_type and
  field_types and
  field and
  fields and
  field_update and
  field_updates

open_bundle record_syntax
begin

syntax
  "_constify"           :: "id => ident"                        (‹_›)
  "_constify"           :: "longid => ident"                    (‹_›)

  "_field_type"         :: "ident => type => field_type"        (‹(‹indent=2 notation=‹infix field type››_ ::/ _)›)
  ""                    :: "field_type => field_types"          (‹_›)
  "_field_types"        :: "field_type => field_types => field_types"    (‹_,/ _›)
  "_record_type"        :: "field_types => type"                (‹(‹indent=3 notation=‹mixfix record type››(_))›)
  "_record_type_scheme" :: "field_types => type => type"        (‹(‹indent=3 notation=‹mixfix record type››(_,/ (‹indent=2 notation=‹infix more type››… ::/ _)))›)

  "_field"              :: "ident => 'a => field"               (‹(‹indent=2 notation=‹infix field value››(‹open_block markup=‹const››_) =/ _)›)
  ""                    :: "field => fields"                    (‹_›)
  "_fields"             :: "field => fields => fields"          (‹_,/ _›)
  "_record"             :: "fields => 'a"                       (‹(‹indent=3 notation=‹mixfix record value››(_))›)
  "_record_scheme"      :: "fields => 'a => 'a"                 (‹(‹indent=3 notation=‹mixfix record value››(_,/ (‹indent=2 notation=‹infix more value››… =/ _)))›)

  "_field_update"       :: "ident => 'a => field_update"        (‹(‹indent=2 notation=‹infix field update››(‹open_block markup=‹const››_) :=/ _)›)
  ""                    :: "field_update => field_updates"      (‹_›)
  "_field_updates"      :: "field_update => field_updates => field_updates"  (‹_,/ _›)
  "_record_update"      :: "'a => field_updates => 'b"          (‹(‹open_block notation=‹mixfix record update››_/(3(_)))› [900, 0] 900)

syntax (ASCII)
  "_record_type"        :: "field_types => type"                (‹(‹indent=3 notation=‹mixfix record type››'(| _ |'))›)
  "_record_type_scheme" :: "field_types => type => type"        (‹(‹indent=3 notation=‹mixfix record type››'(| _,/ (‹indent=2 notation=‹infix more type››... ::/ _) |'))›)
  "_record"             :: "fields => 'a"                       (‹(‹indent=3 notation=‹mixfix record value››'(| _ |'))›)
  "_record_scheme"      :: "fields => 'a => 'a"                 (‹(‹indent=3 notation=‹mixfix record value››'(| _,/ (‹indent=2 notation=‹infix more value››... =/ _) |'))›)
  "_record_update"      :: "'a => field_updates => 'b"          (‹(‹open_block notation=‹mixfix record update››_/(3'(| _ |')))› [900, 0] 900)

end


subsection ‹Record package›

ML_file ‹Tools/record.ML›

hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
  iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
  iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
  iso_tuple_update_accessor_eq_assist tuple_iso_tuple

end