Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: OG_Hoare.thy Sprache: Isabelle

Original von: Isabelle^©

section \<open>The Proof System\<close>

theory OG_Hoare imports OG_Tran begin

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

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

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

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

definition interfree_aux :: "('a ann_com_op \ 'a assn \ 'a ann_com_op) \ bool" where
  "interfree_aux \ \(co, q, co'). co'= None \
                    (\<forall>(r,a) \<in> atomics (the co'). \<parallel>= (q \<inter> r) a q \<and>
                    (co = None \<or> (\<forall>p \<in> assertions (the co). \<parallel>= (p \<inter> r) a p)))"

definition interfree :: "(('a ann_triple_op) list) \ bool" where
  "interfree Ts \ \i j. i < length Ts \ j < length Ts \ i \ j \
                         interfree_aux (com (Ts!i), post (Ts!i), com (Ts!j)) "

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

| AnnSeq:   "\ \ c0 pre c1; \ c1 q \ \ \ (AnnSeq c0 c1) q"

| AnnCond1: "\ r \ b \ pre c1; \ c1 q; r \ -b \ pre c2; \ c2 q\
              \<Longrightarrow> \<turnstile> (AnnCond1 r b c1 c2) q"
| AnnCond2: "\ r \ b \ pre c; \ c q; r \ -b \ q \ \ \ (AnnCond2 r b c) q"

| AnnWhile: "\ r \ i; i \ b \ pre c; \ c i; i \ -b \ q \
              \<Longrightarrow> \<turnstile> (AnnWhile r b i c) q"

| AnnAwait:  "\ atom_com c; \- (r \ b) c q \ \ \ (AnnAwait r b c) q"

| AnnConseq: "\\ c q; q \ q' \ \ \ c q'"

| Parallel: "\ \ic q. Ts!i = (Some c, q) \ \ c q; interfree Ts \
           \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts!i))))
                     Parallel Ts
                  (\<Inter>i\<in>{i. i<length Ts}. post(Ts!i))"

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

| Seq:    "\ \- p c1 r; \- r c2 q \ \ \- p (Seq c1 c2) q "

| Cond:   "\ \- (p \ b) c1 q; \- (p \ -b) c2 q \ \ \- p (Cond b c1 c2) q"

| While:  "\ \- (p \ b) c p \ \ \- p (While b i c) (p \ -b)"

| Conseq: "\ p' \ p; \- p c q ; q \ q' \ \ \- p' c q'"

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

lemmas [cong del] = if_weak_cong

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

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

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

subsection \<open>Soundness of the System for Atomic Programs\<close>

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

lemma SEM_fwhile: "SEM S (p \ b) \ p \ SEM (fwhile b S k) p \ (p \ -b)"
apply (induct "k")
apply(simp (no_asm) add: L3_5v_lemma3)
apply(simp (no_asm) add: L3_5iv L3_5ii Parallel_empty)
apply(rule conjI)
apply (blast dest: L3_5i)
apply(simp add: SEM_def sem_def id_def)
apply (auto dest: Basic_ntran rtrancl_imp_UN_relpow)
apply blast
done

lemma atom_hoare_sound [rule_format]:
" \- p c q \ atom_com(c) \ \= p c q"
apply (unfold com_validity_def)
apply(rule oghoare_induct)
apply simp_all
\<comment> \<open>Basic\<close>
    apply(simp add: SEM_def sem_def)
    apply(fast dest: rtrancl_imp_UN_relpow Basic_ntran)
\<comment> \<open>Seq\<close>
   apply(rule impI)
   apply(rule subset_trans)
    prefer 2 apply simp
   apply(simp add: L3_5ii L3_5i)
\<comment> \<open>Cond\<close>
  apply(simp add: L3_5iv)
\<comment> \<open>While\<close>
apply (force simp add: L3_5v dest: SEM_fwhile)
\<comment> \<open>Conseq\<close>
apply(force simp add: SEM_def sem_def)
done

subsection \<open>Soundness of the System for Component Programs\<close>

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

text \<open>Strong Soundness for Component Programs:\<close>

