src/ZF/simpdata.ML
 changeset 467 92868dab2939 parent 435 ca5356bd315a child 485 5e00a676a211
equal 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 =`