tuned proofs;
authorwenzelm
Thu Jun 14 23:04:39 2007 +0200 (2007-06-14)
changeset 23394474ff28210c0
parent 23393 31781b2de73d
child 23395 15fb6637690e
tuned proofs;
src/HOL/Library/Char_nat.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Library/Graphs.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/Kleene_Algebras.thy
src/HOL/Library/List_Prefix.thy
src/HOL/Library/NatPair.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/SCT_Implementation.thy
src/HOL/Library/SCT_Interpretation.thy
src/HOL/Library/SCT_Misc.thy
src/HOL/Library/SCT_Theorem.thy
src/HOL/Unix/Unix.thy
     1.1 --- a/src/HOL/Library/Char_nat.thy	Thu Jun 14 23:04:36 2007 +0200
     1.2 +++ b/src/HOL/Library/Char_nat.thy	Thu Jun 14 23:04:39 2007 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  fun
     1.6    nat_of_nibble :: "nibble \<Rightarrow> nat" where
     1.7 -  "nat_of_nibble Nibble0 = 0"
     1.8 +    "nat_of_nibble Nibble0 = 0"
     1.9    | "nat_of_nibble Nibble1 = 1"
    1.10    | "nat_of_nibble Nibble2 = 2"
    1.11    | "nat_of_nibble Nibble3 = 3"
    1.12 @@ -83,7 +83,8 @@
    1.13  
    1.14  lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16"
    1.15  proof -
    1.16 -  have nibble_nat_enum: "n mod 16 \<in> {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15}"
    1.17 +  have nibble_nat_enum:
    1.18 +    "n mod 16 \<in> {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15}"
    1.19    proof -
    1.20      have set_unfold: "\<And>n. {0..Suc n} = insert (Suc n) {0..n}" by auto
    1.21      have "(n\<Colon>nat) mod 16 \<in> {0..Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
    1.22 @@ -111,8 +112,7 @@
    1.23  text {* Conversion between chars and nats. *}
    1.24  
    1.25  definition
    1.26 -  nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble"
    1.27 -where
    1.28 +  nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble" where
    1.29    "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
    1.30  
    1.31  lemma nibble_of_pair [code func]:
    1.32 @@ -146,7 +146,7 @@
    1.33    proof -
    1.34      fix m k n :: nat
    1.35      show "(k * n + m) mod n = m mod n"
    1.36 -    by (simp only: mod_mult_self1 [symmetric, of m n k] add_commute)
    1.37 +      by (simp only: mod_mult_self1 [symmetric, of m n k] add_commute)
    1.38    qed
    1.39    from mod_div_decomp [of n 256] obtain k l where n: "n = k * 256 + l"
    1.40      and k: "k = n div 256" and l: "l = n mod 256" by blast
    1.41 @@ -163,28 +163,31 @@
    1.42    have aux4: "(k * 256 + l) mod 16 = l mod 16"
    1.43      unfolding 256 mult_assoc [symmetric] mod_mult_self3 ..
    1.44    show ?thesis
    1.45 -  by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair nat_of_nibble_of_nat mod_mult_distrib
    1.46 -    n aux3 mod_mult_self3 l_256 aux4 mod_add1_eq [of "256 * k"] l_div_256)
    1.47 +    by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
    1.48 +      nat_of_nibble_of_nat mod_mult_distrib
    1.49 +      n aux3 mod_mult_self3 l_256 aux4 mod_add1_eq [of "256 * k"] l_div_256)
    1.50  qed
    1.51  
    1.52  lemma nibble_pair_of_nat_char:
    1.53    "nibble_pair_of_nat (nat_of_char (Char n m)) = (n, m)"
    1.54  proof -
    1.55    have nat_of_nibble_256:
    1.56 -    "\<And>n m. (nat_of_nibble n * 16 + nat_of_nibble m) mod 256 = nat_of_nibble n * 16 + nat_of_nibble m"
    1.57 +    "\<And>n m. (nat_of_nibble n * 16 + nat_of_nibble m) mod 256 =
    1.58 +      nat_of_nibble n * 16 + nat_of_nibble m"
    1.59    proof -
    1.60      fix n m
    1.61      have nat_of_nibble_less_eq_15: "\<And>n. nat_of_nibble n \<le> 15"
    1.62 -    using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: nat_number)
    1.63 -    have less_eq_240: "nat_of_nibble n * 16 \<le> 240" using nat_of_nibble_less_eq_15 by auto
    1.64 +      using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: nat_number)
    1.65 +    have less_eq_240: "nat_of_nibble n * 16 \<le> 240"
    1.66 +      using nat_of_nibble_less_eq_15 by auto
    1.67      have "nat_of_nibble n * 16 + nat_of_nibble m \<le> 240 + 15"
    1.68 -    by (rule add_le_mono [of _ 240 _ 15]) (auto intro: nat_of_nibble_less_eq_15 less_eq_240)
    1.69 +      by (rule add_le_mono [of _ 240 _ 15]) (auto intro: nat_of_nibble_less_eq_15 less_eq_240)
    1.70      then have "nat_of_nibble n * 16 + nat_of_nibble m < 256" (is "?rhs < _") by auto
    1.71      then show "?rhs mod 256 = ?rhs" by auto
    1.72    qed
    1.73    show ?thesis
    1.74 -  unfolding nibble_pair_of_nat_def Char_char_of_nat nat_of_char_of_nat nat_of_nibble_256
    1.75 -  by (simp add: add_commute nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
    1.76 +    unfolding nibble_pair_of_nat_def Char_char_of_nat nat_of_char_of_nat nat_of_nibble_256
    1.77 +    by (simp add: add_commute nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
    1.78  qed
    1.79  
    1.80  
     2.1 --- a/src/HOL/Library/Char_ord.thy	Thu Jun 14 23:04:36 2007 +0200
     2.2 +++ b/src/HOL/Library/Char_ord.thy	Thu Jun 14 23:04:39 2007 +0200
     2.3 @@ -13,32 +13,36 @@
     2.4    nibble_less_eq_def: "n \<le> m \<equiv> nat_of_nibble n \<le> nat_of_nibble m"
     2.5    nibble_less_def: "n < m \<equiv> nat_of_nibble n < nat_of_nibble m"
     2.6  proof
     2.7 -  fix n :: nibble show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
     2.8 +  fix n :: nibble
     2.9 +  show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
    2.10  next
    2.11    fix n m q :: nibble
    2.12    assume "n \<le> m"
    2.13 -  and "m \<le> q"
    2.14 +    and "m \<le> q"
    2.15    then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
    2.16  next
    2.17    fix n m :: nibble
    2.18    assume "n \<le> m"
    2.19 -  and "m \<le> n"
    2.20 -  then show "n = m" unfolding nibble_less_eq_def nibble_less_def by (auto simp add: nat_of_nibble_eq)
    2.21 +    and "m \<le> n"
    2.22 +  then show "n = m"
    2.23 +    unfolding nibble_less_eq_def nibble_less_def
    2.24 +    by (auto simp add: nat_of_nibble_eq)
    2.25  next
    2.26    fix n m :: nibble
    2.27    show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m"
    2.28 -  unfolding nibble_less_eq_def nibble_less_def less_le by (auto simp add: nat_of_nibble_eq)
    2.29 +    unfolding nibble_less_eq_def nibble_less_def less_le
    2.30 +    by (auto simp add: nat_of_nibble_eq)
    2.31  next
    2.32    fix n m :: nibble
    2.33    show "n \<le> m \<or> m \<le> n"
    2.34 -  unfolding nibble_less_eq_def by auto
    2.35 +    unfolding nibble_less_eq_def by auto
    2.36  qed
    2.37  
    2.38  instance nibble :: distrib_lattice
    2.39 -  "inf \<equiv> min"
    2.40 -  "sup \<equiv> max"
    2.41 -  by default
    2.42 -    (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    2.43 +    "inf \<equiv> min"
    2.44 +    "sup \<equiv> max"
    2.45 +  by default (auto simp add:
    2.46 +    inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    2.47  
    2.48  instance char :: linorder
    2.49    char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    2.50 @@ -50,10 +54,10 @@
    2.51  lemmas [code func del] = char_less_eq_def char_less_def
    2.52  
    2.53  instance char :: distrib_lattice
    2.54 -  "inf \<equiv> min"
    2.55 -  "sup \<equiv> max"
    2.56 -  by default
    2.57 -    (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
    2.58 +    "inf \<equiv> min"
    2.59 +    "sup \<equiv> max"
    2.60 +  by default (auto simp add:
    2.61 +    inf_char_def sup_char_def min_max.sup_inf_distrib1)
    2.62  
    2.63  lemma [simp, code func]:
    2.64    shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
     3.1 --- a/src/HOL/Library/EfficientNat.thy	Thu Jun 14 23:04:36 2007 +0200
     3.2 +++ b/src/HOL/Library/EfficientNat.thy	Thu Jun 14 23:04:39 2007 +0200
     3.3 @@ -48,13 +48,13 @@
     3.4    fixes k
     3.5    assumes "k \<ge> 0"
     3.6    shows "number_of k = nat_of_int (number_of k)"
     3.7 -  unfolding nat_of_int_def [OF prems] nat_number_of_def number_of_is_id ..
     3.8 +  unfolding nat_of_int_def [OF assms] nat_number_of_def number_of_is_id ..
     3.9  
    3.10  lemma nat_of_int_of_number_of_aux:
    3.11    fixes k
    3.12    assumes "Numeral.Pls \<le> k \<equiv> True"
    3.13    shows "k \<ge> 0"
    3.14 -  using prems unfolding Pls_def by simp
    3.15 +  using assms unfolding Pls_def by simp
    3.16  
    3.17  lemma nat_of_int_int:
    3.18    "nat_of_int (int' n) = n"
     4.1 --- a/src/HOL/Library/ExecutableSet.thy	Thu Jun 14 23:04:36 2007 +0200
     4.2 +++ b/src/HOL/Library/ExecutableSet.thy	Thu Jun 14 23:04:39 2007 +0200
     4.3 @@ -56,10 +56,9 @@
     4.4    insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
     4.5    "insertl x xs = (if member xs x then xs else x#xs)"
     4.6  
     4.7 -lemma
     4.8 -  [code target: List]: "member [] y \<longleftrightarrow> False"
     4.9 +lemma [code target: List]: "member [] y \<longleftrightarrow> False"
    4.10    and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
    4.11 -unfolding member_def by (induct xs) simp_all
    4.12 +  unfolding member_def by (induct xs) simp_all
    4.13  
    4.14  fun
    4.15    drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    4.16 @@ -201,7 +200,7 @@
    4.17    fixes ys
    4.18    assumes distnct: "distinct ys"
    4.19    shows "set (subtract' ys xs) = set ys - set xs"
    4.20 -  and "distinct (subtract' ys xs)"
    4.21 +    and "distinct (subtract' ys xs)"
    4.22    unfolding subtract'_def flip_def subtract_def
    4.23    using distnct by (induct xs arbitrary: ys) auto
    4.24  
    4.25 @@ -211,7 +210,8 @@
    4.26  
    4.27  lemma iso_unions:
    4.28    "set (unions xss) = \<Union> set (map set xss)"
    4.29 -unfolding unions_def proof (induct xss)
    4.30 +  unfolding unions_def
    4.31 +proof (induct xss)
    4.32    case Nil show ?case by simp
    4.33  next
    4.34    case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
     5.1 --- a/src/HOL/Library/Graphs.thy	Thu Jun 14 23:04:36 2007 +0200
     5.2 +++ b/src/HOL/Library/Graphs.thy	Thu Jun 14 23:04:39 2007 +0200
     5.3 @@ -399,7 +399,7 @@
     5.4      hence "fst (path_nth p (Suc i mod ?l)) = fst (path_nth p 0)" 
     5.5        by (simp add: mod_Suc)
     5.6      also from fst_p0 have "\<dots> = fst p" .
     5.7 -    also have "\<dots> = end_node p" by assumption
     5.8 +    also have "\<dots> = end_node p" by fact
     5.9      also have "\<dots> = snd (snd (path_nth p ?k))" 
    5.10        by (auto simp: endnode_nth wrap)
    5.11      finally show ?thesis .
     6.1 --- a/src/HOL/Library/Infinite_Set.thy	Thu Jun 14 23:04:36 2007 +0200
     6.2 +++ b/src/HOL/Library/Infinite_Set.thy	Thu Jun 14 23:04:39 2007 +0200
     6.3 @@ -346,7 +346,7 @@
     6.4  lemma inf_img_fin_domE:
     6.5    assumes "finite (f`A)" and "infinite A"
     6.6    obtains y where "y \<in> f`A" and "infinite (f -` {y})"
     6.7 -  using prems by (blast dest: inf_img_fin_dom)
     6.8 +  using assms by (blast dest: inf_img_fin_dom)
     6.9  
    6.10  
    6.11  subsection "Infinitely Many and Almost All"
     7.1 --- a/src/HOL/Library/Kleene_Algebras.thy	Thu Jun 14 23:04:36 2007 +0200
     7.2 +++ b/src/HOL/Library/Kleene_Algebras.thy	Thu Jun 14 23:04:39 2007 +0200
     7.3 @@ -100,8 +100,7 @@
     7.4    fixes l :: "'a :: complete_lattice"
     7.5    assumes "l \<le> M i"
     7.6    shows "l \<le> (SUP i. M i)"
     7.7 -  using prems
     7.8 -  by (rule order_trans) (rule le_SUPI [OF UNIV_I])
     7.9 +  using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
    7.10  
    7.11  lemma zero_minimum[simp]: "(0::'a::pre_kleene) \<le> x"
    7.12    unfolding order_def by simp
    7.13 @@ -428,7 +427,7 @@
    7.14    fixes A X :: "'a :: {kleene}"
    7.15    assumes "mk_tcl_dom (A, X)"
    7.16    shows "mk_tcl A X = X * star A"
    7.17 -  using prems
    7.18 +  using assms
    7.19    by induct (auto simp:mk_tcl_lemma1 mk_tcl_lemma2)
    7.20  
    7.21  lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
    7.22 @@ -446,7 +445,7 @@
    7.23    fixes A X :: "'a :: {kleene}"
    7.24    assumes "mk_tcl A A \<noteq> 0"
    7.25    shows "mk_tcl A A = tcl A"
    7.26 -  using prems mk_tcl_default mk_tcl_correctness
    7.27 +  using assms mk_tcl_default mk_tcl_correctness
    7.28    unfolding tcl_def 
    7.29    by (auto simp:star_commute)
    7.30  
     8.1 --- a/src/HOL/Library/List_Prefix.thy	Thu Jun 14 23:04:36 2007 +0200
     8.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu Jun 14 23:04:39 2007 +0200
     8.3 @@ -26,7 +26,7 @@
     8.4  lemma prefixE [elim?]:
     8.5    assumes "xs \<le> ys"
     8.6    obtains zs where "ys = xs @ zs"
     8.7 -  using prems unfolding prefix_def by blast
     8.8 +  using assms unfolding prefix_def by blast
     8.9  
    8.10  lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
    8.11    unfolding strict_prefix_def prefix_def by blast
    8.12 @@ -47,7 +47,7 @@
    8.13    fixes xs ys :: "'a list"
    8.14    assumes "xs < ys"
    8.15    obtains "xs \<le> ys" and "xs \<noteq> ys"
    8.16 -  using prems unfolding strict_prefix_def by blast
    8.17 +  using assms unfolding strict_prefix_def by blast
    8.18  
    8.19  
    8.20  subsection {* Basic properties of prefixes *}
    8.21 @@ -168,7 +168,7 @@
    8.22  lemma parallelE [elim]:
    8.23    assumes "xs \<parallel> ys"
    8.24    obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"
    8.25 -  using prems unfolding parallel_def by blast
    8.26 +  using assms unfolding parallel_def by blast
    8.27  
    8.28  theorem prefix_cases:
    8.29    obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"
    8.30 @@ -227,7 +227,7 @@
    8.31  lemma postfixE [elim?]:
    8.32    assumes "xs >>= ys"
    8.33    obtains zs where "xs = zs @ ys"
    8.34 -  using prems unfolding postfix_def by blast
    8.35 +  using assms unfolding postfix_def by blast
    8.36  
    8.37  lemma postfix_refl [iff]: "xs >>= xs"
    8.38    by (auto simp add: postfix_def)
     9.1 --- a/src/HOL/Library/NatPair.thy	Thu Jun 14 23:04:36 2007 +0200
     9.2 +++ b/src/HOL/Library/NatPair.thy	Thu Jun 14 23:04:39 2007 +0200
     9.3 @@ -73,22 +73,19 @@
     9.4  theorem nat2_to_nat_inj: "inj nat2_to_nat"
     9.5  proof -
     9.6    {
     9.7 -    fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
     9.8 +    fix u v x y
     9.9 +    assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    9.10      then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
    9.11 -    also from prems [symmetric] have "x+y \<le> u+v"
    9.12 +    also from eq1 [symmetric] have "x+y \<le> u+v"
    9.13        by (rule nat2_to_nat_help)
    9.14 -    finally have eq: "u+v = x+y" .
    9.15 -    with prems have ux: "u=x"
    9.16 +    finally have eq2: "u+v = x+y" .
    9.17 +    with eq1 have ux: "u=x"
    9.18        by (simp add: nat2_to_nat_def Let_def)
    9.19 -    with eq have vy: "v=y"
    9.20 -      by simp
    9.21 -    with ux have "(u,v) = (x,y)"
    9.22 -      by simp
    9.23 +    with eq2 have vy: "v=y" by simp
    9.24 +    with ux have "(u,v) = (x,y)" by simp
    9.25    }
    9.26 -  then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
    9.27 -    by fast
    9.28 -  then show ?thesis
    9.29 -    by (unfold inj_on_def) simp
    9.30 +  then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast
    9.31 +  then show ?thesis unfolding inj_on_def by simp
    9.32  qed
    9.33  
    9.34  end
    10.1 --- a/src/HOL/Library/Nested_Environment.thy	Thu Jun 14 23:04:36 2007 +0200
    10.2 +++ b/src/HOL/Library/Nested_Environment.thy	Thu Jun 14 23:04:39 2007 +0200
    10.3 @@ -103,7 +103,7 @@
    10.4  theorem lookup_append_none:
    10.5    assumes "lookup env xs = None"
    10.6    shows "lookup env (xs @ ys) = None"
    10.7 -  using prems
    10.8 +  using assms
    10.9  proof (induct xs arbitrary: env)
   10.10    case Nil
   10.11    then have False by simp
   10.12 @@ -140,7 +140,7 @@
   10.13  theorem lookup_append_some:
   10.14    assumes "lookup env xs = Some e"
   10.15    shows "lookup env (xs @ ys) = lookup e ys"
   10.16 -  using prems
   10.17 +  using assms
   10.18  proof (induct xs arbitrary: env e)
   10.19    case Nil
   10.20    then have "env = e" by simp
   10.21 @@ -190,7 +190,7 @@
   10.22    assumes "lookup env (xs @ ys) = Some e"
   10.23    shows "\<exists>e. lookup env xs = Some e"
   10.24  proof -
   10.25 -  from prems have "lookup env (xs @ ys) \<noteq> None" by simp
   10.26 +  from assms have "lookup env (xs @ ys) \<noteq> None" by simp
   10.27    then have "lookup env xs \<noteq> None"
   10.28      by (rule contrapos_nn) (simp only: lookup_append_none)
   10.29    then show ?thesis by (simp)
   10.30 @@ -208,7 +208,7 @@
   10.31      lookup env xs = Some (Env b' es') \<and>
   10.32      es' y = Some env' \<and>
   10.33      lookup env' ys = Some e"
   10.34 -  using prems
   10.35 +  using assms
   10.36  proof (induct xs arbitrary: env e)
   10.37    case Nil
   10.38    from Nil.prems have "lookup env (y # ys) = Some e"
   10.39 @@ -328,7 +328,7 @@
   10.40  theorem lookup_update_some:
   10.41    assumes "lookup env xs = Some e"
   10.42    shows "lookup (update xs (Some env') env) xs = Some env'"
   10.43 -  using prems
   10.44 +  using assms
   10.45  proof (induct xs arbitrary: env e)
   10.46    case Nil
   10.47    then have "env = e" by simp
   10.48 @@ -377,7 +377,7 @@
   10.49  theorem update_append_none:
   10.50    assumes "lookup env xs = None"
   10.51    shows "update (xs @ y # ys) opt env = env"
   10.52 -  using prems
   10.53 +  using assms
   10.54  proof (induct xs arbitrary: env)
   10.55    case Nil
   10.56    then have False by simp
   10.57 @@ -420,7 +420,7 @@
   10.58  theorem update_append_some:
   10.59    assumes "lookup env xs = Some e"
   10.60    shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
   10.61 -  using prems
   10.62 +  using assms
   10.63  proof (induct xs arbitrary: env e)
   10.64    case Nil
   10.65    then have "env = e" by simp
    11.1 --- a/src/HOL/Library/Quotient.thy	Thu Jun 14 23:04:36 2007 +0200
    11.2 +++ b/src/HOL/Library/Quotient.thy	Thu Jun 14 23:04:39 2007 +0200
    11.3 @@ -185,7 +185,7 @@
    11.4    assumes "!!X Y. f X Y == g (pick X) (pick Y)"
    11.5      and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
    11.6    shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
    11.7 -  using prems and TrueI
    11.8 +  using assms and TrueI
    11.9    by (rule quot_cond_function)
   11.10  
   11.11  theorem quot_function':
    12.1 --- a/src/HOL/Library/SCT_Implementation.thy	Thu Jun 14 23:04:36 2007 +0200
    12.2 +++ b/src/HOL/Library/SCT_Implementation.thy	Thu Jun 14 23:04:39 2007 +0200
    12.3 @@ -88,9 +88,9 @@
    12.4    assumes "A \<le> B"
    12.5    assumes "no_bad_graphs B"
    12.6    shows "no_bad_graphs A"
    12.7 -using prems
    12.8 -unfolding no_bad_graphs_def has_edge_def graph_leq_def 
    12.9 -by blast
   12.10 +  using assms
   12.11 +  unfolding no_bad_graphs_def has_edge_def graph_leq_def 
   12.12 +  by blast
   12.13  
   12.14  
   12.15  
    13.1 --- a/src/HOL/Library/SCT_Interpretation.thy	Thu Jun 14 23:04:36 2007 +0200
    13.2 +++ b/src/HOL/Library/SCT_Interpretation.thy	Thu Jun 14 23:04:39 2007 +0200
    13.3 @@ -74,7 +74,7 @@
    13.4  lemma some_rd:
    13.5    assumes "mk_rel rds x y"
    13.6    shows "\<exists>rd\<in>set rds. in_cdesc rd x y"
    13.7 -  using prems
    13.8 +  using assms
    13.9    by (induct rds) (auto simp:in_cdesc_def)
   13.10  
   13.11  (* from a value sequence, get a sequence of rds *)
   13.12 @@ -125,19 +125,19 @@
   13.13  
   13.14  
   13.15  lemma decr_in_cdesc:
   13.16 -  assumes	"in_cdesc RD1 y x"
   13.17 +  assumes "in_cdesc RD1 y x"
   13.18    assumes "in_cdesc RD2 z y"
   13.19    assumes "decr RD1 RD2 m1 m2"
   13.20    shows "m2 y < m1 x"
   13.21 -  using prems
   13.22 +  using assms
   13.23    by (cases RD1, cases RD2, auto simp:decr_def)
   13.24  
   13.25  lemma decreq_in_cdesc:
   13.26 -  assumes	"in_cdesc RD1 y x"
   13.27 +  assumes "in_cdesc RD1 y x"
   13.28    assumes "in_cdesc RD2 z y"
   13.29    assumes "decreq RD1 RD2 m1 m2"
   13.30    shows "m2 y \<le> m1 x"
   13.31 -  using prems
   13.32 +  using assms
   13.33    by (cases RD1, cases RD2, auto simp:decreq_def)
   13.34  
   13.35  
   13.36 @@ -208,7 +208,7 @@
   13.37    assumes "stepP c1 c2 (ms1 i) (ms2 j) (op <)"
   13.38    assumes "approx (Graph Es) c1 c2 ms1 ms2"
   13.39    shows "approx (Graph (insert (i, \<down>, j) Es)) c1 c2 ms1 ms2"
   13.40 -  using prems
   13.41 +  using assms
   13.42    unfolding approx_def has_edge_def dest_graph.simps decr_def
   13.43    by auto
   13.44  
   13.45 @@ -216,7 +216,7 @@
   13.46    assumes "stepP c1 c2 (ms1 i) (ms2 j) (op \<le>)"
   13.47    assumes "approx (Graph Es) c1 c2 ms1 ms2"
   13.48    shows "approx (Graph (insert (i, \<Down>, j) Es)) c1 c2 ms1 ms2"
   13.49 -  using prems
   13.50 +  using assms
   13.51    unfolding approx_def has_edge_def dest_graph.simps decreq_def
   13.52    by auto
   13.53  
   13.54 @@ -276,7 +276,7 @@
   13.55    assumes "in_cdesc RD1 y x"
   13.56    assumes "in_cdesc RD2 z y"
   13.57    shows "\<not> no_step RD1 RD2"
   13.58 -  using prems
   13.59 +  using assms
   13.60    by (cases RD1, cases RD2) (auto simp:no_step_def)
   13.61  
   13.62  
    14.1 --- a/src/HOL/Library/SCT_Misc.thy	Thu Jun 14 23:04:36 2007 +0200
    14.2 +++ b/src/HOL/Library/SCT_Misc.thy	Thu Jun 14 23:04:39 2007 +0200
    14.3 @@ -32,7 +32,7 @@
    14.4    assumes "a3 \<Longrightarrow> thesis"
    14.5    assumes "\<And>R. \<lbrakk>a1 \<Longrightarrow> R; a2 \<Longrightarrow> R; a3 \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
    14.6    shows "thesis"
    14.7 -  using prems
    14.8 +  using assms
    14.9    by auto
   14.10  
   14.11  
   14.12 @@ -44,32 +44,34 @@
   14.13  
   14.14  subsubsection {* Increasing sequences *}
   14.15  
   14.16 -definition increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
   14.17 -where
   14.18 +definition
   14.19 +  increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
   14.20    "increasing s = (\<forall>i j. i < j \<longrightarrow> s i < s j)"
   14.21  
   14.22  lemma increasing_strict:
   14.23    assumes "increasing s"
   14.24    assumes "i < j"
   14.25    shows "s i < s j"
   14.26 -  using prems
   14.27 +  using assms
   14.28    unfolding increasing_def by simp
   14.29  
   14.30  lemma increasing_weak:
   14.31    assumes "increasing s"
   14.32    assumes "i \<le> j"
   14.33    shows "s i \<le> s j"
   14.34 -  using prems increasing_strict[of s i j]
   14.35 -  by (cases "i<j") auto
   14.36 +  using assms increasing_strict[of s i j]
   14.37 +  by (cases "i < j") auto
   14.38  
   14.39  lemma increasing_inc:
   14.40 -  assumes [simp]: "increasing s"
   14.41 +  assumes "increasing s"
   14.42    shows "n \<le> s n"
   14.43  proof (induct n)
   14.44 +  case 0 then show ?case by simp
   14.45 +next
   14.46    case (Suc n)
   14.47 -  with increasing_strict[of s n "Suc n"]
   14.48 +  with increasing_strict [OF `increasing s`, of n "Suc n"]
   14.49    show ?case by auto
   14.50 -qed auto
   14.51 +qed
   14.52  
   14.53  lemma increasing_bij:
   14.54    assumes [simp]: "increasing s"
   14.55 @@ -162,10 +164,10 @@
   14.56  qed 
   14.57    
   14.58  lemma in_section_of: 
   14.59 -  assumes [simp, intro]: "increasing s"
   14.60 +  assumes "increasing s"
   14.61    assumes "s i \<le> k"
   14.62    shows "k \<in> section s (section_of s k)"
   14.63 -  using prems
   14.64 +  using assms
   14.65    by (auto intro:section_of1 section_of2)
   14.66  
   14.67  end
    15.1 --- a/src/HOL/Library/SCT_Theorem.thy	Thu Jun 14 23:04:36 2007 +0200
    15.2 +++ b/src/HOL/Library/SCT_Theorem.thy	Thu Jun 14 23:04:39 2007 +0200
    15.3 @@ -797,7 +797,7 @@
    15.4  
    15.5      have "i < s (Suc ?k)" by (rule section_of2) simp
    15.6      also have "\<dots> \<le> s j"
    15.7 -      by (rule increasing_weak [of s], assumption) (insert `?k < j`, arith)
    15.8 +      by (rule increasing_weak [OF `increasing s`]) (insert `?k < j`, arith)
    15.9      also note `\<dots> \<le> l`
   15.10      finally have "i < l" .
   15.11      with desc
    16.1 --- a/src/HOL/Unix/Unix.thy	Thu Jun 14 23:04:36 2007 +0200
    16.2 +++ b/src/HOL/Unix/Unix.thy	Thu Jun 14 23:04:39 2007 +0200
    16.3 @@ -591,7 +591,7 @@
    16.4    assumes "root =xs\<Rightarrow> root'"
    16.5      and "\<exists>att dir. root = Env att dir"
    16.6    shows "\<exists>att dir. root' = Env att dir"
    16.7 -  using transition_type_safe and prems
    16.8 +  using transition_type_safe and assms
    16.9  proof (rule transitions_invariant)
   16.10    show "\<forall>x \<in> set xs. True" by blast
   16.11  qed