lemma ann_hoare_case_analysis [rule_format]: "\ C q' \
  ((\<forall>r f. C = AnnBasic r f \<longrightarrow> (\<exists>q. r \<subseteq> {s. f s \<in> q} \<and> q \<subseteq> q')) \<and>
  (\<forall>c0 c1. C = AnnSeq c0 c1 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<turnstile> c0 pre c1 \<and> \<turnstile> c1 q)) \<and>
  (\<forall>r b c1 c2. C = AnnCond1 r b c1 c2 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and>
  r \<inter> b \<subseteq> pre c1 \<and> \<turnstile> c1 q \<and> r \<inter> -b \<subseteq> pre c2 \<and> \<turnstile> c2 q)) \<and>
  (\<forall>r b c. C = AnnCond2 r b c \<longrightarrow>
  (\<exists>q. q \<subseteq> q' \<and> r \<inter> b \<subseteq> pre c  \<and> \<turnstile> c q \<and> r \<inter> -b \<subseteq> q)) \<and>
  (\<forall>r i b c. C = AnnWhile r b i c \<longrightarrow>
  (\<exists>q. q \<subseteq> q' \<and> r \<subseteq> i \<and> i \<inter> b \<subseteq> pre c \<and> \<turnstile> c i \<and> i \<inter> -b \<subseteq> q)) \<and>
  (\<forall>r b c. C = AnnAwait r b c \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<parallel>- (r \<inter> b) c q)))"
apply(rule ann_hoare_induct)
apply simp_all
apply(rule_tac x=q in exI,simp)+
apply(rule conjI,clarify,simp,clarify,rule_tac x=qa in exI,fast)+
apply(clarify,simp,clarify,rule_tac x=qa in exI,fast)
done

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

lemma Strong_Soundness_aux_aux [rule_format]:
"(co, s) -1\ (co', t) \ (\c. co = Some c \ s\ pre c \
(\<forall>q. \<turnstile> c q \<longrightarrow> (if co' = None then t\<in>q else t \<in> pre(the co') \<and> \<turnstile> (the co') q )))"
apply(rule ann_transition_transition.induct [THEN conjunct1])
apply simp_all
\<comment> \<open>Basic\<close>
         apply clarify
         apply(frule ann_hoare_case_analysis)
         apply force
\<comment> \<open>Seq\<close>
        apply clarify
        apply(frule ann_hoare_case_analysis,simp)
        apply(fast intro: AnnConseq)
       apply clarify
       apply(frule ann_hoare_case_analysis,simp)
       apply clarify
       apply(rule conjI)
        apply force
       apply(rule AnnSeq,simp)
       apply(fast intro: AnnConseq)
\<comment> \<open>Cond1\<close>
      apply clarify
      apply(frule ann_hoare_case_analysis,simp)
      apply(fast intro: AnnConseq)
     apply clarify
     apply(frule ann_hoare_case_analysis,simp)
     apply(fast intro: AnnConseq)
\<comment> \<open>Cond2\<close>
    apply clarify
    apply(frule ann_hoare_case_analysis,simp)
    apply(fast intro: AnnConseq)
   apply clarify
   apply(frule ann_hoare_case_analysis,simp)
   apply(fast intro: AnnConseq)
\<comment> \<open>While\<close>
  apply clarify
  apply(frule ann_hoare_case_analysis,simp)
  apply force
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply auto
apply(rule AnnSeq)
  apply simp
apply(rule AnnWhile)
  apply simp_all
\<comment> \<open>Await\<close>
apply(frule ann_hoare_case_analysis,simp)
apply clarify
apply(drule atom_hoare_sound)
apply simp
apply(simp add: com_validity_def SEM_def sem_def)
apply(simp add: Help All_None_def)
apply force
done

lemma Strong_Soundness_aux: "\ (Some c, s) -*\ (co, t); s \ pre c; \ c q \
  \<Longrightarrow> if co = None then t \<in> q else t \<in> pre (the co) \<and> \<turnstile> (the co) q"
apply(erule rtrancl_induct2)
apply simp
apply(case_tac "a")
apply(fast elim: ann_transition_cases)
apply(erule Strong_Soundness_aux_aux)
apply simp
apply simp_all
done

lemma Strong_Soundness: "\ (Some c, s)-*\(co, t); s \ pre c; \ c q \
  \<Longrightarrow> if co = None then t\<in>q else t \<in> pre (the co)"
apply(force dest:Strong_Soundness_aux)
done

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

subsection \<open>Soundness of the System for Parallel Programs\<close>

lemma Parallel_length_post_P1: "(Parallel Ts,s) -P1\ (R', t) \
  (\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and>
  (\<forall>i. i<length Ts \<longrightarrow> post(Rs ! i) = post(Ts ! i)))"
apply(erule transition_cases)
apply simp
apply clarify
apply(case_tac "i=ia")
apply simp+
done

lemma Parallel_length_post_PStar: "(Parallel Ts,s) -P*\ (R',t) \
  (\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and>
  (\<forall>i. i<length Ts \<longrightarrow> post(Ts ! i) = post(Rs ! i)))"
