Initial response to feedback from Norbert, Makarius on record patch
As Norbert recommended, the IsTuple.thy and istuple_support.ML files
have been integrated into Record.thy and record.ML. I haven't merged
the structures - record.ML now contains Record and IsTupleSupport.
Some of the cosmetic changes Makarius requested have been made,
including renaming variables with camel-case and run-together names
and removing the tab character from the Author: line. Constants are
defined with definition rather than constdefs. The split_ex_prf
inner function has been cleaned up.
--- a/src/HOL/IsTuple.thy Tue Sep 22 13:52:19 2009 +1000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,389 +0,0 @@
-(* Title: HOL/IsTuple.thy
- Author: Thomas Sewell, NICTA
-*)
-
-header {* Operators on types isomorphic to tuples *}
-
-theory IsTuple imports Product_Type
-
-uses ("Tools/istuple_support.ML")
-
-begin
-
-text {*
-This module provides operators and lemmas for types isomorphic to tuples.
-These types are used in defining efficient records. 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 \<times> ('b \<times> ('c \<times> 'd)). If we balance the tuple tree to
-('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 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. The 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 analagous
-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 analagous traversal, we define the functions seen below:
-istuple_fst, istuple_snd, istuple_fst_update and istuple_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 rule assumption. All rules are
-structured to aid net matching, using either a point-free form or an
-encapsulating predicate.
-*}
-
-typedef ('a, 'b, 'c) tuple_isomorphism
- = "UNIV :: (('a \<Rightarrow> ('b \<times> 'c)) \<times> (('b \<times> 'c) \<Rightarrow> 'a)) set"
- by simp
-
-constdefs
- "TupleIsomorphism repr abst \<equiv> Abs_tuple_isomorphism (repr, abst)"
-
-constdefs
- istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b"
- "istuple_fst isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in fst \<circ> repr"
- istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c"
- "istuple_snd isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in snd \<circ> repr"
- istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)"
- "istuple_fst_update isom \<equiv>
- let (repr, abst) = Rep_tuple_isomorphism isom in
- (\<lambda>f v. abst (f (fst (repr v)), snd (repr v)))"
- istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)"
- "istuple_snd_update isom \<equiv>
- let (repr, abst) = Rep_tuple_isomorphism isom in
- (\<lambda>f v. abst (fst (repr v), f (snd (repr v))))"
- istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a"
- "istuple_cons isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in curry abst"
-
-text {*
-These predicates are used in the introduction rule set to constrain
-matching appropriately. The elimination rules for them produce the
-desired theorems once they are proven. The final introduction rules are
-used when no further rules from the introduction rule set can apply.
-*}
-
-constdefs
- istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
- "istuple_surjective_proof_assist x y f \<equiv> f x = y"
- istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a))
- \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
- "istuple_update_accessor_cong_assist upd acc
- \<equiv> (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v)
- \<and> (\<forall>v. upd id v = v)"
- istuple_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"
- "istuple_update_accessor_eq_assist upd acc v f v' x
- \<equiv> upd f v = v' \<and> acc v = x
- \<and> istuple_update_accessor_cong_assist upd acc"
-
-lemma update_accessor_congruence_foldE:
- assumes uac: "istuple_update_accessor_cong_assist upd acc"
- and r: "r = r'" and v: "acc 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 (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
- apply (simp add: istuple_update_accessor_cong_assist_def)
- apply (simp add: f)
- done
-
-lemma update_accessor_congruence_unfoldE:
- "\<lbrakk> istuple_update_accessor_cong_assist upd acc;
- r = r'; acc r' = v'; \<And>v. v = v' \<Longrightarrow> f v = f' v \<rbrakk>
- \<Longrightarrow> upd f r = upd f' r'"
- apply (erule(2) update_accessor_congruence_foldE)
- apply simp
- done
-
-lemma istuple_update_accessor_cong_assist_id:
- "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
- by (rule ext, simp add: istuple_update_accessor_cong_assist_def)
-
-lemma update_accessor_noopE:
- assumes uac: "istuple_update_accessor_cong_assist upd acc"
- and acc: "f (acc x) = acc x"
- shows "upd f x = x"
- using uac
- by (simp add: acc istuple_update_accessor_cong_assist_id[OF uac, unfolded id_def]
- cong: update_accessor_congruence_unfoldE[OF uac])
-
-lemma update_accessor_noop_compE:
- assumes uac: "istuple_update_accessor_cong_assist upd acc"
- assumes acc: "f (acc x) = acc x"
- shows "upd (g \<circ> f) x = upd g x"
- by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
-
-lemma update_accessor_cong_assist_idI:
- "istuple_update_accessor_cong_assist id id"
- by (simp add: istuple_update_accessor_cong_assist_def)
-
-lemma update_accessor_cong_assist_triv:
- "istuple_update_accessor_cong_assist upd acc
- \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
- by assumption
-
-lemma update_accessor_accessor_eqE:
- "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> acc v = x"
- by (simp add: istuple_update_accessor_eq_assist_def)
-
-lemma update_accessor_updator_eqE:
- "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> upd f v = v'"
- by (simp add: istuple_update_accessor_eq_assist_def)
-
-lemma istuple_update_accessor_eq_assist_idI:
- "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
- by (simp add: istuple_update_accessor_eq_assist_def
- update_accessor_cong_assist_idI)
-
-lemma istuple_update_accessor_eq_assist_triv:
- "istuple_update_accessor_eq_assist upd acc v f v' x
- \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
- by assumption
-
-lemma istuple_update_accessor_cong_from_eq:
- "istuple_update_accessor_eq_assist upd acc v f v' x
- \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
- by (simp add: istuple_update_accessor_eq_assist_def)
-
-lemma o_eq_dest:
- "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
- apply (clarsimp simp: o_def)
- apply (erule fun_cong)
- done
-
-lemma o_eq_elim:
- "\<lbrakk> a o b = c o d; \<lbrakk> \<And>v. a (b v) = c (d v) \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
- apply (erule meta_mp)
- apply (erule o_eq_dest)
- done
-
-lemma istuple_surjective_proof_assistI:
- "f x = y \<Longrightarrow>
- istuple_surjective_proof_assist x y f"
- by (simp add: istuple_surjective_proof_assist_def)
-
-lemma istuple_surjective_proof_assist_idE:
- "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
- by (simp add: istuple_surjective_proof_assist_def)
-
-locale isomorphic_tuple =
- fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
- and repr and abst
- defines "repr \<equiv> fst (Rep_tuple_isomorphism isom)"
- defines "abst \<equiv> snd (Rep_tuple_isomorphism isom)"
- assumes repr_inv: "\<And>x. abst (repr x) = x"
- assumes abst_inv: "\<And>y. repr (abst y) = y"
-
-begin
-
-lemma repr_inj:
- "(repr x = repr y) = (x = y)"
- apply (rule iffI, simp_all)
- apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
- done
-
-lemma abst_inj:
- "(abst x = abst y) = (x = y)"
- apply (rule iffI, simp_all)
- apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
- done
-
-lemma split_Rep:
- "split f (Rep_tuple_isomorphism isom)
- = f repr abst"
- by (simp add: split_def repr_def abst_def)
-
-lemmas simps = Let_def split_Rep repr_inv abst_inv repr_inj abst_inj
-
-lemma istuple_access_update_fst_fst:
- "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
- (f o istuple_fst isom) o (istuple_fst_update isom o h) g
- = j o (f o istuple_fst isom)"
- by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
- intro!: ext elim!: o_eq_elim)
-
-lemma istuple_access_update_snd_snd:
- "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
- (f o istuple_snd isom) o (istuple_snd_update isom o h) g
- = j o (f o istuple_snd isom)"
- by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
- intro!: ext elim!: o_eq_elim)
-
-lemma istuple_access_update_fst_snd:
- "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
- = id o (f o istuple_fst isom)"
- by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
- intro!: ext elim!: o_eq_elim)
-
-lemma istuple_access_update_snd_fst:
- "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
- = id o (f o istuple_snd isom)"
- by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
- intro!: ext elim!: o_eq_elim)
-
-lemma istuple_update_swap_fst_fst:
- "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
- (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
- = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
- by (clarsimp simp: istuple_fst_update_def simps
- intro!: ext elim!: o_eq_elim)
-
-lemma istuple_update_swap_snd_snd:
- "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
- (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
- = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
- by (clarsimp simp: istuple_snd_update_def simps
- intro!: ext elim!: o_eq_elim)
-
-lemma istuple_update_swap_fst_snd:
- "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
- = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
- by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
- intro!: ext elim!: o_eq_elim)
-
-lemma istuple_update_swap_snd_fst:
- "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
- = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
- by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
- intro!: ext elim!: o_eq_elim)
-
-lemma istuple_update_compose_fst_fst:
- "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
- (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
- = (istuple_fst_update isom o k) (f o g)"
- by (fastsimp simp: istuple_fst_update_def simps
- intro!: ext elim!: o_eq_elim dest: fun_cong)
-
-lemma istuple_update_compose_snd_snd:
- "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
- (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
- = (istuple_snd_update isom o k) (f o g)"
- by (fastsimp simp: istuple_snd_update_def simps
- intro!: ext elim!: o_eq_elim dest: fun_cong)
-
-lemma istuple_surjective_proof_assist_step:
- "\<lbrakk> istuple_surjective_proof_assist v a (istuple_fst isom o f);
- istuple_surjective_proof_assist v b (istuple_snd isom o f) \<rbrakk>
- \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
- by (clarsimp simp: istuple_surjective_proof_assist_def simps
- istuple_fst_def istuple_snd_def istuple_cons_def)
-
-lemma istuple_fst_update_accessor_cong_assist:
- "istuple_update_accessor_cong_assist f g \<Longrightarrow>
- istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
- by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
- istuple_fst_update_def istuple_fst_def)
-
-lemma istuple_snd_update_accessor_cong_assist:
- "istuple_update_accessor_cong_assist f g \<Longrightarrow>
- istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
- by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
- istuple_snd_update_def istuple_snd_def)
-
-lemma istuple_fst_update_accessor_eq_assist:
- "istuple_update_accessor_eq_assist f g a u a' v \<Longrightarrow>
- istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
- (istuple_cons isom a b) u (istuple_cons isom a' b) v"
- by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def
- istuple_update_accessor_cong_assist_def istuple_cons_def simps)
-
-lemma istuple_snd_update_accessor_eq_assist:
- "istuple_update_accessor_eq_assist f g b u b' v \<Longrightarrow>
- istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
- (istuple_cons isom a b) u (istuple_cons isom a b') v"
- by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def
- istuple_update_accessor_cong_assist_def istuple_cons_def simps)
-
-lemma istuple_cons_conj_eqI:
- "\<lbrakk> (a = c \<and> b = d \<and> P) = Q \<rbrakk> \<Longrightarrow>
- (istuple_cons isom a b = istuple_cons isom c d \<and> P) = Q"
- by (clarsimp simp: istuple_cons_def simps)
-
-lemmas intros =
- istuple_access_update_fst_fst
- istuple_access_update_snd_snd
- istuple_access_update_fst_snd
- istuple_access_update_snd_fst
- istuple_update_swap_fst_fst
- istuple_update_swap_snd_snd
- istuple_update_swap_fst_snd
- istuple_update_swap_snd_fst
- istuple_update_compose_fst_fst
- istuple_update_compose_snd_snd
- istuple_surjective_proof_assist_step
- istuple_fst_update_accessor_eq_assist
- istuple_snd_update_accessor_eq_assist
- istuple_fst_update_accessor_cong_assist
- istuple_snd_update_accessor_cong_assist
- istuple_cons_conj_eqI
-
-end
-
-lemma isomorphic_tuple_intro:
- assumes repr_inj: "\<And>x y. (repr x = repr y) = (x = y)"
- and abst_inv: "\<And>z. repr (abst z) = z"
- shows "v \<equiv> TupleIsomorphism repr abst \<Longrightarrow> isomorphic_tuple v"
- apply (rule isomorphic_tuple.intro,
- simp_all add: TupleIsomorphism_def Abs_tuple_isomorphism_inverse
- tuple_isomorphism_def abst_inv)
- apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
- apply (simp add: abst_inv)
- done
-
-constdefs
- "tuple_istuple \<equiv> TupleIsomorphism id id"
-
-lemma tuple_istuple:
- "isomorphic_tuple tuple_istuple"
- by (simp add: isomorphic_tuple_intro[OF _ _ reflexive] tuple_istuple_def)
-
-lemma refl_conj_eq:
- "Q = R \<Longrightarrow> (P \<and> Q) = (P \<and> R)"
- by simp
-
-lemma meta_all_sameI:
- "(\<And>x. PROP P x \<equiv> PROP Q x) \<Longrightarrow> (\<And>x. PROP P x) \<equiv> (\<And>x. PROP Q x)"
- by simp
-
-lemma istuple_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
- by simp
-
-lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
- by simp
-
-use "Tools/istuple_support.ML";
-
-end
--- a/src/HOL/Record.thy Tue Sep 22 13:52:19 2009 +1000
+++ b/src/HOL/Record.thy Wed Sep 23 19:17:48 2009 +1000
@@ -1,11 +1,12 @@
(* Title: HOL/Record.thy
- Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
+ Authors: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
+ Thomas Sewell, NICTA
*)
header {* Extensible records with structural subtyping *}
theory Record
-imports Product_Type IsTuple
+imports Product_Type
uses ("Tools/record.ML")
begin
@@ -64,6 +65,402 @@
"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
+subsection {* Operators and lemmas for types isomorphic to tuples *}
+
+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 \<times> ('b \<times> ('c \<times> 'd)). If we balance the tuple tree to
+('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 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 analagous
+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 analagous traversal, we define the functions seen below:
+istuple_fst, istuple_snd, istuple_fst_update and istuple_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.
+*}
+
+typedef ('a, 'b, 'c) tuple_isomorphism
+ = "UNIV :: (('a \<Rightarrow> ('b \<times> 'c)) \<times> (('b \<times> 'c) \<Rightarrow> 'a)) set"
+ by simp
+
+definition
+ "TupleIsomorphism repr abst = Abs_tuple_isomorphism (repr, abst)"
+
+definition
+ istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+ "istuple_fst isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in fst \<circ> repr"
+
+definition
+ istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c"
+where
+ "istuple_snd isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in snd \<circ> repr"
+
+definition
+ istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)"
+where
+ "istuple_fst_update isom \<equiv>
+ let (repr, abst) = Rep_tuple_isomorphism isom in
+ (\<lambda>f v. abst (f (fst (repr v)), snd (repr v)))"
+
+definition
+ istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)"
+where
+ "istuple_snd_update isom \<equiv>
+ let (repr, abst) = Rep_tuple_isomorphism isom in
+ (\<lambda>f v. abst (fst (repr v), f (snd (repr v))))"
+
+definition
+ istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a"
+where
+ "istuple_cons isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in curry abst"
+
+text {*
+These predicates are used in the introduction rule set to constrain
+matching appropriately. The elimination rules for them produce the
+desired theorems once they are proven. The final introduction rules are
+used when no further rules from the introduction rule set can apply.
+*}
+
+definition
+ istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+where
+ "istuple_surjective_proof_assist x y f \<equiv> (f x = y)"
+
+definition
+ istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a))
+ \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+where
+ "istuple_update_accessor_cong_assist upd acc
+ \<equiv> (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v)
+ \<and> (\<forall>v. upd id v = v)"
+
+definition
+ istuple_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
+ "istuple_update_accessor_eq_assist upd acc v f v' x
+ \<equiv> upd f v = v' \<and> acc v = x
+ \<and> istuple_update_accessor_cong_assist upd acc"
+
+lemma update_accessor_congruence_foldE:
+ assumes uac: "istuple_update_accessor_cong_assist upd acc"
+ and r: "r = r'" and v: "acc 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 (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
+ apply (simp add: istuple_update_accessor_cong_assist_def)
+ apply (simp add: f)
+ done
+
+lemma update_accessor_congruence_unfoldE:
+ "\<lbrakk> istuple_update_accessor_cong_assist upd acc;
+ r = r'; acc r' = v'; \<And>v. v = v' \<Longrightarrow> f v = f' v \<rbrakk>
+ \<Longrightarrow> upd f r = upd f' r'"
+ apply (erule(2) update_accessor_congruence_foldE)
+ apply simp
+ done
+
+lemma istuple_update_accessor_cong_assist_id:
+ "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
+ by (rule ext, simp add: istuple_update_accessor_cong_assist_def)
+
+lemma update_accessor_noopE:
+ assumes uac: "istuple_update_accessor_cong_assist upd acc"
+ and acc: "f (acc x) = acc x"
+ shows "upd f x = x"
+ using uac
+ by (simp add: acc istuple_update_accessor_cong_assist_id[OF uac, unfolded id_def]
+ cong: update_accessor_congruence_unfoldE[OF uac])
+
+lemma update_accessor_noop_compE:
+ assumes uac: "istuple_update_accessor_cong_assist upd acc"
+ assumes acc: "f (acc x) = acc x"
+ shows "upd (g \<circ> f) x = upd g x"
+ by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
+
+lemma update_accessor_cong_assist_idI:
+ "istuple_update_accessor_cong_assist id id"
+ by (simp add: istuple_update_accessor_cong_assist_def)
+
+lemma update_accessor_cong_assist_triv:
+ "istuple_update_accessor_cong_assist upd acc
+ \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
+ by assumption
+
+lemma update_accessor_accessor_eqE:
+ "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> acc v = x"
+ by (simp add: istuple_update_accessor_eq_assist_def)
+
+lemma update_accessor_updator_eqE:
+ "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> upd f v = v'"
+ by (simp add: istuple_update_accessor_eq_assist_def)
+
+lemma istuple_update_accessor_eq_assist_idI:
+ "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
+ by (simp add: istuple_update_accessor_eq_assist_def
+ update_accessor_cong_assist_idI)
+
+lemma istuple_update_accessor_eq_assist_triv:
+ "istuple_update_accessor_eq_assist upd acc v f v' x
+ \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
+ by assumption
+
+lemma istuple_update_accessor_cong_from_eq:
+ "istuple_update_accessor_eq_assist upd acc v f v' x
+ \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
+ by (simp add: istuple_update_accessor_eq_assist_def)
+
+lemma o_eq_dest:
+ "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
+ apply (clarsimp simp: o_def)
+ apply (erule fun_cong)
+ done
+
+lemma o_eq_elim:
+ "\<lbrakk> a o b = c o d; \<lbrakk> \<And>v. a (b v) = c (d v) \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
+ apply (erule meta_mp)
+ apply (erule o_eq_dest)
+ done
+
+lemma istuple_surjective_proof_assistI:
+ "f x = y \<Longrightarrow>
+ istuple_surjective_proof_assist x y f"
+ by (simp add: istuple_surjective_proof_assist_def)
+
+lemma istuple_surjective_proof_assist_idE:
+ "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
+ by (simp add: istuple_surjective_proof_assist_def)
+
+locale isomorphic_tuple =
+ fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
+ and repr and abst
+ defines "repr \<equiv> fst (Rep_tuple_isomorphism isom)"
+ defines "abst \<equiv> snd (Rep_tuple_isomorphism isom)"
+ assumes repr_inv: "\<And>x. abst (repr x) = x"
+ assumes abst_inv: "\<And>y. repr (abst y) = y"
+
+begin
+
+lemma repr_inj:
+ "(repr x = repr y) = (x = y)"
+ apply (rule iffI, simp_all)
+ apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
+ done
+
+lemma abst_inj:
+ "(abst x = abst y) = (x = y)"
+ apply (rule iffI, simp_all)
+ apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
+ done
+
+lemma split_Rep:
+ "split f (Rep_tuple_isomorphism isom)
+ = f repr abst"
+ by (simp add: split_def repr_def abst_def)
+
+lemmas simps = Let_def split_Rep repr_inv abst_inv repr_inj abst_inj
+
+lemma istuple_access_update_fst_fst:
+ "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
+ (f o istuple_fst isom) o (istuple_fst_update isom o h) g
+ = j o (f o istuple_fst isom)"
+ by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
+ intro!: ext elim!: o_eq_elim)
+
+lemma istuple_access_update_snd_snd:
+ "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
+ (f o istuple_snd isom) o (istuple_snd_update isom o h) g
+ = j o (f o istuple_snd isom)"
+ by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
+ intro!: ext elim!: o_eq_elim)
+
+lemma istuple_access_update_fst_snd:
+ "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
+ = id o (f o istuple_fst isom)"
+ by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
+ intro!: ext elim!: o_eq_elim)
+
+lemma istuple_access_update_snd_fst:
+ "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
+ = id o (f o istuple_snd isom)"
+ by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
+ intro!: ext elim!: o_eq_elim)
+
+lemma istuple_update_swap_fst_fst:
+ "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
+ (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
+ = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
+ by (clarsimp simp: istuple_fst_update_def simps
+ intro!: ext elim!: o_eq_elim)
+
+lemma istuple_update_swap_snd_snd:
+ "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
+ (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
+ = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
+ by (clarsimp simp: istuple_snd_update_def simps
+ intro!: ext elim!: o_eq_elim)
+
+lemma istuple_update_swap_fst_snd:
+ "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
+ = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
+ by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
+ intro!: ext elim!: o_eq_elim)
+
+lemma istuple_update_swap_snd_fst:
+ "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
+ = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
+ by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
+ intro!: ext elim!: o_eq_elim)
+
+lemma istuple_update_compose_fst_fst:
+ "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
+ (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
+ = (istuple_fst_update isom o k) (f o g)"
+ by (fastsimp simp: istuple_fst_update_def simps
+ intro!: ext elim!: o_eq_elim dest: fun_cong)
+
+lemma istuple_update_compose_snd_snd:
+ "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
+ (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
+ = (istuple_snd_update isom o k) (f o g)"
+ by (fastsimp simp: istuple_snd_update_def simps
+ intro!: ext elim!: o_eq_elim dest: fun_cong)
+
+lemma istuple_surjective_proof_assist_step:
+ "\<lbrakk> istuple_surjective_proof_assist v a (istuple_fst isom o f);
+ istuple_surjective_proof_assist v b (istuple_snd isom o f) \<rbrakk>
+ \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
+ by (clarsimp simp: istuple_surjective_proof_assist_def simps
+ istuple_fst_def istuple_snd_def istuple_cons_def)
+
+lemma istuple_fst_update_accessor_cong_assist:
+ "istuple_update_accessor_cong_assist f g \<Longrightarrow>
+ istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
+ by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
+ istuple_fst_update_def istuple_fst_def)
+
+lemma istuple_snd_update_accessor_cong_assist:
+ "istuple_update_accessor_cong_assist f g \<Longrightarrow>
+ istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
+ by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
+ istuple_snd_update_def istuple_snd_def)
+
+lemma istuple_fst_update_accessor_eq_assist:
+ "istuple_update_accessor_eq_assist f g a u a' v \<Longrightarrow>
+ istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
+ (istuple_cons isom a b) u (istuple_cons isom a' b) v"
+ by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def
+ istuple_update_accessor_cong_assist_def istuple_cons_def simps)
+
+lemma istuple_snd_update_accessor_eq_assist:
+ "istuple_update_accessor_eq_assist f g b u b' v \<Longrightarrow>
+ istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
+ (istuple_cons isom a b) u (istuple_cons isom a b') v"
+ by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def
+ istuple_update_accessor_cong_assist_def istuple_cons_def simps)
+
+lemma istuple_cons_conj_eqI:
+ "\<lbrakk> (a = c \<and> b = d \<and> P) = Q \<rbrakk> \<Longrightarrow>
+ (istuple_cons isom a b = istuple_cons isom c d \<and> P) = Q"
+ by (clarsimp simp: istuple_cons_def simps)
+
+lemmas intros =
+ istuple_access_update_fst_fst
+ istuple_access_update_snd_snd
+ istuple_access_update_fst_snd
+ istuple_access_update_snd_fst
+ istuple_update_swap_fst_fst
+ istuple_update_swap_snd_snd
+ istuple_update_swap_fst_snd
+ istuple_update_swap_snd_fst
+ istuple_update_compose_fst_fst
+ istuple_update_compose_snd_snd
+ istuple_surjective_proof_assist_step
+ istuple_fst_update_accessor_eq_assist
+ istuple_snd_update_accessor_eq_assist
+ istuple_fst_update_accessor_cong_assist
+ istuple_snd_update_accessor_cong_assist
+ istuple_cons_conj_eqI
+
+end
+
+lemma isomorphic_tuple_intro:
+ assumes repr_inj: "\<And>x y. (repr x = repr y) = (x = y)"
+ and abst_inv: "\<And>z. repr (abst z) = z"
+ shows "v \<equiv> TupleIsomorphism repr abst \<Longrightarrow> isomorphic_tuple v"
+ apply (rule isomorphic_tuple.intro,
+ simp_all add: TupleIsomorphism_def Abs_tuple_isomorphism_inverse
+ tuple_isomorphism_def abst_inv)
+ apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
+ apply (simp add: abst_inv)
+ done
+
+definition
+ "tuple_istuple \<equiv> TupleIsomorphism id id"
+
+lemma tuple_istuple:
+ "isomorphic_tuple tuple_istuple"
+ by (simp add: isomorphic_tuple_intro[OF _ _ reflexive] tuple_istuple_def)
+
+lemma refl_conj_eq:
+ "Q = R \<Longrightarrow> (P \<and> Q) = (P \<and> R)"
+ by simp
+
+lemma meta_all_sameI:
+ "(\<And>x. PROP P x \<equiv> PROP Q x) \<Longrightarrow> (\<And>x. PROP P x) \<equiv> (\<And>x. PROP Q x)"
+ by simp
+
+lemma istuple_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
+ by simp
+
+lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
+ by simp
+
use "Tools/record.ML"
setup Record.setup
--- a/src/HOL/Tools/istuple_support.ML Tue Sep 22 13:52:19 2009 +1000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,149 +0,0 @@
-(* Title: HOL/Tools/ntuple_support.ML
- Author: Thomas Sewell, NICTA
-
-Support for defining instances of tuple-like types and supplying
-introduction rules needed by the record package.
-*)
-
-
-signature ISTUPLE_SUPPORT =
-sig
- val add_istuple_type: bstring * string list -> (typ * typ) -> theory ->
- (term * term * theory);
-
- val mk_cons_tuple: term * term -> term;
- val dest_cons_tuple: term -> term * term;
-
- val istuple_intros_tac: theory -> int -> tactic;
-
- val named_cterm_instantiate: (string * cterm) list -> thm -> thm;
-end;
-
-structure IsTupleSupport : ISTUPLE_SUPPORT =
-struct
-
-val isomN = "_TupleIsom";
-val defN = "_def";
-
-val istuple_UNIV_I = @{thm "istuple_UNIV_I"};
-val istuple_True_simp = @{thm "istuple_True_simp"};
-
-val istuple_intro = @{thm "isomorphic_tuple_intro"};
-val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"});
-
-val constname = fst o dest_Const;
-val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple});
-
-val istuple_constN = constname @{term isomorphic_tuple};
-val istuple_consN = constname @{term istuple_cons};
-
-val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"});
-
-fun named_cterm_instantiate values thm = let
- fun match name (Var ((name', _), _)) = name = name'
- | match name _ = false;
- fun getvar name = case (find_first (match name)
- (OldTerm.term_vars (prop_of thm)))
- of SOME var => cterm_of (theory_of_thm thm) var
- | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
- in
- cterm_instantiate (map (apfst getvar) values) thm
- end;
-
-structure IsTupleThms = TheoryDataFun
-(
- type T = thm Symtab.table;
- val empty = Symtab.make [tuple_istuple];
- val copy = I;
- val extend = I;
- val merge = K (Symtab.merge Thm.eq_thm_prop);
-);
-
-fun do_typedef name repT alphas thy =
- let
- fun get_thms thy name =
- let
- val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT,
- Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name;
- val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp];
- in (map rewrite_rule [rep_inject, abs_inverse],
- Const (absN, repT --> absT), absT) end;
- in
- thy
- |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
- |-> (fn (name, _) => `(fn thy => get_thms thy name))
- end;
-
-fun mk_cons_tuple (left, right) = let
- val (leftT, rightT) = (fastype_of left, fastype_of right);
- val prodT = HOLogic.mk_prodT (leftT, rightT);
- val isomT = Type (tup_isom_typeN, [prodT, leftT, rightT]);
- in
- Const (istuple_consN, isomT --> leftT --> rightT --> prodT)
- $ Const (fst tuple_istuple, isomT) $ left $ right
- end;
-
-fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right)
- = if ic = istuple_consN then (left, right)
- else raise TERM ("dest_cons_tuple", [v])
- | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]);
-
-fun add_istuple_type (name, alphas) (leftT, rightT) thy =
-let
- val repT = HOLogic.mk_prodT (leftT, rightT);
-
- val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
- thy
- |> do_typedef name repT alphas
- ||> Sign.add_path name;
-
- (* construct a type and body for the isomorphism constant by
- instantiating the theorem to which the definition will be applied *)
- val intro_inst = rep_inject RS
- (named_cterm_instantiate [("abst", cterm_of typ_thy absC)]
- istuple_intro);
- val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
- val isomT = fastype_of body;
- val isomBind = Binding.name (name ^ isomN);
- val isom = Const (Sign.full_name typ_thy isomBind, isomT);
- val isom_spec = (name ^ isomN ^ defN, Logic.mk_equals (isom, body));
-
- val ([isom_def], cdef_thy) =
- typ_thy
- |> Sign.add_consts_i [Syntax.no_syn (isomBind, isomT)]
- |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
-
- val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
- val cons = Const (istuple_consN, isomT --> leftT --> rightT --> absT)
-
- val thm_thy =
- cdef_thy
- |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop
- (constname isom, istuple))
- |> Sign.parent_path;
-in
- (isom, cons $ isom, thm_thy)
-end;
-
-fun istuple_intros_tac thy = let
- val isthms = IsTupleThms.get thy;
- fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
- val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let
- val goal' = Envir.beta_eta_contract goal;
- val isom = case goal' of (Const tp $ (Const pr $ Const is))
- => if fst tp = "Trueprop" andalso fst pr = istuple_constN
- then Const is
- else err "unexpected goal predicate" goal'
- | _ => err "unexpected goal format" goal';
- val isthm = case Symtab.lookup isthms (constname isom) of
- SOME isthm => isthm
- | NONE => err "no thm found for constant" isom;
- in rtac isthm n end);
- in
- fn n => resolve_from_net_tac istuple_intros n
- THEN use_istuple_thm_tac n
- end;
-
-end;
-
-
--- a/src/HOL/Tools/record.ML Tue Sep 22 13:52:19 2009 +1000
+++ b/src/HOL/Tools/record.ML Wed Sep 23 19:17:48 2009 +1000
@@ -52,6 +52,146 @@
end;
+signature ISTUPLE_SUPPORT =
+sig
+ val add_istuple_type: bstring * string list -> (typ * typ) -> theory ->
+ (term * term * theory);
+
+ val mk_cons_tuple: term * term -> term;
+ val dest_cons_tuple: term -> term * term;
+
+ val istuple_intros_tac: theory -> int -> tactic;
+
+ val named_cterm_instantiate: (string * cterm) list -> thm -> thm;
+end;
+
+structure IsTupleSupport : ISTUPLE_SUPPORT =
+struct
+
+val isomN = "_TupleIsom";
+val defN = "_def";
+
+val istuple_UNIV_I = @{thm "istuple_UNIV_I"};
+val istuple_True_simp = @{thm "istuple_True_simp"};
+
+val istuple_intro = @{thm "isomorphic_tuple_intro"};
+val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"});
+
+val constname = fst o dest_Const;
+val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple});
+
+val istuple_constN = constname @{term isomorphic_tuple};
+val istuple_consN = constname @{term istuple_cons};
+
+val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"});
+
+fun named_cterm_instantiate values thm = let
+ fun match name (Var ((name', _), _)) = name = name'
+ | match name _ = false;
+ fun getvar name = case (find_first (match name)
+ (OldTerm.term_vars (prop_of thm)))
+ of SOME var => cterm_of (theory_of_thm thm) var
+ | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
+ in
+ cterm_instantiate (map (apfst getvar) values) thm
+ end;
+
+structure IsTupleThms = TheoryDataFun
+(
+ type T = thm Symtab.table;
+ val empty = Symtab.make [tuple_istuple];
+ val copy = I;
+ val extend = I;
+ val merge = K (Symtab.merge Thm.eq_thm_prop);
+);
+
+fun do_typedef name repT alphas thy =
+ let
+ fun get_thms thy name =
+ let
+ val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT,
+ Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name;
+ val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp];
+ in (map rewrite_rule [rep_inject, abs_inverse],
+ Const (absN, repT --> absT), absT) end;
+ in
+ thy
+ |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
+ |-> (fn (name, _) => `(fn thy => get_thms thy name))
+ end;
+
+fun mk_cons_tuple (left, right) = let
+ val (leftT, rightT) = (fastype_of left, fastype_of right);
+ val prodT = HOLogic.mk_prodT (leftT, rightT);
+ val isomT = Type (tup_isom_typeN, [prodT, leftT, rightT]);
+ in
+ Const (istuple_consN, isomT --> leftT --> rightT --> prodT)
+ $ Const (fst tuple_istuple, isomT) $ left $ right
+ end;
+
+fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right)
+ = if ic = istuple_consN then (left, right)
+ else raise TERM ("dest_cons_tuple", [v])
+ | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]);
+
+fun add_istuple_type (name, alphas) (leftT, rightT) thy =
+let
+ val repT = HOLogic.mk_prodT (leftT, rightT);
+
+ val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
+ thy
+ |> do_typedef name repT alphas
+ ||> Sign.add_path name;
+
+ (* construct a type and body for the isomorphism constant by
+ instantiating the theorem to which the definition will be applied *)
+ val intro_inst = rep_inject RS
+ (named_cterm_instantiate [("abst", cterm_of typ_thy absC)]
+ istuple_intro);
+ val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
+ val isomT = fastype_of body;
+ val isom_bind = Binding.name (name ^ isomN);
+ val isom = Const (Sign.full_name typ_thy isom_bind, isomT);
+ val isom_spec = (name ^ isomN ^ defN, Logic.mk_equals (isom, body));
+
+ val ([isom_def], cdef_thy) =
+ typ_thy
+ |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
+ |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
+
+ val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
+ val cons = Const (istuple_consN, isomT --> leftT --> rightT --> absT)
+
+ val thm_thy =
+ cdef_thy
+ |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop
+ (constname isom, istuple))
+ |> Sign.parent_path;
+in
+ (isom, cons $ isom, thm_thy)
+end;
+
+fun istuple_intros_tac thy = let
+ val isthms = IsTupleThms.get thy;
+ fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
+ val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let
+ val goal' = Envir.beta_eta_contract goal;
+ val isom = case goal' of (Const tp $ (Const pr $ Const is))
+ => if fst tp = "Trueprop" andalso fst pr = istuple_constN
+ then Const is
+ else err "unexpected goal predicate" goal'
+ | _ => err "unexpected goal format" goal';
+ val isthm = case Symtab.lookup isthms (constname isom) of
+ SOME isthm => isthm
+ | NONE => err "no thm found for constant" isom;
+ in rtac isthm n end);
+ in
+ fn n => resolve_from_net_tac istuple_intros n
+ THEN use_istuple_thm_tac n
+ end;
+
+end;
+
structure Record: RECORD =
struct
@@ -68,6 +208,7 @@
val o_assoc = @{thm "o_assoc"};
val id_apply = @{thm id_apply};
val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
+val Not_eq_iff = @{thm Not_eq_iff};
val refl_conj_eq = thm "refl_conj_eq";
val meta_all_sameI = thm "meta_all_sameI";
@@ -966,14 +1107,14 @@
val T = range_type (fastype_of f);
in mk_comp (Const ("Fun.id", T --> T)) f end;
-fun get_updfuns (upd $ _ $ t) = upd :: get_updfuns t
- | get_updfuns _ = [];
+fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
+ | get_upd_funs _ = [];
fun get_accupd_simps thy term defset intros_tac = let
val (acc, [body]) = strip_comb term;
val recT = domain_type (fastype_of acc);
- val updfuns = sort_distinct TermOrd.fast_term_ord
- (get_updfuns body);
+ val upd_funs = sort_distinct TermOrd.fast_term_ord
+ (get_upd_funs body);
fun get_simp upd = let
val T = domain_type (fastype_of upd);
val lhs = mk_comp acc (upd $ Free ("f", T));
@@ -987,7 +1128,7 @@
val dest = if is_sel_upd_pair thy acc upd
then o_eq_dest else o_eq_id_dest;
in standard (othm RS dest) end;
- in map get_simp updfuns end;
+ in map get_simp upd_funs end;
structure SymSymTab = Table(type key = string * string
val ord = prod_ord fast_string_ord fast_string_ord);
@@ -1009,26 +1150,26 @@
fun get_updupd_simps thy term defset intros_tac = let
val recT = fastype_of term;
- val updfuns = get_updfuns term;
+ val upd_funs = get_upd_funs term;
val cname = fst o dest_Const;
fun getswap u u' = get_updupd_simp thy defset intros_tac u u'
(cname u = cname u');
- fun buildswapstoeq upd [] swaps = swaps
- | buildswapstoeq upd (u::us) swaps = let
+ fun build_swaps_to_eq upd [] swaps = swaps
+ | build_swaps_to_eq upd (u::us) swaps = let
val key = (cname u, cname upd);
val newswaps = if SymSymTab.defined swaps key then swaps
else SymSymTab.insert (K true)
(key, getswap u upd) swaps;
in if cname u = cname upd then newswaps
- else buildswapstoeq upd us newswaps end;
- fun swapsneeded [] prev seen swaps = map snd (SymSymTab.dest swaps)
- | swapsneeded (u::us) prev seen swaps =
+ else build_swaps_to_eq upd us newswaps end;
+ fun swaps_needed [] prev seen swaps = map snd (SymSymTab.dest swaps)
+ | swaps_needed (u::us) prev seen swaps =
if Symtab.defined seen (cname u)
- then swapsneeded us prev seen
- (buildswapstoeq u prev swaps)
- else swapsneeded us (u::prev)
+ then swaps_needed us prev seen
+ (build_swaps_to_eq u prev swaps)
+ else swaps_needed us (u::prev)
(Symtab.insert (K true) (cname u, ()) seen) swaps;
- in swapsneeded updfuns [] Symtab.empty SymSymTab.empty end;
+ in swaps_needed upd_funs [] Symtab.empty SymSymTab.empty end;
val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
@@ -2222,14 +2363,13 @@
fun split_ex_prf () =
let
- val ss = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1];
- val [Pv] = OldTerm.term_vars (prop_of split_object);
- val cPv = cterm_of defs_thy Pv;
- val cP = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
- val so3 = cterm_instantiate ([(cPv, cP)]) split_object;
- val so4 = simplify ss so3;
+ val ss = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff];
+ val P_nm = fst (dest_Free P);
+ val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
+ val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
+ val so'' = simplify ss so';
in
- prove_standard [] split_ex_prop (fn prems => resolve_tac [so4] 1)
+ prove_standard [] split_ex_prop (fn prems => resolve_tac [so''] 1)
end;
val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;