Theory OG_Annotations

(*
 * Copyright 2016, Data61, CSIRO
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 *)
section ‹Annotations, assertions and associated operations›

theory OG_Annotations
imports SmallStep
begin

type_synonym 's assn = "'s set"

datatype ('s, dead 'p, dead 'f) ann =
    AnnExpr "'s assn" 
  | AnnRec "'s assn" "('s, 'p, 'f) ann"
  | AnnWhile "'s assn" "'s assn" "('s, 'p, 'f) ann"
  | AnnComp "('s, 'p, 'f) ann" "('s, 'p, 'f) ann"
  | AnnBin "'s assn" "('s, 'p, 'f) ann" "('s, 'p, 'f) ann"
  | AnnPar "(('s, 'p, 'f) ann × 's assn × 's assn) list"
  | AnnCall "'s assn" nat

type_synonym ('s, 'p, 'f) ann_triple = "('s, 'p, 'f) ann × 's assn × 's assn"

text ‹
 The list of ‹ann_triple› is useful if the code calls the same function multiple times
 and require different annotations for the function body each time.
›
type_synonym ('s,'p,'f) proc_assns = "'p ⇒ (('s, 'p, 'f) ann) list option"

abbreviation  (input) pres:: "('s, 'p, 'f) ann_triple ⇒ ('s, 'p, 'f) ann"
where "pres a ≡ fst a"

abbreviation (input) postcond :: "('s, 'p, 'f) ann_triple ⇒ 's assn"
where "postcond a ≡ fst (snd a)"

abbreviation (input) abrcond :: "('s, 'p, 'f) ann_triple ⇒ 's assn"
where "abrcond a ≡ snd (snd a)"

fun pre :: "('s, 'p, 'f) ann ⇒ 's assn" where
  "pre (AnnExpr r)      = r"                                                                                               
| "pre (AnnRec r e)     = r"
| "pre (AnnWhile r i e) = r"
| "pre (AnnComp e⇩1 e⇩2)   =  pre e⇩1"
| "pre (AnnBin r e⇩1 e⇩2)  = r"
| "pre (AnnPar as)      = ⋂ (pre ` set (map pres (as)))"
| "pre (AnnCall r n)    = r"

fun pre_par :: "('s, 'p, 'f) ann ⇒ bool" where
  "pre_par (AnnComp e⇩1 e⇩2) =  pre_par e⇩1"
| "pre_par (AnnPar as)  = True"
| "pre_par _    = False"

fun pre_set :: "('s, 'p, 'f) ann ⇒ ('s assn) set" where
  "pre_set (AnnExpr r)      = {r}"
| "pre_set (AnnRec r e)     = {r}"
| "pre_set (AnnWhile r i e) = {r}"
| "pre_set (AnnComp e⇩1 e⇩2)   =  pre_set e⇩1"
| "pre_set (AnnBin r e⇩1 e⇩2)  = {r}"
| "pre_set (AnnPar as)       = ⋃ (pre_set ` set (map pres (as)))"
(*| "pre_set (AnnPar e⇩1 e⇩2)    = pre_set (pres e⇩1) ∪ pre_set (pres e⇩2)" *)
| "pre_set (AnnCall r n)    = {r}"

lemma fst_BNFs[simp]:
  "a ∈ Basic_BNFs.fsts (a,b)"
   using fsts.intros by auto

lemma "¬pre_par c  ⟹ pre c ∈ pre_set c"
  by (induct c; simp)

lemma pre_set:
  "pre c = ⋂ (pre_set c)"
  by (induct c; fastforce)

lemma pre_imp_pre_set:
  "s ∈ pre c ⟹ a ∈ pre_set c ⟹ s ∈ a"
  by (simp add: pre_set)

abbreviation precond :: "('s, 'p, 'f) ann_triple ⇒ 's assn"
where "precond a ≡ pre (fst a)"

fun strengthen_pre :: "('s, 'p, 'f) ann ⇒ 's assn ⇒ ('s, 'p, 'f) ann" where
  "strengthen_pre (AnnExpr r)      r' = AnnExpr (r ∩ r')"                                                                                               
| "strengthen_pre (AnnRec r e)     r' = AnnRec (r ∩ r') e"
| "strengthen_pre (AnnWhile r i e) r' = AnnWhile (r ∩ r') i e"
| "strengthen_pre (AnnComp e⇩1 e⇩2)   r' = AnnComp (strengthen_pre e⇩1 r') e⇩2"
| "strengthen_pre (AnnBin r e⇩1 e⇩2) r' = AnnBin (r ∩ r') e⇩1 e⇩2"
| "strengthen_pre (AnnPar as)    r' = (AnnPar as)"
| "strengthen_pre (AnnCall r n)    r' = AnnCall (r ∩ r') n"

fun weaken_pre :: "('s, 'p, 'f) ann ⇒ 's assn ⇒ ('s, 'p, 'f) ann" where
  "weaken_pre (AnnExpr r)      r' = AnnExpr (r ∪ r')"                                                                                               
| "weaken_pre (AnnRec r e)     r' = AnnRec (r ∪ r') e"
| "weaken_pre (AnnWhile r i e) r' = AnnWhile (r ∪ r') i e"
| "weaken_pre (AnnComp e⇩1 e⇩2)   r' = AnnComp (weaken_pre e⇩1 r') e⇩2"
| "weaken_pre (AnnBin r e⇩1 e⇩2) r' = AnnBin (r ∪ r') e⇩1 e⇩2"
| "weaken_pre (AnnPar as)   r' = AnnPar as"
| "weaken_pre (AnnCall r n)    r' = AnnCall (r ∪ r') n"

lemma weaken_pre_empty[simp]:
  "weaken_pre r {} = r"
  by (induct r) auto

text ‹Annotations for call definition (see Language.thy)›
definition
 ann_call :: "'s assn ⇒ 's assn ⇒ nat ⇒  's assn ⇒'s assn ⇒  's assn ⇒ 's assn ⇒ ('s,'p,'f) ann"
where
 "ann_call init r n restoreq return restorea A ≡ 
  AnnRec init (AnnComp (AnnComp (AnnComp (AnnExpr init) (AnnCall r n)) (AnnComp (AnnExpr restorea) (AnnExpr A)))
          (AnnRec restoreq (AnnComp (AnnExpr restoreq) (AnnExpr return))))"


inductive ann_matches :: "('s,'p,'f) body ⇒ ('s,'p,'f) proc_assns ⇒ ('s, 'p, 'f) ann ⇒ ('s, 'p, 'f) com ⇒ bool" where
  ann_skip: "ann_matches Γ Θ (AnnExpr a) Skip"
| ann_basic: "ann_matches Γ Θ (AnnExpr a) (Basic f)"
| ann_spec: "ann_matches Γ Θ (AnnExpr a) (Spec r)"
| ann_throw: "ann_matches Γ Θ (AnnExpr a) (Throw)"
| ann_await: "ann_matches Γ Θ a e ⟹
               ann_matches Γ Θ (AnnRec r a) (Await b e)"
| ann_seq: "⟦ ann_matches Γ Θ a1 p1; ann_matches Γ Θ a2 p2 ⟧ ⟹
               ann_matches Γ Θ (AnnComp a1 a2) (Seq p1 p2)"
| ann_cond: "⟦ ann_matches Γ Θ a1 c1; ann_matches Γ Θ a2 c2 ⟧ ⟹
               ann_matches Γ Θ (AnnBin a a1 a2) (Cond b c1 c2)"
| ann_catch: "⟦ ann_matches Γ Θ a1 c1; ann_matches Γ Θ a2 c2 ⟧ ⟹
                ann_matches Γ Θ (AnnComp a1 a2) (Catch c1 c2)"
| ann_while: "ann_matches Γ Θ a' e ⟹
                ann_matches Γ Θ (AnnWhile a i a') (While b e)"
| ann_guard: "⟦ ann_matches Γ Θ a' e ⟧ ⟹ 
                ann_matches Γ Θ (AnnRec a a') (Guard f b e)"
| ann_call: "⟦ Θ f = Some as; Γ f = Some b; n < length as;
               ann_matches Γ Θ (as!n) b⟧ ⟹
   ann_matches Γ Θ (AnnCall a n) (Call f)"
| ann_dyncom: "∀s∈r. ann_matches Γ Θ a (c s) ⟹
               ann_matches Γ Θ (AnnRec r a) (DynCom c)"
| ann_parallel: "⟦ length as = length cs;
                   ∀i<length cs. ann_matches Γ Θ (pres (as!i)) (cs!i) ⟧ ⟹
   ann_matches Γ Θ (AnnPar as) (Parallel cs)"

primrec ann_guards:: "'s assn ⇒ ('f × 's bexp ) list ⇒
                  ('s,'p,'f) ann ⇒ ('s,'p,'f) ann"
where
  "ann_guards _ [] c = c" |
  "ann_guards r (g#gs) c = AnnRec r (ann_guards (r ∩ snd g) gs c)"

end