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