paulson@11451: (*  Title:      HOL/Hilbert_Choice.thy
paulson@11451:     ID:         $Id$
paulson@11451:     Author:     Lawrence C Paulson
paulson@11451:     Copyright   2001  University of Cambridge
paulson@11451: 
paulson@11451: Hilbert's epsilon-operator and everything to do with the Axiom of Choice
paulson@11451: *)
paulson@11451: 
paulson@11451: theory Hilbert_Choice = NatArith
paulson@11451: files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
paulson@11451: 
paulson@11451: consts
paulson@11451:   Eps           :: "('a => bool) => 'a"
paulson@11451: 
paulson@11451: 
paulson@11451: syntax (input)
wenzelm@11506:   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\<epsilon>_./ _)" [0, 10] 10)
paulson@11451: 
paulson@11451: syntax (HOL)
paulson@11451:   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
paulson@11451: 
paulson@11451: syntax
paulson@11451:   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3SOME _./ _)" [0, 10] 10)
paulson@11451: 
paulson@11451: translations
paulson@11451:   "SOME x. P"             == "Eps (%x. P)"
paulson@11451: 
paulson@11451: axioms  
paulson@11451:   someI:        "P (x::'a) ==> P (SOME x. P x)"
paulson@11451: 
paulson@11451: 
paulson@11454: (*used in TFL*)
wenzelm@11506: lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
paulson@11454:   by (blast intro: someI)
paulson@11454: 
paulson@11454: 
paulson@11451: constdefs  
paulson@11451:   inv :: "('a => 'b) => ('b => 'a)"
paulson@11451:     "inv(f::'a=>'b) == % y. @x. f(x)=y"
paulson@11451: 
paulson@11451:   Inv :: "['a set, 'a => 'b] => ('b => 'a)"
paulson@11451:     "Inv A f == (% x. (@ y. y : A & f y = x))"
paulson@11451: 
paulson@11451: 
paulson@11451: use "Hilbert_Choice_lemmas.ML"
paulson@11451: 
paulson@11451: 
paulson@11451: (** Least value operator **)
paulson@11451: 
paulson@11451: constdefs
paulson@11451:   LeastM   :: "['a => 'b::ord, 'a => bool] => 'a"
paulson@11451:               "LeastM m P == @x. P x & (ALL y. P y --> m x <= m y)"
paulson@11451: 
paulson@11451: syntax
paulson@11451:  "@LeastM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0,4,10]10)
paulson@11451: 
paulson@11451: translations
paulson@11451:                 "LEAST x WRT m. P" == "LeastM m (%x. P)"
paulson@11451: 
paulson@11451: lemma LeastMI2:
paulson@11451:   "[| P x; !!y. P y ==> m x <= m y;
wenzelm@11506:            !!x. [| P x; \<forall>y. P y --> m x \<le> m y |] ==> Q x |]
paulson@11451:    ==> Q (LeastM m P)";
paulson@11451: apply (unfold LeastM_def)
paulson@11451: apply (rule someI2_ex)
paulson@11451: apply  blast
paulson@11451: apply blast
paulson@11451: done
paulson@11451: 
paulson@11451: lemma LeastM_equality:
paulson@11451:  "[| P k; !!x. P x ==> m k <= m x |] ==> m (LEAST x WRT m. P x) = 
paulson@11451:      (m k::'a::order)";
paulson@11451: apply (rule LeastMI2)
paulson@11451: apply   assumption
paulson@11451: apply  blast
paulson@11451: apply (blast intro!: order_antisym) 
paulson@11451: done
paulson@11451: 
paulson@11454: lemma wf_linord_ex_has_least:
paulson@11454:      "[|wf r;  ALL x y. ((x,y):r^+) = ((y,x)~:r^*);  P k|]  \
paulson@11454: \     ==> EX x. P x & (!y. P y --> (m x,m y):r^*)" 
paulson@11454: apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
paulson@11454: apply (drule_tac x = "m`Collect P" in spec)
paulson@11454: apply force
paulson@11454: done
paulson@11454: 
paulson@11454: (* successor of obsolete nonempty_has_least *)
paulson@11454: lemma ex_has_least_nat:
paulson@11454:      "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
paulson@11454: apply (simp only: pred_nat_trancl_eq_le [symmetric])
paulson@11454: apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
paulson@11454: apply (simp (no_asm) add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
paulson@11454: apply assumption
paulson@11454: done
paulson@11454: 
paulson@11454: lemma LeastM_nat_lemma: 
paulson@11454:   "P k ==> P (LeastM m P) & (ALL y. P y --> m (LeastM m P) <= (m y::nat))"
paulson@11454: apply (unfold LeastM_def)
paulson@11454: apply (rule someI_ex)
paulson@11454: apply (erule ex_has_least_nat)
paulson@11454: done
paulson@11454: 
paulson@11454: lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
paulson@11454: 
paulson@11454: lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
paulson@11454: apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
paulson@11454: apply assumption
paulson@11454: apply assumption
paulson@11454: done
paulson@11454: 
paulson@11451: 
paulson@11451: (** Greatest value operator **)
paulson@11451: 
paulson@11451: constdefs
paulson@11451:   GreatestM   :: "['a => 'b::ord, 'a => bool] => 'a"
paulson@11451:               "GreatestM m P == @x. P x & (ALL y. P y --> m y <= m x)"
paulson@11451:   
paulson@11451:   Greatest    :: "('a::ord => bool) => 'a"         (binder "GREATEST " 10)
paulson@11451:               "Greatest     == GreatestM (%x. x)"
paulson@11451: 
paulson@11451: syntax
paulson@11451:  "@GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
paulson@11451:                                         ("GREATEST _ WRT _. _" [0,4,10]10)
paulson@11451: 
paulson@11451: translations
paulson@11451:               "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
paulson@11451: 
paulson@11451: lemma GreatestMI2:
paulson@11451:      "[| P x;
paulson@11451: 	 !!y. P y ==> m y <= m x;
wenzelm@11506:          !!x. [| P x; \<forall>y. P y --> m y \<le> m x |] ==> Q x |]
paulson@11451:       ==> Q (GreatestM m P)";
paulson@11451: apply (unfold GreatestM_def)
paulson@11451: apply (rule someI2_ex)
paulson@11451: apply  blast
paulson@11451: apply blast
paulson@11451: done
paulson@11451: 
paulson@11451: lemma GreatestM_equality:
paulson@11451:  "[| P k;  !!x. P x ==> m x <= m k |]
paulson@11451:   ==> m (GREATEST x WRT m. P x) = (m k::'a::order)";
paulson@11451: apply (rule_tac m=m in GreatestMI2)
paulson@11451: apply   assumption
paulson@11451: apply  blast
paulson@11451: apply (blast intro!: order_antisym) 
paulson@11451: done
paulson@11451: 
paulson@11451: lemma Greatest_equality:
paulson@11451:   "[| P (k::'a::order); !!x. P x ==> x <= k |] ==> (GREATEST x. P x) = k";
paulson@11451: apply (unfold Greatest_def)
paulson@11451: apply (erule GreatestM_equality)
paulson@11451: apply blast
paulson@11451: done
paulson@11451: 
paulson@11451: lemma ex_has_greatest_nat_lemma:
paulson@11451:      "[|P k;  ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))|]  
paulson@11451:       ==> EX y. P y & ~ (m y < m k + n)"
paulson@11451: apply (induct_tac "n")
paulson@11451: apply force
paulson@11451: (*ind step*)
paulson@11451: apply (force simp add: le_Suc_eq)
paulson@11451: done
paulson@11451: 
paulson@11451: lemma ex_has_greatest_nat: "[|P k;  ! y. P y --> m y < b|]  
paulson@11451:       ==> ? x. P x & (! y. P y --> (m y::nat) <= m x)"
paulson@11451: apply (rule ccontr)
paulson@11451: apply (cut_tac P = "P" and n = "b - m k" in ex_has_greatest_nat_lemma)
paulson@11451: apply (subgoal_tac [3] "m k <= b")
paulson@11451: apply auto
paulson@11451: done
paulson@11451: 
paulson@11451: lemma GreatestM_nat_lemma: 
paulson@11451:      "[|P k;  ! y. P y --> m y < b|]  
paulson@11451:       ==> P (GreatestM m P) & (!y. P y --> (m y::nat) <= m (GreatestM m P))"
paulson@11451: apply (unfold GreatestM_def)
paulson@11451: apply (rule someI_ex)
paulson@11451: apply (erule ex_has_greatest_nat)
paulson@11451: apply assumption
paulson@11451: done
paulson@11451: 
paulson@11451: lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
paulson@11451: 
paulson@11451: lemma GreatestM_nat_le: "[|P x;  ! y. P y --> m y < b|]  
paulson@11451:       ==> (m x::nat) <= m (GreatestM m P)"
paulson@11451: apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) 
paulson@11451: done
paulson@11451: 
paulson@11451: (** Specialization to GREATEST **)
paulson@11451: 
paulson@11451: lemma GreatestI: 
paulson@11451:      "[|P (k::nat);  ! y. P y --> y < b|] ==> P (GREATEST x. P x)"
paulson@11451: 
paulson@11451: apply (unfold Greatest_def)
paulson@11451: apply (rule GreatestM_natI)
paulson@11451: apply auto
paulson@11451: done
paulson@11451: 
paulson@11451: lemma Greatest_le: 
paulson@11451:      "[|P x;  ! y. P y --> y < b|] ==> (x::nat) <= (GREATEST x. P x)"
paulson@11451: apply (unfold Greatest_def)
paulson@11451: apply (rule GreatestM_nat_le)
paulson@11451: apply auto
paulson@11451: done
paulson@11451: 
paulson@11451: 
paulson@11451: use "meson_lemmas.ML"
paulson@11451: use "Tools/meson.ML"
paulson@11451: setup meson_setup
paulson@11451: 
paulson@11451: end