src/ZF/simpdata.ML
 author paulson Mon Jul 13 16:43:57 1998 +0200 (1998-07-13 ago) changeset 5137 60205b0de9b9 parent 4091 771b1f6422a8 child 5202 084ceb3844f5 permissions -rw-r--r--
Huge tidy-up: removal of leading \!\!
 clasohm@0 ` 1` ```(* Title: ZF/simpdata ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1991 University of Cambridge ``` clasohm@0 ` 5` paulson@2469 ` 6` ```Rewriting for ZF set theory: specialized extraction of rewrites from theorems ``` clasohm@0 ` 7` ```*) ``` clasohm@0 ` 8` paulson@2469 ` 9` ```(** Rewriting **) ``` clasohm@0 ` 10` paulson@3425 ` 11` ```local ``` paulson@3425 ` 12` ``` (*For proving rewrite rules*) ``` paulson@3425 ` 13` ``` fun prover s = (prove_goal ZF.thy s (fn _ => [Blast_tac 1])); ``` paulson@3425 ` 14` paulson@3425 ` 15` ```in ``` clasohm@0 ` 16` paulson@3425 ` 17` ```val ball_simps = map prover ``` paulson@3425 ` 18` ``` ["(ALL x:A. P(x) | Q) <-> ((ALL x:A. P(x)) | Q)", ``` paulson@3425 ` 19` ``` "(ALL x:A. P | Q(x)) <-> (P | (ALL x:A. Q(x)))", ``` paulson@3425 ` 20` ``` "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))", ``` paulson@3425 ` 21` ``` "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)", ``` paulson@3425 ` 22` ``` "(ALL x:0.P(x)) <-> True", ``` wenzelm@3840 ` 23` ``` "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))", ``` wenzelm@3840 ` 24` ``` "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))", ``` paulson@2482 ` 25` ``` "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))", ``` paulson@2482 ` 26` ``` "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))", ``` nipkow@3859 ` 27` ``` "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))", ``` nipkow@3859 ` 28` ``` "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"]; ``` paulson@2482 ` 29` paulson@3425 ` 30` ```val ball_conj_distrib = ``` paulson@3425 ` 31` ``` prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"; ``` paulson@3425 ` 32` paulson@3425 ` 33` ```val bex_simps = map prover ``` paulson@3425 ` 34` ``` ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)", ``` paulson@3425 ` 35` ``` "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))", ``` paulson@3425 ` 36` ``` "(EX x:0.P(x)) <-> False", ``` wenzelm@3840 ` 37` ``` "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))", ``` wenzelm@3840 ` 38` ``` "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))", ``` paulson@2482 ` 39` ``` "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))", ``` paulson@2482 ` 40` ``` "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))", ``` nipkow@3859 ` 41` ``` "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))", ``` nipkow@3859 ` 42` ``` "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"]; ``` paulson@2482 ` 43` paulson@3425 ` 44` ```val bex_disj_distrib = ``` paulson@3425 ` 45` ``` prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))"; ``` paulson@3425 ` 46` paulson@3425 ` 47` ```val Rep_simps = map prover ``` paulson@3425 ` 48` ``` ["{x:0. P(x)} = 0", ``` paulson@3425 ` 49` ``` "{x:A. False} = 0", ``` paulson@3425 ` 50` ``` "{x:A. True} = A", ``` paulson@3425 ` 51` ``` "RepFun(0,f) = 0", ``` paulson@3425 ` 52` ``` "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))", ``` paulson@3425 ` 53` ``` "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"] ``` clasohm@0 ` 54` paulson@3425 ` 55` ```val misc_simps = map prover ``` paulson@3425 ` 56` ``` ["0 Un A = A", "A Un 0 = A", ``` paulson@3425 ` 57` ``` "0 Int A = 0", "A Int 0 = 0", ``` paulson@3425 ` 58` ``` "0-A = 0", "A-0 = A", ``` paulson@3425 ` 59` ``` "Union(0) = 0", ``` paulson@3425 ` 60` ``` "Union(cons(b,A)) = b Un Union(A)", ``` paulson@3425 ` 61` ``` "Inter({b}) = b"] ``` clasohm@0 ` 62` paulson@3425 ` 63` ```end; ``` paulson@3425 ` 64` paulson@3425 ` 65` ```Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps); ``` paulson@3425 ` 66` clasohm@0 ` 67` clasohm@0 ` 68` ```(** New version of mk_rew_rules **) ``` clasohm@0 ` 69` clasohm@0 ` 70` ```(*Should False yield False<->True, or should it solve goals some other way?*) ``` clasohm@0 ` 71` lcp@1036 ` 72` ```(*Analyse a theorem to atomic rewrite rules*) ``` lcp@1036 ` 73` ```fun atomize (conn_pairs, mem_pairs) th = ``` lcp@1036 ` 74` ``` let fun tryrules pairs t = ``` clasohm@1461 ` 75` ``` case head_of t of ``` clasohm@1461 ` 76` ``` Const(a,_) => ``` clasohm@1461 ` 77` ``` (case assoc(pairs,a) of ``` clasohm@1461 ` 78` ``` Some rls => flat (map (atomize (conn_pairs, mem_pairs)) ``` clasohm@1461 ` 79` ``` ([th] RL rls)) ``` clasohm@1461 ` 80` ``` | None => [th]) ``` clasohm@1461 ` 81` ``` | _ => [th] ``` lcp@1036 ` 82` ``` in case concl_of th of ``` clasohm@1461 ` 83` ``` Const("Trueprop",_) \$ P => ``` clasohm@1461 ` 84` ``` (case P of ``` clasohm@1461 ` 85` ``` Const("op :",_) \$ a \$ b => tryrules mem_pairs b ``` clasohm@1461 ` 86` ``` | Const("True",_) => [] ``` clasohm@1461 ` 87` ``` | Const("False",_) => [] ``` clasohm@1461 ` 88` ``` | A => tryrules conn_pairs A) ``` lcp@1036 ` 89` ``` | _ => [th] ``` lcp@1036 ` 90` ``` end; ``` lcp@1036 ` 91` clasohm@0 ` 92` ```(*Analyse a rigid formula*) ``` lcp@1036 ` 93` ```val ZF_conn_pairs = ``` clasohm@1461 ` 94` ``` [("Ball", [bspec]), ``` clasohm@1461 ` 95` ``` ("All", [spec]), ``` clasohm@1461 ` 96` ``` ("op -->", [mp]), ``` clasohm@1461 ` 97` ``` ("op &", [conjunct1,conjunct2])]; ``` clasohm@0 ` 98` clasohm@0 ` 99` ```(*Analyse a:b, where b is rigid*) ``` lcp@1036 ` 100` ```val ZF_mem_pairs = ``` clasohm@1461 ` 101` ``` [("Collect", [CollectD1,CollectD2]), ``` clasohm@1461 ` 102` ``` ("op -", [DiffD1,DiffD2]), ``` clasohm@1461 ` 103` ``` ("op Int", [IntD1,IntD2])]; ``` clasohm@0 ` 104` lcp@1036 ` 105` ```val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); ``` lcp@1036 ` 106` paulson@5137 ` 107` ```simpset_ref() := simpset() setmksimps (map mk_meta_eq o ZF_atomize o gen_all) ``` paulson@5137 ` 108` ``` addsplits [split_if]; ``` paulson@2469 ` 109` wenzelm@4091 ` 110` ```val ZF_ss = simpset(); ```