Theory AxCompl

Up to index of Isabelle/Bali4

theory AxCompl = AxSem
files [AxCompl.ML]:

(*  Title:      isabelle/Bali/AxCompl.thy
    ID:         $Id: AxCompl.thy,v 1.30 2000/09/13 13:51:57 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

Completeness proof for Axiomatic semantics of Java expressions and statements

design issues:
* proof structured by Most General Formulas (-> Thomas Kleymann)
*)

AxCompl = AxSem + 

constdefs

  nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> tname set"
 "nyinitcls G s \<equiv> {C. is_class G C \<and> ¬ initd C s}"

  init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"            ("_\<turnstile>init\<le>_"  [51,51] 50)
 "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n"
  
consts (* Most General Triples and Formulas *)

  MGF  ::"[rstate assn,term,prog]\<Rightarrow>rstate triple"   ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
  MGFn ::"[nat        ,term,prog]\<Rightarrow>rstate triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)


defs
  
  MGF_def
  "{P} t\<succ> {G\<rightarrow>} \<equiv> {P} t\<succ> {\<lambda>(Y',s') (Y,s). \<exists>w. Y'=res t w Y \<and> G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s')}"

  MGFn_def
  "{=:n} t\<succ> {G\<rightarrow>} \<equiv> {op = \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"

end

ninitcls

theorem finite_nyinitcls:

  finite (nyinitcls G s)

theorem nyinitcls_set_locals_cong:

  nyinitcls G (x, set_locals l s) = nyinitcls G (x, s)

theorem nyinitcls_xcpt_cong:

  nyinitcls G (f x, y) = nyinitcls G (x, y)

theorem card_nyinitcls_xcpt_congE:

  card (nyinitcls G (x, s)) <= n ==> card (nyinitcls G (y, s)) <= n

theorem nyinitcls_new_xcpt_var:

  nyinitcls G (new_xcpt_var vn s) = nyinitcls G s

theorem nyinitcls_init_lvars:

  nyinitcls G (init_lvars G C sig mode a' pvs s) = nyinitcls G s

theorem nyinitcls_emptyD:

  [| nyinitcls G s = {}; is_class G C |] ==> initd C s

theorem card_Suc_lemma:

  [| card (insert a A) <= Suc n; a ~: A; finite A |] ==> card A <= n

theorem nyinitcls_le_SucD:

  [| card (nyinitcls G (x, s)) <= Suc n; ¬ inited C (globs s);
     class G C = Some y |]
  ==> card (nyinitcls G (x, (init_class_obj G C) s)) <= n

theorem nyinitcls_gext:

  snd s\<le>|snd s' ==> nyinitcls G s' <= nyinitcls G s

theorem card_nyinitcls_gext:

  [| snd s\<le>|snd s'; card (nyinitcls G s) <= n |]
  ==> card (nyinitcls G s') <= n

init_le

theorem init_le_def2:

  (G\<turnstile>init\<le>n) s = (card (nyinitcls G s) <= n)

theorem All_init_leD:

  ALL n. G,A|-{P \<and>. G\<turnstile>init\<le>n} t> {Q} ==> G,A|-{P} t> {Q}

MGF

theorem MGF_valid:

  G,{}|={op =} t\<succ> {G\<rightarrow>}  [!]

theorem MGF_res_eq_lemma:

  (ALL Y' Y s. Y = Y' & P s --> Q s) = (ALL s. P s --> Q s)

theorem MGF_stmt_eq:

  G,A|-{P} .c. {%(Y', s') (Y, s). Y' = Y & (EX w. (s, In1r c, w, s') : eval G)} =
  G,A|-{P} .c. {%(Y', s') (Y, s). Y' = Y & (s, In1r c, In1 Unit, s') : eval G}

theorem MGFn_def2:

  G,A|-{=:n} t\<succ> {G\<rightarrow>} =
  G,A|-{op = \<and>. G\<turnstile>init\<le>n} t>
  {%(Y', s') (Y, s). EX w. Y' = res t w Y & (s, t, w, s') : eval G}

theorem MGF_MGFn_iff:

  G,A|-{op =} t\<succ> {G\<rightarrow>} =
  (ALL n. G,A|-{=:n} t\<succ> {G\<rightarrow>})

theorem MGFnD:

  G,A|-{=:n} t\<succ> {G\<rightarrow>}
  ==> G,A|-{(%(Y', s') (Y, s). Y' = Y & s' = s & P s) \<and>.
            G\<turnstile>init\<le>n}
      t> {(%(Y', s') (Y, s).
              (EX w. Y' = res t w Y & (s, t, w, s') : eval G) & P s) \<and>.
          G\<turnstile>init\<le>n}
    [!]

theorem MGFn_stmtD:

  G,A|-{=:n} In1r c\<succ> {G\<rightarrow>}
  ==> G,A|-{(%(Y', s') (Y, s). Y' = Y & s' = s & P s) \<and>.
            G\<turnstile>init\<le>n}
      .c. {(%(Y', s') (Y, s).
               Y' = Y & (s, In1r c, In1 Unit, s') : eval G & P s) \<and>.
           G\<turnstile>init\<le>n}
    [!]

theorem MGFNormalI:

  G,A|-{Normal op =} t\<succ> {G\<rightarrow>}
  ==> G,A|-{op =} t\<succ> {G\<rightarrow>}

