(*  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

*)

header {* Extensible records with structural subtyping *}

theory Record

imports Quickcheck_Narrowing

keywords "record" :: thy_decl

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 @{text "alpha (beta_update f

  rec) = alpha rec"} for distinct fields alpha and beta of some record

  rec with n fields. There are @{text "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

  @{text "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 @{text "'a"}, @{text "'b"}, @{text "'c"}

  and @{text "'d"} might be introduced as isomorphic to @{text "'a \<times>

  ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to @{text "('a \<times>

  'b) \<times> ('c \<times> '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 @{text

  "fst_update"} and @{text "snd_update"} function. Furthermore, we can

  prove the access/update theorem in O(log(n)) steps by using simple

  rewrites on fst, snd, @{text "fst_update"} and @{text "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 @{text

  "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 @{text "O(log(n)^2)"}

  time as the intermediate terms are @{text "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: @{text

  "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"}

  and @{text "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 @{text "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 ('a, 'b, 'c) tuple_isomorphism =

  Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"

primrec

  repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where

  "repr (Tuple_Isomorphism r a) = r"

primrec

  abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where

  "abst (Tuple_Isomorphism r a) = a"

definition

  iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where

  "iso_tuple_fst isom = fst \<circ> repr isom"

definition

  iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where

  "iso_tuple_snd isom = snd \<circ> repr isom"

definition

  iso_tuple_fst_update ::

    "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where

  "iso_tuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"

definition

  iso_tuple_snd_update ::

    "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where

  "iso_tuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"

definition

  iso_tuple_cons ::

    "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where

  "iso_tuple_cons isom = curry (abst isom)"

subsection {* Logical infrastructure for records *}

definition

  iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where

  "iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"

definition

  iso_tuple_update_accessor_cong_assist ::

    "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where

  "iso_tuple_update_accessor_cong_assist upd ac \<longleftrightarrow>

     (\<forall>f v. upd (\<lambda>x. f (ac v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"

definition

  iso_tuple_update_accessor_eq_assist ::

    "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where

  "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<longleftrightarrow>

     upd f v = v' \<and> ac v = x \<and> 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: "\<And>v. v' = v \<Longrightarrow> f v = f' v"

  shows "upd f r = upd f' r'"

  using uac r v [symmetric]

  apply (subgoal_tac "upd (\<lambda>x. f (ac r')) r' = upd (\<lambda>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 \<Longrightarrow>

    r = r' \<Longrightarrow> ac r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v) \<Longrightarrow>

    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 \<Longrightarrow> 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 \<circ> 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 \<Longrightarrow>

    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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow>

    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 \<Longrightarrow>

    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 \<Longrightarrow> 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 \<Longrightarrow> x = y"

  by (simp add: iso_tuple_surjective_proof_assist_def)

locale isomorphic_tuple =

  fixes isom :: "('a, 'b, 'c) tuple_isomorphism"

  assumes repr_inv: "\<And>x. abst isom (repr isom x) = x"

    and abst_inv: "\<And>y. repr isom (abst isom y) = y"

begin

lemma repr_inj: "repr isom x = repr isom y \<longleftrightarrow> 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 \<longleftrightarrow> 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 o h g = j o f \<Longrightarrow>

    (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g =

      j o (f o 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 o h g = j o f \<Longrightarrow>

    (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g =

      j o (f o 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 o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g =

    id o (f o 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 o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g =

    id o (f o 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 o j g = j g o h f \<Longrightarrow>

    (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g =

      (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o 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 o j g = j g o h f \<Longrightarrow>

    (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g =

      (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o 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 o h) f o (iso_tuple_fst_update isom o j) g =

    (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o 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 o h) f o (iso_tuple_snd_update isom o j) g =

    (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o 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 o j g = k (f o g) \<Longrightarrow>

    (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g =

      (iso_tuple_fst_update isom o k) (f o g)"

  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)

lemma iso_tuple_update_compose_snd_snd:

  "h f o j g = k (f o g) \<Longrightarrow>

    (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g =

      (iso_tuple_snd_update isom o k) (f o 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 o f) \<Longrightarrow>

    iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f) \<Longrightarrow>

    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 o f) (g o 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 o f) (g o 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 o f) (g o 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 o f) (g o 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 \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>

    iso_tuple_cons isom a b = iso_tuple_cons isom c d \<and> P \<longleftrightarrow> 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: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"

    and abst_inv: "\<And>z. repr (abst z) = z"

    and v: "v \<equiv> 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 \<equiv> 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 \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"

  by simp

lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"

  by simp

lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"

  by simp

lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"

  by simp

lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>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

syntax

  "_constify"           :: "id => ident"                        ("_")

  "_constify"           :: "longid => ident"                    ("_")

  "_field_type"         :: "ident => type => field_type"        ("(2_ ::/ _)")

  ""                    :: "field_type => field_types"          ("_")

  "_field_types"        :: "field_type => field_types => field_types"    ("_,/ _")

  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")

  "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")

  "_field"              :: "ident => 'a => field"               ("(2_ =/ _)")

  ""                    :: "field => fields"                    ("_")

  "_fields"             :: "field => fields => fields"          ("_,/ _")

  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")

  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")

  "_field_update"       :: "ident => 'a => field_update"        ("(2_ :=/ _)")

  ""                    :: "field_update => field_updates"      ("_")

  "_field_updates"      :: "field_update => field_updates => field_updates"  ("_,/ _")

  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)

syntax (xsymbols)

  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")

  "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")

  "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")

  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")

  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)

subsection {* Record package *}

ML_file "Tools/record.ML" setup Record.setup

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