src/HOL/simpdata.ML
changeset 3896 ee8ebb74ec00
parent 3842 b55686a7b22c
child 3904 c0d56e4c823e
equal deleted inserted replaced
3895:b2463861c86a 3896:ee8ebb74ec00
    78 
    78 
    79   fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
    79   fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
    80 
    80 
    81 in
    81 in
    82 
    82 
    83   fun mk_meta_eq r = case concl_of r of
    83   fun mk_meta_eq r = r RS eq_reflection;
       
    84 
       
    85   fun mk_meta_eq_simp r = case concl_of r of
    84           Const("==",_)$_$_ => r
    86           Const("==",_)$_$_ => r
    85       |   _$(Const("op =",_)$_$_) => r RS eq_reflection
    87       |   _$(Const("op =",_)$lhs$rhs) =>
       
    88              (case fst(Logic.loops (#sign(rep_thm r)) (prems_of r) lhs rhs) of
       
    89                 None => mk_meta_eq r
       
    90               | Some _ => r RS P_imp_P_eq_True)
    86       |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
    91       |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
    87       |   _ => r RS P_imp_P_eq_True;
    92       |   _ => r RS P_imp_P_eq_True;
    88   (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    93   (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    89 
    94 
    90 val simp_thms = map prover
    95 val simp_thms = map prover
   112 fun ss delcongs congs = ss deleqcongs (map standard (congs RL [eq_reflection]));
   117 fun ss delcongs congs = ss deleqcongs (map standard (congs RL [eq_reflection]));
   113 
   118 
   114 fun Addcongs congs = (simpset := !simpset addcongs congs);
   119 fun Addcongs congs = (simpset := !simpset addcongs congs);
   115 fun Delcongs congs = (simpset := !simpset delcongs congs);
   120 fun Delcongs congs = (simpset := !simpset delcongs congs);
   116 
   121 
   117 fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
   122 fun mksimps pairs = map mk_meta_eq_simp o atomize pairs o gen_all;
   118 
   123 
   119 val imp_cong = impI RSN
   124 val imp_cong = impI RSN
   120     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
   125     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
   121         (fn _=> [blast_tac HOL_cs 1]) RS mp RS mp);
   126         (fn _=> [blast_tac HOL_cs 1]) RS mp RS mp);
   122 
   127