src/ZF/simpdata.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 1612 f9f0145e1c7e
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title:      ZF/simpdata
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Rewriting for ZF set theory -- based on FOL rewriting
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
(** Tactics for type checking -- from CTT **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
      not (is_Var (head_of a))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  | is_rigid_elem _ = false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
(*Try solving a:A by assumption provided a is rigid!*) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
val test_assume_tac = SUBGOAL(fn (prem,i) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
    if is_rigid_elem (Logic.strip_assums_concl prem)
762
1cf9ebcc3ff3 test_assume_tac: now tries eq_assume_tac on exceptional cases
lcp
parents: 533
diff changeset
    18
    then  assume_tac i  else  eq_assume_tac i);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
(*Type checking solves a:?A (a rigid, ?A maybe flexible).  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  match_tac is too strict; would refuse to instantiate ?A*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
fun typechk_step_tac tyrls =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
    FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
855
4c8d0ece1f95 Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents: 762
diff changeset
    27
val ZF_typechecks =
4c8d0ece1f95 Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents: 762
diff changeset
    28
    [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    30
(*Instantiates variables in typing conditions.
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    31
  drawback: does not simplify conjunctions*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
fun type_auto_tac tyrls hyps = SELECT_GOAL
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
    (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    34
           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
(** New version of mk_rew_rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
(*Should False yield False<->True, or should it solve goals some other way?*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    40
(*Analyse a theorem to atomic rewrite rules*)
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    41
fun atomize (conn_pairs, mem_pairs) th = 
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    42
  let fun tryrules pairs t =
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    43
          case head_of t of
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    44
              Const(a,_) => 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    45
                (case assoc(pairs,a) of
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    46
                     Some rls => flat (map (atomize (conn_pairs, mem_pairs))
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    47
                                       ([th] RL rls))
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    48
                   | None     => [th])
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    49
            | _ => [th]
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    50
  in case concl_of th of 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    51
         Const("Trueprop",_) $ P => 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    52
            (case P of
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    53
                 Const("op :",_) $ a $ b => tryrules mem_pairs b
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    54
               | Const("True",_)         => []
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    55
               | Const("False",_)        => []
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    56
               | A => tryrules conn_pairs A)
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    57
       | _                       => [th]
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    58
  end;
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    59
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
(*Analyse a rigid formula*)
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    61
val ZF_conn_pairs =
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    62
  [("Ball",     [bspec]), 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    63
   ("All",      [spec]),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    64
   ("op -->",   [mp]),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    65
   ("op &",     [conjunct1,conjunct2])];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
(*Analyse a:b, where b is rigid*)
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    68
val ZF_mem_pairs = 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    69
  [("Collect",  [CollectD1,CollectD2]),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    70
   ("op -",     [DiffD1,DiffD2]),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    71
   ("op Int",   [IntD1,IntD2])];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
855
4c8d0ece1f95 Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents: 762
diff changeset
    73
val ZF_simps = 
4c8d0ece1f95 Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents: 762
diff changeset
    74
    [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
4c8d0ece1f95 Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents: 762
diff changeset
    75
     beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, singleton_iff,
4c8d0ece1f95 Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents: 762
diff changeset
    76
     Sigma_empty1, Sigma_empty2, triv_RepFun, subset_refl];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    78
(*Sigma_cong, Pi_cong NOT included by default since they cause
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    79
  flex-flex pairs and the "Check your prover" error -- because most
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    80
  Sigma's and Pi's are abbreviated as * or -> *)
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    81
val ZF_congs =
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    82
   [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    84
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    85
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    86
val ZF_ss = FOL_ss 
1036
0d28f4bc8a44 Recoded function atomize so that new ways of creating
lcp
parents: 855
diff changeset
    87
      setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
855
4c8d0ece1f95 Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
lcp
parents: 762
diff changeset
    88
      addsimps (ZF_simps @ mem_simps @ bquant_simps @ 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1036
diff changeset
    89
                Collect_simps @ UnInt_simps)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    90
      addcongs ZF_congs;