src/ZF/simpdata.ML
 author lcp Fri, 17 Sep 1993 16:16:38 +0200 changeset 6 8ce8c4d13d4d parent 0 a5a9c433f639 child 14 1c0926788772 permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
```
(*  Title:      ZF/simpdata
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

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

fun prove_fun s =
(writeln s;  prove_goal ZF.thy s
(fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));

val mem_simps = map prove_fun
[ "a:0 <-> False",
"a : A Un B <-> a:A | a:B",
"a : A Int B <-> a:A & a:B",
"a : A-B <-> a:A & ~a:B",
"a : cons(b,B) <-> a=b | a:B",
"i : succ(j) <-> i=j | i:j",
"<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
"a : Collect(A,P) <-> a:A & P(a)" ];

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

fun is_rigid_elem (Const("Trueprop",_) \$ (Const("op :",_) \$ 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  no_tac);

(*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];

(*To instantiate variables in typing conditions;
to perform type checking faster than rewriting can
NOT TERRIBLY USEFUL because it 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 =
Const(a,_) =>
(case assoc(pairs,a) of
Some rls => flat (map atomize ([th] RL rls))
| None     => [th])
| _ => [th]
in case concl_of th of (*The operator below is Trueprop*)
_ \$ (Const("op :",_) \$ a \$ b) => tryrules atomize_mem_pairs b
| _ \$ (Const("True",_)) => []	(*True is DELETED*)
| _ \$ (Const("False",_)) => []	(*should False do something??*)
| _ \$ A => tryrules atomize_pairs A
end;

fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);

val ZF_simps = [empty_subsetI, ball_simp, if_true, if_false,
beta, eta, restrict, fst_conv, snd_conv, split];

(*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 ZF_mk_rew_rules