# Theory Example

Up to index of Isabelle/HOL/MicroJava

theory Example
imports SystemClasses Eval
begin

    (*  Title:      HOL/MicroJava/J/Example.thy
        ID:         $Id: Example.thy,v 1.20 2005/06/17 14:13:09 haftmann Exp $
        Author:     David von Oheimb
        Copyright   1999 Technische Universitaet Muenchen
    *)

    header {* \isaheader{Example MicroJava Program} *}

    theory Example imports SystemClasses Eval begin

    text {*
    The following example MicroJava program includes:
     class declarations with inheritance, hiding of fields, and overriding of
      methods (with refined result type),
     instance creation, local assignment, sequential composition,
     method call with dynamic binding, literal values,
     expression statement, local access, type cast, field assignment (in part),
     skip.

    \begin{verbatim}
    class Base {
      boolean vee;
      Base foo(Base x) {return x;}
    }

    class Ext extends Base {
      int vee;
      Ext foo(Base x) {((Ext)x).vee=1; return null;}
    }

    class Example {
      public static void main (String args[]) {
        Base e=new Ext();
        e.foo(null);
      }
    }
    \end{verbatim}
    *}

    datatype cnam_ = Base_ | Ext_
    datatype vnam_ = vee_ | x_ | e_

    consts
      cnam_ :: "cnam_ => cname"
      vnam_ :: "vnam_ => vnam"

    -- "@{text cnam_} and @{text vnam_} are intended to be isomorphic
        to @{text cnam} and @{text vnam}"
    axioms
      inj_cnam_:  "(cnam_ x = cnam_ y) = (x = y)"
      inj_vnam_:  "(vnam_ x = vnam_ y) = (x = y)"

      surj_cnam_: "∃m. n = cnam_ m"
      surj_vnam_: "∃m. n = vnam_ m"

    declare inj_cnam_ [simp] inj_vnam_ [simp]

    syntax
      Base :: cname
      Ext  :: cname
      vee  :: vname
      x    :: vname
      e    :: vname

    translations
      "Base" == "cnam_ Base_"
      "Ext"  == "cnam_ Ext_"
      "vee"  == "VName (vnam_ vee_)"
      "x"  == "VName (vnam_ x_)"
      "e"  == "VName (vnam_ e_)"

    axioms
      Base_not_Object: "Base ≠ Object"
      Ext_not_Object:  "Ext  ≠ Object"
      Base_not_Xcpt:   "Base ≠ Xcpt z"
      Ext_not_Xcpt:    "Ext  ≠ Xcpt z"
      e_not_This:      "e ≠ This"

    declare Base_not_Object [simp] Ext_not_Object [simp]
    declare Base_not_Xcpt [simp] Ext_not_Xcpt [simp]
    declare e_not_This [simp]
    declare Base_not_Object [symmetric, simp]
    declare Ext_not_Object  [symmetric, simp]
    declare Base_not_Xcpt [symmetric, simp]
    declare Ext_not_Xcpt  [symmetric, simp]

    consts
      foo_Base::  java_mb
      foo_Ext ::  java_mb
      BaseC   :: "java_mb cdecl"
      ExtC    :: "java_mb cdecl"
      test    ::  stmt
      foo   ::  mname
      a   ::  loc
      b       ::  loc

    defs
      foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
      BaseC_def:"BaseC == (Base, (Object,
               [(vee, PrimT Boolean)],
               [((foo,[Class Base]),Class Base,foo_Base)]))"
      foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
                   (LAcc x)..vee:=Lit (Intg Numeral1)),
               Lit Null)"
      ExtC_def: "ExtC  == (Ext,  (Base  ,
               [(vee, PrimT Integer)],
               [((foo,[Class Base]),Class Ext,foo_Ext)]))"

      test_def:"test == Expr(e::=NewC Ext);;
                        Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"

    syntax

      NP  :: xcpt
      tprg  ::"java_mb prog"
      obj1  :: obj
      obj2  :: obj
      s0  :: state
      s1  :: state
      s2  :: state
      s3  :: state
      s4  :: state

    translations
      "NP"   == "NullPointer"
      "tprg" == "[ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
      "obj1"    <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
             ((vee, Ext )\<mapsto>Intg 0))"
      "s0" == " Norm    (empty, empty)"
      "s1" == " Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
      "s2" == " Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
      "s3" == "(Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"

    ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *}
    lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"
    apply (simp (no_asm))
    done
    lemma map_of_Cons2 [simp]: "aa≠k ==> map_of ((k,bb)#ps) aa = map_of ps aa"
    apply (simp (no_asm_simp))
    done
    declare map_of_Cons [simp del] -- "sic!"

    lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])"
    apply (unfold ObjectC_def class_def)
    apply (simp (no_asm))
    done

    lemma class_tprg_NP [simp]: "class tprg (Xcpt NP) = Some (Object, [], [])"
    apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
    apply (simp (no_asm))
    done

    lemma class_tprg_OM [simp]: "class tprg (Xcpt OutOfMemory) = Some (Object, [], [])"
    apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
    apply (simp (no_asm))
    done

    lemma class_tprg_CC [simp]: "class tprg (Xcpt ClassCast) = Some (Object, [], [])"
    apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
    apply (simp (no_asm))
    done

    lemma class_tprg_Base [simp]:
    "class tprg Base = Some (Object,
        [(vee, PrimT Boolean)],
              [((foo, [Class Base]), Class Base, foo_Base)])"
    apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
    apply (simp (no_asm))
    done

    lemma class_tprg_Ext [simp]:
    "class tprg Ext = Some (Base,
        [(vee, PrimT Integer)],
              [((foo, [Class Base]), Class Ext, foo_Ext)])"
    apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
    apply (simp (no_asm))
    done

    lemma not_Object_subcls [elim!]: "(Object,C) ∈ (subcls1 tprg)^+ ==> R"
    apply (auto dest!: tranclD subcls1D)
    done

    lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object"
    apply (erule rtrancl_induct)
    apply  auto
    apply (drule subcls1D)
    apply auto
    done

    lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) ∈ (subcls1 tprg)^+ ==> R"
    apply (auto dest!: tranclD subcls1D)
    done

    lemma class_tprgD:
    "class tprg C = Some z ==> C=Object ∨ C=Base ∨ C=Ext ∨ C=Xcpt NP ∨ C=Xcpt ClassCast ∨ C=Xcpt OutOfMemory"
    apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
    apply (auto split add: split_if_asm simp add: map_of_Cons)
    done

    lemma not_class_subcls_class [elim!]: "(C,C) ∈ (subcls1 tprg)^+ ==> R"
    apply (auto dest!: tranclD subcls1D)
    apply (frule class_tprgD)
    apply (auto dest!:)
    apply (drule rtranclD)
    apply auto
    done

    lemma unique_classes: "unique tprg"
    apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
    done

    lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]

    lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
    apply (rule subcls_direct)
    apply auto
    done

    lemma Ext_widen_Base [simp]: "tprg\<turnstile>Class Ext\<preceq> Class Base"
    apply (rule widen.subcls)
    apply (simp (no_asm))
    done

    declare ty_expr_ty_exprs_wt_stmt.intros [intro!]

    lemma acyclic_subcls1_: "acyclic (subcls1 tprg)"
    apply (rule acyclicI)
    apply safe
    done

    lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]]

    lemmas fields_rec_ = wf_subcls1_ [THEN [2] fields_rec_lemma]

    lemma fields_Object [simp]: "fields (tprg, Object) = []"
    apply (subst fields_rec_)
    apply   auto
    done

    declare is_class_def [simp]

    lemma fields_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]"
    apply (subst fields_rec_)
    apply   auto
    done

    lemma fields_Ext [simp]:
      "fields (tprg, Ext)  = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)"
    apply (rule trans)
    apply  (rule fields_rec_)
    apply   auto
    done

    lemmas method_rec_ = wf_subcls1_ [THEN [2] method_rec_lemma]

    lemma method_Object [simp]: "method (tprg,Object) = map_of []"
    apply (subst method_rec_)
    apply  auto
    done

    lemma method_Base [simp]: "method (tprg, Base) = map_of
      [((foo, [Class Base]), Base, (Class Base, foo_Base))]"
    apply (rule trans)
    apply  (rule method_rec_)
    apply  auto
    done

    lemma method_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of
      [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"
    apply (rule trans)
    apply  (rule method_rec_)
    apply  auto
    done

    lemma wf_foo_Base:
    "wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))"
    apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Base_def)
    apply auto
    done

    lemma wf_foo_Ext:
    "wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))"
    apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Ext_def)
    apply auto
    apply  (rule ty_expr_ty_exprs_wt_stmt.Cast)
    prefer 2
    apply   (simp)
    apply   (rule_tac [2] cast.subcls)
    apply   (unfold field_def)
    apply   auto
    done

    lemma wf_ObjectC:
    "ws_cdecl tprg ObjectC ∧
      wf_cdecl_mdecl wf_java_mdecl tprg ObjectC ∧ wf_mrT tprg ObjectC"
    apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
      wf_mrT_def wf_fdecl_def ObjectC_def)
    apply (simp (no_asm))
    done

    lemma wf_NP:
    "ws_cdecl tprg NullPointerC ∧
      wf_cdecl_mdecl wf_java_mdecl tprg NullPointerC ∧ wf_mrT tprg NullPointerC"
    apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
      wf_mrT_def wf_fdecl_def NullPointerC_def)
    apply (simp add: class_def)
    apply (fold NullPointerC_def class_def)
    apply auto
    done

    lemma wf_OM:
    "ws_cdecl tprg OutOfMemoryC ∧
      wf_cdecl_mdecl wf_java_mdecl tprg OutOfMemoryC ∧ wf_mrT tprg OutOfMemoryC"
    apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
      wf_mrT_def wf_fdecl_def OutOfMemoryC_def)
    apply (simp add: class_def)
    apply (fold OutOfMemoryC_def class_def)
    apply auto
    done

    lemma wf_CC:
    "ws_cdecl tprg ClassCastC ∧
      wf_cdecl_mdecl wf_java_mdecl tprg ClassCastC ∧ wf_mrT tprg ClassCastC"
    apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
      wf_mrT_def wf_fdecl_def ClassCastC_def)
    apply (simp add: class_def)
    apply (fold ClassCastC_def class_def)
    apply auto
    done

    lemma wf_BaseC:
    "ws_cdecl tprg BaseC ∧
      wf_cdecl_mdecl wf_java_mdecl tprg BaseC ∧ wf_mrT tprg BaseC"
    apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
      wf_mrT_def wf_fdecl_def BaseC_def)
    apply (simp (no_asm))
    apply (fold BaseC_def)
    apply (rule mp) defer apply (rule wf_foo_Base)
    apply (auto simp add: wf_mdecl_def)
    done

    lemma wf_ExtC:
    "ws_cdecl tprg ExtC ∧
      wf_cdecl_mdecl wf_java_mdecl tprg ExtC ∧ wf_mrT tprg ExtC"
    apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
      wf_mrT_def wf_fdecl_def ExtC_def)
    apply (simp (no_asm))
    apply (fold ExtC_def)
    apply (rule mp) defer apply (rule wf_foo_Ext)
    apply (auto simp add: wf_mdecl_def)
    apply (drule rtranclD)
    apply auto
    done

    lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def)

    lemma wf_tprg:
    "wf_prog wf_java_mdecl tprg"
    apply (unfold wf_prog_def ws_prog_def Let_def)
    apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes)
    apply (rule wf_syscls)
    apply (simp add: SystemClasses_def)
    done

    lemma appl_methds_foo_Base:
    "appl_methds tprg Base (foo, [NT]) =
      {((Class Base, Class Base), [Class Base])}"
    apply (unfold appl_methds_def)
    apply (simp (no_asm))
    done

    lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) =
      {((Class Base, Class Base), [Class Base])}"
    apply (unfold max_spec_def)
    apply (auto simp add: appl_methds_foo_Base)
    done

    ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *}
    lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>
      Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
    apply (tactic t) -- ";;"
    apply  (tactic t) -- "Expr"
    apply  (tactic t) -- "LAss"
    apply    simp -- {* @{text "e ≠ This"} *}
    apply    (tactic t) -- "LAcc"
    apply     (simp (no_asm))
    apply    (simp (no_asm))
    apply   (tactic t) -- "NewC"
    apply   (simp (no_asm))
    apply  (simp (no_asm))
    apply (tactic t) -- "Expr"
    apply (tactic t) -- "Call"
    apply   (tactic t) -- "LAcc"
    apply    (simp (no_asm))
    apply   (simp (no_asm))
    apply  (tactic t) -- "Cons"
    apply   (tactic t) -- "Lit"
    apply   (simp (no_asm))
    apply  (tactic t) -- "Nil"
    apply (simp (no_asm))
    apply (rule max_spec_foo_Base)
    done

    ML {* fun e t = resolve_tac (thm "NewCI"::thms "eval_evals_exec.intros") 1 t *}

    declare split_if [split del]
    declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
    lemma exec_test:
    " [|new_Addr (heap (snd s0)) = (a, None)|] ==>
      tprg\<turnstile>s0 -test-> ?s"
    apply (unfold test_def)
    -- "?s = s3 "
    apply (tactic e) -- ";;"
    apply  (tactic e) -- "Expr"
    apply  (tactic e) -- "LAss"
    apply   (tactic e) -- "NewC"
    apply    force
    apply   force
    apply  (simp (no_asm))
    apply (erule thin_rl)
    apply (tactic e) -- "Expr"
    apply (tactic e) -- "Call"
    apply       (tactic e) -- "LAcc"
    apply      force
    apply     (tactic e) -- "Cons"
    apply      (tactic e) -- "Lit"
    apply     (tactic e) -- "Nil"
    apply    (simp (no_asm))
    apply   (force simp add: foo_Ext_def)
    apply  (simp (no_asm))
    apply  (tactic e) -- "Expr"
    apply  (tactic e) -- "FAss"
    apply       (tactic e) -- "Cast"
    apply        (tactic e) -- "LAcc"
    apply       (simp (no_asm))
    apply      (simp (no_asm))
    apply     (simp (no_asm))
    apply     (tactic e) -- "XcptE"
    apply    (simp (no_asm))
    apply   (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force)
    apply  (simp (no_asm))
    apply (simp (no_asm))
    apply (tactic e) -- "XcptE"
    done

    end

