--- a/src/HOL/IMP/Comp_Rev.thy Fri Oct 21 08:24:57 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy Fri Oct 21 08:25:04 2011 +0200
@@ -39,7 +39,7 @@
lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
-lemma exec_Suc [trans]:
+lemma exec_Suc:
"\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''"
by (fastforce simp del: split_paired_Ex)
@@ -350,7 +350,7 @@
from step `isize P \<le> i`
have "P' \<turnstile> (i - isize P, s, stk) \<rightarrow> (i' - isize P, s'', stk'')"
by (rule exec1_drop_left)
- also
+ moreover
then have "i' - isize P \<in> succs P' 0"
by (fastforce dest!: succs_iexec1)
with `exits P' \<subseteq> {0..}`
@@ -358,8 +358,8 @@
from rest this `exits P' \<subseteq> {0..}`
have "P' \<turnstile> (i' - isize P, s'', stk'') \<rightarrow>^k (n - isize P, s', stk')"
by (rule Suc.IH)
- finally
- show ?case .
+ ultimately
+ show ?case by auto
qed
lemmas exec_n_drop_Cons =
--- a/src/HOL/IMP/Sem_Equiv.thy Fri Oct 21 08:24:57 2011 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy Fri Oct 21 08:25:04 2011 +0200
@@ -43,7 +43,7 @@
"(P \<Turnstile> c \<sim> c') = (P \<Turnstile> c' \<sim> c)"
by (auto simp: equiv_up_to_def)
-lemma equiv_up_to_trans [trans]:
+lemma equiv_up_to_trans:
"P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> c' \<sim> c'' \<Longrightarrow> P \<Turnstile> c \<sim> c''"
by (auto simp: equiv_up_to_def)
@@ -56,7 +56,7 @@
"(P \<Turnstile> b <\<sim>> b') = (P \<Turnstile> b' <\<sim>> b)"
by (auto simp: bequiv_up_to_def)
-lemma bequiv_up_to_trans [trans]:
+lemma bequiv_up_to_trans:
"P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
by (auto simp: bequiv_up_to_def)
--- a/src/HOL/IMP/Small_Step.thy Fri Oct 21 08:24:57 2011 +0200
+++ b/src/HOL/IMP/Small_Step.thy Fri Oct 21 08:25:04 2011 +0200
@@ -46,16 +46,6 @@
declare small_step.intros[simp,intro]
-text{* So-called transitivity rules. See below. *}
-
-declare step[trans] step1[trans]
-
-lemma step2[trans]:
- "cs \<rightarrow> cs' \<Longrightarrow> cs' \<rightarrow> cs'' \<Longrightarrow> cs \<rightarrow>* cs''"
-by(metis refl step)
-
-declare star_trans[trans]
-
text{* Rule inversion: *}
inductive_cases SkipE[elim!]: "(SKIP,s) \<rightarrow> ct"
@@ -92,9 +82,7 @@
by(blast intro: star.step star_semi2 star_trans)
text{* The following proof corresponds to one on the board where one would
-show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. This is what the
-also/finally proof steps do: they compose chains, implicitly using the rules
-declared with attribute [trans] above. *}
+show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. *}
lemma big_to_small:
"cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
@@ -110,21 +98,23 @@
fix s::state and b c0 c1 t
assume "bval b s"
hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c0,s)" by simp
- also assume "(c0,s) \<rightarrow>* (SKIP,t)"
- finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" . --"= by assumption"
+ moreover assume "(c0,s) \<rightarrow>* (SKIP,t)"
+ ultimately
+ show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
next
fix s::state and b c0 c1 t
assume "\<not>bval b s"
hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c1,s)" by simp
- also assume "(c1,s) \<rightarrow>* (SKIP,t)"
- finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" .
+ moreover assume "(c1,s) \<rightarrow>* (SKIP,t)"
+ ultimately
+ show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
next
fix b c and s::state
assume b: "\<not>bval b s"
let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP"
have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast
- also have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
- finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by auto
+ moreover have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
+ ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by (metis refl step)
next
fix b c s s' t
let ?w = "WHILE b DO c"
@@ -133,9 +123,9 @@
assume c: "(c,s) \<rightarrow>* (SKIP,s')"
assume b: "bval b s"
have "(?w,s) \<rightarrow> (?if, s)" by blast
- also have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
- also have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w])
- finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by auto
+ moreover have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
+ moreover have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w])
+ ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
qed
text{* Each case of the induction can be proved automatically: *}
--- a/src/HOL/Int.thy Fri Oct 21 08:24:57 2011 +0200
+++ b/src/HOL/Int.thy Fri Oct 21 08:25:04 2011 +0200
@@ -1543,7 +1543,7 @@
lemmas int_arith_rules =
neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
minus_zero diff_minus left_minus right_minus
- mult_zero_left mult_zero_right mult_Bit1 mult_1_left mult_1_right
+ mult_zero_left mult_zero_right mult_1_left mult_1_right
mult_minus_left mult_minus_right
minus_add_distrib minus_minus mult_assoc
of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
--- a/src/HOL/Orderings.thy Fri Oct 21 08:24:57 2011 +0200
+++ b/src/HOL/Orderings.thy Fri Oct 21 08:25:04 2011 +0200
@@ -883,7 +883,7 @@
text {* These support proving chains of decreasing inequalities
a >= b >= c ... in Isar proofs. *}
-lemma xt1:
+lemma xt1 [no_atp]:
"a = b ==> b > c ==> a > c"
"a > b ==> b = c ==> a > c"
"a = b ==> b >= c ==> a >= c"
@@ -902,39 +902,39 @@
"a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c"
by auto
-lemma xt2:
+lemma xt2 [no_atp]:
"(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
by (subgoal_tac "f b >= f c", force, force)
-lemma xt3: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==>
+lemma xt3 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==>
(!!x y. x >= y ==> f x >= f y) ==> f a >= c"
by (subgoal_tac "f a >= f b", force, force)
-lemma xt4: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
+lemma xt4 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
(!!x y. x >= y ==> f x >= f y) ==> a > f c"
by (subgoal_tac "f b >= f c", force, force)
-lemma xt5: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
+lemma xt5 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
(!!x y. x > y ==> f x > f y) ==> f a > c"
by (subgoal_tac "f a > f b", force, force)
-lemma xt6: "(a::'a::order) >= f b ==> b > c ==>
+lemma xt6 [no_atp]: "(a::'a::order) >= f b ==> b > c ==>
(!!x y. x > y ==> f x > f y) ==> a > f c"
by (subgoal_tac "f b > f c", force, force)
-lemma xt7: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
+lemma xt7 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
(!!x y. x >= y ==> f x >= f y) ==> f a > c"
by (subgoal_tac "f a >= f b", force, force)
-lemma xt8: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
+lemma xt8 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
(!!x y. x > y ==> f x > f y) ==> a > f c"
by (subgoal_tac "f b > f c", force, force)
-lemma xt9: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
+lemma xt9 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
(!!x y. x > y ==> f x > f y) ==> f a > c"
by (subgoal_tac "f a > f b", force, force)
-lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9
+lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 [no_atp]
(*
Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands