removed [trans] concept from basic material
authorkleing
Thu Oct 20 12:30:43 2011 -0400 (2011-10-20)
changeset 45218f115540543d8
parent 45217 c4fab1099cd0
child 45220 1c9f10955ec1
removed [trans] concept from basic material
src/HOL/IMP/Comp_Rev.thy
src/HOL/IMP/Sem_Equiv.thy
src/HOL/IMP/Small_Step.thy
     1.1 --- a/src/HOL/IMP/Comp_Rev.thy	Thu Oct 20 10:44:00 2011 +0200
     1.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Thu Oct 20 12:30:43 2011 -0400
     1.3 @@ -39,7 +39,7 @@
     1.4  
     1.5  lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
     1.6  
     1.7 -lemma exec_Suc [trans]:
     1.8 +lemma exec_Suc:
     1.9    "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''" 
    1.10    by (fastforce simp del: split_paired_Ex)
    1.11  
    1.12 @@ -350,7 +350,7 @@
    1.13    from step `isize P \<le> i`
    1.14    have "P' \<turnstile> (i - isize P, s, stk) \<rightarrow> (i' - isize P, s'', stk'')" 
    1.15      by (rule exec1_drop_left)
    1.16 -  also
    1.17 +  moreover
    1.18    then have "i' - isize P \<in> succs P' 0"
    1.19      by (fastforce dest!: succs_iexec1)
    1.20    with `exits P' \<subseteq> {0..}`
    1.21 @@ -358,8 +358,8 @@
    1.22    from rest this `exits P' \<subseteq> {0..}`     
    1.23    have "P' \<turnstile> (i' - isize P, s'', stk'') \<rightarrow>^k (n - isize P, s', stk')"
    1.24      by (rule Suc.IH)
    1.25 -  finally
    1.26 -  show ?case .
    1.27 +  ultimately
    1.28 +  show ?case by auto
    1.29  qed
    1.30  
    1.31  lemmas exec_n_drop_Cons = 
     2.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Thu Oct 20 10:44:00 2011 +0200
     2.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Thu Oct 20 12:30:43 2011 -0400
     2.3 @@ -43,7 +43,7 @@
     2.4    "(P \<Turnstile> c \<sim> c') = (P \<Turnstile> c' \<sim> c)"
     2.5    by (auto simp: equiv_up_to_def)
     2.6  
     2.7 -lemma equiv_up_to_trans [trans]:
     2.8 +lemma equiv_up_to_trans:
     2.9    "P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> c' \<sim> c'' \<Longrightarrow> P \<Turnstile> c \<sim> c''"
    2.10    by (auto simp: equiv_up_to_def)
    2.11  
    2.12 @@ -56,7 +56,7 @@
    2.13    "(P \<Turnstile> b <\<sim>> b') = (P \<Turnstile> b' <\<sim>> b)"
    2.14    by (auto simp: bequiv_up_to_def)
    2.15  
    2.16 -lemma bequiv_up_to_trans [trans]:
    2.17 +lemma bequiv_up_to_trans:
    2.18    "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
    2.19    by (auto simp: bequiv_up_to_def)
    2.20  
     3.1 --- a/src/HOL/IMP/Small_Step.thy	Thu Oct 20 10:44:00 2011 +0200
     3.2 +++ b/src/HOL/IMP/Small_Step.thy	Thu Oct 20 12:30:43 2011 -0400
     3.3 @@ -46,16 +46,6 @@
     3.4  
     3.5  declare small_step.intros[simp,intro]
     3.6  
     3.7 -text{* So-called transitivity rules. See below. *}
     3.8 -
     3.9 -declare step[trans] step1[trans]
    3.10 -
    3.11 -lemma step2[trans]:
    3.12 -  "cs \<rightarrow> cs' \<Longrightarrow> cs' \<rightarrow> cs'' \<Longrightarrow> cs \<rightarrow>* cs''"
    3.13 -by(metis refl step)
    3.14 -
    3.15 -declare star_trans[trans]
    3.16 -
    3.17  text{* Rule inversion: *}
    3.18  
    3.19  inductive_cases SkipE[elim!]: "(SKIP,s) \<rightarrow> ct"
    3.20 @@ -92,9 +82,7 @@
    3.21  by(blast intro: star.step star_semi2 star_trans)
    3.22  
    3.23  text{* The following proof corresponds to one on the board where one would
    3.24 -show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. This is what the
    3.25 -also/finally proof steps do: they compose chains, implicitly using the rules
    3.26 -declared with attribute [trans] above. *}
    3.27 +show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. *}
    3.28  
    3.29  lemma big_to_small:
    3.30    "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
    3.31 @@ -110,21 +98,23 @@
    3.32    fix s::state and b c0 c1 t
    3.33    assume "bval b s"
    3.34    hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c0,s)" by simp
    3.35 -  also assume "(c0,s) \<rightarrow>* (SKIP,t)"
    3.36 -  finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" . --"= by assumption"
    3.37 +  moreover assume "(c0,s) \<rightarrow>* (SKIP,t)"
    3.38 +  ultimately 
    3.39 +  show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
    3.40  next
    3.41    fix s::state and b c0 c1 t
    3.42    assume "\<not>bval b s"
    3.43    hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c1,s)" by simp
    3.44 -  also assume "(c1,s) \<rightarrow>* (SKIP,t)"
    3.45 -  finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" .
    3.46 +  moreover assume "(c1,s) \<rightarrow>* (SKIP,t)"
    3.47 +  ultimately 
    3.48 +  show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
    3.49  next
    3.50    fix b c and s::state
    3.51    assume b: "\<not>bval b s"
    3.52    let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP"
    3.53    have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast
    3.54 -  also have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
    3.55 -  finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by auto
    3.56 +  moreover have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
    3.57 +  ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by (metis refl step)
    3.58  next
    3.59    fix b c s s' t
    3.60    let ?w  = "WHILE b DO c"
    3.61 @@ -133,9 +123,9 @@
    3.62    assume c: "(c,s) \<rightarrow>* (SKIP,s')"
    3.63    assume b: "bval b s"
    3.64    have "(?w,s) \<rightarrow> (?if, s)" by blast
    3.65 -  also have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
    3.66 -  also have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w])
    3.67 -  finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by auto
    3.68 +  moreover have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
    3.69 +  moreover have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w])
    3.70 +  ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
    3.71  qed
    3.72  
    3.73  text{* Each case of the induction can be proved automatically: *}