Theory AxCompl

Up to index of Isabelle/Bali5

theory AxCompl = AxSem
files [AxCompl.ML]:

(*  Title:      isabelle/Bali/AxCompl.thy
    ID:         $Id: AxCompl.thy,v 1.32 2000/11/19 19:09:34 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 *)
  
  remember_init_state :: "state assn"                ("\<doteq>")
  MGF ::"[state assn, term, prog] \<Rightarrow> state triple"   ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
  MGFn::"[nat       , term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)


defs
  
  remember_init_state_def "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"

  MGF_def
  "{P} t\<succ> {G\<rightarrow>} \<equiv> {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"

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

end

theorem remember_init_state_def2:

  \<doteq> Y = op =

ninitcls

theorem nyinitcls_subset_class:

  nyinitcls G s <= {C. is_class G C}

theorem finite_nyinitcls:

  finite (nyinitcls G s)

theorem card_nyinitcls_bound:

  card (nyinitcls G s) <= card {C. is_class G C}

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 nyinitcls_xupd_cong:

  nyinitcls G (xupd f s) = nyinitcls G s

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,{}|={\<doteq>} 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 MGFn_def2:

  G,A|-{=:n} t\<succ> {G\<rightarrow>} =
  G,A|-{\<doteq> \<and>. G\<turnstile>init\<le>n} t> {%Y s' s. G|-s -t>-> (Y, s')}

theorem MGF_MGFn_iff:

  G,A|-{\<doteq>} 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' s. s' = s & P s) \<and>. G\<turnstile>init\<le>n} t>
      {(%Y' s' s. G|-s -t>-> (Y', s') & P s) \<and>. G\<turnstile>init\<le>n}

theorem MGFNormalI:

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

theorem MGFNormalD:

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

theorem MGFn_NormalI:

  G,A|-{Normal ((%Y' s' s. s' = s & normal s) \<and>. G\<turnstile>init\<le>n)} t>
  {%Y s' s. G|-s -t>-> (Y, s')}
  ==> 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_altern:

  G,A|-{Normal (\<doteq> \<and>. p)} t\<succ> {G\<rightarrow>} =
  G,A|-{Normal ((%Y s Z. ALL w s'. G|-s -t>-> (w, s') --> (w, s') = Z) \<and>. p)}
  t> {%Y s. op = (Y, s)}
    [!]

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_asm:

  ALL C sig.
     is_methd G C sig -->
     G,A|-{\<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}
  ==> G,A|-{\<doteq>} 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 \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>})
     A|-{Normal \<doteq>} In1l (body G C sig)\<succ> {G\<rightarrow>}
  ==> G,A|-{Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}

theorem MGF_deriv:

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

simultaneous version

theorem MGF_simult_Methd_lemma:

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

theorem MGF_simult_Methd:

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

theorem MGF_deriv:

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

corollaries

theorem MGF_complete:

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

theorem ax_complete:

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