src/ZF/simpdata.ML
author haftmann
Wed, 12 May 2021 17:05:29 +0000
changeset 73682 78044b2f001c
parent 69593 3dda49e08b9d
permissions -rw-r--r--
explicit type class operations for type-specific implementations
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]
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 42794
diff changeset
    21
  in case Thm.concl_of th of
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 59582
diff changeset
    22
         Const(\<^const_name>\<open>Trueprop\<close>,_) $ P =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    23
            (case P of
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 59582
diff changeset
    24
                 Const(\<^const_name>\<open>mem\<close>,_) $ a $ b => tryrules mem_pairs b
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 59582
diff changeset
    25
               | Const(\<^const_name>\<open>True\<close>,_)         => []
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 59582
diff changeset
    26
               | Const(\<^const_name>\<open>False\<close>,_)        => []
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 =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 59582
diff changeset
    33
  [(\<^const_name>\<open>Ball\<close>, [@{thm bspec}]),
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 59582
diff changeset
    34
   (\<^const_name>\<open>All\<close>, [@{thm spec}]),
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 59582
diff changeset
    35
   (\<^const_name>\<open>imp\<close>, [@{thm mp}]),
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 59582
diff changeset
    36
   (\<^const_name>\<open>conj\<close>, [@{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 =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 59582
diff changeset
    40
  [(\<^const_name>\<open>Collect\<close>, [@{thm CollectD1}, @{thm CollectD2}]),
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 59582
diff changeset
    41
   (\<^const_name>\<open>Diff\<close>, [@{thm DiffD1}, @{thm DiffD2}]),
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 59582
diff changeset
    42
   (\<^const_name>\<open>Int\<close>, [@{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