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