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();
```