src/HOL/simpdata.ML
changeset 6128 2acc5d36610c
parent 5975 cd19eaa90f45
child 6293 2a4357301973
     1.1 --- a/src/HOL/simpdata.ML	Thu Jan 14 12:32:13 1999 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Thu Jan 14 13:18:09 1999 +0100
     1.3 @@ -64,31 +64,28 @@
     1.4  
     1.5    fun prover s = prove_goal HOL.thy s (K [Blast_tac 1]);
     1.6  
     1.7 -  val P_imp_P_iff_True = prover "P --> (P = True)" RS mp;
     1.8 -  val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
     1.9 -
    1.10 -  val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp;
    1.11 -  val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection;
    1.12 -
    1.13  in
    1.14  
    1.15  (*Make meta-equalities.  The operator below is Trueprop*)
    1.16  
    1.17 -  fun mk_meta_eq r = r RS eq_reflection;
    1.18 +fun mk_meta_eq r = r RS eq_reflection;
    1.19 +
    1.20 +val Eq_TrueI  = mk_meta_eq(prover  "P --> (P = True)"  RS mp);
    1.21 +val Eq_FalseI = mk_meta_eq(prover "~P --> (P = False)" RS mp);
    1.22  
    1.23 -  fun mk_eq th = case concl_of th of
    1.24 -          Const("==",_)$_$_       => th
    1.25 -      |   _$(Const("op =",_)$_$_) => mk_meta_eq th
    1.26 -      |   _$(Const("Not",_)$_)    => th RS not_P_imp_P_eq_False
    1.27 -      |   _                       => th RS P_imp_P_eq_True;
    1.28 -  (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    1.29 +fun mk_eq th = case concl_of th of
    1.30 +        Const("==",_)$_$_       => th
    1.31 +    |   _$(Const("op =",_)$_$_) => mk_meta_eq th
    1.32 +    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
    1.33 +    |   _                       => th RS Eq_TrueI;
    1.34 +(* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    1.35  
    1.36 -  fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
    1.37 +fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI);
    1.38  
    1.39 -  fun mk_meta_cong rl =
    1.40 -    standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    1.41 -    handle THM _ =>
    1.42 -    error("Premises and conclusion of congruence rules must be =-equalities");
    1.43 +fun mk_meta_cong rl =
    1.44 +  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    1.45 +  handle THM _ =>
    1.46 +  error("Premises and conclusion of congruence rules must be =-equalities");
    1.47  
    1.48  val not_not = prover "(~ ~ P) = P";
    1.49  
    1.50 @@ -505,6 +502,6 @@
    1.51                 eresolve_tac [disjE] 1) THEN
    1.52          ref_tac 1;
    1.53    in EVERY'[TRY o filter_prems_tac test,
    1.54 -            REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
    1.55 +            DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
    1.56              SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
    1.57    end;