src/ZF/simpdata.ML
 changeset 13462 56610e2ba220 parent 12825 f1f7964ed05c child 13780 af7b79271364
```     1.1 --- a/src/ZF/simpdata.ML	Tue Aug 06 11:20:47 2002 +0200
1.2 +++ b/src/ZF/simpdata.ML	Tue Aug 06 11:22:05 2002 +0200
1.3 @@ -11,17 +11,17 @@
1.4  (*Should False yield False<->True, or should it solve goals some other way?*)
1.5
1.6  (*Analyse a theorem to atomic rewrite rules*)
1.7 -fun atomize (conn_pairs, mem_pairs) th =
1.8 +fun atomize (conn_pairs, mem_pairs) th =
1.9    let fun tryrules pairs t =
1.11 -              Const(a,_) =>
1.12 +              Const(a,_) =>
1.13                  (case assoc(pairs,a) of
1.14                       Some rls => flat (map (atomize (conn_pairs, mem_pairs))
1.15                                         ([th] RL rls))
1.16                     | None     => [th])
1.17              | _ => [th]
1.18 -  in case concl_of th of
1.19 -         Const("Trueprop",_) \$ P =>
1.20 +  in case concl_of th of
1.21 +         Const("Trueprop",_) \$ P =>
1.22              (case P of
1.23                   Const("op :",_) \$ a \$ b => tryrules mem_pairs b
1.24                 | Const("True",_)         => []
1.25 @@ -32,13 +32,13 @@
1.26
1.27  (*Analyse a rigid formula*)
1.28  val ZF_conn_pairs =
1.29 -  [("Ball",     [bspec]),
1.30 +  [("Ball",     [bspec]),
1.31     ("All",      [spec]),
1.32     ("op -->",   [mp]),
1.33     ("op &",     [conjunct1,conjunct2])];
1.34
1.35  (*Analyse a:b, where b is rigid*)
1.36 -val ZF_mem_pairs =
1.37 +val ZF_mem_pairs =
1.38    [("Collect",  [CollectD1,CollectD2]),
1.39     ("op -",     [DiffD1,DiffD2]),
1.40     ("op Int",   [IntD1,IntD2])];
1.41 @@ -55,8 +55,8 @@
1.42  (** Splitting IFs in the assumptions **)
1.43
1.44  Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))";
1.45 -by (Simp_tac 1);
1.46 -qed "split_if_asm";
1.47 +by (Simp_tac 1);
1.48 +qed "split_if_asm";
1.49
1.50  bind_thms ("if_splits", [split_if, split_if_asm]);
1.51
1.52 @@ -65,8 +65,8 @@
1.53
1.54  local
1.55    (*For proving rewrite rules*)
1.56 -  fun prover s = (print s;prove_goalw (the_context ()) [Inter_def] s
1.57 -                  (fn _ => [Simp_tac 1,
1.58 +  fun prover s = (print s;prove_goalw (the_context ()) [Inter_def] s
1.59 +                  (fn _ => [Simp_tac 1,
1.61
1.62  in
1.63 @@ -86,7 +86,7 @@
1.64       "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
1.65       "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
1.66
1.67 -val ball_conj_distrib =
1.68 +val ball_conj_distrib =
1.69      prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
1.70
1.71  val bex_simps = map prover
1.72 @@ -104,14 +104,14 @@
1.73       "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
1.74       "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
1.75
1.76 -val bex_disj_distrib =
1.77 +val bex_disj_distrib =
1.78      prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
1.79
1.80  val Rep_simps = map prover
1.81 -    ["{x. y:0, R(x,y)} = 0",	(*Replace*)
1.82 -     "{x:0. P(x)} = 0",		(*Collect*)
1.83 +    ["{x. y:0, R(x,y)} = 0",    (*Replace*)
1.84 +     "{x:0. P(x)} = 0",         (*Collect*)
1.85       "{x:A. P} = (if P then A else 0)",
1.86 -     "RepFun(0,f) = 0",		(*RepFun*)
1.87 +     "RepFun(0,f) = 0",         (*RepFun*)
1.88       "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
1.89       "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
1.90
1.91 @@ -124,7 +124,7 @@
1.92       "Inter({b}) = b"]
1.93
1.94
1.95 -val UN_simps = map prover
1.96 +val UN_simps = map prover
1.97      ["(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))",
1.98       "(UN x:C. A(x) Un B)   = (if C=0 then 0 else (UN x:C. A(x)) Un B)",
1.99       "(UN x:C. A Un B(x))   = (if C=0 then 0 else A Un (UN x:C. B(x)))",
1.100 @@ -145,10 +145,10 @@
1.101       "(INT x:C. A(x) Un B)  = (if C=0 then 0 else (INT x:C. A(x)) Un B)",
1.102       "(INT x:C. A Un B(x))  = (if C=0 then 0 else A Un (INT x:C. B(x)))"];
1.103
1.104 -(** The _extend_simps rules are oriented in the opposite direction, to
1.105 +(** The _extend_simps rules are oriented in the opposite direction, to
1.106      pull UN and INT outwards. **)
1.107
1.108 -val UN_extend_simps = map prover
1.109 +val UN_extend_simps = map prover
1.110      ["cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))",
1.111       "(UN x:C. A(x)) Un B   = (if C=0 then B else (UN x:C. A(x) Un B))",
1.112       "A Un (UN x:C. B(x))   = (if C=0 then A else (UN x:C. A Un B(x)))",
1.113 @@ -220,30 +220,25 @@
1.114            ball_one_point1,ball_one_point2];
1.115
1.116
1.117 -let
1.118 -val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
1.119 -    ("EX x:A. P(x) & Q(x)",FOLogic.oT)
1.120 +local
1.121
1.122 -val prove_bex_tac = rewtac Bex_def THEN
1.123 -                    Quantifier1.prove_one_point_ex_tac;
1.124 -
1.125 +val prove_bex_tac = rewtac Bex_def THEN Quantifier1.prove_one_point_ex_tac;
1.126  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
1.127
1.128 -val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
1.129 -    ("ALL x:A. P(x) --> Q(x)",FOLogic.oT)
1.130 -
1.131 -val prove_ball_tac = rewtac Ball_def THEN
1.132 -                     Quantifier1.prove_one_point_all_tac;
1.133 -
1.134 +val prove_ball_tac = rewtac Ball_def THEN Quantifier1.prove_one_point_all_tac;
1.135  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
1.136
1.137 -val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
1.138 -val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
1.139  in
1.140
1.142 +val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
1.143 +  "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
1.144 +
1.145 +val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
1.146 +  "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
1.147
1.148  end;
1.149
1.151 +
1.152
1.153  val ZF_ss = simpset();
```