# HG changeset patch # User schirmer # Date 1089138666 -7200 # Node ID c5768e8c4da4df89c83ea8808277a6135a2ed2b2 # Parent 97ab70c3d9552ae5614bf0ba8d5599c8129053d1 * record_upd_simproc also simplifies trivial updates: r(|x := x r|) = r * tuned quick and dirty mode diff -r 97ab70c3d955 -r c5768e8c4da4 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Sat Jul 03 15:26:58 2004 +0200 +++ b/src/HOL/Tools/record_package.ML Tue Jul 06 20:31:06 2004 +0200 @@ -24,12 +24,13 @@ sig include BASIC_RECORD_PACKAGE val quiet_mode: bool ref - val record_definition_quick_and_dirty_sensitive: bool ref + val record_quick_and_dirty_sensitive: bool ref val updateN: string val ext_typeN: string val last_extT: typ -> (string * typ list) option val dest_recTs : typ -> (string * typ list) list val get_extension: Sign.sg -> Symtab.key -> (string * typ list) option + val get_extinjects: Sign.sg -> thm list val print_records: theory -> unit val add_record: string list * string -> string option -> (string * string * mixfix) list -> theory -> theory @@ -75,6 +76,8 @@ (*** utilities ***) fun but_last xs = fst (split_last xs); +fun list None = [] + | list (Some x) = [x] (* messages *) @@ -201,14 +204,17 @@ updates: string Symtab.table, simpset: Simplifier.simpset}, equalities: thm Symtab.table, + extinjects: thm list, + extsplit: thm Symtab.table, (* maps extension name to split rule *) splits: (thm*thm*thm*thm) Symtab.table, (* !!,!,EX - split-equalities,induct rule *) extfields: (string*typ) list Symtab.table, (* maps extension to its fields *) fieldext: (string*typ list) Symtab.table (* maps field to its extension *) }; -fun make_record_data records sel_upd equalities splits extfields fieldext = +fun make_record_data + records sel_upd equalities extinjects extsplit splits extfields fieldext = {records = records, sel_upd = sel_upd, - equalities = equalities, splits = splits, + equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, extfields = extfields, fieldext = fieldext }: record_data; structure RecordsArgs = @@ -219,7 +225,7 @@ val empty = make_record_data Symtab.empty {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss} - Symtab.empty Symtab.empty Symtab.empty Symtab.empty; + Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty; val copy = I; val prep_ext = I; @@ -227,12 +233,16 @@ ({records = recs1, sel_upd = {selectors = sels1, updates = upds1, simpset = ss1}, equalities = equalities1, + extinjects = extinjects1, + extsplit = extsplit1, splits = splits1, extfields = extfields1, fieldext = fieldext1}, {records = recs2, sel_upd = {selectors = sels2, updates = upds2, simpset = ss2}, - equalities = equalities2, + equalities = equalities2, + extinjects = extinjects2, + extsplit = extsplit2, splits = splits2, extfields = extfields2, fieldext = fieldext2}) = @@ -242,6 +252,8 @@ updates = Symtab.merge (K true) (upds1, upds2), simpset = Simplifier.merge_ss (ss1, ss2)} (Symtab.merge Thm.eq_thm (equalities1, equalities2)) + (extinjects1 @ extinjects2) + (Symtab.merge Thm.eq_thm (extsplit1,extsplit2)) (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) @@ -277,9 +289,10 @@ fun put_record name info thy = let - val {records, sel_upd, equalities, splits,extfields,fieldext} = RecordsData.get thy; + val {records, sel_upd, equalities, extinjects,extsplit,splits,extfields,fieldext} = + RecordsData.get thy; val data = make_record_data (Symtab.update ((name, info), records)) - sel_upd equalities splits extfields fieldext; + sel_upd equalities extinjects extsplit splits extfields fieldext; in RecordsData.put data thy end; (* access 'sel_upd' *) @@ -302,38 +315,70 @@ val upds = map (suffix updateN) names ~~ names; val {records, sel_upd = {selectors, updates, simpset}, - equalities, splits, extfields,fieldext} = RecordsData.get thy; + equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy; val data = make_record_data records {selectors = Symtab.extend (selectors, sels), updates = Symtab.extend (updates, upds), simpset = Simplifier.addsimps (simpset, simps)} - equalities splits extfields fieldext; + equalities extinjects extsplit splits extfields fieldext; in RecordsData.put data thy end; (* access 'equalities' *) fun add_record_equalities name thm thy = let - val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy; + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = + RecordsData.get thy; val data = make_record_data records sel_upd - (Symtab.update_new ((name, thm), equalities)) splits extfields fieldext; + (Symtab.update_new ((name, thm), equalities)) extinjects extsplit + splits extfields fieldext; in RecordsData.put data thy end; fun get_equalities sg name = Symtab.lookup (#equalities (RecordsData.get_sg sg), name); +(* access 'extinjects' *) + +fun add_extinjects thm thy = + let + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = + RecordsData.get thy; + val data = make_record_data records sel_upd equalities (extinjects@[thm]) extsplit + splits extfields fieldext; + in RecordsData.put data thy end; + +fun get_extinjects sg = #extinjects (RecordsData.get_sg sg); + +(* access 'extsplit' *) + +fun add_extsplit name thm thy = + let + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = + RecordsData.get thy; + val data = make_record_data records sel_upd + equalities extinjects (Symtab.update_new ((name, thm), extsplit)) splits + extfields fieldext; + in RecordsData.put data thy end; + +fun get_extsplit sg name = + Symtab.lookup (#extsplit (RecordsData.get_sg sg), name); + (* access 'splits' *) fun add_record_splits name thmP thy = let - val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy; + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = + RecordsData.get thy; val data = make_record_data records sel_upd - equalities (Symtab.update_new ((name, thmP), splits)) extfields fieldext; + equalities extinjects extsplit (Symtab.update_new ((name, thmP), splits)) + extfields fieldext; in RecordsData.put data thy end; fun get_splits sg name = Symtab.lookup (#splits (RecordsData.get_sg sg), name); + + (* extension of a record name *) fun get_extension sg name = case Symtab.lookup (#records (RecordsData.get_sg sg),name) of @@ -344,9 +389,11 @@ fun add_extfields name fields thy = let - val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy; + val {records, sel_upd, equalities, extinjects, extsplit,splits, extfields, fieldext} = + RecordsData.get thy; val data = make_record_data records sel_upd - equalities splits (Symtab.update_new ((name, fields), extfields)) fieldext; + equalities extinjects extsplit splits + (Symtab.update_new ((name, fields), extfields)) fieldext; in RecordsData.put data thy end; fun get_extfields sg name = @@ -356,10 +403,12 @@ fun add_fieldext extname_types fields thy = let - val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy; + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = + RecordsData.get thy; val fieldext' = foldl (fn (table,field) => Symtab.update_new ((field,extname_types),table)) (fieldext,fields); - val data = make_record_data records sel_upd equalities splits extfields fieldext'; + val data=make_record_data records sel_upd equalities extinjects extsplit + splits extfields fieldext'; in RecordsData.put data thy end; @@ -707,22 +756,41 @@ (list_comb (Syntax.const name_sfx,ts)) in (name_sfx, tr') end; +(** record simprocs **) -(** record simprocs **) -fun quick_and_dirty_prove sg xs asms prop tac = -Tactic.prove_standard sg xs asms prop - (if !quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac); +val record_quick_and_dirty_sensitive = ref false; + +fun quick_and_dirty_prove sg asms prop tac = + if !record_quick_and_dirty_sensitive andalso !quick_and_dirty + then Tactic.prove sg [] [] (Logic.list_implies (map Logic.varify asms,Logic.varify prop)) + (K (SkipProof.cheat_tac HOL.thy)) + (* standard can take quite a while for large records, thats why + * we varify the proposition manually here.*) + else Tactic.prove_standard sg [] asms prop tac; fun prove_split_simp sg T prop = (case get_splits sg (rec_id T) of Some (all_thm,_,_,_) - => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg; - in (quick_and_dirty_prove sg [] [] prop - (K (simp_tac (simpset addsimps [all_thm]) 1))) + => let + val {sel_upd={simpset,...},extsplit,...} = RecordsData.get_sg sg; + val extsplits = + foldl (fn (thms,(n,_)) => (list (Symtab.lookup (extsplit,n)))@thms) + ([],dest_recTs T); + val thms = all_thm::(case extsplits of [thm] => [] | _ => extsplits); + (* [thm] is the same as all_thm *) + in (quick_and_dirty_prove sg [] prop + (fn _ => (simp_tac (simpset addsimps thms) 1))) end | _ => error "RecordPackage.prove_split_simp:code should never been reached") + + +local +fun get_fields extfields T = + foldl (fn (xs,(eN,_))=>xs@(map fst (Symtab.lookup_multi (extfields,eN)))) + ([],(dest_recTs T)); +in (* record_simproc *) (* Simplifies selections of an record update: * (1) S (r(|S:=k|)) = k respectively @@ -738,15 +806,13 @@ val record_simproc = Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"] (fn sg => fn _ => fn t => - (case t of (sel as Const (s, Type (_,[domS,rangeS]))) $ ((upd as Const (u, _)) $ k $ r) => + (case t of (sel as Const (s, Type (_,[domS,rangeS])))$((upd as Const (u, _)) $ k $ r)=> (case get_selectors sg s of Some () => (case get_updates sg u of Some u_name => let fun mk_abs_var x t = (x, fastype_of t); val {sel_upd={updates,...},extfields,...} = RecordsData.get_sg sg; - fun flds T = - foldl (fn (xs,(eN,_))=>xs@(map fst (Symtab.lookup_multi (extfields,eN)))) - ([],(dest_recTs T)); + fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) = (case (Symtab.lookup (updates,u)) of None => None @@ -758,8 +824,8 @@ val kv = mk_abs_var "k" k val kb = Bound 1 in Some (upd$kb$rb,kb,[kv,rv],true) end - else if u_name mem (flds rangeS) - orelse s mem (flds updT) + else if u_name mem (get_fields extfields rangeS) + orelse s mem (get_fields extfields updT) then None else (case mk_eq_terms r of Some (trm,trm',vars,update_s) @@ -789,6 +855,114 @@ | None => None) | _ => None)); +(* record_upd_simproc *) +(* simplify multiple updates: + * (1) "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)" + * (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|) +*) +val record_upd_simproc = + Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u k r)"] + (fn sg => fn _ => fn t => + (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) => + let datatype ('a,'b) calc = Init of 'b | Inter of 'a + val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get_sg sg; + + fun mk_abs_var x t = (x, fastype_of t); + fun sel_name u = NameSpace.base (unsuffix updateN u); + + fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) = + if s mem (get_fields extfields mT) then upd else seed s r + | seed _ r = r; + + fun grow u uT k vars (sprout,skeleton) = + if sel_name u = moreN + then let val kv = mk_abs_var "k" k; + val kb = Bound (length vars); + in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end + else ((sprout,skeleton),vars); + + fun is_upd_same (sprout,skeleton) u ((sel as Const (s,_))$r) = + if (unsuffix updateN u) = s andalso (seed s sprout) = r + then Some (sel,seed s skeleton) + else None + | is_upd_same _ _ _ = None + + fun init_seed r = ((r,Bound 0), [mk_abs_var "r" r]); + + (* 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)) $ k $ r)) = + if is_some (Symtab.lookup (upds,u)) + then let + fun rest already = mk_updterm upds already + in if is_some (Symtab.lookup (already,u)) + then (case (rest already r) of + Init ((sprout,skel),vars) => + let + val kv = mk_abs_var (sel_name u) k; + val kb = Bound (length vars); + val (sprout',vars')= grow u uT k (kv::vars) (sprout,skel); + in Inter (upd$kb$skel,skel,vars',sprout') end + | Inter (trm,trm',vars,sprout) => + let + val kv = mk_abs_var (sel_name u) k; + val kb = Bound (length vars); + val (sprout',vars') = grow u uT k (kv::vars) sprout; + in Inter(upd$kb$trm,trm',kv::vars',sprout') end) + else + (case rest (Symtab.update ((u,()),already)) r of + Init ((sprout,skel),vars) => + (case is_upd_same (sprout,skel) u k of + Some (sel,skel') => + let + val (sprout',vars') = grow u uT k vars (sprout,skel); + in Inter(upd$(sel$skel')$skel,skel,vars',sprout') end + | None => + let + val kv = mk_abs_var (sel_name u) k; + val kb = Bound (length vars); + in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end) + | Inter (trm,trm',vars,sprout) => + (case is_upd_same sprout u k of + Some (sel,skel) => + let + val (sprout',vars') = grow u uT k vars sprout + in Inter(upd$(sel$skel)$trm,trm',vars',sprout') end + | None => + let + val kv = mk_abs_var (sel_name u) k + val kb = Bound (length vars) + val (sprout',vars') = grow u uT k (kv::vars) sprout + in Inter (upd$kb$trm,upd$kb$trm',vars',sprout') end)) + end + else Init (init_seed t) + | mk_updterm _ _ t = Init (init_seed t); + + in (case mk_updterm updates Symtab.empty t of + Inter (trm,trm',vars,_) + => Some (prove_split_simp sg T + (list_all(vars,(Logic.mk_equals (trm,trm'))))) + | _ => None) + end + | _ => None)); +end + (* record_eq_simproc *) (* looks up the most specific record-equality. * Note on efficiency: @@ -813,52 +987,6 @@ | Some thm => Some (thm RS Eq_TrueI))) | _ => None)); - -(* record_upd_simproc *) -(* simplify multiple updates; for example: "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)" *) -val record_upd_simproc = - Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u1 k1 (u2 k2 r))"] - (fn sg => fn _ => fn t => - (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) => - let val {sel_upd={updates,...},...} = RecordsData.get_sg sg; - fun mk_abs_var x t = (x, fastype_of t); - - fun mk_updterm upds already ((upd as Const (u,_)) $ k $ r) = - if is_some (Symtab.lookup (upds,u)) - then let - fun rest already = mk_updterm upds already - in if is_some (Symtab.lookup (already,u)) - then (case (rest already r) of - None => let - val rv = mk_abs_var "r" r - val rb = Bound 0 - val kv = mk_abs_var "k" k - val kb = Bound 1 - in Some (upd$kb$rb,rb,[kv,rv]) end - | Some (trm,trm',vars) - => let - val kv = mk_abs_var "k" k - val kb = Bound (length vars) - in Some (upd$kb$trm,trm',kv::vars) end) - else (case rest (Symtab.update ((u,()),already)) r of - None => None - | Some (trm,trm',vars) - => let - val kv = mk_abs_var "k" k - val kb = Bound (length vars) - in Some (upd$kb$trm,upd$kb$trm',kv::vars) end) - end - else None - | mk_updterm _ _ _ = None; - - in (case mk_updterm updates Symtab.empty t of - Some (trm,trm',vars) - => Some (prove_split_simp sg T - (list_all(vars,(Logic.mk_equals (trm,trm'))))) - | None => None) - end - | _ => None)); - (* record_split_simproc *) (* splits quantified occurrences of records, for which P holds. P can peek on the * subterm starting at the quantified occurrence of the record (including the quantifier) @@ -888,7 +1016,7 @@ Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"] (fn sg => fn _ => fn t => let - fun prove prop = (quick_and_dirty_prove sg [] [] prop + fun prove prop = (quick_and_dirty_prove sg [] prop (fn _ => (simp_tac ((get_simpset sg) addsimps simp_thms addsimprocs [record_split_simproc (K true)]) 1))); @@ -1068,16 +1196,6 @@ (x, list_abs (params, Bound 0))])) rule' in compose_tac (false, rule'', nprems_of rule) i st end; - -val record_definition_quick_and_dirty_sensitive = ref false; - -(* fun is crucial here; val would evaluate only once! *) -fun definition_prove_standard sg = - if !record_definition_quick_and_dirty_sensitive - then quick_and_dirty_prove sg - else Tactic.prove_standard sg; - - fun extension_typedef name repT alphas thy = let val UNIV = HOLogic.mk_UNIV repT; @@ -1147,10 +1265,11 @@ val vars_more = vars@[more]; val named_vars_more = (names@[full moreN])~~vars_more; + val variants = map (fn (Free (x,_))=>x) vars_more; val ext = list_comb (Const ext_decl,vars_more); val s = Free (rN, extT); - val P = Free (variant (map (fn (Free (x,_))=>x) vars_more) "P", extT-->HOLogic.boolT); - val C = Free (variant (map (fn (Free (x,_))=>x) vars_more) "C", HOLogic.boolT); + val P = Free (variant variants "P", extT-->HOLogic.boolT); + val C = Free (variant variants "C", HOLogic.boolT); val inject_prop = let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more; @@ -1174,10 +1293,21 @@ val dest_conv_props = map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more; - val prove_standard = definition_prove_standard (Theory.sign_of defs_thy); + val surjective_prop = + let val args = + map (fn (c, Free (_,T)) => mk_sel s (suffix ext_dest c,T)) named_vars_more; + in s === list_comb (Const ext_decl, args) end; + + val split_meta_prop = + let val P = Free (variant variants "P", extT-->Term.propT) in + Logic.mk_equals + (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext)) + end; + + val prove_standard = quick_and_dirty_prove (Theory.sign_of defs_thy); fun prove_simp simps = let val tac = simp_all_tac HOL_ss simps - in fn prop => prove_standard [] [] prop (K tac) end; + in fn prop => prove_standard [] prop (K tac) end; (* prove propositions *) @@ -1186,7 +1316,7 @@ fun induct_prf () = let val (assm, concl) = induct_prop - in prove_standard [] [assm] concl (fn prems => + 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]) @@ -1194,7 +1324,7 @@ val induct = timeit_msg "record extension induct proof:" induct_prf; fun cases_prf () = - prove_standard [] [] cases_prop (fn prems => + prove_standard [] cases_prop (fn prems => EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1, try_param_tac rN induct 1, rtac impI 1, @@ -1207,16 +1337,33 @@ ([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; - val (thm_thy,([inject',induct',cases'],[dest_convs'])) = + fun surjective_prf () = + prove_standard [] surjective_prop (fn prems => + (EVERY [try_param_tac rN induct 1, + simp_tac (HOL_basic_ss addsimps dest_convs) 1])); + val surjective = timeit_msg "record extension surjective proof:" surjective_prf; + + fun split_meta_prf () = + prove_standard [] split_meta_prop (fn prems => + EVERY [rtac equal_intr_rule 1, + rtac meta_allE 1, etac triv_goal 1, atac 1, + rtac (prop_subst OF [surjective]) 1, + REPEAT (EVERY [rtac meta_allE 1, etac triv_goal 1, etac thin_rl 1]), + atac 1]); + val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf; + + val (thm_thy,([inject',induct',cases',surjective',split_meta'],[dest_convs'])) = defs_thy |> (PureThy.add_thms o map Thm.no_attributes) [("ext_inject", inject), ("ext_induct", induct), - ("ext_cases", cases)] + ("ext_cases", cases), + ("ext_surjective", surjective), + ("ext_split", split_meta)] |>>> (PureThy.add_thmss o map Thm.no_attributes) [("dest_convs",dest_convs)] - in (thm_thy,extT,induct',inject',dest_convs') + in (thm_thy,extT,induct',inject',dest_convs',split_meta') end; fun chunks [] [] = [] @@ -1295,7 +1442,7 @@ (* 1st stage: extension_thy *) - val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs) = + val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs,ext_split) = thy |> Theory.add_path bname |> extension_definition full extN fields names alphas_ext zeta moreT more vars; @@ -1501,10 +1648,10 @@ (* 3rd stage: thms_thy *) - val prove_standard = definition_prove_standard (Theory.sign_of defs_thy); + val prove_standard = quick_and_dirty_prove (Theory.sign_of defs_thy); fun prove_simp ss simps = let val tac = simp_all_tac ss simps - in fn prop => prove_standard [] [] prop (K tac) end; + in fn prop => prove_standard [] prop (K tac) end; val ss = get_simpset (sign_of defs_thy); @@ -1518,7 +1665,7 @@ val parent_induct = if null parents then [] else [#induct (hd (rev parents))]; - fun induct_scheme_prf () = prove_standard [] [] induct_scheme_prop (fn prems => + fun induct_scheme_prf () = prove_standard [] induct_scheme_prop (fn prems => (EVERY [if null parent_induct then all_tac else try_param_tac rN (hd parent_induct) 1, try_param_tac rN ext_induct 1, @@ -1528,7 +1675,7 @@ fun induct_prf () = let val (assm, concl) = induct_prop; in - prove_standard [] [assm] concl (fn prems => + prove_standard [assm] concl (fn prems => try_param_tac rN induct_scheme 1 THEN try_param_tac "more" unit_induct 1 THEN resolve_tac prems 1) @@ -1536,13 +1683,13 @@ val induct = timeit_msg "record induct proof:" induct_prf; fun surjective_prf () = - prove_standard [] [] surjective_prop (fn prems => + prove_standard [] surjective_prop (fn prems => (EVERY [try_param_tac rN induct_scheme 1, simp_tac (ss addsimps sel_convs) 1])) val surjective = timeit_msg "record surjective proof:" surjective_prf; fun cases_scheme_prf () = - prove_standard [] [] cases_scheme_prop (fn prems => + prove_standard [] cases_scheme_prop (fn prems => EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1, try_param_tac rN induct_scheme 1, rtac impI 1, @@ -1552,13 +1699,13 @@ val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf; fun cases_prf () = - prove_standard [] [] cases_prop (fn _ => + prove_standard [] cases_prop (fn _ => try_param_tac rN cases_scheme 1 THEN simp_all_tac HOL_basic_ss [unit_all_eq1]); val cases = timeit_msg "record cases proof:" cases_prf; fun split_meta_prf () = - prove_standard [] [] split_meta_prop (fn prems => + prove_standard [] split_meta_prop (fn prems => EVERY [rtac equal_intr_rule 1, rtac meta_allE 1, etac triv_goal 1, atac 1, rtac (prop_subst OF [surjective]) 1, @@ -1567,7 +1714,7 @@ val split_meta = timeit_msg "record split_meta proof:" split_meta_prf; fun split_object_prf () = - prove_standard [] [] split_object_prop (fn prems => + prove_standard [] split_object_prop (fn prems => EVERY [rtac iffI 1, REPEAT (rtac allI 1), etac allE 1, atac 1, rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]); @@ -1575,7 +1722,7 @@ fun split_ex_prf () = - prove_standard [] [] split_ex_prop (fn prems => + prove_standard [] split_ex_prop (fn prems => EVERY [rtac iffI 1, etac exE 1, simp_tac (HOL_basic_ss addsimps [split_meta]) 1, @@ -1592,14 +1739,14 @@ val eqs' = map (simplify ss') eqs; in simp_tac (HOL_basic_ss addsimps (s'::s::eqs')) 1 end; - fun equality_prf () = prove_standard [] [] equality_prop (fn _ => + fun equality_prf () = prove_standard [] equality_prop (fn _ => fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in st |> (res_inst_tac [(rN, s)] cases_scheme 1 THEN res_inst_tac [(rN, s')] cases_scheme 1 THEN (METAHYPS equality_tac 1)) (* simp_all_tac ss (sel_convs) would also work but is less efficient *) end); - val equality = timeit_msg "record equality proof':" equality_prf; + val equality = timeit_msg "record equality proof:" equality_prf; val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'], derived_defs'], @@ -1632,6 +1779,8 @@ |> put_record name (make_record_info args parent fields extension induct_scheme') |> put_sel_upd (names @ [full_moreN]) sel_upd_simps |> add_record_equalities extension_id equality' + |> add_extinjects ext_inject + |> add_extsplit extension_name ext_split |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme') |> add_extfields extension_name (fields @ [(full_moreN,moreT)]) |> add_fieldext (extension_name,snd extension) (names @ [full_moreN])