--- a/Admin/isatest/settings/mac-poly-M4 Fri Jul 31 09:34:05 2009 +0200
+++ b/Admin/isatest/settings/mac-poly-M4 Fri Jul 31 09:34:21 2009 +0200
@@ -23,6 +23,6 @@
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4 -t true"
+ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4 -t true -q 2"
HOL_USEDIR_OPTIONS="-p 2 -q 0"
--- a/Admin/isatest/settings/mac-poly-M8 Fri Jul 31 09:34:05 2009 +0200
+++ b/Admin/isatest/settings/mac-poly-M8 Fri Jul 31 09:34:21 2009 +0200
@@ -23,6 +23,6 @@
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-ISABELLE_USEDIR_OPTIONS="-i false -d false -M 8 -t true"
+ISABELLE_USEDIR_OPTIONS="-i false -d false -M 8 -t true -q 2"
HOL_USEDIR_OPTIONS="-p 2 -q 0"
--- a/etc/settings Fri Jul 31 09:34:05 2009 +0200
+++ b/etc/settings Fri Jul 31 09:34:21 2009 +0200
@@ -92,7 +92,7 @@
### Batch sessions (cf. isabelle usedir)
###
-ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML"
+ISABELLE_USEDIR_OPTIONS="-M max -p 1 -q 2 -v true -V outline=/proof,/ML"
# Specifically for the HOL image
HOL_USEDIR_OPTIONS=""
--- a/src/CCL/Wfd.thy Fri Jul 31 09:34:05 2009 +0200
+++ b/src/CCL/Wfd.thy Fri Jul 31 09:34:21 2009 +0200
@@ -498,13 +498,14 @@
structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
in
-fun eval_tac ctxt ths i =
- DEPTH_SOLVE_1 (resolve_tac (ths @ Data.get ctxt) i ORELSE assume_tac i);
+fun eval_tac ths =
+ Subgoal.FOCUS_PREMS (fn {context, prems, ...} =>
+ DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1));
val eval_setup =
Data.setup #>
Method.setup @{binding eval}
- (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ctxt ths)))
+ (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt)))
"evaluation";
end;
--- a/src/HOL/Decision_Procs/Approximation.thy Fri Jul 31 09:34:05 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Jul 31 09:34:21 2009 +0200
@@ -3337,7 +3337,7 @@
REPEAT (FIRST' [etac @{thm intervalE},
etac @{thm meta_eqE},
rtac @{thm impI}] i)
- THEN FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
+ THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
THEN TRY (filter_prems_tac (K false) i)
THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
--- a/src/HOL/Prolog/prolog.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML Fri Jul 31 09:34:21 2009 +0200
@@ -67,7 +67,7 @@
imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *)
-(*val hyp_resolve_tac = FOCUS (fn {prems, ...} =>
+(*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
resolve_tac (maps atomizeD prems) 1);
-- is nice, but cannot instantiate unknowns in the assumptions *)
fun hyp_resolve_tac i st = let
--- a/src/HOL/Tools/cnf_funcs.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Fri Jul 31 09:34:21 2009 +0200
@@ -517,7 +517,7 @@
fun cnf_rewrite_tac ctxt i =
(* cut the CNF formulas as new premises *)
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let
val thy = ProofContext.theory_of ctxt
val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
@@ -540,7 +540,7 @@
fun cnfx_rewrite_tac ctxt i =
(* cut the CNF formulas as new premises *)
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let
val thy = ProofContext.theory_of ctxt;
val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems
--- a/src/HOL/Tools/meson.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/HOL/Tools/meson.ML Fri Jul 31 09:34:21 2009 +0200
@@ -586,9 +586,9 @@
SELECT_GOAL
(EVERY [ObjectLogic.atomize_prems_tac 1,
rtac ccontr 1,
- FOCUS (fn {context = ctxt', prems = negs, ...} =>
+ Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
EVERY1 [skolemize_prems_tac ctxt negs,
- FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
+ Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
(** Best-first search versions **)
--- a/src/HOL/Tools/record.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/HOL/Tools/record.ML Fri Jul 31 09:34:21 2009 +0200
@@ -2161,7 +2161,7 @@
fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
- THEN (FOCUS (fn {prems, ...} => equality_tac prems) context 1))
+ THEN (Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1))
(* simp_all_tac ss (sel_convs) would also work but is less efficient *)
end);
val equality = timeit_msg "record equality proof:" equality_prf;
--- a/src/HOL/Tools/res_axioms.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Jul 31 09:34:21 2009 +0200
@@ -517,7 +517,7 @@
SUBGOAL (fn (prop, i) =>
let val ts = Logic.strip_assums_hyp prop in
EVERY'
- [FOCUS
+ [Subgoal.FOCUS
(fn {prems, ...} =>
(Method.insert_tac
(map forall_intr_vars (neg_clausify prems)) i)) ctxt,
--- a/src/HOL/Tools/sat_funcs.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Fri Jul 31 09:34:21 2009 +0200
@@ -411,7 +411,7 @@
(* ------------------------------------------------------------------------- *)
fun rawsat_tac ctxt i =
- FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
+ Subgoal.FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
(* ------------------------------------------------------------------------- *)
(* pre_cnf_tac: converts the i-th subgoal *)
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Jul 31 09:34:21 2009 +0200
@@ -788,7 +788,7 @@
all_tac) THEN
PRIMITIVE (trace_thm ctxt "State after neqE:") THEN
(* use theorems generated from the actual justifications *)
- FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i
+ Subgoal.FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i
in
(* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
--- a/src/Provers/order.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Provers/order.ML Fri Jul 31 09:34:21 2009 +0200
@@ -1235,12 +1235,12 @@
val prfs = gen_solve mkconcl thy (lesss, C);
val (subgoals, prf) = mkconcl decomp less_thms thy C;
in
- FOCUS (fn {prems = asms, ...} =>
+ Subgoal.FOCUS (fn {prems = asms, ...} =>
let val thms = map (prove (prems @ asms)) prfs
in rtac (prove thms prf) 1 end) ctxt n st
end
handle Contr p =>
- (FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
+ (Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
handle Subscript => Seq.empty)
| Cannot => Seq.empty
| Subscript => Seq.empty)
--- a/src/Provers/quasi.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Provers/quasi.ML Fri Jul 31 09:34:21 2009 +0200
@@ -551,7 +551,7 @@
fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
- val thy = Thm.theory_of_thm st;
+ val thy = ProofContext.theory_of ctxt;
val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
@@ -560,11 +560,11 @@
val (subgoal, prf) = mkconcl_trans thy C;
in
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove prems) prfs
in rtac (prove thms prf) 1 end) ctxt n st
end
- handle Contr p => FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+ handle Contr p => Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
| Cannot => Seq.empty);
@@ -572,7 +572,7 @@
fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
- val thy = Thm.theory_of_thm st;
+ val thy = ProofContext.theory_of ctxt
val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
@@ -580,12 +580,12 @@
val prfs = solveQuasiOrder thy (lesss, C);
val (subgoals, prf) = mkconcl_quasi thy C;
in
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove prems) prfs
in rtac (prove thms prf) 1 end) ctxt n st
end
handle Contr p =>
- (FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+ (Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
handle Subscript => Seq.empty)
| Cannot => Seq.empty
| Subscript => Seq.empty);
--- a/src/Provers/trancl.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Provers/trancl.ML Fri Jul 31 09:34:21 2009 +0200
@@ -533,7 +533,7 @@
fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
- val thy = Thm.theory_of_thm st;
+ val thy = ProofContext.theory_of ctxt;
val Hs = Logic.strip_assums_hyp A;
val C = Logic.strip_assums_concl A;
val (rel, subgoals, prf) = mkconcl_trancl C;
@@ -541,7 +541,7 @@
val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));
val prfs = solveTrancl (prems, C);
in
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove thy rel prems) prfs
in rtac (prove thy rel thms prf) 1 end) ctxt n st
end
@@ -550,7 +550,7 @@
fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
- val thy = Thm.theory_of_thm st;
+ val thy = ProofContext.theory_of ctxt;
val Hs = Logic.strip_assums_hyp A;
val C = Logic.strip_assums_concl A;
val (rel, subgoals, prf) = mkconcl_rtrancl C;
@@ -558,7 +558,7 @@
val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));
val prfs = solveRtrancl (prems, C);
in
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove thy rel prems) prfs
in rtac (prove thy rel thms prf) 1 end) ctxt n st
end
--- a/src/Pure/Concurrent/future.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Fri Jul 31 09:34:21 2009 +0200
@@ -120,11 +120,11 @@
fun SYNCHRONIZED name = SimpleThread.synchronized name lock;
fun wait cond = (*requires SYNCHRONIZED*)
- ConditionVar.wait (cond, lock) handle Exn.Interrupt => ();
+ Multithreading.sync_wait NONE cond lock;
-fun wait_interruptible cond timeout = (*requires SYNCHRONIZED*)
+fun wait_interruptible timeout cond = (*requires SYNCHRONIZED*)
interruptible (fn () =>
- ignore (ConditionVar.waitUntil (cond, lock, Time.+ (Time.now (), timeout)))) ();
+ ignore (Multithreading.sync_wait (SOME (Time.+ (Time.now (), timeout))) cond lock)) ();
fun signal cond = (*requires SYNCHRONIZED*)
ConditionVar.signal cond;
@@ -194,7 +194,7 @@
(* worker threads *)
fun worker_wait cond = (*requires SYNCHRONIZED*)
- (change_active false; wait cond; change_active true);
+ (change_active false; wait cond; change_active true);
fun worker_next () = (*requires SYNCHRONIZED*)
if ! excessive > 0 then
@@ -269,10 +269,14 @@
(*canceled groups*)
val _ =
if null (! canceled) then ()
- else (change canceled (filter_out (Task_Queue.cancel (! queue))); broadcast_work ());
+ else
+ (Multithreading.tracing 1 (fn () =>
+ string_of_int (length (! canceled)) ^ " canceled groups");
+ change canceled (filter_out (Task_Queue.cancel (! queue)));
+ broadcast_work ());
(*delay loop*)
- val _ = wait_interruptible scheduler_event next_round
+ val _ = wait_interruptible next_round scheduler_event
handle Exn.Interrupt =>
(Multithreading.tracing 1 (fn () => "Interrupt");
List.app do_cancel (Task_Queue.cancel_all (! queue)));
--- a/src/Pure/Concurrent/synchronized.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Fri Jul 31 09:34:21 2009 +0200
@@ -48,11 +48,9 @@
(case f x of
SOME (y, x') => (var := x'; SOME y)
| NONE =>
- (case time_limit x of
- NONE => (ConditionVar.wait (cond, lock); try_change ())
- | SOME t =>
- if ConditionVar.waitUntil (cond, lock, t) then try_change ()
- else NONE))
+ if Multithreading.sync_wait (time_limit x) cond lock
+ then try_change ()
+ else NONE)
end;
val res = try_change ();
val _ = ConditionVar.broadcast cond;
--- a/src/Pure/ML-Systems/multithreading.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML Fri Jul 31 09:34:21 2009 +0200
@@ -26,6 +26,7 @@
val restricted_interrupts: Thread.threadAttribute list
val with_attributes: Thread.threadAttribute list ->
(Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
+ val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool
val self_critical: unit -> bool
val serial: unit -> int
end;
@@ -48,6 +49,9 @@
fun max_threads_value () = 1: int;
fun enabled () = false;
+
+(* attributes *)
+
val no_interrupts =
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
@@ -59,6 +63,8 @@
fun with_attributes _ f x = f [] x;
+fun sync_wait _ _ _ = false;
+
(* critical section *)
@@ -74,5 +80,5 @@
end;
-structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
-open BasicMultithreading;
+structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
+open Basic_Multithreading;
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Fri Jul 31 09:34:21 2009 +0200
@@ -110,6 +110,9 @@
val _ = Thread.setAttributes orig_atts;
in Exn.release result end;
+
+(* regular interruptibility *)
+
fun interruptible f x =
(Thread.testInterrupt (); with_attributes regular_interrupts (fn _ => fn x => f x) x);
@@ -118,6 +121,29 @@
f (fn g => with_attributes atts (fn _ => fn y => g y)) x);
+(* synchronous wait *)
+
+fun sync_attributes e =
+ let
+ val orig_atts = Thread.getAttributes ();
+ val broadcast =
+ (case List.find (fn Thread.EnableBroadcastInterrupt _ => true | _ => false) orig_atts of
+ NONE => Thread.EnableBroadcastInterrupt false
+ | SOME att => att);
+ val interrupt_state =
+ (case List.find (fn Thread.InterruptState _ => true | _ => false) orig_atts of
+ NONE => Thread.InterruptState Thread.InterruptDefer
+ | SOME (state as Thread.InterruptState Thread.InterruptDefer) => state
+ | _ => Thread.InterruptState Thread.InterruptSynch);
+ in with_attributes [broadcast, interrupt_state] (fn _ => fn () => e ()) () end;
+
+fun sync_wait time cond lock =
+ sync_attributes (fn () =>
+ (case time of
+ SOME t => ConditionVar.waitUntil (cond, lock, t)
+ | NONE => (ConditionVar.wait (cond, lock); true)));
+
+
(* execution with time limit *)
structure TimeLimit =
@@ -192,8 +218,9 @@
val _ = while ! result = Wait do
restore_attributes (fn () =>
- (ConditionVar.waitUntil (result_cond, result_mutex, Time.now () + Time.fromMilliseconds 100); ())
- handle Exn.Interrupt => kill 10) ();
+ (ignore (sync_wait (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100)))
+ result_cond result_mutex)
+ handle Exn.Interrupt => kill 10)) ();
(*cleanup*)
val output = read_file output_name handle IO.Io _ => "";
@@ -269,5 +296,5 @@
end;
-structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
-open BasicMultithreading;
+structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
+open Basic_Multithreading;
--- a/src/Pure/ML-Systems/polyml.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Fri Jul 31 09:34:21 2009 +0200
@@ -17,7 +17,7 @@
use "ML-Systems/polyml_common.ML";
if ml_system = "polyml-5.2"
-then use "ML-Systems/thread_dummy.ML"
+then (use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML")
else use "ML-Systems/multithreading_polyml.ML";
val pointer_eq = PolyML.pointerEq;
--- a/src/Pure/more_thm.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Pure/more_thm.ML Fri Jul 31 09:34:21 2009 +0200
@@ -41,6 +41,11 @@
val elim_implies: thm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
+ val certify_inst: theory ->
+ ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
+ (ctyp * ctyp) list * (cterm * cterm) list
+ val certify_instantiate:
+ ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
val unvarify: thm -> thm
val close_derivation: thm -> thm
val add_axiom: binding * term -> theory -> thm * theory
@@ -269,24 +274,29 @@
end;
+(* certify_instantiate *)
+
+fun certify_inst thy (instT, inst) =
+ (map (fn (v, T) => (Thm.ctyp_of thy (TVar v), Thm.ctyp_of thy T)) instT,
+ map (fn (v, t) => (Thm.cterm_of thy (Var v), Thm.cterm_of thy t)) inst);
+
+fun certify_instantiate insts th =
+ Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
+
+
(* unvarify: global schematic variables *)
fun unvarify th =
let
- val thy = Thm.theory_of_thm th;
- val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
-
val prop = Thm.full_prop_of th;
val _ = map Logic.unvarify (prop :: Thm.hyps_of th)
handle TERM (msg, _) => raise THM (msg, 0, [th]);
- val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
- val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
+ val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
- let val T' = Term_Subst.instantiateT instT0 T
- in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
- in Thm.instantiate (instT, inst) th end;
+ let val T' = Term_Subst.instantiateT instT T
+ in (((a, i), T'), Free ((a, T'))) end);
+ in certify_instantiate (instT, inst) th end;
(* close_derivation *)
--- a/src/Pure/subgoal.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Pure/subgoal.ML Fri Jul 31 09:34:21 2009 +0200
@@ -1,20 +1,23 @@
(* Title: Pure/subgoal.ML
Author: Makarius
-Tactical operations with explicit subgoal focus, based on
-canonical proof decomposition (similar to fix/assume/show).
+Tactical operations with explicit subgoal focus, based on canonical
+proof decomposition. The "visible" part of the text within the
+context is fixed, the remaining goal may be schematic.
*)
signature SUBGOAL =
sig
type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
- asms: cterm list, concl: cterm, schematics: ctyp list * cterm list}
+ asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
+ val focus_params: Proof.context -> int -> thm -> focus * thm
+ val focus_prems: Proof.context -> int -> thm -> focus * thm
val focus: Proof.context -> int -> thm -> focus * thm
- val focus_params: Proof.context -> int -> thm -> focus * thm
val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
int -> thm -> thm -> thm Seq.seq
+ val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
+ val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
- val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
end;
@@ -24,24 +27,35 @@
(* focus *)
type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
- asms: cterm list, concl: cterm, schematics: ctyp list * cterm list};
+ asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
-fun gen_focus params_only ctxt i st =
+fun gen_focus (do_prems, do_concl) ctxt i raw_st =
let
- val ((schematics, [st']), ctxt') =
- Variable.import true [Simplifier.norm_hhf_protect st] ctxt;
- val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
+ val st = Simplifier.norm_hhf_protect raw_st;
+ val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
+ val ((params, goal), ctxt2) = Variable.focus (Thm.cprem_of st' i) ctxt1;
+
val (asms, concl) =
- if params_only then ([], goal)
- else (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal);
- val (prems, context) = Assumption.add_assumes asms ctxt'';
+ if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
+ else ([], goal);
+ val text = asms @ (if do_concl then [concl] else []);
+
+ val ((_, schematic_terms), ctxt3) =
+ Variable.import_inst true (map Thm.term_of text) ctxt2
+ |>> Thm.certify_inst (Thm.theory_of_thm raw_st);
+
+ val schematics = (schematic_types, schematic_terms);
+ val asms' = map (Thm.instantiate_cterm schematics) asms;
+ val concl' = Thm.instantiate_cterm schematics concl;
+ val (prems, context) = Assumption.add_assumes asms' ctxt3;
in
({context = context, params = params, prems = prems,
- asms = asms, concl = concl, schematics = schematics}, Goal.init concl)
+ asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
end;
-val focus = gen_focus false;
-val focus_params = gen_focus true;
+val focus_params = gen_focus (false, false);
+val focus_prems = gen_focus (true, false);
+val focus = gen_focus (true, true);
(* lift and retrofit *)
@@ -51,29 +65,40 @@
----------------
B ['b, y params]
*)
-fun lift_import params th ctxt =
+fun lift_import idx params th ctxt =
let
- val cert = Thm.cterm_of (Thm.theory_of_thm th);
+ val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
val Ts = map (#T o Thm.rep_cterm) params;
val ts = map Thm.term_of params;
- val vars = rev (Term.add_vars (Thm.full_prop_of th') []);
+ val prop = Thm.full_prop_of th';
+ val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
+ val vars = rev (Term.add_vars prop []);
val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
- fun var_inst (v as (_, T)) y =
- (cert (Var v), cert (list_comb (Free (y, Ts ---> T), ts)));
- val th'' = Thm.instantiate ([], map2 var_inst vars ys) th';
- in (th'', ctxt'') end;
+
+ fun var_inst v y =
+ let
+ val ((x, i), T) = v;
+ val (U, args) =
+ if member (op =) concl_vars v then (T, [])
+ else (Ts ---> T, ts);
+ val u = Free (y, U);
+ in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
+ val (inst1, inst2) = split_list (map (pairself (pairself cert)) (map2 var_inst vars ys));
+
+ val th'' = Thm.instantiate ([], inst1) th';
+ in ((inst2, th''), ctxt'') end;
(*
- [x, A x]
+ [x, A x]
:
- B x ==> C
+ B x ==> C
------------------
[!!x. A x ==> B x]
- :
- C
+ :
+ C
*)
fun lift_subgoals params asms th =
let
@@ -87,36 +112,37 @@
fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
let
+ val idx = Thm.maxidx_of st0 + 1;
val ps = map #2 params;
- val (st2, ctxt2) = lift_import ps st1 ctxt1;
+ val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
val (subgoals, st3) = lift_subgoals params asms st2;
val result = st3
|> Goal.conclude
|> Drule.implies_intr_list asms
|> Drule.forall_intr_list ps
|> Drule.implies_intr_list subgoals
- |> singleton (Variable.export ctxt2 ctxt0)
- |> Drule.zero_var_indexes
- |> Drule.incr_indexes st0;
+ |> fold_rev (Thm.forall_intr o #1) subgoal_inst
+ |> fold (Thm.forall_elim o #2) subgoal_inst
+ |> Thm.adjust_maxidx_thm idx
+ |> singleton (Variable.export ctxt2 ctxt0);
in Thm.compose_no_flatten false (result, Thm.nprems_of st1) i st0 end;
(* tacticals *)
-fun GEN_FOCUS params_only tac ctxt i st =
+fun GEN_FOCUS flags tac ctxt i st =
if Thm.nprems_of st < i then Seq.empty
else
- let val (args as {context, params, asms, ...}, st') = gen_focus params_only ctxt i st;
+ let val (args as {context, params, asms, ...}, st') = gen_focus flags ctxt i st;
in Seq.lifts (retrofit context ctxt params asms i) (tac args st') st end;
-val FOCUS = GEN_FOCUS false;
-val FOCUS_PARAMS = GEN_FOCUS true;
+val FOCUS_PARAMS = GEN_FOCUS (false, false);
+val FOCUS_PREMS = GEN_FOCUS (true, false);
+val FOCUS = GEN_FOCUS (true, true);
fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
end;
-val FOCUS = Subgoal.FOCUS;
-val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
val SUBPROOF = Subgoal.SUBPROOF;
--- a/src/Pure/variable.ML Fri Jul 31 09:34:05 2009 +0200
+++ b/src/Pure/variable.ML Fri Jul 31 09:34:21 2009 +0200
@@ -51,10 +51,10 @@
(((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
val importT_terms: term list -> Proof.context -> term list * Proof.context
val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
- val importT: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
+ val importT: thm list -> Proof.context -> ((ctyp * ctyp) list * thm list) * Proof.context
val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
val import: bool -> thm list -> Proof.context ->
- ((ctyp list * cterm list) * thm list) * Proof.context
+ (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context
val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
val focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
@@ -427,11 +427,10 @@
fun importT ths ctxt =
let
val thy = ProofContext.theory_of ctxt;
- val certT = Thm.ctyp_of thy;
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
- val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
- val ths' = map (Thm.instantiate (instT', [])) ths;
- in ((map #2 instT', ths'), ctxt') end;
+ val insts' as (instT', _) = Thm.certify_inst thy (instT, []);
+ val ths' = map (Thm.instantiate insts') ths;
+ in ((instT', ths'), ctxt') end;
fun import_prf is_open prf ctxt =
let
@@ -442,13 +441,10 @@
fun import is_open ths ctxt =
let
val thy = ProofContext.theory_of ctxt;
- val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
- val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
- val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
- val inst' = map (fn (v, t) => (cert (Var v), cert t)) inst;
- val ths' = map (Thm.instantiate (instT', inst')) ths;
- in (((map #2 instT', map #2 inst'), ths'), ctxt') end;
+ val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
+ val insts' = Thm.certify_inst thy insts;
+ val ths' = map (Thm.instantiate insts') ths;
+ in ((insts', ths'), ctxt') end;
(* import/export *)