--- a/NEWS Thu Jun 27 10:11:11 2013 +0200
+++ b/NEWS Thu Jun 27 12:34:58 2013 +0200
@@ -68,6 +68,10 @@
* Discontinued empty name bindings in 'axiomatization'.
INCOMPATIBILITY.
+* SELECT_GOAL now retains the syntactic context of the overall goal
+state (schematic variables etc.). Potential INCOMPATIBILITY in rare
+situations.
+
*** HOL ***
--- a/src/Doc/IsarImplementation/Proof.thy Thu Jun 27 10:11:11 2013 +0200
+++ b/src/Doc/IsarImplementation/Proof.thy Thu Jun 27 12:34:58 2013 +0200
@@ -387,7 +387,6 @@
text %mlref {*
\begin{mldecls}
- @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
@{index_ML SUBPROOF: "(Subgoal.focus -> tactic) ->
Proof.context -> int -> tactic"} \\
@{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) ->
@@ -414,10 +413,6 @@
\begin{description}
- \item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the
- specified subgoal @{text "i"}. This introduces a nested goal state,
- without decomposing the internal structure of the subgoal yet.
-
\item @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure
of the specified sub-goal, producing an extended context and a
reduced goal, which needs to be solved by the given tactic. All
--- a/src/Doc/IsarImplementation/Tactic.thy Thu Jun 27 10:11:11 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy Thu Jun 27 12:34:58 2013 +0200
@@ -179,6 +179,8 @@
@{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
@{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
@{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
+ @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
+ @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\
\end{mldecls}
\begin{description}
@@ -218,6 +220,16 @@
avoids expensive re-certification in situations where the subgoal is
used directly for primitive inferences.
+ \item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the
+ specified subgoal @{text "i"}. This rearranges subgoals and the
+ main goal protection (\secref{sec:tactical-goals}), while retaining
+ the syntactic context of the overall goal state (concerning
+ schematic variables etc.).
+
+ \item @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put
+ @{text "i"} in front. This is similar to @{ML SELECT_GOAL}, but
+ without changing the main goal protection.
+
\end{description}
*}
@@ -479,7 +491,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML compose_tac: "(bool * thm * int) -> int -> tactic"} \\
- @{index_ML compose: "thm * int * thm -> thm list"} \\
+ @{index_ML Drule.compose: "thm * int * thm -> thm list"} \\
@{index_ML_op COMP: "thm * thm -> thm"} \\
\end{mldecls}
@@ -493,14 +505,14 @@
performs elim-resolution --- it solves the first premise of @{text
"rule"} by assumption and deletes that assumption.
- \item @{ML compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
+ \item @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
regarded as an atomic formula, to solve premise @{text "i"} of
@{text "thm\<^sub>2"}. Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text
"\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}. For each @{text "s"} that unifies
@{text "\<psi>"} and @{text "\<phi>"}, the result list contains the theorem
@{text "(\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}.
- \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} calls @{text "compose (thm\<^sub>1, 1,
+ \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} calls @{text "Drule.compose (thm\<^sub>1, 1,
thm\<^sub>2)"} and returns the result, if unique; otherwise, it raises
exception @{ML THM}.
--- a/src/Provers/classical.ML Thu Jun 27 10:11:11 2013 +0200
+++ b/src/Provers/classical.ML Thu Jun 27 12:34:58 2013 +0200
@@ -802,13 +802,13 @@
fun astar_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL
- (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
+ (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
(step_tac ctxt 1));
fun slow_astar_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL
- (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
+ (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
(slow_step_tac ctxt 1));
--- a/src/Pure/Syntax/syntax_phases.ML Thu Jun 27 10:11:11 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Thu Jun 27 12:34:58 2013 +0200
@@ -533,15 +533,16 @@
fun aprop t = Syntax.const "_aprop" $ t;
fun is_prop Ts t =
- Type_Annotation.fastype_of Ts t = propT handle TERM _ => false;
+ Type_Annotation.clean (Type_Annotation.fastype_of Ts t) = propT
+ handle TERM _ => false;
fun is_term (Const ("Pure.term", _) $ _) = true
| is_term _ = false;
fun mark _ (t as Const _) = t
| mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t
- | mark _ (t as Free (x, T)) = if T = propT then aprop (Syntax.free x) else t
- | mark _ (t as Var (xi, T)) = if T = propT then aprop (Syntax.var xi) else t
+ | mark Ts (t as Free _) = if is_prop Ts t then aprop t else t
+ | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t
| mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
| mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
| mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
@@ -628,7 +629,12 @@
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
and constrain t T0 =
- let val T = Type_Annotation.smash T0 in
+ let
+ val T =
+ if show_markup andalso not show_types
+ then Type_Annotation.clean T0
+ else Type_Annotation.smash T0;
+ in
if (show_types orelse show_markup) andalso T <> dummyT then
Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
ast_of_termT ctxt trf (term_of_typ ctxt T)]
--- a/src/Pure/Syntax/type_annotation.ML Thu Jun 27 10:11:11 2013 +0200
+++ b/src/Pure/Syntax/type_annotation.ML Thu Jun 27 12:34:58 2013 +0200
@@ -10,6 +10,7 @@
val ignore_free_types: term -> term
val is_ignored: typ -> bool
val is_omitted: typ -> bool
+ val clean: typ -> typ
val smash: typ -> typ
val fastype_of: typ list -> term -> typ
end;
@@ -28,6 +29,10 @@
fun is_omitted T = is_ignored T orelse T = dummyT;
+fun clean (Type ("_ignore_type", [T])) = clean T
+ | clean (Type (a, Ts)) = Type (a, map clean Ts)
+ | clean T = T;
+
fun smash (Type ("_ignore_type", [_])) = dummyT
| smash (Type (a, Ts)) = Type (a, map smash Ts)
| smash T = T;
--- a/src/Pure/drule.ML Thu Jun 27 10:11:11 2013 +0200
+++ b/src/Pure/drule.ML Thu Jun 27 12:34:58 2013 +0200
@@ -34,7 +34,6 @@
val RL: thm list * thm list -> thm list
val MRS: thm list * thm -> thm
val OF: thm * thm list -> thm
- val compose: thm * int * thm -> thm list
val COMP: thm * thm -> thm
val INCR_COMP: thm * thm -> thm
val COMP_INCR: thm * thm -> thm
@@ -69,6 +68,7 @@
val store_standard_thm_open: binding -> thm -> thm
val multi_resolve: thm list -> thm -> thm Seq.seq
val multi_resolves: thm list -> thm list -> thm Seq.seq
+ val compose: thm * int * thm -> thm list
val compose_single: thm * int * thm -> thm
val equals_cong: thm
val imp_cong: thm
--- a/src/Pure/goal.ML Thu Jun 27 10:11:11 2013 +0200
+++ b/src/Pure/goal.ML Thu Jun 27 12:34:58 2013 +0200
@@ -51,8 +51,6 @@
({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_sorry_global: theory -> string list -> term list -> term ->
({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
@@ -349,22 +347,6 @@
(** goal structure **)
-(* nested goals *)
-
-fun extract i n st =
- (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
- else if n = 1 then Seq.single (Thm.cprem_of st i)
- else
- Seq.single (Conjunction.mk_conjunction_balanced (map (Thm.cprem_of st) (i upto i + n - 1))))
- |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
-
-fun retrofit i n st' st =
- (if n = 1 then st
- else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
- |> Thm.bicompose {flatten = false, match = false, incremented = false}
- (false, conclude st', Thm.nprems_of st') i;
-
-
(* rearrange subgoals *)
fun restrict i n st =
@@ -439,16 +421,30 @@
in fold_rev (curry op APPEND') tacs (K no_tac) i end);
-(* parallel tacticals *)
+
+(** parallel tacticals **)
-(*parallel choice of single results*)
+(* parallel choice of single results *)
+
fun PARALLEL_CHOICE tacs st =
(case Par_List.get_some (fn tac => SINGLE tac st) tacs of
NONE => Seq.empty
| SOME st' => Seq.single st');
-(*parallel refinement of non-schematic goal by single results*)
+
+(* parallel refinement of non-schematic goal by single results *)
+
+local
+
exception FAILED of unit;
+
+fun retrofit st' =
+ rotate_prems ~1 #>
+ Thm.bicompose {flatten = false, match = false, incremented = false}
+ (false, conclude st', Thm.nprems_of st') 1;
+
+in
+
fun PARALLEL_GOALS tac =
Thm.adjust_maxidx_thm ~1 #>
(fn st =>
@@ -463,10 +459,12 @@
val goals = Drule.strip_imp_prems (Thm.cprop_of st);
val results = Par_List.map (try_tac o init) goals;
- in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st end
+ in EVERY (map retrofit (rev results)) st end
handle FAILED () => Seq.empty);
end;
+end;
+
structure Basic_Goal: BASIC_GOAL = Goal;
open Basic_Goal;