src/ZF/simpdata.ML
author wenzelm
Thu, 15 Nov 2001 18:21:38 +0100
changeset 12209 09bc6f8456b9
parent 12199 8213fd95acb5
child 12484 7ad150f5fc10
permissions -rw-r--r--
type_solver_tac: use TCSET' to refer to context of goal state (does *not* work with local proof contexts of Isar / new-style locales);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title:      ZF/simpdata
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1791
diff changeset
     6
Rewriting for ZF set theory: specialized extraction of rewrites from theorems
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
12199
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
     9
(*** New version of mk_rew_rules ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
(*Should False yield False<->True, or should it solve goals some other way?*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    13
(*Analyse a theorem to atomic rewrite rules*)
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    14
fun atomize (conn_pairs, mem_pairs) th = 
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    15
  let fun tryrules pairs t =
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    16
          case head_of t of
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    17
              Const(a,_) => 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    18
                (case assoc(pairs,a) of
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    19
                     Some rls => flat (map (atomize (conn_pairs, mem_pairs))
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    20
                                       ([th] RL rls))
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    21
                   | None     => [th])
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    22
            | _ => [th]
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    23
  in case concl_of th of 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    24
         Const("Trueprop",_) $ P => 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    25
            (case P of
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    26
                 Const("op :",_) $ a $ b => tryrules mem_pairs b
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    27
               | Const("True",_)         => []
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    28
               | Const("False",_)        => []
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    29
               | A => tryrules conn_pairs A)
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    30
       | _                       => [th]
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    31
  end;
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    32
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
(*Analyse a rigid formula*)
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    34
val ZF_conn_pairs =
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    35
  [("Ball",     [bspec]), 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    36
   ("All",      [spec]),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    37
   ("op -->",   [mp]),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    38
   ("op &",     [conjunct1,conjunct2])];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
(*Analyse a:b, where b is rigid*)
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    41
val ZF_mem_pairs = 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    42
  [("Collect",  [CollectD1,CollectD2]),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    43
   ("op -",     [DiffD1,DiffD2]),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    44
   ("op Int",   [IntD1,IntD2])];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    46
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    47
12209
09bc6f8456b9 type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents: 12199
diff changeset
    48
simpset_ref() :=
09bc6f8456b9 type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents: 12199
diff changeset
    49
  simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
09bc6f8456b9 type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents: 12199
diff changeset
    50
  addcongs [if_weak_cong]
09bc6f8456b9 type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents: 12199
diff changeset
    51
  addsplits [split_if]
09bc6f8456b9 type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents: 12199
diff changeset
    52
  setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));
09bc6f8456b9 type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents: 12199
diff changeset
    53
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1791
diff changeset
    54
11323
92eddd0914a9 if_splits and split_if_asm
paulson
parents: 11233
diff changeset
    55
(** Splitting IFs in the assumptions **)
92eddd0914a9 if_splits and split_if_asm
paulson
parents: 11233
diff changeset
    56
92eddd0914a9 if_splits and split_if_asm
paulson
parents: 11233
diff changeset
    57
Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))";
92eddd0914a9 if_splits and split_if_asm
paulson
parents: 11233
diff changeset
    58
by (Simp_tac 1); 
92eddd0914a9 if_splits and split_if_asm
paulson
parents: 11233
diff changeset
    59
qed "split_if_asm";   
92eddd0914a9 if_splits and split_if_asm
paulson
parents: 11233
diff changeset
    60
92eddd0914a9 if_splits and split_if_asm
paulson
parents: 11233
diff changeset
    61
bind_thms ("if_splits", [split_if, split_if_asm]);
92eddd0914a9 if_splits and split_if_asm
paulson
parents: 11233
diff changeset
    62
