src/ZF/simpdata.ML
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 42794 07155da3b2f4
child 59582 0fbed69ff081
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35762
af3ff2ba4c54 removed old CVS Ids;
wenzelm
parents: 35409
diff changeset
     1
(*  Title:      ZF/simpdata.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
35762
af3ff2ba4c54 removed old CVS Ids;
wenzelm
parents: 35409
diff changeset
     5
Rewriting for ZF set theory: specialized extraction of rewrites from theorems.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
12199
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
     8
(*** New version of mk_rew_rules ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
(*Should False yield False<->True, or should it solve goals some other way?*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    12
(*Analyse a theorem to atomic rewrite rules*)
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    13
fun atomize (conn_pairs, mem_pairs) th =
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    14
  let fun tryrules pairs t =
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    15
          case head_of t of
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    16
              Const(a,_) =>
17325
d9d50222808e introduced new-style AList operations
haftmann
parents: 17002
diff changeset
    17
                (case AList.lookup (op =) pairs a of
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 26499
diff changeset
    18
                     SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls)
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 26499
diff changeset
    19
                   | NONE => [th])
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    20
            | _ => [th]
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    21
  in case concl_of th of
38513
33ab01218ae1 more antiquotations
haftmann
parents: 36543
diff changeset
    22
         Const(@{const_name Trueprop},_) $ P =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    23
            (case P of
24826
78e6a3cea367 avoid unnamed infixes;
wenzelm
parents: 18735
diff changeset
    24
                 Const(@{const_name mem},_) $ a $ b => tryrules mem_pairs b
38513
33ab01218ae1 more antiquotations
haftmann
parents: 36543
diff changeset
    25
               | Const(@{const_name True},_)         => []
33ab01218ae1 more antiquotations
haftmann
parents: 36543
diff changeset
    26
               | Const(@{const_name False},_)        => []
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    27
               | A => tryrules conn_pairs A)
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    28
       | _                       => [th]
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    29
  end;
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    30
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
(*Analyse a rigid formula*)
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    32
val ZF_conn_pairs =
38513
33ab01218ae1 more antiquotations
haftmann
parents: 36543
diff changeset
    33
  [(@{const_name Ball}, [@{thm bspec}]),
33ab01218ae1 more antiquotations
haftmann
parents: 36543
diff changeset
    34
   (@{const_name All}, [@{thm spec}]),
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 40241
diff changeset
    35
   (@{const_name imp}, [@{thm mp}]),
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 40241
diff changeset
    36
   (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}])];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
(*Analyse a:b, where b is rigid*)
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    39
val ZF_mem_pairs =
38513
33ab01218ae1 more antiquotations
haftmann
parents: 36543
diff changeset
    40
  [(@{const_name Collect}, [@{thm CollectD1}, @{thm CollectD2}]),
33ab01218ae1 more antiquotations
haftmann
parents: 36543
diff changeset
    41
   (@{const_name Diff}, [@{thm DiffD1}, @{thm DiffD2}]),
33ab01218ae1 more antiquotations
haftmann
parents: 36543
diff changeset
    42
   (@{const_name Int}, [@{thm IntD1}, @{thm IntD2}])];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    44
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
    45