src/ZF/simpdata.ML
 author paulson Fri Jun 07 10:56:37 1996 +0200 (1996-06-07 ago) changeset 1791 6b38717439c6 parent 1612 f9f0145e1c7e child 2469 b50b8c0eec01 permissions -rw-r--r--
Addition of converse_iff, domain_converse, range_converse as rewrites
```     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 (** Tactics for type checking -- from CTT **)
```
```    10
```
```    11 fun is_rigid_elem (Const("Trueprop",_) \$ (Const("op :",_) \$ a \$ _)) =
```
```    12       not (is_Var (head_of a))
```
```    13   | is_rigid_elem _ = false;
```
```    14
```
```    15 (*Try solving a:A by assumption provided a is rigid!*)
```
```    16 val test_assume_tac = SUBGOAL(fn (prem,i) =>
```
```    17     if is_rigid_elem (Logic.strip_assums_concl prem)
```
```    18     then  assume_tac i  else  eq_assume_tac i);
```
```    19
```
```    20 (*Type checking solves a:?A (a rigid, ?A maybe flexible).
```
```    21   match_tac is too strict; would refuse to instantiate ?A*)
```
```    22 fun typechk_step_tac tyrls =
```
```    23     FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
```
```    24
```
```    25 fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
```
```    26
```
```    27 val ZF_typechecks =
```
```    28     [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
```
```    29
```
```    30 (*Instantiates variables in typing conditions.
```
```    31   drawback: does not simplify conjunctions*)
```
```    32 fun type_auto_tac tyrls hyps = SELECT_GOAL
```
```    33     (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
```
```    34            ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
```
```    35
```
```    36 (** New version of mk_rew_rules **)
```
```    37
```
```    38 (*Should False yield False<->True, or should it solve goals some other way?*)
```
```    39
```
```    40 (*Analyse a theorem to atomic rewrite rules*)
```
```    41 fun atomize (conn_pairs, mem_pairs) th =
```
```    42   let fun tryrules pairs t =
```
```    43           case head_of t of
```
```    44               Const(a,_) =>
```
```    45                 (case assoc(pairs,a) of
```
```    46                      Some rls => flat (map (atomize (conn_pairs, mem_pairs))
```
```    47                                        ([th] RL rls))
```
```    48                    | None     => [th])
```
```    49             | _ => [th]
```
```    50   in case concl_of th of
```
```    51          Const("Trueprop",_) \$ P =>
```
```    52             (case P of
```
```    53                  Const("op :",_) \$ a \$ b => tryrules mem_pairs b
```
```    54                | Const("True",_)         => []
```
```    55                | Const("False",_)        => []
```
```    56                | A => tryrules conn_pairs A)
```
```    57        | _                       => [th]
```
```    58   end;
```
```    59
```
```    60 (*Analyse a rigid formula*)
```
```    61 val ZF_conn_pairs =
```
```    62   [("Ball",     [bspec]),
```
```    63    ("All",      [spec]),
```
```    64    ("op -->",   [mp]),
```
```    65    ("op &",     [conjunct1,conjunct2])];
```
```    66
```
```    67 (*Analyse a:b, where b is rigid*)
```
```    68 val ZF_mem_pairs =
```
```    69   [("Collect",  [CollectD1,CollectD2]),
```
```    70    ("op -",     [DiffD1,DiffD2]),
```
```    71    ("op Int",   [IntD1,IntD2])];
```
```    72
```
```    73 val ZF_simps =
```
```    74     [empty_subsetI, consI1, cons_not_0, cons_not_0 RS not_sym,
```
```    75      succI1, succ_not_0, succ_not_0 RS not_sym, succ_inject_iff,
```
```    76      ball_simp, if_true, if_false,
```
```    77      beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, singleton_iff,
```
```    78      converse_iff, domain_converse, range_converse,
```
```    79      Sigma_empty1, Sigma_empty2, triv_RepFun, subset_refl];
```
```    80
```
```    81 (*Sigma_cong, Pi_cong NOT included by default since they cause
```
```    82   flex-flex pairs and the "Check your prover" error -- because most
```
```    83   Sigma's and Pi's are abbreviated as * or -> *)
```
```    84 val ZF_congs =
```
```    85    [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
```
```    86
```
```    87 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
```
```    88
```
```    89 val ZF_ss = FOL_ss
```
```    90       setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
```
```    91       addsimps (ZF_simps @ mem_simps @ bquant_simps @
```
```    92                 Collect_simps @ UnInt_simps)
```
```    93       addcongs ZF_congs;
```