src/ZF/simpdata.ML
 author wenzelm Thu Nov 15 18:21:38 2001 +0100 (2001-11-15) changeset 12209 09bc6f8456b9 parent 12199 8213fd95acb5 child 12484 7ad150f5fc10 permissions -rw-r--r--
type_solver_tac: use TCSET' to refer to context of goal state (does
*not* work with local proof contexts of Isar / new-style locales);
 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@12199 ` 9` ```(*** New version of mk_rew_rules ***) ``` clasohm@0 ` 10` clasohm@0 ` 11` ```(*Should False yield False<->True, or should it solve goals some other way?*) ``` clasohm@0 ` 12` lcp@1036 ` 13` ```(*Analyse a theorem to atomic rewrite rules*) ``` lcp@1036 ` 14` ```fun atomize (conn_pairs, mem_pairs) th = ``` lcp@1036 ` 15` ``` let fun tryrules pairs t = ``` clasohm@1461 ` 16` ``` case head_of t of ``` clasohm@1461 ` 17` ``` Const(a,_) => ``` clasohm@1461 ` 18` ``` (case assoc(pairs,a) of ``` clasohm@1461 ` 19` ``` Some rls => flat (map (atomize (conn_pairs, mem_pairs)) ``` clasohm@1461 ` 20` ``` ([th] RL rls)) ``` clasohm@1461 ` 21` ``` | None => [th]) ``` clasohm@1461 ` 22` ``` | _ => [th] ``` lcp@1036 ` 23` ``` in case concl_of th of ``` clasohm@1461 ` 24` ``` Const("Trueprop",_) \$ P => ``` clasohm@1461 ` 25` ``` (case P of ``` clasohm@1461 ` 26` ``` Const("op :",_) \$ a \$ b => tryrules mem_pairs b ``` clasohm@1461 ` 27` ``` | Const("True",_) => [] ``` clasohm@1461 ` 28` ``` | Const("False",_) => [] ``` clasohm@1461 ` 29` ``` | A => tryrules conn_pairs A) ``` lcp@1036 ` 30` ``` | _ => [th] ``` lcp@1036 ` 31` ``` end; ``` lcp@1036 ` 32` clasohm@0 ` 33` ```(*Analyse a rigid formula*) ``` lcp@1036 ` 34` ```val ZF_conn_pairs = ``` clasohm@1461 ` 35` ``` [("Ball", [bspec]), ``` clasohm@1461 ` 36` ``` ("All", [spec]), ``` clasohm@1461 ` 37` ``` ("op -->", [mp]), ``` clasohm@1461 ` 38` ``` ("op &", [conjunct1,conjunct2])]; ``` clasohm@0 ` 39` clasohm@0 ` 40` ```(*Analyse a:b, where b is rigid*) ``` lcp@1036 ` 41` ```val ZF_mem_pairs = ``` clasohm@1461 ` 42` ``` [("Collect", [CollectD1,CollectD2]), ``` clasohm@1461 ` 43` ``` ("op -", [DiffD1,DiffD2]), ``` clasohm@1461 ` 44` ``` ("op Int", [IntD1,IntD2])]; ``` clasohm@0 ` 45` lcp@1036 ` 46` ```val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); ``` lcp@1036 ` 47` wenzelm@12209 ` 48` ```simpset_ref() := ``` wenzelm@12209 ` 49` ``` simpset() setmksimps (map mk_eq o ZF_atomize o gen_all) ``` wenzelm@12209 ` 50` ``` addcongs [if_weak_cong] ``` wenzelm@12209 ` 51` ``` addsplits [split_if] ``` wenzelm@12209 ` 52` ``` setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems))); ``` wenzelm@12209 ` 53` paulson@2469 ` 54` paulson@11323 ` 55` ```(** Splitting IFs in the assumptions **) ``` paulson@11323 ` 56` paulson@11323 ` 57` ```Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))"; ``` paulson@11323 ` 58` ```by (Simp_tac 1); ``` paulson@11323 ` 59` ```qed "split_if_asm"; ``` paulson@11323 ` 60` paulson@11323 ` 61` ```bind_thms ("if_splits", [split_if, split_if_asm]); ``` paulson@11323 ` 62` paulson@12199 ` 63` paulson@12199 ` 64` ```(*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***) ``` paulson@12199 ` 65` paulson@12199 ` 66` ```local ``` paulson@12199 ` 67` ``` (*For proving rewrite rules*) ``` paulson@12199 ` 68` ``` fun prover s = (print s;prove_goalw (the_context ()) [Inter_def] s ``` paulson@12199 ` 69` ``` (fn _ => [Simp_tac 1, ``` paulson@12199 ` 70` ``` ALLGOALS (blast_tac (claset() addSIs[equalityI]))])); ``` paulson@12199 ` 71` paulson@12199 ` 72` ```in ``` paulson@12199 ` 73` paulson@12199 ` 74` ```val ball_simps = map prover ``` paulson@12199 ` 75` ``` ["(ALL x:A. P(x) | Q) <-> ((ALL x:A. P(x)) | Q)", ``` paulson@12199 ` 76` ``` "(ALL x:A. P | Q(x)) <-> (P | (ALL x:A. Q(x)))", ``` paulson@12199 ` 77` ``` "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))", ``` paulson@12199 ` 78` ``` "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)", ``` paulson@12199 ` 79` ``` "(ALL x:0.P(x)) <-> True", ``` paulson@12199 ` 80` ``` "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))", ``` paulson@12199 ` 81` ``` "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))", ``` paulson@12199 ` 82` ``` "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))", ``` paulson@12199 ` 83` ``` "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))", ``` paulson@12199 ` 84` ``` "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))", ``` paulson@12199 ` 85` ``` "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"]; ``` paulson@12199 ` 86` paulson@12199 ` 87` ```val ball_conj_distrib = ``` paulson@12199 ` 88` ``` prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"; ``` paulson@12199 ` 89` paulson@12199 ` 90` ```val bex_simps = map prover ``` paulson@12199 ` 91` ``` ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)", ``` paulson@12199 ` 92` ``` "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))", ``` paulson@12199 ` 93` ``` "(EX x:0.P(x)) <-> False", ``` paulson@12199 ` 94` ``` "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))", ``` paulson@12199 ` 95` ``` "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))", ``` paulson@12199 ` 96` ``` "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))", ``` paulson@12199 ` 97` ``` "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))", ``` paulson@12199 ` 98` ``` "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))", ``` paulson@12199 ` 99` ``` "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"]; ``` paulson@12199 ` 100` paulson@12199 ` 101` ```val bex_disj_distrib = ``` paulson@12199 ` 102` ``` prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))"; ``` paulson@12199 ` 103` paulson@12199 ` 104` ```val Rep_simps = map prover ``` paulson@12199 ` 105` ``` ["{x. y:0, R(x,y)} = 0", (*Replace*) ``` paulson@12199 ` 106` ``` "{x:0. P(x)} = 0", (*Collect*) ``` paulson@12199 ` 107` ``` "{x:A. False} = 0", ``` paulson@12199 ` 108` ``` "{x:A. True} = A", ``` paulson@12199 ` 109` ``` "RepFun(0,f) = 0", (*RepFun*) ``` paulson@12199 ` 110` ``` "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))", ``` paulson@12199 ` 111` ``` "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"] ``` paulson@12199 ` 112` paulson@12199 ` 113` ```val misc_simps = map prover ``` paulson@12199 ` 114` ``` ["0 Un A = A", "A Un 0 = A", ``` paulson@12199 ` 115` ``` "0 Int A = 0", "A Int 0 = 0", ``` paulson@12199 ` 116` ``` "0 - A = 0", "A - 0 = A", ``` paulson@12199 ` 117` ``` "Union(0) = 0", ``` paulson@12199 ` 118` ``` "Union(cons(b,A)) = b Un Union(A)", ``` paulson@12199 ` 119` ``` "Inter({b}) = b"] ``` paulson@12199 ` 120` paulson@12199 ` 121` paulson@12199 ` 122` ```val UN_simps = map prover ``` paulson@12199 ` 123` ``` ["(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))", ``` paulson@12199 ` 124` ``` "(UN x:C. A(x) Un B) = (if C=0 then 0 else (UN x:C. A(x)) Un B)", ``` paulson@12199 ` 125` ``` "(UN x:C. A Un B(x)) = (if C=0 then 0 else A Un (UN x:C. B(x)))", ``` paulson@12199 ` 126` ``` "(UN x:C. A(x) Int B) = ((UN x:C. A(x)) Int B)", ``` paulson@12199 ` 127` ``` "(UN x:C. A Int B(x)) = (A Int (UN x:C. B(x)))", ``` paulson@12199 ` 128` ``` "(UN x:C. A(x) - B) = ((UN x:C. A(x)) - B)", ``` paulson@12199 ` 129` ``` "(UN x:C. A - B(x)) = (if C=0 then 0 else A - (INT x:C. B(x)))", ``` paulson@12199 ` 130` ``` "(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))", ``` paulson@12199 ` 131` ``` "(UN z: (UN x:A. B(x)). C(z)) = (UN x:A. UN z: B(x). C(z))", ``` paulson@12199 ` 132` ``` "(UN x: RepFun(A,f). B(x)) = (UN a:A. B(f(a)))"]; ``` paulson@12199 ` 133` paulson@12199 ` 134` ```val INT_simps = map prover ``` paulson@12199 ` 135` ``` ["(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B", ``` paulson@12199 ` 136` ``` "(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))", ``` paulson@12199 ` 137` ``` "(INT x:C. A(x) - B) = (INT x:C. A(x)) - B", ``` paulson@12199 ` 138` ``` "(INT x:C. A - B(x)) = (if C=0 then 0 else A - (UN x:C. B(x)))", ``` paulson@12199 ` 139` ``` "(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))", ``` paulson@12199 ` 140` ``` "(INT x:C. A(x) Un B) = (if C=0 then 0 else (INT x:C. A(x)) Un B)", ``` paulson@12199 ` 141` ``` "(INT x:C. A Un B(x)) = (if C=0 then 0 else A Un (INT x:C. B(x)))"]; ``` paulson@12199 ` 142` paulson@12199 ` 143` ```(** The _extend_simps rules are oriented in the opposite direction, to ``` paulson@12199 ` 144` ``` pull UN and INT outwards. **) ``` paulson@12199 ` 145` paulson@12199 ` 146` ```val UN_extend_simps = map prover ``` paulson@12199 ` 147` ``` ["cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))", ``` paulson@12199 ` 148` ``` "(UN x:C. A(x)) Un B = (if C=0 then B else (UN x:C. A(x) Un B))", ``` paulson@12199 ` 149` ``` "A Un (UN x:C. B(x)) = (if C=0 then A else (UN x:C. A Un B(x)))", ``` paulson@12199 ` 150` ``` "((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)", ``` paulson@12199 ` 151` ``` "(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))", ``` paulson@12199 ` 152` ``` "((UN x:C. A(x)) - B) = (UN x:C. A(x) - B)", ``` paulson@12199 ` 153` ``` "A - (INT x:C. B(x)) = (if C=0 then A else (UN x:C. A - B(x)))", ``` paulson@12199 ` 154` ``` "(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))", ``` paulson@12199 ` 155` ``` "(UN x:A. UN z: B(x). C(z)) = (UN z: (UN x:A. B(x)). C(z))", ``` paulson@12199 ` 156` ``` "(UN a:A. B(f(a))) = (UN x: RepFun(A,f). B(x))"]; ``` paulson@12199 ` 157` paulson@12199 ` 158` ```val INT_extend_simps = map prover ``` paulson@12199 ` 159` ``` ["(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)", ``` paulson@12199 ` 160` ``` "A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))", ``` paulson@12199 ` 161` ``` "(INT x:C. A(x)) - B = (INT x:C. A(x) - B)", ``` paulson@12199 ` 162` ``` "A - (UN x:C. B(x)) = (if C=0 then A else (INT x:C. A - B(x)))", ``` paulson@12199 ` 163` ``` "cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))", ``` paulson@12199 ` 164` ``` "(INT x:C. A(x)) Un B = (if C=0 then B else (INT x:C. A(x) Un B))", ``` paulson@12199 ` 165` ``` "A Un (INT x:C. B(x)) = (if C=0 then A else (INT x:C. A Un B(x)))"]; ``` paulson@12199 ` 166` paulson@12199 ` 167` ```end; ``` paulson@12199 ` 168` paulson@12199 ` 169` ```bind_thms ("ball_simps", ball_simps); ``` paulson@12199 ` 170` ```bind_thm ("ball_conj_distrib", ball_conj_distrib); ``` paulson@12199 ` 171` ```bind_thms ("bex_simps", bex_simps); ``` paulson@12199 ` 172` ```bind_thm ("bex_disj_distrib", bex_disj_distrib); ``` paulson@12199 ` 173` ```bind_thms ("Rep_simps", Rep_simps); ``` paulson@12199 ` 174` ```bind_thms ("misc_simps", misc_simps); ``` paulson@12199 ` 175` paulson@12199 ` 176` ```Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps); ``` paulson@12199 ` 177` paulson@12199 ` 178` ```bind_thms ("UN_simps", UN_simps); ``` paulson@12199 ` 179` ```bind_thms ("INT_simps", INT_simps); ``` paulson@12199 ` 180` paulson@12199 ` 181` ```Addsimps (UN_simps @ INT_simps); ``` paulson@12199 ` 182` paulson@12199 ` 183` ```bind_thms ("UN_extend_simps", UN_extend_simps); ``` paulson@12199 ` 184` ```bind_thms ("INT_extend_simps", INT_extend_simps); ``` paulson@12199 ` 185` paulson@12199 ` 186` paulson@11233 ` 187` ```(** One-point rule for bounded quantifiers: see HOL/Set.ML **) ``` paulson@11233 ` 188` paulson@11233 ` 189` ```Goal "(EX x:A. x=a) <-> (a:A)"; ``` paulson@11233 ` 190` ```by (Blast_tac 1); ``` paulson@11233 ` 191` ```qed "bex_triv_one_point1"; ``` paulson@11233 ` 192` paulson@11233 ` 193` ```Goal "(EX x:A. a=x) <-> (a:A)"; ``` paulson@11233 ` 194` ```by (Blast_tac 1); ``` paulson@11233 ` 195` ```qed "bex_triv_one_point2"; ``` paulson@11233 ` 196` paulson@11233 ` 197` ```Goal "(EX x:A. x=a & P(x)) <-> (a:A & P(a))"; ``` paulson@11233 ` 198` ```by (Blast_tac 1); ``` paulson@11233 ` 199` ```qed "bex_one_point1"; ``` paulson@11233 ` 200` paulson@11233 ` 201` ```Goal "(EX x:A. a=x & P(x)) <-> (a:A & P(a))"; ``` paulson@11233 ` 202` ```by(Blast_tac 1); ``` paulson@11233 ` 203` ```qed "bex_one_point2"; ``` paulson@11233 ` 204` paulson@11233 ` 205` ```Goal "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))"; ``` paulson@11233 ` 206` ```by (Blast_tac 1); ``` paulson@11233 ` 207` ```qed "ball_one_point1"; ``` paulson@11233 ` 208` paulson@11233 ` 209` ```Goal "(ALL x:A. a=x --> P(x)) <-> (a:A --> P(a))"; ``` paulson@11233 ` 210` ```by (Blast_tac 1); ``` paulson@11233 ` 211` ```qed "ball_one_point2"; ``` paulson@11233 ` 212` paulson@11233 ` 213` ```Addsimps [bex_triv_one_point1,bex_triv_one_point2, ``` paulson@11233 ` 214` ``` bex_one_point1,bex_one_point2, ``` paulson@11233 ` 215` ``` ball_one_point1,ball_one_point2]; ``` paulson@11233 ` 216` paulson@12199 ` 217` paulson@11233 ` 218` ```let ``` paulson@11233 ` 219` ```val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) ``` paulson@11233 ` 220` ``` ("EX x:A. P(x) & Q(x)",FOLogic.oT) ``` paulson@11233 ` 221` paulson@11233 ` 222` ```val prove_bex_tac = rewrite_goals_tac [Bex_def] THEN ``` paulson@11233 ` 223` ``` Quantifier1.prove_one_point_ex_tac; ``` paulson@11233 ` 224` paulson@11233 ` 225` ```val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; ``` paulson@11233 ` 226` paulson@11233 ` 227` ```val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) ``` paulson@11233 ` 228` ``` ("ALL x:A. P(x) --> Q(x)",FOLogic.oT) ``` paulson@11233 ` 229` paulson@11233 ` 230` ```val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN ``` paulson@11233 ` 231` ``` Quantifier1.prove_one_point_all_tac; ``` paulson@11233 ` 232` paulson@11233 ` 233` ```val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; ``` paulson@11233 ` 234` paulson@11233 ` 235` ```val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex; ``` paulson@11233 ` 236` ```val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball; ``` paulson@11233 ` 237` ```in ``` paulson@11233 ` 238` paulson@11233 ` 239` ```Addsimprocs [defBALL_regroup,defBEX_regroup] ``` paulson@11233 ` 240` paulson@11233 ` 241` ```end; ``` paulson@11233 ` 242` paulson@12199 ` 243` wenzelm@4091 ` 244` ```val ZF_ss = simpset(); ```