theorem map_of_Cons:

      map_of (p # ps) = map_of ps(fst p |-> snd p)

lemma map_of_Cons1:

      map_of ((aa, bb) # ps) aa = Some bb

lemma map_of_Cons2:

      aa ≠ k ==> map_of ((k, bb) # ps) aa = map_of ps aa

lemma class_tprg_Object:

      class tprg Object = Some (arbitrary, [], [])

lemma class_tprg_NP:

      class tprg (Xcpt NP) = Some (Object, [], [])

lemma class_tprg_OM:

      class tprg (Xcpt OutOfMemory) = Some (Object, [], [])

lemma class_tprg_CC:

      class tprg (Xcpt ClassCast) = Some (Object, [], [])

lemma class_tprg_Base:

      class tprg Base =
      Some (Object, [(vee, PrimT Boolean)],
            [((foo, [Class Base]), Class Base, foo_Base)])

lemma class_tprg_Ext:

      class tprg Ext =
      Some (Base, [(vee, PrimT Integer)], [((foo, [Class Base]), Class Ext, foo_Ext)])

lemma not_Object_subcls:

      (Object, C) ∈ (subcls1 tprg)+ ==> R

lemma subcls_ObjectD:

      tprg |- Object <=C C ==> C = Object

lemma not_Base_subcls_Ext:

      (Base, Ext) ∈ (subcls1 tprg)+ ==> R

lemma class_tprgD:

      class tprg C = Some z
      ==> C = Object ∨
          C = Base ∨ C = Ext ∨ C = Xcpt NP ∨ C = Xcpt ClassCast ∨ C = Xcpt OutOfMemory

lemma not_class_subcls_class:

      (C, C) ∈ (subcls1 tprg)+ ==> R

lemma unique_classes:

      unique tprg

lemmas subcls_direct:

      [| class G1 C1 = Some (D1, rest1); C1 ≠ Object |] ==> G1 |- C1 <=C D1

lemmas subcls_direct:

      [| class G1 C1 = Some (D1, rest1); C1 ≠ Object |] ==> G1 |- C1 <=C D1

lemma Ext_subcls_Base:

      tprg |- Ext <=C Base

lemma Ext_widen_Base:

      tprg |- Class Ext <= Class Base

lemma acyclic_subcls1_:

      acyclic (subcls1 tprg)

lemmas wf_subcls1_:

      wf ((subcls1 tprg)^-1)

lemmas wf_subcls1_:

      wf ((subcls1 tprg)^-1)

lemmas fields_rec_:

      class tprg C = Some (D, fs, ms)
      ==> fields (tprg, C) =
          map (%(fn, ft). ((fn, C), ft)) fs @
          (if C = Object then [] else fields (tprg, D))

lemmas fields_rec_:

      class tprg C = Some (D, fs, ms)
      ==> fields (tprg, C) =
          map (%(fn, ft). ((fn, C), ft)) fs @
          (if C = Object then [] else fields (tprg, D))

lemma fields_Object:

      fields (tprg, Object) = []

lemma fields_Base:

      fields (tprg, Base) = [((vee, Base), PrimT Boolean)]

lemma fields_Ext:

      fields (tprg, Ext) = [((vee, Ext), PrimT Integer)] @ fields (tprg, Base)

lemmas method_rec_:

      class tprg C = Some (D, fs, ms)
      ==> method (tprg, C) =
          (if C = Object then empty else method (tprg, D)) ++
          map_of (map (%(s, m). (s, C, m)) ms)

lemmas method_rec_:

      class tprg C = Some (D, fs, ms)
      ==> method (tprg, C) =
          (if C = Object then empty else method (tprg, D)) ++
          map_of (map (%(s, m). (s, C, m)) ms)

lemma method_Object:

      method (tprg, Object) = map_of []

lemma method_Base:

      method (tprg, Base) = map_of [((foo, [Class Base]), Base, Class Base, foo_Base)]

lemma method_Ext:

      method (tprg, Ext) =
      method (tprg, Base) ++ map_of [((foo, [Class Base]), Ext, Class Ext, foo_Ext)]

lemma wf_foo_Base:

      wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), Class Base, foo_Base)

lemma wf_foo_Ext:

      wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), Class Ext, foo_Ext)

