1(* Title: ZF/simpdata.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1991 University of Cambridge 4 5Rewriting for ZF set theory: specialized extraction of rewrites from theorems. 6*) 7 8(*** New version of mk_rew_rules ***) 9 10(*Should False yield False<->True, or should it solve goals some other way?*) 11 12(*Analyse a theorem to atomic rewrite rules*) 13fun atomize (conn_pairs, mem_pairs) th = 14 let fun tryrules pairs t = 15 case head_of t of 16 Const(a,_) => 17 (case AList.lookup (op =) pairs a of 18 SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls) 19 | NONE => [th]) 20 | _ => [th] 21 in case Thm.concl_of th of 22 Const(\<^const_name>\<open>Trueprop\<close>,_) $ P => 23 (case P of 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>,_) => [] 27 | A => tryrules conn_pairs A) 28 | _ => [th] 29 end; 30 31(*Analyse a rigid formula*) 32val ZF_conn_pairs = 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}])]; 37 38(*Analyse a:b, where b is rigid*) 39val ZF_mem_pairs = 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}])]; 43 44val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); 45 46