# HG changeset patch # User huffman # Date 1333226746 -7200 # Node ID 403b363c138749ba123c2247df1711c76c3591d4 # Parent 1caeecc72aea02838c759dd6803334ff12820bd0# Parent 72ab1fbf2f41097cd52df9084705a2d54108fc07 merged diff -r 1caeecc72aea -r 403b363c1387 src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy --- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Sat Mar 31 20:09:24 2012 +0200 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Sat Mar 31 22:45:46 2012 +0200 @@ -967,7 +967,7 @@ done -declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (SOME o symmetric_fun))) *} +declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym Simplifier.default_mk_sym) *} end diff -r 1caeecc72aea -r 403b363c1387 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Sat Mar 31 20:09:24 2012 +0200 +++ b/src/HOL/Tools/typedef.ML Sat Mar 31 22:45:46 2012 +0200 @@ -192,7 +192,7 @@ val cert = Thm.cterm_of (Proof_Context.theory_of axiom_lthy); val typedef = - Local_Defs.contract axiom_lthy defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom; + Local_Defs.contract defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom; in ((RepC, AbsC, axiom_name, typedef), axiom_lthy) end; val alias_lthy = typedef_lthy @@ -210,7 +210,7 @@ let val cert = Thm.cterm_of (Proof_Context.theory_of lthy1); val inhabited' = - Local_Defs.contract lthy1 (the_list set_def) (cert (mk_inhabited set')) inhabited; + Local_Defs.contract (the_list set_def) (cert (mk_inhabited set')) inhabited; val typedef' = inhabited' RS typedef; fun make th = Goal.norm_result (typedef' RS th); val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject), diff -r 1caeecc72aea -r 403b363c1387 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Sat Mar 31 20:09:24 2012 +0200 +++ b/src/Pure/Isar/generic_target.ML Sat Mar 31 22:45:46 2012 +0200 @@ -58,7 +58,6 @@ (*term and type parameters*) val crhs = Thm.cterm_of thy rhs; val ((defs, _), rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of; - val rhs_conv = Raw_Simplifier.rewrite true defs crhs; val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' []; val T = Term.fastype_of rhs; @@ -83,12 +82,12 @@ (*local definition*) val ((lhs, local_def), lthy3) = lthy2 |> Local_Defs.add_def ((b, NoSyn), lhs'); - val def = Local_Defs.trans_terms lthy3 - [(*c == global.c xs*) local_def, - (*global.c xs == rhs'*) global_def, - (*rhs' == rhs*) Thm.symmetric rhs_conv]; - (*note*) + (*result*) + val def = + Thm.transitive local_def global_def + |> Local_Defs.contract defs + (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs))); val ([(res_name, [res])], lthy4) = lthy3 |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])]; in ((lhs, (res_name, res)), lthy4) end; @@ -134,7 +133,7 @@ val result'' = (fold (curry op COMP) asms' result' handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms')) - |> Local_Defs.contract ctxt defs (Thm.cprop_of th) + |> Local_Defs.contract defs (Thm.cprop_of th) |> Goal.norm_result |> Global_Theory.name_thm false false name; diff -r 1caeecc72aea -r 403b363c1387 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Sat Mar 31 20:09:24 2012 +0200 +++ b/src/Pure/Isar/local_defs.ML Sat Mar 31 22:45:46 2012 +0200 @@ -17,9 +17,7 @@ (term * term) * Proof.context val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm val export_cterm: Proof.context -> Proof.context -> cterm -> (thm list * thm list) * cterm - val trans_terms: Proof.context -> thm list -> thm - val trans_props: Proof.context -> thm list -> thm - val contract: Proof.context -> thm list -> cterm -> thm -> thm + val contract: thm list -> cterm -> thm -> thm val print_rules: Proof.context -> unit val defn_add: attribute val defn_del: attribute @@ -137,7 +135,7 @@ let val exp = Assumption.export false inner outer; val exp_term = Assumption.export_term inner outer; - val prems = Assumption.all_prems_of inner; + val prems = Assumption.local_prems_of inner outer; in fn th => let @@ -166,30 +164,9 @@ fun export_cterm inner outer ct = export inner outer (Drule.mk_term ct) ||> Drule.dest_term; - -(* basic transitivity reasoning -- modulo beta-eta *) - -local - -val is_trivial = Pattern.aeconv o Logic.dest_equals o Thm.prop_of; +fun contract defs ct th = + th COMP (Raw_Simplifier.rewrite true defs ct COMP_INCR Drule.equal_elim_rule2); -fun trans_list _ _ [] = raise List.Empty - | trans_list trans ctxt (th :: raw_eqs) = - (case filter_out is_trivial raw_eqs of - [] => th - | eqs => - let val ((_, th' :: eqs'), ctxt') = Variable.import true (th :: eqs) ctxt - in singleton (Variable.export ctxt' ctxt) (fold trans eqs' th') end); - -in - -val trans_terms = trans_list (fn eq2 => fn eq1 => eq2 COMP (eq1 COMP Drule.transitive_thm)); -val trans_props = trans_list (fn eq => fn th => th COMP (eq COMP Drule.equal_elim_rule1)); - -end; - -fun contract ctxt defs ct th = - trans_props ctxt [th, Thm.symmetric (Raw_Simplifier.rewrite true defs ct)]; (** defived definitions **) diff -r 1caeecc72aea -r 403b363c1387 src/Pure/assumption.ML --- a/src/Pure/assumption.ML Sat Mar 31 20:09:24 2012 +0200 +++ b/src/Pure/assumption.ML Sat Mar 31 22:45:46 2012 +0200 @@ -56,7 +56,7 @@ datatype data = Data of {assms: (export * cterm list) list, (*assumes: A ==> _*) - prems: thm list}; (*prems: A |- A*) + prems: thm list}; (*prems: A |- norm_hhf A*) fun make_data (assms, prems) = Data {assms = assms, prems = prems}; diff -r 1caeecc72aea -r 403b363c1387 src/Pure/drule.ML --- a/src/Pure/drule.ML Sat Mar 31 20:09:24 2012 +0200 +++ b/src/Pure/drule.ML Sat Mar 31 22:45:46 2012 +0200 @@ -43,7 +43,6 @@ val reflexive_thm: thm val symmetric_thm: thm val transitive_thm: thm - val symmetric_fun: thm -> thm val extensional: thm -> thm val asm_rl: thm val cut_rl: thm @@ -400,8 +399,6 @@ val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm); in store_standard_thm_open (Binding.name "transitive") thm end; -fun symmetric_fun thm = thm RS symmetric_thm; - fun extensional eq = let val eq' = Thm.abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (cprop_of eq)))) eq diff -r 1caeecc72aea -r 403b363c1387 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Sat Mar 31 20:09:24 2012 +0200 +++ b/src/Pure/raw_simplifier.ML Sat Mar 31 22:45:46 2012 +0200 @@ -101,6 +101,7 @@ val solver: simpset -> solver -> int -> tactic val simp_depth_limit_raw: Config.raw val clear_ss: simpset -> simpset + val default_mk_sym: simpset -> thm -> thm option val simproc_global_i: theory -> string -> term list -> (theory -> simpset -> term -> thm option) -> simproc val simproc_global: theory -> string -> string list @@ -766,11 +767,13 @@ init_ss mk_rews termless subgoal_tac solvers |> inherit_context ss; +fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm); + val empty_ss = init_ss {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], mk_cong = K I, - mk_sym = K (SOME o Drule.symmetric_fun), + mk_sym = default_mk_sym, mk_eq_True = K (K NONE), reorient = default_reorient} Term_Ord.termless (K (K no_tac)) ([], []); diff -r 1caeecc72aea -r 403b363c1387 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Mar 31 20:09:24 2012 +0200 +++ b/src/Pure/simplifier.ML Sat Mar 31 22:45:46 2012 +0200 @@ -33,6 +33,7 @@ val map_simpset_global: (simpset -> simpset) -> theory -> theory val pretty_ss: Proof.context -> simpset -> Pretty.T val clear_ss: simpset -> simpset + val default_mk_sym: simpset -> thm -> thm option val debug_bounds: bool Unsynchronized.ref val prems_of: simpset -> thm list val add_simp: thm -> simpset -> simpset