# HG changeset patch # User paulson # Date 934966484 -7200 # Node ID 322151fe6f02b06b1370863617478cd2ef348415 # Parent aad87acc8fa39f0e4cb6be9e038c37de87d89a84 new primitive rule permute_prems to underlie defer_tac and rotate_prems diff -r aad87acc8fa3 -r 322151fe6f02 src/Pure/drule.ML --- 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. diff -r aad87acc8fa3 -r 322151fe6f02 src/Pure/tactic.ML --- 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 diff -r aad87acc8fa3 -r 322151fe6f02 src/Pure/thm.ML --- 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