--- a/src/HOL/Tools/record.ML Tue Nov 17 10:17:53 2009 +0000
+++ b/src/HOL/Tools/record.ML Tue Nov 17 10:18:51 2009 +0000
@@ -1009,14 +1009,20 @@
(** record simprocs **)
fun future_forward_prf_standard thy prf prop () =
- let val thm = if !quick_and_dirty then Skip_Proof.make_thm thy prop
- else Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop;
- in Drule.standard thm end;
+ let val thm =
+ if ! quick_and_dirty then Skip_Proof.make_thm thy prop
+ else if Goal.future_enabled () then
+ Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop
+ else prf ()
+ in Drule.standard 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 then Goal.prove else Goal.prove_future;
- val prf = prv (ProofContext.init 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 (ProofContext.init thy) [] asms prop tac;
in if stndrd then Drule.standard prf else prf end;
val prove_future_global = prove_common false;
--- a/src/HOL/Tools/rewrite_hol_proof.ML Tue Nov 17 10:17:53 2009 +0000
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Tue Nov 17 10:18:51 2009 +0000
@@ -7,7 +7,7 @@
signature REWRITE_HOL_PROOF =
sig
val rews: (Proofterm.proof * Proofterm.proof) list
- val elim_cong: typ list -> Proofterm.proof -> Proofterm.proof option
+ val elim_cong: typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
end;
structure RewriteHOLProof : REWRITE_HOL_PROOF =
@@ -309,17 +309,19 @@
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
-fun elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
+fun elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
- | elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
+ | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
(strip_cong [] (incr_pboundvars 1 0 prf))
- | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
+ | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 [] o
apsnd (map (make_sym Ts))) (strip_cong [] prf1)
- | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
+ | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
- | elim_cong _ _ = NONE;
+ | elim_cong_aux _ _ = NONE;
+
+fun elim_cong Ts prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
end;
--- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Nov 17 10:17:53 2009 +0000
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Nov 17 10:18:51 2009 +0000
@@ -6,8 +6,9 @@
signature PROOF_REWRITE_RULES =
sig
- val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
- val rprocs : bool -> (typ list -> Proofterm.proof -> Proofterm.proof option) list
+ val rew : bool -> typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
+ val rprocs : bool ->
+ (typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
@@ -183,7 +184,7 @@
end
| rew' _ = NONE;
- in rew' end;
+ in rew' #> Option.map (rpair no_skel) end;
fun rprocs b = [rew b];
val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));
--- a/src/Pure/defs.ML Tue Nov 17 10:17:53 2009 +0000
+++ b/src/Pure/defs.ML Tue Nov 17 10:18:51 2009 +0000
@@ -10,10 +10,10 @@
val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
val plain_args: typ list -> bool
type T
- val all_specifications_of: T -> (string * {def: string option, description: string,
- lhs: typ list, rhs: (string * typ list) list} list) list
- val specifications_of: T -> string -> {def: string option, description: string,
- lhs: typ list, rhs: (string * typ list) list} list
+ type spec =
+ {def: string option, description: string, lhs: typ list, rhs: (string * typ list) list}
+ val all_specifications_of: T -> (string * spec list) list
+ val specifications_of: T -> string -> spec list
val dest: T ->
{restricts: ((string * typ list) * string) list,
reducts: ((string * typ list) * (string * typ list) list) list}
--- a/src/Pure/item_net.ML Tue Nov 17 10:17:53 2009 +0000
+++ b/src/Pure/item_net.ML Tue Nov 17 10:18:51 2009 +0000
@@ -40,12 +40,14 @@
(* standard operations *)
-fun member (Items {eq, index, net, ...}) x =
- exists (fn t => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t)) (index x);
+fun member (Items {eq, index, content, net, ...}) x =
+ (case index x of
+ [] => Library.member eq content x
+ | t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t));
fun cons x (Items {eq, index, content, next, net}) =
mk_items eq index (x :: content) (next - 1)
- (fold (fn t => Net.insert_term_safe (eq o pairself #2) (t, (next, x))) (index x) net);
+ (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
fun merge (items1, Items {content = content2, ...}) =
--- a/src/Pure/more_thm.ML Tue Nov 17 10:17:53 2009 +0000
+++ b/src/Pure/more_thm.ML Tue Nov 17 10:18:51 2009 +0000
@@ -75,9 +75,6 @@
val untag_rule: string -> thm -> thm
val tag: Properties.property -> attribute
val untag: string -> attribute
- val position_of: thm -> Position.T
- val default_position: Position.T -> thm -> thm
- val default_position_of: thm -> thm -> thm
val def_name: string -> string
val def_name_optional: string -> string -> string
val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
@@ -380,14 +377,6 @@
fun untag s x = rule_attribute (K (untag_rule s)) x;
-(* position *)
-
-val position_of = Position.of_properties o Thm.get_tags;
-
-fun default_position pos = Thm.map_tags (Position.default_properties pos);
-val default_position_of = default_position o position_of;
-
-
(* def_name *)
fun def_name c = c ^ "_def";
--- a/src/Pure/proofterm.ML Tue Nov 17 10:17:53 2009 +0000
+++ b/src/Pure/proofterm.ML Tue Nov 17 10:18:51 2009 +0000
@@ -109,18 +109,20 @@
val axm_proof: string -> term -> proof
val oracle_proof: string -> term -> oracle * proof
val promise_proof: theory -> serial -> term -> proof
- val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
+ val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
val thm_proof: theory -> string -> term list -> term ->
(serial * proof_body future) list -> proof_body -> pthm * proof
val get_name: term list -> term -> proof -> string
(** rewriting on proof terms **)
val add_prf_rrule: proof * proof -> theory -> theory
- val add_prf_rproc: (typ list -> proof -> proof option) -> theory -> theory
+ val add_prf_rproc: (typ list -> proof -> (proof * proof) option) -> theory -> theory
+ val no_skel: proof
+ val normal_skel: proof
val rewrite_proof: theory -> (proof * proof) list *
- (typ list -> proof -> proof option) list -> proof -> proof
+ (typ list -> proof -> (proof * proof) option) list -> proof -> proof
val rewrite_proof_notypes: (proof * proof) list *
- (typ list -> proof -> proof option) list -> proof -> proof
+ (typ list -> proof -> (proof * proof) option) list -> proof -> proof
val rew_proof: theory -> proof -> proof
end
@@ -1169,28 +1171,30 @@
(**** rewriting on proof terms ****)
-val skel0 = PBound 0;
+val no_skel = PBound 0;
+val normal_skel = Hyp (Var ((Name.uu, 0), propT));
fun rewrite_prf tymatch (rules, procs) prf =
let
- fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, skel0)
- | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, skel0)
- | rew Ts prf = (case get_first (fn r => r Ts prf) procs of
- SOME prf' => SOME (prf', skel0)
- | NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
- (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
- handle PMatch => NONE) (filter (could_unify prf o fst) rules));
+ fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
+ | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
+ | rew Ts prf =
+ (case get_first (fn r => r Ts prf) procs of
+ NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
+ (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
+ handle PMatch => NONE) (filter (could_unify prf o fst) rules)
+ | some => some);
fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) =
if prf_loose_Pbvar1 prf' 0 then rew Ts prf
else
let val prf'' = incr_pboundvars (~1) 0 prf'
- in SOME (the_default (prf'', skel0) (rew Ts prf'')) end
+ in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
| rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) =
if prf_loose_bvar1 prf' 0 then rew Ts prf
else
let val prf'' = incr_pboundvars 0 (~1) prf'
- in SOME (the_default (prf'', skel0) (rew Ts prf'')) end
+ in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
| rew0 Ts prf = rew Ts prf;
fun rew1 _ (Hyp (Var _)) _ = NONE
@@ -1205,20 +1209,20 @@
and rew2 Ts skel (prf % SOME t) = (case prf of
Abst (_, _, body) =>
let val prf' = prf_subst_bounds [t] body
- in SOME (the_default prf' (rew2 Ts skel0 prf')) end
- | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf of
+ in SOME (the_default prf' (rew2 Ts no_skel prf')) end
+ | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf of
SOME prf' => SOME (prf' % SOME t)
| NONE => NONE))
| rew2 Ts skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
- (rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf)
+ (rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf)
| rew2 Ts skel (prf1 %% prf2) = (case prf1 of
AbsP (_, _, body) =>
let val prf' = prf_subst_pbounds [prf2] body
- in SOME (the_default prf' (rew2 Ts skel0 prf')) end
+ in SOME (the_default prf' (rew2 Ts no_skel prf')) end
| _ =>
let val (skel1, skel2) = (case skel of
skel1 %% skel2 => (skel1, skel2)
- | _ => (skel0, skel0))
+ | _ => (no_skel, no_skel))
in case rew1 Ts skel1 prf1 of
SOME prf1' => (case rew1 Ts skel2 prf2 of
SOME prf2' => SOME (prf1' %% prf2')
@@ -1228,16 +1232,16 @@
| NONE => NONE)
end)
| rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts)
- (case skel of Abst (_, _, skel') => skel' | _ => skel0) prf of
+ (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of
SOME prf' => SOME (Abst (s, T, prf'))
| NONE => NONE)
| rew2 Ts skel (AbsP (s, t, prf)) = (case rew1 Ts
- (case skel of AbsP (_, _, skel') => skel' | _ => skel0) prf of
+ (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
SOME prf' => SOME (AbsP (s, t, prf'))
| NONE => NONE)
| rew2 _ _ _ = NONE;
- in the_default prf (rew1 [] skel0 prf) end;
+ in the_default prf (rew1 [] no_skel prf) end;
fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) =>
Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
@@ -1249,7 +1253,9 @@
structure ProofData = Theory_Data
(
- type T = (stamp * (proof * proof)) list * (stamp * (typ list -> proof -> proof option)) list;
+ type T =
+ (stamp * (proof * proof)) list *
+ (stamp * (typ list -> proof -> (proof * proof) option)) list;
val empty = ([], []);
val extend = I;
@@ -1277,27 +1283,26 @@
| _ => false));
in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
-fun fulfill_proof _ [] body0 = body0
- | fulfill_proof thy ps body0 =
- let
- val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
- val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
- val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
- val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
+fun fulfill_norm_proof thy ps body0 =
+ let
+ val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
+ val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
+ val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
+ val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
- fun fill (Promise (i, prop, Ts)) =
- (case Inttab.lookup proofs i of
- NONE => NONE
- | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf))
- | fill _ = NONE;
- val (rules, procs) = get_data thy;
- val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
- in PBody {oracles = oracles, thms = thms, proof = proof} end;
+ fun fill (Promise (i, prop, Ts)) =
+ (case Inttab.lookup proofs i of
+ NONE => NONE
+ | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf, normal_skel))
+ | fill _ = NONE;
+ val (rules, procs) = get_data thy;
+ val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
+ in PBody {oracles = oracles, thms = thms, proof = proof} end;
fun fulfill_proof_future _ [] body = Future.value body
| fulfill_proof_future thy promises body =
Future.fork_deps (map snd promises) (fn () =>
- fulfill_proof thy (map (apsnd Future.join) promises) body);
+ fulfill_norm_proof thy (map (apsnd Future.join) promises) body);
(***** theorems *****)
--- a/src/Pure/thm.ML Tue Nov 17 10:17:53 2009 +0000
+++ b/src/Pure/thm.ML Tue Nov 17 10:18:51 2009 +0000
@@ -540,7 +540,7 @@
fun raw_body (Thm (Deriv {body, ...}, _)) = body;
fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
- Pt.fulfill_proof (Theory.deref thy_ref)
+ Pt.fulfill_norm_proof (Theory.deref thy_ref)
(map #1 promises ~~ fulfill_bodies (map #2 promises)) body
and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));