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