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