src/ZF/simpdata.ML
author wenzelm
Mon Dec 04 22:54:31 2017 +0100 (20 months ago)
changeset 67131 85d10959c2e4
parent 59582 0fbed69ff081
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned signature;
     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 Thm.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