src/HOL/Hilbert_Choice.thy
changeset 11454 7514e5e21cb8
parent 11451 8abfb4f7bd02
child 11506 244a02a2968b
equal deleted inserted replaced
11453:1b15f655da2c 11454:7514e5e21cb8
    25 translations
    25 translations
    26   "SOME x. P"             == "Eps (%x. P)"
    26   "SOME x. P"             == "Eps (%x. P)"
    27 
    27 
    28 axioms  
    28 axioms  
    29   someI:        "P (x::'a) ==> P (SOME x. P x)"
    29   someI:        "P (x::'a) ==> P (SOME x. P x)"
       
    30 
       
    31 
       
    32 (*used in TFL*)
       
    33 lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
       
    34   by (blast intro: someI)
    30 
    35 
    31 
    36 
    32 constdefs  
    37 constdefs  
    33   inv :: "('a => 'b) => ('b => 'a)"
    38   inv :: "('a => 'b) => ('b => 'a)"
    34     "inv(f::'a=>'b) == % y. @x. f(x)=y"
    39     "inv(f::'a=>'b) == % y. @x. f(x)=y"
    67      (m k::'a::order)";
    72      (m k::'a::order)";
    68 apply (rule LeastMI2)
    73 apply (rule LeastMI2)
    69 apply   assumption
    74 apply   assumption
    70 apply  blast
    75 apply  blast
    71 apply (blast intro!: order_antisym) 
    76 apply (blast intro!: order_antisym) 
       
    77 done
       
    78 
       
    79 lemma wf_linord_ex_has_least:
       
    80      "[|wf r;  ALL x y. ((x,y):r^+) = ((y,x)~:r^*);  P k|]  \
       
    81 \     ==> EX x. P x & (!y. P y --> (m x,m y):r^*)" 
       
    82 apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
       
    83 apply (drule_tac x = "m`Collect P" in spec)
       
    84 apply force
       
    85 done
       
    86 
       
    87 (* successor of obsolete nonempty_has_least *)
       
    88 lemma ex_has_least_nat:
       
    89      "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
       
    90 apply (simp only: pred_nat_trancl_eq_le [symmetric])
       
    91 apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
       
    92 apply (simp (no_asm) add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
       
    93 apply assumption
       
    94 done
       
    95 
       
    96 lemma LeastM_nat_lemma: 
       
    97   "P k ==> P (LeastM m P) & (ALL y. P y --> m (LeastM m P) <= (m y::nat))"
       
    98 apply (unfold LeastM_def)
       
    99 apply (rule someI_ex)
       
   100 apply (erule ex_has_least_nat)
       
   101 done
       
   102 
       
   103 lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
       
   104 
       
   105 lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
       
   106 apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
       
   107 apply assumption
       
   108 apply assumption
    72 done
   109 done
    73 
   110 
    74 
   111 
    75 (** Greatest value operator **)
   112 (** Greatest value operator **)
    76 
   113