--- a/src/HOL/IMP/Hoare.thy Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(* Title: HOL/IMP/Hoare.thy
- Author: Tobias Nipkow
-*)
-
-header "Inductive Definition of Hoare Logic"
-
-theory Hoare imports Natural begin
-
-type_synonym assn = "state => bool"
-
-inductive
- hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
-where
- skip: "|- {P}\<SKIP>{P}"
-| ass: "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
-| semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
-| If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
- |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
-| While: "|- {%s. P s & b s} c {P} ==>
- |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
-| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
- |- {P'}c{Q'}"
-
-lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
-by (blast intro: conseq)
-
-lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
-by (blast intro: conseq)
-
-lemma While':
-assumes "|- {%s. P s & b s} c {P}" and "ALL s. P s & \<not> b s \<longrightarrow> Q s"
-shows "|- {P} \<WHILE> b \<DO> c {Q}"
-by(rule weaken_post[OF While[OF assms(1)] assms(2)])
-
-
-lemmas [simp] = skip ass semi If
-
-lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
-
-end