author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1612  f9f0145e1c7e 
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 
(** Tactics for type checking  from CTT **) 

10 

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

12 
not (is_Var (head_of a)) 

13 
 is_rigid_elem _ = false; 

14 

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

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

17 
if is_rigid_elem (Logic.strip_assums_concl prem) 

762
1cf9ebcc3ff3
test_assume_tac: now tries eq_assume_tac on exceptional cases
lcp
parents:
533
diff
changeset

18 
then assume_tac i else eq_assume_tac i); 
0  19 

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

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

22 
fun typechk_step_tac tyrls = 

23 
FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3); 

24 

25 
fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls); 

26 

855
4c8d0ece1f95
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents:
762
diff
changeset

27 
val ZF_typechecks = 
4c8d0ece1f95
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents:
762
diff
changeset

28 
[if_type, lam_type, SigmaI, apply_type, split_type, consI1]; 
0  29 

516  30 
(*Instantiates variables in typing conditions. 
31 
drawback: does not simplify conjunctions*) 

0  32 
fun type_auto_tac tyrls hyps = SELECT_GOAL 
33 
(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

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

36 
(** New version of mk_rew_rules **) 

37 

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

39 

1036  40 
(*Analyse a theorem to atomic rewrite rules*) 
41 
fun atomize (conn_pairs, mem_pairs) th = 

42 
let fun tryrules pairs t = 

1461  43 
case head_of t of 
44 
Const(a,_) => 

45 
(case assoc(pairs,a) of 

46 
Some rls => flat (map (atomize (conn_pairs, mem_pairs)) 

47 
([th] RL rls)) 

48 
 None => [th]) 

49 
 _ => [th] 

1036  50 
in case concl_of th of 
1461  51 
Const("Trueprop",_) $ P => 
52 
(case P of 

53 
Const("op :",_) $ a $ b => tryrules mem_pairs b 

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

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

56 
 A => tryrules conn_pairs A) 

1036  57 
 _ => [th] 
58 
end; 

59 

0  60 
(*Analyse a rigid formula*) 
1036  61 
val ZF_conn_pairs = 
1461  62 
[("Ball", [bspec]), 
63 
("All", [spec]), 

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

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

0  66 

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

1036  68 
val ZF_mem_pairs = 
1461  69 
[("Collect", [CollectD1,CollectD2]), 
70 
("op ", [DiffD1,DiffD2]), 

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

0  72 

855
4c8d0ece1f95
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents:
762
diff
changeset

73 
val ZF_simps = 
4c8d0ece1f95
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents:
762
diff
changeset

74 
[empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
4c8d0ece1f95
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents:
762
diff
changeset

75 
beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, singleton_iff, 
4c8d0ece1f95
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents:
762
diff
changeset

76 
Sigma_empty1, Sigma_empty2, triv_RepFun, subset_refl]; 
0  77 

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

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

79 
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

80 
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

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

82 
[ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong]; 
0  83 

1036  84 
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); 
85 

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

86 
val ZF_ss = FOL_ss 
1036  87 
setmksimps (map mk_meta_eq o ZF_atomize o gen_all) 
855
4c8d0ece1f95
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents:
762
diff
changeset

88 
addsimps (ZF_simps @ mem_simps @ bquant_simps @ 
1461  89 
Collect_simps @ UnInt_simps) 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

90 
addcongs ZF_congs; 