File ‹simpdata.ML›

(*  Title:      ZF/simpdata.ML
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Rewriting for ZF set theory: specialized extraction of rewrites from theorems.

(*** New version of mk_rew_rules ***)

(*Should False yield False<->True, or should it solve goals some other way?*)

(*Analyse a theorem to atomic rewrite rules*)
fun atomize (conn_pairs, mem_pairs) th =
  let fun tryrules pairs t =
          case head_of t of
              Const(a,_) =>
                (case AList.lookup (op =) pairs a of
                     SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls)
                   | NONE => [th])
            | _ => [th]
  in case Thm.concl_of th of
         Const_Trueprop for P =>
            (case P of
                 Const_mem for a b => tryrules mem_pairs b
               | Const_True => []
               | Const_False => []
               | A => tryrules conn_pairs A)
       | _                       => [th]

(*Analyse a rigid formula*)
val ZF_conn_pairs =
  [(const_nameBall, [@{thm bspec}]),
   (const_nameAll, [@{thm spec}]),
   (const_nameimp, [@{thm mp}]),
   (const_nameconj, [@{thm conjunct1}, @{thm conjunct2}])];

(*Analyse a:b, where b is rigid*)
val ZF_mem_pairs =
  [(const_nameCollect, [@{thm CollectD1}, @{thm CollectD2}]),
   (const_nameDiff, [@{thm DiffD1}, @{thm DiffD2}]),
   (const_nameInt, [@{thm IntD1}, @{thm IntD2}])];

val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);