author lcp
Thu, 30 Sep 1993 10:10:21 +0100
changeset 14 1c0926788772
parent 6 8ce8c4d13d4d
child 279 7738aed3f84d
permissions -rw-r--r--
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed

(*  Title:      ZF/simpdata
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Rewriting for ZF set theory -- based on FOL rewriting

fun prove_fun s = 
    (writeln s;  prove_goal ZF.thy s
       (fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));

val mem_simps = map prove_fun
 [ "a : 0             <-> False",
   "a : A Un B        <-> a:A | a:B",
   "a : A Int B       <-> a:A & a:B",
   "a : A-B           <-> a:A & ~a:B",
   "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
   "a : Collect(A,P)  <-> a:A & P(a)" ];

(*INCLUDED: should be??*)
val bquant_simps = map prove_fun
 [ "(ALL x:0.P(x)) <-> True",
   "(EX  x:0.P(x)) <-> False",
   "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
   "(EX  x:succ(i).P(x)) <-> P(i) | (EX  x:i.P(x))" ];

(** Tactics for type checking -- from CTT **)

fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
      not (is_Var (head_of a))
  | is_rigid_elem _ = false;

(*Try solving a:A by assumption provided a is rigid!*) 
val test_assume_tac = SUBGOAL(fn (prem,i) =>
    if is_rigid_elem (Logic.strip_assums_concl prem)
    then  assume_tac i  else  no_tac);

(*Type checking solves a:?A (a rigid, ?A maybe flexible).  
  match_tac is too strict; would refuse to instantiate ?A*)
fun typechk_step_tac tyrls =
    FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);

fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);

val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];

(*To instantiate variables in typing conditions; 
  to perform type checking faster than rewriting can
  NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
fun type_auto_tac tyrls hyps = SELECT_GOAL
    (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));

(** New version of mk_rew_rules **)

(*Should False yield False<->True, or should it solve goals some other way?*)

(*Analyse a rigid formula*)
val atomize_pairs =
  [("Ball",	[bspec]), 
   ("All",	[spec]),
   ("op -->",	[mp]),
   ("op &",	[conjunct1,conjunct2])];

(*Analyse a:b, where b is rigid*)
val atomize_mem_pairs = 
  [("Collect",	[CollectD1,CollectD2]),
   ("op -",	[DiffD1,DiffD2]),
   ("op Int",	[IntD1,IntD2])];

(*Analyse a theorem to atomic rewrite rules*)
fun atomize th = 
  let fun tryrules pairs t =
	  case head_of t of
	      Const(a,_) => 
		(case assoc(pairs,a) of
		     Some rls => flat (map atomize ([th] RL rls))
		   | None     => [th])
	    | _ => [th]
  in case concl_of th of (*The operator below is Trueprop*)
	_ $ (Const("op :",_) $ a $ b) => tryrules atomize_mem_pairs b
      | _ $ (Const("True",_)) => []	(*True is DELETED*)
      | _ $ (Const("False",_)) => []	(*should False do something??*)
      | _ $ A => tryrules atomize_pairs A

fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);

val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
		beta, eta, restrict, fst_conv, snd_conv, split];

(*Sigma_cong, Pi_cong NOT included by default since they cause
  flex-flex pairs and the "Check your prover" error -- because most
  Sigma's and Pi's are abbreviated as * or -> *)
val ZF_congs =
   [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];

val ZF_ss = FOL_ss 
      setmksimps ZF_mk_rew_rules
      addsimps (ZF_simps @ mem_simps @ bquant_simps)
      addcongs ZF_congs;