author | lcp |
Mon, 15 Aug 1994 18:15:09 +0200 | |
changeset 524 | b1bf18e83302 |
parent 516 | 1957113f0d7d |
child 533 | 7357160bc56a |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: ZF/simpdata |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1991 University of Cambridge |
|
5 |
||
6 |
Rewriting for ZF set theory -- based on FOL rewriting |
|
7 |
*) |
|
8 |
||
9 |
fun prove_fun s = |
|
10 |
(writeln s; prove_goal ZF.thy s |
|
11 |
(fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ])); |
|
12 |
||
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
13 |
(*INCLUDED IN ZF_ss*) |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
14 |
val mem_simps = map prove_fun |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
15 |
[ "a : 0 <-> False", |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
16 |
"a : A Un B <-> a:A | a:B", |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
17 |
"a : A Int B <-> a:A & a:B", |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
18 |
"a : A-B <-> a:A & ~a:B", |
0 | 19 |
"<a,b>: Sigma(A,B) <-> a:A & b:B(a)", |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
20 |
"a : Collect(A,P) <-> a:A & P(a)" ]; |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
21 |
|
467 | 22 |
goal ZF.thy "{x.x:A} = A"; |
23 |
by (fast_tac eq_cs 1); |
|
24 |
val triv_RepFun = result(); |
|
25 |
||
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
26 |
(*INCLUDED: should be??*) |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
27 |
val bquant_simps = map prove_fun |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
28 |
[ "(ALL x:0.P(x)) <-> True", |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
29 |
"(EX x:0.P(x)) <-> False", |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
30 |
"(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))", |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
31 |
"(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))" ]; |
0 | 32 |
|
33 |
(** Tactics for type checking -- from CTT **) |
|
34 |
||
35 |
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = |
|
36 |
not (is_Var (head_of a)) |
|
37 |
| is_rigid_elem _ = false; |
|
38 |
||
39 |
(*Try solving a:A by assumption provided a is rigid!*) |
|
40 |
val test_assume_tac = SUBGOAL(fn (prem,i) => |
|
41 |
if is_rigid_elem (Logic.strip_assums_concl prem) |
|
42 |
then assume_tac i else no_tac); |
|
43 |
||
44 |
(*Type checking solves a:?A (a rigid, ?A maybe flexible). |
|
45 |
match_tac is too strict; would refuse to instantiate ?A*) |
|
46 |
fun typechk_step_tac tyrls = |
|
47 |
FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3); |
|
48 |
||
49 |
fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls); |
|
50 |
||
51 |
val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type]; |
|
52 |
||
516 | 53 |
(*Instantiates variables in typing conditions. |
54 |
drawback: does not simplify conjunctions*) |
|
0 | 55 |
fun type_auto_tac tyrls hyps = SELECT_GOAL |
56 |
(DEPTH_SOLVE (typechk_step_tac (tyrls@hyps) |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
57 |
ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1)); |
0 | 58 |
|
59 |
(** New version of mk_rew_rules **) |
|
60 |
||
61 |
(*Should False yield False<->True, or should it solve goals some other way?*) |
|
62 |
||
63 |
(*Analyse a rigid formula*) |
|
64 |
val atomize_pairs = |
|
65 |
[("Ball", [bspec]), |
|
66 |
("All", [spec]), |
|
67 |
("op -->", [mp]), |
|
68 |
("op &", [conjunct1,conjunct2])]; |
|
69 |
||
70 |
(*Analyse a:b, where b is rigid*) |
|
71 |
val atomize_mem_pairs = |
|
72 |
[("Collect", [CollectD1,CollectD2]), |
|
73 |
("op -", [DiffD1,DiffD2]), |
|
74 |
("op Int", [IntD1,IntD2])]; |
|
75 |
||
76 |
(*Analyse a theorem to atomic rewrite rules*) |
|
77 |
fun atomize th = |
|
78 |
let fun tryrules pairs t = |
|
79 |
case head_of t of |
|
80 |
Const(a,_) => |
|
81 |
(case assoc(pairs,a) of |
|
82 |
Some rls => flat (map atomize ([th] RL rls)) |
|
83 |
| None => [th]) |
|
84 |
| _ => [th] |
|
435 | 85 |
in case concl_of th of |
86 |
Const("Trueprop",_) $ P => |
|
87 |
(case P of |
|
88 |
Const("op :",_) $ a $ b => tryrules atomize_mem_pairs b |
|
89 |
| Const("True",_) => [] |
|
90 |
| Const("False",_) => [] |
|
91 |
| A => tryrules atomize_pairs A) |
|
92 |
| _ => [th] |
|
0 | 93 |
end; |
94 |
||
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
95 |
val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, |
467 | 96 |
beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, |
485 | 97 |
triv_RepFun, subset_refl]; |
0 | 98 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
99 |
(*Sigma_cong, Pi_cong NOT included by default since they cause |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
100 |
flex-flex pairs and the "Check your prover" error -- because most |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
101 |
Sigma's and Pi's are abbreviated as * or -> *) |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
102 |
val ZF_congs = |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
103 |
[ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong]; |
0 | 104 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
105 |
val ZF_ss = FOL_ss |
279 | 106 |
setmksimps (map mk_meta_eq o atomize o gen_all) |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
107 |
addsimps (ZF_simps @ mem_simps @ bquant_simps) |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
108 |
addcongs ZF_congs; |