src/ZF/simpdata.ML
 author lcp Tue Jul 12 18:05:03 1994 +0200 (1994-07-12 ago) changeset 467 92868dab2939 parent 435 ca5356bd315a child 485 5e00a676a211 permissions -rw-r--r--
new cardinal arithmetic developments
```     1 (*  Title:      ZF/simpdata
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1991  University of Cambridge
```
```     5
```
```     6 Rewriting for ZF set theory -- based on FOL rewriting
```
```     7 *)
```
```     8
```
```     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) ]));
```
```    12
```
```    13 (*INCLUDED IN ZF_ss*)
```
```    14 val mem_simps = map prove_fun
```
```    15  [ "a : 0             <-> False",
```
```    16    "a : A Un B        <-> a:A | a:B",
```
```    17    "a : A Int B       <-> a:A & a:B",
```
```    18    "a : A-B           <-> a:A & ~a:B",
```
```    19    "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
```
```    20    "a : Collect(A,P)  <-> a:A & P(a)" ];
```
```    21
```
```    22 goal ZF.thy "{x.x:A} = A";
```
```    23 by (fast_tac eq_cs 1);
```
```    24 val triv_RepFun = result();
```
```    25
```
```    26 (*INCLUDED: should be??*)
```
```    27 val bquant_simps = map prove_fun
```
```    28  [ "(ALL x:0.P(x)) <-> True",
```
```    29    "(EX  x:0.P(x)) <-> False",
```
```    30    "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
```
```    31    "(EX  x:succ(i).P(x)) <-> P(i) | (EX  x:i.P(x))" ];
```
```    32
```
```    33 (** Tactics for type checking -- from CTT **)
```
```    34
```
```    35 fun is_rigid_elem (Const("Trueprop",_) \$ (Const("op :",_) \$ a \$ _)) =
```
```    36       not (is_Var (head_of a))
```
```    37   | is_rigid_elem _ = false;
```
```    38
```
```    39 (*Try solving a:A by assumption provided a is rigid!*)
```
```    40 val test_assume_tac = SUBGOAL(fn (prem,i) =>
```
```    41     if is_rigid_elem (Logic.strip_assums_concl prem)
```
```    42     then  assume_tac i  else  no_tac);
```
```    43
```
```    44 (*Type checking solves a:?A (a rigid, ?A maybe flexible).
```
```    45   match_tac is too strict; would refuse to instantiate ?A*)
```
```    46 fun typechk_step_tac tyrls =
```
```    47     FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
```
```    48
```
```    49 fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
```
```    50
```
```    51 val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
```
```    52
```
```    53 (*To instantiate variables in typing conditions;
```
```    54   to perform type checking faster than rewriting can
```
```    55   NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
```
```    56 fun type_auto_tac tyrls hyps = SELECT_GOAL
```
```    57     (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
```
```    58            ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
```
```    59
```
```    60 (** New version of mk_rew_rules **)
```
```    61
```
```    62 (*Should False yield False<->True, or should it solve goals some other way?*)
```
```    63
```
```    64 (*Analyse a rigid formula*)
```
```    65 val atomize_pairs =
```
```    66   [("Ball",	[bspec]),
```
```    67    ("All",	[spec]),
```
```    68    ("op -->",	[mp]),
```
```    69    ("op &",	[conjunct1,conjunct2])];
```
```    70
```
```    71 (*Analyse a:b, where b is rigid*)
```
```    72 val atomize_mem_pairs =
```
```    73   [("Collect",	[CollectD1,CollectD2]),
```
```    74    ("op -",	[DiffD1,DiffD2]),
```
```    75    ("op Int",	[IntD1,IntD2])];
```
```    76
```
```    77 (*Analyse a theorem to atomic rewrite rules*)
```
```    78 fun atomize th =
```
```    79   let fun tryrules pairs t =
```
```    80 	  case head_of t of
```
```    81 	      Const(a,_) =>
```
```    82 		(case assoc(pairs,a) of
```
```    83 		     Some rls => flat (map atomize ([th] RL rls))
```
```    84 		   | None     => [th])
```
```    85 	    | _ => [th]
```
```    86   in case concl_of th of
```
```    87        Const("Trueprop",_) \$ P =>
```
```    88 	  (case P of
```
```    89 	       Const("op :",_) \$ a \$ b => tryrules atomize_mem_pairs b
```
```    90 	     | Const("True",_)         => []
```
```    91 	     | Const("False",_)        => []
```
```    92 	     | A => tryrules atomize_pairs A)
```
```    93      | _                       => [th]
```
```    94   end;
```
```    95
```
```    96 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false,
```
```    97 		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff,
```
```    98 		triv_RepFun];
```
```    99
```
```   100 (*Sigma_cong, Pi_cong NOT included by default since they cause
```
```   101   flex-flex pairs and the "Check your prover" error -- because most
```
```   102   Sigma's and Pi's are abbreviated as * or -> *)
```
```   103 val ZF_congs =
```
```   104    [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
```
```   105
```
```   106 val ZF_ss = FOL_ss
```
```   107       setmksimps (map mk_meta_eq o atomize o gen_all)
```
```   108       addsimps (ZF_simps @ mem_simps @ bquant_simps)
```
```   109       addcongs ZF_congs;
```