src/ZF/simpdata.ML
 author paulson Wed Apr 02 15:37:35 1997 +0200 (1997-04-02 ago) changeset 2876 02c12d4c8b97 parent 2496 40efb87985b5 child 3425 fc4ca570d185 permissions -rw-r--r--
Uses ZF.thy again, to make that theory usable
 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@2469 ` 11` ```(*For proving rewrite rules*) ``` paulson@2469 ` 12` ```fun prove_fun s = ``` paulson@2876 ` 13` ``` (writeln s; prove_goal ZF.thy s ``` paulson@2496 ` 14` ``` (fn prems => [ (cut_facts_tac prems 1), (Fast_tac 1) ])); ``` clasohm@0 ` 15` paulson@2469 ` 16` ```(*Are all these really suitable?*) ``` paulson@2482 ` 17` ```val ball_simps = map prove_fun ``` paulson@2482 ` 18` ``` ["(ALL x:0.P(x)) <-> True", ``` paulson@2482 ` 19` ``` "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))", ``` paulson@2482 ` 20` ``` "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))", ``` paulson@2482 ` 21` ``` "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))", ``` paulson@2482 ` 22` ``` "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))", ``` paulson@2482 ` 23` ``` "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"]; ``` paulson@2482 ` 24` paulson@2482 ` 25` ```val bex_simps = map prove_fun ``` paulson@2482 ` 26` ``` ["(EX x:0.P(x)) <-> False", ``` paulson@2482 ` 27` ``` "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))", ``` paulson@2482 ` 28` ``` "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B.P(x))", ``` paulson@2482 ` 29` ``` "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))", ``` paulson@2482 ` 30` ``` "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))", ``` paulson@2482 ` 31` ``` "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"]; ``` paulson@2482 ` 32` paulson@2482 ` 33` ```Addsimps (ball_simps @ bex_simps); ``` clasohm@0 ` 34` paulson@2469 ` 35` ```Addsimps (map prove_fun ``` paulson@2469 ` 36` ``` ["{x:0. P(x)} = 0", ``` paulson@2469 ` 37` ``` "{x:A. False} = 0", ``` paulson@2469 ` 38` ``` "{x:A. True} = A", ``` paulson@2469 ` 39` ``` "RepFun(0,f) = 0", ``` paulson@2469 ` 40` ``` "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))", ``` paulson@2469 ` 41` ``` "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]); ``` clasohm@0 ` 42` paulson@2469 ` 43` ```Addsimps (map prove_fun ``` paulson@2469 ` 44` ``` ["0 Un A = A", "A Un 0 = A", ``` paulson@2469 ` 45` ``` "0 Int A = 0", "A Int 0 = 0", ``` paulson@2469 ` 46` ``` "0-A = 0", "A-0 = A", ``` paulson@2469 ` 47` ``` "Union(0) = 0", ``` paulson@2469 ` 48` ``` "Union(cons(b,A)) = b Un Union(A)", ``` paulson@2469 ` 49` ``` "Inter({b}) = b"]); ``` clasohm@0 ` 50` clasohm@0 ` 51` ```(** New version of mk_rew_rules **) ``` clasohm@0 ` 52` clasohm@0 ` 53` ```(*Should False yield False<->True, or should it solve goals some other way?*) ``` clasohm@0 ` 54` lcp@1036 ` 55` ```(*Analyse a theorem to atomic rewrite rules*) ``` lcp@1036 ` 56` ```fun atomize (conn_pairs, mem_pairs) th = ``` lcp@1036 ` 57` ``` let fun tryrules pairs t = ``` clasohm@1461 ` 58` ``` case head_of t of ``` clasohm@1461 ` 59` ``` Const(a,_) => ``` clasohm@1461 ` 60` ``` (case assoc(pairs,a) of ``` clasohm@1461 ` 61` ``` Some rls => flat (map (atomize (conn_pairs, mem_pairs)) ``` clasohm@1461 ` 62` ``` ([th] RL rls)) ``` clasohm@1461 ` 63` ``` | None => [th]) ``` clasohm@1461 ` 64` ``` | _ => [th] ``` lcp@1036 ` 65` ``` in case concl_of th of ``` clasohm@1461 ` 66` ``` Const("Trueprop",_) \$ P => ``` clasohm@1461 ` 67` ``` (case P of ``` clasohm@1461 ` 68` ``` Const("op :",_) \$ a \$ b => tryrules mem_pairs b ``` clasohm@1461 ` 69` ``` | Const("True",_) => [] ``` clasohm@1461 ` 70` ``` | Const("False",_) => [] ``` clasohm@1461 ` 71` ``` | A => tryrules conn_pairs A) ``` lcp@1036 ` 72` ``` | _ => [th] ``` lcp@1036 ` 73` ``` end; ``` lcp@1036 ` 74` clasohm@0 ` 75` ```(*Analyse a rigid formula*) ``` lcp@1036 ` 76` ```val ZF_conn_pairs = ``` clasohm@1461 ` 77` ``` [("Ball", [bspec]), ``` clasohm@1461 ` 78` ``` ("All", [spec]), ``` clasohm@1461 ` 79` ``` ("op -->", [mp]), ``` clasohm@1461 ` 80` ``` ("op &", [conjunct1,conjunct2])]; ``` clasohm@0 ` 81` clasohm@0 ` 82` ```(*Analyse a:b, where b is rigid*) ``` lcp@1036 ` 83` ```val ZF_mem_pairs = ``` clasohm@1461 ` 84` ``` [("Collect", [CollectD1,CollectD2]), ``` clasohm@1461 ` 85` ``` ("op -", [DiffD1,DiffD2]), ``` clasohm@1461 ` 86` ``` ("op Int", [IntD1,IntD2])]; ``` clasohm@0 ` 87` lcp@1036 ` 88` ```val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); ``` lcp@1036 ` 89` paulson@2469 ` 90` ```simpset := !simpset setmksimps (map mk_meta_eq o ZF_atomize o gen_all); ``` paulson@2469 ` 91` paulson@2469 ` 92` ```val ZF_ss = !simpset; ```