Simplification of various aspects of the IsTuple component
of the new record package. Extensive documentation added in
IsTuple.thy - it should now be possible to figure out what's
going on from the sources supplied.
--- a/src/HOL/IsTuple.thy Thu Sep 10 15:18:43 2009 +1000
+++ b/src/HOL/IsTuple.thy Thu Sep 10 16:38:18 2009 +1000
@@ -1,20 +1,95 @@
+(* 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 type with n fields. There
+are n^2 such theorems, which is 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. 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. With a little
+thinking they can be presented as an introduction rule set rather than
+a rewrite rule set. This 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 applications.
+*}
+
+typedef ('a, 'b, 'c) tuple_isomorphism
+ = "UNIV :: (('a \<Rightarrow> ('b \<times> 'c)) \<times> (('b \<times> 'c) \<Rightarrow> 'a)) set"
+ by simp
+
constdefs
- istuple_fst :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> 'a \<Rightarrow> 'b"
- "istuple_fst isom \<equiv> (fst \<circ> isom)"
- istuple_snd :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> 'a \<Rightarrow> 'c"
- "istuple_snd isom \<equiv> (snd \<circ> isom)"
- istuple_fst_update :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> (('b \<times> 'c) \<Rightarrow> 'a)
- \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)"
- "istuple_fst_update isom inv \<equiv> \<lambda>f v. inv (f (fst (isom v)), snd (isom v))"
- istuple_snd_update :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> (('b \<times> 'c) \<Rightarrow> 'a)
- \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)"
- "istuple_snd_update isom inv \<equiv> \<lambda>f v. inv (fst (isom v), f (snd (isom v)))"
+ "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"
@@ -121,129 +196,137 @@
by (simp add: istuple_surjective_proof_assist_def)
locale isomorphic_tuple =
- fixes isom :: "'a \<Rightarrow> ('b \<times> 'c)" and inv :: "('b \<times> 'c) \<Rightarrow> 'a"
- and cons :: "'b \<Rightarrow> 'c \<Rightarrow> 'a"
- assumes isom_eq: "(isom x = isom y) = (x = y)"
- and inverse_inv: "isom (inv v) = v"
- and cons_def: "cons \<equiv> curry inv"
+ 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 inverse_isom:
- "(inv (isom v)) = v"
- by (rule iffD1 [OF isom_eq], simp add: inverse_inv)
-
-lemma inv_eq:
- "(inv x = inv y) = (x = y)"
- apply (rule iffI)
- apply (drule arg_cong[where f=isom])
- apply (simp add: inverse_inv)
- apply simp
+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
-lemmas simps = isom_eq inv_eq inverse_inv inverse_isom cons_def
+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 inv o h) g
+ (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 inv o h) g
+ (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 inv o h) g
+ "(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 inv o h) g
+ "(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 inv o h) f o (istuple_fst_update isom inv o j) g
- = (istuple_fst_update isom inv o j) g o (istuple_fst_update isom inv o h) f"
+ (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 inv o h) f o (istuple_snd_update isom inv o j) g
- = (istuple_snd_update isom inv o j) g o (istuple_snd_update isom inv o h) f"
+ (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 inv o h) f o (istuple_fst_update isom inv o j) g
- = (istuple_fst_update isom inv o j) g o (istuple_snd_update isom inv o h) f"
+ "(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 inv o h) f o (istuple_snd_update isom inv o j) g
- = (istuple_snd_update isom inv o j) g o (istuple_fst_update isom inv o h) f"
+ "(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 inv o h) f o (istuple_fst_update isom inv o j) g
- = (istuple_fst_update isom inv o k) (f o g)"
+ (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 inv o h) f o (istuple_snd_update isom inv o j) g
- = (istuple_snd_update isom inv o k) (f o g)"
+ (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 (cons a b) f"
+ \<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_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 inv o f) (g o istuple_fst isom)"
- by (simp add: istuple_update_accessor_cong_assist_def istuple_fst_update_def istuple_fst_def simps)
+ 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 inv o f) (g o istuple_snd isom)"
- by (simp add: istuple_update_accessor_cong_assist_def istuple_snd_update_def istuple_snd_def simps)
+ 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 inv o f) (g o istuple_fst isom)
- (cons a b) u (cons a' b) v"
- by (simp add: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def simps
- istuple_update_accessor_cong_assist_def)
+ 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 inv o f) (g o istuple_snd isom)
- (cons a b) u (cons a b') v"
- by (simp add: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def simps
- istuple_update_accessor_cong_assist_def)
+ 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 cons_conj_eqI:
+lemma istuple_cons_conj_eqI:
"\<lbrakk> (a = c \<and> b = d \<and> P) = Q \<rbrakk> \<Longrightarrow>
- (cons a b = cons c d \<and> P) = Q"
- by (simp add: simps)
+ (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
@@ -261,12 +344,27 @@
istuple_snd_update_accessor_eq_assist
istuple_fst_update_accessor_cong_assist
istuple_snd_update_accessor_cong_assist
- cons_conj_eqI
+ istuple_cons_conj_eqI
end
-interpretation tuple_automorphic: isomorphic_tuple "id" "id" "Pair"
- by (unfold_locales, simp_all add: curry_def)
+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)"
--- a/src/HOL/Record.thy Thu Sep 10 15:18:43 2009 +1000
+++ b/src/HOL/Record.thy Thu Sep 10 16:38:18 2009 +1000
@@ -1,5 +1,4 @@
(* Title: HOL/Record.thy
- ID: $Id: Record.thy,v 1.33 2007/12/19 15:32:12 schirmer Exp $
Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
*)
--- a/src/HOL/Tools/istuple_support.ML Thu Sep 10 15:18:43 2009 +1000
+++ b/src/HOL/Tools/istuple_support.ML Thu Sep 10 16:38:18 2009 +1000
@@ -1,7 +1,7 @@
(* Title: HOL/Tools/ntuple_support.ML
Author: Thomas Sewell, NICTA
-Support for defining instances of tuple-like types and extracting
+Support for defining instances of tuple-like types and supplying
introduction rules needed by the record package.
*)
@@ -9,82 +9,56 @@
signature ISTUPLE_SUPPORT =
sig
val add_istuple_type: bstring * string list -> (typ * typ) -> theory ->
- (term * theory);
- type tagged_net = ((string * int) * thm) Net.net;
-
- val get_istuple_intros: theory -> tagged_net;
+ (term * term * theory);
- val build_tagged_net: string -> thm list -> tagged_net;
- val resolve_from_tagged_net: tagged_net -> int -> tactic;
- val tag_thm_trace: thm list ref;
- val merge_tagged_nets: (tagged_net * tagged_net) -> tagged_net;
+ 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 consN = "_NTupleCons";
+val isomN = "_TupleIsom";
val defN = "_def";
-val istuple_UNIV_I = thm "istuple_UNIV_I";
-val istuple_True_simp = thm "istuple_True_simp";
+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 = thms "isomorphic_tuple.intros";
-
-val init_intros = thms "tuple_automorphic.intros";
-
-type tagged_net = ((string * int) * thm) Net.net;
+val istuple_intro = @{thm "isomorphic_tuple_intro"};
+val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"});
-(* broadly similar to the use of nets in Tactic.resolve_from_net_tac.
- the tag strings identify which group of theorems a theorem in the
- net belongs to. *)
-fun build_tagged_net tag thms = let
- fun add_to_net thm (i, net) =
- (i + 1, Net.insert_term (K false) (concl_of thm, ((tag, i), thm)) net);
- val (n, net) = fold add_to_net thms (0, Net.empty);
- in net end;
+val constname = fst o dest_Const;
+val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple});
-val tag_thm_trace = ref ([] : thm list);
+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"});
-(* we check here that only theorems from a single group are being
- selected for unification, and that there are no duplicates. this
- is a good test that the net is doing its job, picking exactly the
- appropriate rules rather than overapproximating. *)
-fun tagged_thms_check t xs = let
- val tags = sort_distinct string_ord (map (fst o fst) xs);
- val ids = sort_distinct int_ord (map (snd o fst) xs);
- val thms = map snd xs;
-in
- if length tags > 1
- then (tag_thm_trace := t :: thms;
- raise THM ("tag mismatch " ^ hd tags ^ ", " ^ nth tags 1, 1, t :: thms))
- else if length ids < length xs
- then (tag_thm_trace := t :: thms;
- raise THM ("tag match duplicate id ", 1, t :: thms))
- else ()
-end;
+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;
-fun resolve_from_tagged_net net i t =
- SUBGOAL (fn (prem, i) => let
- val options = Net.unify_term net (Logic.strip_assums_concl prem);
- val sorted = sort (int_ord o pairself (snd o fst)) options;
- val check = tagged_thms_check t sorted;
- in resolve_tac (map snd sorted) i end) i t;
-
-val merge_tagged_nets = Net.merge (Thm.eq_thm_prop o pairself snd);
-
-structure IsTupleIntros = TheoryDataFun
+structure IsTupleThms = TheoryDataFun
(
- type T = tagged_net;
- val empty = build_tagged_net "initial introduction rules" init_intros;
+ type T = thm Symtab.table;
+ val empty = Symtab.make [tuple_istuple];
val copy = I;
val extend = I;
- val merge = K merge_tagged_nets;
+ val merge = K (Symtab.merge Thm.eq_thm_prop);
);
-val get_istuple_intros = IsTupleIntros.get;
-
fun do_typedef name repT alphas thy =
let
fun get_thms thy name =
@@ -93,52 +67,83 @@
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)) end;
+ 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;
-(* copied from earlier version of HOLogic *)
-fun mk_curry t =
- (case Term.fastype_of t of
- T as (Type ("fun", [Type ("*", [A, B]), C])) =>
- Const ("curry", T --> A --> B --> C) $ t
- | _ => raise TERM ("mk_curry: bad body type", [t]));
+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 add_istuple_type (name, alphas) (left, right) thy =
+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 (left, right);
+ val repT = HOLogic.mk_prodT (leftT, rightT);
- val (([rep_inject, abs_inverse], abs), typ_thy) =
+ val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
thy
|> do_typedef name repT alphas
||> Sign.add_path name;
- val abs_curry = mk_curry abs;
- val consT = fastype_of abs_curry;
- val consBind = Binding.name (name ^ consN);
- val cons = Const (Sign.full_name typ_thy consBind, consT);
- val cons_spec = (name ^ consN ^ defN, Logic.mk_equals (cons, abs_curry));
+ (* 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 ([cons_def], cdef_thy) =
+ val ([isom_def], cdef_thy) =
typ_thy
- |> Sign.add_consts_i [Syntax.no_syn (consBind, consT)]
- |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name cons_spec)];
+ |> Sign.add_consts_i [Syntax.no_syn (isomBind, isomT)]
+ |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
- val istuple = [abs_inverse, cons_def] MRS (rep_inject RS istuple_intro);
- val intros = [istuple] RL istuple_intros;
- val intro_net = build_tagged_net name intros;
+ 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
- |> IsTupleIntros.map (curry merge_tagged_nets intro_net)
+ |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop
+ (constname isom, istuple))
|> Sign.parent_path;
in
- (cons, thm_thy)
+ (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 Thu Sep 10 15:18:43 2009 +1000
+++ b/src/HOL/Tools/record.ML Thu Sep 10 16:38:18 2009 +1000
@@ -1,5 +1,6 @@
(* Title: HOL/Tools/record.ML
- Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
+ Authors: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
+ Thomas Sewell, NICTA
Extensible records with structural subtyping in HOL.
*)
@@ -1029,22 +1030,12 @@
(Symtab.insert (K true) (cname u, ()) seen) swaps;
in swapsneeded updfuns [] Symtab.empty SymSymTab.empty end;
-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;
+val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
fun prove_unfold_defs thy ss T ex_simps ex_simprs prop =
let
val defset = get_sel_upd_defs thy;
- val intros = IsTupleSupport.get_istuple_intros thy;
- val in_tac = IsTupleSupport.resolve_from_tagged_net intros;
+ val in_tac = IsTupleSupport.istuple_intros_tac thy;
val prop' = Envir.beta_eta_contract prop;
val (lhs, rhs) = Logic.dest_equals (Logic.strip_assums_concl prop');
val (head, args) = strip_comb lhs;
@@ -1136,8 +1127,7 @@
| _ => NONE));
fun get_upd_acc_cong_thm upd acc thy simpset = let
- val intros = IsTupleSupport.get_istuple_intros thy;
- val in_tac = IsTupleSupport.resolve_from_tagged_net intros;
+ val in_tac = IsTupleSupport.istuple_intros_tac thy;
val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)]
val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv);
@@ -1567,14 +1557,14 @@
val left = List.take (xs, half);
val right = List.drop (xs, half);
in
- HOLogic.mk_prod (mktreeV left, mktreeV right)
+ IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right)
end;
fun mk_istuple ((thy, i), (left, rght)) =
let
val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i);
val nm = suffix suff (Long_Name.base_name name);
- val (cons, thy') = IsTupleSupport.add_istuple_type
+ val (isom, cons, thy') = IsTupleSupport.add_istuple_type
(nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
in
((thy', i + 1), cons $ left $ rght)
@@ -1585,7 +1575,7 @@
fun mk_even_istuple ((thy, i), [arg]) =
((thy, i), arg)
| mk_even_istuple ((thy, i), args) =
- mk_istuple ((thy, i), HOLogic.dest_prod (mktreeV args));
+ mk_istuple ((thy, i), IsTupleSupport.dest_cons_tuple (mktreeV args));
fun build_meta_tree_type i thy vars more =
let
@@ -1645,8 +1635,7 @@
val w = Free (wN, extT);
val P = Free (Name.variant variants "P", extT-->HOLogic.boolT);
val C = Free (Name.variant variants "C", HOLogic.boolT);
- val intros = IsTupleSupport.get_istuple_intros defs_thy;
- val intros_tac = IsTupleSupport.resolve_from_tagged_net intros;
+ val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy;
val inject_prop =
let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
@@ -1934,8 +1923,7 @@
(Binding.name bname, alphas, recT0, Syntax.NoSyn)];
val ext_defs = ext_def :: map #extdef parents;
- val intros = IsTupleSupport.get_istuple_intros extension_thy;
- val intros_tac = IsTupleSupport.resolve_from_tagged_net intros;
+ val intros_tac = IsTupleSupport.istuple_intros_tac extension_thy;
(* Theorems from the istuple intros.
This is complex enough to deserve a full comment.