src/ZF/simpdata.ML
author lcp
Fri, 17 Sep 1993 16:16:38 +0200
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title:      ZF/simpdata
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Rewriting for ZF set theory -- based on FOL rewriting
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
fun prove_fun s = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
    (writeln s;  prove_goal ZF.thy s
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
       (fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    13
val mem_simps = map prove_fun
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
 [ "a:0 <-> False",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
   "a : A Un B <-> a:A | a:B",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
   "a : A Int B <-> a:A & a:B",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
   "a : A-B <-> a:A & ~a:B",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
   "a : cons(b,B) <-> a=b | a:B",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
   "i : succ(j) <-> i=j | i:j",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
   "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
   "a : Collect(A,P) <-> a:A & P(a)" ];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
(** Tactics for type checking -- from CTT **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
      not (is_Var (head_of a))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  | is_rigid_elem _ = false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
(*Try solving a:A by assumption provided a is rigid!*) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
val test_assume_tac = SUBGOAL(fn (prem,i) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
    if is_rigid_elem (Logic.strip_assums_concl prem)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
    then  assume_tac i  else  no_tac);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
(*Type checking solves a:?A (a rigid, ?A maybe flexible).  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  match_tac is too strict; would refuse to instantiate ?A*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
fun typechk_step_tac tyrls =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
    FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
(*To instantiate variables in typing conditions; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
  to perform type checking faster than rewriting can
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
fun type_auto_tac tyrls hyps = SELECT_GOAL
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
    (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    48
           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
(** New version of mk_rew_rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
(*Should False yield False<->True, or should it solve goals some other way?*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
(*Analyse a rigid formula*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
val atomize_pairs =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
  [("Ball",	[bspec]), 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
   ("All",	[spec]),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
   ("op -->",	[mp]),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
   ("op &",	[conjunct1,conjunct2])];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
(*Analyse a:b, where b is rigid*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
val atomize_mem_pairs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  [("Collect",	[CollectD1,CollectD2]),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
   ("op -",	[DiffD1,DiffD2]),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
   ("op Int",	[IntD1,IntD2])];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
(*Analyse a theorem to atomic rewrite rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
fun atomize th = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  let fun tryrules pairs t =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
	  case head_of t of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
	      Const(a,_) => 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
		(case assoc(pairs,a) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
		     Some rls => flat (map atomize ([th] RL rls))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
		   | None     => [th])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
	    | _ => [th]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  in case concl_of th of (*The operator below is Trueprop*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
	_ $ (Const("op :",_) $ a $ b) => tryrules atomize_mem_pairs b
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
      | _ $ (Const("True",_)) => []	(*True is DELETED*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
      | _ $ (Const("False",_)) => []	(*should False do something??*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
      | _ $ A => tryrules atomize_pairs A
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    83
fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    86
val ZF_simps = [empty_subsetI, ball_simp, if_true, if_false, 
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    87
		beta, eta, restrict, fst_conv, snd_conv, split];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    89
(*Sigma_cong, Pi_cong NOT included by default since they cause
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    90
  flex-flex pairs and the "Check your prover" error -- because most
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    91
  Sigma's and Pi's are abbreviated as * or -> *)
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    92
val ZF_congs =
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    93
   [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    95
val ZF_ss = FOL_ss 
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    96
      setmksimps ZF_mk_rew_rules
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    97
      addsimps (ZF_simps@mem_simps)
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    98
      addcongs ZF_congs;