# HG changeset patch # User wenzelm # Date 1325187179 -3600 # Node ID 1e184c0d88be43f471c7598ab21011e18b4ac9fe # Parent 1e3ff542e83ead6cdea05af9f5de081ba62d0ae3# Parent 6170af176fbb392912e06e9a2e28fa6b1a2a674f merged diff -r 1e3ff542e83e -r 1e184c0d88be src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Thu Dec 29 18:54:07 2011 +0100 +++ b/src/HOL/Tools/Function/function_common.ML Thu Dec 29 20:32:59 2011 +0100 @@ -68,6 +68,7 @@ (* Termination rules *) +(* FIXME just one data slot (record) per program unit *) structure TerminationRule = Generic_Data ( type T = thm list @@ -108,6 +109,7 @@ defname = name defname, is_partial=is_partial } end +(* FIXME just one data slot (record) per program unit *) structure FunctionData = Generic_Data ( type T = (term * info) Item_Net.T; @@ -168,6 +170,7 @@ (* Default Termination Prover *) +(* FIXME just one data slot (record) per program unit *) structure TerminationProver = Generic_Data ( type T = Proof.context -> tactic @@ -321,6 +324,7 @@ (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) end +(* FIXME just one data slot (record) per program unit *) structure Preprocessor = Generic_Data ( type T = preproc diff -r 1e3ff542e83e -r 1e184c0d88be src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Thu Dec 29 18:54:07 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Thu Dec 29 20:32:59 2011 +0100 @@ -428,6 +428,8 @@ (** generator compiliation **) +(* FIXME just one data slot (record) per program unit *) + structure Counterexample = Proof_Data ( type T = unit -> int -> bool -> int -> (bool * term list) option diff -r 1e3ff542e83e -r 1e184c0d88be src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Dec 29 18:54:07 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Dec 29 20:32:59 2011 +0100 @@ -313,7 +313,8 @@ in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end; (** counterexample generator **) - + +(* FIXME just one data slot (record) per program unit *) structure Counterexample = Proof_Data ( type T = unit -> (bool * term list) option @@ -330,6 +331,7 @@ | map_counterexample f (Existential_Counterexample cs) = Existential_Counterexample (map (fn (t, c) => (f t, map_counterexample f c)) cs) +(* FIXME just one data slot (record) per program unit *) structure Existential_Counterexample = Proof_Data ( type T = unit -> counterexample option diff -r 1e3ff542e83e -r 1e184c0d88be src/HOL/Tools/SMT/smt_builtin.ML --- a/src/HOL/Tools/SMT/smt_builtin.ML Thu Dec 29 18:54:07 2011 +0100 +++ b/src/HOL/Tools/SMT/smt_builtin.ML Thu Dec 29 20:32:59 2011 +0100 @@ -94,6 +94,7 @@ (* built-in types *) +(* FIXME just one data slot (record) per program unit *) structure Builtin_Types = Generic_Data ( type T = @@ -148,6 +149,7 @@ type bfunr = string * int * term list * (term list -> term) +(* FIXME just one data slot (record) per program unit *) structure Builtin_Funcs = Generic_Data ( type T = (term list bfun, bfunr option bfun) btab diff -r 1e3ff542e83e -r 1e184c0d88be src/HOL/Tools/SMT/smt_config.ML --- a/src/HOL/Tools/SMT/smt_config.ML Thu Dec 29 18:54:07 2011 +0100 +++ b/src/HOL/Tools/SMT/smt_config.ML Thu Dec 29 20:32:59 2011 +0100 @@ -64,6 +64,7 @@ avail: unit -> bool, options: Proof.context -> string list } +(* FIXME just one data slot (record) per program unit *) structure Solvers = Generic_Data ( type T = (solver_info * string list) Symtab.table * string option @@ -182,6 +183,7 @@ (* certificates *) +(* FIXME just one data slot (record) per program unit *) structure Certificates = Generic_Data ( type T = Cache_IO.cache option diff -r 1e3ff542e83e -r 1e184c0d88be src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Dec 29 18:54:07 2011 +0100 +++ b/src/HOL/Tools/record.ML Thu Dec 29 20:32:59 2011 +0100 @@ -109,11 +109,10 @@ let val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT; val vs = map (Proof_Context.check_tfree ctxt) raw_vs; - val tac = Tactic.rtac UNIV_witness 1; in thy |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn) - (HOLogic.mk_UNIV repT) NONE tac + (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1) |-> (fn (tyco, info) => get_typedef_info tyco vs info) end; @@ -194,18 +193,6 @@ structure Record: RECORD = struct -val eq_reflection = @{thm eq_reflection}; -val meta_allE = @{thm Pure.meta_allE}; -val prop_subst = @{thm prop_subst}; -val K_record_comp = @{thm K_record_comp}; -val K_comp_convs = [@{thm o_apply}, K_record_comp]; -val o_assoc = @{thm o_assoc}; -val id_apply = @{thm id_apply}; -val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}]; -val Not_eq_iff = @{thm Not_eq_iff}; - -val refl_conj_eq = @{thm refl_conj_eq}; - val surject_assistI = @{thm iso_tuple_surjective_proof_assistI}; val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE}; @@ -222,10 +209,6 @@ val updacc_cong_triv = @{thm update_accessor_cong_assist_triv}; val updacc_cong_from_eq = @{thm iso_tuple_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 **) @@ -396,10 +379,10 @@ sel_upd: {selectors: (int * bool) Symtab.table, updates: string Symtab.table, - simpset: Simplifier.simpset, - defset: Simplifier.simpset, - foldcong: Simplifier.simpset, - unfoldcong: Simplifier.simpset}, + simpset: simpset, + defset: simpset, + foldcong: simpset, + unfoldcong: simpset}, equalities: thm Symtab.table, extinjects: thm list, extsplit: thm Symtab.table, (*maps extension name to split rule*) @@ -511,8 +494,8 @@ val data = make_data records {selectors = fold Symtab.update_new sels selectors, updates = fold Symtab.update_new upds updates, - simpset = Simplifier.addsimps (simpset, simps), - defset = Simplifier.addsimps (defset, defs), + simpset = simpset addsimps simps, + defset = defset addsimps defs, foldcong = foldcong |> fold Simplifier.add_cong folds, unfoldcong = unfoldcong |> fold Simplifier.add_cong unfolds} equalities extinjects extsplit splits extfields fieldext; @@ -910,9 +893,9 @@ val _ = null fields andalso raise Match; val u = foldr1 fields_tr' (map field_tr' fields); in - case more of + (case more of Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u - | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more + | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more) end; in @@ -966,7 +949,7 @@ (** record simprocs **) -fun future_forward_prf_standard thy prf prop () = +fun future_forward_prf thy prf prop = let val thm = if ! quick_and_dirty then Skip_Proof.make_thm thy prop else if Goal.future_enabled () then @@ -974,18 +957,6 @@ else prf () in Drule.export_without_context thm end; -fun prove_common immediate stndrd thy asms prop tac = - let - val prv = - if ! quick_and_dirty then Skip_Proof.prove - else if immediate orelse not (Goal.future_enabled ()) then Goal.prove - else Goal.prove_future; - val prf = prv (Proof_Context.init_global thy) [] asms prop tac; - in if stndrd then Drule.export_without_context prf else prf end; - -val prove_future_global = prove_common false; -val prove_global = prove_common true; - fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) = (case get_updates thy u of SOME u_name => u_name = s @@ -1017,11 +988,11 @@ (fn _ => simp_tac defset 1 THEN REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN - TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)); + TRY (simp_tac (HOL_ss addsimps @{thms id_apply id_o o_id}) 1)); val dest = if is_sel_upd_pair thy acc upd - then o_eq_dest - else o_eq_id_dest; + then @{thm o_eq_dest} + else @{thm o_eq_id_dest}; in Drule.export_without_context (othm RS dest) end; in map get_simp upd_funs end; @@ -1041,8 +1012,8 @@ (fn _ => simp_tac defset 1 THEN REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN - TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)); - val dest = if comp then o_eq_dest_lhs else o_eq_dest; + TRY (simp_tac (HOL_ss addsimps @{thms id_apply}) 1)); + val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest}; in Drule.export_without_context (othm RS dest) end; fun get_updupd_simps thy term defset = @@ -1080,7 +1051,7 @@ in Goal.prove (Proof_Context.init_global thy) [] [] prop' (fn _ => - simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN + simp_tac (HOL_basic_ss addsimps (simps @ @{thms K_record_comp})) 1 THEN TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1)) end; @@ -1348,8 +1319,8 @@ SOME (case quantifier of @{const_name all} => all_thm - | @{const_name All} => All_thm RS eq_reflection - | @{const_name Ex} => Ex_thm RS eq_reflection + | @{const_name All} => All_thm RS @{thm eq_reflection} + | @{const_name Ex} => Ex_thm RS @{thm eq_reflection} | _ => raise Fail "split_simproc")) else NONE end) @@ -1361,7 +1332,7 @@ (fn thy => fn ss => fn t => let fun prove prop = - prove_global true thy [] prop + Skip_Proof.prove_global thy [] [] prop (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy) addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1); @@ -1449,10 +1420,10 @@ end)); val simprocs = if has_rec goal then [split_simproc P] else []; - val thms' = K_comp_convs @ thms; + val thms' = @{thms o_apply K_record_comp} @ thms; in EVERY split_frees_tacs THEN - Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i + full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i end); @@ -1473,7 +1444,7 @@ | is_all _ = 0; in if has_rec goal then - Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i + full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i else no_tac end); @@ -1496,8 +1467,6 @@ (* tactics *) -fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps)); - (*Do case analysis / induction according to rule on last parameter of ith subgoal (or on s if there are no parameters). Instatiation of record variable (and predicate) in rule is calculated to @@ -1591,9 +1560,8 @@ (* 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 ctxt "record extension nested type def:" get_meta_tree; + val (ext_body, typ_thy) = timeit_msg ctxt "record extension nested type def:" (fn () => + build_meta_tree_type 1 thy vars more); (* prepare declarations and definitions *) @@ -1603,13 +1571,11 @@ fun mk_ext args = list_comb (Const (ext_name, ext_type), args); val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body); - fun mk_defs () = + val ([ext_def], defs_thy) = timeit_msg ctxt "record extension constructor def:" (fn () => typ_thy |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])] - ||> Theory.checkpoint - val ([ext_def], defs_thy) = - timeit_msg ctxt "record extension constructor def:" mk_defs; + ||> Theory.checkpoint); (* prepare propositions *) @@ -1639,19 +1605,18 @@ (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext)) end; - val prove_standard = prove_future_global true defs_thy; - - fun inject_prf () = + val prove = Skip_Proof.prove_global defs_thy; + + val inject = timeit_msg ctxt "record extension inject proof:" (fn () => simplify HOL_ss - (prove_standard [] inject_prop + (prove [] [] inject_prop (fn _ => simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN REPEAT_DETERM - (rtac refl_conj_eq 1 ORELSE + (rtac @{thm refl_conj_eq} 1 ORELSE Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE - rtac refl 1))); - - val inject = timeit_msg ctxt "record extension inject proof:" inject_prf; + rtac refl 1)))); + (*We need a surjection property r = (| f = f r, g = g r ... |) to prove other theorems. We haven't given names to the accessors @@ -1660,7 +1625,7 @@ operate on it as far as it can. We then use Drule.export_without_context to convert the free variables into unifiable variables and unify them with (roughly) the definition of the accessor.*) - fun surject_prf () = + val surject = timeit_msg ctxt "record extension surjective proof:" (fn () => let val cterm_ext = cterm_of defs_thy ext; val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE; @@ -1672,28 +1637,26 @@ val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway)); in surject - end; - val surject = timeit_msg ctxt "record extension surjective proof:" surject_prf; - - fun split_meta_prf () = - prove_standard [] split_meta_prop + end); + + + val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () => + prove [] [] split_meta_prop (fn _ => EVERY1 [rtac equal_intr_rule, Goal.norm_hhf_tac, - etac meta_allE, atac, - rtac (prop_subst OF [surject]), - REPEAT o etac meta_allE, atac]); - val split_meta = timeit_msg ctxt "record extension split_meta proof:" split_meta_prf; - - fun induct_prf () = + etac @{thm meta_allE}, atac, + rtac (@{thm prop_subst} OF [surject]), + REPEAT o etac @{thm meta_allE}, atac])); + + val induct = timeit_msg ctxt "record extension induct proof:" (fn () => let val (assm, concl) = induct_prop in - prove_standard [assm] concl + prove [] [assm] concl (fn {prems, ...} => cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN resolve_tac prems 2 THEN asm_simp_tac HOL_ss 1) - end; - val induct = timeit_msg ctxt "record extension induct proof:" induct_prf; + end); val ([induct', inject', surjective', split_meta'], thm_thy) = defs_thy @@ -1828,10 +1791,11 @@ Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)); fun tac eq_def = Class.intro_classes_tac [] - THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def]) + THEN rewrite_goals_tac [Simpdata.mk_eq eq_def] THEN ALLGOALS (rtac @{thm refl}); - fun mk_eq thy eq_def = Simplifier.rewrite_rule - [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject; + fun mk_eq thy eq_def = + Simplifier.rewrite_rule + [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject; fun mk_eq_refl thy = @{thm equal_refl} |> Thm.instantiate @@ -2002,31 +1966,30 @@ 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 r_rec0_Vars = - let - (*pick variable indices of 1 to avoid possible variable - collisions with existing variables in updacc_eq_triv*) - fun to_Var (Free (c, T)) = Var ((c, 1), T); - in mk_rec (map to_Var all_vars_more) 0 end; - - val cterm_rec = cterm_of ext_thy r_rec0; - val cterm_vrs = cterm_of ext_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 (Iso_Tuple_Support.iso_tuple_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 ctxt "record getting tree access/updates:" get_access_update_thms; + timeit_msg ctxt "record getting tree access/updates:" (fn () => + let + val r_rec0_Vars = + let + (*pick variable indices of 1 to avoid possible variable + collisions with existing variables in updacc_eq_triv*) + fun to_Var (Free (c, T)) = Var ((c, 1), T); + in mk_rec (map to_Var all_vars_more) 0 end; + + val cterm_rec = cterm_of ext_thy r_rec0; + val cterm_vrs = cterm_of ext_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 (Iso_Tuple_Support.iso_tuple_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); fun lastN xs = drop parent_fields_len xs; @@ -2071,29 +2034,28 @@ (* 2st stage: defs_thy *) - fun mk_defs () = - ext_thy - |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, []) - |> Sign.restore_naming thy - |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd - |> Typedecl.abbrev_global - (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd - |> Sign.qualified_path false binding - |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx)) - (sel_decls ~~ (field_syntax @ [NoSyn])) - |> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn)) - (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl]) - |> (Global_Theory.add_defs false o - map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs - ||>> (Global_Theory.add_defs false o - map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs - ||>> (Global_Theory.add_defs false o - map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) - [make_spec, fields_spec, extend_spec, truncate_spec] - ||> Theory.checkpoint val (((sel_defs, upd_defs), derived_defs), defs_thy) = timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:" - mk_defs; + (fn () => + ext_thy + |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, []) + |> Sign.restore_naming thy + |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd + |> Typedecl.abbrev_global + (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd + |> Sign.qualified_path false binding + |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx)) + (sel_decls ~~ (field_syntax @ [NoSyn])) + |> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn)) + (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl]) + |> (Global_Theory.add_defs false o + map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs + ||>> (Global_Theory.add_defs false o + map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs + ||>> (Global_Theory.add_defs false o + map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) + [make_spec, fields_spec, extend_spec, truncate_spec] + ||> Theory.checkpoint); (* prepare propositions *) val _ = timing_msg ctxt "record preparing propositions"; @@ -2164,58 +2126,42 @@ (* 3rd stage: thms_thy *) - fun prove stndrd = prove_future_global stndrd defs_thy; - val prove_standard = prove_future_global true defs_thy; - val future_forward_prf = future_forward_prf_standard defs_thy; - - fun prove_simp stndrd ss simps = - let val tac = simp_all_tac ss simps - in fn prop => prove stndrd [] prop (K tac) end; + val prove = Skip_Proof.prove_global defs_thy; val ss = get_simpset defs_thy; - - fun sel_convs_prf () = - map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props; - val sel_convs = timeit_msg ctxt "record sel_convs proof:" sel_convs_prf; - fun sel_convs_standard_prf () = map Drule.export_without_context sel_convs; - val sel_convs_standard = - timeit_msg ctxt "record sel_convs_standard proof:" sel_convs_standard_prf; - - fun upd_convs_prf () = - map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props; - val upd_convs = timeit_msg ctxt "record upd_convs proof:" upd_convs_prf; - fun upd_convs_standard_prf () = map Drule.export_without_context upd_convs; - val upd_convs_standard = - timeit_msg ctxt "record upd_convs_standard proof:" upd_convs_standard_prf; - - fun get_upd_acc_congs () = + val simp_defs_tac = + asm_full_simp_tac (ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms)); + + val sel_convs = timeit_msg ctxt "record sel_convs proof:" (fn () => + map (fn prop => prove [] [] prop (K (ALLGOALS simp_defs_tac))) sel_conv_props); + + val upd_convs = timeit_msg ctxt "record upd_convs proof:" (fn () => + map (fn prop => prove [] [] prop (K (ALLGOALS simp_defs_tac))) upd_conv_props); + + val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () => let val symdefs = map Thm.symmetric (sel_defs @ upd_defs); val fold_ss = HOL_basic_ss addsimps symdefs; val ua_congs = map (Drule.export_without_context o 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 ctxt "record upd fold/unfold congs:" get_upd_acc_congs; + in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end); val parent_induct = Option.map #induct_scheme (try List.last parents); - fun induct_scheme_prf () = - prove_standard [] induct_scheme_prop + val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" (fn () => + prove [] [] induct_scheme_prop (fn _ => EVERY [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1, try_param_tac rN ext_induct 1, - asm_simp_tac HOL_basic_ss 1]); - val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" induct_scheme_prf; - - fun induct_prf () = + asm_simp_tac HOL_basic_ss 1])); + + val induct = timeit_msg ctxt "record induct proof:" (fn () => let val (assm, concl) = induct_prop in - prove_standard [assm] concl (fn {prems, ...} => + prove [] [assm] concl (fn {prems, ...} => try_param_tac rN induct_scheme 1 THEN try_param_tac "more" @{thm unit.induct} 1 THEN resolve_tac prems 1) - end; - val induct = timeit_msg ctxt "record induct proof:" induct_prf; + end); fun cases_scheme_prf () = let @@ -2227,22 +2173,22 @@ induct_scheme; in Object_Logic.rulify (mp OF [ind, refl]) end; - val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop; - val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" cases_scheme_prf; - - fun cases_prf () = - prove_standard [] cases_prop + val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () => + future_forward_prf defs_thy cases_scheme_prf cases_scheme_prop); + + val cases = timeit_msg ctxt "record cases proof:" (fn () => + prove [] [] cases_prop (fn _ => try_param_tac rN cases_scheme 1 THEN - simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]); - val cases = timeit_msg ctxt "record cases proof:" cases_prf; - - fun surjective_prf () = + ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps [@{thm unit_all_eq1}])))); + + val surjective = timeit_msg ctxt "record surjective proof:" (fn () => let - val leaf_ss = get_sel_upd_defs defs_thy addsimps (sel_defs @ (o_assoc :: id_o_apps)); + val leaf_ss = + get_sel_upd_defs defs_thy addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id}); val init_ss = HOL_basic_ss addsimps ext_defs; in - prove_standard [] surjective_prop + prove [] [] surjective_prop (fn _ => EVERY [rtac surject_assist_idE 1, @@ -2250,28 +2196,23 @@ REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))]) - end; - val surjective = timeit_msg ctxt "record surjective proof:" surjective_prf; - - fun split_meta_prf () = - prove false [] split_meta_prop + end); + + val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () => + prove [] [] split_meta_prop (fn _ => EVERY1 [rtac equal_intr_rule, Goal.norm_hhf_tac, - etac meta_allE, atac, - rtac (prop_subst OF [surjective]), - REPEAT o etac meta_allE, atac]); - val split_meta = timeit_msg ctxt "record split_meta proof:" split_meta_prf; - fun split_meta_standardise () = Drule.export_without_context split_meta; - val split_meta_standard = - timeit_msg ctxt "record split_meta standard:" split_meta_standardise; + etac @{thm meta_allE}, atac, + rtac (@{thm prop_subst} OF [surjective]), + REPEAT o etac @{thm meta_allE}, atac])); fun split_object_prf () = let - val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P $ r0))); - val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta_standard)); + val cPI = cterm_of defs_thy (lambda r0 (Trueprop (P $ r0))); + val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta)); val cP = cterm_of defs_thy P; - val split_meta' = cterm_instantiate [(cP, cPI)] split_meta_standard; + val split_meta' = cterm_instantiate [(cP, cPI)] split_meta; val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop); val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l); val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r); @@ -2289,40 +2230,34 @@ |> Thm.implies_intr cr (* 2 ==> 1 *) in thr COMP (thl COMP iffI) end; - - val split_object_prf = future_forward_prf split_object_prf split_object_prop; - val split_object = timeit_msg ctxt "record split_object proof:" split_object_prf; - - - fun split_ex_prf () = + val split_object = timeit_msg ctxt "record split_object proof:" (fn () => + future_forward_prf defs_thy split_object_prf split_object_prop); + + val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () => let - val ss = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff]; + val ss = HOL_basic_ss addsimps @{thms not_ex [symmetric] Not_eq_iff}; val P_nm = fst (dest_Free P); val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0))); val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object; val so'' = simplify ss so'; - in - prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1) - end; - val split_ex = timeit_msg ctxt "record split_ex proof:" split_ex_prf; + in prove [] [] split_ex_prop (fn _ => resolve_tac [so''] 1) end); fun equality_tac thms = let val s' :: s :: eqs = rev thms; - val ss' = ss addsimps (s' :: s :: sel_convs_standard); + val ss' = ss addsimps (s' :: s :: sel_convs); 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 {context, ...} => + val equality = timeit_msg ctxt "record equality proof:" (fn () => + prove [] [] equality_prop (fn {context, ...} => fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1) - (*simp_all_tac ss (sel_convs) would also work but is less efficient*) - end); - val equality = timeit_msg ctxt "record equality proof:" equality_prf; + (*simp_defs_tac would also work but is less efficient*) + end)); val ((([sel_convs', upd_convs', sel_defs', upd_defs', fold_congs', unfold_congs', @@ -2331,13 +2266,13 @@ [induct_scheme', induct', cases_scheme', cases']), thms_thy) = defs_thy |> (Global_Theory.add_thmss o map (Thm.no_attributes o apfst Binding.name)) - [("select_convs", sel_convs_standard), - ("update_convs", upd_convs_standard), + [("select_convs", sel_convs), + ("update_convs", upd_convs), ("select_defs", sel_defs), ("update_defs", upd_defs), ("fold_congs", fold_congs), ("unfold_congs", unfold_congs), - ("splits", [split_meta_standard, split_object, split_ex]), + ("splits", [split_meta, split_object, split_ex]), ("defs", derived_defs)] ||>> (Global_Theory.add_thms o map (Thm.no_attributes o apfst Binding.name)) [("surjective", surjective), @@ -2350,14 +2285,13 @@ 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 ([simps', iffs'], thms_thy') = thms_thy |> Global_Theory.add_thmss [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]), - ((Binding.name "iffs", iffs), [iff_add])]; + ((Binding.name "iffs", [ext_inject]), [iff_add])]; val info = make_info alphas parent fields extension diff -r 1e3ff542e83e -r 1e184c0d88be src/Pure/Isar/skip_proof.ML --- a/src/Pure/Isar/skip_proof.ML Thu Dec 29 18:54:07 2011 +0100 +++ b/src/Pure/Isar/skip_proof.ML Thu Dec 29 20:32:59 2011 +0100 @@ -33,11 +33,9 @@ ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st; fun prove ctxt xs asms prop tac = - (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop - (fn args => fn st => - if ! quick_and_dirty - then cheat_tac (Proof_Context.theory_of ctxt) st - else tac args st); + if ! quick_and_dirty then + Goal.prove ctxt xs asms prop (fn _ => cheat_tac (Proof_Context.theory_of ctxt)) + else (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop tac; fun prove_global thy xs asms prop tac = Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);