author  lcp 
Tue, 21 Jun 1994 17:20:34 +0200  
changeset 435  ca5356bd315a 
parent 279  7738aed3f84d 
child 467  92868dab2939 
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 

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

22 
(*INCLUDED: should be??*) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

23 
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

24 
[ "(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

25 
"(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

26 
"(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

27 
"(EX x:succ(i).P(x)) <> P(i)  (EX x:i.P(x))" ]; 
0  28 

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

30 

31 
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 

32 
not (is_Var (head_of a)) 

33 
 is_rigid_elem _ = false; 

34 

35 
(*Try solving a:A by assumption provided a is rigid!*) 

36 
val test_assume_tac = SUBGOAL(fn (prem,i) => 

37 
if is_rigid_elem (Logic.strip_assums_concl prem) 

38 
then assume_tac i else no_tac); 

39 

40 
(*Type checking solves a:?A (a rigid, ?A maybe flexible). 

41 
match_tac is too strict; would refuse to instantiate ?A*) 

42 
fun typechk_step_tac tyrls = 

43 
FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3); 

44 

45 
fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls); 

46 

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

48 

49 
(*To instantiate variables in typing conditions; 

50 
to perform type checking faster than rewriting can 

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

52 
fun type_auto_tac tyrls hyps = SELECT_GOAL 

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

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

56 
(** New version of mk_rew_rules **) 

57 

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

59 

60 
(*Analyse a rigid formula*) 

61 
val atomize_pairs = 

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

63 
("All", [spec]), 

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

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

66 

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

68 
val atomize_mem_pairs = 

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

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

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

72 

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

74 
fun atomize th = 

75 
let fun tryrules pairs t = 

76 
case head_of t of 

77 
Const(a,_) => 

78 
(case assoc(pairs,a) of 

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

80 
 None => [th]) 

81 
 _ => [th] 

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

84 
(case P of 

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

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

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

88 
 A => tryrules atomize_pairs A) 

89 
 _ => [th] 

0  90 
end; 
91 

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

92 
val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
435  93 
beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff]; 
0  94 

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

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

96 
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

97 
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

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

99 
[ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong]; 
0  100 

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

101 
val ZF_ss = FOL_ss 
279  102 
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

103 
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

104 
addcongs ZF_congs; 