src/HOL/Hilbert_Choice.thy
changeset 14208 144f45277d5a
parent 14115 65ec3f73d00b
child 14399 dc677b35e54f
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Sep 26 10:34:28 2003 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Sep 26 10:34:57 2003 +0200
     1.3 @@ -72,17 +72,13 @@
     1.4      ==> (!!x. P x ==> \<forall>y. P y --> m x \<le> m y ==> Q x)
     1.5      ==> Q (LeastM m P)"
     1.6    apply (unfold LeastM_def)
     1.7 -  apply (rule someI2_ex)
     1.8 -   apply blast
     1.9 -  apply blast
    1.10 +  apply (rule someI2_ex, blast, blast)
    1.11    done
    1.12  
    1.13  lemma LeastM_equality:
    1.14    "P k ==> (!!x. P x ==> m k <= m x)
    1.15      ==> m (LEAST x WRT m. P x) = (m k::'a::order)"
    1.16 -  apply (rule LeastMI2)
    1.17 -    apply assumption
    1.18 -   apply blast
    1.19 +  apply (rule LeastMI2, assumption, blast)
    1.20    apply (blast intro!: order_antisym)
    1.21    done
    1.22  
    1.23 @@ -90,16 +86,14 @@
    1.24    "wf r ==> ALL x y. ((x,y):r^+) = ((y,x)~:r^*) ==> P k
    1.25      ==> EX x. P x & (!y. P y --> (m x,m y):r^*)"
    1.26    apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
    1.27 -  apply (drule_tac x = "m`Collect P" in spec)
    1.28 -  apply force
    1.29 +  apply (drule_tac x = "m`Collect P" in spec, force)
    1.30    done
    1.31  
    1.32  lemma ex_has_least_nat:
    1.33      "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
    1.34    apply (simp only: pred_nat_trancl_eq_le [symmetric])
    1.35    apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
    1.36 -   apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
    1.37 -  apply assumption
    1.38 +   apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le, assumption)
    1.39    done
    1.40  
    1.41  lemma LeastM_nat_lemma:
    1.42 @@ -112,10 +106,7 @@
    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 +by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp], assumption, assumption)
    1.51  
    1.52  
    1.53  subsection {* Greatest value operator *}
    1.54 @@ -139,32 +130,26 @@
    1.55      ==> (!!x. P x ==> \<forall>y. P y --> m y \<le> m x ==> Q x)
    1.56      ==> Q (GreatestM m P)"
    1.57    apply (unfold GreatestM_def)
    1.58 -  apply (rule someI2_ex)
    1.59 -   apply blast
    1.60 -  apply blast
    1.61 +  apply (rule someI2_ex, blast, blast)
    1.62    done
    1.63  
    1.64  lemma GreatestM_equality:
    1.65   "P k ==> (!!x. P x ==> m x <= m k)
    1.66      ==> m (GREATEST x WRT m. P x) = (m k::'a::order)"
    1.67 -  apply (rule_tac m = m in GreatestMI2)
    1.68 -    apply assumption
    1.69 -   apply blast
    1.70 +  apply (rule_tac m = m in GreatestMI2, assumption, blast)
    1.71    apply (blast intro!: order_antisym)
    1.72    done
    1.73  
    1.74  lemma Greatest_equality:
    1.75    "P (k::'a::order) ==> (!!x. P x ==> x <= k) ==> (GREATEST x. P x) = k"
    1.76    apply (unfold Greatest_def)
    1.77 -  apply (erule GreatestM_equality)
    1.78 -  apply blast
    1.79 +  apply (erule GreatestM_equality, blast)
    1.80    done
    1.81  
    1.82  lemma ex_has_greatest_nat_lemma:
    1.83    "P k ==> ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))
    1.84      ==> EX y. P y & ~ (m y < m k + n)"
    1.85 -  apply (induct_tac n)
    1.86 -   apply force
    1.87 +  apply (induct_tac n, force)
    1.88    apply (force simp add: le_Suc_eq)
    1.89    done
    1.90  
    1.91 @@ -173,8 +158,7 @@
    1.92      ==> EX x. P x & (ALL y. P y --> (m y::nat) <= m x)"
    1.93    apply (rule ccontr)
    1.94    apply (cut_tac P = P and n = "b - m k" in ex_has_greatest_nat_lemma)
    1.95 -    apply (subgoal_tac [3] "m k <= b")
    1.96 -     apply auto
    1.97 +    apply (subgoal_tac [3] "m k <= b", auto)
    1.98    done
    1.99  
   1.100  lemma GreatestM_nat_lemma:
   1.101 @@ -182,8 +166,7 @@
   1.102      ==> P (GreatestM m P) & (ALL y. P y --> (m y::nat) <= m (GreatestM m P))"
   1.103    apply (unfold GreatestM_def)
   1.104    apply (rule someI_ex)
   1.105 -  apply (erule ex_has_greatest_nat)
   1.106 -  apply assumption
   1.107 +  apply (erule ex_has_greatest_nat, assumption)
   1.108    done
   1.109  
   1.110  lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
   1.111 @@ -199,15 +182,13 @@
   1.112  
   1.113  lemma GreatestI: "P (k::nat) ==> ALL y. P y --> y < b ==> P (GREATEST x. P x)"
   1.114    apply (unfold Greatest_def)
   1.115 -  apply (rule GreatestM_natI)
   1.116 -   apply auto
   1.117 +  apply (rule GreatestM_natI, auto)
   1.118    done
   1.119  
   1.120  lemma Greatest_le:
   1.121      "P x ==> ALL y. P y --> y < b ==> (x::nat) <= (GREATEST x. P x)"
   1.122    apply (unfold Greatest_def)
   1.123 -  apply (rule GreatestM_nat_le)
   1.124 -   apply auto
   1.125 +  apply (rule GreatestM_nat_le, auto)
   1.126    done
   1.127  
   1.128