src/Provers/hypsubst.ML
changeset 4179 cc4b6791d5dc
parent 3537 79ac9b475621
child 4223 f60e3d2c81d3
equal deleted inserted replaced
4178:e64ff1c1bc70 4179:cc4b6791d5dc
    23 *)
    23 *)
    24 
    24 
    25 signature HYPSUBST_DATA =
    25 signature HYPSUBST_DATA =
    26   sig
    26   sig
    27   structure Simplifier : SIMPLIFIER
    27   structure Simplifier : SIMPLIFIER
    28   val dest_eq	       : term -> term*term
    28   val dest_eq	       : term -> term*term*typ
    29   val eq_reflection    : thm		   (* a=b ==> a==b *)
    29   val eq_reflection    : thm		   (* a=b ==> a==b *)
    30   val imp_intr	       : thm		   (* (P ==> Q) ==> P-->Q *)
    30   val imp_intr	       : thm		   (* (P ==> Q) ==> P-->Q *)
    31   val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
    31   val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
    32   val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
    32   val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
    33   val sym	       : thm		   (* a=b ==> b=a *)
    33   val sym	       : thm		   (* a=b ==> b=a *)
    40   val hyp_subst_tac          : int -> tactic
    40   val hyp_subst_tac          : int -> tactic
    41     (*exported purely for debugging purposes*)
    41     (*exported purely for debugging purposes*)
    42   val gen_hyp_subst_tac      : bool -> int -> tactic
    42   val gen_hyp_subst_tac      : bool -> int -> tactic
    43   val vars_gen_hyp_subst_tac : bool -> int -> tactic
    43   val vars_gen_hyp_subst_tac : bool -> int -> tactic
    44   val eq_var                 : bool -> bool -> term -> int * bool
    44   val eq_var                 : bool -> bool -> term -> int * bool
    45   val inspect_pair           : bool -> bool -> term * term -> bool
    45   val inspect_pair           : bool -> bool -> term * term * typ -> bool
    46   val mk_eqs                 : thm -> thm list
    46   val mk_eqs                 : thm -> thm list
    47   val thin_leading_eqs_tac   : bool -> int -> int -> tactic
    47   val thin_leading_eqs_tac   : bool -> int -> int -> tactic
    48   end;
    48   end;
    49 
    49 
    50 
    50 
    79     Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
    79     Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
    80     Not if it involves a variable free in the premises, 
    80     Not if it involves a variable free in the premises, 
    81         but we can't check for this -- hence bnd and bound_hyp_subst_tac
    81         but we can't check for this -- hence bnd and bound_hyp_subst_tac
    82   Prefer to eliminate Bound variables if possible.
    82   Prefer to eliminate Bound variables if possible.
    83   Result:  true = use as is,  false = reorient first *)
    83   Result:  true = use as is,  false = reorient first *)
    84 fun inspect_pair bnd novars (t,u) =
    84 fun inspect_pair bnd novars (t,u,T) =
       
    85   if novars andalso maxidx_of_typ T <> ~1 
       
    86   then raise Match   (*variables in the type!*)
       
    87   else
    85   case (contract t, contract u) of
    88   case (contract t, contract u) of
    86        (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
    89        (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
    87 		       then raise Match 
    90 		       then raise Match 
    88 		       else true		(*eliminates t*)
    91 		       else true		(*eliminates t*)
    89      | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t  
    92      | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t