apply(erule rtrancl_induct2)
apply(simp_all)
apply clarify
apply simp
apply(drule Parallel_length_post_P1)
apply auto
done

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

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

lemma interfree_aux2 [rule_format]:
  "(c,s) -1\ (r,t) \ (interfree_aux(c, q, a) \ interfree_aux(r, q, a) )"
apply (rule ann_transition_transition.induct [THEN conjunct1])
apply(force simp add:interfree_aux_def)+
done

lemma interfree_lemma: "\ (Some c, s) -1\ (r, t);interfree Ts ; i
           Ts!i = (Some c, q) \<rbrakk> \<Longrightarrow> interfree (Ts[i:= (r, q)])"
apply(simp add: interfree_def)
apply clarify
apply(case_tac "i=j")
apply(drule_tac t = "ia" in not_sym)
apply simp_all
apply(force elim: interfree_aux1)
apply(force elim: interfree_aux2 simp add:nth_list_update)
done

text \<open>Strong Soundness Theorem for Parallel Programs:\<close>

lemma Parallel_Strong_Soundness_Seq_aux:
  "\interfree Ts; i
  \<Longrightarrow>  interfree (Ts[i:=(Some c0, pre c1)])"
apply(simp add: interfree_def)
apply clarify
apply(case_tac "i=j")
apply(force simp add: nth_list_update interfree_aux_def)
apply(case_tac "i=ia")
apply(erule_tac x=ia in allE)
apply(force simp add:interfree_aux_def assertions_lemma)
apply simp
done

lemma Parallel_Strong_Soundness_Seq [rule_format (no_asm)]:
"\ \i post(Ts!i)
  else b \<in> pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i));
  com(Ts ! i) = Some(AnnSeq c0 c1); i<length Ts; interfree Ts \<rbrakk> \<Longrightarrow>
(\<forall>ia<length Ts. (if com(Ts[i:=(Some c0, pre c1)]! ia) = None
  then b \<in> post(Ts[i:=(Some c0, pre c1)]! ia)
else b \<in> pre(the(com(Ts[i:=(Some c0, pre c1)]! ia))) \<and>
\<turnstile> the(com(Ts[i:=(Some c0, pre c1)]! ia)) post(Ts[i:=(Some c0, pre c1)]! ia)))
  \<and> interfree (Ts[i:= (Some c0, pre c1)])"
apply(rule conjI)
apply safe
apply(case_tac "i=ia")
  apply simp
  apply(force dest: ann_hoare_case_analysis)
apply simp
apply(fast elim: Parallel_Strong_Soundness_Seq_aux)
done

lemma Parallel_Strong_Soundness_aux_aux [rule_format]:
"(Some c, b) -1\ (co, t) \
  (\<forall>Ts. i<length Ts \<longrightarrow> com(Ts ! i) = Some c \<longrightarrow>
  (\<forall>i<length Ts. (if com(Ts ! i) = None then b\<in>post(Ts!i)
  else b\<in>pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i))) \<longrightarrow>
interfree Ts \<longrightarrow>
  (\<forall>j. j<length Ts \<and> i\<noteq>j \<longrightarrow> (if com(Ts!j) = None then t\<in>post(Ts!j)
  else t\<in>pre(the(com(Ts!j))) \<and> \<turnstile> the(com(Ts!j)) post(Ts!j))) )"
apply(rule ann_transition_transition.induct [THEN conjunct1])
apply safe
prefer 11
apply(rule TrueI)
apply simp_all
\<comment> \<open>Basic\<close>
   apply(erule_tac x = "i" in all_dupE, erule (1) notE impE)
   apply(erule_tac x = "j" in allE , erule (1) notE impE)
   apply(simp add: interfree_def)
   apply(erule_tac x = "j" in allE,simp)
   apply(erule_tac x = "i" in allE,simp)
   apply(drule_tac t = "i" in not_sym)
   apply(case_tac "com(Ts ! j)=None")
    apply(force intro: converse_rtrancl_into_rtrancl
          simp add: interfree_aux_def com_validity_def SEM_def sem_def All_None_def)
   apply(simp add:interfree_aux_def)
   apply clarify
   apply simp
   apply(erule_tac x="pre y" in ballE)
    apply(force intro: converse_rtrancl_into_rtrancl
          simp add: com_validity_def SEM_def sem_def All_None_def)
   apply(simp add:assertions_lemma)
