tuned proofs;
authorwenzelm
Tue Mar 29 22:36:56 2011 +0200 (2011-03-29)
changeset 42154478bdcea240a
parent 42153 fa108629d132
child 42155 ffe99b07c9c0
tuned proofs;
src/HOL/Hoare/Examples.thy
src/HOL/Hoare/ExamplesAbort.thy
src/HOL/Hoare/SchorrWaite.thy
     1.1 --- a/src/HOL/Hoare/Examples.thy	Tue Mar 29 21:48:01 2011 +0200
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Tue Mar 29 22:36:56 2011 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4   {c = A^B}"
     1.5  apply vcg_simp
     1.6  apply(case_tac "b")
     1.7 - apply(simp add: mod_less)
     1.8 + apply simp
     1.9  apply simp
    1.10  done
    1.11  
     2.1 --- a/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 29 21:48:01 2011 +0200
     2.2 +++ b/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 29 22:36:56 2011 +0200
     2.3 @@ -14,8 +14,7 @@
     2.4  lemma
     2.5   "VARS a i j
     2.6   {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
     2.7 -apply vcg_simp
     2.8 -done
     2.9 +by vcg_simp
    2.10  
    2.11  lemma "VARS (a::int list) i
    2.12   {True}
    2.13 @@ -24,7 +23,6 @@
    2.14   INV {i <= length a}
    2.15   DO a[i] := 7; i := i+1 OD
    2.16   {True}"
    2.17 -apply vcg_simp
    2.18 -done
    2.19 +by vcg_simp
    2.20  
    2.21  end
     3.1 --- a/src/HOL/Hoare/SchorrWaite.thy	Tue Mar 29 21:48:01 2011 +0200
     3.2 +++ b/src/HOL/Hoare/SchorrWaite.thy	Tue Mar 29 22:36:56 2011 +0200
     3.3 @@ -40,7 +40,7 @@
     3.4  done
     3.5  
     3.6  lemma still_reachable: "\<lbrakk>B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Rb\<^sup>* `` B \<subseteq> Ra\<^sup>* `` A "
     3.7 -apply (clarsimp simp only:Image_iff intro:subsetI)
     3.8 +apply (clarsimp simp only:Image_iff)
     3.9  apply (erule rtrancl_induct)
    3.10   apply blast
    3.11  apply (subgoal_tac "(y, z) \<in> Ra\<union>(Rb-Ra)")