(* Title: HOL/Hoare/Hoare_Logic.thy Author: Leonor Prensa Nieto & Tobias Nipkow Copyright 1998 TUM Author: Walter Guttmann (extension to total-correctness proofs)
*)
section \<open>Hoare logic\<close>
theory Hoare_Logic imports Hoare_Syntax Hoare_Tac begin
subsection \<open>Sugared semantic embedding of Hoare logic\<close>
text\<open>
Strictly speaking a shallow embedding (as implemented by Norbert Galm
following Mike Gordon) would suffice. Maybe the datatype com comes in useful
later. \<close>
abbreviation annskip (\<open>SKIP\<close>) where "SKIP == Basic id"
type_synonym'a sem = "'a => 'a => bool"
inductive Sem :: "'a com \ 'a sem" where "Sem (Basic f) s (f s)"
| "Sem c1 s s'' \ Sem c2 s'' s' \ Sem (Seq c1 c2) s s'"
| "s \ b \ Sem c1 s s' \ Sem (Cond b c1 c2) s s'"
| "s \ b \ Sem c2 s s' \ Sem (Cond b c1 c2) s s'"
| "s \ b \ Sem (While b c) s s"
| "s \ b \ Sem c s s'' \ Sem (While b c) s'' s' \
Sem (While b c) s s'"
definition Valid :: "'a bexp \ 'a com \ 'a anno \ 'a bexp \ bool" where"Valid p c a q \ \s s'. Sem c s s' \ s \ p \ s' \ q"
definition ValidTC :: "'a bexp \ 'a com \ 'a anno \ 'a bexp \ bool" where"ValidTC p c a q \ \s. s \ p \ (\t. Sem c s t \ t \ q)"
inductive_cases [elim!]: "Sem (Basic f) s s'""Sem (Seq c1 c2) s s'" "Sem (Cond b c1 c2) s s'"
lemma Sem_deterministic: assumes"Sem c s s1" and"Sem c s s2" shows"s1 = s2" proof - have"Sem c s s1 \ (\s2. Sem c s s2 \ s1 = s2)" by (induct rule: Sem.induct) (subst Sem.simps, blast)+ thus ?thesis using assms by simp qed
lemma tc_implies_pc: "ValidTC p c a q \ Valid p c a q" by (metis Sem_deterministic Valid_def ValidTC_def)
lemma tc_extract_function: "ValidTC p c a q \ \f . \s . s \ p \ f s \ q" by (metis ValidTC_def)
lemma SkipRule: "p \ q \ Valid p (Basic id) a q" by (auto simp:Valid_def)
lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) a q" by (auto simp:Valid_def)
lemma SeqRule: "Valid P c1 a1 Q \ Valid Q c2 a2 R \ Valid P (Seq c1 c2) (Aseq a1 a2) R" by (auto simp:Valid_def)
lemma CondRule: "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} \<Longrightarrow> Valid w c1 a1 q \<Longrightarrow> Valid w' c2 a2 q \<Longrightarrow> Valid p (Cond b c1 c2) (Acond a1 a2) q" by (auto simp:Valid_def)
lemma While_aux: assumes"Sem (While b c) s s'" shows"\s s'. Sem c s s' \ s \ I \ s \ b \ s' \ I \
s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b" using assms by (induct "While b c" s s') auto
lemma WhileRule: "p \ i \ Valid (i \ b) c (A 0) i \ i \ (-b) \ q \ Valid p (While b c) (Awhile i v A) q" apply (clarsimp simp:Valid_def) apply(drule While_aux) apply assumption apply blast apply blast done
lemma SkipRuleTC: assumes"p \ q" shows"ValidTC p (Basic id) a q" by (metis assms Sem.intros(1) ValidTC_def id_apply subsetD)
lemma BasicRuleTC: assumes"p \ {s. f s \ q}" shows"ValidTC p (Basic f) a q" by (metis assms Ball_Collect Sem.intros(1) ValidTC_def)
lemma SeqRuleTC: assumes"ValidTC p c1 a1 q" and"ValidTC q c2 a2 r" shows"ValidTC p (Seq c1 c2) (Aseq a1 a2) r" by (meson assms Sem.intros(2) ValidTC_def)
lemma CondRuleTC: assumes"p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')}" and"ValidTC w c1 a1 q" and"ValidTC w' c2 a2 q" shows"ValidTC p (Cond b c1 c2) (Acond a1 a2) q" proof (unfold ValidTC_def, rule allI) fix s show"s \ p \ (\t . Sem (Cond b c1 c2) s t \ t \ q)" apply (cases "s \ b") apply (metis (mono_tags, lifting) assms(1,2) Ball_Collect Sem.intros(3) ValidTC_def) by (metis (mono_tags, lifting) assms(1,3) Ball_Collect Sem.intros(4) ValidTC_def) qed
lemma WhileRuleTC: assumes"p \ i" and"\n::nat . ValidTC (i \ b \ {s . v s = n}) c (A n) (i \ {s . v s < n})" and"i \ uminus b \ q" shows"ValidTC p (While b c) (Awhile i v (\n. A n)) q" proof - have"s \ i \ v s = n \ (\t . Sem (While b c) s t \ t \ q)" for s n proof (induction"n" arbitrary: s rule: less_induct) fix n :: nat fix s :: 'a assume 1: "\(m::nat) s::'a . m < n \ s \ i \ v s = m \ (\t . Sem (While b c) s t \ t \q)" show"s \ i \ v s = n \ (\t . Sem (While b c) s t \ t \ q)" proof (rule impI, cases "s \ b") assume 2: "s \ b" and "s \ i \ v s = n" hence"s \ i \ b \ {s . v s = n}" using assms(1) by auto hence"\t . Sem c s t \ t \ i \ {s . v s < n}" by (metis assms(2) ValidTC_def) from this obtain t where 3: "Sem c s t \ t \ i \ {s . v s < n}" by auto hence"\u . Sem (While b c) t u \ u \ q" using 1 by auto thus"\t . Sem (While b c) s t \ t \ q" using 2 3 Sem.intros(6) by force next assume"s \ b" and "s \ i \ v s = n" thus"\t . Sem (While b c) s t \ t \ q" using Sem.intros(5) assms(3) by fastforce qed qed thus ?thesis using assms(1) ValidTC_def by force qed
declare BasicRule [Hoare_Tac.BasicRule] and SkipRule [Hoare_Tac.SkipRule] and SeqRule [Hoare_Tac.SeqRule] and CondRule [Hoare_Tac.CondRule] and WhileRule [Hoare_Tac.WhileRule]
declare BasicRuleTC [Hoare_Tac.BasicRuleTC] and SkipRuleTC [Hoare_Tac.SkipRuleTC] and SeqRuleTC [Hoare_Tac.SeqRuleTC] and CondRuleTC [Hoare_Tac.CondRuleTC] and WhileRuleTC [Hoare_Tac.WhileRuleTC]
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
