# HG changeset patch # User tsewell@rubicon.NSW.bigpond.net.au # Date 1251297653 -36000 # Node ID c4e9a48bc50e4ff53e51d9f7c0632b102c56fa2f # Parent a97e9caebd60ae95fb749ffda721a562856fa9ba Initial attempt at porting record update to repository Isabelle. diff -r a97e9caebd60 -r c4e9a48bc50e src/HOL/IsTuple.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IsTuple.thy Thu Aug 27 00:40:53 2009 +1000 @@ -0,0 +1,289 @@ +theory IsTuple imports Product_Type + +uses ("Tools/istuple_support.ML") + +begin + +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)))" + +constdefs + istuple_surjective_proof_assist :: "'a \ 'b \ ('a \ 'b) \ bool" + "istuple_surjective_proof_assist x y f \ f x = y" + istuple_update_accessor_cong_assist :: "(('b \ 'b) \ ('a \ 'a)) + \ ('a \ 'b) \ bool" + "istuple_update_accessor_cong_assist upd acc + \ (\f v. upd (\x. f (acc v)) v = upd f v) + \ (\v. upd id v = v)" + istuple_update_accessor_eq_assist :: "(('b \ 'b) \ ('a \ 'a)) \ ('a \ 'b) + \ 'a \ ('b \ 'b) \ 'a \ 'b \ bool" + "istuple_update_accessor_eq_assist upd acc v f v' x + \ upd f v = v' \ acc v = x + \ 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: "\v. v' = v \ f v = f' v" + shows "upd f r = upd f' r'" + using uac r v[symmetric] + apply (subgoal_tac "upd (\x. f (acc r')) r' = upd (\x. f' (acc r')) r'") + apply (simp add: istuple_update_accessor_cong_assist_def) + apply (simp add: f) + done + +lemma update_accessor_congruence_unfoldE: + "\ istuple_update_accessor_cong_assist upd acc; + r = r'; acc r' = v'; \v. v = v' \ f v = f' v \ + \ upd f r = upd f' r'" + apply (erule(2) update_accessor_congruence_foldE) + apply simp + done + +lemma istuple_update_accessor_cong_assist_id: + "istuple_update_accessor_cong_assist upd acc \ 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 \ 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 + \ istuple_update_accessor_cong_assist upd acc" + by assumption + +lemma update_accessor_accessor_eqE: + "\ istuple_update_accessor_eq_assist upd acc v f v' x \ \ acc v = x" + by (simp add: istuple_update_accessor_eq_assist_def) + +lemma update_accessor_updator_eqE: + "\ istuple_update_accessor_eq_assist upd acc v f v' x \ \ upd f v = v'" + by (simp add: istuple_update_accessor_eq_assist_def) + +lemma istuple_update_accessor_eq_assist_idI: + "v' = f v \ 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 + \ 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 + \ 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 \ a (b v) = c (d v)" + apply (clarsimp simp: o_def) + apply (erule fun_cong) + done + +lemma o_eq_elim: + "\ a o b = c o d; \ \v. a (b v) = c (d v) \ \ R \ \ R" + apply (erule meta_mp) + apply (erule o_eq_dest) + done + +lemma istuple_surjective_proof_assistI: + "f x = y \ + 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 \ x = y" + 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" + +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 + done + +lemmas simps = isom_eq inv_eq inverse_inv inverse_isom cons_def + +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 + = 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 + = 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 + = 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 + = 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" + 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" + 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" + 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" + 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)" + 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)" + 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" + by (clarsimp simp: istuple_surjective_proof_assist_def simps + istuple_fst_def istuple_snd_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) + +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) + +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) + +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) + +lemma cons_conj_eqI: + "\ (a = c \ b = d \ P) = Q \ \ + (cons a b = cons c d \ P) = Q" + by (simp add: 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 + cons_conj_eqI + +end + +interpretation tuple_automorphic: isomorphic_tuple [id id Pair] + by (unfold_locales, simp_all add: curry_def) + +lemma refl_conj_eq: + "Q = R \ (P \ Q) = (P \ R)" + by simp + +lemma meta_all_sameI: + "(\x. PROP P x \ PROP Q x) \ (\x. PROP P x) \ (\x. PROP Q x)" + by simp + +lemma istuple_UNIV_I: "\x. x\UNIV \ True" + by simp + +lemma istuple_True_simp: "(True \ PROP P) \ PROP P" + by simp + +ML {* val traceref = ref [TrueI]; *} + +use "Tools/istuple_support.ML"; + +end diff -r a97e9caebd60 -r c4e9a48bc50e src/HOL/Record.thy --- a/src/HOL/Record.thy Sat Aug 15 15:29:54 2009 +0200 +++ b/src/HOL/Record.thy Thu Aug 27 00:40:53 2009 +1000 @@ -1,26 +1,36 @@ (* 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 *) header {* Extensible records with structural subtyping *} theory Record -imports Product_Type -uses ("Tools/record.ML") +imports Product_Type IsTuple +uses ("Tools/record_package.ML") begin lemma prop_subst: "s = t \ PROP P t \ PROP P s" by simp -lemma rec_UNIV_I: "\x. x\UNIV \ True" - by simp - -lemma rec_True_simp: "(True \ PROP P) \ PROP P" - by simp - lemma K_record_comp: "(\x. c) \ f = (\x. c)" by (simp add: comp_def) +lemma meta_iffD2: + "\ PROP P \ PROP Q; PROP Q \ \ PROP P" + by simp + +lemma o_eq_dest_lhs: + "a o b = c \ a (b v) = c v" + by clarsimp + +lemma id_o_refl: + "id o f = f o id" + by simp + +lemma o_eq_id_dest: + "a o b = id o c \ a (b v) = c v" + by clarsimp subsection {* Concrete record syntax *} @@ -55,7 +65,7 @@ "_record_scheme" :: "[fields, 'a] => 'a" ("(3\_,/ (2\ =/ _)\)") "_record_update" :: "['a, updates] => 'b" ("_/(3\_\)" [900,0] 900) -use "Tools/record.ML" -setup Record.setup +use "Tools/record_package.ML" +setup RecordPackage.setup end diff -r a97e9caebd60 -r c4e9a48bc50e src/HOL/Tools/istuple_support.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/istuple_support.ML Thu Aug 27 00:40:53 2009 +1000 @@ -0,0 +1,145 @@ +(* Title: HOL/Tools/ntuple_support.ML + Author: Thomas Sewell, NICTA + +Support for defining instances of tuple-like types and extracting +introduction rules needed by the record package. +*) + + +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; + + 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; +end; + +structure IsTupleSupport : ISTUPLE_SUPPORT = +struct + +val consN = "_NTupleCons"; +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 = thms "isomorphic_tuple.intros"; + +val init_intros = thms "tuple_automorphic.intros"; + +type tagged_net = ((string * int) * thm) Net.net; + +(* 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 tag_thm_trace = ref ([] : thm list); + +(* 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 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 +( + type T = tagged_net; + val empty = build_tagged_net "initial introduction rules" init_intros; + val copy = I; + val extend = I; + val merge = K merge_tagged_nets; +); + +val get_istuple_intros = IsTupleIntros.get; + +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, ...} = TypedefPackage.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; + in + thy + |> TypecopyPackage.add_typecopy (name, alphas) repT NONE + |-> (fn (name, _) => `(fn thy => get_thms thy name)) + end; + +fun add_istuple_type (name, alphas) (left, right) thy = +let + val repT = HOLogic.mk_prodT (left, right); + + val (([rep_inject, abs_inverse], abs), typ_thy) = + thy + |> do_typedef name repT alphas + ||> Sign.add_path name; + + val abs_curry = HOLogic.mk_curry abs; + val consT = fastype_of abs_curry; + val cons = Const (Sign.full_name typ_thy (name ^ consN), consT); + val cons_spec = (name ^ consN ^ defN, Logic.mk_equals (cons, abs_curry)); + + val ([cons_def], cdef_thy) = + typ_thy + |> Sign.add_consts_i [Syntax.no_syn (name ^ consN, consT)] + |> PureThy.add_defs_i false [Thm.no_attributes cons_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 thm_thy = + cdef_thy + |> IsTupleIntros.map (curry merge_tagged_nets intro_net) + |> Sign.parent_path; +in + (cons, thm_thy) +end; + +end; + +structure IsTupleIntros2 = TheoryDataFun +( + type T = IsTupleSupport.tagged_net; + val empty = IsTupleSupport.build_tagged_net "" []; + val copy = I; + val extend = I; + val merge = K IsTupleSupport.merge_tagged_nets; +); + + diff -r a97e9caebd60 -r c4e9a48bc50e src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat Aug 15 15:29:54 2009 +0200 +++ b/src/HOL/Tools/record.ML Thu Aug 27 00:40:53 2009 +1000 @@ -55,8 +55,6 @@ struct val eq_reflection = thm "eq_reflection"; -val rec_UNIV_I = thm "rec_UNIV_I"; -val rec_True_simp = thm "rec_True_simp"; val Pair_eq = thm "Product_Type.prod.inject"; val atomize_all = thm "HOL.atomize_all"; val atomize_imp = thm "HOL.atomize_imp"; @@ -65,6 +63,34 @@ val Pair_sel_convs = [fst_conv,snd_conv]; val K_record_comp = @{thm "K_record_comp"}; val K_comp_convs = [@{thm o_apply}, K_record_comp] +val transitive_thm = thm "transitive"; +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 refl_conj_eq = thm "refl_conj_eq"; +val meta_all_sameI = thm "meta_all_sameI"; +val meta_iffD2 = thm "meta_iffD2"; + +val surject_assistI = @{thm "istuple_surjective_proof_assistI"}; +val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"}; + +val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"}; +val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"}; +val updacc_eq_idI = @{thm "istuple_update_accessor_eq_assist_idI"}; +val updacc_eq_triv = @{thm "istuple_update_accessor_eq_assist_triv"}; + +val updacc_foldE = @{thm "update_accessor_congruence_foldE"}; +val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"}; +val updacc_noopE = @{thm "update_accessor_noopE"}; +val updacc_noop_compE = @{thm "update_accessor_noop_compE"}; +val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"}; +val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"}; +val updacc_cong_from_eq = @{thm "istuple_update_accessor_cong_from_eq"}; + +val o_eq_dest = thm "o_eq_dest"; +val o_eq_id_dest = thm "o_eq_id_dest"; +val o_eq_dest_lhs = thm "o_eq_dest_lhs"; (** name components **) @@ -73,6 +99,7 @@ val moreN = "more"; val schemeN = "_scheme"; val ext_typeN = "_ext_type"; +val inner_typeN = "_inner_type"; val extN ="_ext"; val casesN = "_cases"; val ext_dest = "_sel"; @@ -232,23 +259,26 @@ parent: (typ list * string) option, fields: (string * typ) list, extension: (string * typ list), - induct: thm + induct: thm, + extdef: thm }; -fun make_record_info args parent fields extension induct = +fun make_record_info args parent fields extension induct extdef = {args = args, parent = parent, fields = fields, extension = extension, - induct = induct}: record_info; + induct = induct, extdef = extdef}: record_info; type parent_info = {name: string, fields: (string * typ) list, extension: (string * typ list), - induct: thm + induct: thm, + extdef: thm }; -fun make_parent_info name fields extension induct = - {name = name, fields = fields, extension = extension, induct = induct}: parent_info; +fun make_parent_info name fields extension induct extdef = + {name = name, fields = fields, extension = extension, + induct = induct, extdef = extdef}: parent_info; (* theory data *) @@ -278,14 +308,18 @@ type T = record_data; val empty = make_record_data Symtab.empty - {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss} + {selectors = Symtab.empty, updates = Symtab.empty, + simpset = HOL_basic_ss, defset = HOL_basic_ss, + foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss} Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty; val copy = I; val extend = I; fun merge _ ({records = recs1, - sel_upd = {selectors = sels1, updates = upds1, simpset = ss1}, + sel_upd = {selectors = sels1, updates = upds1, + simpset = ss1, defset = ds1, + foldcong = fc1, unfoldcong = uc1}, equalities = equalities1, extinjects = extinjects1, extsplit = extsplit1, @@ -293,7 +327,9 @@ extfields = extfields1, fieldext = fieldext1}, {records = recs2, - sel_upd = {selectors = sels2, updates = upds2, simpset = ss2}, + sel_upd = {selectors = sels2, updates = upds2, + simpset = ss2, defset = ds2, + foldcong = fc2, unfoldcong = uc2}, equalities = equalities2, extinjects = extinjects2, extsplit = extsplit2, @@ -304,7 +340,10 @@ (Symtab.merge (K true) (recs1, recs2)) {selectors = Symtab.merge (K true) (sels1, sels2), updates = Symtab.merge (K true) (upds1, upds2), - simpset = Simplifier.merge_ss (ss1, ss2)} + simpset = Simplifier.merge_ss (ss1, ss2), + defset = Simplifier.merge_ss (ds1, ds2), + foldcong = Simplifier.merge_ss (fc1, fc2), + unfoldcong = Simplifier.merge_ss (uc1, uc2)} (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2)) (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2)) (Symtab.merge Thm.eq_thm_prop (extsplit1,extsplit2)) @@ -355,7 +394,21 @@ val is_selector = Symtab.defined o #selectors o get_sel_upd; val get_updates = Symtab.lookup o #updates o get_sel_upd; -fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy)); +fun get_ss_with_context getss thy = + Simplifier.theory_context thy (getss (get_sel_upd thy)); + +val get_simpset = get_ss_with_context (#simpset); +val get_sel_upd_defs = get_ss_with_context (#defset); +val get_foldcong_ss = get_ss_with_context (#foldcong); +val get_unfoldcong_ss = get_ss_with_context (#unfoldcong); + +fun get_update_details u thy = let + val sel_upd = get_sel_upd thy; + in case (Symtab.lookup (#updates sel_upd) u) of + SOME s => let + val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s; + in SOME (s, dep, ismore) end + | NONE => NONE end; fun put_sel_upd names simps = RecordsData.map (fn {records, sel_upd = {selectors, updates, simpset}, @@ -489,7 +542,7 @@ let fun err msg = error (msg ^ " parent record " ^ quote name); - val {args, parent, fields, extension, induct} = + val {args, parent, fields, extension, induct, extdef} = (case get_record thy name of SOME info => info | NONE => err "Unknown"); val _ = if length types <> length args then err "Bad number of arguments for" else (); @@ -505,7 +558,7 @@ val extension' = apsnd (map subst) extension; in add_parents thy parent' - (make_parent_info name fields' extension' induct :: parents) + (make_parent_info name fields' extension' induct extdef :: parents) end; @@ -882,95 +935,113 @@ then noopt () else opt (); -local -fun abstract_over_fun_app (Abs (f,fT,t)) = - let - val (f',t') = Term.dest_abs (f,fT,t); - val T = domain_type fT; - val (x,T') = hd (Term.variant_frees t' [("x",T)]); - val f_x = Free (f',fT)$(Free (x,T')); - fun is_constr (Const (c,_)$_) = can (unsuffix extN) c - | is_constr _ = false; - fun subst (t as u$w) = if Free (f',fT)=u - then if is_constr w then f_x - else raise TERM ("abstract_over_fun_app",[t]) - else subst u$subst w - | subst (Abs (x,T,t)) = (Abs (x,T,subst t)) - | subst t = t - val t'' = abstract_over (f_x,subst t'); - val vars = strip_qnt_vars "all" t''; - val bdy = strip_qnt_body "all" t''; - - in list_abs ((x,T')::vars,bdy) end - | abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]); -(* Generates a theorem of the kind: - * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x* - *) -fun mk_fun_apply_eq (Abs (f, fT, t)) thy = +fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t')) + = case (get_updates thy u) + of SOME u_name => u_name = s + | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]); + +fun mk_comp f g = let + val x = fastype_of g; + val a = domain_type x; + val b = range_type x; + val c = range_type (fastype_of f); + val T = (b --> c) --> ((a --> b) --> (a --> c)) + in Const ("Fun.comp", T) $ f $ g end; + +fun mk_comp_id f = let + 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_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 Term.fast_term_ord + (get_updfuns body); + fun get_simp upd = let + val T = domain_type (fastype_of upd); + val lhs = mk_comp acc (upd $ Free ("f", T)); + val rhs = if is_sel_upd_pair thy acc upd + then mk_comp (Free ("f", T)) acc else mk_comp_id acc; + val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); + val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn prems => + EVERY [simp_tac defset 1, + REPEAT_DETERM (intros_tac 1), + TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)]); + 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; + +structure SymSymTab = TableFun(type key = string * string + val ord = prod_ord fast_string_ord fast_string_ord); + +fun get_updupd_simp thy defset intros_tac u u' comp = let + val f = Free ("f", domain_type (fastype_of u)); + val f' = Free ("f'", domain_type (fastype_of u')); + val lhs = mk_comp (u $ f) (u' $ f'); + val rhs = if comp + then u $ mk_comp f f' + else mk_comp (u' $ f') (u $ f); + val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); + val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn prems => + EVERY [simp_tac defset 1, + REPEAT_DETERM (intros_tac 1), + TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]); + val dest = if comp then o_eq_dest_lhs else o_eq_dest; + in standard (othm RS dest) end; + +fun get_updupd_simps thy term defset intros_tac = let + val recT = fastype_of term; + val updfuns = get_updfuns 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 + 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 = + if Symtab.defined seen (cname u) + then swapsneeded us prev seen + (buildswapstoeq u prev swaps) + else swapsneeded us (u::prev) + (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) (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 prove_unfold_defs thy ss T ex_simps ex_simprs prop = let - val rT = domain_type fT; - val vars = Term.strip_qnt_vars "all" t; - val Ts = map snd vars; - val n = length vars; - fun app_bounds 0 t = t$Bound 0 - | app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t - - - val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)]; - val prop = Logic.mk_equals - (list_all ((f,fT)::vars, - app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))), - list_all ((fst r,rT)::vars, - app_bounds (n - 1) ((Free P)$Bound n))); - val prove_standard = quick_and_dirty_prove true thy; - val thm = prove_standard [] prop (fn _ => - EVERY [rtac equal_intr_rule 1, - Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1, - Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]); - in thm end - | mk_fun_apply_eq t thy = raise TERM ("mk_fun_apply_eq",[t]); - -in -(* During proof of theorems produced by record_simproc you can end up in - * situations like "!!f ... . ... f r ..." where f is an extension update function. - * In order to split "f r" we transform this to "!!r ... . ... r ..." so that the - * usual split rules for extensions can apply. - *) -val record_split_f_more_simproc = - Simplifier.simproc @{theory HOL} "record_split_f_more_simp" ["x"] - (fn thy => fn _ => fn t => - (case t of (Const ("all", Type (_, [Type (_, [Type("fun",[T,T']), _]), _])))$ - (trm as Abs _) => - (case rec_id (~1) T of - "" => NONE - | n => if T=T' - then (let - val P=cterm_of thy (abstract_over_fun_app trm); - val thm = mk_fun_apply_eq trm thy; - val PV = cterm_of thy (hd (OldTerm.term_vars (prop_of thm))); - val thm' = cterm_instantiate [(PV,P)] thm; - in SOME thm' end handle TERM _ => NONE) - else NONE) - | _ => NONE)) -end - -fun prove_split_simp thy ss T prop = - let - val {sel_upd={simpset,...},extsplit,...} = RecordsData.get thy; - val extsplits = - Library.foldl (fn (thms,(n,_)) => the_list (Symtab.lookup extsplit n) @ thms) - ([],dest_recTs T); - val thms = (case get_splits thy (rec_id (~1) T) of - SOME (all_thm,_,_,_) => - all_thm::(case extsplits of [thm] => [] | _ => extsplits) - (* [thm] is the same as all_thm *) - | NONE => extsplits) - val thms'=K_comp_convs@thms; - val ss' = (Simplifier.inherit_context ss simpset - addsimps thms' - addsimprocs [record_split_f_more_simproc]); + val defset = get_sel_upd_defs thy; + val intros = IsTupleSupport.get_istuple_intros thy; + val in_tac = IsTupleSupport.resolve_from_tagged_net intros; + val prop' = Envir.beta_eta_contract prop; + val (lhs, rhs) = Logic.dest_equals (Logic.strip_assums_concl prop'); + val (head, args) = strip_comb lhs; + val simps = if length args = 1 + then get_accupd_simps thy lhs defset in_tac + else get_updupd_simps thy lhs defset in_tac; in - quick_and_dirty_prove true thy [] prop (fn _ => simp_tac ss' 1) + Goal.prove (ProofContext.init thy) [] [] prop' (fn prems => + simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 + THEN TRY (simp_tac (HOL_basic_ss addsimps ex_simps + addsimprocs ex_simprs) 1)) end; @@ -984,21 +1055,6 @@ if null (loose_bnos t) then ((n,kT),(Abs (x,xT,Bound (i+1)))) else ((n,T),b) | K_skeleton n T b _ = ((n,T),b); -(* -fun K_skeleton n _ b ((K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_) = - ((n,kT),K_rec$b) - | K_skeleton n _ (Bound i) - (Abs (x,T,(K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_$Bound 0)) = - ((n,kT),Abs (x,T,(K_rec$Bound (i+1)$Bound 0))) - | K_skeleton n T b _ = ((n,T),b); - *) - -fun normalize_rhs thm = - let - val ss = HOL_basic_ss addsimps K_comp_convs; - val rhs = thm |> Thm.cprop_of |> Thm.dest_comb |> snd; - val rhs' = (Simplifier.rewrite ss rhs); - in Thm.transitive thm rhs' end; in (* record_simproc *) (* Simplifies selections of an record update: @@ -1044,7 +1100,7 @@ else (case mk_eq_terms r of SOME (trm,trm',vars) => let - val (kv,kb) = + val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k; in SOME (upd$kb$trm,trm',kv::vars) end | NONE @@ -1057,150 +1113,140 @@ in (case mk_eq_terms (upd$k$r) of SOME (trm,trm',vars) - => SOME (prove_split_simp thy ss domS - (list_all(vars, Logic.mk_equals (sel $ trm, trm')))) + => SOME (prove_unfold_defs thy ss domS [] [] + (list_all(vars,(equals rangeS$(sel$trm)$trm')))) | NONE => NONE) end | NONE => NONE) else NONE | _ => 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 insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)] + val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv); + in Goal.prove (ProofContext.init thy) [] [] prop (fn prems => + EVERY [simp_tac simpset 1, + REPEAT_DETERM (in_tac 1), + TRY (resolve_tac [updacc_cong_idI] 1)]) + end; + (* record_upd_simproc *) (* simplify multiple updates: * (1) "N_update y (M_update g (N_update x (M_update f r))) = (N_update (y o x) (M_update (g o f) r))" * (2) "r(|M:= M r|) = r" - * For (2) special care of "more" updates has to be taken: - * r(|more := m; A := A r|) - * If A is contained in the fields of m we cannot remove the update A := A r! - * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|) + * In both cases "more" updates complicate matters: for this reason + * we omit considering further updates if doing so would introduce + * both a more update and an update to a field within it. *) val record_upd_simproc = Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"] (fn thy => fn ss => fn t => - (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) => - let datatype ('a,'b) calc = Init of 'b | Inter of 'a - val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy; - - (*fun mk_abs_var x t = (x, fastype_of t);*) - fun sel_name u = Long_Name.base_name (unsuffix updateN u); - - fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) = - if has_field extfields s (domain_type' mT) then upd else seed s r - | seed _ r = r; - - fun grow u uT k kT vars (sprout,skeleton) = - if sel_name u = moreN - then let val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k; - in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end - else ((sprout,skeleton),vars); - - - fun dest_k (Abs (x,T,((sel as Const (s,_))$r))) = - if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE - | dest_k (Abs (_,_,(Abs (x,T,((sel as Const (s,_))$r)))$Bound 0)) = - (* eta expanded variant *) - if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE - | dest_k _ = NONE; - - fun is_upd_same (sprout,skeleton) u k = - (case dest_k k of SOME (x,T,sel,s,r) => - if (unsuffix updateN u) = s andalso (seed s sprout) = r - then SOME (fn t => Abs (x,T,incr_boundvars 1 t),sel,seed s skeleton) - else NONE - | NONE => NONE); - - fun init_seed r = ((r,Bound 0), [("r", rT)]); - - fun add (n:string) f fmaps = - (case AList.lookup (op =) fmaps n of - NONE => AList.update (op =) (n,[f]) fmaps - | SOME fs => AList.update (op =) (n,f::fs) fmaps) - - fun comps (n:string) T fmaps = - (case AList.lookup (op =) fmaps n of - SOME fs => - foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs - | NONE => error ("record_upd_simproc.comps")) - - (* mk_updterm returns either - * - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made, - * where vars are the bound variables in the skeleton - * - Inter (orig-term-skeleton,simplified-term-skeleton, - * vars, (term-sprout, skeleton-sprout)) - * where "All vars. orig-term-skeleton = simplified-term-skeleton" is - * the desired simplification rule, - * the sprouts accumulate the "more-updates" on the way from the seed - * to the outermost update. It is only relevant to calculate the - * possible simplification for (2) - * The algorithm first walks down the updates to the seed-record while - * memorising the updates in the already-table. While walking up the - * updates again, the optimised term is constructed. - *) - fun mk_updterm upds already - (t as ((upd as Const (u,uT as (Type (_,[kT,_])))) $ k $ r)) = - if Symtab.defined upds u - then let - fun rest already = mk_updterm upds already - in if u mem_string already - then (case (rest already r) of - Init ((sprout,skel),vars) => - let - val n = sel_name u; - val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; - val (sprout',vars')= grow u uT k kT (kv::vars) (sprout,skel); - in Inter (upd$kb$skel,skel,vars',add n kb [],sprout') end - | Inter (trm,trm',vars,fmaps,sprout) => - let - val n = sel_name u; - val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; - val (sprout',vars') = grow u uT k kT (kv::vars) sprout; - in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout') - end) - else - (case rest (u::already) r of - Init ((sprout,skel),vars) => - (case is_upd_same (sprout,skel) u k of - SOME (K_rec,sel,skel') => - let - val (sprout',vars') = grow u uT k kT vars (sprout,skel); - in Inter(upd$(K_rec (sel$skel'))$skel,skel,vars',[],sprout') - end - | NONE => - let - val n = sel_name u; - val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; - in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end) - | Inter (trm,trm',vars,fmaps,sprout) => - (case is_upd_same sprout u k of - SOME (K_rec,sel,skel) => - let - val (sprout',vars') = grow u uT k kT vars sprout - in Inter(upd$(K_rec (sel$skel))$trm,trm',vars',fmaps,sprout') - end - | NONE => - let - val n = sel_name u - val T = domain_type kT - val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; - val (sprout',vars') = grow u uT k kT (kv::vars) sprout - val fmaps' = add n kb fmaps - in Inter (upd$kb$trm,upd$comps n T fmaps'$trm' - ,vars',fmaps',sprout') end)) - end - else Init (init_seed t) - | mk_updterm _ _ t = Init (init_seed t); - - in (case mk_updterm updates [] t of - Inter (trm,trm',vars,_,_) - => SOME (normalize_rhs - (prove_split_simp thy ss rT - (list_all(vars, Logic.mk_equals (trm, trm'))))) - | _ => NONE) - end - | _ => NONE)) + let + (* we can use more-updators with other updators as long + as none of the other updators go deeper than any more + updator. min here is the depth of the deepest other + updator, max the depth of the shallowest more updator *) + fun include_depth (dep, true) (min, max) = + if (min <= dep) + then SOME (min, if dep <= max orelse max = ~1 then dep else max) + else NONE + | include_depth (dep, false) (min, max) = + if (dep <= max orelse max = ~1) + then SOME (if min <= dep then dep else min, max) + else NONE; + + fun getupdseq (term as (upd as Const (u, T)) $ f $ tm) min max = + (case get_update_details u thy of + SOME (s, dep, ismore) => + (case include_depth (dep, ismore) (min, max) of + SOME (min', max') => let + val (us, bs, _) = getupdseq tm min' max'; + in ((upd, s, f) :: us, bs, fastype_of term) end + | NONE => ([], term, HOLogic.unitT)) + | NONE => ([], term, HOLogic.unitT)) + | getupdseq term _ _ = ([], term, HOLogic.unitT); + + val (upds, base, baseT) = getupdseq t 0 ~1; + + fun is_upd_noop s (f as Abs (n, T, Const (s', T') $ tm')) tm = + if s = s' andalso null (loose_bnos tm') + andalso subst_bound (HOLogic.unit, tm') = tm + then (true, Abs (n, T, Const (s', T') $ Bound 1)) + else (false, HOLogic.unit) + | is_upd_noop s f tm = (false, HOLogic.unit); + + fun get_noop_simps (upd as Const (u, T)) + (f as Abs (n, T', (acc as Const (s, T'')) $ _)) = let + + val ss = get_sel_upd_defs thy; + val uathm = get_upd_acc_cong_thm upd acc thy ss; + in [standard (uathm RS updacc_noopE), + standard (uathm RS updacc_noop_compE)] end; + + (* if f is constant then (f o g) = f. we know that K_skeleton + only returns constant abstractions thus when we see an + abstraction we can discard inner updates. *) + fun add_upd (f as Abs _) fs = [f] + | add_upd f fs = (f :: fs); + + (* mk_updterm returns + * (orig-term-skeleton, simplified-skeleton, + * variables, duplicate-updates, simp-flag, noop-simps) + * + * where duplicate-updates is a table used to pass upward + * the list of update functions which can be composed + * into an update above them, simp-flag indicates whether + * any simplification was achieved, and noop-simps are + * used for eliminating case (2) defined above + *) + fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term = let + val (lhs, rhs, vars, dups, simp, noops) = + mk_updterm upds (Symtab.update (u, ()) above) term; + val (fvar, skelf) = K_skeleton (Sign.base_name s) (domain_type T) + (Bound (length vars)) f; + val (isnoop, skelf') = is_upd_noop s f term; + val funT = domain_type T; + fun mk_comp_local (f, f') = + Const ("Fun.comp", funT --> funT --> funT) $ f $ f'; + in if isnoop + then (upd $ skelf' $ lhs, rhs, vars, + Symtab.update (u, []) dups, true, + if Symtab.defined noops u then noops + else Symtab.update (u, get_noop_simps upd skelf') noops) + else if Symtab.defined above u + then (upd $ skelf $ lhs, rhs, fvar :: vars, + Symtab.map_default (u, []) (add_upd skelf) dups, + true, noops) + else case Symtab.lookup dups u of + SOME fs => + (upd $ skelf $ lhs, + upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs, + fvar :: vars, dups, true, noops) + | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, + fvar :: vars, dups, simp, noops) + end + | mk_updterm [] above term = (Bound 0, Bound 0, [("r", baseT)], + Symtab.empty, false, Symtab.empty) + | mk_updterm us above term = raise TERM ("mk_updterm match", + map (fn (x, y, z) => x) us); + + val (lhs, rhs, vars, dups, simp, noops) + = mk_updterm upds Symtab.empty base; + val noops' = flat (map snd (Symtab.dest noops)); + in + if simp then + SOME (prove_unfold_defs thy ss baseT noops' [record_simproc] + (list_all(vars,(equals baseT$lhs$rhs)))) + else NONE + end) + end + (* record_eq_simproc *) (* looks up the most specific record-equality. * Note on efficiency: @@ -1467,28 +1513,6 @@ i st)) (st,((length params) - 1) downto 0)) end; -fun extension_typedef name repT alphas thy = - let - fun get_thms thy name = - let - val SOME { Abs_induct = abs_induct, - Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = Typedef.get_info thy name; - val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp]; - in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end; - val tname = Binding.name (Long_Name.base_name name); - in - thy - |> Typecopy.typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE - |-> (fn (name, _) => `(fn thy => get_thms thy name)) - end; - -fun mixit convs refls = - let - fun f ((res,lhs,rhs),refl) = - ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs); - in #1 (Library.foldl f (([],[],convs),refls)) end; - - fun extension_definition full name fields names alphas zeta moreT more vars thy = let val base = Long_Name.base_name; @@ -1498,7 +1522,6 @@ val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS); val extT_name = suffix ext_typeN name val extT = Type (extT_name, alphas_zetaTs); - val repT = foldr1 HOLogic.mk_prodT (fieldTs@[moreT]); val fields_more = fields@[(full moreN,moreT)]; val fields_moreTs = fieldTs@[moreT]; val bfields_more = map (apfst base) fields_more; @@ -1506,61 +1529,97 @@ val len = length fields; val idxms = 0 upto len; + (* before doing anything else, create the tree of new types + that will back the record extension *) + + fun mktreeT [] = raise (TYPE ("mktreeT: empty list", [], [])) + | mktreeT [T] = T + | mktreeT xs = + let + val len = length xs; + val half = len div 2; + val left = List.take (xs, half); + val right = List.drop (xs, half); + in + HOLogic.mk_prodT (mktreeT left, mktreeT right) + end; + + fun mktreeV [] = raise (TYPE ("mktreeV: empty list", [], [])) + | mktreeV [T] = T + | mktreeV xs = + let + val len = length xs; + val half = len div 2; + val left = List.take (xs, half); + val right = List.drop (xs, half); + in + HOLogic.mk_prod (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 (Sign.base_name name); + val (cons, thy') = IsTupleSupport.add_istuple_type + (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy; + in + ((thy', i + 1), cons $ left $ rght) + end; + + (* trying to create a 1-element istuple will fail, and + is pointless anyway *) + 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)); + + fun build_meta_tree_type i thy vars more = + let + val len = length vars; + in + if len < 1 + then raise (TYPE ("meta_tree_type args too short", [], vars)) + else if len > 16 + then let + fun group16 [] = [] + | group16 xs = Library.take (16, xs) + :: group16 (Library.drop (16, xs)); + val vars' = group16 vars; + val ((thy', i'), composites) = + foldl_map mk_even_istuple ((thy, i), vars'); + in + build_meta_tree_type i' thy' composites more + end + else let + val ((thy', i'), term) + = mk_istuple ((thy, 0), (mktreeV vars, more)); + in + (term, thy') + end + end; + + val _ = timing_msg "record extension preparing definitions"; + + (* 1st stage part 1: introduce the tree of new types *) + fun get_meta_tree () = build_meta_tree_type 1 thy vars more; + val (ext_body, typ_thy) = + timeit_msg "record extension nested type def:" get_meta_tree; + (* prepare declarations and definitions *) (*fields constructor*) val ext_decl = (mk_extC (name,extT) fields_moreTs); - (* - val ext_spec = Const ext_decl :== - (foldr (uncurry lambda) - (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))) (vars@[more])) - *) - val ext_spec = list_comb (Const ext_decl,vars@[more]) :== - (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))); + val ext_spec = list_comb (Const ext_decl,vars@[more]) :== ext_body; fun mk_ext args = list_comb (Const ext_decl, args); - (*destructors*) - val _ = timing_msg "record extension preparing definitions"; - val dest_decls = map (mk_selC extT o (apfst (suffix ext_dest))) bfields_more; - - fun mk_dest_spec (i, (c,T)) = - let val snds = (funpow i HOLogic.mk_snd (mk_Rep name repT extT $ r)) - in Const (mk_selC extT (suffix ext_dest c,T)) - :== (lambda r (if i=len then snds else HOLogic.mk_fst snds)) - end; - val dest_specs = - ListPair.map mk_dest_spec (idxms, fields_more); - - (*updates*) - val upd_decls = map (mk_updC updN extT) bfields_more; - fun mk_upd_spec (c,T) = - let - val args = map (fn (n,nT) => if n=c then Free (base c,T --> T)$ - (mk_sel r (suffix ext_dest n,nT)) - else (mk_sel r (suffix ext_dest n,nT))) - fields_more; - in Const (mk_updC updN extT (c,T))$(Free (base c,T --> T))$r - :== mk_ext args - end; - val upd_specs = map mk_upd_spec fields_more; - - (* 1st stage: defs_thy *) + (* 1st stage part 2: define the ext constant *) fun mk_defs () = - thy - |> extension_typedef name repT (alphas @ [zeta]) - ||> Sign.add_consts_i - (map (Syntax.no_syn o apfst Binding.name) (apfst base ext_decl :: dest_decls @ upd_decls)) - ||>> PureThy.add_defs false - (map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs)) - ||>> PureThy.add_defs false - (map (Thm.no_attributes o apfst Binding.name) upd_specs) - |-> (fn args as ((_, dest_defs), upd_defs) => - fold Code.add_default_eqn dest_defs - #> fold Code.add_default_eqn upd_defs - #> pair args); - val ((([abs_inject, abs_inverse, abs_induct], ext_def :: dest_defs), upd_defs), defs_thy) = - timeit_msg "record extension type/selector/update defs:" mk_defs; + typ_thy + |> Sign.add_consts_i [Syntax.no_syn (apfst (Binding.name o base) ext_decl)] + |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name ext_spec)] + val ([ext_def], defs_thy) = + timeit_msg "record extension constructor def:" mk_defs; (* prepare propositions *) val _ = timing_msg "record extension preparing propositions"; @@ -1572,14 +1631,17 @@ 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 inject_prop = let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more; - in All (map dest_Free (vars_more@vars_more')) - ((HOLogic.eq_const extT $ - mk_ext vars_more$mk_ext vars_more') - === - foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more'))) + in + ((HOLogic.mk_conj (HOLogic.eq_const extT $ + mk_ext vars_more$mk_ext vars_more', HOLogic.true_const)) + === + foldr1 HOLogic.mk_conj + (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const])) end; val induct_prop = @@ -1590,22 +1652,6 @@ (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C)) ==> Trueprop C; - (*destructors*) - val dest_conv_props = - map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more; - - (*updates*) - fun mk_upd_prop (i,(c,T)) = - let val x' = Free (Name.variant variants (base c ^ "'"),T --> T) - val args' = nth_map i (K (x'$nth vars_more i)) vars_more - in mk_upd updN c x' ext === mk_ext args' end; - val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more); - - val surjective_prop = - let val args = - map (fn (c, Free (_,T)) => mk_sel s (suffix ext_dest c,T)) named_vars_more; - in s === mk_ext args end; - val split_meta_prop = let val P = Free (Name.variant variants "P", extT-->Term.propT) in Logic.mk_equals @@ -1618,110 +1664,65 @@ let val tac = simp_all_tac HOL_ss simps in fn prop => prove stndrd [] prop (K tac) end; - fun inject_prf () = (prove_simp true [ext_def,abs_inject,Pair_eq] inject_prop); + fun inject_prf () = + simplify HOL_ss ( + prove_standard [] inject_prop (fn prems => + EVERY [simp_tac (HOL_basic_ss addsimps [ext_def]) 1, + REPEAT_DETERM (resolve_tac [refl_conj_eq] 1 + ORELSE intros_tac 1 + ORELSE resolve_tac [refl] 1)])); + val inject = timeit_msg "record extension inject proof:" inject_prf; + (* We need a surjection property r = (| f = f r, g = g r ... |) + to prove other theorems. We haven't given names to the accessors + f, g etc yet however, so we generate an ext structure with + free variables as all arguments and allow the introduction tactic to + operate on it as far as it can. We then use standard to convert + the free variables into unifiable variables and unify them with + (roughly) the definition of the accessor. *) + fun surject_prf () = let + val cterm_ext = cterm_of defs_thy ext; + val start = named_cterm_instantiate [("y", cterm_ext)] + surject_assist_idE; + val tactic1 = simp_tac (HOL_basic_ss addsimps [ext_def]) 1 + THEN REPEAT_ALL_NEW intros_tac 1 + val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1); + val [halfway] = Seq.list_of (tactic1 start); + val [surject] = Seq.list_of (tactic2 (standard halfway)); + in + surject + end; + val surject = timeit_msg "record extension surjective proof:" surject_prf; + + fun split_meta_prf () = + prove_standard [] split_meta_prop (fn prems => + EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1, + etac meta_allE 1, atac 1, + rtac (prop_subst OF [surject]) 1, + REPEAT (etac meta_allE 1), atac 1]); + val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf; + fun induct_prf () = let val (assm, concl) = induct_prop in prove_standard [assm] concl (fn {prems, ...} => - EVERY [try_param_tac rN abs_induct 1, - simp_tac (HOL_ss addsimps [split_paired_all]) 1, - resolve_tac (map (rewrite_rule [ext_def]) prems) 1]) - end; + EVERY [cut_rules_tac [split_meta RS meta_iffD2] 1, + resolve_tac prems 2, + asm_simp_tac HOL_ss 1]) end; val induct = timeit_msg "record extension induct proof:" induct_prf; - fun cases_prf_opt () = - let - val (_$(Pvar$_)) = concl_of induct; - val ind = cterm_instantiate - [(cterm_of defs_thy Pvar, cterm_of defs_thy - (lambda w (HOLogic.imp$HOLogic.mk_eq(r,w)$C)))] - induct; - in standard (ObjectLogic.rulify (mp OF [ind, refl])) end; - - fun cases_prf_noopt () = - prove_standard [] cases_prop (fn _ => - EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1, - try_param_tac rN induct 1, - rtac impI 1, - REPEAT (etac allE 1), - etac mp 1, - rtac refl 1]) - - val cases_prf = quick_and_dirty_prf cases_prf_noopt cases_prf_opt; - val cases = timeit_msg "record extension cases proof:" cases_prf; - - fun dest_convs_prf () = map (prove_simp false - ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props; - val dest_convs = timeit_msg "record extension dest_convs proof:" dest_convs_prf; - fun dest_convs_standard_prf () = map standard dest_convs; - - val dest_convs_standard = - timeit_msg "record extension dest_convs_standard proof:" dest_convs_standard_prf; - - fun upd_convs_prf_noopt () = map (prove_simp true (dest_convs_standard@upd_defs)) - upd_conv_props; - fun upd_convs_prf_opt () = - let - - fun mkrefl (c,T) = Thm.reflexive - (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T-->T))); - val refls = map mkrefl fields_more; - val dest_convs' = map mk_meta_eq dest_convs; - val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs'); - - val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext)); - - fun mkthm (udef,(fld_refl,thms)) = - let val bdyeq = Library.foldl (uncurry Thm.combination) (constr_refl,thms); - (* (|N=N (|N=N,M=M,K=K,more=more|) - M=M (|N=N,M=M,K=K,more=more|) - K=K' - more = more (|N=N,M=M,K=K,more=more|) = - (|N=N,M=M,K=K',more=more|) - *) - val (_$(_$v$r)$_) = prop_of udef; - val (_$(v'$_)$_) = prop_of fld_refl; - val udef' = cterm_instantiate - [(cterm_of defs_thy v,cterm_of defs_thy v'), - (cterm_of defs_thy r,cterm_of defs_thy ext)] udef; - in standard (Thm.transitive udef' bdyeq) end; - in map mkthm (rev upd_defs ~~ (mixit dest_convs' map_eqs)) end; - - val upd_convs_prf = quick_and_dirty_prf upd_convs_prf_noopt upd_convs_prf_opt; - - val upd_convs = - timeit_msg "record extension upd_convs proof:" upd_convs_prf; - - fun surjective_prf () = - prove_standard [] surjective_prop (fn _ => - (EVERY [try_param_tac rN induct 1, - simp_tac (HOL_basic_ss addsimps dest_convs_standard) 1])); - val surjective = timeit_msg "record extension surjective proof:" surjective_prf; - - fun split_meta_prf () = - prove_standard [] split_meta_prop (fn _ => - EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1, - etac meta_allE 1, atac 1, - rtac (prop_subst OF [surjective]) 1, - REPEAT (etac meta_allE 1), atac 1]); - val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf; - - - val (([inject',induct',cases',surjective',split_meta'], + val (([inject',induct',surjective',split_meta',ext_def'], [dest_convs',upd_convs']), thm_thy) = defs_thy |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name)) [("ext_inject", inject), ("ext_induct", induct), - ("ext_cases", cases), ("ext_surjective", surjective), - ("ext_split", split_meta)] - ||>> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name)) - [("dest_convs", dest_convs_standard), ("upd_convs", upd_convs)] - - in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs') + ("ext_split", split_meta), + ("ext_def", ext_def)] + + in (thm_thy,extT,induct',inject',split_meta',ext_def') end; fun chunks [] [] = [] @@ -1826,7 +1827,7 @@ val all_named_vars_more = all_named_vars @ [(full_moreN,more)]; (* 1st stage: extension_thy *) - val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs,ext_split,u_convs) = + val (extension_thy,extT,ext_induct,ext_inject,ext_split,ext_def) = thy |> Sign.add_path bname |> extension_definition full extN fields names alphas_ext zeta moreT more vars; @@ -1862,6 +1863,9 @@ val r_rec0 = mk_rec all_vars_more 0; val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0; + val r_rec0_Vars = let + fun to_Var (Free (c, T)) = Var ((c, 0), T); + in mk_rec (map to_Var all_vars_more) 0 end; fun r n = Free (rN, rec_schemeT n) val r0 = r 0; @@ -1916,21 +1920,63 @@ [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn), (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; + + (* Theorems from the istuple intros. + This is complex enough to deserve a full comment. + By unfolding ext_defs from r_rec0 we create a tree of constructor + calls (many of them Pair, but others as well). The introduction + rules for update_accessor_eq_assist can unify two different ways + on these constructors. If we take the complete result sequence of + running a the introduction tactic, we get one theorem for each upd/acc + pair, from which we can derive the bodies of our selector and + updator and their convs. *) + fun get_access_update_thms () = let + val cterm_rec = cterm_of extension_thy r_rec0; + val cterm_vrs = cterm_of extension_thy r_rec0_Vars; + val insts = [("v", cterm_rec), ("v'", cterm_vrs)]; + val init_thm = named_cterm_instantiate insts updacc_eq_triv; + val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1; + val tactic = simp_tac (HOL_basic_ss addsimps ext_defs) 1 + THEN REPEAT (intros_tac 1 ORELSE terminal); + val updaccs = Seq.list_of (tactic init_thm); + in + (updaccs RL [updacc_accessor_eqE], + updaccs RL [updacc_updator_eqE], + updaccs RL [updacc_cong_from_eq]) + end; + val (accessor_thms, updator_thms, upd_acc_cong_assists) = + timeit_msg "record getting tree access/updates:" get_access_update_thms; + + fun lastN xs = List.drop (xs, parent_fields_len); + (*selectors*) - fun mk_sel_spec (c,T) = - Const (mk_selC rec_schemeT0 (c,T)) - :== (lambda r0 (Const (mk_selC extT (suffix ext_dest c,T))$parent_more r0)); - val sel_specs = map mk_sel_spec fields_more; + fun mk_sel_spec ((c,T), thm) = + let + val (acc $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop + o Envir.beta_eta_contract o concl_of) thm; + val _ = if (arg aconv r_rec0) then () + else raise TERM ("mk_sel_spec: different arg", [arg]); + in + Const (mk_selC rec_schemeT0 (c,T)) + :== acc + end; + val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms); (*updates*) - fun mk_upd_spec (c,T) = + fun mk_upd_spec ((c,T), thm) = let - val new = mk_upd' updN c (Free (base c,T-->T)) extT(*(parent_more r0)*); - in Const (mk_updC updateN rec_schemeT0 (c,T))$(Free (base c,T-->T))$r0 - :== (parent_more_upd new r0) + val (upd $ _ $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop + o Envir.beta_eta_contract o concl_of) thm; + val _ = if (arg aconv r_rec0) then () + else raise TERM ("mk_sel_spec: different arg", [arg]); + in Const (mk_updC updateN rec_schemeT0 (c,T)) + :== upd end; - val upd_specs = map mk_upd_spec fields_more; + val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms); (*derived operations*) val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :== @@ -2052,16 +2098,26 @@ val ss = get_simpset defs_thy; fun sel_convs_prf () = map (prove_simp false ss - (sel_defs@ext_dest_convs)) sel_conv_props; + (sel_defs@accessor_thms)) sel_conv_props; val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf; fun sel_convs_standard_prf () = map standard sel_convs val sel_convs_standard = timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf; - fun upd_convs_prf () = - map (prove_simp true ss (upd_defs@u_convs)) upd_conv_props; - + fun upd_convs_prf () = map (prove_simp false ss + (upd_defs@updator_thms)) upd_conv_props; val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf; + fun upd_convs_standard_prf () = map standard upd_convs + val upd_convs_standard = + timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf; + + fun get_upd_acc_congs () = let + val symdefs = map symmetric (sel_defs @ upd_defs); + val fold_ss = HOL_basic_ss addsimps symdefs; + val ua_congs = map (simplify fold_ss) upd_acc_cong_assists; + in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end; + val (fold_congs, unfold_congs) = + timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs; val parent_induct = if null parents then [] else [#induct (hd (rev parents))]; @@ -2114,14 +2170,31 @@ THEN simp_all_tac HOL_basic_ss [unit_all_eq1]); val cases = timeit_msg "record cases proof:" cases_prf; + fun surjective_prf () = let + val o_ass_thm = symmetric (mk_meta_eq o_assoc); + val o_reassoc = simplify (HOL_basic_ss addsimps [o_ass_thm]); + val sel_defs' = map o_reassoc sel_defs; + val ss = HOL_basic_ss addsimps (ext_defs @ sel_defs'); + in + prove_standard [] surjective_prop (fn prems => + (EVERY [rtac surject_assist_idE 1, + simp_tac ss 1, + REPEAT (intros_tac 1 ORELSE + (rtac surject_assistI 1 THEN + simp_tac (HOL_basic_ss addsimps id_o_apps) 1))])) + end; + val surjective = timeit_msg "record surjective proof:" surjective_prf; + fun split_meta_prf () = - prove false [] split_meta_prop (fn _ => + prove false [] split_meta_prop (fn prems => EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1, etac meta_allE 1, atac 1, rtac (prop_subst OF [surjective]) 1, REPEAT (etac meta_allE 1), atac 1]); val split_meta = timeit_msg "record split_meta proof:" split_meta_prf; - val split_meta_standard = standard split_meta; + fun split_meta_standardise () = standard split_meta; + val split_meta_standard = timeit_msg "record split_meta standard:" + split_meta_standardise; fun split_object_prf_opt () = let @@ -2155,16 +2228,16 @@ fun split_ex_prf () = - prove_standard [] split_ex_prop (fn _ => - EVERY [rtac iffI 1, - etac exE 1, - simp_tac (HOL_basic_ss addsimps [split_meta_standard]) 1, - ex_inst_tac 1, - (*REPEAT (rtac exI 1),*) - atac 1, - REPEAT (etac exE 1), - rtac exI 1, - atac 1]); + let + val ss = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1]; + val [Pv] = 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; + in + prove_standard [] split_ex_prop (fn prems => resolve_tac [so4] 1) + end; val split_ex = timeit_msg "record split_ex proof:" split_ex_prf; fun equality_tac thms = @@ -2183,6 +2256,7 @@ val equality = timeit_msg "record equality proof:" equality_prf; val ((([sel_convs', upd_convs', sel_defs', upd_defs', + fold_congs', unfold_congs', surjective', [split_meta', split_object', split_ex'], derived_defs'], [surjective', equality']), [induct_scheme', induct', cases_scheme', cases']), thms_thy) = @@ -2205,15 +2279,18 @@ val sel_upd_simps = sel_convs' @ upd_convs'; + val sel_upd_defs = sel_defs' @ upd_defs'; val iffs = [ext_inject] + val depth = parent_len + 1; val final_thy = thms_thy |> (snd oo PureThy.add_thmss) [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add, Nitpick_Const_Simps.add]), ((Binding.name "iffs", iffs), [iff_add])] - |> put_record name (make_record_info args parent fields extension induct_scheme') - |> put_sel_upd (names @ [full_moreN]) sel_upd_simps + |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def) + |> put_sel_upd_names full_moreN depth sel_upd_simps + sel_upd_defs (fold_congs', unfold_congs') |> add_record_equalities extension_id equality' |> add_extinjects ext_inject |> add_extsplit extension_name ext_split