--- a/src/HOL/Library/reflection.ML Tue Nov 08 14:29:24 2011 +0100
+++ b/src/HOL/Library/reflection.ML Tue Nov 08 17:47:22 2011 +0100
@@ -60,10 +60,11 @@
fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t)))
| mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
fun tryext x = (x RS ext2 handle THM _ => x)
- val cong = (Goal.prove ctxt'' [] (map mk_def env)
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
- (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x))
- THEN rtac th' 1)) RS sym
+ val cong =
+ (Goal.prove ctxt'' [] (map mk_def env)
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
+ (fn {context, prems, ...} =>
+ Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym
val (cong' :: vars') =
Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs)
--- a/src/HOL/Tools/Function/mutual.ML Tue Nov 08 14:29:24 2011 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Tue Nov 08 17:47:22 2011 +0100
@@ -176,7 +176,7 @@
end
fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
- import (export : thm -> thm) sum_psimp_eq =
+ import (export : thm -> thm) sum_psimp_eq =
let
val (MutualPart {f=SOME f, ...}) = get_part fname parts
@@ -190,9 +190,10 @@
in
Goal.prove ctxt [] []
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
- (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
- THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
- THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
+ (fn _ =>
+ Local_Defs.unfold_tac ctxt all_orig_fdefs
+ THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
+ THEN (simp_tac (simpset_of ctxt)) 1)
|> restore_cond
|> export
end
--- a/src/HOL/Tools/Function/partial_function.ML Tue Nov 08 14:29:24 2011 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Tue Nov 08 17:47:22 2011 +0100
@@ -64,7 +64,7 @@
(*rewrite conclusion with k-th assumtion*)
fun rewrite_with_asm_tac ctxt k =
- Subgoal.FOCUS (fn {context=ctxt', prems, ...} =>
+ Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;
fun dest_case thy t =
--- a/src/HOL/Tools/typedef.ML Tue Nov 08 14:29:24 2011 +0100
+++ b/src/HOL/Tools/typedef.ML Tue Nov 08 17:47:22 2011 +0100
@@ -183,7 +183,7 @@
let
val thy = Proof_Context.theory_of set_lthy;
val cert = Thm.cterm_of thy;
- val (defs, A) =
+ val ((defs, _), A) =
Local_Defs.export_cterm set_lthy (Proof_Context.init_global thy) (cert set')
||> Thm.term_of;
--- a/src/Pure/Isar/generic_target.ML Tue Nov 08 14:29:24 2011 +0100
+++ b/src/Pure/Isar/generic_target.ML Tue Nov 08 17:47:22 2011 +0100
@@ -57,7 +57,7 @@
(*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 ((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' [];
@@ -105,11 +105,8 @@
(*export assumes/defines*)
val th = Goal.norm_result raw_th;
- val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
- val assms =
- map (Raw_Simplifier.rewrite_rule defs o Thm.assume)
- (Assumption.all_assms_of ctxt);
- val nprems = Thm.nprems_of th' - Thm.nprems_of th;
+ val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
+ val asms' = map (Raw_Simplifier.rewrite_rule defs) asms;
(*export fixes*)
val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
@@ -134,11 +131,10 @@
val result' = Thm.instantiate (cinstT, cinst) result;
(*import assumes/defines*)
- val assm_tac = FIRST' (map (fn assm => Tactic.compose_tac (false, assm, 0)) assms);
val result'' =
- (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
- NONE => raise THM ("Failed to re-import result", 0, [result'])
- | SOME res => Local_Defs.contract ctxt defs (Thm.cprop_of th) res)
+ (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)
|> Goal.norm_result
|> Global_Theory.name_thm false false name;
--- a/src/Pure/Isar/local_defs.ML Tue Nov 08 14:29:24 2011 +0100
+++ b/src/Pure/Isar/local_defs.ML Tue Nov 08 17:47:22 2011 +0100
@@ -15,8 +15,8 @@
val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
(term * term) * Proof.context
- val export: Proof.context -> Proof.context -> thm -> thm list * thm
- val export_cterm: Proof.context -> Proof.context -> cterm -> thm list * cterm
+ 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
@@ -66,7 +66,7 @@
(* export defs *)
val head_of_def =
- #1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body;
+ Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body;
(*
@@ -78,7 +78,7 @@
*)
fun expand defs =
Drule.implies_intr_list defs
- #> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
+ #> Drule.generalize ([], map (#1 o head_of_def o Thm.term_of) defs)
#> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of);
@@ -136,16 +136,24 @@
fun export inner outer = (*beware of closure sizes*)
let
val exp = Assumption.export false inner outer;
+ val exp_term = Assumption.export_term inner outer;
val prems = Assumption.all_prems_of inner;
- in fn th =>
- let
- val th' = exp th;
- val still_fixed = map #1 (Thm.fold_terms Term.add_frees th' []);
- val defs = prems |> filter_out (fn prem =>
- (case try (head_of_def o Thm.prop_of) prem of
- SOME x => member (op =) still_fixed x
- | NONE => true));
- in (map Drule.abs_def defs, th') end
+ in
+ fn th =>
+ let
+ val th' = exp th;
+ val defs_asms = prems |> map (fn prem =>
+ (case try (head_of_def o Thm.prop_of) prem of
+ NONE => (prem, false)
+ | SOME x =>
+ let val t = Free x in
+ (case try exp_term t of
+ NONE => (prem, false)
+ | SOME u =>
+ if t aconv u then (prem, false)
+ else (Drule.abs_def prem, true))
+ end));
+ in (pairself (map #1) (List.partition #2 defs_asms), th') end
end;
(*
--- a/src/Pure/net.ML Tue Nov 08 14:29:24 2011 +0100
+++ b/src/Pure/net.ML Tue Nov 08 17:47:22 2011 +0100
@@ -54,7 +54,7 @@
| rands (Const(c,_), cs) = AtomK c :: cs
| rands (Free(c,_), cs) = AtomK c :: cs
| rands (Bound i, cs) = AtomK (Name.bound i) :: cs
- in case (head_of t) of
+ in case head_of t of
Var _ => VarK :: cs
| Abs _ => VarK :: cs
| _ => rands(t,cs)
@@ -103,9 +103,7 @@
| ins1 (VarK :: keys, Net{comb,var,atoms}) =
Net{comb=comb, var=ins1(keys,var), atoms=atoms}
| ins1 (AtomK a :: keys, Net{comb,var,atoms}) =
- let
- val net' = the_default empty (Symtab.lookup atoms a);
- val atoms' = Symtab.update (a, ins1 (keys, net')) atoms;
+ let val atoms' = Symtab.map_default (a, empty) (fn net' => ins1 (keys, net')) atoms;
in Net{comb=comb, var=var, atoms=atoms'} end
in ins1 (keys,net) end;
--- a/src/Pure/raw_simplifier.ML Tue Nov 08 14:29:24 2011 +0100
+++ b/src/Pure/raw_simplifier.ML Tue Nov 08 17:47:22 2011 +0100
@@ -456,7 +456,6 @@
val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
- val elhs = if term_of elhs aconv term_of lhs then lhs else elhs; (*share identical copies*)
val erhs = Envir.eta_contract (term_of rhs);
val perm =
var_perm (term_of elhs, erhs) andalso