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