added class quantifiers
authorpaulson
Fri Jun 28 11:24:36 2002 +0200 (2002-06-28)
changeset 13253edbf32029d33
parent 13252 8c79a0dce4c0
child 13254 5146ccaedf42
added class quantifiers
src/ZF/OrdQuant.thy
     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.11 +header {*Special quantifiers*}
    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.49 +by (simp add: rall_def)
    1.50 +
    1.51 +lemma rspec: "[| ALL x[M]. P(x); M(x) |] ==> P(x)"
    1.52 +by (simp add: rall_def)
    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.64 +by (simp add: rall_def)
    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.69 +by (simp add: rall_def)
    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.89 +by (simp add: rex_def)
    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 +
   1.213 +Addsimprocs [defRALL_regroup,defREX_regroup]
   1.214 +
   1.215 +end;
   1.216 +*}
   1.217 +
   1.218  end