src/ZF/simpdata.ML
author wenzelm
Thu, 01 Dec 2005 22:03:01 +0100
changeset 18324 d1c4b1112e33
parent 17876 b9c92f384109
child 18735 f5fd06394f17
permissions -rw-r--r--
unfold_tac: static evaluation of simpset;
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*)
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    14
fun atomize (conn_pairs, mem_pairs) th =
1036
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
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    17
              Const(a,_) =>
17325
d9d50222808e introduced new-style AList operations
haftmann
parents: 17002
diff changeset
    18
                (case AList.lookup (op =) pairs a of
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    19
                     SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs))
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    20
                                       ([th] RL rls))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15092
diff changeset
    21
                   | NONE     => [th])
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    22
            | _ => [th]
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    23
  in case concl_of th of
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    24
         Const("Trueprop",_) $ P =>
1461
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 =
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    35
  [("Ball",     [bspec]),
1461
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*)
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
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
15092
7fe7f022476c keep type_solver;
wenzelm
parents: 13780
diff changeset
    48
val type_solver =
7fe7f022476c keep type_solver;
wenzelm
parents: 13780
diff changeset
    49
  mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems));
7fe7f022476c keep type_solver;
wenzelm
parents: 13780
diff changeset
    50
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 17325
diff changeset
    51
change_simpset (fn ss =>
b9c92f384109 change_claset/simpset;
wenzelm
parents: 17325
diff changeset
    52
  ss setmksimps (map mk_eq o ZF_atomize o gen_all)
12209
09bc6f8456b9 type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents: 12199
diff changeset
    53
  addcongs [if_weak_cong]
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 17325
diff changeset
    54
  setSolver type_solver);
12209
09bc6f8456b9 type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents: 12199
diff changeset
    55
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    56
local
11233
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
    57
18324
d1c4b1112e33 unfold_tac: static evaluation of simpset;
wenzelm
parents: 17876
diff changeset
    58
val unfold_bex_tac = unfold_tac [Bex_def];
d1c4b1112e33 unfold_tac: static evaluation of simpset;
wenzelm
parents: 17876
diff changeset
    59
fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
11233
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
    60
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
    61
18324
d1c4b1112e33 unfold_tac: static evaluation of simpset;
wenzelm
parents: 17876
diff changeset
    62
val unfold_ball_tac = unfold_tac [Ball_def];
d1c4b1112e33 unfold_tac: static evaluation of simpset;
wenzelm
parents: 17876
diff changeset
    63
fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
11233
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
    64
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
    65
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
    66
in
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
    67
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15570
diff changeset
    68
val defBEX_regroup = Simplifier.simproc (the_context ())
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    69
  "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    70
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15570
diff changeset
    71
val defBALL_regroup = Simplifier.simproc (the_context ())
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    72
  "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
11233
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
    73
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
    74
end;
34c81a796ee3 the one-point rule for bounded quantifiers
paulson
parents: 9907
diff changeset
    75
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    76
Addsimprocs [defBALL_regroup, defBEX_regroup];
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12825
diff changeset
    77
12199
8213fd95acb5 miniscoping of UN and INT
paulson
parents: 11695
diff changeset
    78
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3859
diff changeset
    79
val ZF_ss = simpset();