--- a/src/HOL/IMP/Hoare.thy Sun May 26 22:57:48 2013 +0200
+++ b/src/HOL/IMP/Hoare.thy Mon May 27 07:44:10 2013 +0200
@@ -8,6 +8,10 @@
type_synonym assn = "state \<Rightarrow> bool"
+definition
+hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
+"\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)"
+
abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy Sun May 26 22:57:48 2013 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy Mon May 27 07:44:10 2013 +0200
@@ -4,10 +4,6 @@
subsection "Soundness"
-definition
-hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
-"\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)"
-
lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}"
proof(induction rule: hoare.induct)
case (While P b c)