src/ZF/simpdata.ML
author paulson
Wed Apr 02 15:37:35 1997 +0200 (1997-04-02 ago)
changeset 2876 02c12d4c8b97
parent 2496 40efb87985b5
child 3425 fc4ca570d185
permissions -rw-r--r--
Uses ZF.thy again, to make that theory usable
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@2469
     9
(** Rewriting **)
clasohm@0
    10
paulson@2469
    11
(*For proving rewrite rules*)
paulson@2469
    12
fun prove_fun s = 
paulson@2876
    13
    (writeln s;  prove_goal ZF.thy s
paulson@2496
    14
       (fn prems => [ (cut_facts_tac prems 1), (Fast_tac 1) ]));
clasohm@0
    15
paulson@2469
    16
(*Are all these really suitable?*)
paulson@2482
    17
val ball_simps = map prove_fun
paulson@2482
    18
    ["(ALL x:0.P(x)) <-> True",
paulson@2482
    19
     "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
paulson@2482
    20
     "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))",
paulson@2482
    21
     "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
paulson@2482
    22
     "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
paulson@2482
    23
     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"];
paulson@2482
    24
paulson@2482
    25
val bex_simps = map prove_fun
paulson@2482
    26
    ["(EX x:0.P(x)) <-> False",
paulson@2482
    27
     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))",
paulson@2482
    28
     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B.P(x))",
paulson@2482
    29
     "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
paulson@2482
    30
     "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
paulson@2482
    31
     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"];
paulson@2482
    32
paulson@2482
    33
Addsimps (ball_simps @ bex_simps);
clasohm@0
    34
paulson@2469
    35
Addsimps (map prove_fun
paulson@2469
    36
	  ["{x:0. P(x)} = 0",
paulson@2469
    37
	   "{x:A. False} = 0",
paulson@2469
    38
	   "{x:A. True} = A",
paulson@2469
    39
	   "RepFun(0,f) = 0",
paulson@2469
    40
	   "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
paulson@2469
    41
	   "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]);
clasohm@0
    42
paulson@2469
    43
Addsimps (map prove_fun
paulson@2469
    44
	  ["0 Un A = A",  "A Un 0 = A",
paulson@2469
    45
	   "0 Int A = 0", "A Int 0 = 0",
paulson@2469
    46
	   "0-A = 0",     "A-0 = A",
paulson@2469
    47
	   "Union(0) = 0",
paulson@2469
    48
	   "Union(cons(b,A)) = b Un Union(A)",
paulson@2469
    49
	   "Inter({b}) = b"]);
clasohm@0
    50
clasohm@0
    51
(** New version of mk_rew_rules **)
clasohm@0
    52
clasohm@0
    53
(*Should False yield False<->True, or should it solve goals some other way?*)
clasohm@0
    54
lcp@1036
    55
(*Analyse a theorem to atomic rewrite rules*)
lcp@1036
    56
fun atomize (conn_pairs, mem_pairs) th = 
lcp@1036
    57
  let fun tryrules pairs t =
clasohm@1461
    58
          case head_of t of
clasohm@1461
    59
              Const(a,_) => 
clasohm@1461
    60
                (case assoc(pairs,a) of
clasohm@1461
    61
                     Some rls => flat (map (atomize (conn_pairs, mem_pairs))
clasohm@1461
    62
                                       ([th] RL rls))
clasohm@1461
    63
                   | None     => [th])
clasohm@1461
    64
            | _ => [th]
lcp@1036
    65
  in case concl_of th of 
clasohm@1461
    66
         Const("Trueprop",_) $ P => 
clasohm@1461
    67
            (case P of
clasohm@1461
    68
                 Const("op :",_) $ a $ b => tryrules mem_pairs b
clasohm@1461
    69
               | Const("True",_)         => []
clasohm@1461
    70
               | Const("False",_)        => []
clasohm@1461
    71
               | A => tryrules conn_pairs A)
lcp@1036
    72
       | _                       => [th]
lcp@1036
    73
  end;
lcp@1036
    74
clasohm@0
    75
(*Analyse a rigid formula*)
lcp@1036
    76
val ZF_conn_pairs =
clasohm@1461
    77
  [("Ball",     [bspec]), 
clasohm@1461
    78
   ("All",      [spec]),
clasohm@1461
    79
   ("op -->",   [mp]),
clasohm@1461
    80
   ("op &",     [conjunct1,conjunct2])];
clasohm@0
    81
clasohm@0
    82
(*Analyse a:b, where b is rigid*)
lcp@1036
    83
val ZF_mem_pairs = 
clasohm@1461
    84
  [("Collect",  [CollectD1,CollectD2]),
clasohm@1461
    85
   ("op -",     [DiffD1,DiffD2]),
clasohm@1461
    86
   ("op Int",   [IntD1,IntD2])];
clasohm@0
    87
lcp@1036
    88
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
lcp@1036
    89
paulson@2469
    90
simpset := !simpset setmksimps (map mk_meta_eq o ZF_atomize o gen_all);
paulson@2469
    91
paulson@2469
    92
val ZF_ss = !simpset;