# Theory OG_Tran

Up to index of Isabelle/HOL/HoareParallel

theory OG_Tran
imports OG_Com
begin

    header {* \section{Operational Semantics} *}

    theory OG_Tran imports OG_Com begin

    types
      'a ann_com_op = "('a ann_com) option"
      'a ann_triple_op = "('a ann_com_op × 'a assn)"

    consts com :: "'a ann_triple_op => 'a ann_com_op"
    primrec "com (c, q) = c"

    consts post :: "'a ann_triple_op => 'a assn"
    primrec "post (c, q) = q"

    constdefs
      All_None :: "'a ann_triple_op list => bool"
      "All_None Ts ≡ ∀(c, q) ∈ set Ts. c = None"

    subsection {* The Transition Relation *}

    consts
      ann_transition :: "(('a ann_com_op × 'a) × ('a ann_com_op × 'a)) set"
      transition :: "(('a com × 'a) × ('a com × 'a)) set"

    syntax
      "_ann_transition" :: "('a ann_com_op × 'a) => ('a ann_com_op × 'a) => bool"
                               ("_ -1-> _"[81,81] 100)
      "_ann_transition_n" :: "('a ann_com_op × 'a) => nat => ('a ann_com_op × 'a)
                               => bool"  ("_ -_-> _"[81,81] 100)
      "_ann_transition_*" :: "('a ann_com_op × 'a) => ('a ann_com_op × 'a) => bool"
                               ("_ -*-> _"[81,81] 100)

      "_transition" :: "('a com × 'a) => ('a com × 'a) => bool"  ("_ -P1-> _"[81,81] 100)
      "_transition_n" :: "('a com × 'a) => nat => ('a com × 'a) => bool"
                              ("_ -P_-> _"[81,81,81] 100)
      "_transition_*" :: "('a com × 'a) => ('a com × 'a) => bool"  ("_ -P*-> _"[81,81] 100)

    text {* The corresponding syntax translations are: *}

    translations
      "con_0 -1-> con_1" \<rightleftharpoons> "(con_0, con_1) ∈ ann_transition"
      "con_0 -n-> con_1" \<rightleftharpoons> "(con_0, con_1) ∈ ann_transition^n"
      "con_0 -*-> con_1" \<rightleftharpoons> "(con_0, con_1) ∈ ann_transition*"

      "con_0 -P1-> con_1" \<rightleftharpoons> "(con_0, con_1) ∈ transition"
      "con_0 -Pn-> con_1" \<rightleftharpoons> "(con_0, con_1) ∈ transition^n"
      "con_0 -P*-> con_1" \<rightleftharpoons> "(con_0, con_1) ∈ transition*"

    inductive ann_transition  transition
    intros
      AnnBasic:  "(Some (AnnBasic r f), s) -1-> (None, f s)"

      AnnSeq1: "(Some c0, s) -1-> (None, t) ==>
                   (Some (AnnSeq c0 c1), s) -1-> (Some c1, t)"
      AnnSeq2: "(Some c0, s) -1-> (Some c2, t) ==>
                   (Some (AnnSeq c0 c1), s) -1-> (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-> (None, t)"

      Parallel: "[| i<length Ts; Ts!i = (Some c, q); (Some c, s) -1-> (r, t) |]
                  ==> (Parallel Ts, s) -P1-> (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"

    subsection {* Definition of Semantics *}

    constdefs
      ann_sem :: "'a ann_com => 'a => 'a set"
      "ann_sem c ≡ λs. {t. (Some c, s) -*-> (None, t)}"

      ann_SEM :: "'a ann_com => 'a set => 'a set"
      "ann_SEM c S ≡ \<Union>ann_sem c ` S"

      sem :: "'a com => 'a => 'a set"
      "sem c ≡ λs. {t. ∃Ts. (c, s) -P*-> (Parallel Ts, t) ∧ All_None Ts}"

      SEM :: "'a com => 'a set => 'a set"
      "SEM c S ≡ \<Union>sem c ` S "

    syntax "_Omega" :: "'a com"    ("Ω" 63)
    translations  "Ω" \<rightleftharpoons> "While UNIV UNIV (Basic id)"

    consts fwhile :: "'a bexp => 'a com => nat => 'a com"
    primrec
       "fwhile b c 0 = Ω"
       "fwhile b c (Suc n) = Cond b (Seq c (fwhile b c n)) (Basic id)"

    subsubsection {* Proofs *}

    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 rel_pow_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 rel_pow_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_rel_pow)
    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 {* 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*-> (Parallel Ss, s3); All_None Ss |]
     ==> (Seq c1 c2, s1) -P*-> (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) --> (∃y m Rs. (c1,s) -P*-> (Parallel Rs, y) ∧
      (All_None Rs) ∧ (c2, y) -Pm-> (Parallel Ts, t) ∧  m ≤ n)"
    apply(induct "n")
     apply(force)
    apply(safe dest!: rel_pow_Suc_D2)
    apply(erule transition_cases,simp_all)
     apply (fast intro!: le_SucI)
    apply (fast intro!: le_SucI elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
    done

    lemma L3_5ii_lemma3:
     "[|(Seq c1 c2,s) -P*-> (Parallel Ts,t); All_None Ts|] ==>
        (∃y Rs. (c1,s) -P*-> (Parallel Rs,y) ∧ All_None Rs
       ∧ (c2,y) -P*-> (Parallel Ts,t))"
    apply(drule rtrancl_imp_UN_rel_pow)
    apply(fast dest: L3_5ii_lemma2 rel_pow_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 rel_pow_E2)
     apply simp_all
    apply(erule transition_cases)
     apply simp_all
    apply(erule rel_pow_E2)
     apply(simp add: Id_def)
    apply(erule transition_cases,simp_all)
    apply clarify
    apply(erule transition_cases,simp_all)
    apply(erule rel_pow_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_rel_pow 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 -->
      (∃k. (fwhile b c k, s) -P*-> (Parallel Ts, t))"
    apply(rule nat_less_induct)
    apply safe
    apply(erule rel_pow_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*-> (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_rel_pow)
    apply clarify
    apply(erule rel_pow_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. (\<Union>k. SEM (fwhile b c k) x))"
    apply(rule ext)
    apply (simp add: SEM_def sem_def)
    apply safe
     apply(drule rtrancl_imp_UN_rel_pow,simp)
     apply clarify
     apply(fast dest:L3_5v_lemma4)
    apply(fast intro: L3_5v_lemma5)
    done

    section {* Validity of Correctness Formulas *}

    constdefs
      com_validity :: "'a assn => 'a com => 'a assn => bool"  ("(3\<parallel>= _// _//_)" [90,55,90] 50)
      "\<parallel>= p c q ≡ SEM c p ⊆ q"

      ann_com_validity :: "'a ann_com => 'a assn => bool"   ("\<Turnstile> _ _" [60,90] 45)
      "\<Turnstile> c q ≡ ann_SEM c (pre c) ⊆ q"

    end

### The Transition Relation

### Definition of Semantics

#### Proofs

lemmas transition_cases:

      [| (Parallel T, s) -P1-> t;
         !!c i q r t.
            [| i < length T; T ! i = (Some c, q);
               ((Some c, s), r, t) ∈ ann_transition;
               t = (Parallel (T[i := (r, q)]), t) |]
            ==> P |]
      ==> P

      [| (Basic f, s) -P1-> t; t = (Parallel [], f s) ==> P |] ==> P

      [| (Seq c1.0 c2.0, s) -P1-> t;
         !!Ts. [| All_None Ts; t = (c2.0, s); c1.0 = Parallel Ts |] ==> P;
         !!c2 t. [| ((c1.0, s), c2, t) ∈ transition; t = (Seq c2 c2.0, t) |] ==> P |]
      ==> P

      [| (Cond b c1.0 c2.0, s) -P1-> t; [| s ∈ b; t = (c1.0, s) |] ==> P;
         [| s ∉ b; t = (c2.0, s) |] ==> P |]
      ==> P

      [| (While b i c, s) -P1-> t; [| s ∉ b; t = (Parallel [], s) |] ==> P;
         [| s ∈ b; t = (Seq c (While b i c), s) |] ==> P |]
      ==> P

lemma Parallel_empty_lemma:

      ((Parallel [], s), Parallel Ts, t) ∈ transition ^ n ==> Ts = [] ∧ n = 0 ∧ s = t

lemma Parallel_AllNone_lemma:

      [| All_None Ss; ((Parallel Ss, s), Parallel Ts, t) ∈ transition ^ n |]
      ==> Ts = Ss ∧ n = 0 ∧ s = t

lemma Parallel_AllNone:

      All_None Ts ==> SEM (Parallel Ts) X = X

lemma Parallel_empty:

      Ts = [] ==> SEM (Parallel Ts) X = X

lemma L3_5i:

      X ⊆ Y ==> SEM c X ⊆ SEM c Y

lemma L3_5ii_lemma1:

      [| ((c1.0, s1.0), Parallel Ts, s2.0) ∈ transition*; All_None Ts;
         ((c2.0, s2.0), Parallel Ss, s3.0) ∈ transition*; All_None Ss |]
      ==> ((Seq c1.0 c2.0, s1.0), Parallel Ss, s3.0) ∈ transition*

lemma L3_5ii_lemma2:

      [| ((Seq c1.0 c2.0, s), Parallel Ts, t) ∈ transition ^ n; All_None Ts |]
      ==> ∃y m Rs.
             ((c1.0, s), Parallel Rs, y) ∈ transition* ∧
             All_None Rs ∧ ((c2.0, y), Parallel Ts, t) ∈ transition ^ m ∧ m ≤ n

lemma L3_5ii_lemma3:

      [| ((Seq c1.0 c2.0, s), Parallel Ts, t) ∈ transition*; All_None Ts |]
      ==> ∃y Rs. ((c1.0, s), Parallel Rs, y) ∈ transition* ∧
                 All_None Rs ∧ ((c2.0, y), Parallel Ts, t) ∈ transition*

lemma L3_5ii:

      SEM (Seq c1.0 c2.0) X = SEM c2.0 (SEM c1.0 X)

lemma L3_5iii:

      SEM (Seq (Seq c1.0 c2.0) c3.0) X = SEM (Seq c1.0 (Seq c2.0 c3.0)) X

lemma L3_5iv:

      SEM (Cond b c1.0 c2.0) X = SEM c1.0 (X ∩ b) ∪ SEM c2.0 (X ∩ - b)

lemma L3_5v_lemma1:

      [| ((S, s), T, t) ∈ transition ^ n; S = Ω |]
      ==> ¬ (∃Rs. T = Parallel Rs ∧ All_None Rs)

lemma L3_5v_lemma2:

      [| ((Ω, s), Parallel Ts, t) ∈ transition*; All_None Ts |] ==> False

lemma L3_5v_lemma3:

      SEM (Ω) S = {}

lemma L3_5v_lemma4:

      [| ((While b i c, s), Parallel Ts, t) ∈ transition ^ n; All_None Ts |]
      ==> ∃k. ((fwhile b c k, s), Parallel Ts, t) ∈ transition*

lemma L3_5v_lemma5:

      [| ((fwhile b c k, s), Parallel Ts, t) ∈ transition*; All_None Ts |]
      ==> ((While b i c, s), Parallel Ts, t) ∈ transition*

lemma L3_5v:

      SEM (While b i c) = (%x. UN k. SEM (fwhile b c k) x)

## Validity of Correctness Formulas