src/Provers/hypsubst.ML
changeset 21221 ef30d1e6f03a
parent 20974 2a29a21825d1
child 21227 76d6d445d69b
equal deleted inserted replaced
21220:63a7a74a9489 21221:ef30d1e6f03a
    30 \                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
    30 \                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
    31 by (blast_hyp_subst_tac (ref true) 1);
    31 by (blast_hyp_subst_tac (ref true) 1);
    32 *)
    32 *)
    33 
    33 
    34 signature HYPSUBST_DATA =
    34 signature HYPSUBST_DATA =
    35   sig
    35 sig
    36   val dest_Trueprop    : term -> term
    36   val dest_Trueprop    : term -> term
    37   val dest_eq          : term -> (term * term) *typ
    37   val dest_eq          : term -> term * term
    38   val dest_imp         : term -> term * term
    38   val dest_imp         : term -> term * term
    39   val eq_reflection    : thm               (* a=b ==> a==b *)
    39   val eq_reflection    : thm               (* a=b ==> a==b *)
    40   val rev_eq_reflection: thm               (* a==b ==> a=b *)
    40   val rev_eq_reflection: thm               (* a==b ==> a=b *)
    41   val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
    41   val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
    42   val rev_mp           : thm               (* [| P;  P-->Q |] ==> Q *)
    42   val rev_mp           : thm               (* [| P;  P-->Q |] ==> Q *)
    43   val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
    43   val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
    44   val sym              : thm               (* a=b ==> b=a *)
    44   val sym              : thm               (* a=b ==> b=a *)
    45   val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
    45   val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
    46   end;
    46 end;
    47 
       
    48 
    47 
    49 signature HYPSUBST =
    48 signature HYPSUBST =
    50   sig
    49 sig
    51   val bound_hyp_subst_tac    : int -> tactic
    50   val bound_hyp_subst_tac    : int -> tactic
    52   val hyp_subst_tac          : int -> tactic
    51   val hyp_subst_tac          : int -> tactic
    53   val blast_hyp_subst_tac    : bool ref -> int -> tactic
    52   val blast_hyp_subst_tac    : bool ref -> int -> tactic
    54     (*exported purely for debugging purposes*)
       
    55   val gen_hyp_subst_tac      : bool -> int -> tactic
       
    56   val vars_gen_hyp_subst_tac : bool -> int -> tactic
       
    57   val eq_var                 : bool -> bool -> term -> int * bool
       
    58   val inspect_pair           : bool -> bool -> (term * term) * typ -> bool
       
    59   val mk_eqs                 : bool -> thm -> thm list
       
    60   val stac                   : thm -> int -> tactic
    53   val stac                   : thm -> int -> tactic
    61   val hypsubst_setup         : theory -> theory
    54   val hypsubst_setup         : theory -> theory
    62   end;
    55 end;
    63 
       
    64 
       
    65 
    56 
    66 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
    57 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
    67 struct
    58 struct
    68 
    59 
    69 exception EQ_VAR;
    60 exception EQ_VAR;
    75 fun contract t =
    66 fun contract t =
    76   (case Pattern.eta_contract_atom t of
    67   (case Pattern.eta_contract_atom t of
    77     Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
    68     Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
    78   | t' => t');
    69   | t' => t');
    79 
    70 
    80 fun has_vars t = maxidx_of_term t <> ~1;
    71 val has_vars = Term.exists_subterm Term.is_Var;
       
    72 val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar);
    81 
    73 
    82 (*If novars then we forbid Vars in the equality.
    74 (*If novars then we forbid Vars in the equality.
    83   If bnd then we only look for Bound variables to eliminate.
    75   If bnd then we only look for Bound variables to eliminate.
    84   When can we safely delete the equality?
    76   When can we safely delete the equality?
    85     Not if it equates two constants; consider 0=1.
    77     Not if it equates two constants; consider 0=1.
    87     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
    79     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
    88     Not if it involves a variable free in the premises,
    80     Not if it involves a variable free in the premises,
    89         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
    90   Prefer to eliminate Bound variables if possible.
    82   Prefer to eliminate Bound variables if possible.
    91   Result:  true = use as is,  false = reorient first *)
    83   Result:  true = use as is,  false = reorient first *)
    92 fun inspect_pair bnd novars ((t, u), T) =
    84 fun inspect_pair bnd novars (t, u) =
    93   if novars andalso maxidx_of_typ T <> ~1
    85   if novars andalso (has_tvars t orelse has_tvars u)
    94   then raise Match   (*variables in the type!*)
    86   then raise Match   (*variables in the type!*)
    95   else
    87   else
    96   case (contract t, contract u) of
    88   case (contract t, contract u) of
    97        (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
    98                        then raise Match
    90                        then raise Match
   201                                    (r+1, imp_intr_tac i)
   193                                    (r+1, imp_intr_tac i)
   202            in
   194            in
   203                case Seq.pull(tac st) of
   195                case Seq.pull(tac st) of
   204                    NONE       => Seq.single(st)
   196                    NONE       => Seq.single(st)
   205                  | SOME(st',_) => imptac (r',hyps) st'
   197                  | SOME(st',_) => imptac (r',hyps) st'
   206            end handle _ => error "?? in blast_hyp_subst_tac"
   198            end
   207   in  imptac (0, rev hyps)  end;
   199   in  imptac (0, rev hyps)  end;
   208 
   200 
   209 
   201 
   210 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
   202 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
   211       let val (k,symopt) = eq_var false false Bi
   203       let val (k,symopt) = eq_var false false Bi