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.10            case head_of t of
    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.60                              ALLGOALS (blast_tac (claset() addSIs[equalityI]))]));
    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.141 -Addsimprocs [defBALL_regroup,defBEX_regroup]
   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.150 +Addsimprocs [defBALL_regroup, defBEX_regroup];
   1.151 +
   1.152  
   1.153  val ZF_ss = simpset();