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
     1 (*  Title:      ZF/simpdata
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Rewriting for ZF set theory -- based on FOL rewriting
     7 *)
     8 
     9 fun prove_fun s = 
    10     (writeln s;  prove_goal ZF.thy s
    11        (fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));
    12 
    13 val mem_rews = map prove_fun
    14  [ "a:0 <-> False",
    15    "a : A Un B <-> a:A | a:B",
    16    "a : A Int B <-> a:A & a:B",
    17    "a : A-B <-> a:A & ~a:B",
    18    "a : cons(b,B) <-> a=b | a:B",
    19    "i : succ(j) <-> i=j | i:j",
    20    "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
    21    "a : Collect(A,P) <-> a:A & P(a)" ];
    22 
    23 (** Tactics for type checking -- from CTT **)
    24 
    25 fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
    26       not (is_Var (head_of a))
    27   | is_rigid_elem _ = false;
    28 
    29 (*Try solving a:A by assumption provided a is rigid!*) 
    30 val test_assume_tac = SUBGOAL(fn (prem,i) =>
    31     if is_rigid_elem (Logic.strip_assums_concl prem)
    32     then  assume_tac i  else  no_tac);
    33 
    34 (*Type checking solves a:?A (a rigid, ?A maybe flexible).  
    35   match_tac is too strict; would refuse to instantiate ?A*)
    36 fun typechk_step_tac tyrls =
    37     FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
    38 
    39 fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
    40 
    41 val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
    42 
    43 (*To instantiate variables in typing conditions; 
    44   to perform type checking faster than rewriting can
    45   NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
    46 fun type_auto_tac tyrls hyps = SELECT_GOAL
    47     (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
    48            ORELSE ares_tac [TrueI,ballI,allI,conjI,impI] 1));
    49 
    50 (** New version of mk_rew_rules **)
    51 
    52 (*Should False yield False<->True, or should it solve goals some other way?*)
    53 
    54 (*Analyse a rigid formula*)
    55 val atomize_pairs =
    56   [("Ball",	[bspec]), 
    57    ("All",	[spec]),
    58    ("op -->",	[mp]),
    59    ("op &",	[conjunct1,conjunct2])];
    60 
    61 (*Analyse a:b, where b is rigid*)
    62 val atomize_mem_pairs = 
    63   [("Collect",	[CollectD1,CollectD2]),
    64    ("op -",	[DiffD1,DiffD2]),
    65    ("op Int",	[IntD1,IntD2])];
    66 
    67 (*Analyse a theorem to atomic rewrite rules*)
    68 fun atomize th = 
    69   let fun tryrules pairs t =
    70 	  case head_of t of
    71 	      Const(a,_) => 
    72 		(case assoc(pairs,a) of
    73 		     Some rls => flat (map atomize ([th] RL rls))
    74 		   | None     => [th])
    75 	    | _ => [th]
    76   in case concl_of th of (*The operator below is Trueprop*)
    77 	_ $ (Const("op :",_) $ a $ b) => tryrules atomize_mem_pairs b
    78       | _ $ (Const("True",_)) => []	(*True is DELETED*)
    79       | _ $ (Const("False",_)) => []	(*should False do something??*)
    80       | _ $ A => tryrules atomize_pairs A
    81   end;
    82 
    83 fun ZF_mk_rew_rules th = map mk_eq (atomize th);
    84 
    85 
    86 fun auto_tac rls hyps = SELECT_GOAL (DEPTH_SOLVE_1 (ares_tac (rls@hyps) 1));
    87 
    88 structure ZF_SimpData : SIMP_DATA =
    89   struct
    90   val refl_thms		= FOL_SimpData.refl_thms
    91   val trans_thms	= FOL_SimpData.trans_thms
    92   val red1		= FOL_SimpData.red1
    93   val red2		= FOL_SimpData.red2
    94   val mk_rew_rules	= ZF_mk_rew_rules 
    95   val norm_thms		= FOL_SimpData.norm_thms
    96   val subst_thms	= FOL_SimpData.subst_thms
    97   val dest_red		= FOL_SimpData.dest_red
    98   end;
    99 
   100 structure ZF_Simp = SimpFun(ZF_SimpData);
   101 
   102 open ZF_Simp;
   103 
   104 (*Redeclared because the previous FOL_ss belongs to a different instance
   105   of type simpset*)
   106 val FOL_ss = empty_ss addcongs FOL_congs addrews FOL_rews 
   107 		      setauto auto_tac[TrueI,ballI];
   108 
   109 (** Basic congruence and rewrite rules for ZF set theory **)
   110 
   111 val ZF_congs = 
   112    [ball_cong,bex_cong,Replace_cong,RepFun_cong,Collect_cong,the_cong,
   113     if_cong,Sigma_cong,split_cong,Pi_cong,lam_cong] @ basic_ZF_congs;
   114 
   115 val ZF_rews = [empty_subsetI, ball_rew, if_true, if_false, 
   116 	       beta, eta, restrict,
   117 	       fst_conv, snd_conv, split];
   118 
   119 val ZF_ss = FOL_ss addcongs ZF_congs addrews (ZF_rews@mem_rews);
   120