src/ZF/simpdata.ML
author lcp
Thu Apr 13 11:38:48 1995 +0200 (1995-04-13)
changeset 1036 0d28f4bc8a44
parent 855 4c8d0ece1f95
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
Recoded function atomize so that new ways of creating
simplification rules can be added easily.
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
lcp@1036
    40
(*Analyse a theorem to atomic rewrite rules*)
lcp@1036
    41
fun atomize (conn_pairs, mem_pairs) th = 
lcp@1036
    42
  let fun tryrules pairs t =
lcp@1036
    43
	  case head_of t of
lcp@1036
    44
	      Const(a,_) => 
lcp@1036
    45
		(case assoc(pairs,a) of
lcp@1036
    46
		     Some rls => flat (map (atomize (conn_pairs, mem_pairs))
lcp@1036
    47
				       ([th] RL rls))
lcp@1036
    48
		   | None     => [th])
lcp@1036
    49
	    | _ => [th]
lcp@1036
    50
  in case concl_of th of 
lcp@1036
    51
	 Const("Trueprop",_) $ P => 
lcp@1036
    52
	    (case P of
lcp@1036
    53
		 Const("op :",_) $ a $ b => tryrules mem_pairs b
lcp@1036
    54
	       | Const("True",_)         => []
lcp@1036
    55
	       | Const("False",_)        => []
lcp@1036
    56
	       | A => tryrules conn_pairs A)
lcp@1036
    57
       | _                       => [th]
lcp@1036
    58
  end;
lcp@1036
    59
clasohm@0
    60
(*Analyse a rigid formula*)
lcp@1036
    61
val ZF_conn_pairs =
clasohm@0
    62
  [("Ball",	[bspec]), 
clasohm@0
    63
   ("All",	[spec]),
clasohm@0
    64
   ("op -->",	[mp]),
clasohm@0
    65
   ("op &",	[conjunct1,conjunct2])];
clasohm@0
    66
clasohm@0
    67
(*Analyse a:b, where b is rigid*)
lcp@1036
    68
val ZF_mem_pairs = 
clasohm@0
    69
  [("Collect",	[CollectD1,CollectD2]),
clasohm@0
    70
   ("op -",	[DiffD1,DiffD2]),
clasohm@0
    71
   ("op Int",	[IntD1,IntD2])];
clasohm@0
    72
lcp@855
    73
val ZF_simps = 
lcp@855
    74
    [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
lcp@855
    75
     beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, singleton_iff,
lcp@855
    76
     Sigma_empty1, Sigma_empty2, triv_RepFun, subset_refl];
clasohm@0
    77
lcp@6
    78
(*Sigma_cong, Pi_cong NOT included by default since they cause
lcp@6
    79
  flex-flex pairs and the "Check your prover" error -- because most
lcp@6
    80
  Sigma's and Pi's are abbreviated as * or -> *)
lcp@6
    81
val ZF_congs =
lcp@6
    82
   [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
clasohm@0
    83
lcp@1036
    84
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
lcp@1036
    85
lcp@6
    86
val ZF_ss = FOL_ss 
lcp@1036
    87
      setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
lcp@855
    88
      addsimps (ZF_simps @ mem_simps @ bquant_simps @ 
lcp@855
    89
		Collect_simps @ UnInt_simps)
lcp@6
    90
      addcongs ZF_congs;