elim_cong now eta-expands proofs on the fly if required.
authorberghofe
Wed Apr 23 00:12:14 2003 +0200 (2003-04-23)
changeset 13916f078a758e5d8
parent 13915 28ccb51bd2f3
child 13917 a67c9e6570ac
elim_cong now eta-expands proofs on the fly if required.
src/HOL/Tools/rewrite_hol_proof.ML
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Wed Apr 23 00:10:40 2003 +0200
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Wed Apr 23 00:12:14 2003 +0200
     1.3 @@ -242,6 +242,8 @@
     1.4   \        (refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
     1.5   \        (refl % TYPE(bool) % A)))",
     1.6  
     1.7 +   (** transitivity, reflexivity, and symmetry **)
     1.8 +
     1.9     "(iffD1 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
    1.10   \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
    1.11  
    1.12 @@ -307,11 +309,19 @@
    1.13  fun make_sym Ts ((x, y), prf) =
    1.14    ((y, x), change_type (Some [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
    1.15  
    1.16 +fun mk_AbsP P t = AbsP ("H", P, t);
    1.17 +
    1.18  fun elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % _ % _ %% prf1 %% prf2) =
    1.19        apsome (make_subst Ts prf2 []) (strip_cong [] prf1)
    1.20 +  | elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % P % _ %% prf) =
    1.21 +      apsome (mk_AbsP P o make_subst Ts (PBound 0) [])
    1.22 +        (strip_cong [] (incr_pboundvars 1 0 prf))
    1.23    | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % _ %% prf1 %% prf2) =
    1.24        apsome (make_subst Ts prf2 [] o
    1.25          apsnd (map (make_sym Ts))) (strip_cong [] prf1)
    1.26 +  | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % P %% prf) =
    1.27 +      apsome (mk_AbsP P o make_subst Ts (PBound 0) [] o
    1.28 +        apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
    1.29    | elim_cong _ _ = None;
    1.30  
    1.31  end;