--- a/src/Pure/drule.ML Wed Aug 18 10:54:03 1999 +0200
+++ b/src/Pure/drule.ML Wed Aug 18 10:54:44 1999 +0200
@@ -273,35 +273,30 @@
reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.
Similar code in type/freeze_thaw*)
fun freeze_thaw th =
- let val fth = freezeT th
- val {prop,sign,...} = rep_thm fth
- val used = add_term_names (prop, [])
- and vars = term_vars prop
- fun newName (Var(ix,_), (pairs,used)) =
- let val v = variant used (string_of_indexname ix)
- in ((ix,v)::pairs, v::used) end;
- val (alist, _) = foldr newName (vars, ([], used))
- fun mk_inst (Var(v,T)) =
- (cterm_of sign (Var(v,T)),
- cterm_of sign (Free(the (assoc(alist,v)), T)))
- val insts = map mk_inst vars
- fun thaw th' =
- th' |> forall_intr_list (map #2 insts)
- |> forall_elim_list (map #1 insts)
- in (instantiate ([],insts) fth, thaw) end;
+ let val fth = freezeT th
+ val {prop,sign,...} = rep_thm fth
+ in
+ case term_vars prop of
+ [] => (fth, fn x => x)
+ | vars =>
+ let fun newName (Var(ix,_), (pairs,used)) =
+ let val v = variant used (string_of_indexname ix)
+ in ((ix,v)::pairs, v::used) end;
+ val (alist, _) = foldr newName
+ (vars, ([], add_term_names (prop, [])))
+ fun mk_inst (Var(v,T)) =
+ (cterm_of sign (Var(v,T)),
+ cterm_of sign (Free(the (assoc(alist,v)), T)))
+ val insts = map mk_inst vars
+ fun thaw th' =
+ th' |> forall_intr_list (map #2 insts)
+ |> forall_elim_list (map #1 insts)
+ in (instantiate ([],insts) fth, thaw) end
+ end;
-(*Rotates a rule's premises to the left by k. Does nothing if k=0 or
- if k equals the number of premises. Useful, for instance, with etac.
- Similar to tactic/defer_tac*)
-fun rotate_prems k rl =
- let val (rl',thaw) = freeze_thaw rl
- val hyps = strip_imp_prems (adjust_maxidx (cprop_of rl'))
- val hyps' = List.drop(hyps, k)
- in implies_elim_list rl' (map assume hyps)
- |> implies_intr_list (hyps' @ List.take(hyps, k))
- |> thaw |> varifyT
- end;
+(*Rotates a rule's premises to the left by k*)
+val rotate_prems = permute_prems 0;
(*Assume a new formula, read following the same conventions as axioms.
--- a/src/Pure/tactic.ML Wed Aug 18 10:54:03 1999 +0200
+++ b/src/Pure/tactic.ML Wed Aug 18 10:54:44 1999 +0200
@@ -105,26 +105,6 @@
| seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected");
Seq.make(fn()=> seqcell));
-
-(*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.
- Similar to drule/rotate_prems*)
-fun defer_rule i state =
- let val (state',thaw) = freeze_thaw state
- val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
- val hyp::hyps' = List.drop(hyps, i-1)
- in implies_intr hyp (implies_elim_list state' (map assume hyps))
- |> implies_intr_list (List.take(hyps, i-1) @ hyps')
- |> thaw
- end;
-
-fun defer_tac i state =
- (case try (defer_rule i) state of
- Some state' => Seq.single state'
- | None => Seq.empty);
-
-
(*Makes a rule by applying a tactic to an existing rule*)
fun rule_by_tactic tac rl =
let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
@@ -565,6 +545,9 @@
fun rotate_tac 0 i = all_tac
| rotate_tac k i = PRIMITIVE (rotate_rule k i);
+(*Rotates the given subgoal to be the last.*)
+fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
+
(* remove premises that do not satisfy p; fails if all prems satisfy p *)
fun filter_prems_tac p =
let fun Then None tac = Some tac
--- a/src/Pure/thm.ML Wed Aug 18 10:54:03 1999 +0200
+++ b/src/Pure/thm.ML Wed Aug 18 10:54:44 1999 +0200
@@ -68,6 +68,7 @@
| Lift_rule of cterm * int
| Assumption of int * Envir.env option
| Rotate_rule of int * int
+ | Permute_prems of int * int
| Instantiate of (indexname * ctyp) list * (cterm * cterm) list
| Bicompose of bool * bool * int * int * Envir.env
| Flexflex_rule of Envir.env
@@ -139,6 +140,7 @@
val assumption : int -> thm -> thm Seq.seq
val eq_assumption : int -> thm -> thm
val rotate_rule : int -> int -> thm -> thm
+ val permute_prems : int -> int -> thm -> thm
val rename_params_rule: string list * int -> thm -> thm
val bicompose : bool -> bool * thm * int ->
int -> thm -> thm Seq.seq
@@ -344,6 +346,7 @@
| Lift_rule of cterm * int
| Assumption of int * Envir.env option (*includes eq_assumption*)
| Rotate_rule of int * int
+ | Permute_prems of int * int
| Instantiate of (indexname * ctyp) list * (cterm * cterm) list
| Bicompose of bool * bool * int * int * Envir.env
| Flexflex_rule of Envir.env (*identifies unifier chosen*)
@@ -1272,7 +1275,7 @@
Logic.list_implies(List.drop(asms, m) @
List.take(asms, m),
concl))
- else raise THM("rotate_rule", m, [state])
+ else raise THM("rotate_rule", k, [state])
in Thm{sign_ref = sign_ref,
der = infer_derivs (Rotate_rule (k,i), [der]),
maxidx = maxidx,
@@ -1282,6 +1285,33 @@
end;
+(*Rotates a rule's premises to the left by k, leaving the first j premises
+ unchanged. Does nothing if k=0 or if k equals n-j, where n is the
+ number of premises. Useful with etac and underlies tactic/defer_tac*)
+fun permute_prems j k rl =
+ let val Thm{sign_ref,der,maxidx,hyps,prop,shyps} = rl
+ val prems = Logic.strip_imp_prems prop
+ and concl = Logic.strip_imp_concl prop
+ val moved_prems = List.drop(prems, j)
+ and fixed_prems = List.take(prems, j)
+ handle Subscript => raise THM("permute_prems:j", j, [rl])
+ val n_j = length moved_prems
+ fun rot m = if 0 = m orelse m = n_j then prop
+ else if 0<m andalso m<n_j
+ then Logic.list_implies(fixed_prems @
+ List.drop(moved_prems, m) @
+ List.take(moved_prems, m),
+ concl)
+ else raise THM("permute_prems:k", k, [rl])
+ in Thm{sign_ref = sign_ref,
+ der = infer_derivs (Permute_prems (j,k), [der]),
+ maxidx = maxidx,
+ shyps = shyps,
+ hyps = hyps,
+ prop = rot (if k<0 then n_j + k else k)}
+ end;
+
+
(** User renaming of parameters in a subgoal **)
(*Calls error rather than raising an exception because it is intended