author  lcp 
Tue, 26 Jul 1994 13:44:42 +0200  
changeset 485  5e00a676a211 
parent 467  92868dab2939 
child 516  1957113f0d7d 
permissions  rwrr 
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 : AB <> 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 

53 
(*To instantiate variables in typing conditions; 

54 
to perform type checking faster than rewriting can 

55 
NOT TERRIBLY USEFUL because it does not simplify conjunctions*) 

56 
fun type_auto_tac tyrls hyps = SELECT_GOAL 

57 
(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

58 
ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1)); 
0  59 

60 
(** New version of mk_rew_rules **) 

61 

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

63 

64 
(*Analyse a rigid formula*) 

65 
val atomize_pairs = 

66 
[("Ball", [bspec]), 

67 
("All", [spec]), 

68 
("op >", [mp]), 

69 
("op &", [conjunct1,conjunct2])]; 

70 

71 
(*Analyse a:b, where b is rigid*) 

72 
val atomize_mem_pairs = 

73 
[("Collect", [CollectD1,CollectD2]), 

74 
("op ", [DiffD1,DiffD2]), 

75 
("op Int", [IntD1,IntD2])]; 

76 

77 
(*Analyse a theorem to atomic rewrite rules*) 

78 
fun atomize th = 

79 
let fun tryrules pairs t = 

80 
case head_of t of 

81 
Const(a,_) => 

82 
(case assoc(pairs,a) of 

83 
Some rls => flat (map atomize ([th] RL rls)) 

84 
 None => [th]) 

85 
 _ => [th] 

435  86 
in case concl_of th of 
87 
Const("Trueprop",_) $ P => 

88 
(case P of 

89 
Const("op :",_) $ a $ b => tryrules atomize_mem_pairs b 

90 
 Const("True",_) => [] 

91 
 Const("False",_) => [] 

92 
 A => tryrules atomize_pairs A) 

93 
 _ => [th] 

0  94 
end; 
95 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

96 
val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
467  97 
beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, 
485  98 
triv_RepFun, subset_refl]; 
0  99 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

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

101 
flexflex 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

102 
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

103 
val ZF_congs = 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

104 
[ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong]; 
0  105 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

106 
val ZF_ss = FOL_ss 
279  107 
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

108 
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

109 
addcongs ZF_congs; 