Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: OG_Tran.thy Sprache: Isabelle

Original von: Isabelle^©

section \<open>Operational Semantics\<close>

theory OG_Tran imports OG_Com begin

type_synonym 'a ann_com_op = "('a ann_com) option"
type_synonym 'a ann_triple_op = "('a ann_com_op \<times> 'a assn)"

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 All_None :: "'a ann_triple_op list \ bool" where
  "All_None Ts \ \(c, q) \ set Ts. c = None"

subsection \<open>The Transition Relation\<close>

inductive_set
  ann_transition :: "(('a ann_com_op \ 'a) \ ('a ann_com_op \ 'a)) set"
  and transition :: "(('a com \ 'a) \ ('a com \ 'a)) set"
  and ann_transition' :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool"
    ("_ -1\ _"[81,81] 100)
  and transition' :: "('a com \<times> 'a) \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool"
    ("_ -P1\ _"[81,81] 100)
  and transitions :: "('a com \ 'a) \ ('a com \ 'a) \ bool"
    ("_ -P*\ _"[81,81] 100)
where
  "con_0 -1\ con_1 \ (con_0, con_1) \ ann_transition"
| "con_0 -P1\ con_1 \ (con_0, con_1) \ transition"
| "con_0 -P*\ con_1 \ (con_0, con_1) \ transition\<^sup>*"

| AnnBasic:  "(Some (AnnBasic r f), s) -1\ (None, f s)"

| AnnSeq1: "(Some c0, s) -1\ (None, t) \
               (Some (AnnSeq c0 c1), s) -1\<rightarrow> (Some c1, t)"
| AnnSeq2: "(Some c0, s) -1\ (Some c2, t) \
               (Some (AnnSeq c0 c1), s) -1\<rightarrow> (Some (AnnSeq c2 c1), t)"

| AnnCond1T: "s \ b \ (Some (AnnCond1 r b c1 c2), s) -1\ (Some c1, s)"
| AnnCond1F: "s \ b \ (Some (AnnCond1 r b c1 c2), s) -1\ (Some c2, s)"

| AnnCond2T: "s \ b \ (Some (AnnCond2 r b c), s) -1\ (Some c, s)"
| AnnCond2F: "s \ b \ (Some (AnnCond2 r b c), s) -1\ (None, s)"

| AnnWhileF: "s \ b \ (Some (AnnWhile r b i c), s) -1\ (None, s)"
| AnnWhileT: "s \ b \ (Some (AnnWhile r b i c), s) -1\
                         (Some (AnnSeq c (AnnWhile i b i c)), s)"

| AnnAwait: "\ s \ b; atom_com c; (c, s) -P*\ (Parallel [], t) \ \
                   (Some (AnnAwait r b c), s) -1\<rightarrow> (None, t)"

| Parallel: "\ i (r, t) \
              \<Longrightarrow> (Parallel Ts, s) -P1\<rightarrow> (Parallel (Ts [i:=(r, q)]), t)"

| Basic:  "(Basic f, s) -P1\ (Parallel [], f s)"

| Seq1:   "All_None Ts \ (Seq (Parallel Ts) c, s) -P1\ (c, s)"
| Seq2:   "(c0, s) -P1\ (c2, t) \ (Seq c0 c1, s) -P1\ (Seq c2 c1, t)"

| CondT: "s \ b \ (Cond b c1 c2, s) -P1\ (c1, s)"
| CondF: "s \ b \ (Cond b c1 c2, s) -P1\ (c2, s)"

| WhileF: "s \ b \ (While b i c, s) -P1\ (Parallel [], s)"
| WhileT: "s \ b \ (While b i c, s) -P1\ (Seq c (While b i c), s)"

monos "rtrancl_mono"

text \<open>The corresponding abbreviations are:\<close>

abbreviation
  ann_transition_n :: "('a ann_com_op \ 'a) \ nat \ ('a ann_com_op \ 'a)
                           \<Rightarrow> bool"  ("_ -_\<rightarrow> _"[81,81] 100)  where
  "con_0 -n\ con_1 \ (con_0, con_1) \ ann_transition ^^ n"

abbreviation
  ann_transitions :: "('a ann_com_op \ 'a) \ ('a ann_com_op \ 'a) \ bool"
                           ("_ -*\ _"[81,81] 100) where
  "con_0 -*\ con_1 \ (con_0, con_1) \ ann_transition\<^sup>*"

abbreviation
  transition_n :: "('a com \ 'a) \ nat \ ('a com \ 'a) \ bool"
                          ("_ -P_\ _"[81,81,81] 100) where
  "con_0 -Pn\ con_1 \ (con_0, con_1) \ transition ^^ n"

