--- a/src/Doc/IsarImplementation/Tactic.thy Wed Jun 26 18:26:00 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy Wed Jun 26 22:18:06 2013 +0200
@@ -53,8 +53,10 @@
with protected propositions:
\[
- \infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad
- \infer[@{text "(conclude)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}
+ \infer[@{text "(protect n)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}
+ \]
+ \[
+ \infer[@{text "(conclude)"}]{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> C"}}{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> #C"}}
\]
*}
@@ -62,7 +64,7 @@
\begin{mldecls}
@{index_ML Goal.init: "cterm -> thm"} \\
@{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\
- @{index_ML Goal.protect: "thm -> thm"} \\
+ @{index_ML Goal.protect: "int -> thm -> thm"} \\
@{index_ML Goal.conclude: "thm -> thm"} \\
\end{mldecls}
@@ -76,8 +78,9 @@
result by removing the goal protection. The context is only
required for printing error messages.
- \item @{ML "Goal.protect"}~@{text "thm"} protects the full statement
- of theorem @{text "thm"}.
+ \item @{ML "Goal.protect"}~@{text "n thm"} protects the statement
+ of theorem @{text "thm"}. The parameter @{text n} indicates the
+ number of premises to be retained.
\item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
protection, even if there are pending subgoals.
--- a/src/FOLP/intprover.ML Wed Jun 26 18:26:00 2013 +0200
+++ b/src/FOLP/intprover.ML Wed Jun 26 22:18:06 2013 +0200
@@ -9,7 +9,7 @@
Completeness (for propositional logic) is proved in
Roy Dyckhoff.
-Contraction-Free Sequent Calculi for IntPruitionistic Logic.
+Contraction-Free Sequent Calculi for Intuitionistic Logic.
J. Symbolic Logic (in press)
*)
--- a/src/HOL/Tools/Function/function_core.ML Wed Jun 26 18:26:00 2013 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Wed Jun 26 22:18:06 2013 +0200
@@ -425,7 +425,7 @@
val goalstate = Conjunction.intr graph_is_function complete
|> Thm.close_derivation
- |> Goal.protect
+ |> Goal.protect 0
|> fold_rev (Thm.implies_intr o cprop_of) compat
|> Thm.implies_intr (cprop_of complete)
in
--- a/src/Pure/Isar/obtain.ML Wed Jun 26 18:26:00 2013 +0200
+++ b/src/Pure/Isar/obtain.ML Wed Jun 26 22:18:06 2013 +0200
@@ -301,7 +301,7 @@
fun print_result ctxt' (k, [(s, [_, th])]) =
Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
- (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
+ (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
fun after_qed [[_, res]] =
Proof.end_block #> guess_context (check_result ctxt thesis res);
in
--- a/src/Pure/Isar/proof.ML Wed Jun 26 18:26:00 2013 +0200
+++ b/src/Pure/Isar/proof.ML Wed Jun 26 22:18:06 2013 +0200
@@ -402,10 +402,10 @@
ALLGOALS Goal.conjunction_tac (#2 (#2 (get_goal state)))
|> Seq.maps (fn goal =>
state
- |> Seq.lift provide_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
+ |> Seq.lift provide_goal ((PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1) goal)
|> Seq.maps meth
|> Seq.maps (fn state' => state'
- |> Seq.lift provide_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
+ |> Seq.lift provide_goal (PRIMITIVE (Goal.unrestrict 1) (#2 (#2 (get_goal state')))))
|> Seq.maps (apply_method true (K Method.succeed)));
fun apply_text cc text state =
@@ -1133,8 +1133,7 @@
val prop' = Logic.protect prop;
val statement' = (kind, [[], [prop']], prop');
- val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
- (Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
+ val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) (Goal.protect (Thm.nprems_of goal) goal);
val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th);
val result_ctxt =
--- a/src/Pure/goal.ML Wed Jun 26 18:26:00 2013 +0200
+++ b/src/Pure/goal.ML Wed Jun 26 22:18:06 2013 +0200
@@ -9,6 +9,7 @@
val skip_proofs: bool Unsynchronized.ref
val parallel_proofs: int Unsynchronized.ref
val SELECT_GOAL: tactic -> int -> tactic
+ val PREFER_GOAL: tactic -> int -> tactic
val CONJUNCTS: tactic -> int -> tactic
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
val PARALLEL_CHOICE: tactic list -> tactic
@@ -19,7 +20,7 @@
sig
include BASIC_GOAL
val init: cterm -> thm
- val protect: thm -> thm
+ val protect: int -> thm -> thm
val conclude: thm -> thm
val check_finished: Proof.context -> thm -> thm
val finish: Proof.context -> thm -> thm
@@ -52,6 +53,8 @@
({prems: thm list, context: Proof.context} -> tactic) -> thm
val extract: int -> int -> thm -> thm Seq.seq
val retrofit: int -> int -> thm -> thm -> thm Seq.seq
+ val restrict: int -> int -> thm -> thm
+ val unrestrict: int -> thm -> thm
val conjunction_tac: int -> tactic
val precise_conjunction_tac: int -> int -> tactic
val recover_conjunction_tac: tactic
@@ -73,11 +76,11 @@
in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end;
(*
- C
- --- (protect)
- #C
+ A1 ==> ... ==> An ==> C
+ ------------------------ (protect n)
+ A1 ==> ... ==> An ==> #C
*)
-fun protect th = Drule.comp_no_flatten (th, 0) 1 Drule.protectI;
+fun protect n th = Drule.comp_no_flatten (th, n) 1 Drule.protectI;
(*
A ==> ... ==> #C
@@ -361,9 +364,25 @@
|> Thm.bicompose {flatten = false, match = false, incremented = false}
(false, conclude st', Thm.nprems_of st') i;
+
+(* rearrange subgoals *)
+
+fun restrict i n st =
+ if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st
+ then raise THM ("Goal.restrict", i, [st])
+ else rotate_prems (i - 1) st |> protect n;
+
+fun unrestrict i = conclude #> rotate_prems (1 - i);
+
+(*with structural marker*)
fun SELECT_GOAL tac i st =
if Thm.nprems_of st = 1 andalso i = 1 then tac st
- else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;
+ else (PRIMITIVE (restrict i 1) THEN tac THEN PRIMITIVE (unrestrict i)) st;
+
+(*without structural marker*)
+fun PREFER_GOAL tac i st =
+ if i < 1 orelse i > Thm.nprems_of st then Seq.empty
+ else (PRIMITIVE (rotate_prems (i - 1)) THEN tac THEN PRIMITIVE (rotate_prems (1 - i))) st;
(* multiple goals *)
--- a/src/Pure/pure_syn.ML Wed Jun 26 18:26:00 2013 +0200
+++ b/src/Pure/pure_syn.ML Wed Jun 26 22:18:06 2013 +0200
@@ -9,7 +9,8 @@
val _ =
Outer_Syntax.command
- (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
+ (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML")
+ "begin theory context"
(Thy_Header.args >> (fn header =>
Toplevel.print o
Toplevel.init_theory
@@ -17,7 +18,8 @@
val _ =
Outer_Syntax.command
- (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
+ (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML")
+ "ML text from file"
(Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
let
val [{src_path, text, pos}] = files (Context.theory_of gthy);
--- a/src/Pure/simplifier.ML Wed Jun 26 18:26:00 2013 +0200
+++ b/src/Pure/simplifier.ML Wed Jun 26 22:18:06 2013 +0200
@@ -220,7 +220,7 @@
fun simp_loop_tac i =
Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN
(solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
- in SELECT_GOAL (simp_loop_tac 1) end;
+ in PREFER_GOAL (simp_loop_tac 1) end;
local
--- a/src/ZF/Constructible/Relative.thy Wed Jun 26 18:26:00 2013 +0200
+++ b/src/ZF/Constructible/Relative.thy Wed Jun 26 22:18:06 2013 +0200
@@ -753,8 +753,6 @@
"[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
==> M(RepFun(A,f))"
apply (simp add: RepFun_def)
-apply (rule strong_replacement_closed)
-apply (auto dest: transM simp add: univalent_def)
done
lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"