\<comment> \<open>Seqs\<close>
  apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
  apply(drule  Parallel_Strong_Soundness_Seq,simp+)
apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
apply(drule  Parallel_Strong_Soundness_Seq,simp+)
\<comment> \<open>Await\<close>
apply(rule_tac x = "i" in allE , assumption , erule (1) notE impE)
apply(erule_tac x = "j" in allE , erule (1) notE impE)
apply(simp add: interfree_def)
apply(erule_tac x = "j" in allE,simp)
apply(erule_tac x = "i" in allE,simp)
apply(drule_tac t = "i" in not_sym)
apply(case_tac "com(Ts ! j)=None")
apply(force intro: converse_rtrancl_into_rtrancl simp add: interfree_aux_def
        com_validity_def SEM_def sem_def All_None_def Help)
apply(simp add:interfree_aux_def)
apply clarify
apply simp
apply(erule_tac x="pre y" in ballE)
apply(force intro: converse_rtrancl_into_rtrancl
       simp add: com_validity_def SEM_def sem_def All_None_def Help)
apply(simp add:assertions_lemma)
done

lemma Parallel_Strong_Soundness_aux [rule_format]:
"\(Ts',s) -P*\ (Rs',t); Ts' = (Parallel Ts); interfree Ts;
\<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. (Ts ! i) = (Some c, q) \<and> s\<in>(pre c) \<and> \<turnstile> c q ) \<rbrakk> \<Longrightarrow>
  \<forall>Rs. Rs' = (Parallel Rs) \<longrightarrow> (\<forall>j. j<length Rs \<longrightarrow>
  (if com(Rs ! j) = None then t\<in>post(Ts ! j)
  else t\<in>pre(the(com(Rs ! j))) \<and> \<turnstile> the(com(Rs ! j)) post(Ts ! j))) \<and> interfree Rs"
apply(erule rtrancl_induct2)
apply clarify
\<comment> \<open>Base\<close>
apply force
\<comment> \<open>Induction step\<close>
apply clarify
apply(drule Parallel_length_post_PStar)
apply clarify
apply (ind_cases "(Parallel Ts, s) -P1\ (Parallel Rs, t)" for Ts s Rs t)
apply(rule conjI)
apply clarify
apply(case_tac "i=j")
  apply(simp split del:if_split)
  apply(erule Strong_Soundness_aux_aux,simp+)
   apply force
  apply force
apply(simp split del: if_split)
apply(erule Parallel_Strong_Soundness_aux_aux)
apply(simp_all add: split del:if_split)
apply force
apply(rule interfree_lemma)
apply simp_all
done

lemma Parallel_Strong_Soundness:
"\(Parallel Ts, s) -P*\ (Parallel Rs, t); interfree Ts; j
  \<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. Ts ! i = (Some c, q) \<and> s\<in>pre c \<and> \<turnstile> c q) \<rbrakk> \<Longrightarrow>
  if com(Rs ! j) = None then t\<in>post(Ts ! j) else t\<in>pre (the(com(Rs ! j)))"
apply(drule  Parallel_Strong_Soundness_aux)
apply simp+
done

lemma oghoare_sound [rule_format]: "\- p c q \ \= p c q"
apply (unfold com_validity_def)
apply(rule oghoare_induct)
apply(rule TrueI)+
\<comment> \<open>Parallel\<close>
      apply(simp add: SEM_def sem_def)
      apply(clarify, rename_tac x y i Ts')
      apply(frule Parallel_length_post_PStar)
      apply clarify
      apply(drule_tac j=i in Parallel_Strong_Soundness)
         apply clarify
        apply simp
       apply force
      apply simp
      apply(erule_tac V = "\i. P i" for P in thin_rl)
      apply(drule_tac s = "length Rs" in sym)
      apply(erule allE, erule impE, assumption)
      apply(force dest: nth_mem simp add: All_None_def)
\<comment> \<open>Basic\<close>
    apply(simp add: SEM_def sem_def)
    apply(force dest: rtrancl_imp_UN_relpow Basic_ntran)
\<comment> \<open>Seq\<close>
   apply(rule subset_trans)
    prefer 2 apply assumption
   apply(simp add: L3_5ii L3_5i)
\<comment> \<open>Cond\<close>
  apply(simp add: L3_5iv)
\<comment> \<open>While\<close>
apply(simp add: L3_5v)
apply (blast dest: SEM_fwhile)
\<comment> \<open>Conseq\<close>
apply(auto simp add: SEM_def sem_def)
done

end

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.