src/HOL/Hilbert_Choice.thy
 changeset 11454 7514e5e21cb8 parent 11451 8abfb4f7bd02 child 11506 244a02a2968b
equal 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