--- a/src/HOL/Bali/TypeSafe.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Wed Jun 13 18:30:11 2007 +0200
@@ -2680,8 +2680,8 @@
qed
next
case (Super s L accC T A)
- have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
+ note conf_s = `Norm s\<Colon>\<preceq>(G, L)`
+ note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T`
then obtain C c where
C: "L This = Some (Class C)" and
neq_Obj: "C\<noteq>Object" and
@@ -3426,10 +3426,10 @@
have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
moreover
- have "s3 =
+ note `s3 =
(if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or>
abrupt s2 = Some (Jump (Cont l))
- then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)" .
+ then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
ultimately show ?thesis
by force
qed
@@ -3649,8 +3649,8 @@
from eval_e1 wt_e1 da_e1 wf True
have "nrm E1 \<subseteq> dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
- with da_e2 show ?thesis
- by (rule da_weakenE)
+ with da_e2 show thesis
+ by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_e2
obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
--- a/src/HOL/Extraction/Higman.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy Wed Jun 13 18:30:11 2007 +0200
@@ -146,16 +146,18 @@
assumes ab: "a \<noteq> b" and bar: "bar xs"
shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar
proof induct
- fix xs zs assume "good xs" and "T a xs zs"
- show "bar zs" by (rule bar1) (rule lemma3)
+ fix xs zs assume "T a xs zs" and "good xs"
+ hence "good zs" by (rule lemma3)
+ then show "bar zs" by (rule bar1)
next
fix xs ys
assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
assume "bar ys"
thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
proof induct
- fix ys zs assume "good ys" and "T b ys zs"
- show "bar zs" by (rule bar1) (rule lemma3)
+ fix ys zs assume "T b ys zs" and "good ys"
+ then have "good zs" by (rule lemma3)
+ then show "bar zs" by (rule bar1)
next
fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs"
and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs"
@@ -189,8 +191,9 @@
shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar
proof induct
fix xs zs
- assume "good xs" and "R a xs zs"
- show "bar zs" by (rule bar1) (rule lemma2)
+ assume "R a xs zs" and "good xs"
+ then have "good zs" by (rule lemma2)
+ then show "bar zs" by (rule bar1)
next
fix xs zs
assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs"
@@ -299,7 +302,7 @@
thus ?case by iprover
next
case (bar2 ws)
- have "is_prefix (f (length ws) # ws) f" by simp
+ from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp
thus ?case by (iprover intro: bar2)
qed
--- a/src/HOL/Extraction/QuotRem.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Extraction/QuotRem.thy Wed Jun 13 18:30:11 2007 +0200
@@ -30,7 +30,7 @@
thus ?case by iprover
next
assume "r \<noteq> b"
- hence "r < b" by (simp add: order_less_le)
+ with `r \<le> b` have "r < b" by (simp add: order_less_le)
with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp
thus ?case by iprover
qed
--- a/src/HOL/Extraction/Warshall.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Extraction/Warshall.thy Wed Jun 13 18:30:11 2007 +0200
@@ -111,9 +111,10 @@
(\<exists>q. is_path r q i j i) \<and> (\<exists>q'. is_path r q' i i k)"
proof (simp cong add: conj_cong add: split_paired_all is_path_def, (erule conjE)+)
fix xs
- assume "list_all (\<lambda>x. x < Suc i) xs"
- assume "is_path' r j xs k"
- assume "\<not> list_all (\<lambda>x. x < i) xs"
+ assume asms:
+ "list_all (\<lambda>x. x < Suc i) xs"
+ "is_path' r j xs k"
+ "\<not> list_all (\<lambda>x. x < i) xs"
show "(\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i) \<and>
(\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k)"
proof
@@ -182,7 +183,7 @@
qed
qed
qed
- qed
+ qed (rule asms)+
qed
theorem lemma5':
--- a/src/HOL/IMP/Transition.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/IMP/Transition.thy Wed Jun 13 18:30:11 2007 +0200
@@ -366,7 +366,7 @@
"\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
proof
assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
+ then show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
next
assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
@@ -460,7 +460,7 @@
proof -
assume "\<not>b s"
have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
- also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
+ also from `\<not>b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" ..
finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
qed
@@ -471,7 +471,7 @@
proof -
assume "b s"
have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
- also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
+ also from `b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
qed
--- a/src/HOL/Isar_examples/BasicLogic.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Wed Jun 13 18:30:11 2007 +0200
@@ -45,8 +45,8 @@
assume A
show C
proof (rule mp)
- show "B --> C" by (rule mp)
- show B by (rule mp)
+ show "B --> C" by (rule mp) assumption+
+ show B by (rule mp) assumption+
qed
qed
qed
@@ -65,7 +65,7 @@
lemma "A --> A"
proof
assume A
- show A .
+ show A by assumption
qed
text {*
@@ -117,7 +117,7 @@
lemma "A --> B --> A"
proof (intro impI)
assume A
- show A .
+ show A by assumption
qed
text {*
@@ -162,8 +162,8 @@
assume "A & B"
show "B & A"
proof
- show B by (rule conjunct2)
- show A by (rule conjunct1)
+ show B by (rule conjunct2) assumption
+ show A by (rule conjunct1) assumption
qed
qed
@@ -171,10 +171,9 @@
Above, the @{text "conjunct_1/2"} projection rules had to be named
explicitly, since the goals @{text B} and @{text A} did not provide
any structural clue. This may be avoided using \isacommand{from} to
- focus on @{text prems} (i.e.\ the @{text "A \<and> B"} assumption) as the
- current facts, enabling the use of double-dot proofs. Note that
- \isacommand{from} already does forward-chaining, involving the
- \name{conjE} rule here.
+ focus on the @{text "A \<and> B"} assumption as the current facts,
+ enabling the use of double-dot proofs. Note that \isacommand{from}
+ already does forward-chaining, involving the \name{conjE} rule here.
*}
lemma "A & B --> B & A"
@@ -182,8 +181,8 @@
assume "A & B"
show "B & A"
proof
- from prems show B ..
- from prems show A ..
+ from `A & B` show B ..
+ from `A & B` show A ..
qed
qed
@@ -202,8 +201,8 @@
assume "A & B"
then show "B & A"
proof -- {* rule @{text conjE} of @{text "A \<and> B"} *}
- assume A B
- show ?thesis .. -- {* rule @{text conjI} of @{text "B \<and> A"} *}
+ assume B A
+ then show ?thesis .. -- {* rule @{text conjI} of @{text "B \<and> A"} *}
qed
qed
@@ -215,10 +214,10 @@
lemma "A & B --> B & A"
proof
- assume ab: "A & B"
- from ab have a: A ..
- from ab have b: B ..
- from b a show "B & A" ..
+ assume "A & B"
+ from `A & B` have A ..
+ from `A & B` have B ..
+ from `B` `A` show "B & A" ..
qed
text {*
@@ -230,12 +229,12 @@
lemma "A & B --> B & A"
proof -
{
- assume ab: "A & B"
- from ab have a: A ..
- from ab have b: B ..
- from b a have "B & A" ..
+ assume "A & B"
+ from `A & B` have A ..
+ from `A & B` have B ..
+ from `B` `A` have "B & A" ..
}
- thus ?thesis .. -- {* rule \name{impI} *}
+ then show ?thesis .. -- {* rule \name{impI} *}
qed
text {*
@@ -258,19 +257,16 @@
text {*
For our example the most appropriate way of reasoning is probably
the middle one, with conjunction introduction done after
- elimination. This reads even more concisely using
- \isacommand{thus}, which abbreviates
- \isacommand{then}~\isacommand{show}.\footnote{In the same vein,
- \isacommand{hence} abbreviates \isacommand{then}~\isacommand{have}.}
+ elimination.
*}
lemma "A & B --> B & A"
proof
assume "A & B"
- thus "B & A"
+ then show "B & A"
proof
- assume A B
- show ?thesis ..
+ assume B A
+ then show ?thesis ..
qed
qed
@@ -294,13 +290,13 @@
lemma "P | P --> P"
proof
assume "P | P"
- thus P
+ then show P
proof -- {*
rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
*}
- assume P show P .
+ assume P show P by assumption
next
- assume P show P .
+ assume P show P by assumption
qed
qed
@@ -331,11 +327,11 @@
lemma "P | P --> P"
proof
assume "P | P"
- thus P
+ then show P
proof
assume P
- show P .
- show P .
+ show P by assumption
+ show P by assumption
qed
qed
@@ -349,7 +345,7 @@
lemma "P | P --> P"
proof
assume "P | P"
- thus P ..
+ then show P ..
qed
@@ -372,13 +368,13 @@
lemma "(EX x. P (f x)) --> (EX y. P y)"
proof
assume "EX x. P (f x)"
- thus "EX y. P y"
+ then show "EX y. P y"
proof (rule exE) -- {*
rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
*}
fix a
assume "P (f a)" (is "P ?witness")
- show ?thesis by (rule exI [of P ?witness])
+ then show ?thesis by (rule exI [of P ?witness])
qed
qed
@@ -394,11 +390,11 @@
lemma "(EX x. P (f x)) --> (EX y. P y)"
proof
assume "EX x. P (f x)"
- thus "EX y. P y"
+ then show "EX y. P y"
proof
fix a
assume "P (f a)"
- show ?thesis ..
+ then show ?thesis ..
qed
qed
@@ -413,7 +409,7 @@
proof
assume "EX x. P (f x)"
then obtain a where "P (f a)" ..
- thus "EX y. P y" ..
+ then show "EX y. P y" ..
qed
text {*
@@ -443,18 +439,9 @@
assume r: "A ==> B ==> C"
show C
proof (rule r)
- show A by (rule conjunct1)
- show B by (rule conjunct2)
+ show A by (rule conjunct1) assumption
+ show B by (rule conjunct2) assumption
qed
qed
-text {*
- Note that classic Isabelle handles higher rules in a slightly
- different way. The tactic script as given in \cite{isabelle-intro}
- for the same example of \name{conjE} depends on the primitive
- \texttt{goal} command to decompose the rule into premises and
- conclusion. The actual result would then emerge by discharging of
- the context at \texttt{qed} time.
-*}
-
end
--- a/src/HOL/Isar_examples/Cantor.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy Wed Jun 13 18:30:11 2007 +0200
@@ -34,15 +34,15 @@
proof
assume "?S : range f"
then obtain y where "?S = f y" ..
- thus False
+ then show False
proof (rule equalityCE)
assume "y : f y"
- assume "y : ?S" hence "y ~: f y" ..
- thus ?thesis by contradiction
+ assume "y : ?S" then have "y ~: f y" ..
+ with `y : f y` show ?thesis by contradiction
next
assume "y ~: ?S"
- assume "y ~: f y" hence "y : ?S" ..
- thus ?thesis by contradiction
+ assume "y ~: f y" then have "y : ?S" ..
+ with `y ~: ?S` show ?thesis by contradiction
qed
qed
qed
--- a/src/HOL/Isar_examples/ExprCompiler.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy Wed Jun 13 18:30:11 2007 +0200
@@ -121,11 +121,14 @@
case (Cons x xs)
show ?case
proof (induct x)
- case Const show ?case by simp
+ case Const
+ from Cons show ?case by simp
next
- case Load show ?case by simp
+ case Load
+ from Cons show ?case by simp
next
- case Apply show ?case by simp
+ case Apply
+ from Cons show ?case by simp
qed
qed
@@ -139,7 +142,7 @@
next
case Binop then show ?case by (simp add: exec_append)
qed
- thus ?thesis by (simp add: execute_def)
+ then show ?thesis by (simp add: execute_def)
qed
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Wed Jun 13 18:30:11 2007 +0200
@@ -43,12 +43,12 @@
show "(a Un t) Un u : ?T"
proof -
have "a Un (t Un u) : ?T"
+ using `a : A`
proof (rule tiling.Un)
- show "a : A" .
from `(a Un t) Int u = {}` have "t Int u = {}" by blast
then show "t Un u: ?T" by (rule Un)
- have "a <= - t" .
- with `(a Un t) Int u = {}` show "a <= - (t Un u)" by blast
+ from `a <= - t` and `(a Un t) Int u = {}`
+ show "a <= - (t Un u)" by blast
qed
also have "a Un (t Un u) = (a Un t) Un u"
by (simp only: Un_assoc)
@@ -201,7 +201,7 @@
show "?F {}" by (rule finite.emptyI)
fix a t assume "?F t"
assume "a : domino" then have "?F a" by (rule domino_finite)
- then show "?F (a Un t)" by (rule finite_UnI)
+ from this and `?F t` show "?F (a Un t)" by (rule finite_UnI)
qed
lemma tiling_domino_01:
@@ -223,14 +223,17 @@
have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
also obtain i j where e: "?e a b = {(i, j)}"
proof -
+ from `a \<in> domino` and `b < 2`
have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
then show ?thesis by (blast intro: that)
qed
also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
also have "card ... = Suc (card (?e t b))"
proof (rule card_insert_disjoint)
- show "finite (?e t b)"
- by (rule evnodd_finite, rule tiling_domino_finite)
+ from `t \<in> tiling domino` have "finite t"
+ by (rule tiling_domino_finite)
+ then show "finite (?e t b)"
+ by (rule evnodd_finite)
from e have "(i, j) : ?e a b" by simp
with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
qed
--- a/src/HOL/Isar_examples/NestedDatatype.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/NestedDatatype.thy Wed Jun 13 18:30:11 2007 +0200
@@ -44,12 +44,14 @@
fix a show "?P (Var a)" by simp
next
fix b ts assume "?Q ts"
- thus "?P (App b ts)" by (simp add: o_def)
+ then show "?P (App b ts)"
+ by (simp only: subst.simps)
next
show "?Q []" by simp
next
fix t ts
- assume "?P t" "?Q ts" thus "?Q (t # ts)" by simp
+ assume "?P t" "?Q ts" then show "?Q (t # ts)"
+ by (simp only: subst.simps)
qed
qed
@@ -64,12 +66,12 @@
fix a show "P (Var a)" by (rule var)
next
fix b t ts assume "list_all P ts"
- thus "P (App b ts)" by (rule app)
+ then show "P (App b ts)" by (rule app)
next
show "list_all P []" by simp
next
fix t ts assume "P t" "list_all P ts"
- thus "list_all P (t # ts)" by simp
+ then show "list_all P (t # ts)" by simp
qed
lemma
@@ -79,7 +81,7 @@
show ?case by (simp add: o_def)
next
case (App b ts)
- thus ?case by (induct ts) simp_all
+ then show ?case by (induct ts) simp_all
qed
end
--- a/src/HOL/Isar_examples/Peirce.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy Wed Jun 13 18:30:11 2007 +0200
@@ -21,16 +21,16 @@
theorem "((A --> B) --> A) --> A"
proof
- assume aba: "(A --> B) --> A"
+ assume "(A --> B) --> A"
show A
proof (rule classical)
assume "~ A"
have "A --> B"
proof
assume A
- thus B by contradiction
+ with `~ A` show B by contradiction
qed
- with aba show A ..
+ with `(A --> B) --> A` show A ..
qed
qed
@@ -52,17 +52,17 @@
theorem "((A --> B) --> A) --> A"
proof
- assume aba: "(A --> B) --> A"
+ assume "(A --> B) --> A"
show A
proof (rule classical)
presume "A --> B"
- with aba show A ..
+ with `(A --> B) --> A` show A ..
next
assume "~ A"
show "A --> B"
proof
assume A
- thus B by contradiction
+ with `~ A` show B by contradiction
qed
qed
qed
--- a/src/HOL/Lattice/Bounds.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Lattice/Bounds.thy Wed Jun 13 18:30:11 2007 +0200
@@ -147,7 +147,7 @@
from sup show "is_inf (dual x) (dual y) (dual sup)" ..
from sup' show "is_inf (dual x) (dual y) (dual sup')" ..
qed
- thus "sup = sup'" ..
+ then show "sup = sup'" ..
qed
theorem is_Inf_uniq: "is_Inf A inf \<Longrightarrow> is_Inf A inf' \<Longrightarrow> inf = inf'"
@@ -159,12 +159,12 @@
from inf' show "inf \<sqsubseteq> inf'"
proof (rule is_Inf_greatest)
fix x assume "x \<in> A"
- from inf show "inf \<sqsubseteq> x" ..
+ with inf show "inf \<sqsubseteq> x" ..
qed
from inf show "inf' \<sqsubseteq> inf"
proof (rule is_Inf_greatest)
fix x assume "x \<in> A"
- from inf' show "inf' \<sqsubseteq> x" ..
+ with inf' show "inf' \<sqsubseteq> x" ..
qed
qed
qed
@@ -177,7 +177,7 @@
from sup show "is_Inf (dual ` A) (dual sup)" ..
from sup' show "is_Inf (dual ` A) (dual sup')" ..
qed
- thus "sup = sup'" ..
+ then show "sup = sup'" ..
qed
@@ -193,8 +193,8 @@
show ?thesis
proof
show "x \<sqsubseteq> x" ..
- show "x \<sqsubseteq> y" .
- fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" .
+ show "x \<sqsubseteq> y" by assumption
+ fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by assumption
qed
qed
@@ -203,10 +203,10 @@
assume "x \<sqsubseteq> y"
show ?thesis
proof
- show "x \<sqsubseteq> y" .
+ show "x \<sqsubseteq> y" by assumption
show "y \<sqsubseteq> y" ..
fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
- show "y \<sqsubseteq> z" .
+ show "y \<sqsubseteq> z" by assumption
qed
qed
@@ -233,8 +233,8 @@
from is_Inf show "z \<sqsubseteq> inf"
proof (rule is_Inf_greatest)
fix a assume "a \<in> ?A"
- hence "a = x \<or> a = y" by blast
- thus "z \<sqsubseteq> a"
+ then have "a = x \<or> a = y" by blast
+ then show "z \<sqsubseteq> a"
proof
assume "a = x"
with zx show ?thesis by simp
@@ -249,8 +249,8 @@
show "is_Inf {x, y} inf"
proof
fix a assume "a \<in> ?A"
- hence "a = x \<or> a = y" by blast
- thus "inf \<sqsubseteq> a"
+ then have "a = x \<or> a = y" by blast
+ then show "inf \<sqsubseteq> a"
proof
assume "a = x"
also from is_inf have "inf \<sqsubseteq> x" ..
@@ -304,12 +304,12 @@
from is_Inf show "x \<sqsubseteq> sup"
proof (rule is_Inf_greatest)
fix y assume "y \<in> ?B"
- hence "\<forall>a \<in> A. a \<sqsubseteq> y" ..
+ then have "\<forall>a \<in> A. a \<sqsubseteq> y" ..
from this x show "x \<sqsubseteq> y" ..
qed
next
fix z assume "\<forall>x \<in> A. x \<sqsubseteq> z"
- hence "z \<in> ?B" ..
+ then have "z \<in> ?B" ..
with is_Inf show "sup \<sqsubseteq> z" ..
qed
qed
@@ -317,14 +317,14 @@
theorem Sup_Inf: "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf \<Longrightarrow> is_Inf A inf"
proof -
assume "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf"
- hence "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
+ then have "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
by (simp only: dual_Inf dual_leq)
also have "dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual ` A. a' \<sqsubseteq> b'}"
by (auto iff: dual_ball dual_Collect simp add: image_Collect) (* FIXME !? *)
finally have "is_Inf \<dots> (dual inf)" .
- hence "is_Sup (dual ` A) (dual inf)"
+ then have "is_Sup (dual ` A) (dual inf)"
by (rule Inf_Sup)
- thus ?thesis ..
+ then show ?thesis ..
qed
end
--- a/src/HOL/Lattice/CompleteLattice.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy Wed Jun 13 18:30:11 2007 +0200
@@ -22,8 +22,8 @@
theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"
proof -
from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast
- hence "is_Sup A sup" by (rule Inf_Sup)
- thus ?thesis ..
+ then have "is_Sup A sup" by (rule Inf_Sup)
+ then show ?thesis ..
qed
text {*
@@ -50,8 +50,8 @@
lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf"
proof (unfold Meet_def)
assume "is_Inf A inf"
- thus "(THE inf. is_Inf A inf) = inf"
- by (rule the_equality) (rule is_Inf_uniq)
+ then show "(THE inf. is_Inf A inf) = inf"
+ by (rule the_equality) (rule is_Inf_uniq [OF _ `is_Inf A inf`])
qed
lemma MeetI [intro?]:
@@ -63,8 +63,8 @@
lemma Join_equality [elim?]: "is_Sup A sup \<Longrightarrow> \<Squnion>A = sup"
proof (unfold Join_def)
assume "is_Sup A sup"
- thus "(THE sup. is_Sup A sup) = sup"
- by (rule the_equality) (rule is_Sup_uniq)
+ then show "(THE sup. is_Sup A sup) = sup"
+ by (rule the_equality) (rule is_Sup_uniq [OF _ `is_Sup A sup`])
qed
lemma JoinI [intro?]:
@@ -82,7 +82,8 @@
lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
proof (unfold Meet_def)
from ex_Inf obtain inf where "is_Inf A inf" ..
- thus "is_Inf A (THE inf. is_Inf A inf)" by (rule theI) (rule is_Inf_uniq)
+ then show "is_Inf A (THE inf. is_Inf A inf)"
+ by (rule theI) (rule is_Inf_uniq [OF _ `is_Inf A inf`])
qed
lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
@@ -95,7 +96,8 @@
lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
proof (unfold Join_def)
from ex_Sup obtain sup where "is_Sup A sup" ..
- thus "is_Sup A (THE sup. is_Sup A sup)" by (rule theI) (rule is_Sup_uniq)
+ then show "is_Sup A (THE sup. is_Sup A sup)"
+ by (rule theI) (rule is_Sup_uniq [OF _ `is_Sup A sup`])
qed
lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
@@ -122,15 +124,15 @@
have ge: "f ?a \<sqsubseteq> ?a"
proof
fix x assume x: "x \<in> ?H"
- hence "?a \<sqsubseteq> x" ..
- hence "f ?a \<sqsubseteq> f x" by (rule mono)
+ then have "?a \<sqsubseteq> x" ..
+ then have "f ?a \<sqsubseteq> f x" by (rule mono)
also from x have "... \<sqsubseteq> x" ..
finally show "f ?a \<sqsubseteq> x" .
qed
also have "?a \<sqsubseteq> f ?a"
proof
from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
- thus "f ?a \<in> ?H" ..
+ then show "f ?a \<in> ?H" ..
qed
finally show "f ?a = ?a" .
qed
@@ -153,7 +155,7 @@
lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
proof (unfold bottom_def)
have "x \<in> UNIV" ..
- thus "\<Sqinter>UNIV \<sqsubseteq> x" ..
+ then show "\<Sqinter>UNIV \<sqsubseteq> x" ..
qed
lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x"
@@ -161,7 +163,7 @@
assume "\<And>a. x \<sqsubseteq> a"
show "\<Sqinter>UNIV = x"
proof
- fix a show "x \<sqsubseteq> a" .
+ fix a show "x \<sqsubseteq> a" by fact
next
fix b :: "'a::complete_lattice"
assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a"
@@ -173,7 +175,7 @@
lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>"
proof (unfold top_def)
have "x \<in> UNIV" ..
- thus "x \<sqsubseteq> \<Squnion>UNIV" ..
+ then show "x \<sqsubseteq> \<Squnion>UNIV" ..
qed
lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x"
@@ -181,7 +183,7 @@
assume "\<And>a. a \<sqsubseteq> x"
show "\<Squnion>UNIV = x"
proof
- fix a show "a \<sqsubseteq> x" .
+ fix a show "a \<sqsubseteq> x" by fact
next
fix b :: "'a::complete_lattice"
assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b"
@@ -204,8 +206,8 @@
show "\<exists>inf'. is_Inf A' inf'"
proof -
have "\<exists>sup. is_Sup (undual ` A') sup" by (rule ex_Sup)
- hence "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
- thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
+ then have "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
+ then show ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
qed
qed
@@ -217,15 +219,15 @@
theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual ` A)"
proof -
from is_Inf_Meet have "is_Sup (dual ` A) (dual (\<Sqinter>A))" ..
- hence "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" ..
- thus ?thesis ..
+ then have "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" ..
+ then show ?thesis ..
qed
theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual ` A)"
proof -
from is_Sup_Join have "is_Inf (dual ` A) (dual (\<Squnion>A))" ..
- hence "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" ..
- thus ?thesis ..
+ then have "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" ..
+ then show ?thesis ..
qed
text {*
@@ -237,10 +239,10 @@
have "\<top> = dual \<bottom>"
proof
fix a' have "\<bottom> \<sqsubseteq> undual a'" ..
- hence "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
- thus "a' \<sqsubseteq> dual \<bottom>" by simp
+ then have "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
+ then show "a' \<sqsubseteq> dual \<bottom>" by simp
qed
- thus ?thesis ..
+ then show ?thesis ..
qed
theorem dual_top [intro?]: "dual \<top> = \<bottom>"
@@ -248,10 +250,10 @@
have "\<bottom> = dual \<top>"
proof
fix a' have "undual a' \<sqsubseteq> \<top>" ..
- hence "dual \<top> \<sqsubseteq> dual (undual a')" ..
- thus "dual \<top> \<sqsubseteq> a'" by simp
+ then have "dual \<top> \<sqsubseteq> dual (undual a')" ..
+ then show "dual \<top> \<sqsubseteq> a'" by simp
qed
- thus ?thesis ..
+ then show ?thesis ..
qed
@@ -267,13 +269,13 @@
lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})"
proof -
have "is_Inf {x, y} (\<Sqinter>{x, y})" ..
- thus ?thesis by (simp only: is_Inf_binary)
+ then show ?thesis by (simp only: is_Inf_binary)
qed
lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})"
proof -
have "is_Sup {x, y} (\<Squnion>{x, y})" ..
- thus ?thesis by (simp only: is_Sup_binary)
+ then show ?thesis by (simp only: is_Sup_binary)
qed
instance complete_lattice \<subseteq> lattice
@@ -302,16 +304,16 @@
fix a assume "a \<in> A"
also assume "A \<subseteq> B"
finally have "a \<in> B" .
- thus "\<Sqinter>B \<sqsubseteq> a" ..
+ then show "\<Sqinter>B \<sqsubseteq> a" ..
qed
theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
proof -
assume "A \<subseteq> B"
- hence "dual ` A \<subseteq> dual ` B" by blast
- hence "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono)
- hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
- thus ?thesis by (simp only: dual_leq)
+ then have "dual ` A \<subseteq> dual ` B" by blast
+ then have "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono)
+ then have "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
+ then show ?thesis by (simp only: dual_leq)
qed
text {*
@@ -321,7 +323,7 @@
theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
proof
fix a assume "a \<in> A \<union> B"
- thus "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
+ then show "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
proof
assume a: "a \<in> A"
have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" ..
@@ -340,13 +342,13 @@
show "b \<sqsubseteq> \<Sqinter>A"
proof
fix a assume "a \<in> A"
- hence "a \<in> A \<union> B" ..
+ then have "a \<in> A \<union> B" ..
with b show "b \<sqsubseteq> a" ..
qed
show "b \<sqsubseteq> \<Sqinter>B"
proof
fix a assume "a \<in> B"
- hence "a \<in> A \<union> B" ..
+ then have "a \<in> A \<union> B" ..
with b show "b \<sqsubseteq> a" ..
qed
qed
@@ -370,11 +372,11 @@
theorem Meet_singleton: "\<Sqinter>{x} = x"
proof
fix a assume "a \<in> {x}"
- hence "a = x" by simp
- thus "x \<sqsubseteq> a" by (simp only: leq_refl)
+ then have "a = x" by simp
+ then show "x \<sqsubseteq> a" by (simp only: leq_refl)
next
fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a"
- thus "b \<sqsubseteq> x" by simp
+ then show "b \<sqsubseteq> x" by simp
qed
theorem Join_singleton: "\<Squnion>{x} = x"
@@ -392,12 +394,12 @@
proof
fix a :: "'a::complete_lattice"
assume "a \<in> {}"
- hence False by simp
- thus "\<Squnion>UNIV \<sqsubseteq> a" ..
+ then have False by simp
+ then show "\<Squnion>UNIV \<sqsubseteq> a" ..
next
fix b :: "'a::complete_lattice"
have "b \<in> UNIV" ..
- thus "b \<sqsubseteq> \<Squnion>UNIV" ..
+ then show "b \<sqsubseteq> \<Squnion>UNIV" ..
qed
theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV"
--- a/src/HOL/Lattice/Lattice.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Lattice/Lattice.thy Wed Jun 13 18:30:11 2007 +0200
@@ -43,8 +43,8 @@
lemma meet_equality [elim?]: "is_inf x y inf \<Longrightarrow> x \<sqinter> y = inf"
proof (unfold meet_def)
assume "is_inf x y inf"
- thus "(THE inf. is_inf x y inf) = inf"
- by (rule the_equality) (rule is_inf_uniq)
+ then show "(THE inf. is_inf x y inf) = inf"
+ by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y inf`])
qed
lemma meetI [intro?]:
@@ -54,8 +54,8 @@
lemma join_equality [elim?]: "is_sup x y sup \<Longrightarrow> x \<squnion> y = sup"
proof (unfold join_def)
assume "is_sup x y sup"
- thus "(THE sup. is_sup x y sup) = sup"
- by (rule the_equality) (rule is_sup_uniq)
+ then show "(THE sup. is_sup x y sup) = sup"
+ by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y sup`])
qed
lemma joinI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
@@ -71,7 +71,8 @@
lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
proof (unfold meet_def)
from ex_inf obtain inf where "is_inf x y inf" ..
- thus "is_inf x y (THE inf. is_inf x y inf)" by (rule theI) (rule is_inf_uniq)
+ then show "is_inf x y (THE inf. is_inf x y inf)"
+ by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y inf`])
qed
lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
@@ -87,7 +88,8 @@
lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
proof (unfold join_def)
from ex_sup obtain sup where "is_sup x y sup" ..
- thus "is_sup x y (THE sup. is_sup x y sup)" by (rule theI) (rule is_sup_uniq)
+ then show "is_sup x y (THE sup. is_sup x y sup)"
+ by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y sup`])
qed
lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
@@ -115,16 +117,16 @@
show "\<exists>inf'. is_inf x' y' inf'"
proof -
have "\<exists>sup. is_sup (undual x') (undual y') sup" by (rule ex_sup)
- hence "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
+ then have "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
by (simp only: dual_inf)
- thus ?thesis by (simp add: dual_ex [symmetric])
+ then show ?thesis by (simp add: dual_ex [symmetric])
qed
show "\<exists>sup'. is_sup x' y' sup'"
proof -
have "\<exists>inf. is_inf (undual x') (undual y') inf" by (rule ex_inf)
- hence "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
+ then have "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
by (simp only: dual_sup)
- thus ?thesis by (simp add: dual_ex [symmetric])
+ then show ?thesis by (simp add: dual_ex [symmetric])
qed
qed
@@ -136,15 +138,15 @@
theorem dual_meet [intro?]: "dual (x \<sqinter> y) = dual x \<squnion> dual y"
proof -
from is_inf_meet have "is_sup (dual x) (dual y) (dual (x \<sqinter> y))" ..
- hence "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..
- thus ?thesis ..
+ then have "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..
+ then show ?thesis ..
qed
theorem dual_join [intro?]: "dual (x \<squnion> y) = dual x \<sqinter> dual y"
proof -
from is_sup_join have "is_inf (dual x) (dual y) (dual (x \<squnion> y))" ..
- hence "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..
- thus ?thesis ..
+ then have "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..
+ then show ?thesis ..
qed
@@ -179,7 +181,7 @@
proof
show "w \<sqsubseteq> x"
proof -
- have "w \<sqsubseteq> x \<sqinter> y" .
+ have "w \<sqsubseteq> x \<sqinter> y" by fact
also have "\<dots> \<sqsubseteq> x" ..
finally show ?thesis .
qed
@@ -187,11 +189,11 @@
proof
show "w \<sqsubseteq> y"
proof -
- have "w \<sqsubseteq> x \<sqinter> y" .
+ have "w \<sqsubseteq> x \<sqinter> y" by fact
also have "\<dots> \<sqsubseteq> y" ..
finally show ?thesis .
qed
- show "w \<sqsubseteq> z" .
+ show "w \<sqsubseteq> z" by fact
qed
qed
qed
@@ -211,8 +213,8 @@
proof
show "y \<sqinter> x \<sqsubseteq> x" ..
show "y \<sqinter> x \<sqsubseteq> y" ..
- fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
- show "z \<sqsubseteq> y \<sqinter> x" ..
+ fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
+ then show "z \<sqsubseteq> y \<sqinter> x" ..
qed
theorem join_commute: "x \<squnion> y = y \<squnion> x"
@@ -230,16 +232,16 @@
show "x \<sqsubseteq> x" ..
show "x \<sqsubseteq> x \<squnion> y" ..
fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
- show "z \<sqsubseteq> x" .
+ show "z \<sqsubseteq> x" by assumption
qed
theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
proof -
have "dual x \<sqinter> (dual x \<squnion> dual y) = dual x"
by (rule meet_join_absorb)
- hence "dual (x \<squnion> (x \<sqinter> y)) = dual x"
+ then have "dual (x \<squnion> (x \<sqinter> y)) = dual x"
by (simp only: dual_meet dual_join)
- thus ?thesis ..
+ then show ?thesis ..
qed
text {*
@@ -258,9 +260,9 @@
proof -
have "dual x \<sqinter> dual x = dual x"
by (rule meet_idem)
- hence "dual (x \<squnion> x) = dual x"
+ then have "dual (x \<squnion> x) = dual x"
by (simp only: dual_join)
- thus ?thesis ..
+ then show ?thesis ..
qed
text {*
@@ -271,14 +273,15 @@
proof
assume "x \<sqsubseteq> y"
show "x \<sqsubseteq> x" ..
- show "x \<sqsubseteq> y" .
- fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" .
+ show "x \<sqsubseteq> y" by fact
+ fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
+ show "z \<sqsubseteq> x" by fact
qed
theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
proof -
- assume "x \<sqsubseteq> y" hence "dual y \<sqsubseteq> dual x" ..
- hence "dual y \<sqinter> dual x = dual y" by (rule meet_related)
+ assume "x \<sqsubseteq> y" then have "dual y \<sqsubseteq> dual x" ..
+ then have "dual y \<sqinter> dual x = dual y" by (rule meet_related)
also have "dual y \<sqinter> dual x = dual (y \<squnion> x)" by (simp only: dual_join)
also have "y \<squnion> x = x \<squnion> y" by (rule join_commute)
finally show ?thesis ..
@@ -295,8 +298,8 @@
theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
proof
assume "x \<sqsubseteq> y"
- hence "is_inf x y x" ..
- thus "x \<sqinter> y = x" ..
+ then have "is_inf x y x" ..
+ then show "x \<sqinter> y = x" ..
next
have "x \<sqinter> y \<sqsubseteq> y" ..
also assume "x \<sqinter> y = x"
@@ -306,8 +309,8 @@
theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
proof
assume "x \<sqsubseteq> y"
- hence "is_sup x y y" ..
- thus "x \<squnion> y = y" ..
+ then have "is_sup x y y" ..
+ then show "x \<squnion> y = y" ..
next
have "x \<sqsubseteq> x \<squnion> y" ..
also assume "x \<squnion> y = y"
@@ -555,27 +558,27 @@
assume "a \<sqsubseteq> c" have "a \<sqinter> b \<sqsubseteq> c \<sqinter> b"
proof
have "a \<sqinter> b \<sqsubseteq> a" ..
- also have "\<dots> \<sqsubseteq> c" .
+ also have "\<dots> \<sqsubseteq> c" by fact
finally show "a \<sqinter> b \<sqsubseteq> c" .
show "a \<sqinter> b \<sqsubseteq> b" ..
qed
} note this [elim?]
- assume "x \<sqsubseteq> z" hence "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..
+ assume "x \<sqsubseteq> z" then have "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..
also have "\<dots> = y \<sqinter> z" by (rule meet_commute)
- also assume "y \<sqsubseteq> w" hence "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..
+ also assume "y \<sqsubseteq> w" then have "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..
also have "\<dots> = z \<sqinter> w" by (rule meet_commute)
finally show ?thesis .
qed
theorem join_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<squnion> y \<sqsubseteq> z \<squnion> w"
proof -
- assume "x \<sqsubseteq> z" hence "dual z \<sqsubseteq> dual x" ..
- moreover assume "y \<sqsubseteq> w" hence "dual w \<sqsubseteq> dual y" ..
+ assume "x \<sqsubseteq> z" then have "dual z \<sqsubseteq> dual x" ..
+ moreover assume "y \<sqsubseteq> w" then have "dual w \<sqsubseteq> dual y" ..
ultimately have "dual z \<sqinter> dual w \<sqsubseteq> dual x \<sqinter> dual y"
by (rule meet_mono)
- hence "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"
+ then have "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"
by (simp only: dual_join)
- thus ?thesis ..
+ then show ?thesis ..
qed
text {*
@@ -590,8 +593,8 @@
proof
assume morph: "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
fix x y :: "'a::lattice"
- assume "x \<sqsubseteq> y" hence "x \<sqinter> y = x" ..
- hence "x = x \<sqinter> y" ..
+ assume "x \<sqsubseteq> y" then have "x \<sqinter> y = x" ..
+ then have "x = x \<sqinter> y" ..
also have "f \<dots> \<sqsubseteq> f x \<sqinter> f y" by (rule morph)
also have "\<dots> \<sqsubseteq> f y" ..
finally show "f x \<sqsubseteq> f y" .
@@ -602,8 +605,8 @@
fix x y
show "f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
proof
- have "x \<sqinter> y \<sqsubseteq> x" .. thus "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)
- have "x \<sqinter> y \<sqsubseteq> y" .. thus "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)
+ have "x \<sqinter> y \<sqsubseteq> x" .. then show "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)
+ have "x \<sqinter> y \<sqsubseteq> y" .. then show "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)
qed
qed
qed
--- a/src/HOL/Library/AssocList.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/AssocList.thy Wed Jun 13 18:30:11 2007 +0200
@@ -19,7 +19,7 @@
fun
delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where
- "delete k [] = []"
+ "delete k [] = []"
| "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
fun
@@ -79,27 +79,25 @@
fun
restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where
- "restrict A [] = []"
+ "restrict A [] = []"
| "restrict A (p#ps) = (if fst p \<in> A then p#restrict A ps else restrict A ps)"
fun
map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where
- "map_ran f [] = []"
+ "map_ran f [] = []"
| "map_ran f (p#ps) = (fst p, f (fst p) (snd p)) # map_ran f ps"
fun
clearjunk :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where
- "clearjunk [] = []"
+ "clearjunk [] = []"
| "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
lemmas [simp del] = compose_hint
-(* ******************************************************************************** *)
subsection {* Lookup *}
-(* ******************************************************************************** *)
lemma lookup_simps [code func]:
"map_of [] k = None"
@@ -107,9 +105,7 @@
by simp_all
-(* ******************************************************************************** *)
subsection {* @{const delete} *}
-(* ******************************************************************************** *)
lemma delete_def:
"delete k xs = filter (\<lambda>p. fst p \<noteq> k) xs"
@@ -140,7 +136,7 @@
lemma distinct_delete:
assumes "distinct (map fst al)"
shows "distinct (map fst (delete k al))"
-using prems
+using assms
proof (induct al)
case Nil thus ?case by simp
next
@@ -152,7 +148,7 @@
show ?case
proof (cases "fst a = k")
case True
- from True dist_al show ?thesis by simp
+ with Cons dist_al show ?thesis by simp
next
case False
from dist_al
@@ -171,9 +167,8 @@
lemma clearjunk_delete: "clearjunk (delete x al) = delete x (clearjunk al)"
by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
-(* ******************************************************************************** *)
+
subsection {* @{const clearjunk} *}
-(* ******************************************************************************** *)
lemma insert_fst_filter:
"insert a(fst ` {x \<in> set ps. fst x \<noteq> a}) = insert a (fst ` set ps)"
@@ -221,9 +216,8 @@
lemma clearjunk_idem: "clearjunk (clearjunk al) = clearjunk al"
by simp
-(* ******************************************************************************** *)
+
subsection {* @{const dom} and @{term "ran"} *}
-(* ******************************************************************************** *)
lemma dom_map_of': "fst ` set al = dom (map_of al)"
by (induct al) auto
@@ -295,9 +289,8 @@
finally show ?thesis .
qed
-(* ******************************************************************************** *)
+
subsection {* @{const update} *}
-(* ******************************************************************************** *)
lemma update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
by (induct al) auto
@@ -311,7 +304,7 @@
lemma distinct_update:
assumes "distinct (map fst al)"
shows "distinct (map fst (update k v al))"
-using prems
+using assms
proof (induct al)
case Nil thus ?case by simp
next
@@ -374,9 +367,7 @@
by (simp add: update_conv' image_map_upd)
-(* ******************************************************************************** *)
subsection {* @{const updates} *}
-(* ******************************************************************************** *)
lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
proof (induct ks arbitrary: vs al)
@@ -401,7 +392,7 @@
lemma distinct_updates:
assumes "distinct (map fst al)"
shows "distinct (map fst (updates ks vs al))"
- using prems
+ using assms
by (induct ks arbitrary: vs al)
(auto simp add: distinct_update split: list.splits)
@@ -447,9 +438,8 @@
"size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
by (induct xs arbitrary: ys al) (auto split: list.splits)
-(* ******************************************************************************** *)
+
subsection {* @{const map_ran} *}
-(* ******************************************************************************** *)
lemma map_ran_conv: "map_of (map_ran f al) k = option_map (f k) (map_of al k)"
by (induct al) auto
@@ -466,9 +456,8 @@
lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
by (induct al rule: clearjunk.induct) (auto simp add: delete_def map_ran_filter)
-(* ******************************************************************************** *)
+
subsection {* @{const merge} *}
-(* ******************************************************************************** *)
lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
by (induct ys arbitrary: xs) (auto simp add: dom_update)
@@ -476,7 +465,7 @@
lemma distinct_merge:
assumes "distinct (map fst xs)"
shows "distinct (map fst (merge xs ys))"
- using prems
+ using assms
by (induct ys arbitrary: xs) (auto simp add: dom_merge distinct_update)
lemma clearjunk_merge:
@@ -536,14 +525,13 @@
lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)"
by (simp add: merge_conv')
-(* ******************************************************************************** *)
+
subsection {* @{const compose} *}
-(* ******************************************************************************** *)
lemma compose_first_None [simp]:
assumes "map_of xs k = None"
shows "map_of (compose xs ys) k = None"
-using prems by (induct xs ys rule: compose.induct)
+using assms by (induct xs ys rule: compose.induct)
(auto split: option.splits split_if_asm)
lemma compose_conv:
@@ -591,7 +579,7 @@
lemma compose_first_Some [simp]:
assumes "map_of xs k = Some v"
shows "map_of (compose xs ys) k = map_of ys v"
-using prems by (simp add: compose_conv)
+using assms by (simp add: compose_conv)
lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
proof (induct xs ys rule: compose.induct)
@@ -623,7 +611,7 @@
lemma distinct_compose:
assumes "distinct (map fst xs)"
shows "distinct (map fst (compose xs ys))"
-using prems
+using assms
proof (induct xs ys rule: compose.induct)
case 1 thus ?case by simp
next
@@ -695,9 +683,7 @@
by (simp add: compose_conv map_comp_None_iff)
-(* ******************************************************************************** *)
subsection {* @{const restrict} *}
-(* ******************************************************************************** *)
lemma restrict_def:
"restrict A = filter (\<lambda>p. fst p \<in> A)"
--- a/src/HOL/Library/BigO.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/BigO.thy Wed Jun 13 18:30:11 2007 +0200
@@ -282,7 +282,7 @@
apply (subst func_diff)
apply (rule bigo_abs)
done
- also have "... <= O(h)"
+ also from a have "... <= O(h)"
by (rule bigo_elt_subset)
finally show "(%x. abs (f x) - abs (g x)) : O(h)".
qed
--- a/src/HOL/Library/Graphs.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/Graphs.thy Wed Jun 13 18:30:11 2007 +0200
@@ -3,7 +3,7 @@
Author: Alexander Krauss, TU Muenchen
*)
-header ""
+header "" (* FIXME proper header *)
theory Graphs
imports Main SCT_Misc Kleene_Algebras ExecutableSet
@@ -56,8 +56,8 @@
lemma graph_ext:
assumes "\<And>n e n'. has_edge G n e n' = has_edge H n e n'"
shows "G = H"
- using prems
- by (cases G, cases H, auto simp:split_paired_all has_edge_def)
+ using assms
+ by (cases G, cases H) (auto simp:split_paired_all has_edge_def)
instance graph :: (type, type) "{comm_monoid_add}"
@@ -219,7 +219,7 @@
lemma graph_leqI:
assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
shows "G \<le> H"
- using prems
+ using assms
unfolding graph_leq_def has_edge_def
by auto
@@ -229,18 +229,18 @@
assumes "has_edge G n e n' \<Longrightarrow> P"
assumes "has_edge H n e n' \<Longrightarrow> P"
shows P
- using prems
+ using assms
by (auto simp: in_grplus)
lemma
assumes "x \<in> S k"
shows "x \<in> (\<Union>k. S k)"
- using prems by blast
+ using assms by blast
lemma graph_union_least:
assumes "\<And>n. Graph (G n) \<le> C"
shows "Graph (\<Union>n. G n) \<le> C"
- using prems unfolding graph_leq_def
+ using assms unfolding graph_leq_def
by auto
lemma Sup_graph_eq:
@@ -333,15 +333,15 @@
lemma endnode_nth:
assumes "length (snd p) = Suc k"
shows "end_node p = snd (snd (path_nth p k))"
- using prems unfolding end_node_def path_nth_def
+ using assms unfolding end_node_def path_nth_def
by auto
lemma path_nth_graph:
assumes "k < length (snd p)"
assumes "has_fpath G p"
shows "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p k)"
- using prems
-proof (induct k arbitrary:p)
+using assms
+proof (induct k arbitrary: p)
case 0 thus ?case
unfolding path_nth_def by (auto elim:has_fpath.cases)
next
@@ -364,7 +364,7 @@
lemma path_nth_connected:
assumes "Suc k < length (snd p)"
shows "fst (path_nth p (Suc k)) = snd (snd (path_nth p k))"
- using prems
+ using assms
unfolding path_nth_def
by auto
@@ -399,9 +399,9 @@
hence "fst (path_nth p (Suc i mod ?l)) = fst (path_nth p 0)"
by (simp add: mod_Suc)
also from fst_p0 have "\<dots> = fst p" .
- also have "\<dots> = end_node p" .
+ also have "\<dots> = end_node p" by assumption
also have "\<dots> = snd (snd (path_nth p ?k))"
- by (auto simp:endnode_nth wrap)
+ by (auto simp: endnode_nth wrap)
finally show ?thesis .
qed
qed
@@ -411,17 +411,21 @@
and loop: "fst p = end_node p"
and nonempty: "0 < length (snd p)" (is "0 < ?l")
shows "has_ipath G (omega p)"
-proof (auto simp:has_ipath_def)
- fix i
- from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
- by simp
- with path_nth_graph
- have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)" .
+proof -
+ {
+ fix i
+ from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
+ by simp
+ from this and `has_fpath G p`
+ have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)"
+ by (rule path_nth_graph)
- from path_loop_connect[OF loop nonempty] pk_G
- show "has_edge G (fst (omega p i)) (snd (omega p i)) (fst (omega p (Suc i)))"
- unfolding path_loop_def has_edge_def split_def
- by simp
+ from path_loop_connect[OF loop nonempty] pk_G
+ have "has_edge G (fst (omega p i)) (snd (omega p i)) (fst (omega p (Suc i)))"
+ unfolding path_loop_def has_edge_def split_def
+ by simp
+ }
+ then show ?thesis by (auto simp:has_ipath_def)
qed
definition prod :: "('n, 'e::monoid_mult) fpath \<Rightarrow> 'e"
@@ -514,7 +518,7 @@
lemma upto_append[simp]:
assumes "i \<le> j" "j \<le> k"
shows "[ i ..< j ] @ [j ..< k] = [i ..< k]"
- using prems and upt_add_eq_append[of i j "k - j"]
+ using assms and upt_add_eq_append[of i j "k - j"]
by simp
lemma foldr_monoid: "foldr (op *) xs 1 * foldr (op *) ys 1
@@ -525,7 +529,7 @@
assumes "i < j"
assumes "j < k"
shows "prod (p\<langle>i,k\<rangle>) = prod (p\<langle>i,j\<rangle>) * prod (p\<langle>j,k\<rangle>)"
- using prems
+ using assms
unfolding prod_def sub_path_def
by (simp add:map_compose[symmetric] comp_def)
(simp only:foldr_monoid map_append[symmetric] upto_append)
@@ -535,7 +539,7 @@
assumes "length es = l"
assumes "has_fpath G (n,es)"
shows "has_edge (G ^ l) n (prod (n,es)) (end_node (n,es))"
-using prems
+using assms
proof (induct l arbitrary:n es)
case 0 thus ?case
by (simp add:in_grunit end_node_def)
@@ -679,7 +683,7 @@
lemma sub_path_loop:
assumes "0 < k"
- assumes k:"k = length (snd loop)"
+ assumes k: "k = length (snd loop)"
assumes loop: "fst loop = end_node loop"
shows "(omega loop)\<langle>k * i,k * Suc i\<rangle> = loop" (is "?\<omega> = loop")
proof (rule prod_eqI)
@@ -698,14 +702,17 @@
= snd (snd (path_nth loop (i mod k)))"
unfolding k
apply (rule path_loop_connect[OF loop])
- by (insert prems, auto)
+ using `0 < k` and k
+ apply auto
+ done
from `j < k`
show "snd ?\<omega> ! j = snd loop ! j"
unfolding sub_path_def
apply (simp add:path_loop_def split_def add_ac)
apply (simp add:a k[symmetric])
- by (simp add:path_nth_def)
+ apply (simp add:path_nth_def)
+ done
qed
qed
--- a/src/HOL/Library/Multiset.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Jun 13 18:30:11 2007 +0200
@@ -450,7 +450,7 @@
proof (elim exE disjE conjE)
fix M assume "?R M M0" and N: "N = M + {#a#}"
from acc_hyp have "?R M M0 --> ?W (M + {#a#})" ..
- then have "?W (M + {#a#})" ..
+ from this and `?R M M0` have "?W (M + {#a#})" ..
then show "?W N" by (simp only: N)
next
fix K
@@ -487,23 +487,23 @@
from wf have "\<forall>M \<triangleright> ?W. ?W (M + {#a#})"
proof induct
fix a
- assume "!!b. r b a ==> \<forall>M \<triangleright> ?W. ?W (M + {#b#})"
+ assume r: "!!b. r b a ==> \<forall>M \<triangleright> ?W. ?W (M + {#b#})"
show "\<forall>M \<triangleright> ?W. ?W (M + {#a#})"
proof
fix M assume "?W M"
then show "?W (M + {#a#})"
- by (rule acc_induct) (rule tedious_reasoning)
+ by (rule acc_induct) (rule tedious_reasoning [OF _ r])
qed
qed
- then show "?W (M + {#a#})" ..
+ from this and `?W M` show "?W (M + {#a#})" ..
qed
qed
theorem wf_mult1: "wfP r ==> wfP (mult1 r)"
- by (rule acc_wfI, rule all_accessible)
+ by (rule acc_wfI) (rule all_accessible)
theorem wf_mult: "wfP r ==> wfP (mult r)"
- by (unfold mult_def, rule wfP_trancl, rule wf_mult1)
+ unfolding mult_def by (rule wfP_trancl) (rule wf_mult1)
subsubsection {* Closure-free presentation *}
@@ -511,7 +511,7 @@
(*Badly needed: a linear arithmetic procedure for multisets*)
lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})"
-by (simp add: multiset_eq_conv_count_eq)
+ by (simp add: multiset_eq_conv_count_eq)
text {* One direction. *}
@@ -548,7 +548,7 @@
done
lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}"
-by (simp add: multiset_eq_conv_count_eq)
+ by (simp add: multiset_eq_conv_count_eq)
lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}"
apply (erule size_eq_Suc_imp_elem [THEN exE])
@@ -588,8 +588,7 @@
lemma one_step_implies_mult:
"J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. r k j
==> mult r (I + K) (I + J)"
- apply (insert one_step_implies_mult_aux, blast)
- done
+ using one_step_implies_mult_aux by blast
subsubsection {* Partial-order properties *}
@@ -609,9 +608,7 @@
lemma mult_irrefl_aux:
"finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}"
- apply (induct rule: finite_induct)
- apply (auto intro: order_less_trans)
- done
+ by (induct rule: finite_induct) (auto intro: order_less_trans)
lemma mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
apply (unfold less_multiset_def, auto)
@@ -621,15 +618,13 @@
done
lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
-by (insert mult_less_not_refl, fast)
+ using insert mult_less_not_refl by fast
text {* Transitivity. *}
theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)"
- apply (unfold less_multiset_def mult_def)
- apply (blast intro: trancl_trans')
- done
+ unfolding less_multiset_def mult_def by (blast intro: trancl_trans')
text {* Asymmetry. *}
--- a/src/HOL/Library/Quotient.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/Quotient.thy Wed Jun 13 18:30:11 2007 +0200
@@ -31,27 +31,27 @@
lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
proof -
- assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)"
+ assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)"
by (rule contrapos_nn) (rule equiv_sym)
qed
lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
proof -
- assume "\<not> (x \<sim> y)" and yz: "y \<sim> z"
+ assume "\<not> (x \<sim> y)" and "y \<sim> z"
show "\<not> (x \<sim> z)"
proof
assume "x \<sim> z"
- also from yz have "z \<sim> y" ..
+ also from `y \<sim> z` have "z \<sim> y" ..
finally have "x \<sim> y" .
- thus False by contradiction
+ with `\<not> (x \<sim> y)` show False by contradiction
qed
qed
lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
proof -
- assume "\<not> (y \<sim> z)" hence "\<not> (z \<sim> y)" ..
- also assume "x \<sim> y" hence "y \<sim> x" ..
- finally have "\<not> (z \<sim> x)" . thus "(\<not> x \<sim> z)" ..
+ assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
+ also assume "x \<sim> y" then have "y \<sim> x" ..
+ finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" ..
qed
text {*
@@ -80,9 +80,9 @@
theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
proof (cases A)
fix R assume R: "A = Abs_quot R"
- assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
+ assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
- thus ?thesis unfolding class_def .
+ then show ?thesis unfolding class_def .
qed
lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
@@ -105,8 +105,8 @@
by (simp only: class_def Abs_quot_inject quotI)
moreover have "a \<sim> a" ..
ultimately have "a \<in> {x. b \<sim> x}" by blast
- hence "b \<sim> a" by blast
- thus ?thesis ..
+ then have "b \<sim> a" by blast
+ then show ?thesis ..
qed
next
assume ab: "a \<sim> b"
@@ -125,7 +125,7 @@
finally show "a \<sim> x" .
qed
qed
- thus ?thesis by (simp only: class_def)
+ then show ?thesis by (simp only: class_def)
qed
qed
@@ -142,15 +142,15 @@
proof (rule someI2)
show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
- hence "a \<sim> x" .. thus "x \<sim> a" ..
+ then have "a \<sim> x" .. then show "x \<sim> a" ..
qed
qed
theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
proof (cases A)
fix a assume a: "A = \<lfloor>a\<rfloor>"
- hence "pick A \<sim> a" by (simp only: pick_equiv)
- hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
+ then have "pick A \<sim> a" by (simp only: pick_equiv)
+ then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
with a show ?thesis by simp
qed
@@ -175,7 +175,7 @@
moreover
show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
moreover
- show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" .
+ show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P)
ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
qed
finally show ?thesis .
--- a/src/HOL/Library/SCT_Misc.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/SCT_Misc.thy Wed Jun 13 18:30:11 2007 +0200
@@ -3,9 +3,9 @@
Author: Alexander Krauss, TU Muenchen
*)
-header ""
+header "" (* FIXME proper header *)
-theory SCT_Misc
+theory SCT_Misc (* FIXME proper name *)
imports Main
begin
@@ -95,11 +95,13 @@
"section_of s n = (LEAST i. n < s (Suc i))"
lemma section_help:
- assumes [intro, simp]: "increasing s"
+ assumes "increasing s"
shows "\<exists>i. n < s (Suc i)"
proof -
- from increasing_inc have "n \<le> s n" .
- also from increasing_strict have "\<dots> < s (Suc n)" by simp
+ have "n \<le> s n"
+ using `increasing s` by (rule increasing_inc)
+ also have "\<dots> < s (Suc n)"
+ using `increasing s` increasing_strict by simp
finally show ?thesis ..
qed
@@ -107,7 +109,7 @@
assumes "increasing s"
shows "n < s (Suc (section_of s n))"
unfolding section_of_def
- by (rule LeastI_ex) (rule section_help)
+ by (rule LeastI_ex) (rule section_help [OF `increasing s`])
lemma section_of1:
assumes [simp, intro]: "increasing s"
--- a/src/HOL/Library/SCT_Theorem.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/SCT_Theorem.thy Wed Jun 13 18:30:11 2007 +0200
@@ -3,7 +3,7 @@
Author: Alexander Krauss, TU Muenchen
*)
-header ""
+header "" (* FIXME proper header *)
theory SCT_Theorem
imports Main Ramsey SCT_Misc SCT_Definition
@@ -795,10 +795,9 @@
unfolding is_desc_fthread_def
by auto
- have "i < s (Suc ?k)" by (rule section_of2)
- also have "\<dots> \<le> s j"
- by (rule increasing_weak[of s], assumption)
- (insert `?k < j`, arith)
+ have "i < s (Suc ?k)" by (rule section_of2) simp
+ also have "\<dots> \<le> s j"
+ by (rule increasing_weak [of s], assumption) (insert `?k < j`, arith)
also note `\<dots> \<le> l`
finally have "i < l" .
with desc
@@ -925,10 +924,10 @@
{
fix x assume r: "x \<in> section s ?L"
- have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2)
+ have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2) simp
note `s (Suc ?K) < j`
also have "j < s (Suc ?L)"
- by (rule section_of2)
+ by (rule section_of2) simp
finally have "Suc ?K \<le> ?L"
by (simp add:increasing_bij)
with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp
@@ -1074,12 +1073,12 @@
"set2list = inv set"
lemma finite_set2list:
- assumes [intro]: "finite S"
+ assumes "finite S"
shows "set (set2list S) = S"
unfolding set2list_def
proof (rule f_inv_f)
- from finite_list
- have "\<exists>l. set l = S" .
+ from `finite S` have "\<exists>l. set l = S"
+ by (rule finite_list)
thus "S \<in> range set"
unfolding image_def
by auto
@@ -1307,7 +1306,7 @@
by (simp only:split_conv, rule a, auto)
obtain n H m where
- G_struct: "G = (n, H, m)" by (cases G) simp
+ G_struct: "G = (n, H, m)" by (cases G)
let ?s = "enumerate S"
let ?q = "contract ?s p"
@@ -1381,7 +1380,7 @@
proof -
from fin obtain P where b: "bounded_acg P A"
unfolding finite_acg_def ..
- show ?thesis using LJA_Theorem4[OF b]
+ show ?thesis using LJA_Theorem4[OF b] and `SCT' A`
by simp
qed
--- a/src/HOL/Matrix/MatrixGeneral.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy Wed Jun 13 18:30:11 2007 +0200
@@ -85,7 +85,8 @@
next
fix y
assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0"
- 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)
+ 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 add: hyp)
qed
then have "finite (?swap`?A)"
proof -
--- a/src/HOL/NumberTheory/Euler.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/NumberTheory/Euler.thy Wed Jun 13 18:30:11 2007 +0200
@@ -264,7 +264,7 @@
by (auto simp add: zEven_def zOdd_def)
then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
by (auto simp add: even_div_2_prop2)
- then have "1 < (p - 1)"
+ with `2 < p` have "1 < (p - 1)"
by auto
then have " 1 < (2 * ((p - 1) div 2))"
by (auto simp add: aux_1)
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Jun 13 18:30:11 2007 +0200
@@ -115,8 +115,8 @@
(-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
proof -
assume "a \<in> zOdd"
- from QRLemma4 have
- "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)"..
+ from QRLemma4 [OF this] have
+ "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
moreover have "0 \<le> int(card E)"
by auto
moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
--- a/src/HOL/W0/W0.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/W0/W0.thy Wed Jun 13 18:30:11 2007 +0200
@@ -405,7 +405,7 @@
then have "map ($ s) a |- Var n :: map ($ s) a ! n"
by (rule has_type.Var)
also have "map ($ s) a ! n = $ s (a ! n)"
- by (rule nth_map)
+ by (rule nth_map) (rule Var)
also have "map ($ s) a = $ s a"
by (simp only: app_subst_list)
finally show ?case .
--- a/src/HOL/ex/Commutative_Ring_Complete.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/Commutative_Ring_Complete.thy Wed Jun 13 18:30:11 2007 +0200
@@ -150,7 +150,7 @@
then obtain d where X:"x=Suc (Suc d)" ..
from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
- with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp
+ with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption
with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
ultimately show ?case by blast
next
@@ -168,7 +168,7 @@
then obtain d where X:"x=Suc (Suc d)" ..
from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
- with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp
+ with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption
with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
ultimately show ?case by blast
next
--- a/src/HOL/ex/Higher_Order_Logic.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy Wed Jun 13 18:30:11 2007 +0200
@@ -58,7 +58,7 @@
theorem sym [sym]: "x = y \<Longrightarrow> y = x"
proof -
assume "x = y"
- thus "y = x" by (rule subst) (rule refl)
+ then show "y = x" by (rule subst) (rule refl)
qed
lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
@@ -110,7 +110,7 @@
theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
proof (unfold false_def)
assume "\<forall>A. A"
- thus A ..
+ then show A ..
qed
theorem trueI [intro]: \<top>
@@ -121,7 +121,7 @@
theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
proof (unfold not_def)
assume "A \<Longrightarrow> \<bottom>"
- thus "A \<longrightarrow> \<bottom>" ..
+ then show "A \<longrightarrow> \<bottom>" ..
qed
theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
@@ -129,7 +129,7 @@
assume "A \<longrightarrow> \<bottom>"
also assume A
finally have \<bottom> ..
- thus B ..
+ then show B ..
qed
lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
@@ -145,8 +145,8 @@
fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
proof
assume "A \<longrightarrow> B \<longrightarrow> C"
- also have A .
- also have B .
+ also note `A`
+ also note `B`
finally show C .
qed
qed
@@ -161,7 +161,7 @@
also have "A \<longrightarrow> B \<longrightarrow> A"
proof
assume A
- thus "B \<longrightarrow> A" ..
+ then show "B \<longrightarrow> A" ..
qed
finally have A .
} moreover {
@@ -182,9 +182,9 @@
fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
proof
assume "A \<longrightarrow> C"
- also have A .
+ also note `A`
finally have C .
- thus "(B \<longrightarrow> C) \<longrightarrow> C" ..
+ then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
qed
qed
qed
@@ -199,7 +199,7 @@
show "(B \<longrightarrow> C) \<longrightarrow> C"
proof
assume "B \<longrightarrow> C"
- also have B .
+ also note `B`
finally show C .
qed
qed
@@ -213,11 +213,11 @@
from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
also have "A \<longrightarrow> C"
proof
- assume A thus C by (rule r1)
+ assume A then show C by (rule r1)
qed
also have "B \<longrightarrow> C"
proof
- assume B thus C by (rule r2)
+ assume B then show C by (rule r2)
qed
finally show C .
qed
@@ -230,8 +230,8 @@
fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
proof
assume "\<forall>x. P x \<longrightarrow> C"
- hence "P a \<longrightarrow> C" ..
- also have "P a" .
+ then have "P a \<longrightarrow> C" ..
+ also note `P a`
finally show C .
qed
qed
@@ -247,7 +247,7 @@
fix x show "P x \<longrightarrow> C"
proof
assume "P x"
- thus C by (rule r)
+ then show C by (rule r)
qed
qed
finally show C .
@@ -269,7 +269,7 @@
have "A \<longrightarrow> B"
proof
assume A
- thus B by (rule contradiction)
+ with `\<not> A` show B by (rule contradiction)
qed
with a show A ..
qed
@@ -282,7 +282,7 @@
show A
proof (rule classical)
assume "\<not> A"
- thus ?thesis by (rule contradiction)
+ with `\<not> \<not> A` show ?thesis by (rule contradiction)
qed
qed
@@ -294,11 +294,11 @@
assume "\<not> (A \<or> \<not> A)"
have "\<not> A"
proof
- assume A hence "A \<or> \<not> A" ..
- thus \<bottom> by (rule contradiction)
+ assume A then have "A \<or> \<not> A" ..
+ with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
qed
- hence "A \<or> \<not> A" ..
- thus \<bottom> by (rule contradiction)
+ then have "A \<or> \<not> A" ..
+ with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
qed
qed
@@ -309,10 +309,10 @@
from tertium_non_datur show C
proof
assume A
- thus ?thesis by (rule r1)
+ then show ?thesis by (rule r1)
next
assume "\<not> A"
- thus ?thesis by (rule r2)
+ then show ?thesis by (rule r2)
qed
qed
@@ -321,9 +321,9 @@
assume r: "\<not> A \<Longrightarrow> A"
show A
proof (rule classical_cases)
- assume A thus A .
+ assume A then show A .
next
- assume "\<not> A" thus A by (rule r)
+ assume "\<not> A" then show A by (rule r)
qed
qed
--- a/src/HOL/ex/PER.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/PER.thy Wed Jun 13 18:30:11 2007 +0200
@@ -242,7 +242,7 @@
proof (rule someI2)
show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
- then have "a \<sim> x" ..
+ from this and a have "a \<sim> x" ..
then show "x \<sim> a" ..
qed
qed
--- a/src/HOL/ex/ThreeDivides.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/ThreeDivides.thy Wed Jun 13 18:30:11 2007 +0200
@@ -77,7 +77,7 @@
let ?thr = "(3::nat)"
have "?thr dvd 9" by simp
moreover
- have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult)
+ have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult) (rule Suc)
hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)
ultimately
have"?thr dvd ((10^(n+1) - 10) + 9)"
--- a/src/HOL/ex/Unification.thy Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/Unification.thy Wed Jun 13 18:30:11 2007 +0200
@@ -461,7 +461,7 @@
by (rule acc_downward) (rule unify_rel.intros)
hence no_new_vars:
"\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
- by (rule unify_vars)
+ by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
from ih2 show ?case
proof