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;
```