12199
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    63
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    64
(*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***)
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    65
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    66
local
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    67
  (*For proving rewrite rules*)
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    68
  fun prover s = (print s;prove_goalw (the_context ()) [Inter_def] s 
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    69
                  (fn _ => [Simp_tac 1, 
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    70
                            ALLGOALS (blast_tac (claset() addSIs[equalityI]))]));
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    71
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    72
in
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    73
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    74
val ball_simps = map prover
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    75
    ["(ALL x:A. P(x) | Q)   <-> ((ALL x:A. P(x)) | Q)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    76
     "(ALL x:A. P | Q(x))   <-> (P | (ALL x:A. Q(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    77
     "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    78
     "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    79
     "(ALL x:0.P(x)) <-> True",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    80
     "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    81
     "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    82
     "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    83
     "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    84
     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    85
     "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    86
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    87
val ball_conj_distrib = 
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    88
    prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    89
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    90
val bex_simps = map prover
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    91
    ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    92
     "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    93
     "(EX x:0.P(x)) <-> False",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    94
     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    95
     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    96
     "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    97
     "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    98
     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    99
     "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   100
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   101
val bex_disj_distrib = 
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   102
    prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   103
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   104
val Rep_simps = map prover
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   105
    ["{x. y:0, R(x,y)} = 0",	(*Replace*)
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   106
     "{x:0. P(x)} = 0",		(*Collect*)
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   107
     "{x:A. False} = 0",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   108
     "{x:A. True} = A",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   109
     "RepFun(0,f) = 0",		(*RepFun*)
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   110
     "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   111
     "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   112
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   113
val misc_simps = map prover
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   114
    ["0 Un A = A", "A Un 0 = A",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   115
     "0 Int A = 0", "A Int 0 = 0",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   116
     "0 - A = 0", "A - 0 = A",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   117
     "Union(0) = 0",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   118
     "Union(cons(b,A)) = b Un Union(A)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   119
     "Inter({b}) = b"]
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   120
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   121
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   122
val UN_simps = map prover 
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   123
    ["(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   124
     "(UN x:C. A(x) Un B)   = (if C=0 then 0 else (UN x:C. A(x)) Un B)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   125
     "(UN x:C. A Un B(x))   = (if C=0 then 0 else A Un (UN x:C. B(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   126
     "(UN x:C. A(x) Int B)  = ((UN x:C. A(x)) Int B)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   127
     "(UN x:C. A Int B(x))  = (A Int (UN x:C. B(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   128
     "(UN x:C. A(x) - B)    = ((UN x:C. A(x)) - B)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   129
     "(UN x:C. A - B(x))    = (if C=0 then 0 else A - (INT x:C. B(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   130
     "(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   131
     "(UN z: (UN x:A. B(x)). C(z)) = (UN  x:A. UN z: B(x). C(z))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   132
     "(UN x: RepFun(A,f). B(x))     = (UN a:A. B(f(a)))"];
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   133
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   134
val INT_simps = map prover
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   135
    ["(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   136
     "(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   137
     "(INT x:C. A(x) - B)   = (INT x:C. A(x)) - B",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   138
     "(INT x:C. A - B(x))   = (if C=0 then 0 else A - (UN x:C. B(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   139
     "(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   140
     "(INT x:C. A(x) Un B)  = (if C=0 then 0 else (INT x:C. A(x)) Un B)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   141
     "(INT x:C. A Un B(x))  = (if C=0 then 0 else A Un (INT x:C. B(x)))"];
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   142
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   143
(** The _extend_simps rules are oriented in the opposite direction, to 
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   144
    pull UN and INT outwards. **)
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   145
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   146
val UN_extend_simps = map prover 
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   147
    ["cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   148
     "(UN x:C. A(x)) Un B   = (if C=0 then B else (UN x:C. A(x) Un B))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   149
     "A Un (UN x:C. B(x))   = (if C=0 then A else (UN x:C. A Un B(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   150
     "((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   151
     "(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   152
     "((UN x:C. A(x)) - B) = (UN x:C. A(x) - B)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   153
     "A - (INT x:C. B(x))    = (if C=0 then A else (UN x:C. A - B(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   154
     "(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   155
     "(UN  x:A. UN z: B(x). C(z)) = (UN z: (UN x:A. B(x)). C(z))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   156
     "(UN a:A. B(f(a))) = (UN x: RepFun(A,f). B(x))"];
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   157
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   158
val INT_extend_simps = map prover
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   159
    ["(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   160
     "A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   161
     "(INT x:C. A(x)) - B = (INT x:C. A(x) - B)",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   162
     "A - (UN x:C. B(x))   = (if C=0 then A else (INT x:C. A - B(x)))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   163
     "cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   164
     "(INT x:C. A(x)) Un B  = (if C=0 then B else (INT x:C. A(x) Un B))",
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   165
     "A Un (INT x:C. B(x))  = (if C=0 then A else (INT x:C. A Un B(x)))"];
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   166
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   167
end;
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   168
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   169
bind_thms ("ball_simps", ball_simps);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   170
bind_thm ("ball_conj_distrib", ball_conj_distrib);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   171
bind_thms ("bex_simps", bex_simps);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   172
bind_thm ("bex_disj_distrib", bex_disj_distrib);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   173
bind_thms ("Rep_simps", Rep_simps);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   174
bind_thms ("misc_simps", misc_simps);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   175
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   176
Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   177
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   178
bind_thms ("UN_simps", UN_simps);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   179
bind_thms ("INT_simps", INT_simps);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   180
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   181
Addsimps (UN_simps @ INT_simps);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   182
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   183
bind_thms ("UN_extend_simps", UN_extend_simps);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   184
bind_thms ("INT_extend_simps", INT_extend_simps);
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   185
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   186
11233
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   187
(** One-point rule for bounded quantifiers: see HOL/Set.ML **)
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   188
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   189
Goal "(EX x:A. x=a) <-> (a:A)";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   190
by (Blast_tac 1);
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   191
qed "bex_triv_one_point1";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   192
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   193
Goal "(EX x:A. a=x) <-> (a:A)";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   194
by (Blast_tac 1);
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   195
qed "bex_triv_one_point2";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   196
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   197
Goal "(EX x:A. x=a & P(x)) <-> (a:A & P(a))";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   198
by (Blast_tac 1);
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   199
qed "bex_one_point1";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   200
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   201
Goal "(EX x:A. a=x & P(x)) <-> (a:A & P(a))";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   202
by(Blast_tac 1);
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   203
qed "bex_one_point2";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   204
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   205
Goal "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   206
by (Blast_tac 1);
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   207
qed "ball_one_point1";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   208
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   209
Goal "(ALL x:A. a=x --> P(x)) <-> (a:A --> P(a))";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   210
by (Blast_tac 1);
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   211
qed "ball_one_point2";
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   212
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   213
Addsimps [bex_triv_one_point1,bex_triv_one_point2,
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   214
          bex_one_point1,bex_one_point2,
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   215
          ball_one_point1,ball_one_point2];
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   216
12199
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   217
11233
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   218
let
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   219
val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   220
    ("EX x:A. P(x) & Q(x)",FOLogic.oT)
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   221
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   222
val prove_bex_tac = rewrite_goals_tac [Bex_def] THEN
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   223
                    Quantifier1.prove_one_point_ex_tac;
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   224
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   225
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   226
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   227
val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   228
    ("ALL x:A. P(x) --> Q(x)",FOLogic.oT)
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   229
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   230
val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN 
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   231
                     Quantifier1.prove_one_point_all_tac;
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   232
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   233
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   234
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   235
val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   236
val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   237
in
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   238
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   239
Addsimprocs [defBALL_regroup,defBEX_regroup]
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   240
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   241
end;
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
   242
12199
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
   243
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3859
diff changeset
   244
val ZF_ss = simpset();