Theory AxSound

Up to index of Isabelle/Bali5

(*  Title:      isabelle/Bali/AxSound.thy
    ID:         $Id: AxSound.thy,v 1.11 2000/11/19 19:09:35 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>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q 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 Y' s'.
          G|-s -t>-n-> (Y', s') -->
          (ALL L. s\<Colon>\<preceq>(G, L) -->
                  (ALL T. (normal s --> (G, L)|-t::T) -->
                          Q Y' s' Z & s'\<Colon>\<preceq>(G, L)))))

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 Y' s'.
     G|-s -t>-n-> (Y', s') -->
     t = c -->
     Ball A (triple_valid2 G n) -->
     (ALL Y Z.
         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>{{Normal (P'\<leftarrow>=True)} .c. {P}} |]
  ==> G,A|\<Turnstile>\<Colon>{{P} .While(e) c.
                               {P'\<leftarrow>=False\<down>=dummy_res}}
    [!]

theorem all_empty:

  (ALL x. P) = P

theorem sound_valid2_lemma:

  [| ALL v n. Ball A (triple_valid2 G n) --> P v n; Ball A (triple_valid2 G n) |]
  ==> P v n

theorem Call_sound:

  [| wf_prog G; G,A|\<Turnstile>\<Colon>{{Normal P} e-> {Q}};
     ALL a. G,A|\<Turnstile>\<Colon>{{Q\<leftarrow>In1 a} ps#> {R a}};
     ALL a vs D l.
        G,A|\<Turnstile>\<Colon>{{R a\<leftarrow>In3 vs \<and>.
                                  (%s. D = target mode (snd s) a cT &
                                       l = locals (snd s)) ;.
                                  init_lvars G D (mn, pTs) mode a vs \<and>.
                                  (%s. normal s -->
                                       G\<turnstile>mode\<rightarrow>D\<preceq>t)}
                                 Methd D (mn, pTs)-> {set_lvars l .; S}} |]
  ==> 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). {Q}};
     ALL l. G,A|\<Turnstile>\<Colon>{{Q \<and>. (%s. l = locals (snd s)) ;.
                                      set_lvars empty}
                                     .ini. {set_lvars l .; R}} |]
  ==> G,A|\<Turnstile>\<Colon>{{Normal (P \<and>. Not o initd C)} .init C. {R}}
    [!]

theorem all_conjunct2:

  ALL l. P' l & P l ==> ALL l. P l

theorem all4_conjunct2:

  ALL a vs D l. P' a vs D l & P a vs D l ==> ALL a vs D l. P a vs D l

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  [!]