src/HOL/Library/Extended_Real.thy
changeset 53374 a14d2a854c02
parent 53216 ad2e09c30aa8
child 53381 355a4cac5440
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -146,11 +146,11 @@
     1.4  "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
     1.5  proof -
     1.6    case (goal1 P x)
     1.7 -  moreover then obtain a b where "x = (a, b)" by (cases x) auto
     1.8 -  ultimately show P
     1.9 +  then obtain a b where "x = (a, b)" by (cases x) auto
    1.10 +  with goal1 show P
    1.11     by (cases rule: ereal2_cases[of a b]) auto
    1.12  qed auto
    1.13 -termination proof qed (rule wf_empty)
    1.14 +termination by default (rule wf_empty)
    1.15  
    1.16  lemma Infty_neq_0[simp]:
    1.17    "(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
    1.18 @@ -234,8 +234,8 @@
    1.19  | "        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
    1.20  proof -
    1.21    case (goal1 P x)
    1.22 -  moreover then obtain a b where "x = (a,b)" by (cases x) auto
    1.23 -  ultimately show P by (cases rule: ereal2_cases[of a b]) auto
    1.24 +  then obtain a b where "x = (a,b)" by (cases x) auto
    1.25 +  with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
    1.26  qed simp_all
    1.27  termination by (relation "{}") simp
    1.28  
    1.29 @@ -496,8 +496,8 @@
    1.30  "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
    1.31  proof -
    1.32    case (goal1 P x)
    1.33 -  moreover then obtain a b where "x = (a, b)" by (cases x) auto
    1.34 -  ultimately show P by (cases rule: ereal2_cases[of a b]) auto
    1.35 +  then obtain a b where "x = (a, b)" by (cases x) auto
    1.36 +  with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
    1.37  qed simp_all
    1.38  termination by (relation "{}") simp
    1.39  
    1.40 @@ -1338,9 +1338,9 @@
    1.41    next
    1.42      { assume "c = \<infinity>" have ?thesis
    1.43        proof cases
    1.44 -        assume "\<forall>i. f i = 0"
    1.45 -        moreover then have "range f = {0}" by auto
    1.46 -        ultimately show "c * SUPR UNIV f \<le> y" using *
    1.47 +        assume **: "\<forall>i. f i = 0"
    1.48 +        then have "range f = {0}" by auto
    1.49 +        with ** show "c * SUPR UNIV f \<le> y" using *
    1.50            by (auto simp: SUP_def min_max.sup_absorb1)
    1.51        next
    1.52          assume "\<not> (\<forall>i. f i = 0)"
    1.53 @@ -1417,9 +1417,9 @@
    1.54    from `A \<noteq> {}` obtain x where "x \<in> A" by auto
    1.55    show ?thesis
    1.56    proof cases
    1.57 -    assume "\<infinity> \<in> A"
    1.58 -    moreover then have "\<infinity> \<le> Sup A" by (intro complete_lattice_class.Sup_upper)
    1.59 -    ultimately show ?thesis by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
    1.60 +    assume *: "\<infinity> \<in> A"
    1.61 +    then have "\<infinity> \<le> Sup A" by (intro complete_lattice_class.Sup_upper)
    1.62 +    with * show ?thesis by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
    1.63    next
    1.64      assume "\<infinity> \<notin> A"
    1.65      have "\<exists>x\<in>A. 0 \<le> x"
    1.66 @@ -1489,10 +1489,13 @@
    1.67    fixes A :: "ereal set" assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
    1.68    shows "Inf ((\<lambda>x. a - x) ` A) = a - Sup A"
    1.69  proof -
    1.70 -  { fix x have "-a - -x = -(a - x)" using assms by (cases x) auto }
    1.71 -  moreover then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
    1.72 +  {
    1.73 +    fix x
    1.74 +    have "-a - -x = -(a - x)" using assms by (cases x) auto
    1.75 +  } note * = this
    1.76 +  then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
    1.77      by (auto simp: image_image)
    1.78 -  ultimately show ?thesis
    1.79 +  with * show ?thesis
    1.80      using Sup_ereal_cminus[of "uminus ` A" "-a"] assms
    1.81      by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq)
    1.82  qed
    1.83 @@ -1606,9 +1609,9 @@
    1.84    unfolding open_ereal_generated
    1.85  proof (induct rule: generate_topology.induct)
    1.86    case (Int A B)
    1.87 -  moreover then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
    1.88 -      by auto
    1.89 -  ultimately show ?case
    1.90 +  then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
    1.91 +    by auto
    1.92 +  with Int show ?case
    1.93      by (intro exI[of _ "max x z"]) fastforce
    1.94  next
    1.95    { fix x have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t" by (cases x) auto }
    1.96 @@ -1621,9 +1624,9 @@
    1.97    unfolding open_ereal_generated
    1.98  proof (induct rule: generate_topology.induct)
    1.99    case (Int A B)
   1.100 -  moreover then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
   1.101 -      by auto
   1.102 -  ultimately show ?case
   1.103 +  then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
   1.104 +    by auto
   1.105 +  with Int show ?case
   1.106      by (intro exI[of _ "min x z"]) fastforce
   1.107  next
   1.108    { fix x have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" by (cases x) auto }