35762

1 
(* Title: ZF/simpdata.ML

0

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1991 University of Cambridge


4 

35762

5 
Rewriting for ZF set theory: specialized extraction of rewrites from theorems.

0

6 
*)


7 

12199

8 
(*** New version of mk_rew_rules ***)

0

9 


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


11 

1036

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

13462

13 
fun atomize (conn_pairs, mem_pairs) th =

1036

14 
let fun tryrules pairs t =

1461

15 
case head_of t of

13462

16 
Const(a,_) =>

17325

17 
(case AList.lookup (op =) pairs a of

32952

18 
SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls)


19 
 NONE => [th])

1461

20 
 _ => [th]

59582

21 
in case Thm.concl_of th of

69593

22 
Const(\<^const_name>\<open>Trueprop\<close>,_) $ P =>

1461

23 
(case P of

69593

24 
Const(\<^const_name>\<open>mem\<close>,_) $ a $ b => tryrules mem_pairs b


25 
 Const(\<^const_name>\<open>True\<close>,_) => []


26 
 Const(\<^const_name>\<open>False\<close>,_) => []

1461

27 
 A => tryrules conn_pairs A)

1036

28 
 _ => [th]


29 
end;


30 

0

31 
(*Analyse a rigid formula*)

1036

32 
val ZF_conn_pairs =

69593

33 
[(\<^const_name>\<open>Ball\<close>, [@{thm bspec}]),


34 
(\<^const_name>\<open>All\<close>, [@{thm spec}]),


35 
(\<^const_name>\<open>imp\<close>, [@{thm mp}]),


36 
(\<^const_name>\<open>conj\<close>, [@{thm conjunct1}, @{thm conjunct2}])];

0

37 


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

13462

39 
val ZF_mem_pairs =

69593

40 
[(\<^const_name>\<open>Collect\<close>, [@{thm CollectD1}, @{thm CollectD2}]),


41 
(\<^const_name>\<open>Diff\<close>, [@{thm DiffD1}, @{thm DiffD2}]),


42 
(\<^const_name>\<open>Int\<close>, [@{thm IntD1}, @{thm IntD2}])];

0

43 

1036

44 
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);


45 
