Theory AxSound

Up to index of Isabelle/Bali4

(*  Title:      isabelle/Bali/AxSound.thy
    ID:         $Id: AxSound.thy,v 1.9 2000/08/07 21:07:48 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

Soundness proof for Axiomatic semantics of Java expressions and statements
*)

AxSound = AxSem +

consts

 triple_valid2:: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
                                                (   "_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
    ax_valids2:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"
                                                ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)

defs  triple_valid2_def  "G\<Turnstile>n\<Colon>t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
 \<forall>Y s Z. P (Y,s) Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T. (normal s \<longrightarrow> (G,L)\<turnstile>t\<Colon>T) \<longrightarrow>
               (\<forall>w s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<longrightarrow> Q (res t w Y,s') Z \<and> s'\<Colon>\<preceq>(G,L))))"
defs  ax_valids2_def  "G,A|\<Turnstile>\<Colon>ts \<equiv>  \<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t)"

end

validity

theorem triple_valid2_def2:

  G\<Turnstile>n\<Colon>{P} t> {Q} =
  (ALL Y s Z.
      P (Y, s) Z -->
      (ALL w s'.
          (s, t, n, w, s') : evaln G -->
          (ALL L. s\<Colon>\<preceq>(G, L) -->
                  (ALL T. (normal s --> (G, L)|-t::T) -->
                          Q (res t w Y, s') Z & s'\<Colon>\<preceq>(G, L)))))

theorem valids2_inductI:

  ALL s t n w s' Y Z.
     (s, t, n, w, s') : evaln G -->
     t = In1r c -->
     Ball A (triple_valid2 G n) -->
     P (Y, s) Z -->
     (ALL L. s\<Colon>\<preceq>(G, L) -->
             (ALL T. (normal s --> (G, L)|-t::T) -->
                     Q (Y, s') Z & s'\<Colon>\<preceq>(G, L)))
  ==> G,A|\<Turnstile>\<Colon>{{P} .c. {Q}}

theorem triple_valid2_eq:

  wf_prog G ==> triple_valid2 G = triple_valid G  [!]

theorem ax_valids2_eq:

  wf_prog G ==> G,A|\<Turnstile>\<Colon>ts = G,A|\<Turnstile>ts  [!]

theorem triple_valid2_Suc:

  G\<Turnstile>Suc n\<Colon>t ==> G\<Turnstile>n\<Colon>t

theorem Methd_triple_valid2_0:

  G\<Turnstile>0\<Colon>{Normal P} Methd C sig-> {Q}  [!]

theorem Methd_triple_valid2_SucI:

  G\<Turnstile>n\<Colon>{Normal P} body G C sig-> {Q}
  ==> G\<Turnstile>Suc n\<Colon>{Normal P} Methd C sig-> {Q}
    [!]

theorem triples_valid2_Suc:

  Ball ts (triple_valid2 G (Suc n)) ==> Ball ts (triple_valid2 G n)

theorem Methd_sound:

  G,A Un {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ>
  {Q} | ms}
  ==> G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
    [!]

theorem valids2_inductI:

  ALL s t n w s' Y Z.
     (s, t, n, w, s') : evaln G -->
     t = In1r c -->
     Ball A (triple_valid2 G n) -->
     P (Y, s) Z -->
     (ALL L. s\<Colon>\<preceq>(G, L) -->
             (ALL T. (normal s --> (G, L)|-t::T) -->
                     Q (Y, s') Z & s'\<Colon>\<preceq>(G, L)))
  ==> G,A|\<Turnstile>\<Colon>{{P} .c. {Q}}

theorem Loop_sound:

  [| G,A|\<Turnstile>\<Colon>{{P} e-> {P'}};
     G,A|\<Turnstile>\<Colon>{{P'\<up>#Bool=True} .c. {P}} |]
  ==> G,A|\<Turnstile>\<Colon>{{P} .While(e) c. {P'\<up>#Bool=False}}
    [!]

theorem Call_sound:

  [| wf_prog G; G,A|\<Turnstile>\<Colon>{{Normal P} e-> {Q}};
     G,A|\<Turnstile>\<Colon>{{Q} ps#>
                              {\<lambda>Vals:pvs#
                                Val:a#. \<lambda>s: let D = target mode s a cT
            in init_lvars G D (mn, pTs) mode a pvs .;
               R\<up>#DynT D\<up>#Lcls (locals s)}};
     ALL D. P1 D &
            G,A|\<Turnstile>\<Colon>{{R\<up>#DynT D \<and>.
                                      (%s.
  normal s --> G\<turnstile>mode\<rightarrow>D\<preceq>t)}
                                     Methd D (mn, pTs)->
                                     {\<lambda>Val:v#
                                       Lcls:l#. set_lvars l .; S\<up>#Val v}} |]
  ==> G,A|\<Turnstile>\<Colon>{{Normal P} {t,cT,mode}e..mn( {pTs}ps)-> {S}}
    [!]

theorem Init_sound:

  [| wf_prog G; the (class G C) = (sc, si, fs, ms, ini);
     G,A|\<Turnstile>\<Colon>{{Normal
                                (P \<and>. Not o initd C ;.
                                 supd (init_class_obj G C))}
                              .(if C = Object then Skip else init sc).
                              {\<lambda>s: Q\<up>#Lcls (locals s)}};
     G,A|\<Turnstile>\<Colon>{{Q ;. set_lvars empty} .ini.
                              {\<lambda>Lcls:l#. set_lvars l .; R}} |]
  ==> G,A|\<Turnstile>\<Colon>{{Normal (P \<and>. Not o initd C)} .init C. {R}}
    [!]

theorem ax_sound2:

  [| wf_prog G; G,A||-ts |] ==> G,A|\<Turnstile>\<Colon>ts  [!]

theorem ax_sound:

  [| wf_prog G; G,A||-ts |] ==> G,A|\<Turnstile>ts  [!]