src/Pure/tactic.ML

--- a/src/Pure/tactic.ML	Thu Sep 26 10:34:19 1996 +0200
+++ b/src/Pure/tactic.ML	Thu Sep 26 11:10:46 1996 +0200
@@ -26,6 +26,7 @@
   val compose_tac: (bool * thm * int) -> int -> tactic 
   val cut_facts_tac: thm list -> int -> tactic
   val cut_inst_tac: (string*string)list -> thm -> int -> tactic   
+  val defer_tac : int -> tactic
   val dmatch_tac: thm list -> int -> tactic
   val dresolve_tac: thm list -> int -> tactic
   val dres_inst_tac: (string*string)list -> thm -> int -> tactic   
@@ -42,7 +43,7 @@
   val fold_tac: thm list -> tactic
   val forward_tac: thm list -> int -> tactic   
   val forw_inst_tac: (string*string)list -> thm -> int -> tactic
-  val freeze: thm -> thm   
+  val freeze_thaw: thm -> thm * (thm -> thm)
   val insert_tagged_brl:  ('a*(bool*thm)) * 
                     (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
                     ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
@@ -95,22 +96,45 @@
       | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
     			 Sequence.seqof(fn()=> seqcell));
 
-fun string_of (a,0) = a
-  | string_of (a,i) = a ^ "_" ^ string_of_int i;
 
-(*convert all Vars in a theorem to Frees*)
-fun freeze th =
-  let val fth = freezeT th
-      val {prop,sign,...} = rep_thm fth
-      fun mk_inst (Var(v,T)) = 
-	  (cterm_of sign (Var(v,T)),
-	   cterm_of sign (Free(string_of v, T)))
-      val insts = map mk_inst (term_vars prop)
-  in  instantiate ([],insts) fth  end;
+(*Convert all Vars in a theorem to Frees.  Also return a function for 
+  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
+local
+    fun string_of (a,0) = a
+      | string_of (a,i) = a ^ "_" ^ string_of_int i;
+in
+  fun freeze_thaw th =
+    let val fth = freezeT th
+	val {prop,sign,...} = rep_thm fth
+	fun mk_inst (Var(v,T)) = 
+	    (cterm_of sign (Var(v,T)),
+	     cterm_of sign (Free(string_of v, T)))
+	val insts = map mk_inst (term_vars prop)
+	fun thaw th' = 
+	    th' |> forall_intr_list (map #2 insts)
+		|> forall_elim_list (map #1 insts)
+    in  (instantiate ([],insts) fth, thaw)  end;
+end;
+
+
+(*Rotates the given subgoal to be the last.  Useful when re-playing
+  an old proof script, when the proof of an early subgoal fails.
+  DOES NOT WORK FOR TYPE VARIABLES.*)
+fun defer_tac i state = 
+    let val (state',thaw) = freeze_thaw state
+	val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
+	val hyp::hyps' = drop(i-1,hyps)
+    in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
+        |> implies_intr_list (take(i-1,hyps) @ hyps')
+        |> thaw
+        |> Sequence.single
+    end
+    handle _ => Sequence.null;
+
 
 (*Makes a rule by applying a tactic to an existing rule*)
 fun rule_by_tactic tac rl =
-    case Sequence.pull(tac (freeze (standard rl))) of
+    case rl |> standard |> freeze_thaw |> #1 |> tac |> Sequence.pull of
 	None        => raise THM("rule_by_tactic", 0, [rl])
       | Some(rl',_) => standard rl';
  
@@ -234,7 +258,7 @@
   terms that are substituted contain (term or type) unknowns from the
   goal, because it is unable to instantiate goal unknowns at the same time.
 
-  The type checker is instructed not to freezes flexible type vars that
+  The type checker is instructed not to freeze flexible type vars that
   were introduced during type inference and still remain in the term at the
   end.  This increases flexibility but can introduce schematic type vars in
   goals.