# Theory OG_Hoare

theory OG_Hoare
imports OG_Tran
```section ‹The Proof System›

theory OG_Hoare imports OG_Tran begin

primrec assertions :: "'a ann_com ⇒ ('a assn) set" where
"assertions (AnnBasic r f) = {r}"
| "assertions (AnnSeq c1 c2) = assertions c1 ∪ assertions c2"
| "assertions (AnnCond1 r b c1 c2) = {r} ∪ assertions c1 ∪ assertions c2"
| "assertions (AnnCond2 r b c) = {r} ∪ assertions c"
| "assertions (AnnWhile r b i c) = {r, i} ∪ assertions c"
| "assertions (AnnAwait r b c) = {r}"

primrec atomics :: "'a ann_com ⇒ ('a assn × 'a com) set" where
"atomics (AnnBasic r f) = {(r, Basic f)}"
| "atomics (AnnSeq c1 c2) = atomics c1 ∪ atomics c2"
| "atomics (AnnCond1 r b c1 c2) = atomics c1 ∪ atomics c2"
| "atomics (AnnCond2 r b c) = atomics c"
| "atomics (AnnWhile r b i c) = atomics c"
| "atomics (AnnAwait r b c) = {(r ∩ b, c)}"

primrec com :: "'a ann_triple_op ⇒ 'a ann_com_op" where
"com (c, q) = c"

primrec post :: "'a ann_triple_op ⇒ 'a assn" where
"post (c, q) = q"

definition interfree_aux :: "('a ann_com_op × 'a assn × 'a ann_com_op) ⇒ bool" where
"interfree_aux ≡ λ(co, q, co'). co'= None ∨
(∀(r,a) ∈ atomics (the co'). ∥= (q ∩ r) a q ∧
(co = None ∨ (∀p ∈ assertions (the co). ∥= (p ∩ r) a p)))"

definition interfree :: "(('a ann_triple_op) list) ⇒ bool" where
"interfree Ts ≡ ∀i j. i < length Ts ∧ j < length Ts ∧ i ≠ j ⟶
interfree_aux (com (Ts!i), post (Ts!i), com (Ts!j)) "

inductive
oghoare :: "'a assn ⇒ 'a com ⇒ 'a assn ⇒ bool"  ("(3∥- _//_//_)" [90,55,90] 50)
and ann_hoare :: "'a ann_com ⇒ 'a assn ⇒ bool"  ("(2⊢ _// _)" [60,90] 45)
where
AnnBasic: "r ⊆ {s. f s ∈ q} ⟹ ⊢ (AnnBasic r f) q"

| AnnSeq:   "⟦ ⊢ c0 pre c1; ⊢ c1 q ⟧ ⟹ ⊢ (AnnSeq c0 c1) q"

| AnnCond1: "⟦ r ∩ b ⊆ pre c1; ⊢ c1 q; r ∩ -b ⊆ pre c2; ⊢ c2 q⟧
⟹ ⊢ (AnnCond1 r b c1 c2) q"
| AnnCond2: "⟦ r ∩ b ⊆ pre c; ⊢ c q; r ∩ -b ⊆ q ⟧ ⟹ ⊢ (AnnCond2 r b c) q"

| AnnWhile: "⟦ r ⊆ i; i ∩ b ⊆ pre c; ⊢ c i; i ∩ -b ⊆ q ⟧
⟹ ⊢ (AnnWhile r b i c) q"

| AnnAwait:  "⟦ atom_com c; ∥- (r ∩ b) c q ⟧ ⟹ ⊢ (AnnAwait r b c) q"

| AnnConseq: "⟦⊢ c q; q ⊆ q' ⟧ ⟹ ⊢ c q'"

| Parallel: "⟦ ∀i<length Ts. ∃c q. Ts!i = (Some c, q) ∧ ⊢ c q; interfree Ts ⟧
⟹ ∥- (⋂i∈{i. i<length Ts}. pre(the(com(Ts!i))))
Parallel Ts
(⋂i∈{i. i<length Ts}. post(Ts!i))"

| Basic:   "∥- {s. f s ∈q} (Basic f) q"

| Seq:    "⟦ ∥- p c1 r; ∥- r c2 q ⟧ ⟹ ∥- p (Seq c1 c2) q "

| Cond:   "⟦ ∥- (p ∩ b) c1 q; ∥- (p ∩ -b) c2 q ⟧ ⟹ ∥- p (Cond b c1 c2) q"

| While:  "⟦ ∥- (p ∩ b) c p ⟧ ⟹ ∥- p (While b i c) (p ∩ -b)"

| Conseq: "⟦ p' ⊆ p; ∥- p c q ; q ⊆ q' ⟧ ⟹ ∥- p' c q'"

section ‹Soundness›
(* In the version Isabelle-10-Sep-1999: HOL: The THEN and ELSE
parts of conditional expressions (if P then x else y) are no longer
simplified.  (This allows the simplifier to unfold recursive
functional programs.)  To restore the old behaviour, we declare
@{text "lemmas [cong del] = if_weak_cong"}. *)

lemmas [cong del] = if_weak_cong

lemmas ann_hoare_induct = oghoare_ann_hoare.induct [THEN conjunct2]
lemmas oghoare_induct = oghoare_ann_hoare.induct [THEN conjunct1]

lemmas AnnBasic = oghoare_ann_hoare.AnnBasic
lemmas AnnSeq = oghoare_ann_hoare.AnnSeq
lemmas AnnCond1 = oghoare_ann_hoare.AnnCond1
lemmas AnnCond2 = oghoare_ann_hoare.AnnCond2
lemmas AnnWhile = oghoare_ann_hoare.AnnWhile
lemmas AnnAwait = oghoare_ann_hoare.AnnAwait
lemmas AnnConseq = oghoare_ann_hoare.AnnConseq

lemmas Parallel = oghoare_ann_hoare.Parallel
lemmas Basic = oghoare_ann_hoare.Basic
lemmas Seq = oghoare_ann_hoare.Seq
lemmas Cond = oghoare_ann_hoare.Cond
lemmas While = oghoare_ann_hoare.While
lemmas Conseq = oghoare_ann_hoare.Conseq

subsection ‹Soundness of the System for Atomic Programs›

lemma Basic_ntran [rule_format]:
"(Basic f, s) -Pn→ (Parallel Ts, t) ⟶ All_None Ts ⟶ t = f s"
apply(induct "n")
apply(simp (no_asm))
apply(fast dest: relpow_Suc_D2 Parallel_empty_lemma elim: transition_cases)
done

lemma SEM_fwhile: "SEM S (p ∩ b) ⊆ p ⟹ SEM (fwhile b S k) p ⊆ (p ∩ -b)"
apply (induct "k")
apply(simp (no_asm) add: L3_5iv L3_5ii Parallel_empty)
apply(rule conjI)
apply (blast dest: L3_5i)
apply (auto dest: Basic_ntran rtrancl_imp_UN_relpow)
apply blast
done

lemma atom_hoare_sound [rule_format]:
" ∥- p c q ⟶ atom_com(c) ⟶ ∥= p c q"
apply (unfold com_validity_def)
apply(rule oghoare_induct)
apply simp_all
―‹Basic›
apply(fast dest: rtrancl_imp_UN_relpow Basic_ntran)
―‹Seq›
apply(rule impI)
apply(rule subset_trans)
prefer 2 apply simp
―‹Cond›
―‹While›
apply (force simp add: L3_5v dest: SEM_fwhile)
―‹Conseq›
done

subsection ‹Soundness of the System for Component Programs›

inductive_cases ann_transition_cases:
"(None,s) -1→ (c', s')"
"(Some (AnnBasic r f),s) -1→ (c', s')"
"(Some (AnnSeq c1 c2), s) -1→ (c', s')"
"(Some (AnnCond1 r b c1 c2), s) -1→ (c', s')"
"(Some (AnnCond2 r b c), s) -1→ (c', s')"
"(Some (AnnWhile r b I c), s) -1→ (c', s')"
"(Some (AnnAwait r b c),s) -1→ (c', s')"

text ‹Strong Soundness for Component Programs:›

lemma ann_hoare_case_analysis [rule_format]: "⊢ C q' ⟶
((∀r f. C = AnnBasic r f ⟶ (∃q. r ⊆ {s. f s ∈ q} ∧ q ⊆ q')) ∧
(∀c0 c1. C = AnnSeq c0 c1 ⟶ (∃q. q ⊆ q' ∧ ⊢ c0 pre c1 ∧ ⊢ c1 q)) ∧
(∀r b c1 c2. C = AnnCond1 r b c1 c2 ⟶ (∃q. q ⊆ q' ∧
r ∩ b ⊆ pre c1 ∧ ⊢ c1 q ∧ r ∩ -b ⊆ pre c2 ∧ ⊢ c2 q)) ∧
(∀r b c. C = AnnCond2 r b c ⟶
(∃q. q ⊆ q' ∧ r ∩ b ⊆ pre c  ∧ ⊢ c q ∧ r ∩ -b ⊆ q)) ∧
(∀r i b c. C = AnnWhile r b i c ⟶
(∃q. q ⊆ q' ∧ r ⊆ i ∧ i ∩ b ⊆ pre c ∧ ⊢ c i ∧ i ∩ -b ⊆ q)) ∧
(∀r b c. C = AnnAwait r b c ⟶ (∃q. q ⊆ q' ∧ ∥- (r ∩ b) c q)))"
apply(rule ann_hoare_induct)
apply simp_all
apply(rule_tac x=q in exI,simp)+
apply(rule conjI,clarify,simp,clarify,rule_tac x=qa in exI,fast)+
apply(clarify,simp,clarify,rule_tac x=qa in exI,fast)
done

lemma Help: "(transition ∩ {(x,y). True}) = (transition)"
apply force
done

lemma Strong_Soundness_aux_aux [rule_format]:
"(co, s) -1→ (co', t) ⟶ (∀c. co = Some c ⟶ s∈ pre c ⟶
(∀q. ⊢ c q ⟶ (if co' = None then t∈q else t ∈ pre(the co') ∧ ⊢ (the co') q )))"
apply(rule ann_transition_transition.induct [THEN conjunct1])
apply simp_all
―‹Basic›
apply clarify
apply(frule ann_hoare_case_analysis)
apply force
―‹Seq›
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply(fast intro: AnnConseq)
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply clarify
apply(rule conjI)
apply force
apply(rule AnnSeq,simp)
apply(fast intro: AnnConseq)
―‹Cond1›
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply(fast intro: AnnConseq)
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply(fast intro: AnnConseq)
―‹Cond2›
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply(fast intro: AnnConseq)
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply(fast intro: AnnConseq)
―‹While›
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply force
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply auto
apply(rule AnnSeq)
apply simp
apply(rule AnnWhile)
apply simp_all
―‹Await›
apply(frule ann_hoare_case_analysis,simp)
apply clarify
apply(drule atom_hoare_sound)
apply simp
apply force
done

lemma Strong_Soundness_aux: "⟦ (Some c, s) -*→ (co, t); s ∈ pre c; ⊢ c q ⟧
⟹ if co = None then t ∈ q else t ∈ pre (the co) ∧ ⊢ (the co) q"
apply(erule rtrancl_induct2)
apply simp
apply(case_tac "a")
apply(fast elim: ann_transition_cases)
apply(erule Strong_Soundness_aux_aux)
apply simp
apply simp_all
done

lemma Strong_Soundness: "⟦ (Some c, s)-*→(co, t); s ∈ pre c; ⊢ c q ⟧
⟹ if co = None then t∈q else t ∈ pre (the co)"
apply(force dest:Strong_Soundness_aux)
done

lemma ann_hoare_sound: "⊢ c q  ⟹ ⊨ c q"
apply (unfold ann_com_validity_def ann_SEM_def ann_sem_def)
apply clarify
apply(drule Strong_Soundness)
apply simp_all
done

subsection ‹Soundness of the System for Parallel Programs›

lemma Parallel_length_post_P1: "(Parallel Ts,s) -P1→ (R', t) ⟹
(∃Rs. R' = (Parallel Rs) ∧ (length Rs) = (length Ts) ∧
(∀i. i<length Ts ⟶ post(Rs ! i) = post(Ts ! i)))"
apply(erule transition_cases)
apply simp
apply clarify
apply(case_tac "i=ia")
apply simp+
done

lemma Parallel_length_post_PStar: "(Parallel Ts,s) -P*→ (R',t) ⟹
(∃Rs. R' = (Parallel Rs) ∧ (length Rs) = (length Ts) ∧
(∀i. i<length Ts ⟶ post(Ts ! i) = post(Rs ! i)))"
apply(erule rtrancl_induct2)
apply(simp_all)
apply clarify
apply simp
apply(drule Parallel_length_post_P1)
apply auto
done

lemma assertions_lemma: "pre c ∈ assertions c"
apply(rule ann_com_com.induct [THEN conjunct1])
apply auto
done

lemma interfree_aux1 [rule_format]:
"(c,s) -1→ (r,t)  ⟶ (interfree_aux(c1, q1, c) ⟶ interfree_aux(c1, q1, r))"
apply (rule ann_transition_transition.induct [THEN conjunct1])
apply(safe)
prefer 13
apply (rule TrueI)
apply force+
done

lemma interfree_aux2 [rule_format]:
"(c,s) -1→ (r,t) ⟶ (interfree_aux(c, q, a)  ⟶ interfree_aux(r, q, a) )"
apply (rule ann_transition_transition.induct [THEN conjunct1])
done

lemma interfree_lemma: "⟦ (Some c, s) -1→ (r, t);interfree Ts ; i<length Ts;
Ts!i = (Some c, q) ⟧ ⟹ interfree (Ts[i:= (r, q)])"
apply clarify
apply(case_tac "i=j")
apply(drule_tac t = "ia" in not_sym)
apply simp_all
apply(force elim: interfree_aux1)
done

text ‹Strong Soundness Theorem for Parallel Programs:›

lemma Parallel_Strong_Soundness_Seq_aux:
"⟦interfree Ts; i<length Ts; com(Ts ! i) = Some(AnnSeq c0 c1) ⟧
⟹  interfree (Ts[i:=(Some c0, pre c1)])"
apply clarify
apply(case_tac "i=j")
apply(case_tac "i=ia")
apply(erule_tac x=ia in allE)
apply simp
done

lemma Parallel_Strong_Soundness_Seq [rule_format (no_asm)]:
"⟦ ∀i<length Ts. (if com(Ts!i) = None then b ∈ post(Ts!i)
else b ∈ pre(the(com(Ts!i))) ∧ ⊢ the(com(Ts!i)) post(Ts!i));
com(Ts ! i) = Some(AnnSeq c0 c1); i<length Ts; interfree Ts ⟧ ⟹
(∀ia<length Ts. (if com(Ts[i:=(Some c0, pre c1)]! ia) = None
then b ∈ post(Ts[i:=(Some c0, pre c1)]! ia)
else b ∈ pre(the(com(Ts[i:=(Some c0, pre c1)]! ia))) ∧
⊢ the(com(Ts[i:=(Some c0, pre c1)]! ia)) post(Ts[i:=(Some c0, pre c1)]! ia)))
∧ interfree (Ts[i:= (Some c0, pre c1)])"
apply(rule conjI)
apply safe
apply(case_tac "i=ia")
apply simp
apply(force dest: ann_hoare_case_analysis)
apply simp
apply(fast elim: Parallel_Strong_Soundness_Seq_aux)
done

lemma Parallel_Strong_Soundness_aux_aux [rule_format]:
"(Some c, b) -1→ (co, t) ⟶
(∀Ts. i<length Ts ⟶ com(Ts ! i) = Some c ⟶
(∀i<length Ts. (if com(Ts ! i) = None then b∈post(Ts!i)
else b∈pre(the(com(Ts!i))) ∧ ⊢ the(com(Ts!i)) post(Ts!i))) ⟶
interfree Ts ⟶
(∀j. j<length Ts ∧ i≠j ⟶ (if com(Ts!j) = None then t∈post(Ts!j)
else t∈pre(the(com(Ts!j))) ∧ ⊢ the(com(Ts!j)) post(Ts!j))) )"
apply(rule ann_transition_transition.induct [THEN conjunct1])
apply safe
prefer 11
apply(rule TrueI)
apply simp_all
―‹Basic›
apply(erule_tac x = "i" in all_dupE, erule (1) notE impE)
apply(erule_tac x = "j" in allE , erule (1) notE impE)
apply(erule_tac x = "j" in allE,simp)
apply(erule_tac x = "i" in allE,simp)
apply(drule_tac t = "i" in not_sym)
apply(case_tac "com(Ts ! j)=None")
apply(force intro: converse_rtrancl_into_rtrancl
simp add: interfree_aux_def com_validity_def SEM_def sem_def All_None_def)
apply clarify
apply simp
apply(erule_tac x="pre y" in ballE)
apply(force intro: converse_rtrancl_into_rtrancl
simp add: com_validity_def SEM_def sem_def All_None_def)
―‹Seqs›
apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
apply(drule  Parallel_Strong_Soundness_Seq,simp+)
apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
apply(drule  Parallel_Strong_Soundness_Seq,simp+)
―‹Await›
apply(rule_tac x = "i" in allE , assumption , erule (1) notE impE)
apply(erule_tac x = "j" in allE , erule (1) notE impE)
apply(erule_tac x = "j" in allE,simp)
apply(erule_tac x = "i" in allE,simp)
apply(drule_tac t = "i" in not_sym)
apply(case_tac "com(Ts ! j)=None")
apply(force intro: converse_rtrancl_into_rtrancl simp add: interfree_aux_def
com_validity_def SEM_def sem_def All_None_def Help)
apply clarify
apply simp
apply(erule_tac x="pre y" in ballE)
apply(force intro: converse_rtrancl_into_rtrancl
simp add: com_validity_def SEM_def sem_def All_None_def Help)
done

lemma Parallel_Strong_Soundness_aux [rule_format]:
"⟦(Ts',s) -P*→ (Rs',t);  Ts' = (Parallel Ts); interfree Ts;
∀i. i<length Ts ⟶ (∃c q. (Ts ! i) = (Some c, q) ∧ s∈(pre c) ∧ ⊢ c q ) ⟧ ⟹
∀Rs. Rs' = (Parallel Rs) ⟶ (∀j. j<length Rs ⟶
(if com(Rs ! j) = None then t∈post(Ts ! j)
else t∈pre(the(com(Rs ! j))) ∧ ⊢ the(com(Rs ! j)) post(Ts ! j))) ∧ interfree Rs"
apply(erule rtrancl_induct2)
apply clarify
―‹Base›
apply force
―‹Induction step›
apply clarify
apply(drule Parallel_length_post_PStar)
apply clarify
apply (ind_cases "(Parallel Ts, s) -P1→ (Parallel Rs, t)" for Ts s Rs t)
apply(rule conjI)
apply clarify
apply(case_tac "i=j")
apply(simp split del:if_split)
apply(erule Strong_Soundness_aux_aux,simp+)
apply force
apply force
apply(simp split del: if_split)
apply(erule Parallel_Strong_Soundness_aux_aux)
apply force
apply(rule interfree_lemma)
apply simp_all
done

lemma Parallel_Strong_Soundness:
"⟦(Parallel Ts, s) -P*→ (Parallel Rs, t); interfree Ts; j<length Rs;
∀i. i<length Ts ⟶ (∃c q. Ts ! i = (Some c, q) ∧ s∈pre c ∧ ⊢ c q) ⟧ ⟹
if com(Rs ! j) = None then t∈post(Ts ! j) else t∈pre (the(com(Rs ! j)))"
apply(drule  Parallel_Strong_Soundness_aux)
apply simp+
done

lemma oghoare_sound [rule_format]: "∥- p c q ⟶ ∥= p c q"
apply (unfold com_validity_def)
apply(rule oghoare_induct)
apply(rule TrueI)+
―‹Parallel›
apply(clarify, rename_tac x y i Ts')
apply(frule Parallel_length_post_PStar)
apply clarify
apply(drule_tac j=i in Parallel_Strong_Soundness)
apply clarify
apply simp
apply force
apply simp
apply(erule_tac V = "∀i. P i" for P in thin_rl)
apply(drule_tac s = "length Rs" in sym)
apply(erule allE, erule impE, assumption)
apply(force dest: nth_mem simp add: All_None_def)
―‹Basic›
apply(force dest: rtrancl_imp_UN_relpow Basic_ntran)
―‹Seq›
apply(rule subset_trans)
prefer 2 apply assumption