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 }
```