theorem MGFNormalD:

  G,A|-{op =} t\<succ> {G\<rightarrow>}
  ==> G,A|-{Normal op =} t\<succ> {G\<rightarrow>}

theorem MGFn_NormalI:

  G,A|-{Normal
         ((%(Y', s') (Y, s). Y' = Y & s' = s & normal s) \<and>.
          G\<turnstile>init\<le>n)}
  t> {%(Y', s') (Y, s). EX w. Y' = res t w Y & (s, t, w, s') : eval G}
  ==> G,A|-{=:n} t\<succ> {G\<rightarrow>}

theorem MGFn_free_wt:

  (EX T L. (G, L)|-t::T) --> G,A|-{=:n} t\<succ> {G\<rightarrow>}
  ==> G,A|-{=:n} t\<succ> {G\<rightarrow>}

main lemmas

theorem MGFn_Init:

  ALL m. Suc m <= n --> (ALL t. G,A|-{=:m} t\<succ> {G\<rightarrow>})
  ==> G,A|-{=:n} In1r (init C)\<succ> {G\<rightarrow>}
    [!]

theorem MGFn_Call:

  [| ALL C sig. G,A|-{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>};
     G,A|-{=:n} In1l e\<succ> {G\<rightarrow>};
     G,A|-{=:n} In3 ps\<succ> {G\<rightarrow>} |]
  ==> G,A|-{=:n} In1l ({t,cT,mode}e..mn( {pTs'}ps))\<succ> {G\<rightarrow>}
    [!]

theorem MGF_stmt_altern:

  G,A|-{Normal (op = \<and>. p)} .c.
  {%(Y', s') (Y, s). Y' = Y & (s, In1r c, In1 Unit, s') : eval G} =
  G,A|-{Normal
         ((%(Y, s) (Y', s').
              Y' = Y &
              (ALL t. (s, In1r c, In1 Unit, t) : eval G --> t = s')) \<and>.
          p)}
  .c. {op =}
    [!]

theorem MGFn_Loop:

  [| G,A|-{=:n} In1l expr\<succ> {G\<rightarrow>};
     G,A|-{=:n} In1r stmt\<succ> {G\<rightarrow>} |]
  ==> G,A|-{=:n} In1r (While(expr) stmt)\<succ> {G\<rightarrow>}
    [!]

theorem MGFn_lemma:

  ALL n C sig. G,A|-{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>}
  ==> G,A|-{=:n} t\<succ> {G\<rightarrow>}
    [!]

theorem MGF_lemma:

  ALL C sig.
     is_methd G C sig --> G,A|-{op =} In1l (Methd C sig)\<succ> {G\<rightarrow>}
  ==> G,A|-{op =} t\<succ> {G\<rightarrow>}
    [!]

nested version

theorem nesting_lemma':

  [| !!A ts. ts <= A ==> P A ts;
     !!A pn.
        ALL b:bdy pn. P (insert (mgf_call pn) A) {mgf b} ==> P A {mgf_call pn};
     !!A t. ALL pn:U. P A {mgf_call pn} ==> P A {mgf t}; finite U;
     uA = mgf_call `` U; A <= uA; n <= card uA; card A = card uA - n |]
  ==> P A {mgf t}

theorem nesting_lemma:

  [| !!A ts. ts <= A ==> P A ts;
     !!A pn. ALL b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)};
     !!A t. ALL pn:U. P A {mgf (f pn)} ==> P A {mgf t}; finite U |]
  ==> P {} {mgf t}

theorem MGF_nested_Methd:

  G,insert ({Normal op =} In1l (Methd C sig)\<succ> {G\<rightarrow>})
     A|-{Normal op =} In1l (body G C sig)\<succ> {G\<rightarrow>}
  ==> G,A|-{Normal op =} In1l (Methd C sig)\<succ> {G\<rightarrow>}

theorem MGF_deriv:

  ws_prog G ==> G,{}|-{op =} t\<succ> {G\<rightarrow>}  [!]

simultaneous version

theorem MGF_simult_Methd_lemma:

  [| finite ms;
     G,A Un
       (%(C, sig). {Normal op =} In1l (Methd C sig)\<succ> {G\<rightarrow>}) ``
       ms||-(%(C, sig).
                {Normal op =} In1l (body G C sig)\<succ> {G\<rightarrow>}) ``
            ms |]
  ==> G,A||-(%(C, sig).
                {Normal op =} In1l (Methd C sig)\<succ> {G\<rightarrow>}) ``
            ms

theorem MGF_simult_Methd:

  ws_prog G
  ==> G,{}||-(%(C, sig).
                 {Normal op =} In1l (Methd C sig)\<succ> {G\<rightarrow>}) ``
             Collect (split (is_methd G))
    [!]

theorem MGF_deriv:

  ws_prog G ==> G,{}|-{op =} t\<succ> {G\<rightarrow>}  [!]

corollaries

theorem MGF_complete:

  [| G,{}|-{op =} t\<succ> {G\<rightarrow>}; G,{}|={P} t> {Q} |]
  ==> G,{}|-{P} t> {Q}

theorem ax_complete:

  [| ws_prog G; G,{}|={P} t> {Q} |] ==> G,{}|-{P} t> {Q}  [!]