subsection \<open>Definition of Semantics\<close>

definition ann_sem :: "'a ann_com \ 'a \ 'a set" where
  "ann_sem c \ \s. {t. (Some c, s) -*\ (None, t)}"

definition ann_SEM :: "'a ann_com \ 'a set \ 'a set" where
  "ann_SEM c S \ \(ann_sem c ` S)"

definition sem :: "'a com \ 'a \ 'a set" where
  "sem c \ \s. {t. \Ts. (c, s) -P*\ (Parallel Ts, t) \ All_None Ts}"

definition SEM :: "'a com \ 'a set \ 'a set" where
  "SEM c S \ \(sem c ` S)"

abbreviation Omega :: "'a com"    ("\" 63)
  where "\ \ While UNIV UNIV (Basic id)"

primrec fwhile :: "'a bexp \ 'a com \ nat \ 'a com" where
    "fwhile b c 0 = \"
  | "fwhile b c (Suc n) = Cond b (Seq c (fwhile b c n)) (Basic id)"

subsubsection \<open>Proofs\<close>

declare ann_transition_transition.intros [intro]
inductive_cases transition_cases:
    "(Parallel T,s) -P1\ t"
    "(Basic f, s) -P1\ t"
    "(Seq c1 c2, s) -P1\ t"
    "(Cond b c1 c2, s) -P1\ t"
    "(While b i c, s) -P1\ t"

lemma Parallel_empty_lemma [rule_format (no_asm)]:
  "(Parallel [],s) -Pn\ (Parallel Ts,t) \ Ts=[] \ n=0 \ s=t"
apply(induct n)
apply(simp (no_asm))
apply clarify
apply(drule relpow_Suc_D2)
apply(force elim:transition_cases)
done

lemma Parallel_AllNone_lemma [rule_format (no_asm)]:
"All_None Ss \ (Parallel Ss,s) -Pn\ (Parallel Ts,t) \ Ts=Ss \ n=0 \ s=t"
apply(induct "n")
apply(simp (no_asm))
apply clarify
apply(drule relpow_Suc_D2)
apply clarify
apply(erule transition_cases,simp_all)
apply(force dest:nth_mem simp add:All_None_def)
done

lemma Parallel_AllNone: "All_None Ts \ (SEM (Parallel Ts) X) = X"
apply (unfold SEM_def sem_def)
apply auto
apply(drule rtrancl_imp_UN_relpow)
apply clarify
apply(drule Parallel_AllNone_lemma)
apply auto
done

lemma Parallel_empty: "Ts=[] \ (SEM (Parallel Ts) X) = X"
apply(rule Parallel_AllNone)
apply(simp add:All_None_def)
done

text \<open>Set of lemmas from Apt and Olderog "Verification of sequential
and concurrent programs", page 63.\

lemma L3_5i: "X\Y \ SEM c X \ SEM c Y"
apply (unfold SEM_def)
apply force
done

lemma L3_5ii_lemma1:
"\ (c1, s1) -P*\ (Parallel Ts, s2); All_None Ts;
  (c2, s2) -P*\<rightarrow> (Parallel Ss, s3); All_None Ss \<rbrakk>
\<Longrightarrow> (Seq c1 c2, s1) -P*\<rightarrow> (Parallel Ss, s3)"
apply(erule converse_rtrancl_induct2)
apply(force intro:converse_rtrancl_into_rtrancl)+
done

lemma L3_5ii_lemma2 [rule_format (no_asm)]:
"\c1 c2 s t. (Seq c1 c2, s) -Pn\ (Parallel Ts, t) \
  (All_None Ts) \<longrightarrow> (\<exists>y m Rs. (c1,s) -P*\<rightarrow> (Parallel Rs, y) \<and>
  (All_None Rs) \<and> (c2, y) -Pm\<rightarrow> (Parallel Ts, t) \<and>  m \<le> n)"
apply(induct "n")
apply(force)
apply(safe dest!: relpow_Suc_D2)
apply(erule transition_cases,simp_all)
apply (fast intro!: le_SucI)
apply (fast intro!: le_SucI elim!: relpow_imp_rtrancl converse_rtrancl_into_rtrancl)
done

lemma L3_5ii_lemma3:
"\(Seq c1 c2,s) -P*\ (Parallel Ts,t); All_None Ts\ \
    (\<exists>y Rs. (c1,s) -P*\<rightarrow> (Parallel Rs,y) \<and> All_None Rs
   \<and> (c2,y) -P*\<rightarrow> (Parallel Ts,t))"
apply(drule rtrancl_imp_UN_relpow)
apply(fast dest: L3_5ii_lemma2 relpow_imp_rtrancl)
done

