src/ZF/simpdata.ML
author paulson
Mon May 21 14:53:30 2001 +0200 (2001-05-21)
changeset 11323 92eddd0914a9
parent 11233 34c81a796ee3
child 11695 8c66866fb0ff
permissions -rw-r--r--
if_splits and split_if_asm
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@2469
     9
(** Rewriting **)
clasohm@0
    10
paulson@3425
    11
local
paulson@3425
    12
  (*For proving rewrite rules*)
paulson@9570
    13
  fun prover s = (prove_goal (the_context ()) s (fn _ => [Blast_tac 1]));
paulson@3425
    14
paulson@3425
    15
in
clasohm@0
    16
paulson@3425
    17
val ball_simps = map prover
paulson@3425
    18
    ["(ALL x:A. P(x) | Q)   <-> ((ALL x:A. P(x)) | Q)",
paulson@3425
    19
     "(ALL x:A. P | Q(x))   <-> (P | (ALL x:A. Q(x)))",
paulson@3425
    20
     "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
paulson@3425
    21
     "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
paulson@3425
    22
     "(ALL x:0.P(x)) <-> True",
wenzelm@3840
    23
     "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))",
wenzelm@3840
    24
     "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
paulson@2482
    25
     "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
paulson@2482
    26
     "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
nipkow@3859
    27
     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
nipkow@3859
    28
     "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
paulson@2482
    29
paulson@3425
    30
val ball_conj_distrib = 
paulson@3425
    31
    prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
paulson@3425
    32
paulson@3425
    33
val bex_simps = map prover
paulson@3425
    34
    ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
paulson@3425
    35
     "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
paulson@3425
    36
     "(EX x:0.P(x)) <-> False",
wenzelm@3840
    37
     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
wenzelm@3840
    38
     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
paulson@2482
    39
     "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
paulson@2482
    40
     "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
nipkow@3859
    41
     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
nipkow@3859
    42
     "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
paulson@2482
    43
paulson@3425
    44
val bex_disj_distrib = 
paulson@3425
    45
    prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
paulson@3425
    46
paulson@3425
    47
val Rep_simps = map prover
paulson@5202
    48
    ["{x. y:0, R(x,y)} = 0",	(*Replace*)
paulson@5202
    49
     "{x:0. P(x)} = 0",		(*Collect*)
paulson@3425
    50
     "{x:A. False} = 0",
paulson@3425
    51
     "{x:A. True} = A",
paulson@5202
    52
     "RepFun(0,f) = 0",		(*RepFun*)
paulson@3425
    53
     "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
paulson@3425
    54
     "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
clasohm@0
    55
paulson@3425
    56
val misc_simps = map prover
paulson@3425
    57
    ["0 Un A = A",  "A Un 0 = A",
paulson@3425
    58
     "0 Int A = 0", "A Int 0 = 0",
paulson@3425
    59
     "0-A = 0",     "A-0 = A",
paulson@3425
    60
     "Union(0) = 0",
paulson@3425
    61
     "Union(cons(b,A)) = b Un Union(A)",
paulson@3425
    62
     "Inter({b}) = b"]
clasohm@0
    63
paulson@3425
    64
end;
paulson@3425
    65
wenzelm@9907
    66
bind_thms ("ball_simps", ball_simps);
wenzelm@9907
    67
bind_thm ("ball_conj_distrib", ball_conj_distrib);
wenzelm@9907
    68
bind_thms ("bex_simps", bex_simps);
wenzelm@9907
    69
bind_thm ("bex_disj_distrib", bex_disj_distrib);
wenzelm@9907
    70
bind_thms ("Rep_simps", Rep_simps);
wenzelm@9907
    71
bind_thms ("misc_simps", misc_simps);
wenzelm@9907
    72
paulson@3425
    73
Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
paulson@3425
    74
clasohm@0
    75
clasohm@0
    76
(** New version of mk_rew_rules **)
clasohm@0
    77
clasohm@0
    78
(*Should False yield False<->True, or should it solve goals some other way?*)
clasohm@0
    79
lcp@1036
    80
(*Analyse a theorem to atomic rewrite rules*)
lcp@1036
    81
fun atomize (conn_pairs, mem_pairs) th = 
lcp@1036
    82
  let fun tryrules pairs t =
clasohm@1461
    83
          case head_of t of
clasohm@1461
    84
              Const(a,_) => 
clasohm@1461
    85
                (case assoc(pairs,a) of
clasohm@1461
    86
                     Some rls => flat (map (atomize (conn_pairs, mem_pairs))
clasohm@1461
    87
                                       ([th] RL rls))
clasohm@1461
    88
                   | None     => [th])
clasohm@1461
    89
            | _ => [th]
lcp@1036
    90
  in case concl_of th of 
clasohm@1461
    91
         Const("Trueprop",_) $ P => 
clasohm@1461
    92
            (case P of
clasohm@1461
    93
                 Const("op :",_) $ a $ b => tryrules mem_pairs b
clasohm@1461
    94
               | Const("True",_)         => []
clasohm@1461
    95
               | Const("False",_)        => []
clasohm@1461
    96
               | A => tryrules conn_pairs A)
lcp@1036
    97
       | _                       => [th]
lcp@1036
    98
  end;
lcp@1036
    99
clasohm@0
   100
(*Analyse a rigid formula*)
lcp@1036
   101
val ZF_conn_pairs =
clasohm@1461
   102
  [("Ball",     [bspec]), 
clasohm@1461
   103
   ("All",      [spec]),
clasohm@1461
   104
   ("op -->",   [mp]),
clasohm@1461
   105
   ("op &",     [conjunct1,conjunct2])];
clasohm@0
   106
clasohm@0
   107
(*Analyse a:b, where b is rigid*)
lcp@1036
   108
val ZF_mem_pairs = 
clasohm@1461
   109
  [("Collect",  [CollectD1,CollectD2]),
clasohm@1461
   110
   ("op -",     [DiffD1,DiffD2]),
clasohm@1461
   111
   ("op Int",   [IntD1,IntD2])];
clasohm@0
   112
lcp@1036
   113
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
lcp@1036
   114
oheimb@5553
   115
simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
paulson@9570
   116
                           addcongs [if_weak_cong]
paulson@9570
   117
		           addsplits [split_if]
nipkow@7570
   118
                           setSolver (mk_solver "types" Type_solver_tac);
paulson@2469
   119
paulson@11323
   120
(** Splitting IFs in the assumptions **)
paulson@11323
   121
paulson@11323
   122
Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))";
paulson@11323
   123
