src/Pure/tactic.ML
changeset 2029 2fa4c4b1a7fe
parent 1975 eec67972b1bf
child 2043 8de7a0ab463b
     1.1 --- a/src/Pure/tactic.ML	Thu Sep 26 10:34:19 1996 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Sep 26 11:10:46 1996 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4    val compose_tac: (bool * thm * int) -> int -> tactic 
     1.5    val cut_facts_tac: thm list -> int -> tactic
     1.6    val cut_inst_tac: (string*string)list -> thm -> int -> tactic   
     1.7 +  val defer_tac : int -> tactic
     1.8    val dmatch_tac: thm list -> int -> tactic
     1.9    val dresolve_tac: thm list -> int -> tactic
    1.10    val dres_inst_tac: (string*string)list -> thm -> int -> tactic   
    1.11 @@ -42,7 +43,7 @@
    1.12    val fold_tac: thm list -> tactic
    1.13    val forward_tac: thm list -> int -> tactic   
    1.14    val forw_inst_tac: (string*string)list -> thm -> int -> tactic
    1.15 -  val freeze: thm -> thm   
    1.16 +  val freeze_thaw: thm -> thm * (thm -> thm)
    1.17    val insert_tagged_brl:  ('a*(bool*thm)) * 
    1.18                      (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
    1.19                      ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
    1.20 @@ -95,22 +96,45 @@
    1.21        | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
    1.22      			 Sequence.seqof(fn()=> seqcell));
    1.23  
    1.24 -fun string_of (a,0) = a
    1.25 -  | string_of (a,i) = a ^ "_" ^ string_of_int i;
    1.26  
    1.27 -(*convert all Vars in a theorem to Frees*)
    1.28 -fun freeze th =
    1.29 -  let val fth = freezeT th
    1.30 -      val {prop,sign,...} = rep_thm fth
    1.31 -      fun mk_inst (Var(v,T)) = 
    1.32 -	  (cterm_of sign (Var(v,T)),
    1.33 -	   cterm_of sign (Free(string_of v, T)))
    1.34 -      val insts = map mk_inst (term_vars prop)
    1.35 -  in  instantiate ([],insts) fth  end;
    1.36 +(*Convert all Vars in a theorem to Frees.  Also return a function for 
    1.37 +  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
    1.38 +local
    1.39 +    fun string_of (a,0) = a
    1.40 +      | string_of (a,i) = a ^ "_" ^ string_of_int i;
    1.41 +in
    1.42 +  fun freeze_thaw th =
    1.43 +    let val fth = freezeT th
    1.44 +	val {prop,sign,...} = rep_thm fth
    1.45 +	fun mk_inst (Var(v,T)) = 
    1.46 +	    (cterm_of sign (Var(v,T)),
    1.47 +	     cterm_of sign (Free(string_of v, T)))
    1.48 +	val insts = map mk_inst (term_vars prop)
    1.49 +	fun thaw th' = 
    1.50 +	    th' |> forall_intr_list (map #2 insts)
    1.51 +		|> forall_elim_list (map #1 insts)
    1.52 +    in  (instantiate ([],insts) fth, thaw)  end;
    1.53 +end;
    1.54 +
    1.55 +
    1.56 +(*Rotates the given subgoal to be the last.  Useful when re-playing
    1.57 +  an old proof script, when the proof of an early subgoal fails.
    1.58 +  DOES NOT WORK FOR TYPE VARIABLES.*)
    1.59 +fun defer_tac i state = 
    1.60 +    let val (state',thaw) = freeze_thaw state
    1.61 +	val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
    1.62 +	val hyp::hyps' = drop(i-1,hyps)
    1.63 +    in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
    1.64 +        |> implies_intr_list (take(i-1,hyps) @ hyps')
    1.65 +        |> thaw
    1.66 +        |> Sequence.single
    1.67 +    end
    1.68 +    handle _ => Sequence.null;
    1.69 +
    1.70  
    1.71  (*Makes a rule by applying a tactic to an existing rule*)
    1.72  fun rule_by_tactic tac rl =
    1.73 -    case Sequence.pull(tac (freeze (standard rl))) of
    1.74 +    case rl |> standard |> freeze_thaw |> #1 |> tac |> Sequence.pull of
    1.75  	None        => raise THM("rule_by_tactic", 0, [rl])
    1.76        | Some(rl',_) => standard rl';
    1.77   
    1.78 @@ -234,7 +258,7 @@
    1.79    terms that are substituted contain (term or type) unknowns from the
    1.80    goal, because it is unable to instantiate goal unknowns at the same time.
    1.81  
    1.82 -  The type checker is instructed not to freezes flexible type vars that
    1.83 +  The type checker is instructed not to freeze flexible type vars that
    1.84    were introduced during type inference and still remain in the term at the
    1.85    end.  This increases flexibility but can introduce schematic type vars in
    1.86    goals.