Theory OG_Tactics
section ‹Verfication Condition Generator for COMPLX OG›
theory OG_Tactics
imports
OG_Soundness
"lib/Cache_Tactics"
begin
subsection ‹Seq oghoare derivation›
lemmas SeqSkipRule = SeqSkip
lemmas SeqThrowRule = SeqThrow
lemmas SeqBasicRule = SeqBasic
lemmas SeqSpecRule = SeqSpec
lemmas SeqSeqRule = SeqSeq
lemma SeqCondRule:
"⟦ Γ, Θ ⊩⇘/F⇙ C1 P⇩1 c⇩1 Q,A;
Γ, Θ ⊩⇘/F⇙ C2 P⇩2 c⇩2 Q,A ⟧
⟹ Γ, Θ ⊩⇘/F⇙ {s. (s∈b ⟶ s∈C1) ∧ (s∉b ⟶ s∈C2)} (AnnBin r P⇩1 P⇩2)
(Cond b c⇩1 c⇩2) Q,A"
apply (rule SeqCond)
apply (erule SeqConseq[rotated]; clarsimp)
apply (erule SeqConseq[rotated]; clarsimp)
done
lemma SeqWhileRule:
"⟦ Γ, Θ ⊩⇘/F⇙ (i ∩ b) a c i,A; i ∩ - b ⊆ Q ⟧
⟹ Γ, Θ ⊩⇘/F⇙ i (AnnWhile r i a) (While b c) Q,A"
apply (rule SeqConseq[OF _ SeqWhile])
prefer 2 apply assumption
by simp+
lemma DynComRule:
"⟦ r ⊆ pre a; ⋀s. s∈r ⟹ Γ, Θ ⊢⇘/F⇙ a (c s) Q,A ⟧ ⟹
Γ, Θ ⊢⇘/F⇙ (AnnRec r a) (DynCom c) Q,A"
by (erule DynCom) clarsimp
lemma SeqDynComRule:
"⟦r ⊆ pre a;
⋀s. s∈r ⟹ Γ, Θ ⊩⇘/F⇙P a (c s) Q,A;
P⊆r ⟧ ⟹
Γ, Θ ⊩⇘/F⇙ P (AnnRec r a) (DynCom c) Q,A"
by (erule SeqDynCom) clarsimp
lemma SeqCallRule:
"⟦ P' ⊆ P; Γ, Θ ⊩⇘/F⇙ P P'' f Q,A;
n < length as; Γ p = Some f;
as ! n = P''; Θ p = Some as⟧
⟹ Γ, Θ ⊩⇘/F⇙ P' (AnnCall r n) (Call p) Q,A"
by (simp add: SeqCall SeqConseq)
lemma SeqGuardRule:
"⟦ P ∩ g ⊆ P'; P ∩ -g ≠ {} ⟹ f ∈ F;
Γ, Θ ⊩⇘/F⇙ P' a c Q,A ⟧ ⟹
Γ, Θ ⊩⇘/F⇙ P (AnnRec r a) (Guard f g c) Q,A"
by (simp add: SeqGuard SeqConseq)
subsection ‹Parallel-mode rules›
lemma GuardRule:
"⟦ r ∩ g ⊆ pre P; r ∩ -g ≠ {} ⟶ f ∈ F;
Γ, Θ ⊢⇘/F⇙ P c Q,A ⟧ ⟹
Γ, Θ ⊢⇘/F⇙ (AnnRec r P) (Guard f g c) Q,A"
by (simp add: Guard)
lemma CallRule:
"⟦ r ⊆ pre P; Γ, Θ ⊢⇘/F⇙ P f Q,A;
n < length as; Γ p = Some f;
as ! n = P; Θ p = Some as⟧
⟹ Γ, Θ ⊢⇘/F⇙ (AnnCall r n) (Call p) Q,A"
by (simp add: Call)
definition map_ann_hoare :: "('s,'p,'f) body ⇒ ('s,'p,'f) proc_assns ⇒ 'f set
⇒ ('s, 'p, 'f) ann_triple list ⇒ ('s,'p,'f) com list ⇒ bool"
("(4_,_/[⊩]⇘'/_ ⇙(_/ (_)))" [60,60,60,1000,20]60) where
"Γ, Θ [⊩]⇘/F⇙ Ps Ts ≡ ∀i < length Ts. Γ, Θ ⊢⇘/F⇙ (pres (Ps!i)) (Ts!i) (postcond (Ps!i)), (abrcond (Ps!i))"
lemma MapAnnEmpty: "Γ, Θ [⊩]⇘/F⇙ [] []"
by(simp add:map_ann_hoare_def)
lemma MapAnnList: "⟦ Γ, Θ ⊢⇘/F⇙ P c Q, A;
Γ, Θ [⊩]⇘/F⇙ Ps Ts ⟧
⟹ Γ, Θ [⊩]⇘/F⇙ ((P, Q, A)#Ps) (c#Ts)"
apply(simp add:map_ann_hoare_def)
apply clarify
apply (rename_tac i)
apply(case_tac i,simp+)
done
lemma MapAnnMap:
"∀k. i≤k ∧ k<j ⟶ Γ, Θ ⊢⇘/F⇙ (P k) (c k) (Q k), (A k)
⟹ Γ, Θ [⊩]⇘/F⇙ (map (λk. (P k, Q k, A k)) [i..<j]) (map c [i..<j])"
by (simp add: add.commute le_add1 map_ann_hoare_def)
lemma ParallelRule:
"⟦Γ, Θ [⊩]⇘/F⇙ Ps Cs;
interfree Γ Θ F Ps Cs;
length Cs = length Ps
⟧ ⟹ Γ, Θ ⊢⇘/F⇙ (AnnPar Ps)
(Parallel Cs)
(⋂i∈{i. i<length Ps}. postcond (Ps!i)), (⋃i∈{i. i<length Ps}. abrcond (Ps!i))"
apply (clarsimp simp add:neq_Nil_conv Parallel map_ann_hoare_def )+
apply (rule Parallel)
apply fastforce
apply fastforce
apply fastforce
apply clarsimp
apply (clarsimp simp: in_set_conv_nth)
apply (rename_tac i)
apply (rule_tac x=i in exI, fastforce)
done
lemma ParallelConseqRule:
"⟦ Γ, Θ ⊢⇘/F⇙ (AnnPar Ps)
(Parallel Ts)
(⋂i∈{i. i<length Ps}. postcond (Ps!i)), (⋃i∈{i. i<length Ps}. abrcond (Ps!i));
(⋂i∈{i. i<length Ps}. postcond (Ps!i)) ⊆ Q;
(⋃i∈{i. i<length Ps}. abrcond (Ps!i)) ⊆ A
⟧ ⟹ Γ, Θ ⊢⇘/F⇙ (AnnPar Ps) (Parallel Ts) Q, A"
apply (rule Conseq)
apply (rule exI[where x="(⋂i∈{i. i<length Ps}. precond (Ps!i))"])
apply (rule exI[where x="(⋂i∈{i. i<length Ps}. postcond (Ps!i))"])
apply (rule exI[where x="(⋃i∈{i. i<length Ps}. abrcond (Ps!i))"])
apply (clarsimp)
done
text ‹See Soundness.thy for the rest of Parallel-mode rules›
subsection ‹VCG tactic helper definitions and lemmas›
definition interfree_aux_right :: "('s,'p,'f) body ⇒ ('s,'p,'f) proc_assns ⇒ 'f set ⇒ ('s assn × ('s,'p,'f) com × ('s, 'p, 'f) ann) ⇒ bool" where
"interfree_aux_right Γ Θ F ≡ λ(q, cmd, ann). (∀aa ac. atomicsR Γ Θ ann cmd (aa,ac) ⟶ (Γ ⊨⇘/F⇙ (q ∩ aa) ac q, q))"
lemma pre_strengthen: "¬pre_par a ⟹ pre (strengthen_pre a a') = pre a ∩ a'"
by (induct a arbitrary: a', simp_all)
lemma Basic_inter_right:
"Γ, Θ ⊢⇘/F⇙ (AnnExpr (q ∩ r)) (Basic f) q, q ⟹ interfree_aux_right Γ Θ F (q, Basic f, AnnExpr r)"
by (auto simp: interfree_aux_right_def
elim!: atomicsR.cases
dest: oghoare_sound)
lemma Skip_inter_right:
"Γ, Θ ⊢⇘/F⇙ (AnnExpr (q ∩ r)) Skip q, q ⟹ interfree_aux_right Γ Θ F (q, Skip, AnnExpr r)"
by (auto simp: interfree_aux_right_def
elim!: atomicsR.cases
dest: oghoare_sound)
lemma Throw_inter_right:
"Γ, Θ ⊢⇘/F⇙ (AnnExpr (q ∩ r)) Throw q, q ⟹ interfree_aux_right Γ Θ F (q, Throw, AnnExpr r)"
by (auto simp: interfree_aux_right_def
elim!: atomicsR.cases
dest: oghoare_sound)
lemma Spec_inter_right:
"Γ, Θ ⊢⇘/F⇙ (AnnExpr (q ∩ r)) (Spec rel) q, q ⟹ interfree_aux_right Γ Θ F (q, Spec rel, AnnExpr r)"
by (auto simp: interfree_aux_right_def
elim!: atomicsR.cases
dest: oghoare_sound)
lemma valid_Await:
"atom_com c ⟹ Γ⊨⇘/F⇙ (P ∩ b) c Q,A ⟹ Γ⊨⇘/F⇙ P Await b c Q,A"
apply (clarsimp simp: valid_def)
apply (erule converse_rtranclpE)
apply (clarsimp simp: final_def)
apply clarsimp
apply (erule step_Normal_elim_cases)
apply clarsimp
apply (erule disjE)
apply (fastforce dest: no_steps_final simp: final_def)
apply (fastforce dest: no_steps_final simp: final_def)
apply clarsimp
apply (drule no_steps_final, simp add: final_def)
apply clarsimp
apply (rename_tac x c'')
apply (drule_tac x="Normal x" in spec)
apply (drule spec[where x=Stuck])
apply (drule spec[where x=Skip])
apply (erule impE)
apply (cut_tac c=c'' in steps_Stuck[where Γ=Γ])
apply fastforce
apply clarsimp
apply (drule no_steps_final, simp add: final_def)
apply clarsimp
apply (drule_tac x="Normal x" in spec)
apply (drule_tac x="Fault f" in spec)
apply (drule spec[where x=Skip])
apply (erule impE)
apply (rename_tac c'' f)
apply (cut_tac c=c'' and f=f in steps_Fault[where Γ=Γ])
apply fastforce
apply clarsimp
apply clarsimp
done
lemma atomcom_imp_not_prepare:
"ann_matches Γ Θ a c ⟹ atom_com c ⟹
¬ pre_par a"
by (induct rule:ann_matches.induct, simp_all)
lemma Await_inter_right:
"atom_com c ⟹
Γ, Θ ⊩⇘/F⇙ P a c q,q ⟹
q ∩ r ∩ b ⊆ P ⟹
interfree_aux_right Γ Θ F (q, Await b c, AnnRec r a)"
apply (simp add: interfree_aux_right_def )
apply clarsimp
apply (erule atomicsR.cases, simp_all)
apply clarsimp
apply (rule valid_Await, assumption)
apply (drule oghoare_seq_sound)
apply (erule valid_weaken_pre)
apply blast
done
lemma Call_inter_right:
"⟦interfree_aux_right Γ Θ F (q, f, P);
n < length as; Γ p = Some f;
as ! n = P; Θ p = Some as⟧ ⟹
interfree_aux_right Γ Θ F (q, Call p, AnnCall r n)"
by(auto simp: interfree_aux_right_def elim: atomicsR.cases)
lemma DynCom_inter_right:
"⟦⋀s. s ∈ r ⟹ interfree_aux_right Γ Θ F (q, f s, P) ⟧ ⟹
interfree_aux_right Γ Θ F (q, DynCom f, AnnRec r P)"
by(auto simp: interfree_aux_right_def elim: atomicsR.cases)
lemma Guard_inter_right:
"interfree_aux_right Γ Θ F (q, c, a)
⟹ interfree_aux_right Γ Θ F (q, Guard f g c, AnnRec r a)"
by(auto simp: interfree_aux_right_def elim: atomicsR.cases)
lemma Parallel_inter_right_empty:
"interfree_aux_right Γ Θ F (q, Parallel [], AnnPar [])"
by(auto simp: interfree_aux_right_def elim: atomicsR.cases)
lemma Parallel_inter_right_List:
"⟦interfree_aux_right Γ Θ F (q, c, a);
interfree_aux_right Γ Θ F (q, Parallel cs, AnnPar as)⟧
⟹ interfree_aux_right Γ Θ F (q, Parallel (c#cs), AnnPar ((a, Q, A) #as))"
apply (clarsimp simp: interfree_aux_right_def)
apply (erule atomicsR.cases; clarsimp)
apply (rename_tac i aa b)
apply (case_tac i, simp)
apply (fastforce intro: AtParallelExprs)
done
lemma Parallel_inter_right_Map:
"∀k. i≤k ∧ k<j ⟶ interfree_aux_right Γ Θ F (q, c k, a k)
⟹ interfree_aux_right Γ Θ F
(q, Parallel (map c [i..<j]), AnnPar (map (λi. (a i, Q, A)) [i..<j]))"
apply (clarsimp simp: interfree_aux_right_def)
apply (erule atomicsR.cases; clarsimp)
apply (rename_tac ia aa b)
apply (drule_tac x="i+ia" in spec)
by fastforce
lemma Seq_inter_right:
"⟦ interfree_aux_right Γ Θ F (q, c⇩1, a1); interfree_aux_right Γ Θ F (q, c⇩2, a2) ⟧⟹
interfree_aux_right Γ Θ F (q, Seq c⇩1 c⇩2, AnnComp a1 a2)"
by (auto simp add: interfree_aux_right_def elim: atomicsR.cases)
lemma Catch_inter_right:
"⟦ interfree_aux_right Γ Θ F (q, c⇩1, a1); interfree_aux_right Γ Θ F (q, c⇩2, a2) ⟧⟹
interfree_aux_right Γ Θ F (q, Catch c⇩1 c⇩2, AnnComp a1 a2)"
by (auto simp add: interfree_aux_right_def elim: atomicsR.cases)
lemma While_inter_aux_any: "interfree_aux Γ Θ F (Any, (AnyAnn, q, abr), c, P) ⟹
interfree_aux Γ Θ F (Any, (AnyAnn, q, abr), While b c, AnnWhile R I P)"
by (auto simp add: interfree_aux_def
elim: atomicsR.cases[where ?a1.0="AnnWhile _ _ _"] )
lemma While_inter_right:
"interfree_aux_right Γ Θ F (q, c, a)
⟹ interfree_aux_right Γ Θ F (q, While b c, AnnWhile r i a)"
by(auto simp: interfree_aux_right_def elim: atomicsR.cases)
lemma Cond_inter_aux_any:
"⟦ interfree_aux Γ Θ F (Any, (AnyAnn, q, a), c⇩1, a1); interfree_aux Γ Θ F (Any, (AnyAnn, q, a), c⇩2, a2) ⟧⟹
interfree_aux Γ Θ F (Any, (AnyAnn, q, a), Cond b c⇩1 c⇩2, AnnBin r a1 a2)"
by (fastforce simp add: interfree_aux_def
elim: atomicsR.cases[where ?a1.0="AnnBin _ _ _"])
lemma Cond_inter_right:
"⟦ interfree_aux_right Γ Θ F (q, c⇩1, a1); interfree_aux_right Γ Θ F (q, c⇩2, a2) ⟧⟹
interfree_aux_right Γ Θ F (q, Cond b c⇩1 c⇩2, AnnBin r a1 a2)"
by(auto simp: interfree_aux_right_def elim: atomicsR.cases)
lemma Basic_inter_aux:
"⟦interfree_aux_right Γ Θ F (r, com, ann);
interfree_aux_right Γ Θ F (q, com, ann);
interfree_aux_right Γ Θ F (a, com, ann) ⟧ ⟹
interfree_aux Γ Θ F (Basic f, (AnnExpr r, q, a), com, ann)"
by (auto elim: assertionsR.cases simp: interfree_aux_def interfree_aux_right_def)
lemma Skip_inter_aux:
"⟦interfree_aux_right Γ Θ F (r, com, ann);
interfree_aux_right Γ Θ F (q, com, ann);
interfree_aux_right Γ Θ F (a, com, ann) ⟧ ⟹
interfree_aux Γ Θ F (Skip, (AnnExpr r, q, a), com, ann)"
by (auto elim: assertionsR.cases simp: interfree_aux_def interfree_aux_right_def)
lemma Throw_inter_aux:
"⟦interfree_aux_right Γ Θ F (r, com, ann);
interfree_aux_right Γ Θ F (q, com, ann);
interfree_aux_right Γ Θ F (a, com, ann) ⟧ ⟹
interfree_aux Γ Θ F (Throw, (AnnExpr r, q, a), com, ann)"
by (auto elim: assertionsR.cases simp: interfree_aux_def interfree_aux_right_def)
lemma Spec_inter_aux:
"⟦interfree_aux_right Γ Θ F (r, com, ann);
interfree_aux_right Γ Θ F (q, com, ann);
interfree_aux_right Γ Θ F (a, com, ann) ⟧ ⟹
interfree_aux Γ Θ F (Spec rel, (AnnExpr r, q, a), com, ann)"
by (auto elim: assertionsR.cases simp: interfree_aux_def interfree_aux_right_def)
lemma Seq_inter_aux:
"⟦ interfree_aux Γ Θ F (c⇩1, (r⇩1, pre r⇩2, A), com, ann);
interfree_aux Γ Θ F (c⇩2, (r⇩2, Q, A), com, ann) ⟧
⟹ interfree_aux Γ Θ F (Seq c⇩1 c⇩2, (AnnComp r⇩1 r⇩2, Q, A), com, ann)"
by (auto elim: assertionsR.cases simp: interfree_aux_def interfree_aux_right_def)
lemma Catch_inter_aux:
"⟦ interfree_aux Γ Θ F (c⇩1, (r⇩1, Q, pre r⇩2), com, ann);
interfree_aux Γ Θ F (c⇩2, (r⇩2, Q, A), com, ann) ⟧
⟹ interfree_aux Γ Θ F (Catch c⇩1 c⇩2, (AnnComp r⇩1 r⇩2, Q, A), com, ann)"
by (auto elim: assertionsR.cases simp: interfree_aux_def interfree_aux_right_def)
lemma Cond_inter_aux:
"⟦ interfree_aux_right Γ Θ F (r, com, ann);
interfree_aux Γ Θ F (c⇩1, (r⇩1, Q, A), com, ann);
interfree_aux Γ Θ F (c⇩2, (r⇩2, Q, A), com, ann) ⟧
⟹ interfree_aux Γ Θ F (Cond b c⇩1 c⇩2, (AnnBin r r⇩1 r⇩2, Q, A), com, ann)"
by (auto elim: assertionsR.cases simp: interfree_aux_def interfree_aux_right_def)
lemma While_inter_aux:
"⟦ interfree_aux_right Γ Θ F (r, com, ann);
interfree_aux_right Γ Θ F (Q, com, ann);
interfree_aux Γ Θ F (c, (P, i, A), com, ann) ⟧ ⟹
interfree_aux Γ Θ F (While b c, (AnnWhile r i P, Q, A), com, ann)"
by (auto elim: assertionsR.cases simp: interfree_aux_def interfree_aux_right_def)
lemma Await_inter_aux:
"⟦ interfree_aux_right Γ Θ F (r, com, ann);
interfree_aux_right Γ Θ F (Q, com, ann);
interfree_aux_right Γ Θ F (A, com, ann) ⟧
⟹ interfree_aux Γ Θ F (Await b e, (AnnRec r ae, Q, A), com, ann)"
by (auto simp: interfree_aux_def interfree_aux_right_def elim: assertionsR.cases)
lemma Call_inter_aux:
"⟦ interfree_aux_right Γ Θ F (r, com, ann);
interfree_aux Γ Θ F (f, (P, Q, A), com, ann);
n < length as; Γ p = Some f;
as ! n = P; Θ p = Some as ⟧ ⟹
interfree_aux Γ Θ F (Call p, (AnnCall r n, Q, A), com, ann)"
by (auto elim: assertionsR.cases simp: interfree_aux_def interfree_aux_right_def)
lemma DynCom_inter_aux:
"⟦ interfree_aux_right Γ Θ F (r, com, ann);
interfree_aux_right Γ Θ F (Q, com, ann);
interfree_aux_right Γ Θ F (A, com, ann);
⋀s. s∈r ⟹ interfree_aux Γ Θ F (f s, (P, Q, A), com, ann) ⟧ ⟹
interfree_aux Γ Θ F (DynCom f, (AnnRec r P, Q, A), com, ann)"
by (auto elim: assertionsR.cases simp: interfree_aux_def interfree_aux_right_def)
lemma Guard_inter_aux:
"⟦ interfree_aux_right Γ Θ F (r, com, ann);
interfree_aux_right Γ Θ F (Q, com, ann);
interfree_aux Γ Θ F (c, (P, Q, A), com, ann) ⟧ ⟹
interfree_aux Γ Θ F (Guard f g c, (AnnRec r P, Q, A), com, ann)"
by (auto elim: assertionsR.cases simp: interfree_aux_def interfree_aux_right_def)
definition
inter_aux_Par :: "('s,'p,'f) body ⇒ ('s,'p,'f) proc_assns ⇒ 'f set ⇒
(('s, 'p, 'f) com list × (('s, 'p, 'f) ann_triple) list × ('s, 'p, 'f) com × ('s, 'p, 'f) ann) ⇒ bool" where
"inter_aux_Par Γ Θ F ≡
λ(cs, as, c, a). ∀i < length cs. interfree_aux Γ Θ F (cs ! i, as ! i, c, a)"
lemma inter_aux_Par_Empty: "inter_aux_Par Γ Θ F ([], [], c, a)"
by(simp add:inter_aux_Par_def)
lemma inter_aux_Par_List:
"⟦ interfree_aux Γ Θ F (x, a, y, a');
inter_aux_Par Γ Θ F (xs, as, y, a')⟧
⟹ inter_aux_Par Γ Θ F (x#xs, a#as, y, a')"
apply (simp add: inter_aux_Par_def)
apply (rule allI)
apply (rename_tac v)
apply (case_tac v)
apply simp_all
done
lemma inter_aux_Par_Map: "∀k. i≤k ∧ k<j ⟶ interfree_aux Γ Θ F (c k, Q k, x, a)
⟹ inter_aux_Par Γ Θ F (map c [i..<j], map Q [i..<j], x, a)"
by(force simp add: inter_aux_Par_def less_diff_conv)
lemma Parallel_inter_aux:
"⟦ interfree_aux_right Γ Θ F (Q, com, ann);
interfree_aux_right Γ Θ F (A, com, ann);
interfree_aux_right Γ Θ F (⋂ (set (map postcond as)), com, ann);
inter_aux_Par Γ Θ F (cs, as, com, ann) ⟧ ⟹
interfree_aux Γ Θ F (Parallel cs, (AnnPar as, Q, A), com, ann)"
apply (clarsimp simp: interfree_aux_def interfree_aux_right_def inter_aux_Par_def)
by (erule assertionsR.cases; fastforce)
definition interfree_swap :: "('s,'p,'f) body ⇒ ('s,'p,'f) proc_assns ⇒ 'f set ⇒ (('s, 'p, 'f) com × (('s, 'p, 'f) ann × 's assn × 's assn) × ('s, 'p, 'f) com list × (('s, 'p, 'f) ann × 's assn × 's assn) list) ⇒ bool" where
"interfree_swap Γ Θ F ≡ λ(x, a, xs, as). ∀y < length xs. interfree_aux Γ Θ F (x, a, xs ! y, pres (as ! y))
∧ interfree_aux Γ Θ F (xs ! y, as ! y, x, fst a)"
lemma interfree_swap_Empty: "interfree_swap Γ Θ F (x, a, [], [])"
by(simp add:interfree_swap_def)
lemma interfree_swap_List:
"⟦ interfree_aux Γ Θ F (x, a, y, fst (a'));
interfree_aux Γ Θ F (y, a', x, fst a);
interfree_swap Γ Θ F (x, a, xs, as)⟧
⟹ interfree_swap Γ Θ F (x, a, y#xs, a'#as)"
apply (simp add: interfree_swap_def)
apply (rule allI)
apply (rename_tac v)
apply (case_tac v)
apply simp_all
done
lemma interfree_swap_Map: "∀k. i≤k ∧ k<j ⟶ interfree_aux Γ Θ F (x, a, c k, fst (Q k))
∧ interfree_aux Γ Θ F (c k, (Q k), x, fst a)
⟹ interfree_swap Γ Θ F (x, a, map c [i..<j], map Q [i..<j])"
by(force simp add: interfree_swap_def less_diff_conv)
lemma interfree_Empty: "interfree Γ Θ F [] []"
by(simp add:interfree_def)
lemma interfree_List:
"⟦ interfree_swap Γ Θ F (x, a, xs, as); interfree Γ Θ F as xs ⟧ ⟹ interfree Γ Θ F (a#as) (x#xs)"
apply (simp add: interfree_swap_def interfree_def)
apply clarify
apply (rename_tac i j)
apply (case_tac i)
apply (case_tac j)
apply simp_all
apply (case_tac j)
apply simp_all
done
lemma interfree_Map:
"(∀i j. a≤i ∧ i<b ∧ a≤j ∧ j<b ∧ i≠j ⟶ interfree_aux Γ Θ F (c i, A i, c j, pres (A j)))
⟹ interfree Γ Θ F (map (λk. A k) [a..<b]) (map (λk. c k) [a..<b])"
by (force simp add: interfree_def less_diff_conv)
lemma list_lemmas: "length []=0" "length (x#xs) = Suc(length xs)"
"(x#xs) ! 0 = x" "(x#xs) ! Suc n = xs ! n"
by simp_all
lemma le_Suc_eq_insert: "{i. i <Suc n} = insert n {i. i< n}"
by auto
lemmas primrecdef_list = "pre.simps" strengthen_pre.simps
lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append
lemmas my_simp_list = list_lemmas fst_conv snd_conv
not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject
Collect_mem_eq ball_simps option.simps primrecdef_list
ML ‹val hyp_tac = CSUBGOAL (fn (prem,i) => PRIMITIVE (fn thm =>
let
val thm' = Thm.permute_prems 0 (i-1) thm |> Goal.protect 1
val asm = Thm.assume prem
in
case (try (fn thm' => (Thm.implies_elim thm' asm)) thm') of
SOME thm => thm |> Goal.conclude |> Thm.permute_prems 0 (~(i-1))
| NONE => error ("hyp_tac failed:" ^ (@{make_string} (thm',asm)))
end
))
›
ML ‹
fun remove_single_Bound_mem ctxt = SUBGOAL (fn (t, i) => let
val prems = Logic.strip_assums_hyp t
val concl = Logic.strip_assums_concl t
fun bd_member t = (case HOLogic.dest_Trueprop t
of Const (@{const_name "Set.member"}, _) $ Bound j $ _ => SOME j
| _ => NONE) handle TERM _ => NONE
in filter_prems_tac ctxt
(fn prem => case bd_member prem of NONE => true
| SOME j => let val xs = (filter (fn t => loose_bvar1 (t, j)) (concl :: prems))
in length xs <> 1 end)
i
end handle Subscript => no_tac)
›
named_theorems proc_simp
named_theorems oghoare_simps
lemmas guards.simps[oghoare_simps add]
ann_guards.simps[oghoare_simps add]
ML ‹
fun rt ctxt t i =
resolve_tac ctxt [t] i
fun rts ctxt xs i =
resolve_tac ctxt xs i
fun conjI_Tac ctxt tac i st = st |>
( (EVERY [rt ctxt conjI i,
conjI_Tac ctxt tac (i+1),
tac i]) ORELSE (tac i) )
fun get_oghoare_simps ctxt =
Proof_Context.get_thms ctxt "oghoare_simps"
fun simp ctxt extra =
simp_tac (put_simpset HOL_basic_ss ctxt addsimps extra)
fun simp_only ctxt simps =
simp_tac ((clear_simpset ctxt) addsimps simps)
fun prod_sel_simp ctxt =
simp_only ctxt @{thms prod.sel}
fun oghoare_simp ctxt =
simp_only ctxt (get_oghoare_simps ctxt)
fun ParallelConseq ctxt =
clarsimp_tac (put_simpset HOL_basic_ss ctxt addsimps (@{thms ParallelConseq_list} @ @{thms my_simp_list}))
val enable_trace = false;
fun trace str = if enable_trace then tracing str else ();
fun HoareRuleTac (ctxt' as (ctxt,args)) i st =
(Cache_Tactics.SUBGOAL_CACHE (nth args 0)
(fn (_,i) => (SUBGOAL (fn (_,i) =>
(EVERY[rts ctxt @{thms Seq Catch SeqSeq SeqCatch} i,
HoareRuleTac ctxt' (i+1),
HoareRuleTac ctxt' i]
ORELSE
(FIRST[rts ctxt (@{thms SkipRule SeqSkipRule}) i,
rts ctxt (@{thms BasicRule SeqBasicRule}) i,
rts ctxt (@{thms ThrowRule SeqThrowRule}) i,
rts ctxt (@{thms SpecRule SeqSpecRule}) i,
EVERY[rt ctxt (@{thm SeqParallel}) i,
HoareRuleTac ctxt' (i+1)],
EVERY[rt ctxt (@{thm ParallelConseqRule}) i,
ParallelConseq ctxt (i+2),
ParallelConseq ctxt (i+1),
ParallelTac ctxt' i],
EVERY[rt ctxt (@{thm CondRule}) i,
HoareRuleTac ctxt' (i+2),
HoareRuleTac ctxt' (i+1)],
EVERY[rt ctxt @{thm SeqCondRule} i,
HoareRuleTac ctxt' (i+1),
HoareRuleTac ctxt' i],
EVERY[rt ctxt (@{thm WhileRule}) i,
HoareRuleTac ctxt' (i+3)],
EVERY[rt ctxt (@{thm SeqWhileRule}) i,
HoareRuleTac ctxt' i],
EVERY[rt ctxt (@{thm AwaitRule}) i,
HoareRuleTac ctxt' (i+1),
simp ctxt (@{thms atom_com.simps}) i],
EVERY[rts ctxt (@{thms CallRule SeqCallRule}) i,
Call_asm_inst ctxt (i+2),
HoareRuleTac ctxt' (i+1)],
EVERY[rts ctxt (@{thms DynComRule SeqDynComRule}) i,
HoareRuleTac ctxt' (i+1)],
EVERY[rts ctxt (@{thms GuardRule}) i,
HoareRuleTac ctxt' (i+2)],
K all_tac i ])))
THEN_ALL_NEW hyp_tac) i)) i st
and Call_asm_inst ctxt i =
let val proc_simps = Proof_Context.get_thms ctxt "proc_simp" @ @{thms list_lemmas} in
EVERY[rts ctxt proc_simps (i+3),
rts ctxt proc_simps (i+2),
rts ctxt proc_simps (i+1),
ParallelConseq ctxt i]
end
and ParallelTac (ctxt' as (ctxt,args)) i =
EVERY[rt ctxt (@{thm ParallelRule}) i,
ParallelConseq ctxt (i+2),
interfree_Tac ctxt' (i+1),
ParallelConseq ctxt i,
MapAnn_Tac ctxt' i]
and MapAnn_Tac (ctxt' as (ctxt,args)) i st = st |>
(FIRST[rt ctxt (@{thm MapAnnEmpty}) i,
EVERY[rt ctxt (@{thm MapAnnList}) i,
MapAnn_Tac ctxt' (i+1),
HoareRuleTac ctxt' i],
EVERY[rt ctxt (@{thm MapAnnMap}) i,
rt ctxt (@{thm allI}) i, rt ctxt (@{thm impI}) i,
HoareRuleTac ctxt' i]])
and interfree_Tac (ctxt' as (ctxt,args)) i st = st |>
(FIRST[rt ctxt (@{thm interfree_Empty}) i,
EVERY[rt ctxt (@{thm interfree_List}) i,
interfree_Tac ctxt' (i+1),
interfree_swap_Tac ctxt' i],
EVERY[rt ctxt (@{thm interfree_Map}) i,
rt ctxt (@{thm allI}) i, rt ctxt (@{thm allI}) i, rt ctxt (@{thm impI}) i,
interfree_aux_Tac ctxt' i ]])
and interfree_swap_Tac (ctxt' as (ctxt,args)) i st = st |>
(FIRST[rt ctxt (@{thm interfree_swap_Empty}) i,
EVERY[rt ctxt (@{thm interfree_swap_List}) i,
interfree_swap_Tac ctxt' (i+2),
interfree_aux_Tac ctxt' (i+1),
interfree_aux_Tac ctxt' i ],
EVERY[rt ctxt (@{thm interfree_swap_Map}) i,
rt ctxt (@{thm allI}) i, rt ctxt (@{thm impI}) i,
conjI_Tac ctxt (interfree_aux_Tac ctxt') i]])
and inter_aux_Par_Tac (ctxt' as (ctxt,args)) i st = st |>
(FIRST[rt ctxt (@{thm inter_aux_Par_Empty}) i,
EVERY[rt ctxt (@{thm inter_aux_Par_List}) i,
inter_aux_Par_Tac ctxt' (i+1),
interfree_aux_Tac ctxt' i ],
EVERY[rt ctxt (@{thm inter_aux_Par_Map}) i,
rt ctxt (@{thm allI}) i, rt ctxt (@{thm impI}) i,
interfree_aux_Tac ctxt' i]])
and interfree_aux_Tac ctxt' i = dest_inter_aux_Tac ctxt' i
and dest_inter_aux_Tac (ctxt' as (ctxt,args)) i st =
(Cache_Tactics.SUBGOAL_CACHE (nth args 1)
(fn (_,i) => (SUBGOAL (fn (_,i) =>
(TRY (REPEAT (EqSubst.eqsubst_tac ctxt [0] @{thms prod.sel} i)) THEN
FIRST[EVERY[rts ctxt (@{thms Skip_inter_aux Throw_inter_aux Basic_inter_aux Spec_inter_aux}) i,
dest_inter_right_Tac ctxt' (i+2),
dest_inter_right_Tac ctxt' (i+1),
dest_inter_right_Tac ctxt' i],
EVERY[rts ctxt (@{thms Seq_inter_aux Catch_inter_aux}) i,
dest_inter_aux_Tac ctxt' (i+1),
dest_inter_aux_Tac ctxt' (i+0)],
EVERY[rt ctxt (@{thm Cond_inter_aux}) i,
dest_inter_aux_Tac ctxt' (i+2),
dest_inter_aux_Tac ctxt' (i+1),
dest_inter_right_Tac ctxt' i],
EVERY[rt ctxt (@{thm While_inter_aux}) i,
dest_inter_aux_Tac ctxt' (i+2),
dest_inter_right_Tac ctxt' (i+1),
dest_inter_right_Tac ctxt' i],
EVERY[rt ctxt (@{thm Await_inter_aux}) i,
dest_inter_right_Tac ctxt' (i+2),
dest_inter_right_Tac ctxt' (i+1),
dest_inter_right_Tac ctxt' (i+0)],
EVERY[rt ctxt (@{thm Call_inter_aux}) i,
Call_asm_inst ctxt (i+2),
dest_inter_aux_Tac ctxt' (i+1),
dest_inter_right_Tac ctxt' i],
EVERY[rt ctxt (@{thm DynCom_inter_aux}) i,
dest_inter_aux_Tac ctxt' (i+3),
dest_inter_right_Tac ctxt' (i+2),
dest_inter_right_Tac ctxt' (i+1),
dest_inter_right_Tac ctxt' i],
EVERY[rt ctxt (@{thm Guard_inter_aux}) i,
dest_inter_aux_Tac ctxt' (i+2),
dest_inter_right_Tac ctxt' (i+1),
dest_inter_right_Tac ctxt' i],
EVERY[rt ctxt (@{thm Parallel_inter_aux}) i,
inter_aux_Par_Tac ctxt' (i+3),
dest_inter_right_Tac ctxt' (i+2),
dest_inter_right_Tac ctxt' (i+1),
dest_inter_right_Tac ctxt' i],
dest_inter_right_Tac ctxt' i]))
THEN_ALL_NEW hyp_tac) i)) i st
and dest_inter_right_Tac (ctxt' as (ctxt,args)) i st =
(Cache_Tactics.SUBGOAL_CACHE (nth args 2)
(fn (_,i) =>
FIRST[EVERY[rts ctxt (@{thms Skip_inter_right Throw_inter_right
Basic_inter_right Spec_inter_right}) i,
HoareRuleTac ctxt' i],
EVERY[rts ctxt (@{thms Seq_inter_right Catch_inter_right}) i,
dest_inter_right_Tac ctxt' (i+1),
dest_inter_right_Tac ctxt' i],
EVERY[rt ctxt (@{thm Cond_inter_right}) i,
dest_inter_right_Tac ctxt' (i+1),
dest_inter_right_Tac ctxt' i],
EVERY[rt ctxt (@{thm While_inter_right}) i,
dest_inter_right_Tac ctxt' i],
EVERY[rt ctxt (@{thm Await_inter_right}) i,
HoareRuleTac ctxt' (i+1),
simp ctxt (@{thms atom_com.simps}) i],
EVERY[rt ctxt (@{thm Call_inter_right}) i,
Call_asm_inst ctxt (i+1),
dest_inter_right_Tac ctxt' i],
EVERY[rt ctxt (@{thm DynCom_inter_right}) i,
dest_inter_right_Tac ctxt' i],
EVERY[rt ctxt (@{thm Guard_inter_right}) i,
dest_inter_right_Tac ctxt' i],
rt ctxt (@{thm Parallel_inter_right_empty}) i,
EVERY[rt ctxt (@{thm Parallel_inter_right_List}) i,
dest_inter_right_Tac ctxt' (i+1),
dest_inter_right_Tac ctxt' i],
EVERY[rt ctxt (@{thm Parallel_inter_right_Map}) i,
rt ctxt (@{thm allI}) i, rt ctxt (@{thm impI}) i,
dest_inter_right_Tac ctxt' i],
K all_tac i])) i st
›
ML ‹
fun oghoare_tac ctxt =
SUBGOAL (fn (_, i) =>
TRY (prod_sel_simp ctxt i)
THEN TRY (oghoare_simp ctxt i)
THEN Cache_Tactics.cacheify_tactic 3 HoareRuleTac ctxt i)
fun oghoare_tac' ctxt i goal =
let
val results = oghoare_tac ctxt i goal;
in
if (Thm.eq_thm (results |> Seq.hd, goal) handle Option => false)
then no_tac goal
else results
end;
fun oghoare_parallel_tac ctxt i =
TRY (oghoare_simp ctxt i) THEN
Cache_Tactics.cacheify_tactic 3 ParallelTac ctxt i
fun oghoare_interfree_tac ctxt i =
TRY (oghoare_simp ctxt i) THEN
Cache_Tactics.cacheify_tactic 3 interfree_Tac ctxt i
fun oghoare_interfree_aux_tac ctxt i =
TRY (oghoare_simp ctxt i) THEN
Cache_Tactics.cacheify_tactic 3 interfree_aux_Tac ctxt i
›
method_setup oghoare = ‹
Scan.succeed (SIMPLE_METHOD' o oghoare_tac')›
"verification condition generator for the oghoare logic"
method_setup oghoare_parallel = ‹
Scan.succeed (SIMPLE_METHOD' o oghoare_parallel_tac)›
"verification condition generator for the oghoare logic"
method_setup oghoare_interfree = ‹
Scan.succeed (SIMPLE_METHOD' o oghoare_interfree_tac)›
"verification condition generator for the oghoare logic"
method_setup oghoare_interfree_aux = ‹
Scan.succeed (SIMPLE_METHOD' o oghoare_interfree_aux_tac)›
"verification condition generator for the oghoare logic"
end