Quelle  OG_Annotations.thy

(*
 * 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₁ e₂) = pre e₁"
| "pre (AnnBin r e₁ e₂) = 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₁ e₂) = pre_par e₁"
| "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₁ e₂) = pre_set e₁"
| "pre_set (AnnBin r e₁ e₂) = {r}"
| "pre_set (AnnPar as) = ∪ (pre_set ` set (map pres (as)))"
(*| "pre_set (AnnPar e\<^sub>1 e\<^sub>2)    = pre_set (pres e\<^sub>1) \<union> pre_set (pres e\<^sub>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₁ e₂) r' = AnnComp (strengthen_pre e₁ r') e₂"
| "strengthen_pre (AnnBin r e₁ e₂) r' = AnnBin (r ∩ r') e₁ e₂"
| "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₁ e₂) r' = AnnComp (weaken_pre e₁ r') e₂"
| "weaken_pre (AnnBin r e₁ e₂) r' = AnnBin (r ∪ r') e₁ e₂"
| "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