src/ZF/simpdata.ML
changeset 279 7738aed3f84d
parent 14 1c0926788772
child 435 ca5356bd315a
equal deleted inserted replaced
278:523518f44286 279:7738aed3f84d
    84       | _ $ (Const("True",_)) => []	(*True is DELETED*)
    84       | _ $ (Const("True",_)) => []	(*True is DELETED*)
    85       | _ $ (Const("False",_)) => []	(*should False do something??*)
    85       | _ $ (Const("False",_)) => []	(*should False do something??*)
    86       | _ $ A => tryrules atomize_pairs A
    86       | _ $ A => tryrules atomize_pairs A
    87   end;
    87   end;
    88 
    88 
    89 fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
       
    90 
       
    91 
       
    92 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
    89 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
    93 		beta, eta, restrict, fst_conv, snd_conv, split];
    90 		beta, eta, restrict, fst_conv, snd_conv, split];
    94 
    91 
    95 (*Sigma_cong, Pi_cong NOT included by default since they cause
    92 (*Sigma_cong, Pi_cong NOT included by default since they cause
    96   flex-flex pairs and the "Check your prover" error -- because most
    93   flex-flex pairs and the "Check your prover" error -- because most
    97   Sigma's and Pi's are abbreviated as * or -> *)
    94   Sigma's and Pi's are abbreviated as * or -> *)
    98 val ZF_congs =
    95 val ZF_congs =
    99    [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
    96    [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
   100 
    97 
   101 val ZF_ss = FOL_ss 
    98 val ZF_ss = FOL_ss 
   102       setmksimps ZF_mk_rew_rules
    99       setmksimps (map mk_meta_eq o atomize o gen_all)
   103       addsimps (ZF_simps @ mem_simps @ bquant_simps)
   100       addsimps (ZF_simps @ mem_simps @ bquant_simps)
   104       addcongs ZF_congs;
   101       addcongs ZF_congs;