src/Pure/drule.ML
changeset 13659 3cf622f6b0b2
parent 13650 31bd2a8cdbe2
child 14081 6c0f67e2f8d5
     1.1 --- a/src/Pure/drule.ML	Mon Oct 21 17:04:47 2002 +0200
     1.2 +++ b/src/Pure/drule.ML	Mon Oct 21 17:07:27 2002 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4    val list_implies      : cterm list * cterm -> cterm
     1.5    val dest_implies      : cterm -> cterm * cterm
     1.6    val dest_equals       : cterm -> cterm * cterm
     1.7 -  val skip_flexpairs    : cterm -> cterm
     1.8    val strip_imp_prems   : cterm -> cterm list
     1.9    val strip_imp_concl   : cterm -> cterm
    1.10    val cprems_of         : thm -> cterm list
    1.11 @@ -69,7 +68,6 @@
    1.12    val swap_prems_eq     : thm
    1.13    val equal_abs_elim    : cterm  -> thm -> thm
    1.14    val equal_abs_elim_list: cterm list -> thm -> thm
    1.15 -  val flexpair_abs_elim_list: cterm list -> thm -> thm
    1.16    val asm_rl            : thm
    1.17    val cut_rl            : thm
    1.18    val revcut_rl         : thm
    1.19 @@ -159,13 +157,6 @@
    1.20        | _ => raise TERM ("dest_equals", [term_of ct]) ;
    1.21  
    1.22  
    1.23 -(*Discard flexflex pairs; return a cterm*)
    1.24 -fun skip_flexpairs ct =
    1.25 -    case term_of ct of
    1.26 -        (Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
    1.27 -            skip_flexpairs (#2 (dest_implies ct))
    1.28 -      | _ => ct;
    1.29 -
    1.30  (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
    1.31  fun strip_imp_prems ct =
    1.32      let val (cA,cB) = dest_implies ct
    1.33 @@ -179,7 +170,7 @@
    1.34    | _ => ct;
    1.35  
    1.36  (*The premises of a theorem, as a cterm list*)
    1.37 -val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of;
    1.38 +val cprems_of = strip_imp_prems o cprop_of;
    1.39  
    1.40  val proto_sign = Theory.sign_of ProtoPure.thy;
    1.41  
    1.42 @@ -403,16 +394,16 @@
    1.43    Similar code in type/freeze_thaw*)
    1.44  fun freeze_thaw th =
    1.45   let val fth = freezeT th
    1.46 -     val {prop,sign,...} = rep_thm fth
    1.47 +     val {prop, tpairs, sign, ...} = rep_thm fth
    1.48   in
    1.49 -   case term_vars prop of
    1.50 +   case foldr add_term_vars (prop :: Thm.terms_of_tpairs tpairs, []) of
    1.51         [] => (fth, fn x => x)
    1.52       | vars =>
    1.53           let fun newName (Var(ix,_), (pairs,used)) =
    1.54                     let val v = variant used (string_of_indexname ix)
    1.55                     in  ((ix,v)::pairs, v::used)  end;
    1.56 -             val (alist, _) = foldr newName
    1.57 -                                (vars, ([], add_term_names (prop, [])))
    1.58 +             val (alist, _) = foldr newName (vars, ([], foldr add_term_names
    1.59 +               (prop :: Thm.terms_of_tpairs tpairs, [])))
    1.60               fun mk_inst (Var(v,T)) =
    1.61                   (cterm_of sign (Var(v,T)),
    1.62                    cterm_of sign (Free(the (assoc(alist,v)), T)))
    1.63 @@ -791,27 +782,6 @@
    1.64  (*Calling equal_abs_elim with multiple terms*)
    1.65  fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
    1.66  
    1.67 -local
    1.68 -  val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
    1.69 -  fun err th = raise THM("flexpair_inst: ", 0, [th])
    1.70 -  fun flexpair_inst def th =
    1.71 -    let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
    1.72 -        val cterm = cterm_of sign
    1.73 -        fun cvar a = cterm(Var((a,0),alpha))
    1.74 -        val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)]
    1.75 -                   def
    1.76 -    in  equal_elim def' th
    1.77 -    end
    1.78 -    handle THM _ => err th | Bind => err th
    1.79 -in
    1.80 -val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def)
    1.81 -and flexpair_elim = flexpair_inst ProtoPure.flexpair_def
    1.82 -end;
    1.83 -
    1.84 -(*Version for flexflex pairs -- this supports lifting.*)
    1.85 -fun flexpair_abs_elim_list cts =
    1.86 -    flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
    1.87 -
    1.88  
    1.89  (*** Goal (PROP A) <==> PROP A ***)
    1.90