Theory Annotated_Syntax

section ‹Annotated Syntax›
theory Annotated_Syntax
imports "Semantics"
begin

  text ‹Unfold theorems to strip annotations from program, before it is defined as constant›
  named_theorems vcg_annotation_defs ‹Definitions of Annotations›

  text ‹Marker that is inserted around all annotations by the specification parser.›
  definition "ANNOTATION ≡ λx. x"
  
  subsection ‹Annotations›
  text ‹The specification parser must interpret the annotations in the program.›
  
  definition WHILE_annotI :: "(state ⇒ bool) ⇒ bexp ⇒ com ⇒ com" 
    ("(WHILE {_} _/ DO _)"  [0, 0, 61] 61) 
    where [vcg_annotation_defs]: "WHILE_annotI (I::state ⇒ bool) ≡ While"
    
  lemmas annotate_whileI = WHILE_annotI_def[symmetric]
  
  definition WHILE_annotRVI :: "'a rel ⇒ (state ⇒ 'a) ⇒ (state ⇒ bool) ⇒ bexp ⇒ com ⇒ com" 
      ("(WHILE {_} {_} {_} _/ DO _)"  [0, 0, 0, 0, 61] 61)
    where [vcg_annotation_defs]: "WHILE_annotRVI R V I ≡ While" for R V I
    
  lemmas annotate_whileRVI = WHILE_annotRVI_def[symmetric]
  
  definition WHILE_annotVI :: "(state ⇒ int) ⇒ (state ⇒ bool) ⇒ bexp ⇒ com ⇒ com" 
    ("(WHILE {_} {_} _/ DO _)"  [0, 0, 0, 61] 61)
  where [vcg_annotation_defs]: "WHILE_annotVI V I ≡ While" for V I
  lemmas annotate_whileVI = WHILE_annotVI_def[symmetric]
  

  subsection ‹Hoare-Triples for Annotated Commands›
  text ‹The command is a function from pre-state to command, as the annotations that are 
    contained in the command may depend on the pre-state!›
  
  type_synonym HT'_type = "program ⇒ (state ⇒ bool) ⇒ (state ⇒ com) ⇒ (state ⇒ state⇒bool) ⇒ bool"
  
  definition HT'_partial :: HT'_type
    where "HT'_partial π P c Q ≡ (∀s⇩0. P s⇩0 ⟶ wlp π (c s⇩0) (Q s⇩0) s⇩0)"
  
  definition HT' :: HT'_type
    where "HT' π P c Q ≡ (∀s⇩0. P s⇩0 ⟶ wp π (c s⇩0) (Q s⇩0) s⇩0)"
  
  lemma HT'_eq_HT: "HT' π P (λ_. c) Q = HT π P c Q"
    unfolding HT_def HT'_def ..  
    
  lemma HT'_partial_eq_HT: "HT'_partial π P (λ_. c) Q = HT_partial π P c Q"
    unfolding HT_partial_def HT'_partial_def ..  
  
  lemmas HT'_unfolds = HT'_eq_HT HT'_partial_eq_HT
  
  
  type_synonym 'a Θelem_t = "(state⇒'a) × ((state ⇒ bool) × (state ⇒ com) × (state ⇒ state⇒bool))"
  
  definition HT'set :: "program ⇒ 'a Θelem_t set ⇒ bool" where "HT'set π Θ ≡ ∀(n,(P,c,Q))∈Θ. HT' π P c Q"
  
  definition HT'set_r :: "_ ⇒ program ⇒ 'a Θelem_t set ⇒ bool" where "HT'set_r r π Θ ≡ ∀(n,(P,c,Q))∈Θ. HT' π (λs. r n s ∧ P s) c Q"
  
  lemma HT'setI:    
    assumes "wf R"
    assumes RL: "⋀f P c Q s⇩0. ⟦ HT'set_r (λf' s'. ((f' s'),(f s⇩0))∈R ) π Θ; (f,(P,c,Q))∈Θ; P s⇩0 ⟧ ⟹ wp π (c s⇩0) (Q s⇩0) s⇩0"
    shows "HT'set π Θ"
    unfolding HT'set_def HT'_def 
  proof clarsimp
    fix f⇩0 P c Q s⇩0
    assume "(f⇩0,(P,c,Q))∈Θ" "P s⇩0"
    with ‹wf R› show "wp π (c s⇩0) (Q s⇩0) s⇩0"
    proof (induction "f⇩0 s⇩0" arbitrary: f⇩0 c s⇩0 P Q)
      case less
      note RL' = RL[of f⇩0 s⇩0 P, OF _ less.prems]
      show ?case
        apply (rule RL')
        unfolding HT'set_r_def HT'_def using less.hyps by auto
    qed
  qed  
  
  lemma HT'setD:
    assumes "HT'set π (insert (f,(P,c,Q)) Θ)"
    shows "HT' π P c Q" and "HT'set π Θ"
    using assms unfolding HT'set_def by auto
  
  
  
  

end