src/ZF/simpdata.ML
author wenzelm
Wed Aug 25 18:36:22 2010 +0200 (2010-08-25)
changeset 38715 6513ea67d95d
parent 38513 33ab01218ae1
child 40241 56fad09655a5
permissions -rw-r--r--
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm@35762
     1
(*  Title:      ZF/simpdata.ML
clasohm@0
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     3
    Copyright   1991  University of Cambridge
clasohm@0
     4
wenzelm@35762
     5
Rewriting for ZF set theory: specialized extraction of rewrites from theorems.
clasohm@0
     6
*)
clasohm@0
     7
paulson@12199
     8
(*** New version of mk_rew_rules ***)
clasohm@0
     9
clasohm@0
    10
(*Should False yield False<->True, or should it solve goals some other way?*)
clasohm@0
    11
lcp@1036
    12
(*Analyse a theorem to atomic rewrite rules*)
wenzelm@13462
    13
fun atomize (conn_pairs, mem_pairs) th =
lcp@1036
    14
  let fun tryrules pairs t =
clasohm@1461
    15
          case head_of t of
wenzelm@13462
    16
              Const(a,_) =>
haftmann@17325
    17
                (case AList.lookup (op =) pairs a of
wenzelm@32952
    18
                     SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls)
wenzelm@32952
    19
                   | NONE => [th])
clasohm@1461
    20
            | _ => [th]
wenzelm@13462
    21
  in case concl_of th of
haftmann@38513
    22
         Const(@{const_name Trueprop},_) $ P =>
clasohm@1461
    23
            (case P of
wenzelm@24826
    24
                 Const(@{const_name mem},_) $ a $ b => tryrules mem_pairs b
haftmann@38513
    25
               | Const(@{const_name True},_)         => []
haftmann@38513
    26
               | Const(@{const_name False},_)        => []
clasohm@1461
    27
               | A => tryrules conn_pairs A)
lcp@1036
    28
       | _                       => [th]
lcp@1036
    29
  end;
lcp@1036
    30
clasohm@0
    31
(*Analyse a rigid formula*)
lcp@1036
    32
val ZF_conn_pairs =
haftmann@38513
    33
  [(@{const_name Ball}, [@{thm bspec}]),
haftmann@38513
    34
   (@{const_name All}, [@{thm spec}]),
haftmann@38513
    35
   (@{const_name "op -->"}, [@{thm mp}]),
haftmann@38513
    36
   (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}])];
clasohm@0
    37
clasohm@0
    38
(*Analyse a:b, where b is rigid*)
wenzelm@13462
    39
val ZF_mem_pairs =
haftmann@38513
    40
  [(@{const_name Collect}, [@{thm CollectD1}, @{thm CollectD2}]),
haftmann@38513
    41
   (@{const_name Diff}, [@{thm DiffD1}, @{thm DiffD2}]),
haftmann@38513
    42
   (@{const_name Int}, [@{thm IntD1}, @{thm IntD2}])];
clasohm@0
    43
lcp@1036
    44
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
lcp@1036
    45
wenzelm@17876
    46
change_simpset (fn ss =>
wenzelm@36543
    47
  ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
wenzelm@24893
    48
  addcongs [@{thm if_weak_cong}]);
wenzelm@12209
    49
wenzelm@13462
    50
local
paulson@11233
    51
wenzelm@24893
    52
val unfold_bex_tac = unfold_tac [@{thm Bex_def}];
wenzelm@18324
    53
fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
paulson@11233
    54
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
paulson@11233
    55
wenzelm@24893
    56
val unfold_ball_tac = unfold_tac [@{thm Ball_def}];
wenzelm@18324
    57
fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
paulson@11233
    58
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
paulson@11233
    59
paulson@11233
    60
in
paulson@11233
    61
wenzelm@38715
    62
val defBEX_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
wenzelm@13462
    63
  "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
wenzelm@13462
    64
wenzelm@38715
    65
val defBALL_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
wenzelm@13462
    66
  "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
paulson@11233
    67
paulson@11233
    68
end;
paulson@11233
    69
wenzelm@13462
    70
Addsimprocs [defBALL_regroup, defBEX_regroup];
wenzelm@13462
    71
paulson@12199
    72
wenzelm@24893
    73
val ZF_ss = @{simpset};
wenzelm@24893
    74