src/FOLP/IFOLP.ML
changeset 15570 8d8c70b41bab
parent 9263 53e09e592278
child 17480 fd19f77dcf60
equal deleted inserted replaced
15569:1b3115d1a8df 15570:8d8c70b41bab
    76     (fn (prem,i) =>
    76     (fn (prem,i) =>
    77       let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
    77       let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
    78           and concl = discard_proof (Logic.strip_assums_concl prem)
    78           and concl = discard_proof (Logic.strip_assums_concl prem)
    79       in  
    79       in  
    80           if exists (fn hyp => hyp aconv concl) hyps
    80           if exists (fn hyp => hyp aconv concl) hyps
    81           then case distinct (filter (fn hyp=> could_unify(hyp,concl)) hyps) of
    81           then case distinct (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
    82                    [_] => assume_tac i
    82                    [_] => assume_tac i
    83                  |  _  => no_tac
    83                  |  _  => no_tac
    84           else no_tac
    84           else no_tac
    85       end);
    85       end);
    86 end;
    86 end;
   308 qed "pred3_cong";
   308 qed "pred3_cong";
   309 
   309 
   310 (*special cases for free variables P, Q, R, S -- up to 3 arguments*)
   310 (*special cases for free variables P, Q, R, S -- up to 3 arguments*)
   311 
   311 
   312 val pred_congs = 
   312 val pred_congs = 
   313     flat (map (fn c => 
   313     List.concat (map (fn c => 
   314                map (fn th => read_instantiate [("P",c)] th)
   314                map (fn th => read_instantiate [("P",c)] th)
   315                    [pred1_cong,pred2_cong,pred3_cong])
   315                    [pred1_cong,pred2_cong,pred3_cong])
   316                (explode"PQRS"));
   316                (explode"PQRS"));
   317 
   317 
   318 (*special case for the equality predicate!*)
   318 (*special case for the equality predicate!*)