lemma wf_ObjectC:

      ws_cdecl tprg ObjectC ∧
      wf_cdecl_mdecl wf_java_mdecl tprg ObjectC ∧ wf_mrT tprg ObjectC

lemma wf_NP:

      ws_cdecl tprg NullPointerC ∧
      wf_cdecl_mdecl wf_java_mdecl tprg NullPointerC ∧ wf_mrT tprg NullPointerC

lemma wf_OM:

      ws_cdecl tprg OutOfMemoryC ∧
      wf_cdecl_mdecl wf_java_mdecl tprg OutOfMemoryC ∧ wf_mrT tprg OutOfMemoryC

lemma wf_CC:

      ws_cdecl tprg ClassCastC ∧
      wf_cdecl_mdecl wf_java_mdecl tprg ClassCastC ∧ wf_mrT tprg ClassCastC

lemma wf_BaseC:

      ws_cdecl tprg BaseC ∧
      wf_cdecl_mdecl wf_java_mdecl tprg BaseC ∧ wf_mrT tprg BaseC

lemma wf_ExtC:

      ws_cdecl tprg ExtC ∧ wf_cdecl_mdecl wf_java_mdecl tprg ExtC ∧ wf_mrT tprg ExtC

lemma

      fst ObjectC = Object

lemma wf_tprg:

      wf_java_prog tprg

lemma appl_methds_foo_Base:

      appl_methds tprg Base (foo, [NT]) = {((Class Base, Class Base), [Class Base])}

lemma max_spec_foo_Base:

      max_spec tprg Base (foo, [NT]) = {((Class Base, Class Base), [Class Base])}

lemma wt_test:

      (tprg,
       [e |->
        Class
         Base]) |- Expr (e::=NewC Ext);; Expr ({Base}LAcc
              e..foo( {[Class Base]}[Lit Null])) [ok]

lemma exec_test:

      new_Addr (fst (snd s0)) = (a, None)
      ==> (s0, test, Some (Addr (XcptRef NP)),
           fst ([a |->
                 (Ext, map_of [((vee, Ext), Intg 0), ((vee, Base), Bool False)])],
                [x |-> Null, This |-> Addr a]),
           [e |-> Addr a])
          ∈ exec tprg