New operations on cterms. Now same names as in Logic
authorpaulson
Mon Sep 23 17:45:43 1996 +0200 (1996-09-23)
changeset 20043411fe560611
parent 2003 b48f066d52dc
child 2005 a52f53caf424
New operations on cterms. Now same names as in Logic
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Mon Sep 23 17:42:56 1996 +0200
     1.2 +++ b/src/Pure/drule.ML	Mon Sep 23 17:45:43 1996 +0200
     1.3 @@ -17,8 +17,6 @@
     1.4    val COMP		: thm * thm -> thm
     1.5    val compose		: thm * int * thm -> thm list
     1.6    val cprems_of		: thm -> cterm list
     1.7 -  val cskip_flexpairs	: cterm -> cterm
     1.8 -  val cstrip_imp_prems	: cterm -> cterm list
     1.9    val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
    1.10    val cut_rl		: thm
    1.11    val equal_abs_elim	: cterm  -> thm -> thm
    1.12 @@ -35,7 +33,7 @@
    1.13    val forall_elim_vars	: int -> thm -> thm
    1.14    val implies_elim_list	: thm -> thm list -> thm
    1.15    val implies_intr_list	: cterm list -> thm -> thm
    1.16 -  val dest_cimplies     : cterm -> cterm * cterm
    1.17 +  val dest_implies      : cterm -> cterm * cterm
    1.18    val MRL		: thm list list * thm list -> thm list
    1.19    val MRS		: thm list * thm -> thm
    1.20    val read_instantiate	: (string*string)list -> thm -> thm
    1.21 @@ -46,6 +44,7 @@
    1.22                    -> string list -> (string*string)list
    1.23                    -> (indexname*ctyp)list * (cterm*cterm)list
    1.24    val reflexive_thm	: thm
    1.25 +  val refl_implies      : thm
    1.26    val revcut_rl		: thm
    1.27    val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
    1.28          -> meta_simpset -> int -> thm -> thm
    1.29 @@ -56,7 +55,9 @@
    1.30    val RL		: thm list * thm list -> thm list
    1.31    val RLN		: thm list * (int * thm list) -> thm list
    1.32    val size_of_thm	: thm -> int
    1.33 +  val skip_flexpairs	: cterm -> cterm
    1.34    val standard		: thm -> thm
    1.35 +  val strip_imp_prems	: cterm -> cterm list
    1.36    val swap_prems_rl     : thm
    1.37    val symmetric_thm	: thm
    1.38    val thin_rl		: thm
    1.39 @@ -194,32 +195,38 @@
    1.40  
    1.41  (** some cterm->cterm operations: much faster than calling cterm_of! **)
    1.42  
    1.43 +(** SAME NAMES as in structure Logic: use compound identifiers! **)
    1.44 +
    1.45  (*dest_implies for cterms. Note T=prop below*)
    1.46 -fun dest_cimplies ct =
    1.47 -  (let val (ct1, ct2) = dest_comb ct
    1.48 -       val {t, ...} = rep_cterm ct1;
    1.49 -   in case head_of t of
    1.50 -          Const("==>", _) => (snd (dest_comb ct1), ct2)
    1.51 -        | _ => raise TERM ("dest_cimplies", [term_of ct])
    1.52 -   end
    1.53 -  ) handle CTERM "dest_comb" => raise TERM ("dest_cimplies", [term_of ct]);
    1.54 +fun dest_implies ct =
    1.55 +    case term_of ct of 
    1.56 +	(Const("==>", _) $ _ $ _) => 
    1.57 +	    let val (ct1,ct2) = dest_comb ct
    1.58 +	    in  (#2 (dest_comb ct1), ct2)  end	     
    1.59 +      | _ => raise TERM ("dest_implies", [term_of ct]) ;
    1.60  
    1.61  
    1.62  (*Discard flexflex pairs; return a cterm*)
    1.63 -fun cskip_flexpairs ct =
    1.64 +fun skip_flexpairs ct =
    1.65      case term_of ct of
    1.66  	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
    1.67 -	    cskip_flexpairs (#2 (dest_cimplies ct))
    1.68 +	    skip_flexpairs (#2 (dest_implies ct))
    1.69        | _ => ct;
    1.70  
    1.71  (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
    1.72 -fun cstrip_imp_prems ct =
    1.73 -    let val (cA,cB) = dest_cimplies ct
    1.74 -    in  cA :: cstrip_imp_prems cB  end
    1.75 +fun strip_imp_prems ct =
    1.76 +    let val (cA,cB) = dest_implies ct
    1.77 +    in  cA :: strip_imp_prems cB  end
    1.78      handle TERM _ => [];
    1.79  
    1.80 +(* A1==>...An==>B  goes to B, where B is not an implication *)
    1.81 +fun strip_imp_concl ct =
    1.82 +    case term_of ct of (Const("==>", _) $ _ $ _) => 
    1.83 +	strip_imp_concl (#2 (dest_comb ct))
    1.84 +  | _ => ct;
    1.85 +
    1.86  (*The premises of a theorem, as a cterm list*)
    1.87 -val cprems_of = cstrip_imp_prems o cskip_flexpairs o cprop_of;
    1.88 +val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of;
    1.89  
    1.90  
    1.91  (** reading of instantiations **)
    1.92 @@ -518,17 +525,17 @@
    1.93  
    1.94  (** Below, a "conversion" has type cterm -> thm **)
    1.95  
    1.96 -val refl_cimplies = reflexive (cterm_of Sign.proto_pure implies);
    1.97 +val refl_implies = reflexive (cterm_of Sign.proto_pure implies);
    1.98  
    1.99  (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   1.100  (*Do not rewrite flex-flex pairs*)
   1.101  fun goals_conv pred cv =
   1.102    let fun gconv i ct =
   1.103 -        let val (A,B) = dest_cimplies ct
   1.104 +        let val (A,B) = dest_implies ct
   1.105              val (thA,j) = case term_of A of
   1.106                    Const("=?=",_)$_$_ => (reflexive A, i)
   1.107                  | _ => (if pred i then cv A else reflexive A, i+1)
   1.108 -        in  combination (combination refl_cimplies thA) (gconv j B) end
   1.109 +        in  combination (combination refl_implies thA) (gconv j B) end
   1.110          handle TERM _ => reflexive ct
   1.111    in gconv 1 end;
   1.112  
   1.113 @@ -576,7 +583,6 @@
   1.114  fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
   1.115  
   1.116  local
   1.117 -  open Logic
   1.118    val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
   1.119    fun err th = raise THM("flexpair_inst: ", 0, [th])
   1.120    fun flexpair_inst def th =