Theory AxExample

Up to index of Isabelle/Bali5

(*  Title:      isabelle/Bali/AxExample.thy
    ID:         $Id: AxExample.thy,v 1.6 2000/11/23 09:57:30 oheimb Exp $
    Author:     David von Oheimb
    Copyright   2000 Technische Universitaet Muenchen
*)

AxExample = AxSem + Example +

constdefs
  arr_inv :: "st \<Rightarrow> bool"
 "arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
                              snd obj (Inl (arr, Base)) = Some (Addr a) \<and>
                              heap s a = Some (Arr T #2,el)"
end

theorem arr_inv_new_obj:

  [| arr_inv s; new_Addr (heap s) = Some a |]
  ==> arr_inv (gupd(Inl a\<mapsto>x) s)

theorem arr_inv_set_locals:

  arr_inv (set_locals l s) = arr_inv s

theorem arr_inv_gupd_Stat:

  Base ~= C ==> arr_inv (gupd(Inr C\<mapsto>obj) s) = arr_inv s

theorem arr_inv_lupd:

  arr_inv (lupd(x\<mapsto>y) s) = arr_inv s

theorem ax_test:

  tprg,{}|-{Normal (%Y s Z. heap_free 4 s & ¬ initd Base s & ¬ initd Ext s)}
  .test [Class Base]. {%Y s Z. fst s = Some (StdXcpt IndOutBound)}
    [!]

theorem Loop_Xcpt_benchmark:

  Q = (%Y (x, s) Z. x ~= None --> the_Bool (the (locals s i)))
  ==> G,{}|-{Normal (%Y s Z. True)}
      .While(Lit (Bool True)) (If(Acc (LVar i)) Throw
         (Acc (LVar xcpt)) Else Expr (LVar i:=Acc (LVar j))).
      {Q}