src/ZF/OrdQuant.thy
 changeset 13169 394a6c649547 parent 13162 660a71e712af child 13170 9e23faed6c97
```     1.1 --- a/src/ZF/OrdQuant.thy	Tue May 21 13:06:36 2002 +0200
1.2 +++ b/src/ZF/OrdQuant.thy	Tue May 21 18:25:28 2002 +0200
1.3 @@ -39,8 +39,8 @@
1.4  (** simplification of the new quantifiers **)
1.5
1.6
1.7 -(*MOST IMPORTANT that this is added to the simpset BEFORE OrdQuant.ML
1.8 -  is loaded: it's Ord_atomize would convert this rule to
1.9 +(*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize
1.10 +  is proved.  Ord_atomize would convert this rule to
1.11      x < 0 ==> P(x) == True, which causes dire effects!*)
1.12  lemma [simp]: "(ALL x<0. P(x))"
1.14 @@ -199,4 +199,124 @@
1.15       "(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))"
1.16  by (simp add: oall_def atomize_all atomize_imp)
1.17
1.18 +(*** universal quantifier for ordinals ***)
1.19 +
1.20 +lemma oallI [intro!]:
1.21 +    "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"
1.23 +
1.24 +lemma ospec: "[| ALL x<A. P(x);  x<A |] ==> P(x)"
1.26 +
1.27 +lemma oallE:
1.28 +    "[| ALL x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q"
1.30 +apply (blast intro: elim:);
1.31 +done
1.32 +
1.33 +lemma rev_oallE [elim]:
1.34 +    "[| ALL x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q"
1.36 +apply (blast intro: elim:);
1.37 +done
1.38 +
1.39 +
1.40 +(*Trival rewrite rule;   (ALL x<a.P)<->P holds only if a is not 0!*)
1.41 +lemma oall_simp [simp]: "(ALL x<a. True) <-> True"
1.42 +apply (blast intro: elim:);
1.43 +done
1.44 +
1.45 +(*Congruence rule for rewriting*)
1.46 +lemma oall_cong [cong]:
1.47 +    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')"
1.49 +
1.50 +
1.51 +(*** existential quantifier for ordinals ***)
1.52 +
1.53 +lemma oexI [intro]:
1.54 +    "[| P(x);  x<A |] ==> EX x<A. P(x)"
1.56 +apply (blast intro: elim:);
1.57 +done
1.58 +
1.59 +(*Not of the general form for such rules; ~EX has become ALL~ *)
1.60 +lemma oexCI:
1.61 +   "[| ALL x<A. ~P(x) ==> P(a);  a<A |] ==> EX x<A. P(x)"
1.63 +apply (blast intro: elim:);
1.64 +done
1.65 +
1.66 +lemma oexE [elim!]:
1.67 +    "[| EX x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q |] ==> Q"
1.69 +apply (blast intro: elim:);
1.70 +done
1.71 +
1.72 +lemma oex_cong [cong]:
1.73 +    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oex(a,P) <-> oex(a',P')"
1.75 +done
1.76 +
1.77 +
1.78 +(*** Rules for Ordinal-Indexed Unions ***)
1.79 +
1.80 +lemma OUN_I [intro]: "[| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))"
1.81 +apply (unfold OUnion_def lt_def)
1.82 +apply (blast)
1.83 +done
1.84 +
1.85 +lemma OUN_E [elim!]:
1.86 +    "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
1.87 +apply (unfold OUnion_def lt_def)
1.88 +apply (blast)
1.89 +done
1.90 +
1.91 +lemma OUN_iff: "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
1.92 +apply (unfold OUnion_def oex_def lt_def)
1.93 +apply (blast intro: elim:);
1.94 +done
1.95 +
1.96 +lemma OUN_cong [cong]:
1.97 +    "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
1.98 +by (simp add: OUnion_def lt_def OUN_iff)
1.99 +
1.100 +declare ltD [THEN beta, simp]
1.101 +
1.102 +
1.103 +lemma lt_induct:
1.104 +    "[| i<k;  !!x.[| x<k;  ALL y<x. P(y) |] ==> P(x) |]  ==>  P(i)"
1.105 +apply (simp add: lt_def oall_def)
1.106 +apply (erule conjE)
1.107 +apply (erule Ord_induct, assumption)
1.108 +apply (blast intro: elim:);
1.109 +done
1.110 +
1.111 +ML
1.112 +{*
1.113 +val oall_def = thm "oall_def"
1.114 +val oex_def = thm "oex_def"
1.115 +val OUnion_def = thm "OUnion_def"
1.116 +
1.117 +val oallI = thm "oallI";
1.118 +val ospec = thm "ospec";
1.119 +val oallE = thm "oallE";
1.120 +val rev_oallE = thm "rev_oallE";
1.121 +val oall_simp = thm "oall_simp";
1.122 +val oall_cong = thm "oall_cong";
1.123 +val oexI = thm "oexI";
1.124 +val oexCI = thm "oexCI";
1.125 +val oexE = thm "oexE";
1.126 +val oex_cong = thm "oex_cong";
1.127 +val OUN_I = thm "OUN_I";
1.128 +val OUN_E = thm "OUN_E";
1.129 +val OUN_iff = thm "OUN_iff";
1.130 +val OUN_cong = thm "OUN_cong";
1.131 +val lt_induct = thm "lt_induct";
1.132 +
1.133 +val Ord_atomize =
1.134 +    atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
1.135 +simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
1.136 +*}
1.137 +
1.138  end
```