hyp_subst_tac checks if the equality has type variables and uses a suitable
authorpaulson
Thu Nov 06 10:29:37 1997 +0100 (1997-11-06)
changeset 4179cc4b6791d5dc
parent 4178 e64ff1c1bc70
child 4180 2f0df5b390e8
hyp_subst_tac checks if the equality has type variables and uses a suitable
method if so. Affects the dest_eq function
src/FOL/ROOT.ML
src/HOL/cladata.ML
src/Provers/hypsubst.ML
     1.1 --- a/src/FOL/ROOT.ML	Thu Nov 06 10:28:20 1997 +0100
     1.2 +++ b/src/FOL/ROOT.ML	Thu Nov 06 10:29:37 1997 +0100
     1.3 @@ -27,7 +27,8 @@
     1.4    struct
     1.5    structure Simplifier = Simplifier
     1.6      (*Take apart an equality judgement; otherwise raise Match!*)
     1.7 -  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u)
     1.8 +  fun dest_eq (Const("Trueprop",_) $ (Const("op =",T)  $ t $ u)) = 
     1.9 +	(t, u, domain_type T)
    1.10    val eq_reflection = eq_reflection
    1.11    val imp_intr = impI
    1.12    val rev_mp = rev_mp
     2.1 --- a/src/HOL/cladata.ML	Thu Nov 06 10:28:20 1997 +0100
     2.2 +++ b/src/HOL/cladata.ML	Thu Nov 06 10:29:37 1997 +0100
     2.3 @@ -14,7 +14,8 @@
     2.4    struct
     2.5    structure Simplifier = Simplifier
     2.6    (*Take apart an equality judgement; otherwise raise Match!*)
     2.7 -  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
     2.8 +  fun dest_eq (Const("Trueprop",_) $ (Const("op =",T)  $ t $ u)) = 
     2.9 +	(t, u, domain_type T)
    2.10    val eq_reflection = eq_reflection
    2.11    val imp_intr = impI
    2.12    val rev_mp = rev_mp
     3.1 --- a/src/Provers/hypsubst.ML	Thu Nov 06 10:28:20 1997 +0100
     3.2 +++ b/src/Provers/hypsubst.ML	Thu Nov 06 10:29:37 1997 +0100
     3.3 @@ -25,7 +25,7 @@
     3.4  signature HYPSUBST_DATA =
     3.5    sig
     3.6    structure Simplifier : SIMPLIFIER
     3.7 -  val dest_eq	       : term -> term*term
     3.8 +  val dest_eq	       : term -> term*term*typ
     3.9    val eq_reflection    : thm		   (* a=b ==> a==b *)
    3.10    val imp_intr	       : thm		   (* (P ==> Q) ==> P-->Q *)
    3.11    val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
    3.12 @@ -42,7 +42,7 @@
    3.13    val gen_hyp_subst_tac      : bool -> int -> tactic
    3.14    val vars_gen_hyp_subst_tac : bool -> int -> tactic
    3.15    val eq_var                 : bool -> bool -> term -> int * bool
    3.16 -  val inspect_pair           : bool -> bool -> term * term -> bool
    3.17 +  val inspect_pair           : bool -> bool -> term * term * typ -> bool
    3.18    val mk_eqs                 : thm -> thm list
    3.19    val thin_leading_eqs_tac   : bool -> int -> int -> tactic
    3.20    end;
    3.21 @@ -81,7 +81,10 @@
    3.22          but we can't check for this -- hence bnd and bound_hyp_subst_tac
    3.23    Prefer to eliminate Bound variables if possible.
    3.24    Result:  true = use as is,  false = reorient first *)
    3.25 -fun inspect_pair bnd novars (t,u) =
    3.26 +fun inspect_pair bnd novars (t,u,T) =
    3.27 +  if novars andalso maxidx_of_typ T <> ~1 
    3.28 +  then raise Match   (*variables in the type!*)
    3.29 +  else
    3.30    case (contract t, contract u) of
    3.31         (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
    3.32  		       then raise Match