# HG changeset patch
# User kleing
# Date 1319128243 14400
# Node ID f115540543d81ffeccfaea41826098197c22aed7
# Parent  c4fab1099cd0b10ef8426436c93cd5bfad4205d0
removed [trans] concept from basic material

diff -r c4fab1099cd0 -r f115540543d8 src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Thu Oct 20 10:44:00 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy	Thu Oct 20 12:30:43 2011 -0400
@@ -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 = 
diff -r c4fab1099cd0 -r f115540543d8 src/HOL/IMP/Sem_Equiv.thy
--- a/src/HOL/IMP/Sem_Equiv.thy	Thu Oct 20 10:44:00 2011 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy	Thu Oct 20 12:30:43 2011 -0400
@@ -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)
 
diff -r c4fab1099cd0 -r f115540543d8 src/HOL/IMP/Small_Step.thy
--- a/src/HOL/IMP/Small_Step.thy	Thu Oct 20 10:44:00 2011 +0200
+++ b/src/HOL/IMP/Small_Step.thy	Thu Oct 20 12:30:43 2011 -0400
@@ -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: *}