src/ZF/simpdata.ML
 author wenzelm Thu Sep 07 21:12:49 2000 +0200 (2000-09-07 ago) changeset 9907 473a6604da94 parent 9570 e16e168984e1 child 11233 34c81a796ee3 permissions -rw-r--r--
tuned ML code (the_context, bind_thms(s));
 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@9570 ` 13` ``` fun prover s = (prove_goal (the_context ()) 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@5202 ` 48` ``` ["{x. y:0, R(x,y)} = 0", (*Replace*) ``` paulson@5202 ` 49` ``` "{x:0. P(x)} = 0", (*Collect*) ``` paulson@3425 ` 50` ``` "{x:A. False} = 0", ``` paulson@3425 ` 51` ``` "{x:A. True} = A", ``` paulson@5202 ` 52` ``` "RepFun(0,f) = 0", (*RepFun*) ``` paulson@3425 ` 53` ``` "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))", ``` paulson@3425 ` 54` ``` "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"] ``` clasohm@0 ` 55` paulson@3425 ` 56` ```val misc_simps = map prover ``` paulson@3425 ` 57` ``` ["0 Un A = A", "A Un 0 = A", ``` paulson@3425 ` 58` ``` "0 Int A = 0", "A Int 0 = 0", ``` paulson@3425 ` 59` ``` "0-A = 0", "A-0 = A", ``` paulson@3425 ` 60` ``` "Union(0) = 0", ``` paulson@3425 ` 61` ``` "Union(cons(b,A)) = b Un Union(A)", ``` paulson@3425 ` 62` ``` "Inter({b}) = b"] ``` clasohm@0 ` 63` paulson@3425 ` 64` ```end; ``` paulson@3425 ` 65` wenzelm@9907 ` 66` ```bind_thms ("ball_simps", ball_simps); ``` wenzelm@9907 ` 67` ```bind_thm ("ball_conj_distrib", ball_conj_distrib); ``` wenzelm@9907 ` 68` ```bind_thms ("bex_simps", bex_simps); ``` wenzelm@9907 ` 69` ```bind_thm ("bex_disj_distrib", bex_disj_distrib); ``` wenzelm@9907 ` 70` ```bind_thms ("Rep_simps", Rep_simps); ``` wenzelm@9907 ` 71` ```bind_thms ("misc_simps", misc_simps); ``` wenzelm@9907 ` 72` paulson@3425 ` 73` ```Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps); ``` paulson@3425 ` 74` clasohm@0 ` 75` clasohm@0 ` 76` ```(** New version of mk_rew_rules **) ``` clasohm@0 ` 77` clasohm@0 ` 78` ```(*Should False yield False<->True, or should it solve goals some other way?*) ``` clasohm@0 ` 79` lcp@1036 ` 80` ```(*Analyse a theorem to atomic rewrite rules*) ``` lcp@1036 ` 81` ```fun atomize (conn_pairs, mem_pairs) th = ``` lcp@1036 ` 82` ``` let fun tryrules pairs t = ``` clasohm@1461 ` 83` ``` case head_of t of ``` clasohm@1461 ` 84` ``` Const(a,_) => ``` clasohm@1461 ` 85` ``` (case assoc(pairs,a) of ``` clasohm@1461 ` 86` ``` Some rls => flat (map (atomize (conn_pairs, mem_pairs)) ``` clasohm@1461 ` 87` ``` ([th] RL rls)) ``` clasohm@1461 ` 88` ``` | None => [th]) ``` clasohm@1461 ` 89` ``` | _ => [th] ``` lcp@1036 ` 90` ``` in case concl_of th of ``` clasohm@1461 ` 91` ``` Const("Trueprop",_) \$ P => ``` clasohm@1461 ` 92` ``` (case P of ``` clasohm@1461 ` 93` ``` Const("op :",_) \$ a \$ b => tryrules mem_pairs b ``` clasohm@1461 ` 94` ``` | Const("True",_) => [] ``` clasohm@1461 ` 95` ``` | Const("False",_) => [] ``` clasohm@1461 ` 96` ``` | A => tryrules conn_pairs A) ``` lcp@1036 ` 97` ``` | _ => [th] ``` lcp@1036 ` 98` ``` end; ``` lcp@1036 ` 99` clasohm@0 ` 100` ```(*Analyse a rigid formula*) ``` lcp@1036 ` 101` ```val ZF_conn_pairs = ``` clasohm@1461 ` 102` ``` [("Ball", [bspec]), ``` clasohm@1461 ` 103` ``` ("All", [spec]), ``` clasohm@1461 ` 104` ``` ("op -->", [mp]), ``` clasohm@1461 ` 105` ``` ("op &", [conjunct1,conjunct2])]; ``` clasohm@0 ` 106` clasohm@0 ` 107` ```(*Analyse a:b, where b is rigid*) ``` lcp@1036 ` 108` ```val ZF_mem_pairs = ``` clasohm@1461 ` 109` ``` [("Collect", [CollectD1,CollectD2]), ``` clasohm@1461 ` 110` ``` ("op -", [DiffD1,DiffD2]), ``` clasohm@1461 ` 111` ``` ("op Int", [IntD1,IntD2])]; ``` clasohm@0 ` 112` lcp@1036 ` 113` ```val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); ``` lcp@1036 ` 114` oheimb@5553 ` 115` ```simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all) ``` paulson@9570 ` 116` ``` addcongs [if_weak_cong] ``` paulson@9570 ` 117` ``` addsplits [split_if] ``` nipkow@7570 ` 118` ``` setSolver (mk_solver "types" Type_solver_tac); ``` paulson@2469 ` 119` wenzelm@4091 ` 120` ```val ZF_ss = simpset(); ```