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