src/ZF/simpdata.ML
author wenzelm
Thu Dec 01 22:03:01 2005 +0100 (2005-12-01 ago)
changeset 18324 d1c4b1112e33
parent 17876 b9c92f384109
child 18735 f5fd06394f17
permissions -rw-r--r--
unfold_tac: static evaluation of simpset;
     1 (*  Title:      ZF/simpdata
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Rewriting for ZF set theory: specialized extraction of rewrites from theorems
     7 *)
     8 
     9 (*** New version of mk_rew_rules ***)
    10 
    11 (*Should False yield False<->True, or should it solve goals some other way?*)
    12 
    13 (*Analyse a theorem to atomic rewrite rules*)
    14 fun atomize (conn_pairs, mem_pairs) th =
    15   let fun tryrules pairs t =
    16           case head_of t of
    17               Const(a,_) =>
    18                 (case AList.lookup (op =) pairs a of
    19                      SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs))
    20                                        ([th] RL rls))
    21                    | NONE     => [th])
    22             | _ => [th]
    23   in case concl_of th of
    24          Const("Trueprop",_) $ P =>
    25             (case P of
    26                  Const("op :",_) $ a $ b => tryrules mem_pairs b
    27                | Const("True",_)         => []
    28                | Const("False",_)        => []
    29                | A => tryrules conn_pairs A)
    30        | _                       => [th]
    31   end;
    32 
    33 (*Analyse a rigid formula*)
    34 val ZF_conn_pairs =
    35   [("Ball",     [bspec]),
    36    ("All",      [spec]),
    37    ("op -->",   [mp]),
    38    ("op &",     [conjunct1,conjunct2])];
    39 
    40 (*Analyse a:b, where b is rigid*)
    41 val ZF_mem_pairs =
    42   [("Collect",  [CollectD1,CollectD2]),
    43    ("op -",     [DiffD1,DiffD2]),
    44    ("op Int",   [IntD1,IntD2])];
    45 
    46 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
    47 
    48 val type_solver =
    49   mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems));
    50 
    51 change_simpset (fn ss =>
    52   ss setmksimps (map mk_eq o ZF_atomize o gen_all)
    53   addcongs [if_weak_cong]
    54   setSolver type_solver);
    55 
    56 local
    57 
    58 val unfold_bex_tac = unfold_tac [Bex_def];
    59 fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    60 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    61 
    62 val unfold_ball_tac = unfold_tac [Ball_def];
    63 fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    64 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    65 
    66 in
    67 
    68 val defBEX_regroup = Simplifier.simproc (the_context ())
    69   "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
    70 
    71 val defBALL_regroup = Simplifier.simproc (the_context ())
    72   "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
    73 
    74 end;
    75 
    76 Addsimprocs [defBALL_regroup, defBEX_regroup];
    77 
    78 
    79 val ZF_ss = simpset();