src/ZF/simpdata.ML
 author lcp Thu, 12 Jan 1995 03:03:07 +0100 changeset 855 4c8d0ece1f95 parent 762 1cf9ebcc3ff3 child 1036 0d28f4bc8a44 permissions -rw-r--r--
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps and UnInt_simps to ZF_ss. Added consI1 to ZF_typechecks.
```
(*  Title:      ZF/simpdata
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright   1991  University of Cambridge

Rewriting for ZF set theory -- based on FOL rewriting
*)

(** Tactics for type checking -- from CTT **)

fun is_rigid_elem (Const("Trueprop",_) \$ (Const("op :",_) \$ a \$ _)) =
not (is_Var (head_of a))
| is_rigid_elem _ = false;

(*Try solving a:A by assumption provided a is rigid!*)
val test_assume_tac = SUBGOAL(fn (prem,i) =>
if is_rigid_elem (Logic.strip_assums_concl prem)
then  assume_tac i  else  eq_assume_tac i);

(*Type checking solves a:?A (a rigid, ?A maybe flexible).
match_tac is too strict; would refuse to instantiate ?A*)
fun typechk_step_tac tyrls =
FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);

fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);

val ZF_typechecks =
[if_type, lam_type, SigmaI, apply_type, split_type, consI1];

(*Instantiates variables in typing conditions.
drawback: does not simplify conjunctions*)
fun type_auto_tac tyrls hyps = SELECT_GOAL
(DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));

(** New version of mk_rew_rules **)

(*Should False yield False<->True, or should it solve goals some other way?*)

(*Analyse a rigid formula*)
val atomize_pairs =
[("Ball",	[bspec]),
("All",	[spec]),
("op -->",	[mp]),
("op &",	[conjunct1,conjunct2])];

(*Analyse a:b, where b is rigid*)
val atomize_mem_pairs =
[("Collect",	[CollectD1,CollectD2]),
("op -",	[DiffD1,DiffD2]),
("op Int",	[IntD1,IntD2])];

(*Analyse a theorem to atomic rewrite rules*)
fun atomize th =
let fun tryrules pairs t =
case head_of t of
Const(a,_) =>
(case assoc(pairs,a) of
Some rls => flat (map atomize ([th] RL rls))
| None     => [th])
| _ => [th]
in case concl_of th of
Const("Trueprop",_) \$ P =>
(case P of
Const("op :",_) \$ a \$ b => tryrules atomize_mem_pairs b
| Const("True",_)         => []
| Const("False",_)        => []
| A => tryrules atomize_pairs A)
| _                       => [th]
end;

val ZF_simps =
[empty_subsetI, consI1, succI1, ball_simp, if_true, if_false,
beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, singleton_iff,
Sigma_empty1, Sigma_empty2, triv_RepFun, subset_refl];

(*Sigma_cong, Pi_cong NOT included by default since they cause
flex-flex pairs and the "Check your prover" error -- because most
Sigma's and Pi's are abbreviated as * or -> *)
val ZF_congs =
[ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];

val ZF_ss = FOL_ss
setmksimps (map mk_meta_eq o atomize o gen_all)
addsimps (ZF_simps @ mem_simps @ bquant_simps @
Collect_simps @ UnInt_simps)