src/ZF/simpdata.ML
author wenzelm
Fri Apr 22 13:58:13 2011 +0200 (2011-04-22)
changeset 42455 6702c984bf5a
parent 41310 65631ca437c9
child 42794 07155da3b2f4
permissions -rw-r--r--
modernized Quantifier1 simproc setup;
     1 (*  Title:      ZF/simpdata.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1991  University of Cambridge
     4 
     5 Rewriting for ZF set theory: specialized extraction of rewrites from theorems.
     6 *)
     7 
     8 (*** New version of mk_rew_rules ***)
     9 
    10 (*Should False yield False<->True, or should it solve goals some other way?*)
    11 
    12 (*Analyse a theorem to atomic rewrite rules*)
    13 fun atomize (conn_pairs, mem_pairs) th =
    14   let fun tryrules pairs t =
    15           case head_of t of
    16               Const(a,_) =>
    17                 (case AList.lookup (op =) pairs a of
    18                      SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls)
    19                    | NONE => [th])
    20             | _ => [th]
    21   in case concl_of th of
    22          Const(@{const_name Trueprop},_) $ P =>
    23             (case P of
    24                  Const(@{const_name mem},_) $ a $ b => tryrules mem_pairs b
    25                | Const(@{const_name True},_)         => []
    26                | Const(@{const_name False},_)        => []
    27                | A => tryrules conn_pairs A)
    28        | _                       => [th]
    29   end;
    30 
    31 (*Analyse a rigid formula*)
    32 val ZF_conn_pairs =
    33   [(@{const_name Ball}, [@{thm bspec}]),
    34    (@{const_name All}, [@{thm spec}]),
    35    (@{const_name imp}, [@{thm mp}]),
    36    (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}])];
    37 
    38 (*Analyse a:b, where b is rigid*)
    39 val ZF_mem_pairs =
    40   [(@{const_name Collect}, [@{thm CollectD1}, @{thm CollectD2}]),
    41    (@{const_name Diff}, [@{thm DiffD1}, @{thm DiffD2}]),
    42    (@{const_name Int}, [@{thm IntD1}, @{thm IntD2}])];
    43 
    44 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
    45 
    46 change_simpset (fn ss =>
    47   ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
    48   addcongs [@{thm if_weak_cong}]);
    49 
    50 val ZF_ss = @{simpset};
    51