# HG changeset patch # User wenzelm # Date 1372329298 -7200 # Node ID a3b175675843fbfb039017b9dc1b2561f61de4d5 # Parent 92ae850a9bfd79c39cbd27fc60e89661dcff04a1# Parent 4970437fe092bf4ab64c936ae26d4dda1b2bae42 merged diff -r 92ae850a9bfd -r a3b175675843 NEWS --- 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 *** diff -r 92ae850a9bfd -r a3b175675843 src/Doc/IsarImplementation/Proof.thy --- 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 diff -r 92ae850a9bfd -r a3b175675843 src/Doc/IsarImplementation/Tactic.thy --- 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 "\"} and @{text "\\<^sub>1 \ \ \\<^sub>n \ \"}. For each @{text "s"} that unifies @{text "\"} and @{text "\"}, the result list contains the theorem @{text "(\\<^sub>1 \ \ \\<^sub>i\<^sub>-\<^sub>1 \ \\<^sub>i\<^sub>+\<^sub>1 \ \ \\<^sub>n \ \)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}. diff -r 92ae850a9bfd -r a3b175675843 src/Provers/classical.ML --- 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)); diff -r 92ae850a9bfd -r a3b175675843 src/Pure/Syntax/syntax_phases.ML --- 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)] diff -r 92ae850a9bfd -r a3b175675843 src/Pure/Syntax/type_annotation.ML --- 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; diff -r 92ae850a9bfd -r a3b175675843 src/Pure/drule.ML --- 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 diff -r 92ae850a9bfd -r a3b175675843 src/Pure/goal.ML --- 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;