lemma L3_5ii: "SEM (Seq c1 c2) X = SEM c2 (SEM c1 X)"
apply (unfold SEM_def sem_def)
apply auto
apply(fast dest: L3_5ii_lemma3)
apply(fast elim: L3_5ii_lemma1)
done

lemma L3_5iii: "SEM (Seq (Seq c1 c2) c3) X = SEM (Seq c1 (Seq c2 c3)) X"
apply (simp (no_asm) add: L3_5ii)
done

lemma L3_5iv:
"SEM (Cond b c1 c2) X = (SEM c1 (X \ b)) Un (SEM c2 (X \ (-b)))"
apply (unfold SEM_def sem_def)
apply auto
apply(erule converse_rtranclE)
prefer 2
apply (erule transition_cases,simp_all)
  apply(fast intro: converse_rtrancl_into_rtrancl elim: transition_cases)+
done

lemma  L3_5v_lemma1[rule_format]:
"(S,s) -Pn\ (T,t) \ S=\ \ (\(\Rs. T=(Parallel Rs) \ All_None Rs))"
apply (unfold UNIV_def)
apply(rule nat_less_induct)
apply safe
apply(erule relpow_E2)
apply simp_all
apply(erule transition_cases)
apply simp_all
apply(erule relpow_E2)
apply(simp add: Id_def)
apply(erule transition_cases,simp_all)
apply clarify
apply(erule transition_cases,simp_all)
apply(erule relpow_E2,simp)
apply clarify
apply(erule transition_cases)
apply simp+
    apply clarify
    apply(erule transition_cases)
apply simp_all
done

lemma L3_5v_lemma2: "\(\, s) -P*\ (Parallel Ts, t); All_None Ts \ \ False"
apply(fast dest: rtrancl_imp_UN_relpow L3_5v_lemma1)
done

lemma L3_5v_lemma3: "SEM (\) S = {}"
apply (unfold SEM_def sem_def)
apply(fast dest: L3_5v_lemma2)
done

lemma L3_5v_lemma4 [rule_format]:
"\s. (While b i c, s) -Pn\ (Parallel Ts, t) \ All_None Ts \
  (\<exists>k. (fwhile b c k, s) -P*\<rightarrow> (Parallel Ts, t))"
apply(rule nat_less_induct)
apply safe
apply(erule relpow_E2)
apply safe
apply(erule transition_cases,simp_all)
apply (rule_tac x = "1" in exI)
apply(force dest: Parallel_empty_lemma intro: converse_rtrancl_into_rtrancl simp add: Id_def)
apply safe
apply(drule L3_5ii_lemma2)
apply safe
apply(drule le_imp_less_Suc)
apply (erule allE , erule impE,assumption)
apply (erule allE , erule impE, assumption)
apply safe
apply (rule_tac x = "k+1" in exI)
apply(simp (no_asm))
apply(rule converse_rtrancl_into_rtrancl)
apply fast
apply(fast elim: L3_5ii_lemma1)
done

lemma L3_5v_lemma5 [rule_format]:
"\s. (fwhile b c k, s) -P*\ (Parallel Ts, t) \ All_None Ts \
  (While b i c, s) -P*\<rightarrow> (Parallel Ts,t)"
apply(induct "k")
apply(force dest: L3_5v_lemma2)
apply safe
apply(erule converse_rtranclE)
apply simp_all
apply(erule transition_cases,simp_all)
apply(rule converse_rtrancl_into_rtrancl)
  apply(fast)
apply(fast elim!: L3_5ii_lemma1 dest: L3_5ii_lemma3)
apply(drule rtrancl_imp_UN_relpow)
apply clarify
apply(erule relpow_E2)
apply simp_all
apply(erule transition_cases,simp_all)
apply(fast dest: Parallel_empty_lemma)
done

lemma L3_5v: "SEM (While b i c) = (\x. (\k. SEM (fwhile b c k) x))"
apply(rule ext)
apply (simp add: SEM_def sem_def)
apply safe
apply(drule rtrancl_imp_UN_relpow,simp)
apply clarify
apply(fast dest:L3_5v_lemma4)
apply(fast intro: L3_5v_lemma5)
done

section \<open>Validity of Correctness Formulas\<close>

definition com_validity :: "'a assn \ 'a com \ 'a assn \ bool" ("(3\= _// _//_)" [90,55,90] 50) where
  "\= p c q \ SEM c p \ q"

definition ann_com_validity :: "'a ann_com \ 'a assn \ bool" ("\ _ _" [60,90] 45) where
  "\ c q \ ann_SEM c (pre c) \ q"

end

¤ Dauer der Verarbeitung: 0.29 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.