by (Simp_tac 1); 
paulson@11323
   124
qed "split_if_asm";   
paulson@11323
   125
paulson@11323
   126
bind_thms ("if_splits", [split_if, split_if_asm]);
paulson@11323
   127
paulson@11233
   128
(** One-point rule for bounded quantifiers: see HOL/Set.ML **)
paulson@11233
   129
paulson@11233
   130
Goal "(EX x:A. x=a) <-> (a:A)";
paulson@11233
   131
by (Blast_tac 1);
paulson@11233
   132
qed "bex_triv_one_point1";
paulson@11233
   133
paulson@11233
   134
Goal "(EX x:A. a=x) <-> (a:A)";
paulson@11233
   135
by (Blast_tac 1);
paulson@11233
   136
qed "bex_triv_one_point2";
paulson@11233
   137
paulson@11233
   138
Goal "(EX x:A. x=a & P(x)) <-> (a:A & P(a))";
paulson@11233
   139
by (Blast_tac 1);
paulson@11233
   140
qed "bex_one_point1";
paulson@11233
   141
paulson@11233
   142
Goal "(EX x:A. a=x & P(x)) <-> (a:A & P(a))";
paulson@11233
   143
by(Blast_tac 1);
paulson@11233
   144
qed "bex_one_point2";
paulson@11233
   145
paulson@11233
   146
Goal "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))";
paulson@11233
   147
by (Blast_tac 1);
paulson@11233
   148
qed "ball_one_point1";
paulson@11233
   149
paulson@11233
   150
Goal "(ALL x:A. a=x --> P(x)) <-> (a:A --> P(a))";
paulson@11233
   151
by (Blast_tac 1);
paulson@11233
   152
qed "ball_one_point2";
paulson@11233
   153
paulson@11233
   154
Addsimps [bex_triv_one_point1,bex_triv_one_point2,
paulson@11233
   155
          bex_one_point1,bex_one_point2,
paulson@11233
   156
          ball_one_point1,ball_one_point2];
paulson@11233
   157
paulson@11233
   158
let
paulson@11233
   159
val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
paulson@11233
   160
    ("EX x:A. P(x) & Q(x)",FOLogic.oT)
paulson@11233
   161
paulson@11233
   162
val prove_bex_tac = rewrite_goals_tac [Bex_def] THEN
paulson@11233
   163
                    Quantifier1.prove_one_point_ex_tac;
paulson@11233
   164
paulson@11233
   165
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
paulson@11233
   166
paulson@11233
   167
val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
paulson@11233
   168
    ("ALL x:A. P(x) --> Q(x)",FOLogic.oT)
paulson@11233
   169
paulson@11233
   170
val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN 
paulson@11233
   171
                     Quantifier1.prove_one_point_all_tac;
paulson@11233
   172
paulson@11233
   173
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
paulson@11233
   174
paulson@11233
   175
val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
paulson@11233
   176
val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
paulson@11233
   177
in
paulson@11233
   178
paulson@11233
   179
Addsimprocs [defBALL_regroup,defBEX_regroup]
paulson@11233
   180
paulson@11233
   181
end;
paulson@11233
   182
wenzelm@4091
   183
val ZF_ss = simpset();