src/ZF/simpdata.ML
author lcp
Tue, 12 Jul 1994 18:05:03 +0200
changeset 467 92868dab2939
parent 435 ca5356bd315a
child 485 5e00a676a211
permissions -rw-r--r--
new cardinal arithmetic developments
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
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    13
(*INCLUDED IN ZF_ss*)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    14
val mem_simps = map prove_fun
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    15
 [ "a : 0             <-> False",
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    16
   "a : A Un B        <-> a:A | a:B",
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    17
   "a : A Int B       <-> a:A & a:B",
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    18
   "a : A-B           <-> a:A & ~a:B",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
   "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    20
   "a : Collect(A,P)  <-> a:A & P(a)" ];
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    21
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 435
diff changeset
    22
goal ZF.thy "{x.x:A} = A";
92868dab2939 new cardinal arithmetic developments
lcp
parents: 435
diff changeset
    23
by (fast_tac eq_cs 1);
92868dab2939 new cardinal arithmetic developments
lcp
parents: 435
diff changeset
    24
val triv_RepFun = result();
92868dab2939 new cardinal arithmetic developments
lcp
parents: 435
diff changeset
    25
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    26
(*INCLUDED: should be??*)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    27
val bquant_simps = map prove_fun
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    28
 [ "(ALL x:0.P(x)) <-> True",
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    29
   "(EX  x:0.P(x)) <-> False",
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    30
   "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    31
   "(EX  x:succ(i).P(x)) <-> P(i) | (EX  x:i.P(x))" ];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
(** Tactics for type checking -- from CTT **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
      not (is_Var (head_of a))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  | is_rigid_elem _ = false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
(*Try solving a:A by assumption provided a is rigid!*) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
val test_assume_tac = SUBGOAL(fn (prem,i) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
    if is_rigid_elem (Logic.strip_assums_concl prem)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
    then  assume_tac i  else  no_tac);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
(*Type checking solves a:?A (a rigid, ?A maybe flexible).  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  match_tac is too strict; would refuse to instantiate ?A*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
fun typechk_step_tac tyrls =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
    FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
(*To instantiate variables in typing conditions; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
  to perform type checking faster than rewriting can
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
  NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
fun type_auto_tac tyrls hyps = SELECT_GOAL
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
    (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
    58
           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
(** New version of mk_rew_rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
(*Should False yield False<->True, or should it solve goals some other way?*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
(*Analyse a rigid formula*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val atomize_pairs =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
  [("Ball",	[bspec]), 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
   ("All",	[spec]),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
   ("op -->",	[mp]),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
   ("op &",	[conjunct1,conjunct2])];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
(*Analyse a:b, where b is rigid*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
val atomize_mem_pairs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
  [("Collect",	[CollectD1,CollectD2]),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
   ("op -",	[DiffD1,DiffD2]),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
   ("op Int",	[IntD1,IntD2])];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
(*Analyse a theorem to atomic rewrite rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
fun atomize th = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
  let fun tryrules pairs t =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
	  case head_of t of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
	      Const(a,_) => 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
		(case assoc(pairs,a) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
		     Some rls => flat (map atomize ([th] RL rls))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
		   | None     => [th])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
	    | _ => [th]
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    86
  in case concl_of th of 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    87
       Const("Trueprop",_) $ P => 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    88
	  (case P of
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    89
	       Const("op :",_) $ a $ b => tryrules atomize_mem_pairs b
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    90
	     | Const("True",_)         => []
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    91
	     | Const("False",_)        => []
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    92
	     | A => tryrules atomize_pairs A)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    93
     | _                       => [th]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    96
val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 435
diff changeset
    97
		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff,
92868dab2939 new cardinal arithmetic developments
lcp
parents: 435
diff changeset
    98
		triv_RepFun];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   100
(*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
   101
  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
   102
  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
   103
val ZF_congs =
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   104
   [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   106
val ZF_ss = FOL_ss 
279
7738aed3f84d Improved layout for inductive defs
lcp
parents: 14
diff changeset
   107
      setmksimps (map mk_meta_eq o atomize o gen_all)
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   108
      addsimps (ZF_simps @ mem_simps @ bquant_simps)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   109
      addcongs ZF_congs;