src/ZF/simpdata.ML
author lcp
Thu Mar 17 12:36:58 1994 +0100 (1994-03-17 ago)
changeset 279 7738aed3f84d
parent 14 1c0926788772
child 435 ca5356bd315a
permissions -rw-r--r--
Improved layout for inductive defs
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
lcp@14
    13
(*INCLUDED IN ZF_ss*)
lcp@6
    14
val mem_simps = map prove_fun
lcp@14
    15
 [ "a : 0             <-> False",
lcp@14
    16
   "a : A Un B        <-> a:A | a:B",
lcp@14
    17
   "a : A Int B       <-> a:A & a:B",
lcp@14
    18
   "a : A-B           <-> a:A & ~a:B",
clasohm@0
    19
   "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
lcp@14
    20
   "a : Collect(A,P)  <-> a:A & P(a)" ];
lcp@14
    21
lcp@14
    22
(*INCLUDED: should be??*)
lcp@14
    23
val bquant_simps = map prove_fun
lcp@14
    24
 [ "(ALL x:0.P(x)) <-> True",
lcp@14
    25
   "(EX  x:0.P(x)) <-> False",
lcp@14
    26
   "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
lcp@14
    27
   "(EX  x:succ(i).P(x)) <-> P(i) | (EX  x:i.P(x))" ];
clasohm@0
    28
clasohm@0
    29
(** Tactics for type checking -- from CTT **)
clasohm@0
    30
clasohm@0
    31
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
clasohm@0
    32
      not (is_Var (head_of a))
clasohm@0
    33
  | is_rigid_elem _ = false;
clasohm@0
    34
clasohm@0
    35
(*Try solving a:A by assumption provided a is rigid!*) 
clasohm@0
    36
val test_assume_tac = SUBGOAL(fn (prem,i) =>
clasohm@0
    37
    if is_rigid_elem (Logic.strip_assums_concl prem)
clasohm@0
    38
    then  assume_tac i  else  no_tac);
clasohm@0
    39
clasohm@0
    40
(*Type checking solves a:?A (a rigid, ?A maybe flexible).  
clasohm@0
    41
  match_tac is too strict; would refuse to instantiate ?A*)
clasohm@0
    42
fun typechk_step_tac tyrls =
clasohm@0
    43
    FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
clasohm@0
    44
clasohm@0
    45
fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
clasohm@0
    46
clasohm@0
    47
val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
clasohm@0
    48
clasohm@0
    49
(*To instantiate variables in typing conditions; 
clasohm@0
    50
  to perform type checking faster than rewriting can
clasohm@0
    51
  NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
clasohm@0
    52
fun type_auto_tac tyrls hyps = SELECT_GOAL
clasohm@0
    53
    (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
lcp@6
    54
           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
clasohm@0
    55
clasohm@0
    56
(** New version of mk_rew_rules **)
clasohm@0
    57
clasohm@0
    58
(*Should False yield False<->True, or should it solve goals some other way?*)
clasohm@0
    59
clasohm@0
    60
(*Analyse a rigid formula*)
clasohm@0
    61
val atomize_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*)
clasohm@0
    68
val atomize_mem_pairs = 
clasohm@0
    69
  [("Collect",	[CollectD1,CollectD2]),
clasohm@0
    70
   ("op -",	[DiffD1,DiffD2]),
clasohm@0
    71
   ("op Int",	[IntD1,IntD2])];
clasohm@0
    72
clasohm@0
    73
(*Analyse a theorem to atomic rewrite rules*)
clasohm@0
    74
fun atomize th = 
clasohm@0
    75
  let fun tryrules pairs t =
clasohm@0
    76
	  case head_of t of
clasohm@0
    77
	      Const(a,_) => 
clasohm@0
    78
		(case assoc(pairs,a) of
clasohm@0
    79
		     Some rls => flat (map atomize ([th] RL rls))
clasohm@0
    80
		   | None     => [th])
clasohm@0
    81
	    | _ => [th]
clasohm@0
    82
  in case concl_of th of (*The operator below is Trueprop*)
clasohm@0
    83
	_ $ (Const("op :",_) $ a $ b) => tryrules atomize_mem_pairs b
clasohm@0
    84
      | _ $ (Const("True",_)) => []	(*True is DELETED*)
clasohm@0
    85
      | _ $ (Const("False",_)) => []	(*should False do something??*)
clasohm@0
    86
      | _ $ A => tryrules atomize_pairs A
clasohm@0
    87
  end;
clasohm@0
    88
lcp@14
    89
val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
lcp@6
    90
		beta, eta, restrict, fst_conv, snd_conv, split];
clasohm@0
    91
lcp@6
    92
(*Sigma_cong, Pi_cong NOT included by default since they cause
lcp@6
    93
  flex-flex pairs and the "Check your prover" error -- because most
lcp@6
    94
  Sigma's and Pi's are abbreviated as * or -> *)
lcp@6
    95
val ZF_congs =
lcp@6
    96
   [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
clasohm@0
    97
lcp@6
    98
val ZF_ss = FOL_ss 
lcp@279
    99
      setmksimps (map mk_meta_eq o atomize o gen_all)
lcp@14
   100
      addsimps (ZF_simps @ mem_simps @ bquant_simps)
lcp@6
   101
      addcongs ZF_congs;