src/ZF/simpdata.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
permissions -rw-r--r--
Initial revision
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
clasohm@0
    13
val mem_rews = 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)
clasohm@0
    48
           ORELSE ares_tac [TrueI,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
clasohm@0
    83
fun ZF_mk_rew_rules th = map mk_eq (atomize th);
clasohm@0
    84
clasohm@0
    85
clasohm@0
    86
fun auto_tac rls hyps = SELECT_GOAL (DEPTH_SOLVE_1 (ares_tac (rls@hyps) 1));
clasohm@0
    87
clasohm@0
    88
structure ZF_SimpData : SIMP_DATA =
clasohm@0
    89
  struct
clasohm@0
    90
  val refl_thms		= FOL_SimpData.refl_thms
clasohm@0
    91
  val trans_thms	= FOL_SimpData.trans_thms
clasohm@0
    92
  val red1		= FOL_SimpData.red1
clasohm@0
    93
  val red2		= FOL_SimpData.red2
clasohm@0
    94
  val mk_rew_rules	= ZF_mk_rew_rules 
clasohm@0
    95
  val norm_thms		= FOL_SimpData.norm_thms
clasohm@0
    96
  val subst_thms	= FOL_SimpData.subst_thms
clasohm@0
    97
  val dest_red		= FOL_SimpData.dest_red
clasohm@0
    98
  end;
clasohm@0
    99
clasohm@0
   100
structure ZF_Simp = SimpFun(ZF_SimpData);
clasohm@0
   101
clasohm@0
   102
open ZF_Simp;
clasohm@0
   103
clasohm@0
   104
(*Redeclared because the previous FOL_ss belongs to a different instance
clasohm@0
   105
  of type simpset*)
clasohm@0
   106
val FOL_ss = empty_ss addcongs FOL_congs addrews FOL_rews 
clasohm@0
   107
		      setauto auto_tac[TrueI,ballI];
clasohm@0
   108
clasohm@0
   109
(** Basic congruence and rewrite rules for ZF set theory **)
clasohm@0
   110
clasohm@0
   111
val ZF_congs = 
clasohm@0
   112
   [ball_cong,bex_cong,Replace_cong,RepFun_cong,Collect_cong,the_cong,
clasohm@0
   113
    if_cong,Sigma_cong,split_cong,Pi_cong,lam_cong] @ basic_ZF_congs;
clasohm@0
   114
clasohm@0
   115
val ZF_rews = [empty_subsetI, ball_rew, if_true, if_false, 
clasohm@0
   116
	       beta, eta, restrict,
clasohm@0
   117
	       fst_conv, snd_conv, split];
clasohm@0
   118
clasohm@0
   119
val ZF_ss = FOL_ss addcongs ZF_congs addrews (ZF_rews@mem_rews);
clasohm@0
   120