src/ZF/simpdata.ML
changeset 467 92868dab2939
parent 435 ca5356bd315a
child 485 5e00a676a211
equal deleted inserted replaced
466:08d1cce222e1 467:92868dab2939
    16    "a : A Un B        <-> a:A | a:B",
    16    "a : A Un B        <-> a:A | a:B",
    17    "a : A Int B       <-> a:A & a:B",
    17    "a : A Int B       <-> a:A & a:B",
    18    "a : A-B           <-> a:A & ~a:B",
    18    "a : A-B           <-> a:A & ~a:B",
    19    "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
    19    "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
    20    "a : Collect(A,P)  <-> a:A & P(a)" ];
    20    "a : Collect(A,P)  <-> a:A & P(a)" ];
       
    21 
       
    22 goal ZF.thy "{x.x:A} = A";
       
    23 by (fast_tac eq_cs 1);
       
    24 val triv_RepFun = result();
    21 
    25 
    22 (*INCLUDED: should be??*)
    26 (*INCLUDED: should be??*)
    23 val bquant_simps = map prove_fun
    27 val bquant_simps = map prove_fun
    24  [ "(ALL x:0.P(x)) <-> True",
    28  [ "(ALL x:0.P(x)) <-> True",
    25    "(EX  x:0.P(x)) <-> False",
    29    "(EX  x:0.P(x)) <-> False",
    88 	     | A => tryrules atomize_pairs A)
    92 	     | A => tryrules atomize_pairs A)
    89      | _                       => [th]
    93      | _                       => [th]
    90   end;
    94   end;
    91 
    95 
    92 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
    96 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
    93 		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff];
    97 		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff,
       
    98 		triv_RepFun];
    94 
    99 
    95 (*Sigma_cong, Pi_cong NOT included by default since they cause
   100 (*Sigma_cong, Pi_cong NOT included by default since they cause
    96   flex-flex pairs and the "Check your prover" error -- because most
   101   flex-flex pairs and the "Check your prover" error -- because most
    97   Sigma's and Pi's are abbreviated as * or -> *)
   102   Sigma's and Pi's are abbreviated as * or -> *)
    98 val ZF_congs =
   103 val ZF_congs =