src/HOL/Hilbert_Choice.thy
changeset 12298 b344486c33e2
parent 12023 d982f98e0f0d
child 12372 cd3a09c7dac9
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Nov 26 18:33:21 2001 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Nov 26 18:33:57 2001 +0100
     1.3 @@ -9,199 +9,247 @@
     1.4  theory Hilbert_Choice = NatArith
     1.5  files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
     1.6  
     1.7 +
     1.8 +subsection {* Hilbert's epsilon *}
     1.9 +
    1.10  consts
    1.11    Eps           :: "('a => bool) => 'a"
    1.12  
    1.13 -
    1.14  syntax (input)
    1.15 -  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\<epsilon>_./ _)" [0, 10] 10)
    1.16 -
    1.17 +  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<epsilon>_./ _)" [0, 10] 10)
    1.18  syntax (HOL)
    1.19 -  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
    1.20 -
    1.21 +  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3@ _./ _)" [0, 10] 10)
    1.22  syntax
    1.23 -  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3SOME _./ _)" [0, 10] 10)
    1.24 -
    1.25 +  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
    1.26  translations
    1.27 -  "SOME x. P"             == "Eps (%x. P)"
    1.28 +  "SOME x. P" == "Eps (%x. P)"
    1.29  
    1.30 -axioms  
    1.31 -  someI:        "P (x::'a) ==> P (SOME x. P x)"
    1.32 +axioms
    1.33 +  someI: "P (x::'a) ==> P (SOME x. P x)"
    1.34  
    1.35  
    1.36 -(*used in TFL*)
    1.37 -lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    1.38 -  by (blast intro: someI)
    1.39 -
    1.40 +constdefs
    1.41 +  inv :: "('a => 'b) => ('b => 'a)"
    1.42 +  "inv(f :: 'a => 'b) == %y. SOME x. f x = y"
    1.43  
    1.44 -constdefs  
    1.45 -  inv :: "('a => 'b) => ('b => 'a)"
    1.46 -    "inv(f::'a=>'b) == % y. @x. f(x)=y"
    1.47 -
    1.48 -  Inv :: "['a set, 'a => 'b] => ('b => 'a)"
    1.49 -    "Inv A f == (% x. (@ y. y : A & f y = x))"
    1.50 +  Inv :: "'a set => ('a => 'b) => ('b => 'a)"
    1.51 +  "Inv A f == %x. SOME y. y : A & f y = x"
    1.52  
    1.53  
    1.54  use "Hilbert_Choice_lemmas.ML"
    1.55  
    1.56 +lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    1.57 +  -- {* dynamically-scoped fact for TFL *}
    1.58 +  by (blast intro: someI)
    1.59  
    1.60 -(** Least value operator **)
    1.61 +
    1.62 +subsection {* Least value operator *}
    1.63  
    1.64  constdefs
    1.65 -  LeastM   :: "['a => 'b::ord, 'a => bool] => 'a"
    1.66 -              "LeastM m P == @x. P x & (ALL y. P y --> m x <= m y)"
    1.67 +  LeastM :: "['a => 'b::ord, 'a => bool] => 'a"
    1.68 +  "LeastM m P == SOME x. P x & (ALL y. P y --> m x <= m y)"
    1.69  
    1.70  syntax
    1.71 - "@LeastM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0,4,10]10)
    1.72 -
    1.73 +  "_LeastM" :: "[pttrn, 'a => 'b::ord, bool] => 'a"    ("LEAST _ WRT _. _" [0, 4, 10] 10)
    1.74  translations
    1.75 -                "LEAST x WRT m. P" == "LeastM m (%x. P)"
    1.76 +  "LEAST x WRT m. P" == "LeastM m (%x. P)"
    1.77  
    1.78  lemma LeastMI2:
    1.79 -  "[| P x; !!y. P y ==> m x <= m y;
    1.80 -           !!x. [| P x; \<forall>y. P y --> m x \<le> m y |] ==> Q x |]
    1.81 -   ==> Q (LeastM m P)";
    1.82 -apply (unfold LeastM_def)
    1.83 -apply (rule someI2_ex)
    1.84 -apply  blast
    1.85 -apply blast
    1.86 -done
    1.87 +  "P x ==> (!!y. P y ==> m x <= m y)
    1.88 +    ==> (!!x. P x ==> \<forall>y. P y --> m x \<le> m y ==> Q x)
    1.89 +    ==> Q (LeastM m P)"
    1.90 +  apply (unfold LeastM_def)
    1.91 +  apply (rule someI2_ex)
    1.92 +   apply blast
    1.93 +  apply blast
    1.94 +  done
    1.95  
    1.96  lemma LeastM_equality:
    1.97 - "[| P k; !!x. P x ==> m k <= m x |] ==> m (LEAST x WRT m. P x) = 
    1.98 -     (m k::'a::order)";
    1.99 -apply (rule LeastMI2)
   1.100 -apply   assumption
   1.101 -apply  blast
   1.102 -apply (blast intro!: order_antisym) 
   1.103 -done
   1.104 +  "P k ==> (!!x. P x ==> m k <= m x)
   1.105 +    ==> m (LEAST x WRT m. P x) = (m k::'a::order)"
   1.106 +  apply (rule LeastMI2)
   1.107 +    apply assumption
   1.108 +   apply blast
   1.109 +  apply (blast intro!: order_antisym)
   1.110 +  done
   1.111  
   1.112  lemma wf_linord_ex_has_least:
   1.113 -     "[|wf r;  ALL x y. ((x,y):r^+) = ((y,x)~:r^*);  P k|]  \
   1.114 -\     ==> EX x. P x & (!y. P y --> (m x,m y):r^*)" 
   1.115 -apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
   1.116 -apply (drule_tac x = "m`Collect P" in spec)
   1.117 -apply force
   1.118 -done
   1.119 +  "wf r ==> ALL x y. ((x,y):r^+) = ((y,x)~:r^*) ==> P k
   1.120 +    ==> EX x. P x & (!y. P y --> (m x,m y):r^*)"
   1.121 +  apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
   1.122 +  apply (drule_tac x = "m`Collect P" in spec)
   1.123 +  apply force
   1.124 +  done
   1.125  
   1.126 -(* successor of obsolete nonempty_has_least *)
   1.127  lemma ex_has_least_nat:
   1.128 -     "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
   1.129 -apply (simp only: pred_nat_trancl_eq_le [symmetric])
   1.130 -apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
   1.131 -apply (simp (no_asm) add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
   1.132 -apply assumption
   1.133 -done
   1.134 +    "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
   1.135 +  apply (simp only: pred_nat_trancl_eq_le [symmetric])
   1.136 +  apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
   1.137 +   apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
   1.138 +  apply assumption
   1.139 +  done
   1.140  
   1.141 -lemma LeastM_nat_lemma: 
   1.142 -  "P k ==> P (LeastM m P) & (ALL y. P y --> m (LeastM m P) <= (m y::nat))"
   1.143 -apply (unfold LeastM_def)
   1.144 -apply (rule someI_ex)
   1.145 -apply (erule ex_has_least_nat)
   1.146 -done
   1.147 +lemma LeastM_nat_lemma:
   1.148 +    "P k ==> P (LeastM m P) & (ALL y. P y --> m (LeastM m P) <= (m y::nat))"
   1.149 +  apply (unfold LeastM_def)
   1.150 +  apply (rule someI_ex)
   1.151 +  apply (erule ex_has_least_nat)
   1.152 +  done
   1.153  
   1.154  lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
   1.155  
   1.156  lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
   1.157 -apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
   1.158 -apply assumption
   1.159 -apply assumption
   1.160 -done
   1.161 +  apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
   1.162 +   apply assumption
   1.163 +  apply assumption
   1.164 +  done
   1.165  
   1.166  
   1.167 -(** Greatest value operator **)
   1.168 +subsection {* Greatest value operator *}
   1.169  
   1.170  constdefs
   1.171 -  GreatestM   :: "['a => 'b::ord, 'a => bool] => 'a"
   1.172 -              "GreatestM m P == @x. P x & (ALL y. P y --> m y <= m x)"
   1.173 -  
   1.174 -  Greatest    :: "('a::ord => bool) => 'a"         (binder "GREATEST " 10)
   1.175 -              "Greatest     == GreatestM (%x. x)"
   1.176 +  GreatestM :: "['a => 'b::ord, 'a => bool] => 'a"
   1.177 +  "GreatestM m P == SOME x. P x & (ALL y. P y --> m y <= m x)"
   1.178 +
   1.179 +  Greatest :: "('a::ord => bool) => 'a"    (binder "GREATEST " 10)
   1.180 +  "Greatest == GreatestM (%x. x)"
   1.181  
   1.182  syntax
   1.183 - "@GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
   1.184 -                                        ("GREATEST _ WRT _. _" [0,4,10]10)
   1.185 +  "_GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
   1.186 +      ("GREATEST _ WRT _. _" [0, 4, 10] 10)
   1.187  
   1.188  translations
   1.189 -              "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
   1.190 +  "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
   1.191  
   1.192  lemma GreatestMI2:
   1.193 -     "[| P x;
   1.194 -	 !!y. P y ==> m y <= m x;
   1.195 -         !!x. [| P x; \<forall>y. P y --> m y \<le> m x |] ==> Q x |]
   1.196 -      ==> Q (GreatestM m P)";
   1.197 -apply (unfold GreatestM_def)
   1.198 -apply (rule someI2_ex)
   1.199 -apply  blast
   1.200 -apply blast
   1.201 -done
   1.202 +  "P x ==> (!!y. P y ==> m y <= m x)
   1.203 +    ==> (!!x. P x ==> \<forall>y. P y --> m y \<le> m x ==> Q x)
   1.204 +    ==> Q (GreatestM m P)"
   1.205 +  apply (unfold GreatestM_def)
   1.206 +  apply (rule someI2_ex)
   1.207 +   apply blast
   1.208 +  apply blast
   1.209 +  done
   1.210  
   1.211  lemma GreatestM_equality:
   1.212 - "[| P k;  !!x. P x ==> m x <= m k |]
   1.213 -  ==> m (GREATEST x WRT m. P x) = (m k::'a::order)";
   1.214 -apply (rule_tac m=m in GreatestMI2)
   1.215 -apply   assumption
   1.216 -apply  blast
   1.217 -apply (blast intro!: order_antisym) 
   1.218 -done
   1.219 + "P k ==> (!!x. P x ==> m x <= m k)
   1.220 +    ==> m (GREATEST x WRT m. P x) = (m k::'a::order)"
   1.221 +  apply (rule_tac m = m in GreatestMI2)
   1.222 +    apply assumption
   1.223 +   apply blast
   1.224 +  apply (blast intro!: order_antisym)
   1.225 +  done
   1.226  
   1.227  lemma Greatest_equality:
   1.228 -  "[| P (k::'a::order); !!x. P x ==> x <= k |] ==> (GREATEST x. P x) = k";
   1.229 -apply (unfold Greatest_def)
   1.230 -apply (erule GreatestM_equality)
   1.231 -apply blast
   1.232 -done
   1.233 +  "P (k::'a::order) ==> (!!x. P x ==> x <= k) ==> (GREATEST x. P x) = k"
   1.234 +  apply (unfold Greatest_def)
   1.235 +  apply (erule GreatestM_equality)
   1.236 +  apply blast
   1.237 +  done
   1.238  
   1.239  lemma ex_has_greatest_nat_lemma:
   1.240 -     "[|P k;  ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))|]  
   1.241 -      ==> EX y. P y & ~ (m y < m k + n)"
   1.242 -apply (induct_tac "n")
   1.243 -apply force
   1.244 -(*ind step*)
   1.245 -apply (force simp add: le_Suc_eq)
   1.246 -done
   1.247 +  "P k ==> ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))
   1.248 +    ==> EX y. P y & ~ (m y < m k + n)"
   1.249 +  apply (induct_tac n)
   1.250 +   apply force
   1.251 +  apply (force simp add: le_Suc_eq)
   1.252 +  done
   1.253  
   1.254 -lemma ex_has_greatest_nat: "[|P k;  ! y. P y --> m y < b|]  
   1.255 -      ==> ? x. P x & (! y. P y --> (m y::nat) <= m x)"
   1.256 -apply (rule ccontr)
   1.257 -apply (cut_tac P = "P" and n = "b - m k" in ex_has_greatest_nat_lemma)
   1.258 -apply (subgoal_tac [3] "m k <= b")
   1.259 -apply auto
   1.260 -done
   1.261 +lemma ex_has_greatest_nat:
   1.262 +  "P k ==> ALL y. P y --> m y < b
   1.263 +    ==> EX x. P x & (ALL y. P y --> (m y::nat) <= m x)"
   1.264 +  apply (rule ccontr)
   1.265 +  apply (cut_tac P = P and n = "b - m k" in ex_has_greatest_nat_lemma)
   1.266 +    apply (subgoal_tac [3] "m k <= b")
   1.267 +     apply auto
   1.268 +  done
   1.269  
   1.270 -lemma GreatestM_nat_lemma: 
   1.271 -     "[|P k;  ! y. P y --> m y < b|]  
   1.272 -      ==> P (GreatestM m P) & (!y. P y --> (m y::nat) <= m (GreatestM m P))"
   1.273 -apply (unfold GreatestM_def)
   1.274 -apply (rule someI_ex)
   1.275 -apply (erule ex_has_greatest_nat)
   1.276 -apply assumption
   1.277 -done
   1.278 +lemma GreatestM_nat_lemma:
   1.279 +  "P k ==> ALL y. P y --> m y < b
   1.280 +    ==> P (GreatestM m P) & (ALL y. P y --> (m y::nat) <= m (GreatestM m P))"
   1.281 +  apply (unfold GreatestM_def)
   1.282 +  apply (rule someI_ex)
   1.283 +  apply (erule ex_has_greatest_nat)
   1.284 +  apply assumption
   1.285 +  done
   1.286  
   1.287  lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
   1.288  
   1.289 -lemma GreatestM_nat_le: "[|P x;  ! y. P y --> m y < b|]  
   1.290 -      ==> (m x::nat) <= m (GreatestM m P)"
   1.291 -apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) 
   1.292 -done
   1.293 +lemma GreatestM_nat_le:
   1.294 +  "P x ==> ALL y. P y --> m y < b
   1.295 +    ==> (m x::nat) <= m (GreatestM m P)"
   1.296 +  apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec])
   1.297 +  done
   1.298 +
   1.299 +
   1.300 +text {* \medskip Specialization to @{text GREATEST}. *}
   1.301 +
   1.302 +lemma GreatestI: "P (k::nat) ==> ALL y. P y --> y < b ==> P (GREATEST x. P x)"
   1.303 +  apply (unfold Greatest_def)
   1.304 +  apply (rule GreatestM_natI)
   1.305 +   apply auto
   1.306 +  done
   1.307  
   1.308 -(** Specialization to GREATEST **)
   1.309 +lemma Greatest_le:
   1.310 +    "P x ==> ALL y. P y --> y < b ==> (x::nat) <= (GREATEST x. P x)"
   1.311 +  apply (unfold Greatest_def)
   1.312 +  apply (rule GreatestM_nat_le)
   1.313 +   apply auto
   1.314 +  done
   1.315 +
   1.316 +
   1.317 +subsection {* The Meson proof procedure *}
   1.318  
   1.319 -lemma GreatestI: 
   1.320 -     "[|P (k::nat);  ! y. P y --> y < b|] ==> P (GREATEST x. P x)"
   1.321 +subsubsection {* Negation Normal Form *}
   1.322 +
   1.323 +text {* de Morgan laws *}
   1.324 +
   1.325 +lemma meson_not_conjD: "~(P&Q) ==> ~P | ~Q"
   1.326 +  and meson_not_disjD: "~(P|Q) ==> ~P & ~Q"
   1.327 +  and meson_not_notD: "~~P ==> P"
   1.328 +  and meson_not_allD: "!!P. ~(ALL x. P(x)) ==> EX x. ~P(x)"
   1.329 +  and meson_not_exD: "!!P. ~(EX x. P(x)) ==> ALL x. ~P(x)"
   1.330 +  by fast+
   1.331  
   1.332 -apply (unfold Greatest_def)
   1.333 -apply (rule GreatestM_natI)
   1.334 -apply auto
   1.335 -done
   1.336 +text {* Removal of @{text "-->"} and @{text "<->"} (positive and
   1.337 +negative occurrences) *}
   1.338 +
   1.339 +lemma meson_imp_to_disjD: "P-->Q ==> ~P | Q"
   1.340 +  and meson_not_impD: "~(P-->Q) ==> P & ~Q"
   1.341 +  and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
   1.342 +  and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
   1.343 +    -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *}
   1.344 +  by fast+
   1.345 +
   1.346 +
   1.347 +subsubsection {* Pulling out the existential quantifiers *}
   1.348 +
   1.349 +text {* Conjunction *}
   1.350 +
   1.351 +lemma meson_conj_exD1: "!!P Q. (EX x. P(x)) & Q ==> EX x. P(x) & Q"
   1.352 +  and meson_conj_exD2: "!!P Q. P & (EX x. Q(x)) ==> EX x. P & Q(x)"
   1.353 +  by fast+
   1.354 +
   1.355  
   1.356 -lemma Greatest_le: 
   1.357 -     "[|P x;  ! y. P y --> y < b|] ==> (x::nat) <= (GREATEST x. P x)"
   1.358 -apply (unfold Greatest_def)
   1.359 -apply (rule GreatestM_nat_le)
   1.360 -apply auto
   1.361 -done
   1.362 +text {* Disjunction *}
   1.363 +
   1.364 +lemma meson_disj_exD: "!!P Q. (EX x. P(x)) | (EX x. Q(x)) ==> EX x. P(x) | Q(x)"
   1.365 +  -- {* DO NOT USE with forall-Skolemization: makes fewer schematic variables!! *}
   1.366 +  -- {* With ex-Skolemization, makes fewer Skolem constants *}
   1.367 +  and meson_disj_exD1: "!!P Q. (EX x. P(x)) | Q ==> EX x. P(x) | Q"
   1.368 +  and meson_disj_exD2: "!!P Q. P | (EX x. Q(x)) ==> EX x. P | Q(x)"
   1.369 +  by fast+
   1.370 +
   1.371  
   1.372 +subsubsection {* Generating clauses for the Meson Proof Procedure *}
   1.373 +
   1.374 +text {* Disjunctions *}
   1.375 +
   1.376 +lemma meson_disj_assoc: "(P|Q)|R ==> P|(Q|R)"
   1.377 +  and meson_disj_comm: "P|Q ==> Q|P"
   1.378 +  and meson_disj_FalseD1: "False|P ==> P"
   1.379 +  and meson_disj_FalseD2: "P|False ==> P"
   1.380 +  by fast+
   1.381  
   1.382  use "meson_lemmas.ML"
   1.383  use "Tools/meson.ML"