# HG changeset patch # User Thomas Sewell # Date 1252564698 -36000 # Node ID 192d58483fdf9c78084c491a7e2e9f694ec7b14e # Parent 50406c4951d9e3b747f1981a58518ab0e9f2c1b7 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. diff -r 50406c4951d9 -r 192d58483fdf src/HOL/IsTuple.thy --- 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 \ ('b \ ('c \ 'd)). If we balance the tuple tree to +('a \ 'b) \ ('c \ 'd) then accessors can be defined by converting to +the underlying type then using O(log(n)) fst or snd operations. +Updators can be defined similarly, if we introduce a fst_update and +snd_update function. Furthermore, we can prove the access/update +theorem in O(log(n)) steps by using simple rewrites on fst, snd, +fst_update and snd_update. + +The catch is that, although O(log(n)) steps were taken, the underlying +type we converted to is a tuple tree of size O(n). Processing this term +type wastes performance. We avoid this for large n by taking each +subtree of size K and defining a new type isomorphic to that tuple +subtree. 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 \ ('b \ 'c)) \ (('b \ 'c) \ 'a)) set" + by simp + constdefs - istuple_fst :: "('a \ ('b \ 'c)) \ 'a \ 'b" - "istuple_fst isom \ (fst \ isom)" - istuple_snd :: "('a \ ('b \ 'c)) \ 'a \ 'c" - "istuple_snd isom \ (snd \ isom)" - istuple_fst_update :: "('a \ ('b \ 'c)) \ (('b \ 'c) \ 'a) - \ ('b \ 'b) \ ('a \ 'a)" - "istuple_fst_update isom inv \ \f v. inv (f (fst (isom v)), snd (isom v))" - istuple_snd_update :: "('a \ ('b \ 'c)) \ (('b \ 'c) \ 'a) - \ ('c \ 'c) \ ('a \ 'a)" - "istuple_snd_update isom inv \ \f v. inv (fst (isom v), f (snd (isom v)))" + "TupleIsomorphism repr abst \ Abs_tuple_isomorphism (repr, abst)" + +constdefs + istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \ 'a \ 'b" + "istuple_fst isom \ let (repr, abst) = Rep_tuple_isomorphism isom in fst \ repr" + istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \ 'a \ 'c" + "istuple_snd isom \ let (repr, abst) = Rep_tuple_isomorphism isom in snd \ repr" + istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \ ('b \ 'b) \ ('a \ 'a)" + "istuple_fst_update isom \ + let (repr, abst) = Rep_tuple_isomorphism isom in + (\f v. abst (f (fst (repr v)), snd (repr v)))" + istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \ ('c \ 'c) \ ('a \ 'a)" + "istuple_snd_update isom \ + let (repr, abst) = Rep_tuple_isomorphism isom in + (\f v. abst (fst (repr v), f (snd (repr v))))" + istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \ 'b \ 'c \ 'a" + "istuple_cons isom \ 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 \ 'b \ ('a \ 'b) \ bool" @@ -121,129 +196,137 @@ by (simp add: istuple_surjective_proof_assist_def) locale isomorphic_tuple = - fixes isom :: "'a \ ('b \ 'c)" and inv :: "('b \ 'c) \ 'a" - and cons :: "'b \ 'c \ 'a" - assumes isom_eq: "(isom x = isom y) = (x = y)" - and inverse_inv: "isom (inv v) = v" - and cons_def: "cons \ curry inv" + fixes isom :: "('a, 'b, 'c) tuple_isomorphism" + and repr and abst + defines "repr \ fst (Rep_tuple_isomorphism isom)" + defines "abst \ snd (Rep_tuple_isomorphism isom)" + assumes repr_inv: "\x. abst (repr x) = x" + assumes abst_inv: "\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: "\ f o h g = j o f \ \ - (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: "\ f o h g = j o f \ \ - (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: "\ h f o j g = j g o h f \ \ - (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: "\ h f o j g = j g o h f \ \ - (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: "\ h f o j g = k (f o g) \ \ - (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: "\ h f o j g = k (f o g) \ \ - (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: "\ istuple_surjective_proof_assist v a (istuple_fst isom o f); istuple_surjective_proof_assist v b (istuple_snd isom o f) \ - \ istuple_surjective_proof_assist v (cons a b) f" + \ 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 \ - 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 \ - 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 \ - 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 \ - 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: "\ (a = c \ b = d \ P) = Q \ \ - (cons a b = cons c d \ P) = Q" - by (simp add: simps) + (istuple_cons isom a b = istuple_cons isom c d \ 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: "\x y. (repr x = repr y) = (x = y)" + and abst_inv: "\z. repr (abst z) = z" + shows "v \ TupleIsomorphism repr abst \ 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 \ 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 \ (P \ Q) = (P \ R)" diff -r 50406c4951d9 -r 192d58483fdf src/HOL/Record.thy --- 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 *) diff -r 50406c4951d9 -r 192d58483fdf src/HOL/Tools/istuple_support.ML --- 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; diff -r 50406c4951d9 -r 192d58483fdf src/HOL/Tools/record.ML --- 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.