--- 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
--- 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),
--- 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;
--- 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 **)
--- 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};
--- 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
--- 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)) ([], []);
--- 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