src/ZF/OrdQuant.ML
author wenzelm
Sat Jan 12 16:37:58 2002 +0100 (2002-01-12 ago)
changeset 12725 7ede865e1fe5
parent 12720 f8a134b9a57f
permissions -rw-r--r--
renamed forall_elim_vars_safe to gen_all;
wenzelm@9907
     1
(*  Title:      ZF/OrdQuant.ML
paulson@2469
     2
    ID:         $Id$
paulson@2469
     3
    Authors:    Krzysztof Grabczewski and L C Paulson
paulson@2469
     4
paulson@2469
     5
Quantifiers and union operator for ordinals. 
paulson@2469
     6
*)
paulson@2469
     7
paulson@12620
     8
val oall_def = thm "oall_def";
paulson@12620
     9
val oex_def = thm "oex_def"; 
paulson@12620
    10
val OUnion_def = thm "OUnion_def";
paulson@12620
    11
paulson@2469
    12
(*** universal quantifier for ordinals ***)
paulson@2469
    13
paulson@9211
    14
val prems = Goalw [oall_def] 
paulson@9211
    15
    "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)";
paulson@9211
    16
by (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ;
paulson@9211
    17
qed "oallI";
paulson@2469
    18
paulson@9211
    19
Goalw [oall_def] "[| ALL x<A. P(x);  x<A |] ==> P(x)";
paulson@9211
    20
by (etac (spec RS mp) 1);
paulson@9211
    21
by (assume_tac 1) ;
paulson@9211
    22
qed "ospec";
paulson@2469
    23
paulson@9211
    24
val major::prems = Goalw [oall_def] 
paulson@9211
    25
    "[| ALL x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q";
paulson@9211
    26
by (rtac (major RS allE) 1);
paulson@9211
    27
by (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ;
paulson@9211
    28
qed "oallE";
paulson@2469
    29
paulson@9211
    30
val major::prems = Goal
paulson@9180
    31
    "[| ALL x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q";
paulson@9180
    32
by (rtac (major RS oallE) 1);
paulson@9180
    33
by (REPEAT (eresolve_tac prems 1)) ;
paulson@9180
    34
qed "rev_oallE";
paulson@2469
    35
paulson@2469
    36
(*Trival rewrite rule;   (ALL x<a.P)<->P holds only if a is not 0!*)
paulson@9180
    37
Goal "(ALL x<a. True) <-> True";
paulson@9180
    38
by (REPEAT (ares_tac [TrueI,oallI,iffI] 1)) ;
paulson@9180
    39
qed "oall_simp";
paulson@2469
    40
paulson@2469
    41
(*Congruence rule for rewriting*)
paulson@9211
    42
val prems = Goalw [oall_def] 
paulson@9211
    43
    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')";
paulson@9211
    44
by (simp_tac (simpset() addsimps prems) 1) ;
paulson@9211
    45
qed "oall_cong";
paulson@2469
    46
paulson@2469
    47
paulson@2469
    48
(*** existential quantifier for ordinals ***)
paulson@2469
    49
paulson@9211
    50
val prems = Goalw [oex_def] 
paulson@9211
    51
    "[| P(x);  x<A |] ==> EX x<A. P(x)";
paulson@9211
    52
by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ;
paulson@9211
    53
qed "oexI";
paulson@2469
    54
paulson@2469
    55
(*Not of the general form for such rules; ~EX has become ALL~ *)
paulson@9180
    56
val prems = Goal
paulson@9180
    57
   "[| ALL x<A. ~P(x) ==> P(a);  a<A |] ==> EX x<A. P(x)";
paulson@9180
    58
by (rtac classical 1);
paulson@9180
    59
by (REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ;
paulson@9180
    60
qed "oexCI";
paulson@2469
    61
paulson@9211
    62
val major::prems = Goalw [oex_def] 
paulson@2469
    63
    "[| EX x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q \
paulson@9211
    64
\    |] ==> Q";
paulson@9211
    65
by (rtac (major RS exE) 1);
paulson@9211
    66
by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ;
paulson@9211
    67
qed "oexE";
paulson@2469
    68
paulson@9211
    69
val prems = Goalw [oex_def] 
paulson@2469
    70
    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) \
paulson@9211
    71
\    |] ==> oex(a,P) <-> oex(a',P')";
paulson@9211
    72
by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1) ;
paulson@9211
    73
qed "oex_cong";
paulson@2469
    74
paulson@2469
    75
paulson@2469
    76
(*** Rules for Ordinal-Indexed Unions ***)
paulson@2469
    77
paulson@9211
    78
Goalw [OUnion_def] "[| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))";
paulson@9211
    79
by (blast_tac (claset() addSEs [ltE]) 1);
paulson@9211
    80
qed "OUN_I";
paulson@2469
    81
paulson@9211
    82
val major::prems = Goalw [OUnion_def] 
paulson@9211
    83
    "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R";
paulson@9211
    84
by (rtac (major RS CollectE) 1);
paulson@9211
    85
by (rtac UN_E 1);
paulson@9211
    86
by (REPEAT (ares_tac (ltI::prems) 1)) ;
paulson@9211
    87
qed "OUN_E";
paulson@2469
    88
paulson@9211
    89
Goalw [oex_def] "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))";
paulson@9211
    90
by (fast_tac (claset() addIs [OUN_I] addSEs [OUN_E]) 1) ;
paulson@9211
    91
qed "OUN_iff";
paulson@2469
    92
paulson@9180
    93
val prems = Goal
paulson@9180
    94
    "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))";
paulson@9180
    95
by (rtac equality_iffI 1);
paulson@9180
    96
by (simp_tac (simpset() addcongs [oex_cong] addsimps OUN_iff::prems) 1) ;
paulson@9180
    97
qed "OUN_cong";
paulson@2469
    98
paulson@2469
    99
AddSIs [oallI];
paulson@2469
   100
AddIs  [oexI, OUN_I];
paulson@2469
   101
AddSEs [oexE, OUN_E];
paulson@2469
   102
AddEs  [rev_oallE];
paulson@2469
   103
wenzelm@9907
   104
val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
paulson@2469
   105
wenzelm@12725
   106
simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
paulson@2469
   107
                        addsimps [oall_simp, ltD RS beta]
paulson@2469
   108
                        addcongs [oall_cong, oex_cong, OUN_cong];
paulson@2469
   109
paulson@9180
   110
val major::prems = Goalw [lt_def, oall_def]
paulson@2469
   111
    "[| i<k;  !!x.[| x<k;  ALL y<x. P(y) |] ==> P(x) \
paulson@2469
   112
\    |]  ==>  P(i)";
paulson@2469
   113
by (rtac (major RS conjE) 1);
paulson@2469
   114
by (etac Ord_induct 1 THEN assume_tac 1);
wenzelm@4091
   115
by (fast_tac (claset() addIs prems) 1);
paulson@2469
   116
qed "lt_induct";