src/ZF/OrdQuant.thy
 changeset 13253 edbf32029d33 parent 13244 7b37e218f298 child 13289 53e201efdaa2
```     1.1 --- a/src/ZF/OrdQuant.thy	Fri Jun 28 11:24:21 2002 +0200
1.2 +++ b/src/ZF/OrdQuant.thy	Fri Jun 28 11:24:36 2002 +0200
1.3 @@ -1,12 +1,14 @@
1.4  (*  Title:      ZF/AC/OrdQuant.thy
1.5      ID:         \$Id\$
1.6      Authors:    Krzysztof Grabczewski and L C Paulson
1.7 -
1.8 -Quantifiers and union operator for ordinals.
1.9  *)
1.10
1.12 +
1.13  theory OrdQuant = Ordinal:
1.14
1.15 +subsection {*Quantifiers and union operator for ordinals*}
1.16 +
1.17  constdefs
1.18
1.19    (* Ordinal Quantifiers *)
1.20 @@ -185,6 +187,142 @@
1.21  apply (erule Ord_induct, assumption, blast)
1.22  done
1.23
1.24 +
1.25 +subsection {*Quantification over a class*}
1.26 +
1.27 +constdefs
1.28 +  "rall"     :: "[i=>o, i=>o] => o"
1.29 +    "rall(M, P) == ALL x. M(x) --> P(x)"
1.30 +
1.31 +  "rex"      :: "[i=>o, i=>o] => o"
1.32 +    "rex(M, P) == EX x. M(x) & P(x)"
1.33 +
1.34 +syntax
1.35 +  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3ALL _[_]./ _)" 10)
1.36 +  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3EX _[_]./ _)" 10)
1.37 +
1.38 +syntax (xsymbols)
1.39 +  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
1.40 +  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
1.41 +
1.42 +translations
1.43 +  "ALL x[M]. P"  == "rall(M, %x. P)"
1.44 +  "EX x[M]. P"   == "rex(M, %x. P)"
1.45 +
1.46 +(*** Relativized universal quantifier ***)
1.47 +
1.48 +lemma rallI [intro!]: "[| !!x. M(x) ==> P(x) |] ==> ALL x[M]. P(x)"
1.50 +
1.51 +lemma rspec: "[| ALL x[M]. P(x); M(x) |] ==> P(x)"
1.53 +
1.54 +(*Instantiates x first: better for automatic theorem proving?*)
1.55 +lemma rev_rallE [elim]:
1.56 +    "[| ALL x[M]. P(x);  ~ M(x) ==> Q;  P(x) ==> Q |] ==> Q"
1.57 +by (simp add: rall_def, blast)
1.58 +
1.59 +lemma rallE: "[| ALL x[M]. P(x);  P(x) ==> Q;  ~ M(x) ==> Q |] ==> Q"
1.60 +by blast
1.61 +
1.62 +(*Trival rewrite rule;   (ALL x[M].P)<->P holds only if A is nonempty!*)
1.63 +lemma rall_triv [simp]: "(ALL x[M]. P) <-> ((EX x. M(x)) --> P)"
1.65 +
1.66 +(*Congruence rule for rewriting*)
1.67 +lemma rall_cong [cong]:
1.68 +    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> rall(M,P) <-> rall(M,P')"
1.70 +
1.71 +(*** Relativized existential quantifier ***)
1.72 +
1.73 +lemma rexI [intro]: "[| P(x); M(x) |] ==> EX x[M]. P(x)"
1.74 +by (simp add: rex_def, blast)
1.75 +
1.76 +(*The best argument order when there is only one M(x)*)
1.77 +lemma rev_rexI: "[| M(x);  P(x) |] ==> EX x[M]. P(x)"
1.78 +by blast
1.79 +
1.80 +(*Not of the general form for such rules; ~EX has become ALL~ *)
1.81 +lemma rexCI: "[| ALL x[M]. ~P(x) ==> P(a); M(a) |] ==> EX x[M]. P(x)"
1.82 +by blast
1.83 +
1.84 +lemma rexE [elim!]: "[| EX x[M]. P(x);  !!x. [| M(x); P(x) |] ==> Q |] ==> Q"
1.85 +by (simp add: rex_def, blast)
1.86 +
1.87 +(*We do not even have (EX x[M]. True) <-> True unless A is nonempty!!*)
1.88 +lemma rex_triv [simp]: "(EX x[M]. P) <-> ((EX x. M(x)) & P)"
1.90 +
1.91 +lemma rex_cong [cong]:
1.92 +    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> rex(M,P) <-> rex(M,P')"
1.93 +by (simp add: rex_def cong: conj_cong)
1.94 +
1.95 +lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (ALL x[M]. P(x))";
1.96 +by (simp add: rall_def atomize_all atomize_imp)
1.97 +
1.98 +declare atomize_rall [symmetric, rulify]
1.99 +
1.100 +lemma rall_simps1:
1.101 +     "(ALL x[M]. P(x) & Q)   <-> (ALL x[M]. P(x)) & ((ALL x[M]. False) | Q)"
1.102 +     "(ALL x[M]. P(x) | Q)   <-> ((ALL x[M]. P(x)) | Q)"
1.103 +     "(ALL x[M]. P(x) --> Q) <-> ((EX x[M]. P(x)) --> Q)"
1.104 +     "(~(ALL x[M]. P(x))) <-> (EX x[M]. ~P(x))"
1.105 +by blast+
1.106 +
1.107 +lemma rall_simps2:
1.108 +     "(ALL x[M]. P & Q(x))   <-> ((ALL x[M]. False) | P) & (ALL x[M]. Q(x))"
1.109 +     "(ALL x[M]. P | Q(x))   <-> (P | (ALL x[M]. Q(x)))"
1.110 +     "(ALL x[M]. P --> Q(x)) <-> (P --> (ALL x[M]. Q(x)))"
1.111 +by blast+
1.112 +
1.113 +lemmas rall_simps = rall_simps1 rall_simps2
1.114 +
1.115 +lemma rall_conj_distrib:
1.116 +    "(ALL x[M]. P(x) & Q(x)) <-> ((ALL x[M]. P(x)) & (ALL x[M]. Q(x)))"
1.117 +by blast
1.118 +
1.119 +lemma rex_simps1:
1.120 +     "(EX x[M]. P(x) & Q) <-> ((EX x[M]. P(x)) & Q)"
1.121 +     "(EX x[M]. P(x) | Q) <-> (EX x[M]. P(x)) | ((EX x[M]. True) & Q)"
1.122 +     "(EX x[M]. P(x) --> Q) <-> ((ALL x[M]. P(x)) --> ((EX x[M]. True) & Q))"
1.123 +     "(~(EX x[M]. P(x))) <-> (ALL x[M]. ~P(x))"
1.124 +by blast+
1.125 +
1.126 +lemma rex_simps2:
1.127 +     "(EX x[M]. P & Q(x)) <-> (P & (EX x[M]. Q(x)))"
1.128 +     "(EX x[M]. P | Q(x)) <-> ((EX x[M]. True) & P) | (EX x[M]. Q(x))"
1.129 +     "(EX x[M]. P --> Q(x)) <-> (((ALL x[M]. False) | P) --> (EX x[M]. Q(x)))"
1.130 +by blast+
1.131 +
1.132 +lemmas rex_simps = rex_simps1 rex_simps2
1.133 +
1.134 +lemma rex_disj_distrib:
1.135 +    "(EX x[M]. P(x) | Q(x)) <-> ((EX x[M]. P(x)) | (EX x[M]. Q(x)))"
1.136 +by blast
1.137 +
1.138 +
1.139 +(** One-point rule for bounded quantifiers: see HOL/Set.ML **)
1.140 +
1.141 +lemma rex_triv_one_point1 [simp]: "(EX x[M]. x=a) <-> ( M(a))"
1.142 +by blast
1.143 +
1.144 +lemma rex_triv_one_point2 [simp]: "(EX x[M]. a=x) <-> ( M(a))"
1.145 +by blast
1.146 +
1.147 +lemma rex_one_point1 [simp]: "(EX x[M]. x=a & P(x)) <-> ( M(a) & P(a))"
1.148 +by blast
1.149 +
1.150 +lemma rex_one_point2 [simp]: "(EX x[M]. a=x & P(x)) <-> ( M(a) & P(a))"
1.151 +by blast
1.152 +
1.153 +lemma rall_one_point1 [simp]: "(ALL x[M]. x=a --> P(x)) <-> ( M(a) --> P(a))"
1.154 +by blast
1.155 +
1.156 +lemma rall_one_point2 [simp]: "(ALL x[M]. a=x --> P(x)) <-> ( M(a) --> P(a))"
1.157 +by blast
1.158 +
1.159 +
1.160  ML
1.161  {*
1.162  val oall_def = thm "oall_def"
1.163 @@ -207,9 +345,54 @@
1.164  val OUN_cong = thm "OUN_cong";
1.165  val lt_induct = thm "lt_induct";
1.166
1.167 +val rall_def = thm "rall_def"
1.168 +val rex_def = thm "rex_def"
1.169 +
1.170 +val rallI = thm "rallI";
1.171 +val rspec = thm "rspec";
1.172 +val rallE = thm "rallE";
1.173 +val rev_oallE = thm "rev_oallE";
1.174 +val rall_cong = thm "rall_cong";
1.175 +val rexI = thm "rexI";
1.176 +val rexCI = thm "rexCI";
1.177 +val rexE = thm "rexE";
1.178 +val rex_cong = thm "rex_cong";
1.179 +
1.180  val Ord_atomize =
1.181 -    atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
1.182 +    atomize ([("OrdQuant.oall", [ospec]),("OrdQuant.rall", [rspec])]@
1.183 +                 ZF_conn_pairs,
1.184 +             ZF_mem_pairs);
1.185  simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
1.186  *}
1.187
1.188 +text{*Setting up the one-point-rule simproc*}
1.189 +ML
1.190 +{*
1.191 +
1.192 +let
1.193 +val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
1.194 +                                ("EX x[M]. P(x) & Q(x)", FOLogic.oT)
1.195 +
1.196 +val prove_rex_tac = rewtac rex_def THEN
1.197 +                    Quantifier1.prove_one_point_ex_tac;
1.198 +
1.199 +val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
1.200 +
1.201 +val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
1.202 +                                 ("ALL x[M]. P(x) --> Q(x)", FOLogic.oT)
1.203 +
1.204 +val prove_rall_tac = rewtac rall_def THEN
1.205 +                     Quantifier1.prove_one_point_all_tac;
1.206 +
1.207 +val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
1.208 +
1.209 +val defREX_regroup = mk_simproc "defined REX" [ex_pattern] rearrange_bex;
1.210 +val defRALL_regroup = mk_simproc "defined RALL" [all_pattern] rearrange_ball;
1.211 +in
1.212 +