# HG changeset patch # User wenzelm # Date 1325174299 -3600 # Node ID c66fa5ea4305e9eee1fd4fdaccd5e7411b2a05a3 # Parent ab32a87ba01a4a8d4232573f0e7a1c53cb995a85 tuned; diff -r ab32a87ba01a -r c66fa5ea4305 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Dec 29 15:54:37 2011 +0100 +++ b/src/HOL/Tools/record.ML Thu Dec 29 16:58:19 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 **) @@ -1017,11 +1000,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 +1024,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 +1063,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 +1331,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) @@ -1449,7 +1432,7 @@ 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 @@ -1647,7 +1630,7 @@ (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))); @@ -1680,9 +1663,9 @@ (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]); + etac @{thm meta_allE}, atac, + rtac (@{thm prop_subst} OF [surject]), + REPEAT o etac @{thm meta_allE}, atac]); val split_meta = timeit_msg ctxt "record extension split_meta proof:" split_meta_prf; fun induct_prf () = @@ -2239,7 +2222,8 @@ fun surjective_prf () = 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 @@ -2258,9 +2242,9 @@ (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]); + etac @{thm meta_allE}, atac, + rtac (@{thm prop_subst} OF [surjective]), + REPEAT o etac @{thm 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 = @@ -2296,7 +2280,7 @@ fun split_ex_prf () = 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;