src/ZF/simpdata.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
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
clasohm@0
     6
Rewriting for ZF set theory -- based on FOL rewriting
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
fun prove_fun s = 
clasohm@0
    10
    (writeln s;  prove_goal ZF.thy s
clasohm@0
    11
       (fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));
clasohm@0
    12
lcp@6
    13
val mem_simps = map prove_fun
clasohm@0
    14
 [ "a:0 <-> False",
clasohm@0
    15
   "a : A Un B <-> a:A | a:B",
clasohm@0
    16
   "a : A Int B <-> a:A & a:B",
clasohm@0
    17
   "a : A-B <-> a:A & ~a:B",
clasohm@0
    18
   "a : cons(b,B) <-> a=b | a:B",
clasohm@0
    19
   "i : succ(j) <-> i=j | i:j",
clasohm@0
    20
   "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
clasohm@0
    21
   "a : Collect(A,P) <-> a:A & P(a)" ];
clasohm@0
    22
clasohm@0
    23
(** Tactics for type checking -- from CTT **)
clasohm@0
    24
clasohm@0
    25
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
clasohm@0
    26
      not (is_Var (head_of a))
clasohm@0
    27
  | is_rigid_elem _ = false;
clasohm@0
    28
clasohm@0
    29
(*Try solving a:A by assumption provided a is rigid!*) 
clasohm@0
    30
val test_assume_tac = SUBGOAL(fn (prem,i) =>
clasohm@0
    31
    if is_rigid_elem (Logic.strip_assums_concl prem)
clasohm@0
    32
    then  assume_tac i  else  no_tac);
clasohm@0
    33
clasohm@0
    34
(*Type checking solves a:?A (a rigid, ?A maybe flexible).  
clasohm@0
    35
  match_tac is too strict; would refuse to instantiate ?A*)
clasohm@0
    36
fun typechk_step_tac tyrls =
clasohm@0
    37
    FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
clasohm@0
    38
clasohm@0
    39
fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
clasohm@0
    40
clasohm@0
    41
val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
clasohm@0
    42
clasohm@0
    43
(*To instantiate variables in typing conditions; 
clasohm@0
    44
  to perform type checking faster than rewriting can
clasohm@0
    45
  NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
clasohm@0
    46
fun type_auto_tac tyrls hyps = SELECT_GOAL
clasohm@0
    47
    (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
lcp@6
    48
           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
clasohm@0
    49
clasohm@0
    50
(** New version of mk_rew_rules **)
clasohm@0
    51
clasohm@0
    52
(*Should False yield False<->True, or should it solve goals some other way?*)
clasohm@0
    53
clasohm@0
    54
(*Analyse a rigid formula*)
clasohm@0
    55
val atomize_pairs =
clasohm@0
    56
  [("Ball",	[bspec]), 
clasohm@0
    57
   ("All",	[spec]),
clasohm@0
    58
   ("op -->",	[mp]),
clasohm@0
    59
   ("op &",	[conjunct1,conjunct2])];
clasohm@0
    60
clasohm@0
    61
(*Analyse a:b, where b is rigid*)
clasohm@0
    62
val atomize_mem_pairs = 
clasohm@0
    63
  [("Collect",	[CollectD1,CollectD2]),
clasohm@0
    64
   ("op -",	[DiffD1,DiffD2]),
clasohm@0
    65
   ("op Int",	[IntD1,IntD2])];
clasohm@0
    66
clasohm@0
    67
(*Analyse a theorem to atomic rewrite rules*)
clasohm@0
    68
fun atomize th = 
clasohm@0
    69
  let fun tryrules pairs t =
clasohm@0
    70
	  case head_of t of
clasohm@0
    71
	      Const(a,_) => 
clasohm@0
    72
		(case assoc(pairs,a) of
clasohm@0
    73
		     Some rls => flat (map atomize ([th] RL rls))
clasohm@0
    74
		   | None     => [th])
clasohm@0
    75
	    | _ => [th]
clasohm@0
    76
  in case concl_of th of (*The operator below is Trueprop*)
clasohm@0
    77
	_ $ (Const("op :",_) $ a $ b) => tryrules atomize_mem_pairs b
clasohm@0
    78
      | _ $ (Const("True",_)) => []	(*True is DELETED*)
clasohm@0
    79
      | _ $ (Const("False",_)) => []	(*should False do something??*)
clasohm@0
    80
      | _ $ A => tryrules atomize_pairs A
clasohm@0
    81
  end;
clasohm@0
    82
lcp@6
    83
fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
clasohm@0
    84
clasohm@0
    85
lcp@6
    86
val ZF_simps = [empty_subsetI, ball_simp, if_true, if_false, 
lcp@6
    87
		beta, eta, restrict, fst_conv, snd_conv, split];
clasohm@0
    88
lcp@6
    89
(*Sigma_cong, Pi_cong NOT included by default since they cause
lcp@6
    90
  flex-flex pairs and the "Check your prover" error -- because most
lcp@6
    91
  Sigma's and Pi's are abbreviated as * or -> *)
lcp@6
    92
val ZF_congs =
lcp@6
    93
   [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
clasohm@0
    94
lcp@6
    95
val ZF_ss = FOL_ss 
lcp@6
    96
      setmksimps ZF_mk_rew_rules
lcp@6
    97
      addsimps (ZF_simps@mem_simps)
lcp@6
    98
      addcongs ZF_congs;