src/ZF/simpdata.ML
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
     1.1 --- a/src/ZF/simpdata.ML	Fri Sep 17 12:53:53 1993 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Fri Sep 17 16:16:38 1993 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4      (writeln s;  prove_goal ZF.thy s
     1.5         (fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));
     1.6  
     1.7 -val mem_rews = map prove_fun
     1.8 +val mem_simps = map prove_fun
     1.9   [ "a:0 <-> False",
    1.10     "a : A Un B <-> a:A | a:B",
    1.11     "a : A Int B <-> a:A & a:B",
    1.12 @@ -45,7 +45,7 @@
    1.13    NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
    1.14  fun type_auto_tac tyrls hyps = SELECT_GOAL
    1.15      (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
    1.16 -           ORELSE ares_tac [TrueI,ballI,allI,conjI,impI] 1));
    1.17 +           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
    1.18  
    1.19  (** New version of mk_rew_rules **)
    1.20  
    1.21 @@ -80,41 +80,19 @@
    1.22        | _ $ A => tryrules atomize_pairs A
    1.23    end;
    1.24  
    1.25 -fun ZF_mk_rew_rules th = map mk_eq (atomize th);
    1.26 +fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
    1.27  
    1.28  
    1.29 -fun auto_tac rls hyps = SELECT_GOAL (DEPTH_SOLVE_1 (ares_tac (rls@hyps) 1));
    1.30 -
    1.31 -structure ZF_SimpData : SIMP_DATA =
    1.32 -  struct
    1.33 -  val refl_thms		= FOL_SimpData.refl_thms
    1.34 -  val trans_thms	= FOL_SimpData.trans_thms
    1.35 -  val red1		= FOL_SimpData.red1
    1.36 -  val red2		= FOL_SimpData.red2
    1.37 -  val mk_rew_rules	= ZF_mk_rew_rules 
    1.38 -  val norm_thms		= FOL_SimpData.norm_thms
    1.39 -  val subst_thms	= FOL_SimpData.subst_thms
    1.40 -  val dest_red		= FOL_SimpData.dest_red
    1.41 -  end;
    1.42 -
    1.43 -structure ZF_Simp = SimpFun(ZF_SimpData);
    1.44 -
    1.45 -open ZF_Simp;
    1.46 +val ZF_simps = [empty_subsetI, ball_simp, if_true, if_false, 
    1.47 +		beta, eta, restrict, fst_conv, snd_conv, split];
    1.48  
    1.49 -(*Redeclared because the previous FOL_ss belongs to a different instance
    1.50 -  of type simpset*)
    1.51 -val FOL_ss = empty_ss addcongs FOL_congs addrews FOL_rews 
    1.52 -		      setauto auto_tac[TrueI,ballI];
    1.53 -
    1.54 -(** Basic congruence and rewrite rules for ZF set theory **)
    1.55 +(*Sigma_cong, Pi_cong NOT included by default since they cause
    1.56 +  flex-flex pairs and the "Check your prover" error -- because most
    1.57 +  Sigma's and Pi's are abbreviated as * or -> *)
    1.58 +val ZF_congs =
    1.59 +   [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
    1.60  
    1.61 -val ZF_congs = 
    1.62 -   [ball_cong,bex_cong,Replace_cong,RepFun_cong,Collect_cong,the_cong,
    1.63 -    if_cong,Sigma_cong,split_cong,Pi_cong,lam_cong] @ basic_ZF_congs;
    1.64 -
    1.65 -val ZF_rews = [empty_subsetI, ball_rew, if_true, if_false, 
    1.66 -	       beta, eta, restrict,
    1.67 -	       fst_conv, snd_conv, split];
    1.68 -
    1.69 -val ZF_ss = FOL_ss addcongs ZF_congs addrews (ZF_rews@mem_rews);
    1.70 -
    1.71 +val ZF_ss = FOL_ss 
    1.72 +      setmksimps ZF_mk_rew_rules
    1.73 +      addsimps (ZF_simps@mem_simps)
    1.74 +      addcongs ZF_congs;