src/Pure/drule.ML
changeset 19999 9592df0c3176
parent 19906 c23a0e65b285
child 20077 4fc9a4fef219
     1.1 --- a/src/Pure/drule.ML	Tue Jul 04 19:49:49 2006 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Jul 04 19:49:50 2006 +0200
     1.3 @@ -43,7 +43,6 @@
     1.4    val standard': thm -> thm
     1.5    val rotate_prems: int -> thm -> thm
     1.6    val rearrange_prems: int list -> thm -> thm
     1.7 -  val assume_ax: theory -> string -> thm
     1.8    val RSN: thm * (int * thm) -> thm
     1.9    val RS: thm * thm -> thm
    1.10    val RLN: thm list * (int * thm list) -> thm list
    1.11 @@ -87,6 +86,7 @@
    1.12  signature DRULE =
    1.13  sig
    1.14    include BASIC_DRULE
    1.15 +  val generalize: string list * string list -> thm -> thm
    1.16    val dest_binop: cterm -> cterm * cterm
    1.17    val list_comb: cterm * cterm list -> cterm
    1.18    val strip_comb: cterm -> cterm * cterm list
    1.19 @@ -137,7 +137,6 @@
    1.20    val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
    1.21    val rename_bvars: (string * string) list -> thm -> thm
    1.22    val rename_bvars': string option list -> thm -> thm
    1.23 -  val tvars_intr_list: string list -> thm -> (string * (indexname * sort)) list * thm
    1.24    val incr_indexes: thm -> thm -> thm
    1.25    val incr_indexes2: thm -> thm -> thm -> thm
    1.26    val remdups_rl: thm
    1.27 @@ -401,6 +400,8 @@
    1.28      |> fold_rev (Thm.forall_intr o cert) ps
    1.29    end;
    1.30  
    1.31 +(*direct generalization*)
    1.32 +fun generalize names th = Thm.generalize names (Thm.maxidx_of th + 1) th;
    1.33  
    1.34  (*specialization over a list of cterms*)
    1.35  val forall_elim_list = fold forall_elim;
    1.36 @@ -489,7 +490,7 @@
    1.37   end;
    1.38  
    1.39  (*Basic version of the function above. No option to rename Vars apart in thaw.
    1.40 -  The Frees created from Vars have nice names. FIXME: does not check for 
    1.41 +  The Frees created from Vars have nice names. FIXME: does not check for
    1.42    clashes with variables in the assumptions, so delete and use freeze_thaw_robust instead?*)
    1.43  fun freeze_thaw th =
    1.44   let val fth = Thm.freezeT th
    1.45 @@ -526,15 +527,6 @@
    1.46       (permute_prems (new+1) (new-p) (permute_prems new (p-new) thm))
    1.47    in rearr 0 end;
    1.48  
    1.49 -(*Assume a new formula, read following the same conventions as axioms.
    1.50 -  Generalizes over Free variables,
    1.51 -  creates the assumption, and then strips quantifiers.
    1.52 -  Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
    1.53 -             [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
    1.54 -fun assume_ax thy sP =
    1.55 -  let val prop = Logic.close_form (term_of (read_cterm thy (sP, propT)))
    1.56 -  in forall_elim_vars 0 (Thm.assume (cterm_of thy prop)) end;
    1.57 -
    1.58  (*Resolution: exactly one resolvent must be produced.*)
    1.59  fun tha RSN (i,thb) =
    1.60    case Seq.chop 2 (biresolution false [(false,tha)] i thb) of
    1.61 @@ -1081,13 +1073,6 @@
    1.62    end;
    1.63  
    1.64  
    1.65 -(* tvars_intr_list *)
    1.66 -
    1.67 -fun tvars_intr_list tfrees thm =
    1.68 -  apfst (map (fn ((s, S), ixn) => (s, (ixn, S)))) (Thm.varifyT'
    1.69 -    (gen_rems (op = o apfst fst) (tfrees_of thm, tfrees)) thm);
    1.70 -
    1.71 -
    1.72  (* var indexes *)
    1.73  
    1.74  fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);