clarified defer/prefer: more specific errors;
authorwenzelm
Tue Oct 16 17:47:23 2012 +0200 (2012-10-16)
changeset 49865eeaf1ec7eac2
parent 49864 34437e7245cc
child 49866 619acbd72664
clarified defer/prefer: more specific errors;
src/HOL/BNF/Tools/bnf_tactics.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/logic.ML
src/Pure/tactic.ML
src/Pure/tactical.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_tactics.ML	Tue Oct 16 16:50:03 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Tue Oct 16 17:47:23 2012 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4  sig
     1.5    val ss_only: thm list -> simpset
     1.6  
     1.7 -  val prefer_tac: int -> tactic
     1.8    val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
     1.9    val fo_rtac: thm -> Proof.context -> int -> tactic
    1.10    val unfold_thms_tac: Proof.context -> thm list -> tactic
    1.11 @@ -39,9 +38,6 @@
    1.12  
    1.13  fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms;
    1.14  
    1.15 -(* FIXME: why not in "Pure"? *)
    1.16 -fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1);
    1.17 -
    1.18  fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
    1.19    tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
    1.20  
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Oct 16 16:50:03 2012 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 16 17:47:23 2012 +0200
     2.3 @@ -681,12 +681,11 @@
     2.4  
     2.5  val _ =
     2.6    Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
     2.7 -    (Scan.option Parse.nat >> (fn n =>
     2.8 -      (Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.defer n))));
     2.9 +    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (Proof.defer n)));
    2.10  
    2.11  val _ =
    2.12    Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
    2.13 -    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.prefer n)));
    2.14 +    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proof (Proof.prefer n)));
    2.15  
    2.16  val _ =
    2.17    Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
     3.1 --- a/src/Pure/Isar/method.ML	Tue Oct 16 16:50:03 2012 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Tue Oct 16 17:47:23 2012 +0200
     3.3 @@ -20,8 +20,6 @@
     3.4    val SIMPLE_METHOD: tactic -> method
     3.5    val SIMPLE_METHOD': (int -> tactic) -> method
     3.6    val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
     3.7 -  val defer: int option -> method
     3.8 -  val prefer: int -> method
     3.9    val cheating: bool -> Proof.context -> method
    3.10    val intro: thm list -> method
    3.11    val elim: thm list -> method
    3.12 @@ -124,12 +122,6 @@
    3.13  end;
    3.14  
    3.15  
    3.16 -(* shuffle subgoals *)
    3.17 -
    3.18 -fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)));
    3.19 -fun defer opt_i = METHOD (K (Tactic.defer_tac (the_default 1 opt_i)));
    3.20 -
    3.21 -
    3.22  (* cheating *)
    3.23  
    3.24  fun cheating int ctxt =
     4.1 --- a/src/Pure/Isar/proof.ML	Tue Oct 16 16:50:03 2012 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Tue Oct 16 17:47:23 2012 +0200
     4.3 @@ -78,8 +78,8 @@
     4.4    val end_notepad: state -> context
     4.5    val proof: Method.text option -> state -> state Seq.seq
     4.6    val proof_results: Method.text option -> state -> state Seq.result Seq.seq
     4.7 -  val defer: int option -> state -> state Seq.seq
     4.8 -  val prefer: int -> state -> state Seq.seq
     4.9 +  val defer: int -> state -> state
    4.10 +  val prefer: int -> state -> state
    4.11    val apply: Method.text -> state -> state Seq.seq
    4.12    val apply_end: Method.text -> state -> state Seq.seq
    4.13    val apply_results: Method.text -> state -> state Seq.result Seq.seq
    4.14 @@ -835,8 +835,13 @@
    4.15  
    4.16  (* unstructured refinement *)
    4.17  
    4.18 -fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i)));
    4.19 -fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i)));
    4.20 +fun defer i =
    4.21 +  assert_no_chain #>
    4.22 +  refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))) #> Seq.hd;
    4.23 +
    4.24 +fun prefer i =
    4.25 +  assert_no_chain #>
    4.26 +  refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))) #> Seq.hd;
    4.27  
    4.28  fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
    4.29  fun apply_end text = assert_forward #> refine_end text;
     5.1 --- a/src/Pure/logic.ML	Tue Oct 16 16:50:03 2012 +0200
     5.2 +++ b/src/Pure/logic.ML	Tue Oct 16 17:47:23 2012 +0200
     5.3 @@ -557,8 +557,10 @@
     5.4  
     5.5  (* goal states *)
     5.6  
     5.7 -fun get_goal st i = nth_prem (i, st)
     5.8 -  handle TERM _ => error "Goal number out of range";
     5.9 +fun get_goal st i =
    5.10 +  nth_prem (i, st) handle TERM _ =>
    5.11 +    error ("Subgoal number " ^ string_of_int i ^ " out of range (a total of " ^
    5.12 +      string_of_int (count_prems st)  ^ " subgoals)");
    5.13  
    5.14  (*reverses parameters for substitution*)
    5.15  fun goal_params st i =
     6.1 --- a/src/Pure/tactic.ML	Tue Oct 16 16:50:03 2012 +0200
     6.2 +++ b/src/Pure/tactic.ML	Tue Oct 16 17:47:23 2012 +0200
     6.3 @@ -53,6 +53,7 @@
     6.4    val rename_tac: string list -> int -> tactic
     6.5    val rotate_tac: int -> int -> tactic
     6.6    val defer_tac: int -> tactic
     6.7 +  val prefer_tac: int -> tactic
     6.8    val filter_prems_tac: (term -> bool) -> int -> tactic
     6.9  end;
    6.10  
    6.11 @@ -318,6 +319,9 @@
    6.12  (*Rotates the given subgoal to be the last.*)
    6.13  fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1);
    6.14  
    6.15 +(*Rotates the given subgoal to be the first.*)
    6.16 +fun prefer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1 #> Thm.permute_prems 0 ~1);
    6.17 +
    6.18  (* remove premises that do not satisfy p; fails if all prems satisfy p *)
    6.19  fun filter_prems_tac p =
    6.20    let fun Then NONE tac = SOME tac
     7.1 --- a/src/Pure/tactical.ML	Tue Oct 16 16:50:03 2012 +0200
     7.2 +++ b/src/Pure/tactical.ML	Tue Oct 16 17:47:23 2012 +0200
     7.3 @@ -55,6 +55,7 @@
     7.4    val TRYALL: (int -> tactic) -> tactic
     7.5    val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic
     7.6    val SUBGOAL: ((term * int) -> tactic) -> int -> tactic
     7.7 +  val ASSERT_SUBGOAL: (int -> tactic) -> int -> tactic
     7.8    val CHANGED_GOAL: (int -> tactic) -> int -> tactic
     7.9    val SOLVED': (int -> tactic) -> int -> tactic
    7.10    val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic
    7.11 @@ -328,6 +329,8 @@
    7.12  fun SUBGOAL goalfun =
    7.13    CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i));
    7.14  
    7.15 +fun ASSERT_SUBGOAL (tac: int -> tactic) i st = (Logic.get_goal (Thm.prop_of st) i; tac i st);
    7.16 +
    7.17  (*Returns all states that have changed in subgoal i, counted from the LAST
    7.18    subgoal.  For stac, for example.*)
    7.19  fun CHANGED_GOAL tac i st =