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