| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Simpl/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 187 kB |
|
Impressum HoareTotalProps.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(* Author: Norbert Schirmer Maintainer: Norbert Schirmer, norbert.schirmer at web de Copyright (C) 2004-2008 Norbert Schirmer Copyright (c) 2022 Apple Inc. All rights reserved. *) section ‹Properties of Total Correctness Hoare Logic› theory HoareTotalProps imports SmallStep HoareTotalDef HoarePartialProps begin subsection ‹Soundness› lemma hoaret_sound: assumes hoare: "Γ,Θ⊨tF P c Q,A" shows "Γ,Θ⊨tF P c Q,A" using hoare proof (induct) case (Skip Θ F P A) show "Γ,Θ ⊨tF P Skip P,A" proof (rule cvalidtI) fix s t assume "Γ⊨⟨Skip,Normal s⟩ → t" "s ∈ P" thus "t ∈ Normal ` P ∪ Abrupt ` A" by cases auto next fix s show "Γ⊨Skip ↓ Normal s" by (rule terminates.intros) qed next case (Basic Θ F f P A) show "Γ,Θ ⊨tF {s. f s ∈ P} (Basic f) P,A" proof (rule cvalidtI) fix s t assume "Γ⊨⟨Basic f,Normal s⟩ → t" "s ∈ {s. f s ∈ P}" thus "t ∈ Normal ` P ∪ Abrupt ` A" by cases auto next fix s show "Γ⊨Basic f ↓ Normal s" by (rule terminates.intros) qed next case (Spec Θ F r Q A) show "Γ,Θ⊨tF {s. (∀t. (s, t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s, t) ∈ r)} Spec r Q,A" proof (rule cvalidtI) fix s t assume "Γ⊨⟨Spec r ,Normal s⟩ → t" "s ∈ {s. (∀t. (s, t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s, t) ∈ r)}" thus "t ∈ Normal ` Q ∪ Abrupt ` A" by cases auto next fix s show "Γ⊨Spec r ↓ Normal s" by (rule terminates.intros) qed next case (Seq Θ F P c1 R A c2 Q) have valid_c1: "Γ,Θ ⊨tF P c1 R,A" by fact have valid_c2: "Γ,Θ ⊨tF R c2 Q,A" by fact show "Γ,Θ ⊨tF P Seq c1 c2 Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume exec: "Γ⊨⟨Seq c1 c2,Normal s⟩ → t" assume P: "s ∈ P" assume t_notin_F: "t ∉ Fault ` F" from exec P obtain r where exec_c1: "Γ⊨⟨c1,Normal s⟩ → r" and exec_c2: "Γ⊨⟨c2,r⟩ → t" by cases auto with t_notin_F have "r ∉ Fault ` F" by (auto dest: Fault_end) from valid_c1 ctxt exec_c1 P this have r: "r ∈ Normal ` R ∪ Abrupt ` A" by (rule cvalidt_postD) show "t∈Normal ` Q ∪ Abrupt ` A" proof (cases r) case (Normal r') with exec_c2 r show "t∈Normal ` Q ∪ Abrupt ` A" apply - apply (rule cvalidt_postD [OF valid_c2 ctxt _ _ t_notin_F]) apply auto done next case (Abrupt r') with exec_c2 have "t=Abrupt r'" by (auto elim: exec_elim_cases) with Abrupt r show ?thesis by auto next case Fault with r show ?thesis by blast next case Stuck with r show ?thesis by blast qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume P: "s∈P" show "Γ⊨Seq c1 c2 ↓ Normal s" proof - from valid_c1 ctxt P have "Γ⊨c1↓ Normal s" by (rule cvalidt_termD) moreover { fix r assume exec_c1: "Γ⊨⟨c1,Normal s⟩ → r" have "Γ⊨c2 ↓ r" proof (cases r) case (Normal r') with cvalidt_postD [OF valid_c1 ctxt exec_c1 P] have r: "r∈Normal ` R" by auto with cvalidt_termD [OF valid_c2 ctxt] exec_c1 show "Γ⊨c2 ↓ r" by auto qed auto } ultimately show ?thesis by (iprover intro: terminates.intros) qed qed next case (Cond Θ F P b c1 Q A c2) have valid_c1: "Γ,Θ ⊨tF (P ∩ b) c1 Q,A" by fact have valid_c2: "Γ,Θ ⊨tF (P ∩ - b) c2 Q,A" by fact show "Γ,Θ ⊨tF P Cond b c1 c2 Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume exec: "Γ⊨⟨Cond b c1 c2,Normal s⟩ → t" assume P: "s ∈ P" assume t_notin_F: "t ∉ Fault ` F" show "t ∈ Normal ` Q ∪ Abrupt ` A" proof (cases "s∈b") case True with exec have "Γ⊨⟨c1,Normal s⟩ → t" by cases auto with P True show ?thesis by - (rule cvalidt_postD [OF valid_c1 ctxt _ _ t_notin_F],auto) next case False with exec P have "Γ⊨⟨c2,Normal s⟩ → t" by cases auto with P False show ?thesis by - (rule cvalidt_postD [OF valid_c2 ctxt _ _ t_notin_F],auto) qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume P: "s ∈ P" thus "Γ⊨Cond b c1 c2 ↓ Normal s" using cvalidt_termD [OF valid_c1 ctxt] cvalidt_termD [OF valid_c2 ctxt] by (cases "s ∈ b") (auto intro: terminates.intros) qed next case (While r Θ F P b c A) assume wf: "wf r" have valid_c: "∀σ. Γ,Θ⊨tF ({σ} ∩ P ∩ b) c ({t. (t, σ) ∈ r} ∩ P),A" using While.hyps by iprover show "Γ,Θ ⊨tF P (While b c) (P ∩ - b),A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume wprems: "Γ⊨⟨While b c,Normal s⟩ → t" "s ∈ P" "t ∉ Fault ` F" from wf have "∧t. [Γ⊨⟨While b c,Normal s⟩ → t; s ∈ P; t ∉ Fault ` F] ==> t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A" proof (induct) fix s t assume hyp: "∧s' t. [(s',s)∈r; Γ⊨⟨While b c,Normal s'⟩ → t; s' ∈ P; t ∉ Fault ` F] ==> t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A" assume exec: "Γ⊨⟨While b c,Normal s⟩ → t" assume P: "s ∈ P" assume t_notin_F: "t ∉ Fault ` F" from exec show "t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A" proof (cases) fix s' assume b: "s∈b" assume exec_c: "Γ⊨⟨c,Normal s⟩ → s'" assume exec_w: "Γ⊨⟨While b c,s'⟩ → t" from exec_w t_notin_F have "s' ∉ Fault ` F" by (auto dest: Fault_end) from exec_c P b valid_c ctxt this have s': "s' ∈ Normal ` ({s'. (s', s) ∈ r} ∩ P) ∪ Abrupt ` A" by (auto simp add: cvalidt_def validt_def valid_def) show ?thesis proof (cases s') case Normal with exec_w s' t_notin_F show ?thesis by - (rule hyp,auto) next case Abrupt with exec_w have "t=s'" by (auto dest: Abrupt_end) with Abrupt s' show ?thesis by blast next case Fault with exec_w have "t=s'" by (auto dest: Fault_end) with Fault s' show ?thesis by blast next case Stuck with exec_w have "t=s'" by (auto dest: Stuck_end) with Stuck s' show ?thesis by blast qed next assume "s∉b" "t=Normal s" with P show ?thesis by simp qed qed with wprems show "t ∈ Normal ` (P ∩ - b) ∪ Abrupt ` A" by blast next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume "s ∈ P" with wf show "Γ⊨While b c ↓ Normal s" proof (induct) fix s assume hyp: "∧s'. [(s',s)∈r; s' ∈ P] ==> Γ⊨While b c ↓ Normal s'" assume P: "s ∈ P" show "Γ⊨While b c ↓ Normal s" proof (cases "s ∈ b") case False with P show ?thesis by (blast intro: terminates.intros) next case True with valid_c P ctxt have "Γ⊨c ↓ Normal s" by (simp add: cvalidt_def validt_def) moreover { fix s' assume exec_c: "Γ⊨⟨c,Normal s⟩ → s'" have "Γ⊨While b c ↓ s'" proof (cases s') case (Normal s'') with exec_c P True valid_c ctxt have s': "s' ∈ Normal ` ({s'. (s', s) ∈ r} ∩ P)" by (fastforce simp add: cvalidt_def validt_def valid_def) then show ?thesis by (blast intro: hyp) qed auto } ultimately show ?thesis by (blast intro: terminates.intros) qed qed qed next case (Guard Θ F g P c Q A f) have valid_c: "Γ,Θ ⊨tF (g ∩ P) c Q,A" by fact show "Γ,Θ ⊨tF (g ∩ P) Guard f g c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume exec: "Γ⊨⟨Guard f g c,Normal s⟩ → t" assume t_notin_F: "t ∉ Fault ` F" assume P:"s ∈ (g ∩ P)" from exec P have "Γ⊨⟨c,Normal s⟩ → t" by cases auto from valid_c ctxt this P t_notin_F show "t ∈ Normal ` Q ∪ Abrupt ` A" by (rule cvalidt_postD) next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume P:"s ∈ (g ∩ P)" thus "Γ⊨Guard f g c ↓ Normal s" by (auto intro: terminates.intros cvalidt_termD [OF valid_c ctxt]) qed next case (Guarantee f F Θ g P c Q A) have valid_c: "Γ,Θ ⊨tF (g ∩ P) c Q,A" by fact have f_F: "f ∈ F" by fact show "Γ,Θ ⊨tF P Guard f g c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume exec: "Γ⊨⟨Guard f g c,Normal s⟩ → t" assume t_notin_F: "t ∉ Fault ` F" assume P:"s ∈ P" from exec f_F t_notin_F have g: "s ∈ g" by cases auto with P have P': "s ∈ g ∩ P" by blast from exec g have "Γ⊨⟨c,Normal s⟩ → t" by cases auto from valid_c ctxt this P' t_notin_F show "t ∈ Normal ` Q ∪ Abrupt ` A" by (rule cvalidt_postD) next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume P:"s ∈ P" thus "Γ⊨Guard f g c ↓ Normal s" by (auto intro: terminates.intros cvalidt_termD [OF valid_c ctxt]) qed next case (CallRec P p Q A Specs r Specs_wf Θ F) have p: "(P,p,Q,A) ∈ Specs" by fact have wf: "wf r" by fact have Specs_wf: "Specs_wf = (λp τ. (λ(P,q,Q,A). (P ∩ {s. ((s, q),τ,p) ∈ r},q,Q,A)) ` Specs)" by fact from CallRec.hyps have valid_body: "∀(P, p, Q, A)∈Specs. p ∈ dom Γ ∧ (∀τ. Γ,Θ ∪ Specs_wf p τ⊨tF ({τ} ∩ P) the (Γ p) Q,A)" by auto show "Γ,Θ ⊨tF P (Call p) Q,A" proof - { fix τp assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" from wf have "∧τ p P Q A. [τp = (τ,p); (P,p,Q,A) ∈ Specs] ==> Γ⊨tF ({τ} ∩ P) (the (Γ (p))) Q,A" proof (induct τp rule: wf_induct [rule_format, consumes 1, case_names WF]) case (WF τp τ p P Q A) have τp: "τp = (τ, p)" by fact have p: "(P, p, Q, A) ∈ Specs" by fact { fix q P' Q' A' assume q: "(P',q,Q',A') ∈ Specs" have "Γ⊨tF (P' ∩ {s. ((s,q), τ,p) ∈ r}) (Call q) Q',A'" proof (rule validtI) fix s t assume exec_q: "Γ⊨⟨Call q,Normal s⟩ → t" assume Pre: "s ∈ P' ∩ {s. ((s,q), τ,p) ∈ r}" assume t_notin_F: "t ∉ Fault ` F" from Pre q τp have valid_bdy: "Γ⊨tF ({s} ∩ P') the (Γ q) Q',A'" by - (rule WF.hyps, auto) from Pre q have Pre': "s ∈ {s} ∩ P'" by auto from exec_q show "t ∈ Normal ` Q' ∪ Abrupt ` A'" proof (cases) fix bdy assume bdy: "Γ q = Some bdy" assume exec_bdy: "Γ⊨⟨bdy,Normal s⟩ → t" from valid_bdy [simplified bdy option.sel] t_notin_F exec_bdy Pre' have "t ∈ Normal ` Q' ∪ Abrupt ` A'" by (auto simp add: validt_def valid_def) with Pre q show ?thesis by auto next assume "Γ q = None" with q valid_body have False by auto thus ?thesis .. qed next fix s assume Pre: "s ∈ P' ∩ {s. ((s,q), τ,p) ∈ r}" from Pre q τp have valid_bdy: "Γ ⊨tF ({s} ∩ P') (the (Γ q)) Q',A'" by - (rule WF.hyps, auto) from Pre q have Pre': "s ∈ {s} ∩ P'" by auto from valid_bdy ctxt Pre' have "Γ⊨the (Γ q) ↓ Normal s" by (auto simp add: validt_def) with valid_body q show "Γ⊨Call q↓ Normal s" by (fastforce intro: terminates.Call) qed } hence "∀(P, p, Q, A)∈Specs_wf p τ. Γ⊨tF P Call p Q,A" by (auto simp add: cvalidt_def Specs_wf) with ctxt have "∀(P, p, Q, A)∈Θ ∪ Specs_wf p τ. Γ⊨tF P Call p Q,A" by auto with p valid_body show "Γ ⊨tF ({τ} ∩ P) (the (Γ p)) Q,A" by (simp add: cvalidt_def) blast qed } note lem = this have valid_body': "∧τ. ∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A ==> ∀(P,p,Q,A)∈Specs. Γ⊨tF ({τ} ∩ P) (the (Γ p)) Q,A" by (auto intro: lem) show "Γ,Θ ⊨tF P (Call p) Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume exec_call: "Γ⊨⟨Call p,Normal s⟩ → t" assume P: "s ∈ P" assume t_notin_F: "t ∉ Fault ` F" from exec_call show "t ∈ Normal ` Q ∪ Abrupt ` A" proof (cases) fix bdy assume bdy: "Γ p = Some bdy" assume exec_body: "Γ⊨⟨bdy,Normal s⟩ → t" from exec_body bdy p P t_notin_F valid_body' [of "s", OF ctxt] ctxt have "t ∈ Normal ` Q ∪ Abrupt ` A" apply (simp only: cvalidt_def validt_def valid_def) apply (drule (1) bspec) apply auto done with p P show ?thesis by simp next assume "Γ p = None" with p valid_body have False by auto thus ?thesis by simp qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume P: "s ∈ P" show "Γ⊨Call p ↓ Normal s" proof - from ctxt P p valid_body' [of "s",OF ctxt] have "Γ⊨(the (Γ p)) ↓ Normal s" by (auto simp add: cvalidt_def validt_def) with valid_body p show ?thesis by (fastforce intro: terminates.Call) qed qed qed next case (DynCom P Θ F c Q A) hence valid_c: "∀s∈P. Γ,Θ⊨tF P (c s) Q,A" by simp show "Γ,Θ⊨tF P DynCom c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume exec: "Γ⊨⟨DynCom c,Normal s⟩ → t" assume P: "s ∈ P" assume t_notin_F: "t ∉ Fault ` F" from exec show "t ∈ Normal ` Q ∪ Abrupt ` A" proof (cases) assume "Γ⊨⟨c s,Normal s⟩ → t" from cvalidt_postD [OF valid_c [rule_format, OF P] ctxt this P t_notin_F] show ?thesis . qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume P: "s ∈ P" show "Γ⊨DynCom c ↓ Normal s" proof - from cvalidt_termD [OF valid_c [rule_format, OF P] ctxt P] have "Γ⊨c s ↓ Normal s" . thus ?thesis by (rule terminates.intros) qed qed next case (Throw Θ F A Q) show "Γ,Θ ⊨tF A Throw Q,A" proof (rule cvalidtI) fix s t assume "Γ⊨⟨Throw,Normal s⟩ → t" "s ∈ A" then show "t ∈ Normal ` Q ∪ Abrupt ` A" by cases simp next fix s show "Γ⊨Throw ↓ Normal s" by (rule terminates.intros) qed next case (Catch Θ F P c1 Q R c2 A) have valid_c1: "Γ,Θ ⊨tF P c1 Q,R" by fact have valid_c2: "Γ,Θ ⊨tF R c2 Q,A" by fact show "Γ,Θ ⊨tF P Catch c1 c2 Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume exec: "Γ⊨⟨Catch c1 c2,Normal s⟩ → t" assume P: "s ∈ P" assume t_notin_F: "t ∉ Fault ` F" from exec show "t ∈ Normal ` Q ∪ Abrupt ` A" proof (cases) fix s' assume exec_c1: "Γ⊨⟨c1,Normal s⟩ → Abrupt s'" assume exec_c2: "Γ⊨⟨c2,Normal s'⟩ → t" from cvalidt_postD [OF valid_c1 ctxt exec_c1 P] have "Abrupt s' ∈ Abrupt ` R" by auto with cvalidt_postD [OF valid_c2 ctxt] exec_c2 t_notin_F show ?thesis by fastforce next assume exec_c1: "Γ⊨⟨c1,Normal s⟩ → t" assume notAbr: "¬ isAbr t" from cvalidt_postD [OF valid_c1 ctxt exec_c1 P] t_notin_F have "t ∈ Normal ` Q ∪ Abrupt ` R" . with notAbr show ?thesis by auto qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume P: "s ∈ P" show "Γ⊨Catch c1 c2 ↓ Normal s" proof - from valid_c1 ctxt P have "Γ⊨c1↓ Normal s" by (rule cvalidt_termD) moreover { fix r assume exec_c1: "Γ⊨⟨c1,Normal s⟩ → Abrupt r" from cvalidt_postD [OF valid_c1 ctxt exec_c1 P] have r: "Abrupt r∈Normal ` Q ∪ Abrupt ` R" by auto hence "Abrupt r∈Abrupt ` R" by fast with cvalidt_termD [OF valid_c2 ctxt] exec_c1 have "Γ⊨c2 ↓ Normal r" by fast } ultimately show ?thesis by (iprover intro: terminates.intros) qed qed next case (Conseq P Θ F c Q A) hence adapt: "∀s ∈ P. (∃P' Q' A'. (Γ,Θ ⊨tF P' c Q',A') ∧ s ∈ P'∧ Q' ⊆ Q ∧ A' ⊆ A)" by blast show "Γ,Θ ⊨tF P c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume exec: "Γ⊨⟨c,Normal s⟩ → t" assume P: "s ∈ P" assume t_notin_F: "t ∉ Fault ` F" show "t ∈ Normal ` Q ∪ Abrupt ` A" proof - from adapt [rule_format, OF P] obtain P' and Q' and A' where valid_P'_Q': "Γ,Θ ⊨tF P' c Q',A'" and weaken: "s ∈ P'" "Q' ⊆ Q" "A'⊆ A" by blast from exec valid_P'_Q' ctxt t_notin_F have P'_Q': "Normal s ∈ Normal ` P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A'" by (unfold cvalidt_def validt_def valid_def) blast hence "s ∈ P' ⟶ t ∈ Normal ` Q' ∪ Abrupt ` A'" by blast with weaken show ?thesis by blast qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume P: "s ∈ P" show "Γ⊨c ↓ Normal s" proof - from P adapt obtain P' and Q' and A' where "Γ,Θ ⊨tF P' c Q',A'" "s ∈ P'" by blast with ctxt show ?thesis by (simp add: cvalidt_def validt_def) qed qed next case (Asm P p Q A Θ F) assume "(P, p, Q, A) ∈ Θ" then show "Γ,Θ ⊨tF P (Call p) Q,A" by (auto simp add: cvalidt_def ) next case ExFalso thus ?case by iprover qed lemma hoaret_sound': "Γ,{}⊨tF P c Q,A ==> Γ⊨tF P c Q,A" apply (drule hoaret_sound) apply (simp add: cvalidt_def) done theorem total_to_partial: assumes total: "Γ,{}⊨tF P c Q,A" shows "Γ,{}⊨F P c Q,A" proof - from total have "Γ,{}⊨tF P c Q,A" by (rule hoaret_sound) hence "Γ⊨F P c Q,A" by (simp add: cvalidt_def validt_def cvalid_def) thus ?thesis by (rule hoare_complete) qed subsection ‹Completeness› lemma MGT_valid: "Γ⊨tF {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c↓Normal s} c {t. Γ⊨⟨c,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}" proof (rule validtI) fix s t assume "Γ⊨⟨c,Normal s⟩ → t" "s ∈ {s. s = Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c↓Normal s}" "t ∉ Fault ` F" thus "t ∈ Normal ` {t. Γ⊨⟨c,Normal Z⟩ → Normal t} ∪ Abrupt ` {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}" apply (cases t) apply (auto simp add: final_notin_def) done next fix s assume "s ∈ {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c↓Normal s}" thus "Γ⊨c↓Normal s" by blast qed text ‹The consequence rule where the existential @{term Z} is instantiated @{term s}. Usefull in proof of ‹MGT_lemma›.› lemma ConseqMGT: assumes modif: "∀Z::'a. Γ,Θ ⊨tF (P' Z::'a assn) c (Q' Z),(A' Z)" assumes impl: "∧s. s ∈ P ==> s ∈ P' s ∧ (∀t. t ∈ Q' s ⟶ t ∈ Q) ∧ (∀t. t ∈ A' s ⟶ t ∈ A)" shows "Γ,Θ ⊨tF P c Q,A" using impl by - (rule conseq [OF modif],blast) lemma MGT_implies_complete: assumes MGT: "∀Z. Γ,{}⊨tF {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c↓Normal s} c {t. Γ⊨⟨c,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}" assumes valid: "Γ ⊨tF P c Q,A" shows "Γ,{} ⊨tF P c Q,A" using MGT apply (rule ConseqMGT) apply (insert valid) apply (auto simp add: validt_def valid_def intro!: final_notinI) done lemma conseq_extract_state_indep_prop: assumes state_indep_prop:"∀s ∈ P. R" assumes to_show: "R ==> Γ,Θ⊨tF P c Q,A" shows "Γ,Θ⊨tF P c Q,A" apply (rule Conseq) apply (clarify) apply (rule_tac x="P" in exI) apply (rule_tac x="Q" in exI) apply (rule_tac x="A" in exI) using state_indep_prop to_show by blast lemma MGT_lemma: assumes MGT_Calls: "∀p ∈ dom Γ. ∀Z. Γ,Θ ⊨tF {s. s=Z ∧ Γ⊨⟨Call p,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨(Call p)↓Normal s} (Call p) {t. Γ⊨⟨Call p,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Call p,Normal Z⟩ → Abrupt t}" shows "∧Z. Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c↓Normal s} c {t. Γ⊨⟨c,Normal Z⟩ → Normal t},{t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}" proof (induct c) case Skip show "Γ,Θ⊨tF {s. s = Z ∧ Γ⊨⟨Skip,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Skip ↓ Normal s} Skip {t. Γ⊨⟨Skip,Normal Z⟩ → Normal t},{t. Γ⊨⟨Skip,Normal Z⟩ → Abrupt t}" by (rule hoaret.Skip [THEN conseqPre]) (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros terminates.intros) next case (Basic f) show "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨Basic f,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Basic f ↓ Normal s} Basic f {t. Γ⊨⟨Basic f,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Basic f,Normal Z⟩ → Abrupt t}" by (rule hoaret.Basic [THEN conseqPre]) (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros terminates.intros) next case (Spec r) show "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨Spec r,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Spec r ↓ Normal s} Spec r {t. Γ⊨⟨Spec r,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Spec r,Normal Z⟩ → Abrupt t}" apply (rule hoaret.Spec [THEN conseqPre]) apply (clarsimp simp add: final_notin_def) apply (case_tac "∃t. (Z,t) ∈ r") apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros) done next case (Seq c1 c2) have hyp_c1: "∀Z. Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨c1,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c1↓Normal s} c1 {t. Γ⊨⟨c1,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c1,Normal Z⟩ → Abrupt t}" using Seq.hyps by iprover have hyp_c2: "∀ Z. Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c2↓Normal s} c2 {t. Γ⊨⟨c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c2,Normal Z⟩ → Abrupt t}" using Seq.hyps by iprover from hyp_c1 have "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨Seq c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Seq c1 c2↓Normal s} c1 {t. Γ⊨⟨c1,Normal Z⟩ → Normal t ∧ Γ⊨⟨c2,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c2↓Normal t}, {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t}" by (rule ConseqMGT) (auto dest: Seq_NoFaultStuckD1 [simplified] Seq_NoFaultStuckD2 [simplified] elim: terminates_Normal_elim_cases intro: exec.intros) thus "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨Seq c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Seq c1 c2↓Normal s} Seq c1 c2 {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t}" proof (rule hoaret.Seq ) show "Γ,Θ⊨tF {t. Γ⊨⟨c1,Normal Z⟩ → Normal t ∧ Γ⊨⟨c2,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c2 ↓ Normal t} c2 {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t}" proof (rule ConseqMGT [OF hyp_c2],safe) fix r t assume "Γ⊨⟨c1,Normal Z⟩ → Normal r" "Γ⊨⟨c2,Normal r⟩ → Normal t" then show "Γ⊨⟨Seq c1 c2,Normal Z⟩ → Normal t" by (rule exec.intros) next fix r t assume "Γ⊨⟨c1,Normal Z⟩ → Normal r" "Γ⊨⟨c2,Normal r⟩ → Abrupt t" then show "Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t" by (rule exec.intros) qed qed next case (Cond b c1 c2) have "∀Z. Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨c1,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c1↓Normal s} c1 {t. Γ⊨⟨c1,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c1,Normal Z⟩ → Abrupt t}" using Cond.hyps by iprover hence "Γ,Θ ⊨tF ({s. s=Z ∧ Γ⊨⟨Cond b c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨(Cond b c1 c2)↓Normal s}∩b) c1 {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t}" by (rule ConseqMGT) (fastforce simp add: final_notin_def intro: exec.CondTrue elim: terminates_Normal_elim_cases) moreover have "∀Z. Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c2↓Normal s} c2 {t. Γ⊨⟨c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c2,Normal Z⟩ → Abrupt t}" using Cond.hyps by iprover hence "Γ,Θ⊨tF ({s. s=Z ∧ Γ⊨⟨Cond b c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨(Cond b c1 c2)↓Normal s}∩-b) c2 {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t}" by (rule ConseqMGT) (fastforce simp add: final_notin_def intro: exec.CondFalse elim: terminates_Normal_elim_cases) ultimately show "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨Cond b c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨(Cond b c1 c2)↓Normal s} (Cond b c1 c2) {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t}" by (rule hoaret.Cond) next case (While b c) let ?unroll = "({(s,t). s∈b ∧ Γ⊨⟨c,Normal s⟩ → Normal t})*" let ?P' = "λZ. {t. (Z,t)∈?unroll ∧ (∀e. (Z,e)∈?unroll ⟶ e∈b ⟶ Γ⊨⟨c,Normal e⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ (∀u. Γ⊨⟨c,Normal e⟩ →Abrupt u ⟶ Γ⊨⟨While b c,Normal Z⟩ → Abrupt u)) ∧ Γ⊨(While b c)↓Normal t}" let ?A = "λZ. {t. Γ⊨⟨While b c,Normal Z⟩ → Abrupt t}" let ?r = "{(t,s). Γ⊨(While b c)↓Normal s ∧ s∈b ∧ Γ⊨⟨c,Normal s⟩ → Normal t}" show "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨While b c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨(While b c)↓Normal s} (While b c) {t. Γ⊨⟨While b c,Normal Z⟩ → Normal t}, {t. Γ⊨⟨While b c,Normal Z⟩ → Abrupt t}" proof (rule ConseqMGT [where ?P'="λ Z. ?P' Z" and ?Q'="λ Z. ?P' Z ∩ - b"]) have wf_r: "wf ?r" by (rule wf_terminates_while) show "∀ Z. Γ,Θ⊨tF (?P' Z) (While b c) (?P' Z ∩ - b),(?A Z)" proof (rule allI, rule hoaret.While [OF wf_r]) fix Z from While have hyp_c: "∀Z. Γ,Θ⊨tF{s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c↓Normal s} c {t. Γ⊨⟨c,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}" by iprover show "∀σ. Γ,Θ⊨tF ({σ} ∩ ?P' Z ∩ b) c ({t. (t, σ) ∈ ?r} ∩ ?P' Z),(?A Z)" proof (rule allI, rule ConseqMGT [OF hyp_c]) fix σ s assume "s∈ {σ} ∩ {t. (Z, t) ∈ ?unroll ∧ (∀e. (Z,e)∈?unroll ⟶ e∈b ⟶ Γ⊨⟨c,Normal e⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ (∀u. Γ⊨⟨c,Normal e⟩ →Abrupt u ⟶ Γ⊨⟨While b c,Normal Z⟩ → Abrupt u)) ∧ Γ⊨(While b c)↓Normal t} ∩ b" then obtain s_eq_σ: "s=σ" and Z_s_unroll: "(Z,s) ∈ ?unroll" and noabort:"∀e. (Z,e)∈?unroll ⟶ e∈b ⟶ Γ⊨⟨c,Normal e⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ (∀u. Γ⊨⟨c,Normal e⟩ →Abrupt u ⟶ Γ⊨⟨While b c,Normal Z⟩ → Abrupt u)" and while_term: "Γ⊨(While b c)↓Normal s" and s_in_b: "s∈b" by blast show "s ∈ {t. t = s ∧ Γ⊨⟨c,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c↓Normal t} ∧ (∀t. t ∈ {t. Γ⊨⟨c,Normal s⟩ → Normal t} ⟶ t ∈ {t. (t,σ) ∈ ?r} ∩ {t. (Z, t) ∈ ?unroll ∧ (∀e. (Z,e)∈?unroll ⟶ e∈b ⟶ Γ⊨⟨c,Normal e⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ (∀u. Γ⊨⟨c,Normal e⟩ →Abrupt u ⟶ Γ⊨⟨While b c,Normal Z⟩ → Abrupt u)) ∧ Γ⊨(While b c)↓Normal t}) ∧ (∀t. t ∈ {t. Γ⊨⟨c,Normal s⟩ → Abrupt t} ⟶ t ∈ {t. Γ⊨⟨While b c,Normal Z⟩ → Abrupt t})" (is "?C1 ∧ ?C2 ∧ ?C3") proof (intro conjI) from Z_s_unroll noabort s_in_b while_term show ?C1 by (blast elim: terminates_Normal_elim_cases) next { fix t assume s_t: "Γ⊨⟨c,Normal s⟩ → Normal t" with s_eq_σ while_term s_in_b have "(t,σ) ∈ ?r" by blast moreover from Z_s_unroll s_t s_in_b have "(Z, t) ∈ ?unroll" by (blast intro: rtrancl_into_rtrancl) moreover from while_term s_t s_in_b have "Γ⊨(While b c)↓Normal t" by (blast elim: terminates_Normal_elim_cases) moreover note noabort ultimately have "(t,σ) ∈ ?r ∧ (Z, t) ∈ ?unroll ∧ (∀e. (Z,e)∈?unroll ⟶ e∈b ⟶ Γ⊨⟨c,Normal e⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ (∀u. Γ⊨⟨c,Normal e⟩ →Abrupt u ⟶ Γ⊨⟨While b c,Normal Z⟩ → Abrupt u)) ∧ Γ⊨(While b c)↓Normal t" by iprover } then show ?C2 by blast next { fix t assume s_t: "Γ⊨⟨c,Normal s⟩ → Abrupt t" from Z_s_unroll noabort s_t s_in_b have "Γ⊨⟨While b c,Normal Z⟩ → Abrupt t" by blast } thus ?C3 by simp qed qed qed next fix s assume P: "s ∈ {s. s=Z ∧ Γ⊨⟨While b c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨While b c ↓ Normal s}" hence WhileNoFault: "Γ⊨⟨While b c,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))" by auto show "s ∈ ?P' s ∧ (∀t. t∈(?P' s ∩ - b)⟶ t∈{t. Γ⊨⟨While b c,Normal Z⟩ → Normal t})∧ (∀t. t∈?A s ⟶ t∈?A Z)" proof (intro conjI) { fix e assume "(Z,e) ∈ ?unroll" "e ∈ b" from this WhileNoFault have "Γ⊨⟨c,Normal e⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ (∀u. Γ⊨⟨c,Normal e⟩ →Abrupt u ⟶ Γ⊨⟨While b c,Normal Z⟩ → Abrupt u)" (is "?Prop Z e") proof (induct rule: converse_rtrancl_induct [consumes 1]) assume e_in_b: "e ∈ b" assume WhileNoFault: "Γ⊨⟨While b c,Normal e⟩ →∉({Stuck} ∪ Fault ` (-F))" with e_in_b WhileNoFault have cNoFault: "Γ⊨⟨c,Normal e⟩ →∉({Stuck} ∪ Fault ` (-F))" by (auto simp add: final_notin_def intro: exec.intros) moreover { fix u assume "Γ⊨⟨c,Normal e⟩ → Abrupt u" with e_in_b have "Γ⊨⟨While b c,Normal e⟩ → Abrupt u" by (blast intro: exec.intros) } ultimately show "?Prop e e" by iprover next fix Z r assume e_in_b: "e∈b" assume WhileNoFault: "Γ⊨⟨While b c,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))" assume hyp: "[e∈b;Γ⊨⟨While b c,Normal r⟩ →∉({Stuck} ∪ Fault ` (-F))] ==> ?Prop r e" assume Z_r: "(Z, r) ∈ {(Z, r). Z ∈ b ∧ Γ⊨⟨c,Normal Z⟩ → Normal r}" with WhileNoFault have "Γ⊨⟨While b c,Normal r⟩ →∉({Stuck} ∪ Fault ` (-F))" by (auto simp add: final_notin_def intro: exec.intros) from hyp [OF e_in_b this] obtain cNoFault: "Γ⊨⟨c,Normal e⟩ →∉({Stuck} ∪ Fault ` (-F))" and Abrupt_r: "∀u. Γ⊨⟨c,Normal e⟩ → Abrupt u ⟶ Γ⊨⟨While b c,Normal r⟩ → Abrupt u" by simp { fix u assume "Γ⊨⟨c,Normal e⟩ → Abrupt u" with Abrupt_r have "Γ⊨⟨While b c,Normal r⟩ → Abrupt u" by simp moreover from Z_r obtain "Z ∈ b" "Γ⊨⟨c,Normal Z⟩ → Normal r" by simp ultimately have "Γ⊨⟨While b c,Normal Z⟩ → Abrupt u" by (blast intro: exec.intros) } with cNoFault show "?Prop Z e" by iprover qed } with P show "s ∈ ?P' s" by blast next { fix t assume "termination": "t ∉ b" assume "(Z, t) ∈ ?unroll" hence "Γ⊨⟨While b c,Normal Z⟩ → Normal t" proof (induct rule: converse_rtrancl_induct [consumes 1]) from "termination" show "Γ⊨⟨While b c,Normal t⟩ → Normal t" by (blast intro: exec.WhileFalse) next fix Z r assume first_body: "(Z, r) ∈ {(s, t). s ∈ b ∧ Γ⊨⟨c,Normal s⟩ → Normal t}" assume "(r, t) ∈ ?unroll" assume rest_loop: "Γ⊨⟨While b c, Normal r⟩ → Normal t" show "Γ⊨⟨While b c,Normal Z⟩ → Normal t" proof - from first_body obtain "Z ∈ b" "Γ⊨⟨c,Normal Z⟩ → Normal r" by fast moreover from rest_loop have "Γ⊨⟨While b c,Normal r⟩ → Normal t" by fast ultimately show "Γ⊨⟨While b c,Normal Z⟩ → Normal t" by (rule exec.WhileTrue) qed qed } with P show "(∀t. t∈(?P' s ∩ - b) ⟶t∈{t. Γ⊨⟨While b c,Normal Z⟩ → Normal t})" by blast next from P show "∀t. t∈?A s ⟶ t∈?A Z" by simp qed qed next case (Call p) from noStuck_Call have "∀s ∈ {s. s=Z ∧ Γ⊨⟨Call p,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓ Normal s}. p ∈ dom Γ" by (fastforce simp add: final_notin_def) then show ?case proof (rule conseq_extract_state_indep_prop) assume p_defined: "p ∈ dom Γ" with MGT_Calls show "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨Call p ,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F))∧ Γ⊨Call p↓Normal s} (Call p) {t. Γ⊨⟨Call p,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Call p,Normal Z⟩ → Abrupt t}" by (auto) qed next case (DynCom c) have hyp: "∧s'. ∀Z. Γ,Θ⊨tF {s. s = Z ∧ Γ⊨⟨c s',Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c s'↓Normal s} c s' {t. Γ⊨⟨c s',Normal Z⟩ → Normal t},{t. Γ⊨⟨c s',Normal Z⟩ → Abrupt t}" using DynCom by simp have hyp': "Γ,Θ⊨tF {s. s = Z ∧ Γ⊨⟨DynCom c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨DynCom c↓Normal s} (c Z) {t. Γ⊨⟨DynCom c,Normal Z⟩ → Normal t},{t. Γ⊨⟨DynCom c,Normal Z⟩ → Abrupt t}" by (rule ConseqMGT [OF hyp]) (fastforce simp add: final_notin_def intro: exec.intros elim: terminates_Normal_elim_cases) show "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨DynCom c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨DynCom c↓Normal s} DynCom c {t. Γ⊨⟨DynCom c,Normal Z⟩ → Normal t}, {t. Γ⊨⟨DynCom c,Normal Z⟩ → Abrupt t}" apply (rule hoaret.DynCom) apply (clarsimp) apply (rule hyp' [simplified]) done next case (Guard f g c) have hyp_c: "∀Z. Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c↓Normal s} c {t. Γ⊨⟨c,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}" using Guard by iprover show "Γ,Θ⊨tF {s. s = Z ∧ Γ⊨⟨Guard f g c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Guard f g c↓ Normal s} Guard f g c {t. Γ⊨⟨Guard f g c ,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Guard f g c,Normal Z⟩ → Abrupt t}" proof (cases "f ∈ F") case True from hyp_c have "Γ,Θ⊨tF (g ∩ {s. s=Z ∧ Γ⊨⟨Guard f g c,Normal s⟩ →∉({Stuck}∪ Fault ` (-F))∧ Γ⊨Guard f g c↓ Normal s}) c {t. Γ⊨⟨Guard f g c,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Guard f g c,Normal Z⟩ → Abrupt t}" apply (rule ConseqMGT) apply (insert True) apply (auto simp add: final_notin_def intro: exec.intros elim: terminates_Normal_elim_cases) done from True this show ?thesis by (rule conseqPre [OF Guarantee]) auto next case False from hyp_c have "Γ,Θ⊨tF (g ∩ {s. s ∈ g ∧ s=Z ∧ Γ⊨⟨Guard f g c,Normal s⟩ →∉({Stuck}∪ Fault ` (-F))∧ Γ⊨Guard f g c↓ Normal s} ) c {t. Γ⊨⟨Guard f g c,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Guard f g c,Normal Z⟩ → Abrupt t}" apply (rule ConseqMGT) apply clarify apply (frule Guard_noFaultStuckD [OF _ False]) apply (auto simp add: final_notin_def intro: exec.intros elim: terminates_Normal_elim_cases) done then show ?thesis apply (rule conseqPre [OF hoaret.Guard]) apply clarify apply (frule Guard_noFaultStuckD [OF _ False]) apply auto done qed next case Throw show "Γ,Θ⊨tF {s. s = Z ∧ Γ⊨⟨Throw,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Throw ↓ Normal s} Throw {t. Γ⊨⟨Throw,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Throw,Normal Z⟩ → Abrupt t}" by (rule conseqPre [OF hoaret.Throw]) (blast intro: exec.intros terminates.intros) next case (Catch c1 c2) have "∀Z. Γ,Θ⊨tF {s. s = Z ∧ Γ⊨⟨c1,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c1 ↓ Normal s} c1 {t. Γ⊨⟨c1,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c1,Normal Z⟩ → Abrupt t}" using Catch.hyps by iprover hence "Γ,Θ⊨tF {s. s = Z ∧ Γ⊨⟨Catch c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Catch c1 c2 ↓ Normal s} c1 {t. Γ⊨⟨Catch c1 c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c1,Normal Z⟩ → Abrupt t ∧ Γ⊨c2 ↓ Normal t ∧ Γ⊨⟨c2,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F))}" by (rule ConseqMGT) (fastforce intro: exec.intros terminates.intros elim: terminates_Normal_elim_cases simp add: final_notin_def) moreover have "∀Z. Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨c2 ↓ Normal s} c2 {t. Γ⊨⟨c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c2,Normal Z⟩ → Abrupt t}" using Catch.hyps by iprover hence "Γ,Θ⊨tF {s. Γ⊨⟨c1,Normal Z⟩ →Abrupt s ∧ Γ⊨c2 ↓ Normal s ∧ Γ⊨⟨c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F))} c2 {t. Γ⊨⟨Catch c1 c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Catch c1 c2,Normal Z⟩ → Abrupt t}" by (rule ConseqMGT) (fastforce intro: exec.intros terminates.intros simp add: noFault_def') ultimately show "Γ,Θ⊨tF {s. s = Z ∧ Γ⊨⟨Catch c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Catch c1 c2 ↓ Normal s} Catch c1 c2 {t. Γ⊨⟨Catch c1 c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Catch c1 c2,Normal Z⟩ → Abrupt t}" by (rule hoaret.Catch ) qed lemma Call_lemma': assumes Call_hyp: "∀q∈dom Γ. ∀Z. Γ,Θ⊨tF{s. s=Z ∧ Γ⊨⟨Call q,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ} (Call q) {t. Γ⊨⟨Call q,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Call q,Normal Z⟩ → Abrupt t}" shows "∧Z. Γ,Θ ⊨tF {s. s=Z ∧ Γ⊨⟨c,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓Normal σ ∧ (∃c'. Γ⊨(Call p,Normal σ) →+ (c',Normal s) ∧ c ∈ redexes c')} c {t. Γ⊨⟨c,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c,Normal Z⟩ → Abrupt t}" proof (induct c) case Skip show "Γ,Θ⊨tF {s. s = Z ∧ Γ⊨⟨Skip,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p ↓ Normal σ ∧ (∃c'. Γ⊨(Call p,Normal σ) →+ (c',Normal s) ∧ Skip ∈ redexes c')} Skip {t. Γ⊨⟨Skip,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Skip,Normal Z⟩ → Abrupt t}" by (rule hoaret.Skip [THEN conseqPre]) (blast intro: exec.Skip) next case (Basic f) show "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨Basic f,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓Normal σ ∧ (∃c'. Γ⊨(Call p,Normal σ) →+ (c',Normal s) ∧ Basic f ∈ redexes c')} Basic f {t. Γ⊨⟨Basic f,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Basic f,Normal Z⟩ → Abrupt t}" by (rule hoaret.Basic [THEN conseqPre]) (blast intro: exec.Basic) next case (Spec r) show "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨Spec r,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓Normal σ ∧ (∃c'. Γ⊨(Call p,Normal σ) →+ (c',Normal s) ∧ Spec r ∈ redexes c')} Spec r {t. Γ⊨⟨Spec r,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Spec r,Normal Z⟩ → Abrupt t}" apply (rule hoaret.Spec [THEN conseqPre]) apply (clarsimp) apply (case_tac "∃t. (Z,t) ∈ r") apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros) done next case (Seq c1 c2) have hyp_c1: "∀Z. Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨c1,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓Normal σ ∧ (∃c'. Γ⊨(Call p,Normal σ) →+ (c',Normal s) ∧ c1 ∈ redexes c')} c1 {t. Γ⊨⟨c1,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c1,Normal Z⟩ → Abrupt t}" using Seq.hyps by iprover have hyp_c2: "∀Z. Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓Normal σ ∧ (∃c'. Γ⊨(Call p,Normal σ) →+ (c',Normal s) ∧ c2 ∈ redexes c')} c2 {t. Γ⊨⟨c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c2,Normal Z⟩ → Abrupt t}" using Seq.hyps (2) by iprover have c1: "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨Seq c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓Normal σ ∧ (∃c'. Γ⊨(Call p,Normal σ) →+ (c',Normal s) ∧ Seq c1 c2 ∈ redexes c')} c1 {t. Γ⊨⟨c1,Normal Z⟩ → Normal t ∧ Γ⊨⟨c2,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓Normal σ ∧ (∃c'. Γ⊨(Call p,Normal σ) →+ (c',Normal t) ∧ c2 ∈ redexes c')}, {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t}" proof (rule ConseqMGT [OF hyp_c1],clarify,safe) assume "Γ⊨⟨Seq c1 c2,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))" thus "Γ⊨⟨c1,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))" by (blast dest: Seq_NoFaultStuckD1) next fix c' assume steps_c': "Γ⊨ (Call p, Normal σ) →+ (c', Normal Z)" assume red: "Seq c1 c2 ∈ redexes c'" from redexes_subset [OF red] steps_c' show "∃c'. Γ⊨ (Call p, Normal σ) →+ (c', Normal Z) ∧ c1 ∈ redexes c'" by (auto iff: root_in_redexes) next fix t assume "Γ⊨⟨Seq c1 c2,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))" "Γ⊨⟨c1,Normal Z⟩ → Normal t" thus "Γ⊨⟨c2,Normal t⟩ →∉({Stuck} ∪ Fault ` (-F))" by (blast dest: Seq_NoFaultStuckD2) next fix c' t assume steps_c': "Γ⊨ (Call p, Normal σ) →+ (c', Normal Z)" assume red: "Seq c1 c2 ∈ redexes c'" assume exec_c1: "Γ⊨ ⟨c1,Normal Z⟩ → Normal t" show "∃c'. Γ⊨ (Call p, Normal σ) →+ (c', Normal t) ∧ c2 ∈ redexes c'" proof - note steps_c' also from exec_impl_steps_Normal [OF exec_c1] have "Γ⊨ (c1, Normal Z) →* (Skip, Normal t)". from steps_redexes_Seq [OF this red] obtain c'' where steps_c'': "Γ⊨ (c', Normal Z) →* (c'', Normal t)" and Skip: "Seq Skip c2 ∈ redexes c''" by blast note steps_c'' also have step_Skip: "Γ⊨ (Seq Skip c2,Normal t) → (c2,Normal t)" by (rule step.SeqSkip) from step_redexes [OF step_Skip Skip] obtain c''' where step_c''': "Γ⊨ (c'', Normal t) → (c''', Normal t)" and c2: "c2 ∈ redexes c'''" by blast note step_c''' finally show ?thesis using c2 by blast qed next fix t assume "Γ⊨⟨c1,Normal Z⟩ → Abrupt t" thus "Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t" by (blast intro: exec.intros) qed show "Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨Seq c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓Normal σ ∧ (∃c'. Γ⊨(Call p,Normal σ) →+ (c',Normal s) ∧ Seq c1 c2 ∈ redexes c')} Seq c1 c2 {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Seq c1 c2,Normal Z⟩ → Abrupt t}" by (rule hoaret.Seq [OF c1 ConseqMGT [OF hyp_c2]]) (blast intro: exec.intros) next case (Cond b c1 c2) have hyp_c1: "∀Z. Γ,Θ⊨tF {s. s=Z ∧ Γ⊨⟨c1,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓Normal σ ∧ (∃c'. Γ⊨(Call p,Normal σ) →+ (c',Normal s) ∧ c1 ∈ redexes c')} c1 {t. Γ⊨⟨c1,Normal Z⟩ → Normal t}, {t. Γ⊨⟨c1,Normal Z⟩ → Abrupt t}" using Cond.hyps by iprover have "Γ,Θ⊨tF ({s. s=Z ∧ Γ⊨⟨Cond b c1 c2,Normal s⟩ →∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊨Call p↓Normal σ ∧ (∃c'. Γ⊨(Call p,Normal σ) →+ (c',Normal s) ∧ Cond b c1 c2 ∈ redexes c')} ∩ b) c1 {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t}, {t. Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t}" proof (rule ConseqMGT [OF hyp_c1],safe) assume "Z ∈ b" "Γ⊨⟨Cond b c1 c2,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))" thus "Γ⊨⟨c1,Normal Z⟩ →∉({Stuck} ∪ Fault ` (-F))" by (auto simp add: final_notin_def intro: exec.CondTrue) next fix c' assume b: "Z ∈ b" assume steps_c': "Γ⊨ (Call p, Normal σ) →+ (c', Normal Z)" assume redex_c': "Cond b c1 c2 ∈ redexes c'" show "∃c'. Γ⊨ (Call p, Normal σ) →+ (c', Normal Z) ∧ c1 ∈ redexes c'" proof - note steps_c' also from b have "Γ⊨(Cond b c1 c2, Normal Z) → (c1, Normal Z)" by (rule step.CondTrue) from step_redexes [OF this redex_c'] obtain c'' where step_c'': "Γ⊨ (c', Normal Z) → (c'', Normal Z)" and c1: "c1 ∈ redexes c''" by blast note step_c'' finally show ?thesis using c1 by blast qed next fix t assume "Z ∈ b" "Γ⊨⟨c1,Normal Z⟩ → Normal t" thus "Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Normal t" by (blast intro: exec.CondTrue) next fix t assume "Z ∈ b" "Γ⊨⟨c1,Normal Z⟩ → Abrupt t" thus "Γ⊨⟨Cond b c1 c2,Normal Z⟩ → Abrupt t" by (blast intro: exec.CondTrue) qed moreover have hyp_c2: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\< \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c2 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" using Cond.hyps by iprover have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Co \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal s) \<and> Cond b c1 c2 \<in> redexes c')} \<inter> -b) c2 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" proof (rule ConseqMGT [OF hyp_c2],safe) assume "Z \<notin> b" "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow>\<noti thus "\<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Faul by (auto simp add: final_notin_def intro: exec.CondFalse) next fix c' assume b: "Z \<notin> b" assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z assume redex_c': "Cond b c1 c2 \<in> redexes c'" show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) proof - note steps_c' also from b have "\<Gamma>\<turnstile>(Cond b c1 c2, Normal Z) \<rightarrow> (c2, Normal Z)" by (rule step.CondFalse) from step_redexes [OF this redex_c'] obtain c'' where step_c'': "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)" and c1: "c2 \<in> redexes c''" by blast note step_c'' finally show ?thesis using c1 by blast qed next fix t assume "Z \<notin> b" "\<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t" thus "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t" by (blast intro: exec.CondFalse) next fix t assume "Z \<notin> b" "\<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t" thus "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t" by (blast intro: exec.CondFalse) qed ultimately show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Con \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Cond b c1 c2 \<in> redexes c')} (Cond b c1 c2) {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by (rule hoaret.Cond) next case (While b c) let ?unroll = "({(s,t). s\<in>b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> N let ?P' = "\<lambda>Z. {t. (Z,t)\<in>?unroll \<and> (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \< (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarr \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> While b c \<in> redexes c')}" let ?A = "\<lambda>Z. {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrup let ?r = "{(t,s). \<Gamma>\<turnstile>(While b c)\<down>Normal s \<and> s\<in>b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t}" show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>)\<rightarrow>\<^sup>+(c',Normal s) \<and> (While b c) {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" proof (rule ConseqMGT [where ?P'="\<lambda> Z. ?P' Z" and ?Q'="\<lambda> Z. ?P' Z \<inter> - b"]) have wf_r: "wf ?r" by (rule wf_terminates_while) show "\<forall> Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (?P' Z) (While b c) (?P' Z \<in proof (rule allI, rule hoaret.While [OF wf_r]) fix Z from While have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by iprover show "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> ?P' ({t. (t, \<sigma>) \<in> ?r} \<inter> ?P' Z),(?A Z)" proof (rule allI, rule ConseqMGT [OF hyp_c]) fix \<tau> s assume asm: "s\<in> {\<tau>} \<inter> {t. (Z, t) \<in> ?unroll \<and> (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \< (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarr \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> \<Gamma>\<turnstile>Call p\<down> Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> While b c \<in> redexes c')} \<inter> b" then obtain c' where s_eq_\<tau>: "s=\<tau>" and Z_s_unroll: "(Z,s) \<in> ?unroll" and noabort:"\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \< (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarr \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" and termi: "\<Gamma>\<turnstile>Call p \<down> Normal \<sigma>" and reach: "\<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s)" and red_c': "While b c \<in> redexes c'" and s_in_b: "s\<in>b" by blast obtain c'' where reach_c: "\<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c'',Normal s)" "Seq c (While b c) \<in> redexes c''" proof - note reach also from s_in_b have "\<Gamma>\<turnstile>(While b c,Normal s) \<rightarrow> (Seq c (While b c),Normal s)" by (rule step.WhileTrue) from step_redexes [OF this red_c'] obtain c'' where step: "\<Gamma>\<turnstile> (c', Normal s) \<rightarrow> (c'', Normal s)" and red_c'': "Seq c (While b c) \<in> redexes c''" by blast note step finally show ?thesis using red_c'' by (blast intro: that) qed from reach termi have "\<Gamma>\<turnstile>c' \<down> Normal s" by (rule steps_preserves_termination') from redexes_preserves_termination [OF this red_c'] have termi_while: "\<Gamma>\<turnstile>While b c \<down> Normal s" . show "s \<in> {t. t = s \<and> \<Gamma>\<turnstile>\<langle>c,Normal t\<rangle> \<Rightarrow>\<notin>({Stu \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t} \<long t \<in> {t. (t,\<tau>) \<in> ?r} \<inter> {t. (Z, t) \<in> ?unroll \<and> (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \< (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarr \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> While b c \<in> redexes c')}) \<and> (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t} \<long t \<in> {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t})" (is "?C1 \<and> ?C2 \<and> ?C3") proof (intro conjI) from Z_s_unroll noabort s_in_b termi reach_c show ?C1 apply clarsimp apply (drule redexes_subset) apply simp apply (blast intro: root_in_redexes) done next { fix t assume s_t: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t" with s_eq_\<tau> termi_while s_in_b have "(t,\<tau>) \<in> ?r" by blast moreover from Z_s_unroll s_t s_in_b have "(Z, t) \<in> ?unroll" by (blast intro: rtrancl_into_rtrancl) moreover obtain c'' where reach_c'': "\<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c'',Normal t)" "(While b c) \<in> redexes c''" proof - note reach_c (1) also from s_in_b have "\<Gamma>\<turnstile>(While b c,Normal s)\<rightarrow> (Seq c (While b c),Normal s)" by (rule step.WhileTrue) have "\<Gamma>\<turnstile> (Seq c (While b c), Normal s) \<rightarrow>\<^sup>+ (While b c, Normal t)" proof - from exec_impl_steps_Normal [OF s_t] have "\<Gamma>\<turnstile> (c, Normal s) \<rightarrow>\<^sup>* (Skip, Normal t)". hence "\<Gamma>\<turnstile> (Seq c (While b c), Normal s) \<rightarrow>\<^sup>* (Seq Skip (While b c), Normal t)" by (rule SeqSteps) auto moreover have "\<Gamma>\<turnstile>(Seq Skip (While b c), Normal t)\<rightarrow>(While b c, Normal t)" by (rule step.SeqSkip) ultimately show ?thesis by (rule rtranclp_into_tranclp1) qed from steps_redexes' [OF this reach_c (2)] obtain c''' where step: "\<Gamma>\<turnstile> (c'', Normal s) \<rightarrow>\<^sup>+ (c''', Normal t)" and red_c'': "While b c \<in> redexes c'''" by blast note step finally show ?thesis using red_c'' by (blast intro: that) qed moreover note noabort termi ultimately have "(t,\<tau>) \<in> ?r \<and> (Z, t) \<in> ?unroll \<and> (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \< (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarr \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal t) \<and> While b c \<in> redexes c')" by iprover } then show ?C2 by blast next { fix t assume s_t: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t" from Z_s_unroll noabort s_t s_in_b have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t" by blast } thus ?C3 by simp qed qed qed next fix s assume P: "s \<in> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\< \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> While b c \<in> redexes c')}" hence WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<noti by auto show "s \<in> ?P' s \<and> (\<forall>t. t\<in>(?P' s \<inter> - b)\<longrightarrow> t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t})\<and> (\<forall>t. t\<in>?A s \<longrightarrow> t\<in>?A Z)" proof (intro conjI) { fix e assume "(Z,e) \<in> ?unroll" "e \<in> b" from this WhileNoFault have \Gamma\<><cNormal \rangle>(-F)) \<and java.lang.StringIndexOutOfBoundsException: Range [32, 30) out of bounds for leng \ irule [1]) assume:" < java.lang.StringIndexOutOfBoundsException: Index 36 out of bounds for le java.lang.StringIndexOutOfBoundsException: Range [32, 29) out of bounds for leng WhileNoFault have cNoFault: "\<Gamma>\< * comes first; so if l->k compares equalto r-> then l-> is older by:intro:exec.) moreover java.lang.StringIndexOutOfBoundsException: Index 11 out of bounds for length 11 u "Gamma>\<turnstile\langle>,ormal e\rangle>\Rightarrow> Abruptujava.lang.StringIndexOut "\turnstile><java.lang.StringIndexOutOfBoundsException: Range [59, 58) out of boun java.lang.StringIndexOutOfBoundsException: Range [24, 23) out of bounds for leng java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0 ultimately show "?Prop e e" by iprover assume e_in_b: "e\ java.lang.StringIndexOutOfBoundsException: Range [13, 12) out of java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0 assume hyp: "\<lbrakk>e\<in>b;\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> \<Longrightarrow> ?Prop r e" assume Z_r: "(Z, r) \<in> {(Z, r). Z \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Norma with WhileNoFault have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<unio by (auto simp add: final_notin_def intro: exec.intros) from hyp [OF e_in_b this] obtain cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Abrupt_r: "\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u \<lon \<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u" by simp { fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u" with Abrupt_r have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u moreover from Z_r obtain "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r" by simp ultimately have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u" by (blast intro: exec.intros) } with cNoFault show "?Prop Z e" by iprover qed } with P show "s \<in> ?P' s" by blast next { fix t assume "termination": "t \<notin> b" assume "(Z, t) \<in> ?unroll" hence "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" proof (induct rule: converse_rtrancl_induct [consumes 1]) from "termination" show "\<Gamma>\<turnstile>\<langle>While b c,Normal t\<rangle> \<Rightarrow> Normal t" by (blast intro: exec.WhileFalse) next fix Z r assume first_body: "(Z, r) \<in> {(s, t). s \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Norma assume "(r, t) \<in> ?unroll" assume rest_loop: "\<Gamma>\<turnstile>\<langle>While b c, Normal r\<rangle> \<Rightarrow> Normal t show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" proof - from first_body obtain "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r" by fast moreover from rest_loop have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Normal t" by fast ultimately show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" by (rule exec.WhileTrue) qed qed } with P show "\<forall>t. t\<in>(?P' s \<inter> - b) \<longrightarrow>t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> No by blast next from P show "\<forall>t. t\<in>?A s \<longrightarrow> t\<in>?A Z" by simp qed qed next case (Call q) let ?P = "{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q ,Normal s\<rangle> \<Rightarrow>\<notin>({S \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> from noStuck_Call have "\<forall>s \<in> ?P. q \<in> dom \<Gamma>" by (fastforce simp add: final_notin_def) then show ?case proof (rule conseq_extract_state_indep_prop) assume q_defined: "q \<in> dom \<Gamma>" from Call_hyp have "\<forall>q\<in>dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma> (Call q) {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by (simp add: exec_Call_body' noFaultStuck_Call_body' [simplified] terminates_Normal_Call_body) from Call_hyp q_defined have Call_hyp': "\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\< \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma> (Call q) {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by auto show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ?P (Call q) {t. \<Gamma>\<turnstile>\<langle>Call q ,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Call q ,Normal Z\<rangle> \<Rightarrow> Abrupt t}" proof (rule ConseqMGT [OF Call_hyp'],safe) fix c' assume termi: "\<Gamma>\<turnstile>Call p \<down> Normal \<sigma>" assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z assume red_c': "Call q \<in> redexes c'" show "\<Gamma>\<turnstile>Call q \<down> Normal Z" proof - from steps_preserves_termination' [OF steps_c' termi] have "\<Gamma>\<turnstile>c' \<down> Normal Z" . from redexes_preserves_termination [OF this red_c'] show ?thesis . qed next fix c' assume termi: "\<Gamma>\<turnstile>Call p \<down> Normal \<sigma>" assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z assume red_c': "Call q \<in> redexes c'" from redex_redexes [OF this] have "redex c' = Call q" by auto with termi steps_c' show "((Z, q), \<sigma>, p) \<in> termi_call_steps \<Gamma>" by (auto simp add: termi_call_steps_def) qed qed next case (DynCom c) have hyp: "\<And>s'. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c s',Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<uni \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> (c s') {t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnst using DynCom by simp have hyp': "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Dyn \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> (c Z) {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<tu proof (rule ConseqMGT [OF hyp],safe) assume "\<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<un then show "\<Gamma>\<turnstile>\<langle>c Z,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> by (fastforce simp add: final_notin_def intro: exec.intros) next fix c' assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" assume c': "DynCom c \<in> redexes c'" have "\<Gamma>\<turnstile> (DynCom c, Normal Z) \<rightarrow> (c Z,Normal Z)" by (rule step.DynCom) from step_redexes [OF this c'] obtain c'' where step: "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)" and c'': "c Z \<in> redexes c by blast note steps also note step finally show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', N using c'' by blast next fix t assume "\<Gamma>\<turnstile>\<langle>c Z,Normal Z\<rangle> \<Rightarrow> Normal t" thus "\<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t" by (auto intro: exec.intros) next fix t assume "\<Gamma>\<turnstile>\<langle>c Z,Normal Z\<rangle> \<Rightarrow> Abrupt t" thus "\<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t" by (auto intro: exec.intros) qed show ?case apply (rule hoaret.DynCom) apply safe apply (rule hyp') done next case (Guard f g c) have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" using Guard.hyps by iprover show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langl \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Guard f g c {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t}" proof (cases "f \<in> F") case True have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fau \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Guard f g c \<in> redexes c')}) c {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t}" proof (rule ConseqMGT [OF hyp_c], safe) assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<u thus "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault by (auto simp add: final_notin_def intro: exec.intros) next fix c' assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" assume c': "Guard f g c \<in> redexes c'" assume "Z \<in> g" from this have "\<Gamma>\<turnstile>(Guard f g c,Normal Z) \<rightarrow> (c,Normal Z)" by (rule step.Guard) from step_redexes [OF this c'] obtain c'' where step: "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)" and c'': "c \<in> redexes c' by blast note steps also note step finally show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', N using c'' by blast next fix t assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<u "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t" "Z \<in> g" thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t" by (auto simp add: final_notin_def intro: exec.intros ) next fix t assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<u "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t" "Z \<in> g" thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t" by (auto simp add: final_notin_def intro: exec.intros ) qed from True this show ?thesis by (rule conseqPre [OF Guarantee]) auto next case False have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fau \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Guard f g c \<in> redexes c')}) c {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t}" proof (rule ConseqMGT [OF hyp_c], safe) assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<u thus "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault using False by (cases "Z\<in> g") (auto simp add: final_notin_def intro: exec.intros) next fix c' assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" assume c': "Guard f g c \<in> redexes c'" assume "Z \<in> g" from this have "\<Gamma>\<turnstile>(Guard f g c,Normal Z) \<rightarrow> (c,Normal Z)" by (rule step.Guard) from step_redexes [OF this c'] obtain c'' where step: "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)" and c'': "c \<in> redexes c' by blast note steps also note step finally show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', N using c'' by blast next fix t assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<u "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t" thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t" using False by (cases "Z\<in> g") (auto simp add: final_notin_def intro: exec.intros ) next fix t assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<u "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t" thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t" using False by (cases "Z\<in> g") (auto simp add: final_notin_def intro: exec.intros ) qed then show ?thesis apply (rule conseqPre [OF hoaret.Guard]) apply clarify apply (frule Guard_noFaultStuckD [OF _ False]) apply auto done qed next case Throw show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langl \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Throw {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by (rule conseqPre [OF hoaret.Throw]) (blast intro: exec.intros terminates.intros) next case (Catch c\<^sub>1 c\<^sub>2) have hyp_c1: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s= Z \<and> \<Gamma>\<turnstile>\< \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c\<^sub>1 \<in> redexes c')} c\<^sub>1 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<tu using Catch.hyps by iprover have hyp_c2: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s= Z \<and> \<Gamma>\<turnstile>\< \<Gamma>\<turnstile>Call p\<down> Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c\<^sub>2 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<tu using Catch.hyps by iprover have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Cat \<Gamma>\<turnstile>Call p\<down> Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>)\<rightarrow>\<^sup>+(c',Normal s) \<and> Catch c\<^sub>1 c\<^sub>2 \<in> redexes c')} c\<^sub>1 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Faul (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> proof (rule ConseqMGT [OF hyp_c1],clarify,safe) assume "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow>\<noti thus "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<unio by (fastforce simp add: final_notin_def intro: exec.intros) next fix c' assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" assume c': "Catch c\<^sub>1 c\<^sub>2 \<in> redexes c'" from steps redexes_subset [OF this] show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) by (auto iff: root_in_redexes) next fix t assume "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Normal t" thus "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t by (auto intro: exec.intros) next fix t assume "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow>\<noti "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t" thus "\<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<unio by (auto simp add: final_notin_def intro: exec.intros) next fix c' t assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z assume red: "Catch c\<^sub>1 c\<^sub>2 \<in> redexes c'" assume exec_c\<^sub>1: "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abru show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal t) proof - note steps_c' also from exec_impl_steps_Normal_Abrupt [OF exec_c\<^sub>1] have "\<Gamma>\<turnstile> (c\<^sub>1, Normal Z) \<rightarrow>\<^sup>* (Throw, Normal t)". from steps_redexes_Catch [OF this red] obtain c'' where steps_c'': "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow>\<^sup>* (c'', Normal t)" and Catch: "Catch Throw c\<^sub>2 \<in> redexes c''" by blast note steps_c'' also have step_Catch: "\<Gamma>\<turnstile> (Catch Throw c\<^sub>2,Normal t) \<rightarrow> (c\<^sub>2,N by (rule step.CatchThrow) from step_redexes [OF step_Catch Catch] obtain c''' where step_c''': "\<Gamma>\<turnstile> (c'', Normal t) \<rightarrow> (c''', Normal t)" and c2: "c\<^sub>2 \<in> redexes c'''" by blast note step_c''' finally show ?thesis using c2 by blast qed qed moreover have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {t. \<Gamma>\<turnstile>\<langle>c\<^sub> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Faul \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> c\<^sub>2 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by (rule ConseqMGT [OF hyp_c2]) (fastforce intro: exec.intros) ultimately show ?case by (rule hoaret.Catch) qed text \<open>To prove a procedure implementation correct it suffices to assume only the procedure specifications of procedures that actually occur during evaluation of the body. \<close> lemma Call_lemma: assumes A: "\<forall>q \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<u \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma> (Call q) {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}" assumes pdef: "p \<in> dom \<Gamma>" shows "\<And>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> {s. s=Z \<and>\<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal s\<rangle> \<Righ \<Gamma>\<turnstile>the (\<Gamma> p)\<down>Normal s}) the (\<Gamma> p) {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}" apply (rule conseqPre) apply (rule Call_lemma' [OF A]) using pdef apply (fastforce intro: terminates.intros tranclp.r_into_trancl [of "(step \<Gamma>)", OF s done lemma Call_lemma_switch_Call_body: assumes call: "\<forall>q \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<u \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma> (Call q) {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}" assumes p_defined: "p \<in> dom \<Gamma>" shows "\<And>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\< \<Gamma>\<turnstile>Call p\<down>Normal s}) the (\<Gamma> p) {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" apply (simp only: exec_Call_body' [OF p_defined] noFaultStuck_Call_body' [OF p_defined] t apply (rule conseqPre) apply (rule Call_lemma') apply (rule call) using p_defined apply (fastforce intro: terminates.intros tranclp.r_into_trancl [of "(step \<Gamma>)", OF s root_in_redexes) done lemma MGT_Call: "\<forall>p \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call \<Gamma>\<turnstile>(Call p)\<down>Normal s} (Call p) {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" apply (intro ballI allI) apply (rule CallRec' [where Procs="dom \<Gamma>" and P="\<lambda>p Z. {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<no \<Gamma>\<turnstile>Call p\<down>Normal s}" and Q="\<lambda>p Z. {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}" a A="\<lambda>p Z. {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" a r="termi_call_steps \<Gamma>" ]) apply simp apply simp apply (rule wf_termi_call_steps) apply (intro ballI allI) apply simp apply (rule Call_lemma_switch_Call_body [rule_format, simplified]) apply (rule hoaret.Asm) apply fastforce apply assumption done lemma CollInt_iff: "{s. P s} \<inter> {s. Q s} = {s. P s \<and> Q s}" by auto lemma image_Un_conv: "f ` (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {x p Z}) = (\<Union>p\<in>dom \<Gamma>. \< by (auto iff: not_None_eq) text \<open>Another proof of \<open>MGT_Call\<close>, maybe a little more readable\<close> lemma "\<forall>p \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,{} \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,No \<Gamma>\<turnstile>(Call p)\<down>Normal s} (Call p) {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" proof - { fix p Z \<sigma> assume defined: "p \<in> dom \<Gamma>" define Specs where "Specs = (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` \<Gamma>\<turnstile>Call p\<down>Normal s}, p, {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t})})" define Specs_wf where "Specs_wf p \<sigma> = (\<lambda>(P,q,Q,A). (P \<inter> {s. ((s,q),\<sigma>,p) \<in> termi_call_steps \<Gamma>}, q, Q, A)) ` Specs" for p \<sigma> have "\<Gamma>,Specs_wf p \<sigma> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>({\<sigma>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>({S \<Gamma>\<turnstile>the (\<Gamma> p)\<down>Normal s}) (the (\<Gamma> p)) {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}" apply (rule Call_lemma [rule_format, OF _ defined]) apply (rule hoaret.Asm) apply (clarsimp simp add: Specs_wf_def Specs_def image_Un_conv) apply (rule_tac x=q in bexI) apply (rule_tac x=Z in exI) apply (clarsimp simp add: CollInt_iff) apply auto done hence "\<Gamma>,Specs_wf p \<sigma> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>({\<sigma>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<u \<Gamma>\<turnstile>Call p\<down>Normal s}) (the (\<Gamma> p)) {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by (simp only: exec_Call_body' [OF defined] noFaultStuck_Call_body' [OF defined] terminates_Normal_Call_body [OF defined]) } note bdy=this show ?thesis apply (intro ballI allI) apply (rule hoaret.CallRec [where Specs="(\<Union>p\<in>dom \<Gamma>. \<Union>Z. {({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` \<Gamma>\<turnstile>Call p\<down>Normal s}, p, {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t})})", OF _ wf_termi_call_steps [of \<Gamma>] refl]) apply fastforce apply clarify apply (rule conjI) apply fastforce apply (rule allI) apply (simp (no_asm_use) only : Un_empty_left) apply (rule bdy) apply auto done qed theorem hoaret_complete: "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> by (iprover intro: MGT_implies_complete MGT_lemma [OF MGT_Call]) lemma hoaret_complete': assumes cvalid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" proof (cases "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A") case True hence "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" by (rule hoaret_complete) thus "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" by (rule hoaret_augment_context) simp next case False with cvalid show ?thesis by (rule ExFalso) qed subsection \<open>And Now: Some Useful Rules\<close> subsubsection \<open>Modify Return\<close> lemma Proc_exnModifyReturn_sound: assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P call_exn init p retu assumes valid_modif: "\<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call p) (Modif \<sig assumes res_modif: "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t" assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> result_exn (return' s t) t = result_exn (r shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return result_exn proof (rule cvalidtI) fix s t assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" by (auto simp add: validt_def) then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call by (auto intro: valid_augment_Faults) assume exec: "\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> assume P: "s \<in> P" assume t_notin_F: "t \<notin> Fault ` F" from exec show "t \<in> Normal ` Q \<union> Abrupt ` A" proof (cases rule: exec_call_exn_Normal_elim) fix bdy t' assume bdy: "\<Gamma> p = Some bdy" assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Norma assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t" from exec_body bdy have "\<Gamma>\<turnstile>\<langle>(Call p ),Normal (init s)\<rangle> \<Rightarrow> Normal t'" by (auto simp add: intro: exec.intros) from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P have "t' \<in> Modif (init s)" by auto with res_modif have "Normal (return' s t') = Normal (return s t')" by simp with exec_body exec_c bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c,Normal s\<rangle> \<Right by (auto intro: exec_call_exn) from cvalidt_postD [OF valid_call ctxt this] P t_notin_F show ?thesis by simp next fix bdy t' assume bdy: "\<Gamma> p = Some bdy" assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrup assume t: "t = Abrupt (result_exn (return s t') t')" also from exec_body bdy have "\<Gamma>\<turnstile>\<langle>(Call p),Normal (init s)\<rangle> \<Rightarrow> Abrupt t'" by (auto simp add: intro: exec.intros) from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P have "t' \<in> ModifAbr (init s)" by auto with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return' s t by simp finally have "t = Abrupt (result_exn (return' s t') t')" . with exec_body bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c,Normal s\<rangle> \<Right by (auto intro: exec_call_exnAbrupt) from cvalidt_postD [OF valid_call ctxt this] P t_notin_F show ?thesis by simp next fix bdy f assume bdy: "\<Gamma> p = Some bdy" assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f" and t: "t = Fault f" with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c ,Normal s\<rangl by (auto intro: exec_call_exnFault) from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F show ?thesis by simp next fix bdy assume bdy: "\<Gamma> p = Some bdy" assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck" "t = Stuck" with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c ,Normal s\<rangl by (auto intro: exec_call_exnStuck) from valid_call ctxt this P t_notin_F show ?thesis by (rule cvalidt_postD) next assume "\<Gamma> p = None" "t=Stuck" hence "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c ,Normal s\<rangle> \<Righ by (auto intro: exec_call_exnUndefined) from valid_call ctxt this P t_notin_F show ?thesis by (rule cvalidt_postD) qed next fix s assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" by (auto simp add: validt_def) then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call by (auto intro: valid_augment_Faults) assume P: "s \<in> P" from valid_call ctxt P have call: "\<Gamma>\<turnstile>call_exn init p return' result_exn c\<down> Normal s" by (rule cvalidt_termD) show "\<Gamma>\<turnstile>call_exn init p return result_exn c \<down> Normal s" proof (cases "p \<in> dom \<Gamma>") case True with call obtain bdy where bdy: "\<Gamma> p = Some bdy" and termi_bdy: "\<Gamma>\<turnstile>bdy \<down> Normal (init s)" and termi_c: "\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Norm \<Gamma>\<turnstile>c s t \<down> Normal (return' s t)" by cases auto { fix t assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal hence "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)" proof - from exec_bdy bdy have "\<Gamma>\<turnstile>\<langle>(Call p ),Normal (init s)\<rangle> \<Rightarrow> Normal t" by (auto simp add: intro: exec.intros) from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P res_modif have "return' s t = return s t" by auto with termi_c exec_bdy show ?thesis by auto qed } with bdy termi_bdy show ?thesis by (iprover intro: terminates_call_exn) next case False thus ?thesis by (auto intro: terminates_call_exnUndefined) qed qed lemma ProcModifyReturn_sound: assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P call init p return' c assumes valid_modif: "\<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call p) (Modif \<sig assumes res_modif: "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t" assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t" shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" using valid_call valid_modif res_modif ret_modifAbr unfolding call_call_exn by (rule Proc_exnModifyReturn_sound) lemma Proc_exnModifyReturn: assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return' re assumes res_modif: "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)" assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> (result_exn (return' s t) t) = (result_ex assumes modifies_spec: "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call p) (Modif \<sig shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return result_exn apply (rule hoaret_complete') apply (rule Proc_exnModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr, OF _ _ res_modif ret_modifAbr]) apply (rule hoaret_sound [OF spec]) using modifies_spec apply (blast intro: hoare_sound) done lemma ProcModifyReturn: assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return' c) Q,A" assumes res_modif: "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)" assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> (return' s t) = (return s t)" assumes modifies_spec: "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call p) (Modif \<sig shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" using spec res_modif ret_modifAbr modifies_spec unfolding call_call_exn by (rule Proc_exn lemma Proc_exnModifyReturnSameFaults_sound: assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P call_exn init p retu assumes valid_modif: "\<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),( assumes res_modif: "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t" assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> result_exn (return' s t) t = result_exn (r shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return result_exn proof (rule cvalidtI) fix s t assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" by (auto simp add: validt_def) assume exec: "\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> assume P: "s \<in> P" assume t_notin_F: "t \<notin> Fault ` F" from exec show "t \<in> Normal ` Q \<union> Abrupt ` A" proof (cases rule: exec_call_exn_Normal_elim) fix bdy t' assume bdy: "\<Gamma> p = Some bdy" assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Norma assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t" from exec_body bdy have "\<Gamma>\<turnstile>\<langle>(Call p) ,Normal (init s)\<rangle> \<Rightarrow> Normal t'" by (auto simp add: intro: exec.intros) from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P have "t' \<in> Modif (init s)" by auto with res_modif have "Normal (return' s t') = Normal (return s t')" by simp with exec_body exec_c bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c,Normal s\<rangle> \<Right by (auto intro: exec_call_exn) from cvalidt_postD [OF valid_call ctxt this] P t_notin_F show ?thesis by simp next fix bdy t' assume bdy: "\<Gamma> p = Some bdy" assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrup assume t: "t = Abrupt (result_exn (return s t') t')" also from exec_body bdy have "\<Gamma>\<turnstile>\<langle>Call p ,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'" by (auto simp add: intro: exec.intros) from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P have "t' \<in> ModifAbr (init s)" by auto with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return' s t by simp finally have "t = Abrupt (result_exn (return' s t') t')" . with exec_body bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c,Normal s\<rangle> \<Right by (auto intro: exec_call_exnAbrupt) from cvalidt_postD [OF valid_call ctxt this] P t_notin_F show ?thesis by simp next fix bdy f assume bdy: "\<Gamma> p = Some bdy" assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f" and t: "t = Fault f" with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c ,Normal s\<rangl by (auto intro: exec_call_exnFault) from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F show ?thesis by simp next fix bdy assume bdy: "\<Gamma> p = Some bdy" assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck" "t = Stuck" with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c,Normal s\<rangl by (auto intro: exec_call_exnStuck) from valid_call ctxt this P t_notin_F show ?thesis by (rule cvalidt_postD) next assume "\<Gamma> p = None" "t=Stuck" hence "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c,Normal s\<rangle> \<Righ by (auto intro: exec_call_exnUndefined) from valid_call ctxt this P t_notin_F show ?thesis by (rule cvalidt_postD) qed next fix s assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" by (auto simp add: validt_def) assume P: "s \<in> P" from valid_call ctxt P have call: "\<Gamma>\<turnstile>call_exn init p return' result_exn c\<down> Normal s" by (rule cvalidt_termD) show "\<Gamma>\<turnstile>call_exn init p return result_exn c \<down> Normal s" proof (cases "p \<in> dom \<Gamma>") case True with call obtain bdy where bdy: "\<Gamma> p = Some bdy" and termi_bdy: "\<Gamma>\<turnstile>bdy \<down> Normal (init s)" and termi_c: "\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Norm \<Gamma>\<turnstile>c s t \<down> Normal (return' s t)" by cases auto { fix t assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal hence "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)" proof - from exec_bdy bdy have "\<Gamma>\<turnstile>\<langle>(Call p ),Normal (init s)\<rangle> \<Rightarrow> Normal t" by (auto simp add: intro: exec.intros) from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P res_modif have "return' s t = return s t" by auto with termi_c exec_bdy show ?thesis by auto qed } with bdy termi_bdy show ?thesis by (iprover intro: terminates_call_exn) next case False thus ?thesis by (auto intro: terminates_call_exnUndefined) qed qed lemma ProcModifyReturnSameFaults_sound: assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P call init p return' c assumes valid_modif: "\<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),( assumes res_modif: "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t" assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t" shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" using valid_call valid_modif res_modif ret_modifAbr unfolding call_call_exn by (rule Proc_exnModifyReturnSameFaults_sound) lemma Proc_exnModifyReturnSameFaults: assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return' re assumes res_modif: "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)" assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> result_exn (return' s t) t = result_exn (r assumes modifies_spec: "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call p) (Modif \<sigma>) shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return result_exn apply (rule hoaret_complete') apply (rule Proc_exnModifyReturnSameFaults_sound [where Modif=Modif and ModifAbr=Modif OF _ _ res_modif ret_modifAbr]) apply (rule hoaret_sound [OF spec]) using modifies_spec apply (blast intro: hoare_sound) done lemma ProcModifyReturnSameFaults: assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return' c) Q,A" assumes res_modif: "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)" assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> (return' s t) = (return s t)" assumes modifies_spec: "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call p) (Modif \<sigma>) shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" using spec res_modif ret_modifAbr modifies_spec unfolding call_call_exn by (rule Proc_exnModifyReturnSameFaults) subsubsection \<open>DynCall\<close> lemma dynProc_exnModifyReturn_sound: assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall_exn f g init assumes valid_modif: "\<forall>s\<in>P. \<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Cal assumes ret_modif: "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t" assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> result_exn (retu shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f g init p return resul proof (rule cvalidtI) fix s t assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" by (auto simp add: validt_def) then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call by (auto intro: valid_augment_Faults) assume exec: "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return result_exn c,Normal s\<r assume t_notin_F: "t \<notin> Fault ` F" assume P: "s \<in> P" with valid_modif have valid_modif': "\<forall>\<sigma>. \<Gamma>,\<Theta>\<Turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call (p s)) (Modif \< by blast from exec have "\<Gamma>\<turnstile>\<langle>maybe_guard f g (call_exn init (p s) return result_exn c),Nor by (cases rule: exec_dynCall_exn_Normal_elim) then show "t \<in> Normal ` Q \<union> Abrupt ` A" proof (cases rule: exec_maybe_guard_Normal_elim_cases) case noFault from noFault have guards_ok: "s \<in> g" by simp from noFault have "\<Gamma>\<turnstile> \<langle>call_exn init (p s) return result_exn c,Normal s then show "t \<in> Normal ` Q \<union> Abrupt ` A" proof (cases rule: exec_call_exn_Normal_elim) fix bdy t' assume bdy: "\<Gamma> (p s) = Some bdy" assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Norma assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t" from exec_body bdy have "\<Gamma>\<turnstile>\<langle>Call (p s),Normal (init s)\<rangle> \<Rightarrow> Normal t'" by (auto simp add: intro: exec.Call) from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P have "t' \<in> Modif (init s)" by auto with ret_modif have "Normal (return' s t') = Normal (return s t')" by simp with exec_body exec_c bdy have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c,Normal s\<rangle> \<Ri by (auto intro: exec_call_exn) from exec_maybe_guard_noFault [OF this guards_ok] have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> \< by (simp add: dynCall_exn_def exec_maybe_guard_DynCom) from cvalidt_postD [OF valid_call ctxt this] P t_notin_F show ?thesis by simp next fix bdy t' assume bdy: "\<Gamma> (p s) = Some bdy" assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrup assume t: "t = Abrupt (result_exn (return s t') t')" also from exec_body bdy have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'" by (auto simp add: intro: exec.intros) from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P have "t' \<in> ModifAbr (init s)" by auto with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return' s t by simp finally have "t = Abrupt (result_exn (return' s t') t')" . with exec_body bdy have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c,Normal s\<rangle> \<Ri by (auto intro: exec_call_exnAbrupt) from exec_maybe_guard_noFault [OF this guards_ok] have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> \< by (simp add: dynCall_exn_def exec_maybe_guard_DynCom) from cvalidt_postD [OF valid_call ctxt this] P t_notin_F show ?thesis by simp next fix bdy f' assume bdy: "\<Gamma> (p s) = Some bdy" assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f'" and t: "t = Fault f'" with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c ,Normal s\<ra by (auto intro: exec_call_exnFault) from exec_maybe_guard_noFault [OF this guards_ok] have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> \< by (simp add: dynCall_exn_def exec_maybe_guard_DynCom) from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F show ?thesis by blast next fix bdy assume bdy: "\<Gamma> (p s) = Some bdy" assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck" "t = Stuck" with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c ,Normal s\<ra by (auto intro: exec_call_exnStuck) from exec_maybe_guard_noFault [OF this guards_ok] have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> \< by (simp add: dynCall_exn_def exec_maybe_guard_DynCom) from valid_call ctxt this P t_notin_F show ?thesis by (rule cvalidt_postD) next fix bdy assume "\<Gamma> (p s) = None" "t=Stuck" hence "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c ,Normal s\<rangle> \<R by (auto intro: exec_call_exnUndefined) from exec_maybe_guard_noFault [OF this guards_ok] have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> \< by (simp add: dynCall_exn_def exec_maybe_guard_DynCom) from valid_call ctxt this P t_notin_F show ?thesis by (rule cvalidt_postD) qed next case (someFault) then obtain guards_fail:"s \<notin> g" and t: "t = Fault f" by simp from exec_maybe_guard_Fault [OF guards_fail] t have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> \< by (simp add: dynCall_exn_def exec_guards_DynCom) from cvalidt_postD [OF valid_call ctxt this] P t_notin_F show ?thesis by simp qed next fix s assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" by (auto simp add: validt_def) then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call by (auto intro: valid_augment_Faults) assume P: "s \<in> P" from valid_call ctxt P have "\<Gamma>\<turnstile>dynCall_exn f g init p return' result_exn c\<down> Normal s" by (rule cvalidt_termD) thus "\<Gamma>\<turnstile>dynCall_exn f g init p return result_exn c \<down> Normal s" proof (cases rule: terminates_dynCall_exn_elim) case noFault then obtain guards_ok: "s \<in> g" and call: "\<Gamma>\<turnstile>call_exn init (p s) return' result_exn c\<down> Normal s" by auto have "\<Gamma>⊨call_exn init (p s) return result_exn c ↓ Normal s" proof (cases "p s ∈ dom Γ") case True with call obtain bdy where bdy: "Γ (p s) = Some bdy" and termi_bdy: "Γ⊨bdy ↓ Normal (init s)" and termi_c: "∀t. Γ⊨⟨bdy,Normal (init s)⟩ → Normal t ⟶ Γ⊨c s t ↓ Normal (return' s t)" by cases auto { fix t assume exec_bdy: "Γ⊨⟨bdy,Normal (init s)⟩ → Normal t" hence "Γ⊨c s t ↓ Normal (return s t)" proof - from exec_bdy bdy have "Γ⊨⟨Call (p s),Normal (init s)⟩ → Normal t" by (auto simp add: intro: exec.intros) from cvalidD [OF valid_modif [rule_format, of s "init s"] ctxt' this] P ret_modif have "return' s t = return s t" by auto with termi_c exec_bdy show ?thesis by auto qed } with bdy termi_bdy show ?thesis by (iprover intro: terminates_call_exn) next case False thus ?thesis by (auto intro: terminates_call_exnUndefined) qed thus "Γ⊨dynCall_exn f g init p return result_exn c ↓ Normal s" by (iprover intro: terminates_dynCall_exn) next case (someFault) then have guard_fail: "s ∉ g" by simp thus ?thesis by (simp add: terminates_maybe_guard_Fault dynCall_exn_def) qed qed lemma dynProcModifyReturn_sound: assumes valid_call: "Γ,Θ ⊨tF P dynCall init p return' c Q,A" assumes valid_modif: "∀s∈P. ∀σ. Γ,Θ ⊨UNIV {σ} (Call (p s)) (Modif σ),(ModifAbr σ)" assumes ret_modif: "∀s t. t ∈ Modif (init s) ⟶ return' s t = return s t" assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s) ⟶ return' s t = return s t" shows "Γ,Θ ⊨tF P (dynCall init p return c) Q,A" using valid_call valid_modif ret_modif ret_modifAbr unfolding dynCall_dynCall_ex by (rule dynProc_exnModifyReturn_sound) lemma dynProc_exnModifyReturn: assumes dyn_call: "Γ,Θ⊨tF P dynCall_exn f g init p return' result_exn c Q,A" assumes ret_modif: "∀s t. t ∈ Modif (init s) ⟶ return' s t = return s t" assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s) ⟶ result_exn (return' s t) t = result_exn (return s t) t" assumes modif: "∀s ∈ P. ∀σ. Γ,Θ⊨UNIV {σ} Call (p s) (Modif σ),(ModifAbr σ)" shows "Γ,Θ ⊨tF P (dynCall_exn f g init p return result_exn c) Q,A" apply (rule hoaret_complete') apply (rule dynProc_exnModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr, OF hoaret_sound [OF dyn_call] _ ret_modif ret_modifAbr]) apply (intro ballI allI) apply (rule hoare_sound [OF modif [rule_format]]) apply assumption done lemma dynProcModifyReturn: assumes dyn_call: "Γ,Θ⊨tF P dynCall init p return' c Q,A" assumes ret_modif: "∀s t. t ∈ Modif (init s) ⟶ return' s t = return s t" assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s) ⟶ return' s t = return s t" assumes modif: "∀s ∈ P. ∀σ. Γ,Θ⊨UNIV {σ} Call (p s) (Modif σ),(ModifAbr σ)" shows "Γ,Θ ⊨tF P (dynCall init p return c) Q,A" using dyn_call ret_modif ret_modifAbr modif unfolding dynCall_dynCall_exn by (rule dynProc_exnModifyReturn) lemma dynProc_exnModifyReturnSameFaults_sound: assumes valid_call: "Γ,Θ ⊨tF P dynCall_exn f g init p return' result_exn c Q,A" assumes valid_modif: "∀s∈P. ∀σ. Γ,Θ ⊨F {σ} Call (p s) (Modif σ),(ModifAbr σ)" assumes ret_modif: "∀s t. t ∈ Modif (init s) ⟶ return' s t = return s t" assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s) ⟶ result_exn (return' s t) t shows "Γ,Θ ⊨tF P (dynCall_exn f g init p return result_exn c) Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨F P (Call p) Q,A" by (auto simp add: validt_def) assume exec: "Γ⊨⟨dynCall_exn f g init p return result_exn c,Normal s⟩ → t" assume t_notin_F: "t ∉ Fault ` F" assume P: "s ∈ P" with valid_modif have valid_modif': "∀σ. Γ,Θ⊨F {σ} (Call (p s)) (Modif σ),(ModifAbr σ)" by blast from exec have "Γ⊨⟨maybe_guard f g (call_exn init (p s) return result_exn c),Normal s⟩ → t" by (cases rule: exec_dynCall_exn_Normal_elim) then show "t ∈ Normal ` Q ∪ Abrupt ` A" proof (cases rule: exec_maybe_guard_Normal_elim_cases) case noFault from noFault have guards_ok: "s ∈ g" by simp from noFault have "Γ⊨ ⟨call_exn init (p s) return result_exn c,Normal s⟩ → t" by sim then show "t ∈ Normal ` Q ∪ Abrupt ` A" proof (cases rule: exec_call_exn_Normal_elim) fix bdy t' assume bdy: "Γ (p s) = Some bdy" assume exec_body: "Γ⊨⟨bdy,Normal (init s)⟩ → Normal t'" assume exec_c: "Γ⊨⟨c s t',Normal (return s t')⟩ → t" from exec_body bdy have "Γ⊨⟨Call (p s),Normal (init s)⟩ → Normal t'" by (auto simp add: intro: exec.intros) from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P have "t' ∈ Modif (init s)" by auto with ret_modif have "Normal (return' s t') = Normal (return s t')" by simp ecbdy exec_c bdy java.lang.StringIndexOutOfBoundsException: Range [60, 59) out of bounds for leng by (ao iro xccl_x) fr exec_maybe_guard_noFau [OF this guards_ok] have "Γ⊨on ( addjava.lang.StringIndexOutOfBoundsException: Range [38, 37) out of bounds for from [ valid_callctxtthis]P java.lang.StringIndexOutOfBoundsException: Index 62 out java.lang.StringIndexOutOfBoundsException: Range [13, 12) out of bounds for leng fix bdy t' assume bdy: "Γ (p s) Scan.succe (fn ctx > intro_and_in ct assume exec_body: "Γ⊨ assume t: "t = Abrupt (result_exn (return s t') t')" also from exec_body bdy have "Γ⊨⟨Call (p s) ,Normal (init s)⟩ → by (auto simp adend from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P have "t' ∈ ModifAbr (init s)" by auto with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return by simp finally have "t = Abrupt (result_exn (return' s t') t')" . with exec_body bdy have "Γ⊨⟨call_exn init (p s) return' result_exn c,Normal s⟩ → t" by (auto intro: exec_call_exnAbrupt) from exec_maybe_guard_noFault [OF this guards_ok] have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t" by (simp add: dynCall_exn_def exec_maybe_guard_DynCom) from cvalidt_postD [OF valid_call ctxt this] P t_notin_F show ?thesis by simp next fix bdy f' assume bdy: "Γ (p s) = Some bdy" assume "Γ⊨⟨bdy,Normal (init s)⟩ → Fault f'" and t: "t = Fault f'" with bdy have "Γ⊨⟨call_exn init (p s) return' result_exn c ,Normal s⟩ → t" by (auto intro: exec_call_exnFault) from exec_maybe_guard_noFault [OF this guards_ok] have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t" by (simp add: dynCall_exn_def exec_maybe_guard_DynCom) from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F show ?thesis by simp next fix bdy assume bdy: "Γ (p s) = Some bdy" assume "Γ⊨⟨bdy,Normal (init s)⟩ → Stuck" "t = Stuck" with bdy have "Γ⊨⟨call_exn init (p s) return' result_exn c ,Normal s⟩ → t" by (auto intro: exec_call_exnStuck) from exec_maybe_guard_noFault [OF this guards_ok] have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t" by (simp add: dynCall_exn_def exec_maybe_guard_DynCom) from valid_call ctxt this P t_notin_F show ?thesis by (rule cvalidt_postD) next fix bdy assume "Γ (p s) = None" "t=Stuck" hence "Γ⊨⟨call_exn init (p s) return' result_exn c ,Normal s⟩ → t" by (auto intro: exec_call_exnUndefined) from exec_maybe_guard_noFault [OF this guards_ok] have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t" by (simp add: dynCall_exn_def exec_maybe_guard_DynCom) from valid_call ctxt this P t_notin_F show ?thesis by (rule cvalidt_postD) qed next case (someFault) then obtain guards_fail:"s ∉ g" and t: "t = Fault f" by simp from exec_maybe_guard_Fault [OF guards_fail] t have "Γ⊨⟨dynCall_exn f g init p return' result_exn c,Normal s⟩ → t" by (simp add: dynCall_exn_def exec_guards_DynCom) from cvalidt_postD [OF valid_call ctxt this] P t_notin_F show ?thesis by simp qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨F P (Call p) Q,A" by (auto simp add: validt_def) assume P: "s ∈ P" from valid_call ctxt P have "Γ⊨dynCall_exn f g init p return' result_exn c↓ Normal s" by (rule cvalidt_termD) thus "Γ⊨dynCall_exn f g init p return result_exn c ↓ Normal s" proof (cases rule: terminates_dynCall_exn_elim) case noFault then obtain guards_ok: "s ∈ g" and call: "Γ⊨call_exn init (p s) return' result_exn c↓ Normal s" by auto have "Γ⊨call_exn init (p s) return result_exn c ↓ Normal s" proof (cases "p s ∈ dom Γ") case True with call obtain bdy where bdy: "Γ (p s) = Some bdy" and termi_bdy: "Γ⊨bdy ↓ Normal (init s)" and termi_c: "∀t. Γ⊨⟨bdy,Normal (init s)⟩ → Normal t ⟶ Γ⊨c s t ↓ Normal (return' s t)" by cases auto { fix t assume exec_bdy: "Γ⊨⟨bdy,Normal (init s)⟩ → Normal t" hence "Γ⊨c s t ↓ Normal (return s t)" proof - from exec_bdy bdy have "Γ⊨⟨Call (p s),Normal (init s)⟩ → Normal t" by (auto simp add: intro: exec.intros) from cvalidD [OF valid_modif [rule_format, of s "init s"] ctxt' this] P ret_modif have "return' s t = return s t" by auto with termi_c exec_bdy show ?thesis by auto qed } with bdy termi_bdy show ?thesis by (iprover intro: terminates_call_exn) next case False thus ?thesis by (auto intro: terminates_call_exnUndefined) qed thus "Γ⊨dynCall_exn f g init p return result_exn c ↓ Normal s" by (iprover intro: terminates_dynCall_exn) next case (someFault) then have guard_fail: "s ∉ g" by simp thus ?thesis by (simp add: terminates_maybe_guard_Fault dynCall_exn_def) qed qed lemma dynProcModifyReturnSameFaults_sound: assumes valid_call: "Γ,Θ ⊨tF P dynCall init p return' c Q,A" assumes valid_modif: "∀s∈P. ∀σ. Γ,Θ ⊨F {σ} Call (p s) (Modif σ),(ModifAbr σ)" assumes ret_modif: "∀s t. t ∈ Modif (init s) ⟶ return' s t = return s t" assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s) ⟶ return' s t = return s t" shows "Γ,Θ ⊨tF P (dynCall init p return c) Q,A" using valid_call valid_modif ret_modif ret_modifAbr unfolding dynCall_dynCall_ex by (rule dynProc_exnModifyReturnSameFaults_sound) lemma dynProc_exnModifyReturnSameFaults: assumes dyn_call: "Γ,Θ⊨tF P dynCall_exn f g init p return' result_exn c Q,A" assumes ret_modif: "∀s t. t ∈ Modif (init s) ⟶ return' s t = return s t" assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s) ⟶ result_exn (return' s t) t = result_exn (r assumes modif: "∀s ∈ P. ∀σ. Γ,Θ⊨F {σ} Call (p s) (Modif σ),(ModifAbr σ)" shows "Γ,Θ ⊨tF P (dynCall_exn f g init p return result_exn c) Q,A" apply (rule hoaret_complete') apply (rule dynProc_exnModifyReturnSameFaults_sound [where Modif=Modif and ModifAbr=ModifAbr, OF hoaret_sound [OF dyn_call] _ ret_modif ret_modifAbr]) apply (intro ballI allI) apply (rule hoare_sound [OF modif [rule_format]]) apply assumption done lemma dynProcModifyReturnSameFaults: assumes dyn_call: "Γ,Θ⊨tF P dynCall init p return' c Q,A" assumes ret_modif: "∀s t. t ∈ Modif (init s) ⟶ return' s t = return s t" assumes ret_modifAbr: "∀s t. t ∈ ModifAbr (init s) ⟶ return' s t = return s t" assumes modif: "∀s ∈ P. ∀σ. Γ,Θ⊨F {σ} Call (p s) (Modif σ),(ModifAbr σ)" shows "Γ,Θ ⊨tF P (dynCall init p return c) Q,A" using dyn_call ret_modif ret_modifAbr modif unfolding dynCall_dynCall_exn by (rule dynProc_exnModifyReturnSameFaults) subsubsection ‹Conjunction of Postcondition› lemma PostConjI_sound: assumes valid_Q: "Γ,Θ ⊨tF P c Q,A" assumes valid_R: "Γ,Θ ⊨tF P c R,B" shows "Γ,Θ ⊨tF P c (Q ∩ R),(A ∩ B)" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume exec: "Γ⊨⟨c,Normal s⟩ → t" assume P: "s ∈ P" assume t_notin_F: "t ∉ Fault ` F" from valid_Q ctxt exec P t_notin_F have "t ∈ Normal ` Q ∪ Abrupt ` A" by (rule cvalidt_postD) moreover from valid_R ctxt exec P t_notin_F have "t ∈ Normal ` R ∪ Abrupt ` B" by (rule cvalidt_postD) ultimately show "t ∈ Normal ` (Q ∩ R) ∪ Abrupt ` (A ∩ B)" by blast next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume P: "s ∈ P" from valid_Q ctxt P show "Γ⊨c ↓ Normal s" by (rule cvalidt_termD) qed lemma PostConjI: assumes deriv_Q: "Γ,Θ⊨tF P c Q,A" assumes deriv_R: "Γ,Θ⊨tF P c R,B" shows "Γ,Θ⊨tF P c (Q ∩ R),(A ∩ B)" apply (rule hoaret_complete') apply (rule PostConjI_sound) apply (rule hoaret_sound [OF deriv_Q]) apply (rule hoaret_sound [OF deriv_R]) done lemma Merge_PostConj_sound: assumes validF: "Γ,Θ⊨tF P c Q,A" assumes validG: "Γ,Θ⊨tG P' c R,X" assumes F_G: "F ⊆ G" assumes P_P': "P ⊆ P'" shows "Γ,Θ⊨tF P c (Q ∩ R),(A ∩ X)" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" with F_G have ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨tG P (Call p) Q,A" by (auto intro: validt_augment_Faults) assume exec: "Γ⊨⟨c,Normal s⟩ → t" assume P: "s ∈ P" with P_P' have P': "s ∈ P'" by auto assume t_noFault: "t ∉ Fault ` F" show "t ∈ Normal ` (Q ∩ R) ∪ Abrupt ` (A ∩ X)" proof - from cvalidt_postD [OF validF [rule_format] ctxt exec P t_noFault] have t: "t ∈ Normal ` Q ∪ Abrupt ` A". then have "t ∉ Fault ` G" by auto from cvalidt_postD [OF validG [rule_format] ctxt' exec P' this] have "t ∈ Normal ` R ∪ Abrupt ` X" . with t show ?thesis by auto qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume P: "s ∈ P" from validF ctxt P show "Γ⊨c ↓ Normal s" by (rule cvalidt_termD) qed lemma Merge_PostConj: assumes validF: "Γ,Θ⊨tF P c Q,A" assumes validG: "Γ,Θ⊨tG P' c R,X" assumes F_G: "F ⊆ G" assumes P_P': "P ⊆ P'" shows "Γ,Θ⊨tF P c (Q ∩ R),(A ∩ X)" apply (rule hoaret_complete') apply (rule Merge_PostConj_sound [OF _ _ F_G P_P']) using validF apply (blast intro:hoaret_sound) using validG apply (blast intro:hoaret_sound) done subsubsection ‹Guards and Guarantees› lemma SplitGuards_sound: assumes valid_c1: "Γ,Θ⊨tF P c1 Q,A" assumes valid_c2: "Γ,Θ⊨F P c2 UNIV,UNIV" assumes c: "(c1 ∩g c2) = Some c" shows "Γ,Θ⊨tF P c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" hence ctxt': "∀(P, p, Q, A)∈Θ. Γ ⊨F P (Call p) Q,A" by (auto simp add: validt_def) assume exec: "Γ⊨⟨c,Normal s⟩ → t" assume P: "s ∈ P" assume t_notin_F: "t ∉ Fault ` F" show "t ∈ Normal ` Q ∪ Abrupt ` A" proof (cases t) case Normal with inter_guards_exec_noFault [OF c exec] have "Γ⊨⟨c1,Normal s⟩ → t" by simp from valid_c1 ctxt this P t_notin_F show ?thesis by (rule cvalidt_postD) next case Abrupt with inter_guards_exec_noFault [OF c exec] have "Γ⊨⟨c1,Normal s⟩ → t" by simp from valid_c1 ctxt this P t_notin_F show ?thesis by (rule cvalidt_postD) next case (Fault f) assume t: "t=Fault f" with exec inter_guards_exec_Fault [OF c] have "Γ⊨⟨c1,Normal s⟩ → Fault f ∨ Γ⊨⟨c2,Normal s⟩ → Fault f" by auto then show ?thesis proof (cases rule: disjE [consumes 1]) assume "Γ⊨⟨c1,Normal s⟩ → Fault f" from cvalidt_postD [OF valid_c1 ctxt this P] t t_notin_F show ?thesis by blast next assume "Γ⊨⟨c2,Normal s⟩ → Fault f" from cvalidD [OF valid_c2 ctxt' this P] t t_notin_F show ?thesis by blast qed next case Stuck with inter_guards_exec_noFault [OF c exec] have "Γ⊨⟨c1,Normal s⟩ → t" by simp from valid_c1 ctxt this P t_notin_F show ?thesis by (rule cvalidt_postD) qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨tF P (Call p) Q,A" assume P: "s ∈ P" show "Γ⊨c ↓ Normal s" proof - from valid_c1 ctxt P have "Γ⊨c1 ↓ Normal s" by (rule cvalidt_termD) with c show ?thesis by (rule inter_guards_terminates) qed qed lemma SplitGuards: assumes c: "(c1 ∩g c2) = Some c" assumes deriv_c1: "Γ,Θ⊨tF P c1 Q,A" assumes deriv_c2: "Γ,Θ⊨F P c2 UNIV,UNIV" shows "Γ,Θ⊨tF P c Q,A" apply (rule hoaret_complete') apply (rule SplitGuards_sound [OF _ _ c]) apply (rule hoaret_sound [OF deriv_c1]) apply (rule hoare_sound [OF deriv_c2]) done lemma CombineStrip_sound: assumes valid: "Γ,Θ⊨tF P c Q,A" assumes valid_strip: "Γ,Θ⊨{} P (strip_guards (-F) c) UNIV,UNIV" shows "Γ,Θ⊨t{} P c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨t{} P (Call p) Q,A" hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨{} P (Call p) Q,A" by (auto simp add: validt_def) from ctxt have ctxt'': "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" by (auto intro: valid_augment_Faults simp add: validt_def) assume exec: "Γ⊨⟨c,Normal s⟩ → t" assume P: "s ∈ P" assume t_noFault: "t ∉ Fault ` {}" show "t ∈ Normal ` Q ∪ Abrupt ` A" proof (cases t) case (Normal t') from cvalidt_postD [OF valid ctxt'' exec P] Normal show ?thesis by auto next case (Abrupt t') from cvalidt_postD [OF valid ctxt'' exec P] Abrupt show ?thesis by auto next case (Fault f) show ?thesis proof (cases "f ∈ F") case True hence "f ∉ -F" by simp with exec Fault have "Γ⊨⟨strip_guards (-F) c,Normal s⟩ → Fault f" by (auto intro: exec_to_exec_strip_guards_Fault) from cvalidD [OF valid_strip ctxt' this P] Fault have False by auto thus ?thesis .. next case False with cvalidt_postD [OF valid ctxt'' exec P] Fault show ?thesis by auto qed next case Stuck from cvalidt_postD [OF valid ctxt'' exec P] Stuck show ?thesis by auto qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨t{} P (Call p) Q,A" hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" by (auto intro: valid_augment_Faults simp add: validt_def) assume P: "s ∈ P" show "Γ⊨c ↓ Normal s" proof - from valid ctxt' P show "Γ⊨c ↓ Normal s" by (rule cvalidt_termD) qed qed lemma CombineStrip: assumes deriv: "Γ,Θ⊨tF P c Q,A" assumes deriv_strip: "Γ,Θ⊨{} P (strip_guards (-F) c) UNIV,UNIV" shows "Γ,Θ⊨t{} P c Q,A" apply (rule hoaret_complete') apply (rule CombineStrip_sound) apply (iprover intro: hoaret_sound [OF deriv]) apply (iprover intro: hoare_sound [OF deriv_strip]) done lemma GuardsFlip_sound: assumes valid: "Γ,Θ⊨tF P c Q,A" assumes validFlip: "Γ,Θ⊨-F P c UNIV,UNIV" shows "Γ,Θ⊨t{} P c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨t{} P (Call p) Q,A" from ctxt have ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" by (auto intro: valid_augment_Faults simp add: validt_def) from ctxt have ctxtFlip: "∀(P, p, Q, A)∈Θ. Γ⊨-F P (Call p) Q,A" by (auto intro: valid_augment_Faults simp add: validt_def) assume exec: "Γ⊨⟨c,Normal s⟩ → t" assume P: "s ∈ P" assume t_noFault: "t ∉ Fault ` {}" show "t ∈ Normal ` Q ∪ Abrupt ` A" proof (cases t) case (Normal t') from cvalidt_postD [OF valid ctxt' exec P] Normal show ?thesis by auto next case (Abrupt t') from cvalidt_postD [OF valid ctxt' exec P] Abrupt show ?thesis by auto next case (Fault f) show ?thesis proof (cases "f ∈ F") case True hence "f ∉ -F" by simp with cvalidD [OF validFlip ctxtFlip exec P] Fault have False by auto thus ?thesis .. next case False with cvalidt_postD [OF valid ctxt' exec P] Fault show ?thesis by auto qed next case Stuck from cvalidt_postD [OF valid ctxt' exec P] Stuck show ?thesis by auto qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ ⊨t{} P (Call p) Q,A" hence ctxt': "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" by (auto intro: valid_augment_Faults simp add: validt_def) assume P: "s ∈ P" show "Γ⊨c ↓ Normal s" proof - from valid ctxt' P show "Γ⊨c ↓ Normal s" by (rule cvalidt_termD) qed qed lemma GuardsFlip: assumes deriv: "Γ,Θ⊨tF P c Q,A" assumes derivFlip: "Γ,Θ⊨-F P c UNIV,UNIV" shows "Γ,Θ⊨t{} P c Q,A" apply (rule hoaret_complete') apply (rule GuardsFlip_sound) apply (iprover intro: hoaret_sound [OF deriv]) apply (iprover intro: hoare_sound [OF derivFlip]) done lemma MarkGuardsI_sound: assumes valid: "Γ,Θ⊨t{} P c Q,A" shows "Γ,Θ⊨t{} P mark_guards f c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨t{} P (Call p) Q,A" assume exec: "Γ⊨⟨mark_guards f c,Normal s⟩ → t" from exec_mark_guards_to_exec [OF exec] obtain t' where exec_c: "Γ⊨⟨c,Normal s⟩ → t'" and t'_noFault: "¬ isFault t' ⟶ t' = t" by blast assume P: "s ∈ P" assume t_noFault: "t ∉ Fault ` {}" show "t ∈ Normal ` Q ∪ Abrupt ` A" proof - from cvalidt_postD [OF valid [rule_format] ctxt exec_c P] have "t' ∈ Normal ` Q ∪ Abrupt ` A" by blast with t'_noFault show ?thesis by auto qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨t{} P (Call p) Q,A" assume P: "s ∈ P" from cvalidt_termD [OF valid ctxt P] have "Γ⊨c ↓ Normal s". thus "Γ⊨mark_guards f c ↓ Normal s" by (rule terminates_to_terminates_mark_guards) qed lemma MarkGuardsI: assumes deriv: "Γ,Θ⊨t{} P c Q,A" shows "Γ,Θ⊨t{} P mark_guards f c Q,A" apply (rule hoaret_complete') apply (rule MarkGuardsI_sound) apply (iprover intro: hoaret_sound [OF deriv]) done lemma MarkGuardsD_sound: assumes valid: "Γ,Θ⊨t{} P mark_guards f c Q,A" shows "Γ,Θ⊨t{} P c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨t{} P (Call p) Q,A" assume exec: "Γ⊨⟨c,Normal s⟩ → t" assume P: "s ∈ P" assume t_noFault: "t ∉ Fault ` {}" show "t ∈ Normal ` Q ∪ Abrupt ` A" proof (cases "isFault t") case True with exec_to_exec_mark_guards_Fault exec obtain f' where "Γ⊨⟨mark_guards f c,Normal s⟩ → Fault f'" by (fastforce elim: isFaultE) from cvalidt_postD [OF valid [rule_format] ctxt this P] have False by auto thus ?thesis .. next case False from exec_to_exec_mark_guards [OF exec False] obtain f' where "Γ⊨⟨mark_guards f c,Normal s⟩ → t" by auto from cvalidt_postD [OF valid [rule_format] ctxt this P] show ?thesis by auto qed next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨t{} P (Call p) Q,A" assume P: "s ∈ P" from cvalidt_termD [OF valid ctxt P] have "Γ⊨mark_guards f c ↓ Normal s". thus "Γ⊨c ↓ Normal s" by (rule terminates_mark_guards_to_terminates) qed lemma MarkGuardsD: assumes deriv: "Γ,Θ⊨t{} P mark_guards f c Q,A" shows "Γ,Θ⊨t{} P c Q,A" apply (rule hoaret_complete') apply (rule MarkGuardsD_sound) apply (iprover intro: hoaret_sound [OF deriv]) done lemma MergeGuardsI_sound: assumes valid: "Γ,Θ⊨tF P c Q,A" shows "Γ,Θ⊨tF P merge_guards c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume exec_merge: "Γ⊨⟨merge_guards c,Normal s⟩ → t" from exec_merge_guards_to_exec [OF exec_merge] have exec: "Γ⊨⟨c,Normal s⟩ → t" . assume P: "s ∈ P" assume t_notin_F: "t ∉ Fault ` F" from cvalidt_postD [OF valid [rule_format] ctxt exec P t_notin_F] show "t ∈ Normal ` Q ∪ Abrupt ` A". next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume P: "s ∈ P" from cvalidt_termD [OF valid ctxt P] have "Γ⊨c ↓ Normal s". thus "Γ⊨merge_guards c ↓ Normal s" by (rule terminates_to_terminates_merge_guards) qed lemma MergeGuardsI: assumes deriv: "Γ,Θ⊨tF P c Q,A" shows "Γ,Θ⊨tF P merge_guards c Q,A" apply (rule hoaret_complete') apply (rule MergeGuardsI_sound) apply (iprover intro: hoaret_sound [OF deriv]) done lemma MergeGuardsD_sound: assumes valid: "Γ,Θ⊨tF P merge_guards c Q,A" shows "Γ,Θ⊨tF P c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume exec: "Γ⊨⟨c,Normal s⟩ → t" from exec_to_exec_merge_guards [OF exec] have exec_merge: "Γ⊨⟨merge_guards c,Normal s⟩ → t". assume P: "s ∈ P" assume t_notin_F: "t ∉ Fault ` F" from cvalidt_postD [OF valid [rule_format] ctxt exec_merge P t_notin_F] show "t ∈ Normal ` Q ∪ Abrupt ` A". next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume P: "s ∈ P" from cvalidt_termD [OF valid ctxt P] have "Γ⊨merge_guards c ↓ Normal s". thus "Γ⊨c ↓ Normal s" by (rule terminates_merge_guards_to_terminates) qed lemma MergeGuardsD: assumes deriv: "Γ,Θ⊨tF P merge_guards c Q,A" shows "Γ,Θ⊨tF P c Q,A" apply (rule hoaret_complete') apply (rule MergeGuardsD_sound) apply (iprover intro: hoaret_sound [OF deriv]) done lemma SubsetGuards_sound: assumes c_c': "c ⊆g c'" assumes valid: "Γ,Θ⊨t{} P c' Q,A" shows "Γ,Θ⊨t{} P c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨t{} P (Call p) Q,A" assume exec: "Γ⊨⟨c,Normal s⟩ → t" from exec_to_exec_subseteq_guards [OF c_c' exec] obtain t' where exec_c': "Γ⊨⟨c',Normal s⟩ → t'" and t'_noFault: "¬ isFault t' ⟶ t' = t" by blast assume P: "s ∈ P" assume t_noFault: "t ∉ Fault ` {}" from cvalidt_postD [OF valid [rule_format] ctxt exec_c' P] t'_noFault t_noFault show "t ∈ Normal ` Q ∪ Abrupt ` A" by auto next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨t{} P (Call p) Q,A" assume P: "s ∈ P" from cvalidt_termD [OF valid ctxt P] have termi_c': "Γ⊨c' ↓ Normal s". from cvalidt_postD [OF valid ctxt _ P] have noFault_c': "Γ⊨⟨c',Normal s⟩ →∉Fault ` UNIV" by (auto simp add: final_notin_def) from termi_c' c_c' noFault_c' show "Γ⊨c ↓ Normal s" by (rule terminates_fewer_guards) qed lemma SubsetGuards: assumes c_c': "c ⊆g c'" assumes deriv: "Γ,Θ⊨t{} P c' Q,A" shows "Γ,Θ⊨t{} P c Q,A" apply (rule hoaret_complete') apply (rule SubsetGuards_sound [OF c_c']) apply (iprover intro: hoaret_sound [OF deriv]) done lemma NormalizeD_sound: assumes valid: "Γ,Θ⊨tF P (normalize c) Q,A" shows "Γ,Θ⊨tF P c Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume exec: "Γ⊨⟨c,Normal s⟩ → t" hence exec_norm: "Γ⊨⟨normalize c,Normal s⟩ → t" by (rule exec_to_exec_normalize) assume P: "s ∈ P" assume noFault: "t ∉ Fault ` F" from cvalidt_postD [OF valid [rule_format] ctxt exec_norm P noFault] show "t ∈ Normal ` Q ∪ Abrupt ` A". next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume P: "s ∈ P" from cvalidt_termD [OF valid ctxt P] have "Γ⊨normalize c ↓ Normal s". thus "Γ⊨c ↓ Normal s" by (rule terminates_normalize_to_terminates) qed lemma NormalizeD: assumes deriv: "Γ,Θ⊨tF P (normalize c) Q,A" shows "Γ,Θ⊨tF P c Q,A" apply (rule hoaret_complete') apply (rule NormalizeD_sound) apply (iprover intro: hoaret_sound [OF deriv]) done lemma NormalizeI_sound: assumes valid: "Γ,Θ⊨tF P c Q,A" shows "Γ,Θ⊨tF P (normalize c) Q,A" proof (rule cvalidtI) fix s t assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume "Γ⊨⟨normalize c,Normal s⟩ → t" hence exec: "Γ⊨⟨c,Normal s⟩ → t" by (rule exec_normalize_to_exec) assume P: "s ∈ P" assume noFault: "t ∉ Fault ` F" from cvalidt_postD [OF valid [rule_format] ctxt exec P noFault] show "t ∈ Normal ` Q ∪ Abrupt ` A". next fix s assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨tF P (Call p) Q,A" assume P: "s ∈ P" from cvalidt_termD [OF valid ctxt P] have "Γ⊨ c ↓ Normal s". thus "Γ⊨normalize c ↓ Normal s" by (rule terminates_to_terminates_normalize) qed lemma NormalizeI: assumes deriv: "Γ,Θ⊨tF P c Q,A" shows "Γ,Θ⊨tF P (normalize c) Q,A" apply (rule hoaret_complete') apply (rule NormalizeI_sound) apply (iprover intro: hoaret_sound [OF deriv]) done subsubsection ‹Restricting the Procedure Environment› lemma validt_restrict_to_validt: assumes validt_c: "Γ|⊨tF P c Q,A" shows "Γ⊨tF P c Q,A" proof - from validt_c have valid_c: "Γ|⊨F P c Q,A" by (simp add: validt_def) hence "Γ⊨F P c Q,A" by (rule valid_restrict_to_valid) moreover { fix s assume P: "s ∈ P" have "Γ⊨c↓Normal s" proof - from P validt_c have "Γ|⊨c↓Normal s" by (auto simp add: validt_def) moreover from P valid_c have "Γ|⊨⟨c,Normal s⟩ →∉{Stuck}" by (auto simp add: valid_def final_notin_def) ultimately show ?thesis by (rule terminates_restrict_to_terminates) qed } ultimately show ?thesis by (auto simp add: validt_def) qed lemma augment_procs: assumes deriv_c: "Γ|,{}⊨tF P c Q,A" shows "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" apply (rule hoaret_complete) apply (rule validt_restrict_to_validt) apply (insert hoaret_sound [OF deriv_c]) by (simp add: cvalidt_def) subsubsection \<open>Miscellaneous\<close> lemma augment_Faults: assumes deriv_c: "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" assumes F: "F \<subseteq> F'" shows "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F'\<^esub> P c Q,A" apply (rule hoaret_complete) apply (rule validt_augment_Faults [OF _ F]) apply (insert hoaret_sound [OF deriv_c]) by (simp add: cvalidt_def) lemma TerminationPartial_sound: assumes "termination": "\<forall>s \<in> P. \<Gamma>\<turnstile>c\<down>Normal s" assumes partial_corr: "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" using "termination" partial_corr by (auto simp add: cvalidt_def validt_def cvalid_def) lemma TerminationPartial: assumes partial_deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" assumes "termination": "\<forall>s \<in> P. \<Gamma>\<turnstile>c\<down>Normal s" shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" apply (rule hoaret_complete') apply (rule TerminationPartial_sound [OF "termination"]) apply (rule hoare_sound [OF partial_deriv]) done lemma TerminationPartialStrip: assumes partial_deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" assumes "termination": "\<forall>s \<in> P. strip F' \<Gamma>\<turnstile>strip_guards F' c\<down>No shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" proof - from "termination" have "\<forall>s \<in> P. \<Gamma>\<turnstile>c\<down>Normal s" by (auto intro: terminates_strip_guards_to_terminates terminates_strip_to_terminates) with partial_deriv show ?thesis by (rule TerminationPartial) qed lemma SplitTotalPartial: assumes termi: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q',A'" assumes part: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" proof - from hoaret_sound [OF termi] hoare_sound [OF part] have "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def) thus ?thesis by (rule hoaret_complete') qed lemma SplitTotalPartial': assumes termi: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/UNIV\<^esub> P c Q',A'" assumes part: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" proof - from hoaret_sound [OF termi] hoare_sound [OF part] have "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def) thus ?thesis by (rule hoaret_complete') qed end
¤ Dauer der Verarbeitung: 0.231 Sekunden (vorverarbeitet am 2026-11-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01