src/ZF/simpdata.ML
 author clasohm Thu Sep 16 12:20:38 1993 +0200 (1993-09-16 ago) changeset 0 a5a9c433f639 child 6 8ce8c4d13d4d permissions -rw-r--r--
Initial revision
1 (*  Title:      ZF/simpdata
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   1991  University of Cambridge
6 Rewriting for ZF set theory -- based on FOL rewriting
7 *)
9 fun prove_fun s =
10     (writeln s;  prove_goal ZF.thy s
11        (fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));
13 val mem_rews = map prove_fun
14  [ "a:0 <-> False",
15    "a : A Un B <-> a:A | a:B",
16    "a : A Int B <-> a:A & a:B",
17    "a : A-B <-> a:A & ~a:B",
18    "a : cons(b,B) <-> a=b | a:B",
19    "i : succ(j) <-> i=j | i:j",
20    "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
21    "a : Collect(A,P) <-> a:A & P(a)" ];
23 (** Tactics for type checking -- from CTT **)
25 fun is_rigid_elem (Const("Trueprop",_) \$ (Const("op :",_) \$ a \$ _)) =
27   | is_rigid_elem _ = false;
29 (*Try solving a:A by assumption provided a is rigid!*)
30 val test_assume_tac = SUBGOAL(fn (prem,i) =>
31     if is_rigid_elem (Logic.strip_assums_concl prem)
32     then  assume_tac i  else  no_tac);
34 (*Type checking solves a:?A (a rigid, ?A maybe flexible).
35   match_tac is too strict; would refuse to instantiate ?A*)
36 fun typechk_step_tac tyrls =
37     FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
39 fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
41 val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
43 (*To instantiate variables in typing conditions;
44   to perform type checking faster than rewriting can
45   NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
46 fun type_auto_tac tyrls hyps = SELECT_GOAL
47     (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
48            ORELSE ares_tac [TrueI,ballI,allI,conjI,impI] 1));
50 (** New version of mk_rew_rules **)
52 (*Should False yield False<->True, or should it solve goals some other way?*)
54 (*Analyse a rigid formula*)
55 val atomize_pairs =
56   [("Ball",	[bspec]),
57    ("All",	[spec]),
58    ("op -->",	[mp]),
59    ("op &",	[conjunct1,conjunct2])];
61 (*Analyse a:b, where b is rigid*)
62 val atomize_mem_pairs =
63   [("Collect",	[CollectD1,CollectD2]),
64    ("op -",	[DiffD1,DiffD2]),
65    ("op Int",	[IntD1,IntD2])];
67 (*Analyse a theorem to atomic rewrite rules*)
68 fun atomize th =
69   let fun tryrules pairs t =
71 	      Const(a,_) =>
72 		(case assoc(pairs,a) of
73 		     Some rls => flat (map atomize ([th] RL rls))
74 		   | None     => [th])
75 	    | _ => [th]
76   in case concl_of th of (*The operator below is Trueprop*)
77 	_ \$ (Const("op :",_) \$ a \$ b) => tryrules atomize_mem_pairs b
78       | _ \$ (Const("True",_)) => []	(*True is DELETED*)
79       | _ \$ (Const("False",_)) => []	(*should False do something??*)
80       | _ \$ A => tryrules atomize_pairs A
81   end;
83 fun ZF_mk_rew_rules th = map mk_eq (atomize th);
86 fun auto_tac rls hyps = SELECT_GOAL (DEPTH_SOLVE_1 (ares_tac (rls@hyps) 1));
88 structure ZF_SimpData : SIMP_DATA =
89   struct
90   val refl_thms		= FOL_SimpData.refl_thms
91   val trans_thms	= FOL_SimpData.trans_thms
92   val red1		= FOL_SimpData.red1
93   val red2		= FOL_SimpData.red2
94   val mk_rew_rules	= ZF_mk_rew_rules
95   val norm_thms		= FOL_SimpData.norm_thms
96   val subst_thms	= FOL_SimpData.subst_thms
97   val dest_red		= FOL_SimpData.dest_red
98   end;
100 structure ZF_Simp = SimpFun(ZF_SimpData);
102 open ZF_Simp;
104 (*Redeclared because the previous FOL_ss belongs to a different instance
105   of type simpset*)