tuned proofs: avoid implicit prems;
authorwenzelm
Wed Jun 13 18:30:11 2007 +0200 (2007-06-13)
changeset 23373ead82c82da9e
parent 23372 0035be079bee
child 23374 a2f492c599e0
tuned proofs: avoid implicit prems;
src/HOL/Bali/TypeSafe.thy
src/HOL/Extraction/Higman.thy
src/HOL/Extraction/QuotRem.thy
src/HOL/Extraction/Warshall.thy
src/HOL/IMP/Transition.thy
src/HOL/Isar_examples/BasicLogic.thy
src/HOL/Isar_examples/Cantor.thy
src/HOL/Isar_examples/ExprCompiler.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Isar_examples/NestedDatatype.thy
src/HOL/Isar_examples/Peirce.thy
src/HOL/Lattice/Bounds.thy
src/HOL/Lattice/CompleteLattice.thy
src/HOL/Lattice/Lattice.thy
src/HOL/Library/AssocList.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Graphs.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/SCT_Misc.thy
src/HOL/Library/SCT_Theorem.thy
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/NumberTheory/Euler.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/HOL/W0/W0.thy
src/HOL/ex/Commutative_Ring_Complete.thy
src/HOL/ex/Higher_Order_Logic.thy
src/HOL/ex/PER.thy
src/HOL/ex/ThreeDivides.thy
src/HOL/ex/Unification.thy
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Wed Jun 13 16:43:02 2007 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Wed Jun 13 18:30:11 2007 +0200
     1.3 @@ -2680,8 +2680,8 @@
     1.4      qed
     1.5    next
     1.6      case (Super s L accC T A)
     1.7 -    have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
     1.8 -    have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
     1.9 +    note conf_s = `Norm s\<Colon>\<preceq>(G, L)`
    1.10 +    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T`
    1.11      then obtain C c where
    1.12               C: "L This = Some (Class C)" and
    1.13         neq_Obj: "C\<noteq>Object" and
    1.14 @@ -3426,10 +3426,10 @@
    1.15        have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
    1.16  	by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
    1.17        moreover 
    1.18 -      have "s3 =
    1.19 +      note `s3 =
    1.20                  (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
    1.21                          abrupt s2 = Some (Jump (Cont l))
    1.22 -                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)" .
    1.23 +                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
    1.24        ultimately show ?thesis
    1.25  	by force
    1.26      qed
    1.27 @@ -3649,8 +3649,8 @@
    1.28  	from eval_e1 wt_e1 da_e1 wf True
    1.29  	have "nrm E1 \<subseteq> dom (locals (store s1))"
    1.30  	  by (cases rule: da_good_approxE') iprover
    1.31 -	with da_e2 show ?thesis
    1.32 -	  by (rule da_weakenE)
    1.33 +	with da_e2 show thesis
    1.34 +	  by (rule da_weakenE) (rule that)
    1.35        qed
    1.36        with conf_s1 wt_e2
    1.37        obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
     2.1 --- a/src/HOL/Extraction/Higman.thy	Wed Jun 13 16:43:02 2007 +0200
     2.2 +++ b/src/HOL/Extraction/Higman.thy	Wed Jun 13 18:30:11 2007 +0200
     2.3 @@ -146,16 +146,18 @@
     2.4    assumes ab: "a \<noteq> b" and bar: "bar xs"
     2.5    shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar
     2.6  proof induct
     2.7 -  fix xs zs assume "good xs" and "T a xs zs"
     2.8 -  show "bar zs" by (rule bar1) (rule lemma3)
     2.9 +  fix xs zs assume "T a xs zs" and "good xs"
    2.10 +  hence "good zs" by (rule lemma3)
    2.11 +  then show "bar zs" by (rule bar1)
    2.12  next
    2.13    fix xs ys
    2.14    assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
    2.15    assume "bar ys"
    2.16    thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
    2.17    proof induct
    2.18 -    fix ys zs assume "good ys" and "T b ys zs"
    2.19 -    show "bar zs" by (rule bar1) (rule lemma3)
    2.20 +    fix ys zs assume "T b ys zs" and "good ys"
    2.21 +    then have "good zs" by (rule lemma3)
    2.22 +    then show "bar zs" by (rule bar1)
    2.23    next
    2.24      fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs"
    2.25      and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs"
    2.26 @@ -189,8 +191,9 @@
    2.27    shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar
    2.28  proof induct
    2.29    fix xs zs
    2.30 -  assume "good xs" and "R a xs zs"
    2.31 -  show "bar zs" by (rule bar1) (rule lemma2)
    2.32 +  assume "R a xs zs" and "good xs"
    2.33 +  then have "good zs" by (rule lemma2)
    2.34 +  then show "bar zs" by (rule bar1)
    2.35  next
    2.36    fix xs zs
    2.37    assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs"
    2.38 @@ -299,7 +302,7 @@
    2.39    thus ?case by iprover
    2.40  next
    2.41    case (bar2 ws)
    2.42 -  have "is_prefix (f (length ws) # ws) f" by simp
    2.43 +  from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp
    2.44    thus ?case by (iprover intro: bar2)
    2.45  qed
    2.46  
     3.1 --- a/src/HOL/Extraction/QuotRem.thy	Wed Jun 13 16:43:02 2007 +0200
     3.2 +++ b/src/HOL/Extraction/QuotRem.thy	Wed Jun 13 18:30:11 2007 +0200
     3.3 @@ -30,7 +30,7 @@
     3.4      thus ?case by iprover
     3.5    next
     3.6      assume "r \<noteq> b"
     3.7 -    hence "r < b" by (simp add: order_less_le)
     3.8 +    with `r \<le> b` have "r < b" by (simp add: order_less_le)
     3.9      with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp
    3.10      thus ?case by iprover
    3.11    qed
     4.1 --- a/src/HOL/Extraction/Warshall.thy	Wed Jun 13 16:43:02 2007 +0200
     4.2 +++ b/src/HOL/Extraction/Warshall.thy	Wed Jun 13 18:30:11 2007 +0200
     4.3 @@ -111,9 +111,10 @@
     4.4     (\<exists>q. is_path r q i j i) \<and> (\<exists>q'. is_path r q' i i k)"
     4.5  proof (simp cong add: conj_cong add: split_paired_all is_path_def, (erule conjE)+)
     4.6    fix xs
     4.7 -  assume "list_all (\<lambda>x. x < Suc i) xs"
     4.8 -  assume "is_path' r j xs k"
     4.9 -  assume "\<not> list_all (\<lambda>x. x < i) xs"
    4.10 +  assume asms:
    4.11 +    "list_all (\<lambda>x. x < Suc i) xs"
    4.12 +    "is_path' r j xs k"
    4.13 +    "\<not> list_all (\<lambda>x. x < i) xs"
    4.14    show "(\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i) \<and>
    4.15      (\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k)"
    4.16    proof
    4.17 @@ -182,7 +183,7 @@
    4.18        	qed
    4.19        qed
    4.20      qed
    4.21 -  qed
    4.22 +  qed (rule asms)+
    4.23  qed
    4.24  
    4.25  theorem lemma5':
     5.1 --- a/src/HOL/IMP/Transition.thy	Wed Jun 13 16:43:02 2007 +0200
     5.2 +++ b/src/HOL/IMP/Transition.thy	Wed Jun 13 18:30:11 2007 +0200
     5.3 @@ -366,7 +366,7 @@
     5.4    "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
     5.5  proof
     5.6    assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
     5.7 -  show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
     5.8 +  then show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
     5.9  next
    5.10    assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
    5.11    then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
    5.12 @@ -460,7 +460,7 @@
    5.13  proof -
    5.14    assume "\<not>b s"
    5.15    have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
    5.16 -  also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
    5.17 +  also from `\<not>b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
    5.18    also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" ..
    5.19    finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
    5.20  qed
    5.21 @@ -471,7 +471,7 @@
    5.22  proof -
    5.23    assume "b s"
    5.24    have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
    5.25 -  also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
    5.26 +  also from `b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
    5.27    finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
    5.28  qed
    5.29  
     6.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Jun 13 16:43:02 2007 +0200
     6.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Jun 13 18:30:11 2007 +0200
     6.3 @@ -45,8 +45,8 @@
     6.4        assume A
     6.5        show C
     6.6        proof (rule mp)
     6.7 -        show "B --> C" by (rule mp)
     6.8 -        show B by (rule mp)
     6.9 +        show "B --> C" by (rule mp) assumption+
    6.10 +        show B by (rule mp) assumption+
    6.11        qed
    6.12      qed
    6.13    qed
    6.14 @@ -65,7 +65,7 @@
    6.15  lemma "A --> A"
    6.16  proof
    6.17    assume A
    6.18 -  show A .
    6.19 +  show A by assumption
    6.20  qed
    6.21  
    6.22  text {*
    6.23 @@ -117,7 +117,7 @@
    6.24  lemma "A --> B --> A"
    6.25  proof (intro impI)
    6.26    assume A
    6.27 -  show A .
    6.28 +  show A by assumption
    6.29  qed
    6.30  
    6.31  text {*
    6.32 @@ -162,8 +162,8 @@
    6.33    assume "A & B"
    6.34    show "B & A"
    6.35    proof
    6.36 -    show B by (rule conjunct2)
    6.37 -    show A by (rule conjunct1)
    6.38 +    show B by (rule conjunct2) assumption
    6.39 +    show A by (rule conjunct1) assumption
    6.40    qed
    6.41  qed
    6.42  
    6.43 @@ -171,10 +171,9 @@
    6.44    Above, the @{text "conjunct_1/2"} projection rules had to be named
    6.45    explicitly, since the goals @{text B} and @{text A} did not provide
    6.46    any structural clue.  This may be avoided using \isacommand{from} to
    6.47 -  focus on @{text prems} (i.e.\ the @{text "A \<and> B"} assumption) as the
    6.48 -  current facts, enabling the use of double-dot proofs.  Note that
    6.49 -  \isacommand{from} already does forward-chaining, involving the
    6.50 -  \name{conjE} rule here.
    6.51 +  focus on the @{text "A \<and> B"} assumption as the current facts,
    6.52 +  enabling the use of double-dot proofs.  Note that \isacommand{from}
    6.53 +  already does forward-chaining, involving the \name{conjE} rule here.
    6.54  *}
    6.55  
    6.56  lemma "A & B --> B & A"
    6.57 @@ -182,8 +181,8 @@
    6.58    assume "A & B"
    6.59    show "B & A"
    6.60    proof
    6.61 -    from prems show B ..
    6.62 -    from prems show A ..
    6.63 +    from `A & B` show B ..
    6.64 +    from `A & B` show A ..
    6.65    qed
    6.66  qed
    6.67  
    6.68 @@ -202,8 +201,8 @@
    6.69    assume "A & B"
    6.70    then show "B & A"
    6.71    proof                    -- {* rule @{text conjE} of @{text "A \<and> B"} *}
    6.72 -    assume A B
    6.73 -    show ?thesis ..       -- {* rule @{text conjI} of @{text "B \<and> A"} *}
    6.74 +    assume B A
    6.75 +    then show ?thesis ..   -- {* rule @{text conjI} of @{text "B \<and> A"} *}
    6.76    qed
    6.77  qed
    6.78  
    6.79 @@ -215,10 +214,10 @@
    6.80  
    6.81  lemma "A & B --> B & A"
    6.82  proof
    6.83 -  assume ab: "A & B"
    6.84 -  from ab have a: A ..
    6.85 -  from ab have b: B ..
    6.86 -  from b a show "B & A" ..
    6.87 +  assume "A & B"
    6.88 +  from `A & B` have A ..
    6.89 +  from `A & B` have B ..
    6.90 +  from `B` `A` show "B & A" ..
    6.91  qed
    6.92  
    6.93  text {*
    6.94 @@ -230,12 +229,12 @@
    6.95  lemma "A & B --> B & A"
    6.96  proof -
    6.97    {
    6.98 -    assume ab: "A & B"
    6.99 -    from ab have a: A ..
   6.100 -    from ab have b: B ..
   6.101 -    from b a have "B & A" ..
   6.102 +    assume "A & B"
   6.103 +    from `A & B` have A ..
   6.104 +    from `A & B` have B ..
   6.105 +    from `B` `A` have "B & A" ..
   6.106    }
   6.107 -  thus ?thesis ..         -- {* rule \name{impI} *}
   6.108 +  then show ?thesis ..         -- {* rule \name{impI} *}
   6.109  qed
   6.110  
   6.111  text {*
   6.112 @@ -258,19 +257,16 @@
   6.113  text {*
   6.114    For our example the most appropriate way of reasoning is probably
   6.115    the middle one, with conjunction introduction done after
   6.116 -  elimination.  This reads even more concisely using
   6.117 -  \isacommand{thus}, which abbreviates
   6.118 -  \isacommand{then}~\isacommand{show}.\footnote{In the same vein,
   6.119 -  \isacommand{hence} abbreviates \isacommand{then}~\isacommand{have}.}
   6.120 +  elimination.
   6.121  *}
   6.122  
   6.123  lemma "A & B --> B & A"
   6.124  proof
   6.125    assume "A & B"
   6.126 -  thus "B & A"
   6.127 +  then show "B & A"
   6.128    proof
   6.129 -    assume A B
   6.130 -    show ?thesis ..
   6.131 +    assume B A
   6.132 +    then show ?thesis ..
   6.133    qed
   6.134  qed
   6.135  
   6.136 @@ -294,13 +290,13 @@
   6.137  lemma "P | P --> P"
   6.138  proof
   6.139    assume "P | P"
   6.140 -  thus P
   6.141 +  then show P
   6.142    proof                    -- {*
   6.143      rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
   6.144    *}
   6.145 -    assume P show P .
   6.146 +    assume P show P by assumption
   6.147    next
   6.148 -    assume P show P .
   6.149 +    assume P show P by assumption
   6.150    qed
   6.151  qed
   6.152  
   6.153 @@ -331,11 +327,11 @@
   6.154  lemma "P | P --> P"
   6.155  proof
   6.156    assume "P | P"
   6.157 -  thus P
   6.158 +  then show P
   6.159    proof
   6.160      assume P
   6.161 -    show P .
   6.162 -    show P .
   6.163 +    show P by assumption
   6.164 +    show P by assumption
   6.165    qed
   6.166  qed
   6.167  
   6.168 @@ -349,7 +345,7 @@
   6.169  lemma "P | P --> P"
   6.170  proof
   6.171    assume "P | P"
   6.172 -  thus P ..
   6.173 +  then show P ..
   6.174  qed
   6.175  
   6.176  
   6.177 @@ -372,13 +368,13 @@
   6.178  lemma "(EX x. P (f x)) --> (EX y. P y)"
   6.179  proof
   6.180    assume "EX x. P (f x)"
   6.181 -  thus "EX y. P y"
   6.182 +  then show "EX y. P y"
   6.183    proof (rule exE)             -- {*
   6.184      rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
   6.185    *}
   6.186      fix a
   6.187      assume "P (f a)" (is "P ?witness")
   6.188 -    show ?thesis by (rule exI [of P ?witness])
   6.189 +    then show ?thesis by (rule exI [of P ?witness])
   6.190    qed
   6.191  qed
   6.192  
   6.193 @@ -394,11 +390,11 @@
   6.194  lemma "(EX x. P (f x)) --> (EX y. P y)"
   6.195  proof
   6.196    assume "EX x. P (f x)"
   6.197 -  thus "EX y. P y"
   6.198 +  then show "EX y. P y"
   6.199    proof
   6.200      fix a
   6.201      assume "P (f a)"
   6.202 -    show ?thesis ..
   6.203 +    then show ?thesis ..
   6.204    qed
   6.205  qed
   6.206  
   6.207 @@ -413,7 +409,7 @@
   6.208  proof
   6.209    assume "EX x. P (f x)"
   6.210    then obtain a where "P (f a)" ..
   6.211 -  thus "EX y. P y" ..
   6.212 +  then show "EX y. P y" ..
   6.213  qed
   6.214  
   6.215  text {*
   6.216 @@ -443,18 +439,9 @@
   6.217    assume r: "A ==> B ==> C"
   6.218    show C
   6.219    proof (rule r)
   6.220 -    show A by (rule conjunct1)
   6.221 -    show B by (rule conjunct2)
   6.222 +    show A by (rule conjunct1) assumption
   6.223 +    show B by (rule conjunct2) assumption
   6.224    qed
   6.225  qed
   6.226  
   6.227 -text {*
   6.228 -  Note that classic Isabelle handles higher rules in a slightly
   6.229 -  different way.  The tactic script as given in \cite{isabelle-intro}
   6.230 -  for the same example of \name{conjE} depends on the primitive
   6.231 -  \texttt{goal} command to decompose the rule into premises and
   6.232 -  conclusion.  The actual result would then emerge by discharging of
   6.233 -  the context at \texttt{qed} time.
   6.234 -*}
   6.235 -
   6.236  end
     7.1 --- a/src/HOL/Isar_examples/Cantor.thy	Wed Jun 13 16:43:02 2007 +0200
     7.2 +++ b/src/HOL/Isar_examples/Cantor.thy	Wed Jun 13 18:30:11 2007 +0200
     7.3 @@ -34,15 +34,15 @@
     7.4    proof
     7.5      assume "?S : range f"
     7.6      then obtain y where "?S = f y" ..
     7.7 -    thus False
     7.8 +    then show False
     7.9      proof (rule equalityCE)
    7.10        assume "y : f y"
    7.11 -      assume "y : ?S" hence "y ~: f y" ..
    7.12 -      thus ?thesis by contradiction
    7.13 +      assume "y : ?S" then have "y ~: f y" ..
    7.14 +      with `y : f y` show ?thesis by contradiction
    7.15      next
    7.16        assume "y ~: ?S"
    7.17 -      assume "y ~: f y" hence "y : ?S" ..
    7.18 -      thus ?thesis by contradiction
    7.19 +      assume "y ~: f y" then have "y : ?S" ..
    7.20 +      with `y ~: ?S` show ?thesis by contradiction
    7.21      qed
    7.22    qed
    7.23  qed
     8.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Wed Jun 13 16:43:02 2007 +0200
     8.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Wed Jun 13 18:30:11 2007 +0200
     8.3 @@ -121,11 +121,14 @@
     8.4    case (Cons x xs)
     8.5    show ?case
     8.6    proof (induct x)
     8.7 -    case Const show ?case by simp
     8.8 +    case Const
     8.9 +    from Cons show ?case by simp
    8.10    next
    8.11 -    case Load show ?case by simp
    8.12 +    case Load
    8.13 +    from Cons show ?case by simp
    8.14    next
    8.15 -    case Apply show ?case by simp
    8.16 +    case Apply
    8.17 +    from Cons show ?case by simp
    8.18    qed
    8.19  qed
    8.20  
    8.21 @@ -139,7 +142,7 @@
    8.22    next
    8.23      case Binop then show ?case by (simp add: exec_append)
    8.24    qed
    8.25 -  thus ?thesis by (simp add: execute_def)
    8.26 +  then show ?thesis by (simp add: execute_def)
    8.27  qed
    8.28  
    8.29  
     9.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Jun 13 16:43:02 2007 +0200
     9.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Jun 13 18:30:11 2007 +0200
     9.3 @@ -43,12 +43,12 @@
     9.4      show "(a Un t) Un u : ?T"
     9.5      proof -
     9.6        have "a Un (t Un u) : ?T"
     9.7 +	using `a : A`
     9.8        proof (rule tiling.Un)
     9.9 -        show "a : A" .
    9.10          from `(a Un t) Int u = {}` have "t Int u = {}" by blast
    9.11          then show "t Un u: ?T" by (rule Un)
    9.12 -        have "a <= - t" .
    9.13 -        with `(a Un t) Int u = {}` show "a <= - (t Un u)" by blast
    9.14 +        from `a <= - t` and `(a Un t) Int u = {}`
    9.15 +	show "a <= - (t Un u)" by blast
    9.16        qed
    9.17        also have "a Un (t Un u) = (a Un t) Un u"
    9.18          by (simp only: Un_assoc)
    9.19 @@ -201,7 +201,7 @@
    9.20    show "?F {}" by (rule finite.emptyI)
    9.21    fix a t assume "?F t"
    9.22    assume "a : domino" then have "?F a" by (rule domino_finite)
    9.23 -  then show "?F (a Un t)" by (rule finite_UnI)
    9.24 +  from this and `?F t` show "?F (a Un t)" by (rule finite_UnI)
    9.25  qed
    9.26  
    9.27  lemma tiling_domino_01:
    9.28 @@ -223,14 +223,17 @@
    9.29      have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
    9.30      also obtain i j where e: "?e a b = {(i, j)}"
    9.31      proof -
    9.32 +      from `a \<in> domino` and `b < 2`
    9.33        have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
    9.34        then show ?thesis by (blast intro: that)
    9.35      qed
    9.36      also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
    9.37      also have "card ... = Suc (card (?e t b))"
    9.38      proof (rule card_insert_disjoint)
    9.39 -      show "finite (?e t b)"
    9.40 -        by (rule evnodd_finite, rule tiling_domino_finite)
    9.41 +      from `t \<in> tiling domino` have "finite t"
    9.42 +	by (rule tiling_domino_finite)
    9.43 +      then show "finite (?e t b)"
    9.44 +        by (rule evnodd_finite)
    9.45        from e have "(i, j) : ?e a b" by simp
    9.46        with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
    9.47      qed
    10.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Wed Jun 13 16:43:02 2007 +0200
    10.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Wed Jun 13 18:30:11 2007 +0200
    10.3 @@ -44,12 +44,14 @@
    10.4      fix a show "?P (Var a)" by simp
    10.5    next
    10.6      fix b ts assume "?Q ts"
    10.7 -    thus "?P (App b ts)" by (simp add: o_def)
    10.8 +    then show "?P (App b ts)"
    10.9 +      by (simp only: subst.simps)
   10.10    next
   10.11      show "?Q []" by simp
   10.12    next
   10.13      fix t ts
   10.14 -    assume "?P t" "?Q ts" thus "?Q (t # ts)" by simp
   10.15 +    assume "?P t" "?Q ts" then show "?Q (t # ts)"
   10.16 +      by (simp only: subst.simps)
   10.17    qed
   10.18  qed
   10.19  
   10.20 @@ -64,12 +66,12 @@
   10.21    fix a show "P (Var a)" by (rule var)
   10.22  next
   10.23    fix b t ts assume "list_all P ts"
   10.24 -  thus "P (App b ts)" by (rule app)
   10.25 +  then show "P (App b ts)" by (rule app)
   10.26  next
   10.27    show "list_all P []" by simp
   10.28  next
   10.29    fix t ts assume "P t" "list_all P ts"
   10.30 -  thus "list_all P (t # ts)" by simp
   10.31 +  then show "list_all P (t # ts)" by simp
   10.32  qed
   10.33  
   10.34  lemma
   10.35 @@ -79,7 +81,7 @@
   10.36    show ?case by (simp add: o_def)
   10.37  next
   10.38    case (App b ts)
   10.39 -  thus ?case by (induct ts) simp_all
   10.40 +  then show ?case by (induct ts) simp_all
   10.41  qed
   10.42  
   10.43  end
    11.1 --- a/src/HOL/Isar_examples/Peirce.thy	Wed Jun 13 16:43:02 2007 +0200
    11.2 +++ b/src/HOL/Isar_examples/Peirce.thy	Wed Jun 13 18:30:11 2007 +0200
    11.3 @@ -21,16 +21,16 @@
    11.4  
    11.5  theorem "((A --> B) --> A) --> A"
    11.6  proof
    11.7 -  assume aba: "(A --> B) --> A"
    11.8 +  assume "(A --> B) --> A"
    11.9    show A
   11.10    proof (rule classical)
   11.11      assume "~ A"
   11.12      have "A --> B"
   11.13      proof
   11.14        assume A
   11.15 -      thus B by contradiction
   11.16 +      with `~ A` show B by contradiction
   11.17      qed
   11.18 -    with aba show A ..
   11.19 +    with `(A --> B) --> A` show A ..
   11.20    qed
   11.21  qed
   11.22  
   11.23 @@ -52,17 +52,17 @@
   11.24  
   11.25  theorem "((A --> B) --> A) --> A"
   11.26  proof
   11.27 -  assume aba: "(A --> B) --> A"
   11.28 +  assume "(A --> B) --> A"
   11.29    show A
   11.30    proof (rule classical)
   11.31      presume "A --> B"
   11.32 -    with aba show A ..
   11.33 +    with `(A --> B) --> A` show A ..
   11.34    next
   11.35      assume "~ A"
   11.36      show "A --> B"
   11.37      proof
   11.38        assume A
   11.39 -      thus B by contradiction
   11.40 +      with `~ A` show B by contradiction
   11.41      qed
   11.42    qed
   11.43  qed
    12.1 --- a/src/HOL/Lattice/Bounds.thy	Wed Jun 13 16:43:02 2007 +0200
    12.2 +++ b/src/HOL/Lattice/Bounds.thy	Wed Jun 13 18:30:11 2007 +0200
    12.3 @@ -147,7 +147,7 @@
    12.4      from sup show "is_inf (dual x) (dual y) (dual sup)" ..
    12.5      from sup' show "is_inf (dual x) (dual y) (dual sup')" ..
    12.6    qed
    12.7 -  thus "sup = sup'" ..
    12.8 +  then show "sup = sup'" ..
    12.9  qed
   12.10  
   12.11  theorem is_Inf_uniq: "is_Inf A inf \<Longrightarrow> is_Inf A inf' \<Longrightarrow> inf = inf'"
   12.12 @@ -159,12 +159,12 @@
   12.13      from inf' show "inf \<sqsubseteq> inf'"
   12.14      proof (rule is_Inf_greatest)
   12.15        fix x assume "x \<in> A"
   12.16 -      from inf show "inf \<sqsubseteq> x" ..
   12.17 +      with inf show "inf \<sqsubseteq> x" ..
   12.18      qed
   12.19      from inf show "inf' \<sqsubseteq> inf"
   12.20      proof (rule is_Inf_greatest)
   12.21        fix x assume "x \<in> A"
   12.22 -      from inf' show "inf' \<sqsubseteq> x" ..
   12.23 +      with inf' show "inf' \<sqsubseteq> x" ..
   12.24      qed
   12.25    qed
   12.26  qed
   12.27 @@ -177,7 +177,7 @@
   12.28      from sup show "is_Inf (dual ` A) (dual sup)" ..
   12.29      from sup' show "is_Inf (dual ` A) (dual sup')" ..
   12.30    qed
   12.31 -  thus "sup = sup'" ..
   12.32 +  then show "sup = sup'" ..
   12.33  qed
   12.34  
   12.35  
   12.36 @@ -193,8 +193,8 @@
   12.37    show ?thesis
   12.38    proof
   12.39      show "x \<sqsubseteq> x" ..
   12.40 -    show "x \<sqsubseteq> y" .
   12.41 -    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" .
   12.42 +    show "x \<sqsubseteq> y" by assumption
   12.43 +    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by assumption
   12.44    qed
   12.45  qed
   12.46  
   12.47 @@ -203,10 +203,10 @@
   12.48    assume "x \<sqsubseteq> y"
   12.49    show ?thesis
   12.50    proof
   12.51 -    show "x \<sqsubseteq> y" .
   12.52 +    show "x \<sqsubseteq> y" by assumption
   12.53      show "y \<sqsubseteq> y" ..
   12.54      fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
   12.55 -    show "y \<sqsubseteq> z" .
   12.56 +    show "y \<sqsubseteq> z" by assumption
   12.57    qed
   12.58  qed
   12.59  
   12.60 @@ -233,8 +233,8 @@
   12.61        from is_Inf show "z \<sqsubseteq> inf"
   12.62        proof (rule is_Inf_greatest)
   12.63          fix a assume "a \<in> ?A"
   12.64 -        hence "a = x \<or> a = y" by blast
   12.65 -        thus "z \<sqsubseteq> a"
   12.66 +        then have "a = x \<or> a = y" by blast
   12.67 +        then show "z \<sqsubseteq> a"
   12.68          proof
   12.69            assume "a = x"
   12.70            with zx show ?thesis by simp
   12.71 @@ -249,8 +249,8 @@
   12.72      show "is_Inf {x, y} inf"
   12.73      proof
   12.74        fix a assume "a \<in> ?A"
   12.75 -      hence "a = x \<or> a = y" by blast
   12.76 -      thus "inf \<sqsubseteq> a"
   12.77 +      then have "a = x \<or> a = y" by blast
   12.78 +      then show "inf \<sqsubseteq> a"
   12.79        proof
   12.80          assume "a = x"
   12.81          also from is_inf have "inf \<sqsubseteq> x" ..
   12.82 @@ -304,12 +304,12 @@
   12.83      from is_Inf show "x \<sqsubseteq> sup"
   12.84      proof (rule is_Inf_greatest)
   12.85        fix y assume "y \<in> ?B"
   12.86 -      hence "\<forall>a \<in> A. a \<sqsubseteq> y" ..
   12.87 +      then have "\<forall>a \<in> A. a \<sqsubseteq> y" ..
   12.88        from this x show "x \<sqsubseteq> y" ..
   12.89      qed
   12.90    next
   12.91      fix z assume "\<forall>x \<in> A. x \<sqsubseteq> z"
   12.92 -    hence "z \<in> ?B" ..
   12.93 +    then have "z \<in> ?B" ..
   12.94      with is_Inf show "sup \<sqsubseteq> z" ..
   12.95    qed
   12.96  qed
   12.97 @@ -317,14 +317,14 @@
   12.98  theorem Sup_Inf: "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf \<Longrightarrow> is_Inf A inf"
   12.99  proof -
  12.100    assume "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf"
  12.101 -  hence "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
  12.102 +  then have "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
  12.103      by (simp only: dual_Inf dual_leq)
  12.104    also have "dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual ` A. a' \<sqsubseteq> b'}"
  12.105      by (auto iff: dual_ball dual_Collect simp add: image_Collect)  (* FIXME !? *)
  12.106    finally have "is_Inf \<dots> (dual inf)" .
  12.107 -  hence "is_Sup (dual ` A) (dual inf)"
  12.108 +  then have "is_Sup (dual ` A) (dual inf)"
  12.109      by (rule Inf_Sup)
  12.110 -  thus ?thesis ..
  12.111 +  then show ?thesis ..
  12.112  qed
  12.113  
  12.114  end
    13.1 --- a/src/HOL/Lattice/CompleteLattice.thy	Wed Jun 13 16:43:02 2007 +0200
    13.2 +++ b/src/HOL/Lattice/CompleteLattice.thy	Wed Jun 13 18:30:11 2007 +0200
    13.3 @@ -22,8 +22,8 @@
    13.4  theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"
    13.5  proof -
    13.6    from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast
    13.7 -  hence "is_Sup A sup" by (rule Inf_Sup)
    13.8 -  thus ?thesis ..
    13.9 +  then have "is_Sup A sup" by (rule Inf_Sup)
   13.10 +  then show ?thesis ..
   13.11  qed
   13.12  
   13.13  text {*
   13.14 @@ -50,8 +50,8 @@
   13.15  lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf"
   13.16  proof (unfold Meet_def)
   13.17    assume "is_Inf A inf"
   13.18 -  thus "(THE inf. is_Inf A inf) = inf"
   13.19 -    by (rule the_equality) (rule is_Inf_uniq)
   13.20 +  then show "(THE inf. is_Inf A inf) = inf"
   13.21 +    by (rule the_equality) (rule is_Inf_uniq [OF _ `is_Inf A inf`])
   13.22  qed
   13.23  
   13.24  lemma MeetI [intro?]:
   13.25 @@ -63,8 +63,8 @@
   13.26  lemma Join_equality [elim?]: "is_Sup A sup \<Longrightarrow> \<Squnion>A = sup"
   13.27  proof (unfold Join_def)
   13.28    assume "is_Sup A sup"
   13.29 -  thus "(THE sup. is_Sup A sup) = sup"
   13.30 -    by (rule the_equality) (rule is_Sup_uniq)
   13.31 +  then show "(THE sup. is_Sup A sup) = sup"
   13.32 +    by (rule the_equality) (rule is_Sup_uniq [OF _ `is_Sup A sup`])
   13.33  qed
   13.34  
   13.35  lemma JoinI [intro?]:
   13.36 @@ -82,7 +82,8 @@
   13.37  lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
   13.38  proof (unfold Meet_def)
   13.39    from ex_Inf obtain inf where "is_Inf A inf" ..
   13.40 -  thus "is_Inf A (THE inf. is_Inf A inf)" by (rule theI) (rule is_Inf_uniq)
   13.41 +  then show "is_Inf A (THE inf. is_Inf A inf)"
   13.42 +    by (rule theI) (rule is_Inf_uniq [OF _ `is_Inf A inf`])
   13.43  qed
   13.44  
   13.45  lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
   13.46 @@ -95,7 +96,8 @@
   13.47  lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
   13.48  proof (unfold Join_def)
   13.49    from ex_Sup obtain sup where "is_Sup A sup" ..
   13.50 -  thus "is_Sup A (THE sup. is_Sup A sup)" by (rule theI) (rule is_Sup_uniq)
   13.51 +  then show "is_Sup A (THE sup. is_Sup A sup)"
   13.52 +    by (rule theI) (rule is_Sup_uniq [OF _ `is_Sup A sup`])
   13.53  qed
   13.54  
   13.55  lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
   13.56 @@ -122,15 +124,15 @@
   13.57    have ge: "f ?a \<sqsubseteq> ?a"
   13.58    proof
   13.59      fix x assume x: "x \<in> ?H"
   13.60 -    hence "?a \<sqsubseteq> x" ..
   13.61 -    hence "f ?a \<sqsubseteq> f x" by (rule mono)
   13.62 +    then have "?a \<sqsubseteq> x" ..
   13.63 +    then have "f ?a \<sqsubseteq> f x" by (rule mono)
   13.64      also from x have "... \<sqsubseteq> x" ..
   13.65      finally show "f ?a \<sqsubseteq> x" .
   13.66    qed
   13.67    also have "?a \<sqsubseteq> f ?a"
   13.68    proof
   13.69      from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
   13.70 -    thus "f ?a \<in> ?H" ..
   13.71 +    then show "f ?a \<in> ?H" ..
   13.72    qed
   13.73    finally show "f ?a = ?a" .
   13.74  qed
   13.75 @@ -153,7 +155,7 @@
   13.76  lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
   13.77  proof (unfold bottom_def)
   13.78    have "x \<in> UNIV" ..
   13.79 -  thus "\<Sqinter>UNIV \<sqsubseteq> x" ..
   13.80 +  then show "\<Sqinter>UNIV \<sqsubseteq> x" ..
   13.81  qed
   13.82  
   13.83  lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x"
   13.84 @@ -161,7 +163,7 @@
   13.85    assume "\<And>a. x \<sqsubseteq> a"
   13.86    show "\<Sqinter>UNIV = x"
   13.87    proof
   13.88 -    fix a show "x \<sqsubseteq> a" .
   13.89 +    fix a show "x \<sqsubseteq> a" by fact
   13.90    next
   13.91      fix b :: "'a::complete_lattice"
   13.92      assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a"
   13.93 @@ -173,7 +175,7 @@
   13.94  lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>"
   13.95  proof (unfold top_def)
   13.96    have "x \<in> UNIV" ..
   13.97 -  thus "x \<sqsubseteq> \<Squnion>UNIV" ..
   13.98 +  then show "x \<sqsubseteq> \<Squnion>UNIV" ..
   13.99  qed
  13.100  
  13.101  lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x"
  13.102 @@ -181,7 +183,7 @@
  13.103    assume "\<And>a. a \<sqsubseteq> x"
  13.104    show "\<Squnion>UNIV = x"
  13.105    proof
  13.106 -    fix a show "a \<sqsubseteq> x" .
  13.107 +    fix a show "a \<sqsubseteq> x" by fact
  13.108    next
  13.109      fix b :: "'a::complete_lattice"
  13.110      assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b"
  13.111 @@ -204,8 +206,8 @@
  13.112    show "\<exists>inf'. is_Inf A' inf'"
  13.113    proof -
  13.114      have "\<exists>sup. is_Sup (undual ` A') sup" by (rule ex_Sup)
  13.115 -    hence "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
  13.116 -    thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
  13.117 +    then have "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
  13.118 +    then show ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
  13.119    qed
  13.120  qed
  13.121  
  13.122 @@ -217,15 +219,15 @@
  13.123  theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual ` A)"
  13.124  proof -
  13.125    from is_Inf_Meet have "is_Sup (dual ` A) (dual (\<Sqinter>A))" ..
  13.126 -  hence "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" ..
  13.127 -  thus ?thesis ..
  13.128 +  then have "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" ..
  13.129 +  then show ?thesis ..
  13.130  qed
  13.131  
  13.132  theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual ` A)"
  13.133  proof -
  13.134    from is_Sup_Join have "is_Inf (dual ` A) (dual (\<Squnion>A))" ..
  13.135 -  hence "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" ..
  13.136 -  thus ?thesis ..
  13.137 +  then have "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" ..
  13.138 +  then show ?thesis ..
  13.139  qed
  13.140  
  13.141  text {*
  13.142 @@ -237,10 +239,10 @@
  13.143    have "\<top> = dual \<bottom>"
  13.144    proof
  13.145      fix a' have "\<bottom> \<sqsubseteq> undual a'" ..
  13.146 -    hence "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
  13.147 -    thus "a' \<sqsubseteq> dual \<bottom>" by simp
  13.148 +    then have "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
  13.149 +    then show "a' \<sqsubseteq> dual \<bottom>" by simp
  13.150    qed
  13.151 -  thus ?thesis ..
  13.152 +  then show ?thesis ..
  13.153  qed
  13.154  
  13.155  theorem dual_top [intro?]: "dual \<top> = \<bottom>"
  13.156 @@ -248,10 +250,10 @@
  13.157    have "\<bottom> = dual \<top>"
  13.158    proof
  13.159      fix a' have "undual a' \<sqsubseteq> \<top>" ..
  13.160 -    hence "dual \<top> \<sqsubseteq> dual (undual a')" ..
  13.161 -    thus "dual \<top> \<sqsubseteq> a'" by simp
  13.162 +    then have "dual \<top> \<sqsubseteq> dual (undual a')" ..
  13.163 +    then show "dual \<top> \<sqsubseteq> a'" by simp
  13.164    qed
  13.165 -  thus ?thesis ..
  13.166 +  then show ?thesis ..
  13.167  qed
  13.168  
  13.169  
  13.170 @@ -267,13 +269,13 @@
  13.171  lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})"
  13.172  proof -
  13.173    have "is_Inf {x, y} (\<Sqinter>{x, y})" ..
  13.174 -  thus ?thesis by (simp only: is_Inf_binary)
  13.175 +  then show ?thesis by (simp only: is_Inf_binary)
  13.176  qed
  13.177  
  13.178  lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})"
  13.179  proof -
  13.180    have "is_Sup {x, y} (\<Squnion>{x, y})" ..
  13.181 -  thus ?thesis by (simp only: is_Sup_binary)
  13.182 +  then show ?thesis by (simp only: is_Sup_binary)
  13.183  qed
  13.184  
  13.185  instance complete_lattice \<subseteq> lattice
  13.186 @@ -302,16 +304,16 @@
  13.187    fix a assume "a \<in> A"
  13.188    also assume "A \<subseteq> B"
  13.189    finally have "a \<in> B" .
  13.190 -  thus "\<Sqinter>B \<sqsubseteq> a" ..
  13.191 +  then show "\<Sqinter>B \<sqsubseteq> a" ..
  13.192  qed
  13.193  
  13.194  theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
  13.195  proof -
  13.196    assume "A \<subseteq> B"
  13.197 -  hence "dual ` A \<subseteq> dual ` B" by blast
  13.198 -  hence "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono)
  13.199 -  hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
  13.200 -  thus ?thesis by (simp only: dual_leq)
  13.201 +  then have "dual ` A \<subseteq> dual ` B" by blast
  13.202 +  then have "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono)
  13.203 +  then have "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
  13.204 +  then show ?thesis by (simp only: dual_leq)
  13.205  qed
  13.206  
  13.207  text {*
  13.208 @@ -321,7 +323,7 @@
  13.209  theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
  13.210  proof
  13.211    fix a assume "a \<in> A \<union> B"
  13.212 -  thus "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
  13.213 +  then show "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
  13.214    proof
  13.215      assume a: "a \<in> A"
  13.216      have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" ..
  13.217 @@ -340,13 +342,13 @@
  13.218      show "b \<sqsubseteq> \<Sqinter>A"
  13.219      proof
  13.220        fix a assume "a \<in> A"
  13.221 -      hence "a \<in>  A \<union> B" ..
  13.222 +      then have "a \<in>  A \<union> B" ..
  13.223        with b show "b \<sqsubseteq> a" ..
  13.224      qed
  13.225      show "b \<sqsubseteq> \<Sqinter>B"
  13.226      proof
  13.227        fix a assume "a \<in> B"
  13.228 -      hence "a \<in>  A \<union> B" ..
  13.229 +      then have "a \<in>  A \<union> B" ..
  13.230        with b show "b \<sqsubseteq> a" ..
  13.231      qed
  13.232    qed
  13.233 @@ -370,11 +372,11 @@
  13.234  theorem Meet_singleton: "\<Sqinter>{x} = x"
  13.235  proof
  13.236    fix a assume "a \<in> {x}"
  13.237 -  hence "a = x" by simp
  13.238 -  thus "x \<sqsubseteq> a" by (simp only: leq_refl)
  13.239 +  then have "a = x" by simp
  13.240 +  then show "x \<sqsubseteq> a" by (simp only: leq_refl)
  13.241  next
  13.242    fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a"
  13.243 -  thus "b \<sqsubseteq> x" by simp
  13.244 +  then show "b \<sqsubseteq> x" by simp
  13.245  qed
  13.246  
  13.247  theorem Join_singleton: "\<Squnion>{x} = x"
  13.248 @@ -392,12 +394,12 @@
  13.249  proof
  13.250    fix a :: "'a::complete_lattice"
  13.251    assume "a \<in> {}"
  13.252 -  hence False by simp
  13.253 -  thus "\<Squnion>UNIV \<sqsubseteq> a" ..
  13.254 +  then have False by simp
  13.255 +  then show "\<Squnion>UNIV \<sqsubseteq> a" ..
  13.256  next
  13.257    fix b :: "'a::complete_lattice"
  13.258    have "b \<in> UNIV" ..
  13.259 -  thus "b \<sqsubseteq> \<Squnion>UNIV" ..
  13.260 +  then show "b \<sqsubseteq> \<Squnion>UNIV" ..
  13.261  qed
  13.262  
  13.263  theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV"
    14.1 --- a/src/HOL/Lattice/Lattice.thy	Wed Jun 13 16:43:02 2007 +0200
    14.2 +++ b/src/HOL/Lattice/Lattice.thy	Wed Jun 13 18:30:11 2007 +0200
    14.3 @@ -43,8 +43,8 @@
    14.4  lemma meet_equality [elim?]: "is_inf x y inf \<Longrightarrow> x \<sqinter> y = inf"
    14.5  proof (unfold meet_def)
    14.6    assume "is_inf x y inf"
    14.7 -  thus "(THE inf. is_inf x y inf) = inf"
    14.8 -    by (rule the_equality) (rule is_inf_uniq)
    14.9 +  then show "(THE inf. is_inf x y inf) = inf"
   14.10 +    by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y inf`])
   14.11  qed
   14.12  
   14.13  lemma meetI [intro?]:
   14.14 @@ -54,8 +54,8 @@
   14.15  lemma join_equality [elim?]: "is_sup x y sup \<Longrightarrow> x \<squnion> y = sup"
   14.16  proof (unfold join_def)
   14.17    assume "is_sup x y sup"
   14.18 -  thus "(THE sup. is_sup x y sup) = sup"
   14.19 -    by (rule the_equality) (rule is_sup_uniq)
   14.20 +  then show "(THE sup. is_sup x y sup) = sup"
   14.21 +    by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y sup`])
   14.22  qed
   14.23  
   14.24  lemma joinI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
   14.25 @@ -71,7 +71,8 @@
   14.26  lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
   14.27  proof (unfold meet_def)
   14.28    from ex_inf obtain inf where "is_inf x y inf" ..
   14.29 -  thus "is_inf x y (THE inf. is_inf x y inf)" by (rule theI) (rule is_inf_uniq)
   14.30 +  then show "is_inf x y (THE inf. is_inf x y inf)"
   14.31 +    by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y inf`])
   14.32  qed
   14.33  
   14.34  lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
   14.35 @@ -87,7 +88,8 @@
   14.36  lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
   14.37  proof (unfold join_def)
   14.38    from ex_sup obtain sup where "is_sup x y sup" ..
   14.39 -  thus "is_sup x y (THE sup. is_sup x y sup)" by (rule theI) (rule is_sup_uniq)
   14.40 +  then show "is_sup x y (THE sup. is_sup x y sup)"
   14.41 +    by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y sup`])
   14.42  qed
   14.43  
   14.44  lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
   14.45 @@ -115,16 +117,16 @@
   14.46    show "\<exists>inf'. is_inf x' y' inf'"
   14.47    proof -
   14.48      have "\<exists>sup. is_sup (undual x') (undual y') sup" by (rule ex_sup)
   14.49 -    hence "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
   14.50 +    then have "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
   14.51        by (simp only: dual_inf)
   14.52 -    thus ?thesis by (simp add: dual_ex [symmetric])
   14.53 +    then show ?thesis by (simp add: dual_ex [symmetric])
   14.54    qed
   14.55    show "\<exists>sup'. is_sup x' y' sup'"
   14.56    proof -
   14.57      have "\<exists>inf. is_inf (undual x') (undual y') inf" by (rule ex_inf)
   14.58 -    hence "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
   14.59 +    then have "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
   14.60        by (simp only: dual_sup)
   14.61 -    thus ?thesis by (simp add: dual_ex [symmetric])
   14.62 +    then show ?thesis by (simp add: dual_ex [symmetric])
   14.63    qed
   14.64  qed
   14.65  
   14.66 @@ -136,15 +138,15 @@
   14.67  theorem dual_meet [intro?]: "dual (x \<sqinter> y) = dual x \<squnion> dual y"
   14.68  proof -
   14.69    from is_inf_meet have "is_sup (dual x) (dual y) (dual (x \<sqinter> y))" ..
   14.70 -  hence "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..
   14.71 -  thus ?thesis ..
   14.72 +  then have "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..
   14.73 +  then show ?thesis ..
   14.74  qed
   14.75  
   14.76  theorem dual_join [intro?]: "dual (x \<squnion> y) = dual x \<sqinter> dual y"
   14.77  proof -
   14.78    from is_sup_join have "is_inf (dual x) (dual y) (dual (x \<squnion> y))" ..
   14.79 -  hence "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..
   14.80 -  thus ?thesis ..
   14.81 +  then have "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..
   14.82 +  then show ?thesis ..
   14.83  qed
   14.84  
   14.85  
   14.86 @@ -179,7 +181,7 @@
   14.87    proof
   14.88      show "w \<sqsubseteq> x"
   14.89      proof -
   14.90 -      have "w \<sqsubseteq> x \<sqinter> y" .
   14.91 +      have "w \<sqsubseteq> x \<sqinter> y" by fact
   14.92        also have "\<dots> \<sqsubseteq> x" ..
   14.93        finally show ?thesis .
   14.94      qed
   14.95 @@ -187,11 +189,11 @@
   14.96      proof
   14.97        show "w \<sqsubseteq> y"
   14.98        proof -
   14.99 -        have "w \<sqsubseteq> x \<sqinter> y" .
  14.100 +        have "w \<sqsubseteq> x \<sqinter> y" by fact
  14.101          also have "\<dots> \<sqsubseteq> y" ..
  14.102          finally show ?thesis .
  14.103        qed
  14.104 -      show "w \<sqsubseteq> z" .
  14.105 +      show "w \<sqsubseteq> z" by fact
  14.106      qed
  14.107    qed
  14.108  qed
  14.109 @@ -211,8 +213,8 @@
  14.110  proof
  14.111    show "y \<sqinter> x \<sqsubseteq> x" ..
  14.112    show "y \<sqinter> x \<sqsubseteq> y" ..
  14.113 -  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
  14.114 -  show "z \<sqsubseteq> y \<sqinter> x" ..
  14.115 +  fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
  14.116 +  then show "z \<sqsubseteq> y \<sqinter> x" ..
  14.117  qed
  14.118  
  14.119  theorem join_commute: "x \<squnion> y = y \<squnion> x"
  14.120 @@ -230,16 +232,16 @@
  14.121    show "x \<sqsubseteq> x" ..
  14.122    show "x \<sqsubseteq> x \<squnion> y" ..
  14.123    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
  14.124 -  show "z \<sqsubseteq> x" .
  14.125 +  show "z \<sqsubseteq> x" by assumption
  14.126  qed
  14.127  
  14.128  theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
  14.129  proof -
  14.130    have "dual x \<sqinter> (dual x \<squnion> dual y) = dual x"
  14.131      by (rule meet_join_absorb)
  14.132 -  hence "dual (x \<squnion> (x \<sqinter> y)) = dual x"
  14.133 +  then have "dual (x \<squnion> (x \<sqinter> y)) = dual x"
  14.134      by (simp only: dual_meet dual_join)
  14.135 -  thus ?thesis ..
  14.136 +  then show ?thesis ..
  14.137  qed
  14.138  
  14.139  text {*
  14.140 @@ -258,9 +260,9 @@
  14.141  proof -
  14.142    have "dual x \<sqinter> dual x = dual x"
  14.143      by (rule meet_idem)
  14.144 -  hence "dual (x \<squnion> x) = dual x"
  14.145 +  then have "dual (x \<squnion> x) = dual x"
  14.146      by (simp only: dual_join)
  14.147 -  thus ?thesis ..
  14.148 +  then show ?thesis ..
  14.149  qed
  14.150  
  14.151  text {*
  14.152 @@ -271,14 +273,15 @@
  14.153  proof
  14.154    assume "x \<sqsubseteq> y"
  14.155    show "x \<sqsubseteq> x" ..
  14.156 -  show "x \<sqsubseteq> y" .
  14.157 -  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" .
  14.158 +  show "x \<sqsubseteq> y" by fact
  14.159 +  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
  14.160 +  show "z \<sqsubseteq> x" by fact
  14.161  qed
  14.162  
  14.163  theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
  14.164  proof -
  14.165 -  assume "x \<sqsubseteq> y" hence "dual y \<sqsubseteq> dual x" ..
  14.166 -  hence "dual y \<sqinter> dual x = dual y" by (rule meet_related)
  14.167 +  assume "x \<sqsubseteq> y" then have "dual y \<sqsubseteq> dual x" ..
  14.168 +  then have "dual y \<sqinter> dual x = dual y" by (rule meet_related)
  14.169    also have "dual y \<sqinter> dual x = dual (y \<squnion> x)" by (simp only: dual_join)
  14.170    also have "y \<squnion> x = x \<squnion> y" by (rule join_commute)
  14.171    finally show ?thesis ..
  14.172 @@ -295,8 +298,8 @@
  14.173  theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
  14.174  proof
  14.175    assume "x \<sqsubseteq> y"
  14.176 -  hence "is_inf x y x" ..
  14.177 -  thus "x \<sqinter> y = x" ..
  14.178 +  then have "is_inf x y x" ..
  14.179 +  then show "x \<sqinter> y = x" ..
  14.180  next
  14.181    have "x \<sqinter> y \<sqsubseteq> y" ..
  14.182    also assume "x \<sqinter> y = x"
  14.183 @@ -306,8 +309,8 @@
  14.184  theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
  14.185  proof
  14.186    assume "x \<sqsubseteq> y"
  14.187 -  hence "is_sup x y y" ..
  14.188 -  thus "x \<squnion> y = y" ..
  14.189 +  then have "is_sup x y y" ..
  14.190 +  then show "x \<squnion> y = y" ..
  14.191  next
  14.192    have "x \<sqsubseteq> x \<squnion> y" ..
  14.193    also assume "x \<squnion> y = y"
  14.194 @@ -555,27 +558,27 @@
  14.195      assume "a \<sqsubseteq> c" have "a \<sqinter> b \<sqsubseteq> c \<sqinter> b"
  14.196      proof
  14.197        have "a \<sqinter> b \<sqsubseteq> a" ..
  14.198 -      also have "\<dots> \<sqsubseteq> c" .
  14.199 +      also have "\<dots> \<sqsubseteq> c" by fact
  14.200        finally show "a \<sqinter> b \<sqsubseteq> c" .
  14.201        show "a \<sqinter> b \<sqsubseteq> b" ..
  14.202      qed
  14.203    } note this [elim?]
  14.204 -  assume "x \<sqsubseteq> z" hence "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..
  14.205 +  assume "x \<sqsubseteq> z" then have "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..
  14.206    also have "\<dots> = y \<sqinter> z" by (rule meet_commute)
  14.207 -  also assume "y \<sqsubseteq> w" hence "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..
  14.208 +  also assume "y \<sqsubseteq> w" then have "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..
  14.209    also have "\<dots> = z \<sqinter> w" by (rule meet_commute)
  14.210    finally show ?thesis .
  14.211  qed
  14.212  
  14.213  theorem join_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<squnion> y \<sqsubseteq> z \<squnion> w"
  14.214  proof -
  14.215 -  assume "x \<sqsubseteq> z" hence "dual z \<sqsubseteq> dual x" ..
  14.216 -  moreover assume "y \<sqsubseteq> w" hence "dual w \<sqsubseteq> dual y" ..
  14.217 +  assume "x \<sqsubseteq> z" then have "dual z \<sqsubseteq> dual x" ..
  14.218 +  moreover assume "y \<sqsubseteq> w" then have "dual w \<sqsubseteq> dual y" ..
  14.219    ultimately have "dual z \<sqinter> dual w \<sqsubseteq> dual x \<sqinter> dual y"
  14.220      by (rule meet_mono)
  14.221 -  hence "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"
  14.222 +  then have "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"
  14.223      by (simp only: dual_join)
  14.224 -  thus ?thesis ..
  14.225 +  then show ?thesis ..
  14.226  qed
  14.227  
  14.228  text {*
  14.229 @@ -590,8 +593,8 @@
  14.230  proof
  14.231    assume morph: "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
  14.232    fix x y :: "'a::lattice"
  14.233 -  assume "x \<sqsubseteq> y" hence "x \<sqinter> y = x" ..
  14.234 -  hence "x = x \<sqinter> y" ..
  14.235 +  assume "x \<sqsubseteq> y" then have "x \<sqinter> y = x" ..
  14.236 +  then have "x = x \<sqinter> y" ..
  14.237    also have "f \<dots> \<sqsubseteq> f x \<sqinter> f y" by (rule morph)
  14.238    also have "\<dots> \<sqsubseteq> f y" ..
  14.239    finally show "f x \<sqsubseteq> f y" .
  14.240 @@ -602,8 +605,8 @@
  14.241      fix x y
  14.242      show "f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
  14.243      proof
  14.244 -      have "x \<sqinter> y \<sqsubseteq> x" .. thus "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)
  14.245 -      have "x \<sqinter> y \<sqsubseteq> y" .. thus "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)
  14.246 +      have "x \<sqinter> y \<sqsubseteq> x" .. then show "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)
  14.247 +      have "x \<sqinter> y \<sqsubseteq> y" .. then show "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)
  14.248      qed
  14.249    qed
  14.250  qed
    15.1 --- a/src/HOL/Library/AssocList.thy	Wed Jun 13 16:43:02 2007 +0200
    15.2 +++ b/src/HOL/Library/AssocList.thy	Wed Jun 13 18:30:11 2007 +0200
    15.3 @@ -19,7 +19,7 @@
    15.4  fun
    15.5    delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    15.6  where
    15.7 -  "delete k [] = []"
    15.8 +    "delete k [] = []"
    15.9    | "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
   15.10  
   15.11  fun
   15.12 @@ -79,27 +79,25 @@
   15.13  fun
   15.14    restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   15.15  where
   15.16 -  "restrict A [] = []"
   15.17 +    "restrict A [] = []"
   15.18    | "restrict A (p#ps) = (if fst p \<in> A then p#restrict A ps else restrict A ps)"
   15.19  
   15.20  fun
   15.21    map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   15.22  where
   15.23 -  "map_ran f [] = []"
   15.24 +    "map_ran f [] = []"
   15.25    | "map_ran f (p#ps) = (fst p, f (fst p) (snd p)) # map_ran f ps"
   15.26  
   15.27  fun
   15.28    clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   15.29  where
   15.30 -  "clearjunk [] = []"  
   15.31 +    "clearjunk [] = []"  
   15.32    | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
   15.33  
   15.34  lemmas [simp del] = compose_hint
   15.35  
   15.36  
   15.37 -(* ******************************************************************************** *)
   15.38  subsection {* Lookup *}
   15.39 -(* ******************************************************************************** *)
   15.40  
   15.41  lemma lookup_simps [code func]: 
   15.42    "map_of [] k = None"
   15.43 @@ -107,9 +105,7 @@
   15.44    by simp_all
   15.45  
   15.46  
   15.47 -(* ******************************************************************************** *)
   15.48  subsection {* @{const delete} *}
   15.49 -(* ******************************************************************************** *)
   15.50  
   15.51  lemma delete_def:
   15.52    "delete k xs = filter (\<lambda>p. fst p \<noteq> k) xs"
   15.53 @@ -140,7 +136,7 @@
   15.54  lemma distinct_delete:
   15.55    assumes "distinct (map fst al)" 
   15.56    shows "distinct (map fst (delete k al))"
   15.57 -using prems
   15.58 +using assms
   15.59  proof (induct al)
   15.60    case Nil thus ?case by simp
   15.61  next
   15.62 @@ -152,7 +148,7 @@
   15.63    show ?case
   15.64    proof (cases "fst a = k")
   15.65      case True
   15.66 -    from True dist_al show ?thesis by simp
   15.67 +    with Cons dist_al show ?thesis by simp
   15.68    next
   15.69      case False
   15.70      from dist_al
   15.71 @@ -171,9 +167,8 @@
   15.72  lemma clearjunk_delete: "clearjunk (delete x al) = delete x (clearjunk al)"
   15.73    by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
   15.74  
   15.75 -(* ******************************************************************************** *)
   15.76 +
   15.77  subsection {* @{const clearjunk} *}
   15.78 -(* ******************************************************************************** *)
   15.79  
   15.80  lemma insert_fst_filter: 
   15.81    "insert a(fst ` {x \<in> set ps. fst x \<noteq> a}) = insert a (fst ` set ps)"
   15.82 @@ -221,9 +216,8 @@
   15.83  lemma clearjunk_idem: "clearjunk (clearjunk al) = clearjunk al"
   15.84    by simp
   15.85  
   15.86 -(* ******************************************************************************** *)
   15.87 +
   15.88  subsection {* @{const dom} and @{term "ran"} *}
   15.89 -(* ******************************************************************************** *)
   15.90  
   15.91  lemma dom_map_of': "fst ` set al = dom (map_of al)"
   15.92    by (induct al) auto
   15.93 @@ -295,9 +289,8 @@
   15.94    finally show ?thesis .
   15.95  qed
   15.96     
   15.97 -(* ******************************************************************************** *)
   15.98 +
   15.99  subsection {* @{const update} *}
  15.100 -(* ******************************************************************************** *)
  15.101  
  15.102  lemma update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
  15.103    by (induct al) auto
  15.104 @@ -311,7 +304,7 @@
  15.105  lemma distinct_update:
  15.106    assumes "distinct (map fst al)" 
  15.107    shows "distinct (map fst (update k v al))"
  15.108 -using prems
  15.109 +using assms
  15.110  proof (induct al)
  15.111    case Nil thus ?case by simp
  15.112  next
  15.113 @@ -374,9 +367,7 @@
  15.114    by (simp add: update_conv' image_map_upd)
  15.115  
  15.116  
  15.117 -(* ******************************************************************************** *)
  15.118  subsection {* @{const updates} *}
  15.119 -(* ******************************************************************************** *)
  15.120  
  15.121  lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
  15.122  proof (induct ks arbitrary: vs al)
  15.123 @@ -401,7 +392,7 @@
  15.124  lemma distinct_updates:
  15.125    assumes "distinct (map fst al)"
  15.126    shows "distinct (map fst (updates ks vs al))"
  15.127 -  using prems
  15.128 +  using assms
  15.129    by (induct ks arbitrary: vs al)
  15.130     (auto simp add: distinct_update split: list.splits)
  15.131  
  15.132 @@ -447,9 +438,8 @@
  15.133    "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
  15.134    by (induct xs arbitrary: ys al) (auto split: list.splits)
  15.135  
  15.136 -(* ******************************************************************************** *)
  15.137 +
  15.138  subsection {* @{const map_ran} *}
  15.139 -(* ******************************************************************************** *)
  15.140  
  15.141  lemma map_ran_conv: "map_of (map_ran f al) k = option_map (f k) (map_of al k)"
  15.142    by (induct al) auto
  15.143 @@ -466,9 +456,8 @@
  15.144  lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
  15.145    by (induct al rule: clearjunk.induct) (auto simp add: delete_def map_ran_filter)
  15.146  
  15.147 -(* ******************************************************************************** *)
  15.148 +
  15.149  subsection {* @{const merge} *}
  15.150 -(* ******************************************************************************** *)
  15.151  
  15.152  lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
  15.153    by (induct ys arbitrary: xs) (auto simp add: dom_update)
  15.154 @@ -476,7 +465,7 @@
  15.155  lemma distinct_merge:
  15.156    assumes "distinct (map fst xs)"
  15.157    shows "distinct (map fst (merge xs ys))"
  15.158 -  using prems
  15.159 +  using assms
  15.160  by (induct ys arbitrary: xs) (auto simp add: dom_merge distinct_update)
  15.161  
  15.162  lemma clearjunk_merge:
  15.163 @@ -536,14 +525,13 @@
  15.164  lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)"
  15.165    by (simp add: merge_conv')
  15.166  
  15.167 -(* ******************************************************************************** *)
  15.168 +
  15.169  subsection {* @{const compose} *}
  15.170 -(* ******************************************************************************** *)
  15.171  
  15.172  lemma compose_first_None [simp]: 
  15.173    assumes "map_of xs k = None" 
  15.174    shows "map_of (compose xs ys) k = None"
  15.175 -using prems by (induct xs ys rule: compose.induct)
  15.176 +using assms by (induct xs ys rule: compose.induct)
  15.177    (auto split: option.splits split_if_asm)
  15.178  
  15.179  lemma compose_conv: 
  15.180 @@ -591,7 +579,7 @@
  15.181  lemma compose_first_Some [simp]:
  15.182    assumes "map_of xs k = Some v" 
  15.183    shows "map_of (compose xs ys) k = map_of ys v"
  15.184 -using prems by (simp add: compose_conv)
  15.185 +using assms by (simp add: compose_conv)
  15.186  
  15.187  lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
  15.188  proof (induct xs ys rule: compose.induct)
  15.189 @@ -623,7 +611,7 @@
  15.190  lemma distinct_compose:
  15.191   assumes "distinct (map fst xs)"
  15.192   shows "distinct (map fst (compose xs ys))"
  15.193 -using prems
  15.194 +using assms
  15.195  proof (induct xs ys rule: compose.induct)
  15.196    case 1 thus ?case by simp
  15.197  next
  15.198 @@ -695,9 +683,7 @@
  15.199    by (simp add: compose_conv map_comp_None_iff)
  15.200  
  15.201  
  15.202 -(* ******************************************************************************** *)
  15.203  subsection {* @{const restrict} *}
  15.204 -(* ******************************************************************************** *)
  15.205  
  15.206  lemma restrict_def:
  15.207    "restrict A = filter (\<lambda>p. fst p \<in> A)"
    16.1 --- a/src/HOL/Library/BigO.thy	Wed Jun 13 16:43:02 2007 +0200
    16.2 +++ b/src/HOL/Library/BigO.thy	Wed Jun 13 18:30:11 2007 +0200
    16.3 @@ -282,7 +282,7 @@
    16.4      apply (subst func_diff)
    16.5      apply (rule bigo_abs)
    16.6      done
    16.7 -  also have "... <= O(h)"
    16.8 +  also from a have "... <= O(h)"
    16.9      by (rule bigo_elt_subset)
   16.10    finally show "(%x. abs (f x) - abs (g x)) : O(h)".
   16.11  qed
    17.1 --- a/src/HOL/Library/Graphs.thy	Wed Jun 13 16:43:02 2007 +0200
    17.2 +++ b/src/HOL/Library/Graphs.thy	Wed Jun 13 18:30:11 2007 +0200
    17.3 @@ -3,7 +3,7 @@
    17.4      Author:     Alexander Krauss, TU Muenchen
    17.5  *)
    17.6  
    17.7 -header ""
    17.8 +header ""   (* FIXME proper header *)
    17.9  
   17.10  theory Graphs
   17.11  imports Main SCT_Misc Kleene_Algebras ExecutableSet
   17.12 @@ -56,8 +56,8 @@
   17.13  lemma graph_ext:
   17.14    assumes "\<And>n e n'. has_edge G n e n' = has_edge H n e n'"
   17.15    shows "G = H"
   17.16 -  using prems
   17.17 -  by (cases G, cases H, auto simp:split_paired_all has_edge_def)
   17.18 +  using assms
   17.19 +  by (cases G, cases H) (auto simp:split_paired_all has_edge_def)
   17.20  
   17.21  
   17.22  instance graph :: (type, type) "{comm_monoid_add}"
   17.23 @@ -219,7 +219,7 @@
   17.24  lemma graph_leqI:
   17.25    assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
   17.26    shows "G \<le> H"
   17.27 -  using prems
   17.28 +  using assms
   17.29    unfolding graph_leq_def has_edge_def
   17.30    by auto
   17.31  
   17.32 @@ -229,18 +229,18 @@
   17.33    assumes "has_edge G n e n' \<Longrightarrow> P"
   17.34    assumes "has_edge H n e n' \<Longrightarrow> P"
   17.35    shows P
   17.36 -  using prems
   17.37 +  using assms
   17.38    by (auto simp: in_grplus)
   17.39  
   17.40  lemma 
   17.41    assumes "x \<in> S k"
   17.42    shows "x \<in> (\<Union>k. S k)"
   17.43 -  using prems by blast
   17.44 +  using assms by blast
   17.45  
   17.46  lemma graph_union_least:
   17.47    assumes "\<And>n. Graph (G n) \<le> C"
   17.48    shows "Graph (\<Union>n. G n) \<le> C"
   17.49 -  using prems unfolding graph_leq_def
   17.50 +  using assms unfolding graph_leq_def
   17.51    by auto
   17.52  
   17.53  lemma Sup_graph_eq:
   17.54 @@ -333,15 +333,15 @@
   17.55  lemma endnode_nth:
   17.56    assumes "length (snd p) = Suc k"
   17.57    shows "end_node p = snd (snd (path_nth p k))"
   17.58 -  using prems unfolding end_node_def path_nth_def
   17.59 +  using assms unfolding end_node_def path_nth_def
   17.60    by auto
   17.61  
   17.62  lemma path_nth_graph:
   17.63    assumes "k < length (snd p)"
   17.64    assumes "has_fpath G p"
   17.65    shows "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p k)"
   17.66 -  using prems
   17.67 -proof (induct k arbitrary:p)
   17.68 +using assms
   17.69 +proof (induct k arbitrary: p)
   17.70    case 0 thus ?case 
   17.71      unfolding path_nth_def by (auto elim:has_fpath.cases)
   17.72  next
   17.73 @@ -364,7 +364,7 @@
   17.74  lemma path_nth_connected:
   17.75    assumes "Suc k < length (snd p)"
   17.76    shows "fst (path_nth p (Suc k)) = snd (snd (path_nth p k))"
   17.77 -  using prems
   17.78 +  using assms
   17.79    unfolding path_nth_def
   17.80    by auto
   17.81  
   17.82 @@ -399,9 +399,9 @@
   17.83      hence "fst (path_nth p (Suc i mod ?l)) = fst (path_nth p 0)" 
   17.84        by (simp add: mod_Suc)
   17.85      also from fst_p0 have "\<dots> = fst p" .
   17.86 -    also have "\<dots> = end_node p" .
   17.87 +    also have "\<dots> = end_node p" by assumption
   17.88      also have "\<dots> = snd (snd (path_nth p ?k))" 
   17.89 -      by (auto simp:endnode_nth wrap)
   17.90 +      by (auto simp: endnode_nth wrap)
   17.91      finally show ?thesis .
   17.92    qed
   17.93  qed
   17.94 @@ -411,17 +411,21 @@
   17.95    and loop: "fst p = end_node p"
   17.96    and nonempty: "0 < length (snd p)" (is "0 < ?l")
   17.97    shows "has_ipath G (omega p)"
   17.98 -proof (auto simp:has_ipath_def)
   17.99 -  fix i 
  17.100 -  from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
  17.101 -    by simp
  17.102 -  with path_nth_graph 
  17.103 -  have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)" .
  17.104 +proof -
  17.105 +  {
  17.106 +    fix i 
  17.107 +    from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
  17.108 +      by simp
  17.109 +    from this and `has_fpath G p`
  17.110 +    have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)"
  17.111 +      by (rule path_nth_graph)
  17.112  
  17.113 -  from path_loop_connect[OF loop nonempty] pk_G
  17.114 -  show "has_edge G (fst (omega p i)) (snd (omega p i)) (fst (omega p (Suc i)))"
  17.115 -    unfolding path_loop_def has_edge_def split_def
  17.116 -    by simp
  17.117 +    from path_loop_connect[OF loop nonempty] pk_G
  17.118 +    have "has_edge G (fst (omega p i)) (snd (omega p i)) (fst (omega p (Suc i)))"
  17.119 +      unfolding path_loop_def has_edge_def split_def
  17.120 +      by simp
  17.121 +  }
  17.122 +  then show ?thesis by (auto simp:has_ipath_def)
  17.123  qed
  17.124  
  17.125  definition prod :: "('n, 'e::monoid_mult) fpath \<Rightarrow> 'e"
  17.126 @@ -514,7 +518,7 @@
  17.127  lemma upto_append[simp]:
  17.128    assumes "i \<le> j" "j \<le> k"
  17.129    shows "[ i ..< j ] @ [j ..< k] = [i ..< k]"
  17.130 -  using prems and upt_add_eq_append[of i j "k - j"]
  17.131 +  using assms and upt_add_eq_append[of i j "k - j"]
  17.132    by simp
  17.133  
  17.134  lemma foldr_monoid: "foldr (op *) xs 1 * foldr (op *) ys 1
  17.135 @@ -525,7 +529,7 @@
  17.136    assumes "i < j"
  17.137    assumes "j < k"
  17.138    shows "prod (p\<langle>i,k\<rangle>) = prod (p\<langle>i,j\<rangle>) * prod (p\<langle>j,k\<rangle>)"
  17.139 -  using prems
  17.140 +  using assms
  17.141    unfolding prod_def sub_path_def
  17.142    by (simp add:map_compose[symmetric] comp_def)
  17.143     (simp only:foldr_monoid map_append[symmetric] upto_append)
  17.144 @@ -535,7 +539,7 @@
  17.145    assumes "length es = l"
  17.146    assumes "has_fpath G (n,es)"
  17.147    shows "has_edge (G ^ l) n (prod (n,es)) (end_node (n,es))"
  17.148 -using prems
  17.149 +using assms
  17.150  proof (induct l arbitrary:n es)
  17.151    case 0 thus ?case
  17.152      by (simp add:in_grunit end_node_def) 
  17.153 @@ -679,7 +683,7 @@
  17.154  
  17.155  lemma sub_path_loop:
  17.156    assumes "0 < k"
  17.157 -  assumes k:"k = length (snd loop)"
  17.158 +  assumes k: "k = length (snd loop)"
  17.159    assumes loop: "fst loop = end_node loop"
  17.160    shows "(omega loop)\<langle>k * i,k * Suc i\<rangle> = loop" (is "?\<omega> = loop")
  17.161  proof (rule prod_eqI)
  17.162 @@ -698,14 +702,17 @@
  17.163        = snd (snd (path_nth loop (i mod k)))"
  17.164        unfolding k
  17.165        apply (rule path_loop_connect[OF loop])
  17.166 -      by (insert prems, auto)
  17.167 +      using `0 < k` and k
  17.168 +      apply auto
  17.169 +      done
  17.170  
  17.171      from `j < k` 
  17.172      show "snd ?\<omega> ! j = snd loop ! j"
  17.173        unfolding sub_path_def
  17.174        apply (simp add:path_loop_def split_def add_ac)
  17.175        apply (simp add:a k[symmetric])
  17.176 -      by (simp add:path_nth_def)
  17.177 +      apply (simp add:path_nth_def)
  17.178 +      done
  17.179    qed
  17.180  qed
  17.181  
    18.1 --- a/src/HOL/Library/Multiset.thy	Wed Jun 13 16:43:02 2007 +0200
    18.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jun 13 18:30:11 2007 +0200
    18.3 @@ -450,7 +450,7 @@
    18.4        proof (elim exE disjE conjE)
    18.5          fix M assume "?R M M0" and N: "N = M + {#a#}"
    18.6          from acc_hyp have "?R M M0 --> ?W (M + {#a#})" ..
    18.7 -        then have "?W (M + {#a#})" ..
    18.8 +        from this and `?R M M0` have "?W (M + {#a#})" ..
    18.9          then show "?W N" by (simp only: N)
   18.10        next
   18.11          fix K
   18.12 @@ -487,23 +487,23 @@
   18.13      from wf have "\<forall>M \<triangleright> ?W. ?W (M + {#a#})"
   18.14      proof induct
   18.15        fix a
   18.16 -      assume "!!b. r b a ==> \<forall>M \<triangleright> ?W. ?W (M + {#b#})"
   18.17 +      assume r: "!!b. r b a ==> \<forall>M \<triangleright> ?W. ?W (M + {#b#})"
   18.18        show "\<forall>M \<triangleright> ?W. ?W (M + {#a#})"
   18.19        proof
   18.20          fix M assume "?W M"
   18.21          then show "?W (M + {#a#})"
   18.22 -          by (rule acc_induct) (rule tedious_reasoning)
   18.23 +          by (rule acc_induct) (rule tedious_reasoning [OF _ r])
   18.24        qed
   18.25      qed
   18.26 -    then show "?W (M + {#a#})" ..
   18.27 +    from this and `?W M` show "?W (M + {#a#})" ..
   18.28    qed
   18.29  qed
   18.30  
   18.31  theorem wf_mult1: "wfP r ==> wfP (mult1 r)"
   18.32 -  by (rule acc_wfI, rule all_accessible)
   18.33 +  by (rule acc_wfI) (rule all_accessible)
   18.34  
   18.35  theorem wf_mult: "wfP r ==> wfP (mult r)"
   18.36 -  by (unfold mult_def, rule wfP_trancl, rule wf_mult1)
   18.37 +  unfolding mult_def by (rule wfP_trancl) (rule wf_mult1)
   18.38  
   18.39  
   18.40  subsubsection {* Closure-free presentation *}
   18.41 @@ -511,7 +511,7 @@
   18.42  (*Badly needed: a linear arithmetic procedure for multisets*)
   18.43  
   18.44  lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})"
   18.45 -by (simp add: multiset_eq_conv_count_eq)
   18.46 +  by (simp add: multiset_eq_conv_count_eq)
   18.47  
   18.48  text {* One direction. *}
   18.49  
   18.50 @@ -548,7 +548,7 @@
   18.51    done
   18.52  
   18.53  lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}"
   18.54 -by (simp add: multiset_eq_conv_count_eq)
   18.55 +  by (simp add: multiset_eq_conv_count_eq)
   18.56  
   18.57  lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}"
   18.58    apply (erule size_eq_Suc_imp_elem [THEN exE])
   18.59 @@ -588,8 +588,7 @@
   18.60  lemma one_step_implies_mult:
   18.61    "J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. r k j
   18.62      ==> mult r (I + K) (I + J)"
   18.63 -  apply (insert one_step_implies_mult_aux, blast)
   18.64 -  done
   18.65 +  using one_step_implies_mult_aux by blast
   18.66  
   18.67  
   18.68  subsubsection {* Partial-order properties *}
   18.69 @@ -609,9 +608,7 @@
   18.70  
   18.71  lemma mult_irrefl_aux:
   18.72      "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}"
   18.73 -  apply (induct rule: finite_induct)
   18.74 -   apply (auto intro: order_less_trans)
   18.75 -  done
   18.76 +  by (induct rule: finite_induct) (auto intro: order_less_trans)
   18.77  
   18.78  lemma mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
   18.79    apply (unfold less_multiset_def, auto)
   18.80 @@ -621,15 +618,13 @@
   18.81    done
   18.82  
   18.83  lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
   18.84 -by (insert mult_less_not_refl, fast)
   18.85 +  using insert mult_less_not_refl by fast
   18.86  
   18.87  
   18.88  text {* Transitivity. *}
   18.89  
   18.90  theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)"
   18.91 -  apply (unfold less_multiset_def mult_def)
   18.92 -  apply (blast intro: trancl_trans')
   18.93 -  done
   18.94 +  unfolding less_multiset_def mult_def by (blast intro: trancl_trans')
   18.95  
   18.96  text {* Asymmetry. *}
   18.97  
    19.1 --- a/src/HOL/Library/Quotient.thy	Wed Jun 13 16:43:02 2007 +0200
    19.2 +++ b/src/HOL/Library/Quotient.thy	Wed Jun 13 18:30:11 2007 +0200
    19.3 @@ -31,27 +31,27 @@
    19.4  
    19.5  lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
    19.6  proof -
    19.7 -  assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)"
    19.8 +  assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)"
    19.9      by (rule contrapos_nn) (rule equiv_sym)
   19.10  qed
   19.11  
   19.12  lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
   19.13  proof -
   19.14 -  assume "\<not> (x \<sim> y)" and yz: "y \<sim> z"
   19.15 +  assume "\<not> (x \<sim> y)" and "y \<sim> z"
   19.16    show "\<not> (x \<sim> z)"
   19.17    proof
   19.18      assume "x \<sim> z"
   19.19 -    also from yz have "z \<sim> y" ..
   19.20 +    also from `y \<sim> z` have "z \<sim> y" ..
   19.21      finally have "x \<sim> y" .
   19.22 -    thus False by contradiction
   19.23 +    with `\<not> (x \<sim> y)` show False by contradiction
   19.24    qed
   19.25  qed
   19.26  
   19.27  lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
   19.28  proof -
   19.29 -  assume "\<not> (y \<sim> z)" hence "\<not> (z \<sim> y)" ..
   19.30 -  also assume "x \<sim> y" hence "y \<sim> x" ..
   19.31 -  finally have "\<not> (z \<sim> x)" . thus "(\<not> x \<sim> z)" ..
   19.32 +  assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
   19.33 +  also assume "x \<sim> y" then have "y \<sim> x" ..
   19.34 +  finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" ..
   19.35  qed
   19.36  
   19.37  text {*
   19.38 @@ -80,9 +80,9 @@
   19.39  theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
   19.40  proof (cases A)
   19.41    fix R assume R: "A = Abs_quot R"
   19.42 -  assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
   19.43 +  assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
   19.44    with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
   19.45 -  thus ?thesis unfolding class_def .
   19.46 +  then show ?thesis unfolding class_def .
   19.47  qed
   19.48  
   19.49  lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
   19.50 @@ -105,8 +105,8 @@
   19.51        by (simp only: class_def Abs_quot_inject quotI)
   19.52      moreover have "a \<sim> a" ..
   19.53      ultimately have "a \<in> {x. b \<sim> x}" by blast
   19.54 -    hence "b \<sim> a" by blast
   19.55 -    thus ?thesis ..
   19.56 +    then have "b \<sim> a" by blast
   19.57 +    then show ?thesis ..
   19.58    qed
   19.59  next
   19.60    assume ab: "a \<sim> b"
   19.61 @@ -125,7 +125,7 @@
   19.62          finally show "a \<sim> x" .
   19.63        qed
   19.64      qed
   19.65 -    thus ?thesis by (simp only: class_def)
   19.66 +    then show ?thesis by (simp only: class_def)
   19.67    qed
   19.68  qed
   19.69  
   19.70 @@ -142,15 +142,15 @@
   19.71    proof (rule someI2)
   19.72      show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
   19.73      fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
   19.74 -    hence "a \<sim> x" .. thus "x \<sim> a" ..
   19.75 +    then have "a \<sim> x" .. then show "x \<sim> a" ..
   19.76    qed
   19.77  qed
   19.78  
   19.79  theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
   19.80  proof (cases A)
   19.81    fix a assume a: "A = \<lfloor>a\<rfloor>"
   19.82 -  hence "pick A \<sim> a" by (simp only: pick_equiv)
   19.83 -  hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
   19.84 +  then have "pick A \<sim> a" by (simp only: pick_equiv)
   19.85 +  then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
   19.86    with a show ?thesis by simp
   19.87  qed
   19.88  
   19.89 @@ -175,7 +175,7 @@
   19.90      moreover
   19.91      show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
   19.92      moreover
   19.93 -    show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" .
   19.94 +    show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P)
   19.95      ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
   19.96    qed
   19.97    finally show ?thesis .
    20.1 --- a/src/HOL/Library/SCT_Misc.thy	Wed Jun 13 16:43:02 2007 +0200
    20.2 +++ b/src/HOL/Library/SCT_Misc.thy	Wed Jun 13 18:30:11 2007 +0200
    20.3 @@ -3,9 +3,9 @@
    20.4      Author:     Alexander Krauss, TU Muenchen
    20.5  *)
    20.6  
    20.7 -header ""
    20.8 +header ""   (* FIXME proper header *)
    20.9  
   20.10 -theory SCT_Misc
   20.11 +theory SCT_Misc   (* FIXME proper name *)
   20.12  imports Main
   20.13  begin
   20.14  
   20.15 @@ -95,11 +95,13 @@
   20.16    "section_of s n = (LEAST i. n < s (Suc i))"
   20.17  
   20.18  lemma section_help:
   20.19 -  assumes [intro, simp]: "increasing s"
   20.20 +  assumes "increasing s"
   20.21    shows "\<exists>i. n < s (Suc i)" 
   20.22  proof -
   20.23 -  from increasing_inc have "n \<le> s n" .
   20.24 -  also from increasing_strict have "\<dots> < s (Suc n)" by simp
   20.25 +  have "n \<le> s n"
   20.26 +    using `increasing s` by (rule increasing_inc)
   20.27 +  also have "\<dots> < s (Suc n)"
   20.28 +    using `increasing s` increasing_strict by simp
   20.29    finally show ?thesis ..
   20.30  qed
   20.31  
   20.32 @@ -107,7 +109,7 @@
   20.33    assumes "increasing s"
   20.34    shows "n < s (Suc (section_of s n))"
   20.35    unfolding section_of_def
   20.36 -  by (rule LeastI_ex) (rule section_help)
   20.37 +  by (rule LeastI_ex) (rule section_help [OF `increasing s`])
   20.38  
   20.39  lemma section_of1:
   20.40    assumes [simp, intro]: "increasing s"
    21.1 --- a/src/HOL/Library/SCT_Theorem.thy	Wed Jun 13 16:43:02 2007 +0200
    21.2 +++ b/src/HOL/Library/SCT_Theorem.thy	Wed Jun 13 18:30:11 2007 +0200
    21.3 @@ -3,7 +3,7 @@
    21.4      Author:     Alexander Krauss, TU Muenchen
    21.5  *)
    21.6  
    21.7 -header ""
    21.8 +header ""   (* FIXME proper header *)
    21.9  
   21.10  theory SCT_Theorem
   21.11  imports Main Ramsey SCT_Misc SCT_Definition
   21.12 @@ -795,10 +795,9 @@
   21.13        unfolding is_desc_fthread_def
   21.14        by auto
   21.15  
   21.16 -    have "i < s (Suc ?k)" by (rule section_of2)
   21.17 -    also have "\<dots> \<le> s j" 
   21.18 -      by (rule increasing_weak[of s], assumption)
   21.19 -    (insert `?k < j`, arith)
   21.20 +    have "i < s (Suc ?k)" by (rule section_of2) simp
   21.21 +    also have "\<dots> \<le> s j"
   21.22 +      by (rule increasing_weak [of s], assumption) (insert `?k < j`, arith)
   21.23      also note `\<dots> \<le> l`
   21.24      finally have "i < l" .
   21.25      with desc
   21.26 @@ -925,10 +924,10 @@
   21.27        {
   21.28  	fix x assume r: "x \<in> section s ?L"
   21.29  	
   21.30 -	have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2)
   21.31 +	have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2) simp
   21.32          note `s (Suc ?K) < j`
   21.33          also have "j < s (Suc ?L)"
   21.34 -          by (rule section_of2)
   21.35 +          by (rule section_of2) simp
   21.36          finally have "Suc ?K \<le> ?L"
   21.37            by (simp add:increasing_bij)          
   21.38  	with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp
   21.39 @@ -1074,12 +1073,12 @@
   21.40    "set2list = inv set"
   21.41  
   21.42  lemma finite_set2list: 
   21.43 -  assumes [intro]: "finite S" 
   21.44 +  assumes "finite S" 
   21.45    shows "set (set2list S) = S"
   21.46    unfolding set2list_def 
   21.47  proof (rule f_inv_f)
   21.48 -  from finite_list
   21.49 -  have "\<exists>l. set l = S" .
   21.50 +  from `finite S` have "\<exists>l. set l = S"
   21.51 +    by (rule finite_list)
   21.52    thus "S \<in> range set"
   21.53      unfolding image_def
   21.54      by auto
   21.55 @@ -1307,7 +1306,7 @@
   21.56        by (simp only:split_conv, rule a, auto)
   21.57  
   21.58      obtain n H m where
   21.59 -      G_struct: "G = (n, H, m)" by (cases G) simp
   21.60 +      G_struct: "G = (n, H, m)" by (cases G)
   21.61  
   21.62      let ?s = "enumerate S"
   21.63      let ?q = "contract ?s p"
   21.64 @@ -1381,7 +1380,7 @@
   21.65  proof -
   21.66    from fin obtain P where b: "bounded_acg P A"
   21.67      unfolding finite_acg_def ..
   21.68 -  show ?thesis using LJA_Theorem4[OF b]
   21.69 +  show ?thesis using LJA_Theorem4[OF b] and `SCT' A`
   21.70      by simp
   21.71  qed
   21.72  
    22.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Wed Jun 13 16:43:02 2007 +0200
    22.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Wed Jun 13 18:30:11 2007 +0200
    22.3 @@ -85,7 +85,8 @@
    22.4      next
    22.5        fix y
    22.6        assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0"
    22.7 -      show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))" by (rule exI[of _ "snd y"], rule exI[of _ "fst y"], simp)
    22.8 +      show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))"
    22.9 +	by (rule exI[of _ "snd y"], rule exI[of _ "fst y"]) (simp add: hyp)
   22.10      qed
   22.11    then have "finite (?swap`?A)"
   22.12      proof -
    23.1 --- a/src/HOL/NumberTheory/Euler.thy	Wed Jun 13 16:43:02 2007 +0200
    23.2 +++ b/src/HOL/NumberTheory/Euler.thy	Wed Jun 13 18:30:11 2007 +0200
    23.3 @@ -264,7 +264,7 @@
    23.4      by (auto simp add: zEven_def zOdd_def)
    23.5    then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
    23.6      by (auto simp add: even_div_2_prop2)
    23.7 -  then have "1 < (p - 1)"
    23.8 +  with `2 < p` have "1 < (p - 1)"
    23.9      by auto
   23.10    then have " 1 < (2 * ((p - 1) div 2))"
   23.11      by (auto simp add: aux_1)
    24.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 13 16:43:02 2007 +0200
    24.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 13 18:30:11 2007 +0200
    24.3 @@ -115,8 +115,8 @@
    24.4     (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
    24.5  proof -
    24.6    assume "a \<in> zOdd"
    24.7 -  from QRLemma4 have
    24.8 -    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)"..
    24.9 +  from QRLemma4 [OF this] have
   24.10 +    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
   24.11    moreover have "0 \<le> int(card E)"
   24.12      by auto
   24.13    moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
    25.1 --- a/src/HOL/W0/W0.thy	Wed Jun 13 16:43:02 2007 +0200
    25.2 +++ b/src/HOL/W0/W0.thy	Wed Jun 13 18:30:11 2007 +0200
    25.3 @@ -405,7 +405,7 @@
    25.4    then have "map ($ s) a |- Var n :: map ($ s) a ! n"
    25.5      by (rule has_type.Var)
    25.6    also have "map ($ s) a ! n = $ s (a ! n)"
    25.7 -    by (rule nth_map)
    25.8 +    by (rule nth_map) (rule Var)
    25.9    also have "map ($ s) a = $ s a"
   25.10      by (simp only: app_subst_list)
   25.11    finally show ?case .
    26.1 --- a/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Jun 13 16:43:02 2007 +0200
    26.2 +++ b/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Jun 13 18:30:11 2007 +0200
    26.3 @@ -150,7 +150,7 @@
    26.4      then obtain d where X:"x=Suc (Suc d)" ..
    26.5      from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
    26.6      with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
    26.7 -    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp
    26.8 +    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption
    26.9      with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   26.10    ultimately show ?case by blast
   26.11  next
   26.12 @@ -168,7 +168,7 @@
   26.13      then obtain d where X:"x=Suc (Suc d)" ..
   26.14      from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   26.15      with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
   26.16 -    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp
   26.17 +    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption
   26.18      with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   26.19    ultimately show ?case by blast
   26.20  next
    27.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Wed Jun 13 16:43:02 2007 +0200
    27.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Wed Jun 13 18:30:11 2007 +0200
    27.3 @@ -58,7 +58,7 @@
    27.4  theorem sym [sym]: "x = y \<Longrightarrow> y = x"
    27.5  proof -
    27.6    assume "x = y"
    27.7 -  thus "y = x" by (rule subst) (rule refl)
    27.8 +  then show "y = x" by (rule subst) (rule refl)
    27.9  qed
   27.10  
   27.11  lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
   27.12 @@ -110,7 +110,7 @@
   27.13  theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
   27.14  proof (unfold false_def)
   27.15    assume "\<forall>A. A"
   27.16 -  thus A ..
   27.17 +  then show A ..
   27.18  qed
   27.19  
   27.20  theorem trueI [intro]: \<top>
   27.21 @@ -121,7 +121,7 @@
   27.22  theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
   27.23  proof (unfold not_def)
   27.24    assume "A \<Longrightarrow> \<bottom>"
   27.25 -  thus "A \<longrightarrow> \<bottom>" ..
   27.26 +  then show "A \<longrightarrow> \<bottom>" ..
   27.27  qed
   27.28  
   27.29  theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
   27.30 @@ -129,7 +129,7 @@
   27.31    assume "A \<longrightarrow> \<bottom>"
   27.32    also assume A
   27.33    finally have \<bottom> ..
   27.34 -  thus B ..
   27.35 +  then show B ..
   27.36  qed
   27.37  
   27.38  lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
   27.39 @@ -145,8 +145,8 @@
   27.40      fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   27.41      proof
   27.42        assume "A \<longrightarrow> B \<longrightarrow> C"
   27.43 -      also have A .
   27.44 -      also have B .
   27.45 +      also note `A`
   27.46 +      also note `B`
   27.47        finally show C .
   27.48      qed
   27.49    qed
   27.50 @@ -161,7 +161,7 @@
   27.51      also have "A \<longrightarrow> B \<longrightarrow> A"
   27.52      proof
   27.53        assume A
   27.54 -      thus "B \<longrightarrow> A" ..
   27.55 +      then show "B \<longrightarrow> A" ..
   27.56      qed
   27.57      finally have A .
   27.58    } moreover {
   27.59 @@ -182,9 +182,9 @@
   27.60      fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   27.61      proof
   27.62        assume "A \<longrightarrow> C"
   27.63 -      also have A .
   27.64 +      also note `A`
   27.65        finally have C .
   27.66 -      thus "(B \<longrightarrow> C) \<longrightarrow> C" ..
   27.67 +      then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
   27.68      qed
   27.69    qed
   27.70  qed
   27.71 @@ -199,7 +199,7 @@
   27.72        show "(B \<longrightarrow> C) \<longrightarrow> C"
   27.73        proof
   27.74          assume "B \<longrightarrow> C"
   27.75 -        also have B .
   27.76 +        also note `B`
   27.77          finally show C .
   27.78        qed
   27.79      qed
   27.80 @@ -213,11 +213,11 @@
   27.81    from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
   27.82    also have "A \<longrightarrow> C"
   27.83    proof
   27.84 -    assume A thus C by (rule r1)
   27.85 +    assume A then show C by (rule r1)
   27.86    qed
   27.87    also have "B \<longrightarrow> C"
   27.88    proof
   27.89 -    assume B thus C by (rule r2)
   27.90 +    assume B then show C by (rule r2)
   27.91    qed
   27.92    finally show C .
   27.93  qed
   27.94 @@ -230,8 +230,8 @@
   27.95      fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   27.96      proof
   27.97        assume "\<forall>x. P x \<longrightarrow> C"
   27.98 -      hence "P a \<longrightarrow> C" ..
   27.99 -      also have "P a" .
  27.100 +      then have "P a \<longrightarrow> C" ..
  27.101 +      also note `P a`
  27.102        finally show C .
  27.103      qed
  27.104    qed
  27.105 @@ -247,7 +247,7 @@
  27.106      fix x show "P x \<longrightarrow> C"
  27.107      proof
  27.108        assume "P x"
  27.109 -      thus C by (rule r)
  27.110 +      then show C by (rule r)
  27.111      qed
  27.112    qed
  27.113    finally show C .
  27.114 @@ -269,7 +269,7 @@
  27.115      have "A \<longrightarrow> B"
  27.116      proof
  27.117        assume A
  27.118 -      thus B by (rule contradiction)
  27.119 +      with `\<not> A` show B by (rule contradiction)
  27.120      qed
  27.121      with a show A ..
  27.122    qed
  27.123 @@ -282,7 +282,7 @@
  27.124    show A
  27.125    proof (rule classical)
  27.126      assume "\<not> A"
  27.127 -    thus ?thesis by (rule contradiction)
  27.128 +    with `\<not> \<not> A` show ?thesis by (rule contradiction)
  27.129    qed
  27.130  qed
  27.131  
  27.132 @@ -294,11 +294,11 @@
  27.133      assume "\<not> (A \<or> \<not> A)"
  27.134      have "\<not> A"
  27.135      proof
  27.136 -      assume A hence "A \<or> \<not> A" ..
  27.137 -      thus \<bottom> by (rule contradiction)
  27.138 +      assume A then have "A \<or> \<not> A" ..
  27.139 +      with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
  27.140      qed
  27.141 -    hence "A \<or> \<not> A" ..
  27.142 -    thus \<bottom> by (rule contradiction)
  27.143 +    then have "A \<or> \<not> A" ..
  27.144 +    with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
  27.145    qed
  27.146  qed
  27.147  
  27.148 @@ -309,10 +309,10 @@
  27.149    from tertium_non_datur show C
  27.150    proof
  27.151      assume A
  27.152 -    thus ?thesis by (rule r1)
  27.153 +    then show ?thesis by (rule r1)
  27.154    next
  27.155      assume "\<not> A"
  27.156 -    thus ?thesis by (rule r2)
  27.157 +    then show ?thesis by (rule r2)
  27.158    qed
  27.159  qed
  27.160  
  27.161 @@ -321,9 +321,9 @@
  27.162    assume r: "\<not> A \<Longrightarrow> A"
  27.163    show A
  27.164    proof (rule classical_cases)
  27.165 -    assume A thus A .
  27.166 +    assume A then show A .
  27.167    next
  27.168 -    assume "\<not> A" thus A by (rule r)
  27.169 +    assume "\<not> A" then show A by (rule r)
  27.170    qed
  27.171  qed
  27.172  
    28.1 --- a/src/HOL/ex/PER.thy	Wed Jun 13 16:43:02 2007 +0200
    28.2 +++ b/src/HOL/ex/PER.thy	Wed Jun 13 18:30:11 2007 +0200
    28.3 @@ -242,7 +242,7 @@
    28.4    proof (rule someI2)
    28.5      show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
    28.6      fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
    28.7 -    then have "a \<sim> x" ..
    28.8 +    from this and a have "a \<sim> x" ..
    28.9      then show "x \<sim> a" ..
   28.10    qed
   28.11  qed
    29.1 --- a/src/HOL/ex/ThreeDivides.thy	Wed Jun 13 16:43:02 2007 +0200
    29.2 +++ b/src/HOL/ex/ThreeDivides.thy	Wed Jun 13 18:30:11 2007 +0200
    29.3 @@ -77,7 +77,7 @@
    29.4    let ?thr = "(3::nat)"
    29.5    have "?thr dvd 9" by simp
    29.6    moreover
    29.7 -  have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult)
    29.8 +  have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult) (rule Suc)
    29.9    hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)
   29.10    ultimately
   29.11    have"?thr dvd ((10^(n+1) - 10) + 9)"
    30.1 --- a/src/HOL/ex/Unification.thy	Wed Jun 13 16:43:02 2007 +0200
    30.2 +++ b/src/HOL/ex/Unification.thy	Wed Jun 13 18:30:11 2007 +0200
    30.3 @@ -461,7 +461,7 @@
    30.4      by (rule acc_downward) (rule unify_rel.intros)
    30.5    hence no_new_vars: 
    30.6      "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
    30.7 -    by (rule unify_vars)
    30.8 +    by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
    30.9  
   30.10    from ih2 show ?case 
   30.11    proof