src/HOL/Hilbert_Choice.thy
changeset 11454 7514e5e21cb8
parent 11451 8abfb4f7bd02
child 11506 244a02a2968b
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Jul 25 13:44:32 2001 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Jul 25 17:58:26 2001 +0200
     1.3 @@ -29,6 +29,11 @@
     1.4    someI:        "P (x::'a) ==> P (SOME x. P x)"
     1.5  
     1.6  
     1.7 +(*used in TFL*)
     1.8 +lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
     1.9 +  by (blast intro: someI)
    1.10 +
    1.11 +
    1.12  constdefs  
    1.13    inv :: "('a => 'b) => ('b => 'a)"
    1.14      "inv(f::'a=>'b) == % y. @x. f(x)=y"
    1.15 @@ -71,6 +76,38 @@
    1.16  apply (blast intro!: order_antisym) 
    1.17  done
    1.18  
    1.19 +lemma wf_linord_ex_has_least:
    1.20 +     "[|wf r;  ALL x y. ((x,y):r^+) = ((y,x)~:r^*);  P k|]  \
    1.21 +\     ==> EX x. P x & (!y. P y --> (m x,m y):r^*)" 
    1.22 +apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
    1.23 +apply (drule_tac x = "m`Collect P" in spec)
    1.24 +apply force
    1.25 +done
    1.26 +
    1.27 +(* successor of obsolete nonempty_has_least *)
    1.28 +lemma ex_has_least_nat:
    1.29 +     "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
    1.30 +apply (simp only: pred_nat_trancl_eq_le [symmetric])
    1.31 +apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
    1.32 +apply (simp (no_asm) add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
    1.33 +apply assumption
    1.34 +done
    1.35 +
    1.36 +lemma LeastM_nat_lemma: 
    1.37 +  "P k ==> P (LeastM m P) & (ALL y. P y --> m (LeastM m P) <= (m y::nat))"
    1.38 +apply (unfold LeastM_def)
    1.39 +apply (rule someI_ex)
    1.40 +apply (erule ex_has_least_nat)
    1.41 +done
    1.42 +
    1.43 +lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
    1.44 +
    1.45 +lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
    1.46 +apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
    1.47 +apply assumption
    1.48 +apply assumption
    1.49 +done
    1.50 +
    1.51  
    1.52  (** Greatest value operator **)
    1.53