src/ZF/simpdata.ML
 author paulson Mon May 21 14:53:30 2001 +0200 (2001-05-21) changeset 11323 92eddd0914a9 parent 11233 34c81a796ee3 child 11695 8c66866fb0ff permissions -rw-r--r--
if_splits and split_if_asm
 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` paulson@11323 ` 120` ```(** Splitting IFs in the assumptions **) ``` paulson@11323 ` 121` paulson@11323 ` 122` ```Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))"; ``` paulson@11323 ` 123` ```by (Simp_tac 1); ``` paulson@11323 ` 124` ```qed "split_if_asm"; ``` paulson@11323 ` 125` paulson@11323 ` 126` ```bind_thms ("if_splits", [split_if, split_if_asm]); ``` paulson@11323 ` 127` paulson@11233 ` 128` ```(** One-point rule for bounded quantifiers: see HOL/Set.ML **) ``` paulson@11233 ` 129` paulson@11233 ` 130` ```Goal "(EX x:A. x=a) <-> (a:A)"; ``` paulson@11233 ` 131` ```by (Blast_tac 1); ``` paulson@11233 ` 132` ```qed "bex_triv_one_point1"; ``` paulson@11233 ` 133` paulson@11233 ` 134` ```Goal "(EX x:A. a=x) <-> (a:A)"; ``` paulson@11233 ` 135` ```by (Blast_tac 1); ``` paulson@11233 ` 136` ```qed "bex_triv_one_point2"; ``` paulson@11233 ` 137` paulson@11233 ` 138` ```Goal "(EX x:A. x=a & P(x)) <-> (a:A & P(a))"; ``` paulson@11233 ` 139` ```by (Blast_tac 1); ``` paulson@11233 ` 140` ```qed "bex_one_point1"; ``` paulson@11233 ` 141` paulson@11233 ` 142` ```Goal "(EX x:A. a=x & P(x)) <-> (a:A & P(a))"; ``` paulson@11233 ` 143` ```by(Blast_tac 1); ``` paulson@11233 ` 144` ```qed "bex_one_point2"; ``` paulson@11233 ` 145` paulson@11233 ` 146` ```Goal "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))"; ``` paulson@11233 ` 147` ```by (Blast_tac 1); ``` paulson@11233 ` 148` ```qed "ball_one_point1"; ``` paulson@11233 ` 149` paulson@11233 ` 150` ```Goal "(ALL x:A. a=x --> P(x)) <-> (a:A --> P(a))"; ``` paulson@11233 ` 151` ```by (Blast_tac 1); ``` paulson@11233 ` 152` ```qed "ball_one_point2"; ``` paulson@11233 ` 153` paulson@11233 ` 154` ```Addsimps [bex_triv_one_point1,bex_triv_one_point2, ``` paulson@11233 ` 155` ``` bex_one_point1,bex_one_point2, ``` paulson@11233 ` 156` ``` ball_one_point1,ball_one_point2]; ``` paulson@11233 ` 157` paulson@11233 ` 158` ```let ``` paulson@11233 ` 159` ```val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) ``` paulson@11233 ` 160` ``` ("EX x:A. P(x) & Q(x)",FOLogic.oT) ``` paulson@11233 ` 161` paulson@11233 ` 162` ```val prove_bex_tac = rewrite_goals_tac [Bex_def] THEN ``` paulson@11233 ` 163` ``` Quantifier1.prove_one_point_ex_tac; ``` paulson@11233 ` 164` paulson@11233 ` 165` ```val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; ``` paulson@11233 ` 166` paulson@11233 ` 167` ```val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) ``` paulson@11233 ` 168` ``` ("ALL x:A. P(x) --> Q(x)",FOLogic.oT) ``` paulson@11233 ` 169` paulson@11233 ` 170` ```val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN ``` paulson@11233 ` 171` ``` Quantifier1.prove_one_point_all_tac; ``` paulson@11233 ` 172` paulson@11233 ` 173` ```val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; ``` paulson@11233 ` 174` paulson@11233 ` 175` ```val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex; ``` paulson@11233 ` 176` ```val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball; ``` paulson@11233 ` 177` ```in ``` paulson@11233 ` 178` paulson@11233 ` 179` ```Addsimprocs [defBALL_regroup,defBEX_regroup] ``` paulson@11233 ` 180` paulson@11233 ` 181` ```end; ``` paulson@11233 ` 182` wenzelm@4091 ` 183` ```val ZF_ss = simpset(); ```