author  wenzelm 
Thu, 01 Dec 2005 22:03:01 +0100  
changeset 18324  d1c4b1112e33 
parent 17876  b9c92f384109 
child 18735  f5fd06394f17 
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 

2469  6 
Rewriting for ZF set theory: specialized extraction of rewrites from theorems 
0  7 
*) 
8 

12199  9 
(*** New version of mk_rew_rules ***) 
0  10 

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

12 

1036  13 
(*Analyse a theorem to atomic rewrite rules*) 
13462  14 
fun atomize (conn_pairs, mem_pairs) th = 
1036  15 
let fun tryrules pairs t = 
1461  16 
case head_of t of 
13462  17 
Const(a,_) => 
17325  18 
(case AList.lookup (op =) pairs a of 
15570  19 
SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs)) 
1461  20 
([th] RL rls)) 
15531  21 
 NONE => [th]) 
1461  22 
 _ => [th] 
13462  23 
in case concl_of th of 
24 
Const("Trueprop",_) $ P => 

1461  25 
(case P of 
26 
Const("op :",_) $ a $ b => tryrules mem_pairs b 

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

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

29 
 A => tryrules conn_pairs A) 

1036  30 
 _ => [th] 
31 
end; 

32 

0  33 
(*Analyse a rigid formula*) 
1036  34 
val ZF_conn_pairs = 
13462  35 
[("Ball", [bspec]), 
1461  36 
("All", [spec]), 
37 
("op >", [mp]), 

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

0  39 

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

13462  41 
val ZF_mem_pairs = 
1461  42 
[("Collect", [CollectD1,CollectD2]), 
43 
("op ", [DiffD1,DiffD2]), 

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

0  45 

1036  46 
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); 
47 

15092  48 
val type_solver = 
49 
mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)); 

50 

17876  51 
change_simpset (fn ss => 
52 
ss setmksimps (map mk_eq o ZF_atomize o gen_all) 

12209
09bc6f8456b9
type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents:
12199
diff
changeset

53 
addcongs [if_weak_cong] 
17876  54 
setSolver type_solver); 
12209
09bc6f8456b9
type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents:
12199
diff
changeset

55 

13462  56 
local 
11233  57 

18324  58 
val unfold_bex_tac = unfold_tac [Bex_def]; 
59 
fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; 

11233  60 
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; 
61 

18324  62 
val unfold_ball_tac = unfold_tac [Ball_def]; 
63 
fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; 

11233  64 
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; 
65 

66 
in 

67 

17002  68 
val defBEX_regroup = Simplifier.simproc (the_context ()) 
13462  69 
"defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex; 
70 

17002  71 
val defBALL_regroup = Simplifier.simproc (the_context ()) 
13462  72 
"defined BALL" ["ALL x:A. P(x) > Q(x)"] rearrange_ball; 
11233  73 

74 
end; 

75 

13462  76 
Addsimprocs [defBALL_regroup, defBEX_regroup]; 
77 

12199  78 

4091  79 
val ZF_ss = simpset(); 