# Theory Conform

Up to index of Isabelle/HOL/MicroJava

theory Conform
imports State WellType Exceptions
begin

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

    header {* \isaheader{Conformity Relations for Type Soundness Proof} *}

    theory Conform imports State WellType Exceptions begin

    types 'c env_ = "'c prog × (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"

    constdefs

      hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50)
     "h<=|h' == ∀a C fs. h a = Some(C,fs) --> (∃fs'. h' a = Some(C,fs'))"

      conf :: "'c prog => aheap => val => ty => bool"
                                       ("_,_ |- _ ::<= _"  [51,51,51,51] 50)
     "G,h|-v::<=T == ∃T'. typeof (option_map obj_ty o h) v = Some T' ∧ G\<turnstile>T'\<preceq>T"

      lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
                                       ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
     "G,h|-vs[::<=]Ts == ∀n T. Ts n = Some T --> (∃v. vs n = Some v ∧ G,h|-v::<=T)"

      oconf :: "'c prog => aheap => obj => bool" ("_,_ |- _ [ok]" [51,51,51] 50)
     "G,h|-obj [ok] == G,h|-snd obj[::<=]map_of (fields (G,fst obj))"

      hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50)
     "G|-h h [ok]    == ∀a obj. h a = Some obj --> G,h|-obj [ok]"

      xconf :: "aheap => val option => bool"
      "xconf hp vo  == preallocated hp ∧ (∀ v. (vo = Some v) --> (∃ xc. v = (Addr (XcptRef xc))))"

      conforms :: "xstate => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
     "s::<=E == prg E|-h heap (store s) [ok] ∧
                prg E,heap (store s)|-locals (store s)[::<=]localT E ∧
                xconf (heap (store s)) (abrupt s)"

    syntax (xsymbols)
      hext     :: "aheap => aheap => bool"
                  ("_ ≤| _" [51,51] 50)

      conf     :: "'c prog => aheap => val => ty => bool"
                  ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)

      lconf    :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
                  ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)

      oconf    :: "'c prog => aheap => obj => bool"
                  ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)

      hconf    :: "'c prog => aheap => bool"
                  ("_ \<turnstile>h _ \<surd>" [51,51] 50)

      conforms :: "state => java_mb env_ => bool"
                  ("_ ::\<preceq> _" [51,51] 50)

    section "hext"

    lemma hextI:
    " ∀a C fs . h  a = Some (C,fs) -->
          (∃fs'. h' a = Some (C,fs')) ==> h≤|h'"
    apply (unfold hext_def)
    apply auto
    done

    lemma hext_objD: "[|h≤|h'; h a = Some (C,fs) |] ==> ∃fs'. h' a = Some (C,fs')"
    apply (unfold hext_def)
    apply (force)
    done

    lemma hext_refl [simp]: "h≤|h"
    apply (rule hextI)
    apply (fast)
    done

    lemma hext_new [simp]: "h a = None ==> h≤|h(a\<mapsto>x)"
    apply (rule hextI)
    apply auto
    done

    lemma hext_trans: "[|h≤|h'; h'≤|h''|] ==> h≤|h''"
    apply (rule hextI)
    apply (fast dest: hext_objD)
    done

    lemma hext_upd_obj: "h a = Some (C,fs) ==> h≤|h(a\<mapsto>(C,fs'))"
    apply (rule hextI)
    apply auto
    done

    section "conf"

    lemma conf_Null [simp]: "G,h\<turnstile>Null::\<preceq>T = G\<turnstile>RefT NullT\<preceq>T"
    apply (unfold conf_def)
    apply (simp (no_asm))
    done

    lemma conf_litval [rule_format (no_asm), simp]:
      "typeof (λv. None) v = Some T --> G,h\<turnstile>v::\<preceq>T"
    apply (unfold conf_def)
    apply (rule val.induct)
    apply auto
    done

    lemma conf_AddrI: "[|h a = Some obj; G\<turnstile>obj_ty obj\<preceq>T|] ==> G,h\<turnstile>Addr a::\<preceq>T"
    apply (unfold conf_def)
    apply (simp)
    done

    lemma conf_obj_AddrI: "[|h a = Some (C,fs); G\<turnstile>C\<preceq>C D|] ==> G,h\<turnstile>Addr a::\<preceq> Class D"
    apply (unfold conf_def)
    apply (simp)
    done

    lemma defval_conf [rule_format (no_asm)]:
      "is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"
    apply (unfold conf_def)
    apply (rule_tac y = "T" in ty.exhaust)
    apply  (erule ssubst)
    apply  (rule_tac y = "prim_ty" in prim_ty.exhaust)
    apply    (auto simp add: widen.null)
    done

    lemma conf_upd_obj:
    "h a = Some (C,fs) ==> (G,h(a\<mapsto>(C,fs'))\<turnstile>x::\<preceq>T) = (G,h\<turnstile>x::\<preceq>T)"
    apply (unfold conf_def)
    apply (rule val.induct)
    apply auto
    done

    lemma conf_widen [rule_format (no_asm)]:
      "wf_prog wf_mb G ==> G,h\<turnstile>x::\<preceq>T --> G\<turnstile>T\<preceq>T' --> G,h\<turnstile>x::\<preceq>T'"
    apply (unfold conf_def)
    apply (rule val.induct)
    apply (auto intro: widen_trans)
    done

    lemma conf_hext [rule_format (no_asm)]: "h≤|h' ==> G,h\<turnstile>v::\<preceq>T --> G,h'\<turnstile>v::\<preceq>T"
    apply (unfold conf_def)
    apply (rule val.induct)
    apply (auto dest: hext_objD)
    done

    lemma new_locD: "[|h a = None; G,h\<turnstile>Addr t::\<preceq>T|] ==> t≠a"
    apply (unfold conf_def)
    apply auto
    done

    lemma conf_RefTD [rule_format (no_asm)]:
     "G,h\<turnstile>a'::\<preceq>RefT T --> a' = Null |
      (∃a obj T'. a' = Addr a ∧  h a = Some obj ∧  obj_ty obj = T' ∧  G\<turnstile>T'\<preceq>RefT T)"
    apply (unfold conf_def)
    apply(induct_tac "a'")
    apply(auto)
    done

    lemma conf_NullTD: "G,h\<turnstile>a'::\<preceq>RefT NullT ==> a' = Null"
    apply (drule conf_RefTD)
    apply auto
    done

    lemma non_npD: "[|a' ≠ Null; G,h\<turnstile>a'::\<preceq>RefT t|] ==>
      ∃a C fs. a' = Addr a ∧  h a = Some (C,fs) ∧  G\<turnstile>Class C\<preceq>RefT t"
    apply (drule conf_RefTD)
    apply auto
    done

    lemma non_np_objD: "!!G. [|a' ≠ Null; G,h\<turnstile>a'::\<preceq> Class C|] ==>
      (∃a C' fs. a' = Addr a ∧  h a = Some (C',fs) ∧  G\<turnstile>C'\<preceq>C C)"
    apply (fast dest: non_npD)
    done

    lemma non_np_objD' [rule_format (no_asm)]:
      "a' ≠ Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t -->
      (∃a C fs. a' = Addr a ∧  h a = Some (C,fs) ∧  G\<turnstile>Class C\<preceq>RefT t)"
    apply(rule_tac y = "t" in ref_ty.exhaust)
     apply (fast dest: conf_NullTD)
    apply (fast dest: non_np_objD)
    done

    lemma conf_list_gext_widen [rule_format (no_asm)]:
      "wf_prog wf_mb G ==> ∀Ts Ts'. list_all2 (conf G h) vs Ts -->
      list_all2 (λT T'. G\<turnstile>T\<preceq>T') Ts Ts' -->  list_all2 (conf G h) vs Ts'"
    apply(induct_tac "vs")
     apply(clarsimp)
    apply(clarsimp)
    apply(frule list_all2_lengthD [THEN sym])
    apply(simp (no_asm_use) add: length_Suc_conv)
    apply(safe)
    apply(frule list_all2_lengthD [THEN sym])
    apply(simp (no_asm_use) add: length_Suc_conv)
    apply(clarify)
    apply(fast elim: conf_widen)
    done

    section "lconf"

    lemma lconfD: "[| G,h\<turnstile>vs[::\<preceq>]Ts; Ts n = Some T |] ==> G,h\<turnstile>(the (vs n))::\<preceq>T"
    apply (unfold lconf_def)
    apply (force)
    done

    lemma lconf_hext [elim]: "[| G,h\<turnstile>l[::\<preceq>]L; h≤|h' |] ==> G,h'\<turnstile>l[::\<preceq>]L"
    apply (unfold lconf_def)
    apply  (fast elim: conf_hext)
    done

    lemma lconf_upd: "!!X. [| G,h\<turnstile>l[::\<preceq>]lT;
      G,h\<turnstile>v::\<preceq>T; lT va = Some T |] ==> G,h\<turnstile>l(va\<mapsto>v)[::\<preceq>]lT"
    apply (unfold lconf_def)
    apply auto
    done

    lemma lconf_init_vars_lemma [rule_format (no_asm)]:
      "∀x. P x --> R (dv x) x ==> (∀x. map_of fs f = Some x --> P x) -->
      (∀T. map_of fs f = Some T -->
      (∃v. map_of (map (λ(f,ft). (f, dv ft)) fs) f = Some v ∧  R v T))"
    apply( induct_tac "fs")
    apply auto
    done

    lemma lconf_init_vars [intro!]:
    "∀n. ∀T. map_of fs n = Some T --> is_type G T ==> G,h\<turnstile>init_vars fs[::\<preceq>]map_of fs"
    apply (unfold lconf_def init_vars_def)
    apply auto
    apply( rule lconf_init_vars_lemma)
    apply(   erule_tac [3] asm_rl)
    apply(  intro strip)
    apply(  erule defval_conf)
    apply auto
    done

    lemma lconf_ext: "[|G,s\<turnstile>l[::\<preceq>]L; G,s\<turnstile>v::\<preceq>T|] ==> G,s\<turnstile>l(vn\<mapsto>v)[::\<preceq>]L(vn\<mapsto>T)"
    apply (unfold lconf_def)
    apply auto
    done

    lemma lconf_ext_list [rule_format (no_asm)]:
      "G,h\<turnstile>l[::\<preceq>]L ==> ∀vs Ts. distinct vns --> length Ts = length vns -->
      list_all2 (λv T. G,h\<turnstile>v::\<preceq>T) vs Ts --> G,h\<turnstile>l(vns[\<mapsto>]vs)[::\<preceq>]L(vns[\<mapsto>]Ts)"
    apply (unfold lconf_def)
    apply( induct_tac "vns")
    apply(  clarsimp)
    apply( clarsimp)
    apply( frule list_all2_lengthD)
    apply( auto simp add: length_Suc_conv)
    done

    lemma lconf_restr: "[|lT vn = None; G, h \<turnstile> l [::\<preceq>] lT(vn\<mapsto>T)|] ==> G, h \<turnstile> l [::\<preceq>] lT"
    apply (unfold lconf_def)
    apply (intro strip)
    apply (case_tac "n = vn")
    apply auto
    done

    section "oconf"

    lemma oconf_hext: "G,h\<turnstile>obj\<surd> ==> h≤|h' ==> G,h'\<turnstile>obj\<surd>"
    apply (unfold oconf_def)
    apply (fast)
    done

    lemma oconf_obj: "G,h\<turnstile>(C,fs)\<surd> =
      (∀T f. map_of(fields (G,C)) f = Some T --> (∃v. fs f = Some v ∧  G,h\<turnstile>v::\<preceq>T))"
    apply (unfold oconf_def lconf_def)
    apply auto
    done

    lemmas oconf_objD = oconf_obj [THEN iffD1, THEN spec, THEN spec, THEN mp]

    section "hconf"

    lemma hconfD: "[|G\<turnstile>h h\<surd>; h a = Some obj|] ==> G,h\<turnstile>obj\<surd>"
    apply (unfold hconf_def)
    apply (fast)
    done

    lemma hconfI: "∀a obj. h a=Some obj --> G,h\<turnstile>obj\<surd> ==> G\<turnstile>h h\<surd>"
    apply (unfold hconf_def)
    apply (fast)
    done

    section "xconf"

    lemma xconf_raise_if: "xconf h x ==> xconf h (raise_if b xcn x)"
    by (simp add: xconf_def raise_if_def)

    section "conforms"

    lemma conforms_heapD: "(x, (h, l))::\<preceq>(G, lT) ==> G\<turnstile>h h\<surd>"
    apply (unfold conforms_def)
    apply (simp)
    done

    lemma conforms_localD: "(x, (h, l))::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT"
    apply (unfold conforms_def)
    apply (simp)
    done

    lemma conforms_xcptD: "(x, (h, l))::\<preceq>(G, lT) ==> xconf h x"
    apply (unfold conforms_def)
    apply (simp)
    done

    lemma conformsI: "[|G\<turnstile>h h\<surd>; G,h\<turnstile>l[::\<preceq>]lT; xconf h x|] ==> (x, (h, l))::\<preceq>(G, lT)"
    apply (unfold conforms_def)
    apply auto
    done

    lemma conforms_restr: "[|lT vn = None; s ::\<preceq> (G, lT(vn\<mapsto>T)) |] ==> s ::\<preceq> (G, lT)"
    by (simp add: conforms_def, fast intro: lconf_restr)

    lemma conforms_xcpt_change: "[| (x, (h,l))::\<preceq> (G, lT); xconf h x --> xconf h x' |] ==> (x', (h,l))::\<preceq> (G, lT)"
    by (simp add: conforms_def)

    lemma preallocated_hext: "[| preallocated h; h≤|h'|] ==> preallocated h'"
    by (simp add: preallocated_def hext_def)

    lemma xconf_hext: "[| xconf h vo; h≤|h'|] ==> xconf h' vo"
    by (simp add: xconf_def preallocated_def hext_def)

    lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h≤|h'; G\<turnstile>h h'\<surd> |]
      ==> (x,(h',l))::\<preceq>(G,lT)"
    by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)

    lemma conforms_upd_obj:
      "[|(x,(h,l))::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h≤|h(a\<mapsto>obj)|]
      ==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)"
    apply(rule conforms_hext)
    apply  auto
    apply(rule hconfI)
    apply(drule conforms_heapD)
    apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"]
                    addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *})
    done

    lemma conforms_upd_local:
    "[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|]
      ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)"
    apply (unfold conforms_def)
    apply( auto elim: lconf_upd)
    done

    end

## hext

lemma hextI:

      ∀a C fs. h a = Some (C, fs) --> (∃fs'. h' a = Some (C, fs')) ==> h <=| h'

lemma hext_objD:

      [| h <=| h'; h a = Some (C, fs) |] ==> ∃fs'. h' a = Some (C, fs')

lemma hext_refl:

      h <=| h

lemma hext_new:

      h a = None ==> h <=| h(a |-> x)

lemma hext_trans:

      [| h <=| h'; h' <=| h'' |] ==> h <=| h''

lemma hext_upd_obj:

      h a = Some (C, fs) ==> h <=| h(a |-> (C, fs'))

## conf

lemma conf_Null:

      (G,h |- Null ::<= T) = G |- NT <= T

lemma conf_litval:

      typeof empty v = Some T ==> G,h |- v ::<= T

lemma conf_AddrI:

      [| h a = Some obj; G |- obj_ty obj <= T |] ==> G,h |- Addr a ::<= T

lemma conf_obj_AddrI:

      [| h a = Some (C, fs); G |- C <=C D |] ==> G,h |- Addr a ::<= Class D

lemma defval_conf:

      is_type G T ==> G,h |- default_val T ::<= T

lemma conf_upd_obj:

      h a = Some (C, fs) ==> (G,h(a |-> (C, fs')) |- x ::<= T) = (G,h |- x ::<= T)

lemma conf_widen:

      [| wf_prog wf_mb G; G,h |- x ::<= T; G |- T <= T' |] ==> G,h |- x ::<= T'

lemma conf_hext:

      [| h <=| h'; G,h |- v ::<= T |] ==> G,h' |- v ::<= T

lemma new_locD:

      [| h a = None; G,h |- Addr t ::<= T |] ==> t ≠ a

lemma conf_RefTD:

      G,h |- a' ::<= RefT T
      ==> a' = Null ∨
          (∃a obj T'.
              a' = Addr a ∧ h a = Some obj ∧ obj_ty obj = T' ∧ G |- T' <= RefT T)

lemma conf_NullTD:

      G,h |- a' ::<= NT ==> a' = Null

lemma non_npD:

      [| a' ≠ Null; G,h |- a' ::<= RefT t |]
      ==> ∃a C fs. a' = Addr a ∧ h a = Some (C, fs) ∧ G |- Class C <= RefT t

lemma non_np_objD:

      [| a' ≠ Null; G,h |- a' ::<= Class C |]
      ==> ∃a C' fs. a' = Addr a ∧ h a = Some (C', fs) ∧ G |- C' <=C C

lemma non_np_objD':

      [| a' ≠ Null; wf_prog wf_mb G; G,h |- a' ::<= RefT t |]
      ==> ∃a C fs. a' = Addr a ∧ h a = Some (C, fs) ∧ G |- Class C <= RefT t

lemma conf_list_gext_widen:

      [| wf_prog wf_mb G; list_all2 (conf G h) vs Ts;
         list_all2 (%T T'. G |- T <= T') Ts Ts' |]
      ==> list_all2 (conf G h) vs Ts'

## lconf

lemma lconfD:

      [| G,h |- vs [::<=] Ts; Ts n = Some T |] ==> G,h |- the (vs n) ::<= T

lemma lconf_hext:

      [| G,h |- l [::<=] L; h <=| h' |] ==> G,h' |- l [::<=] L

lemma lconf_upd:

      [| G,h |- l [::<=] lT; G,h |- v ::<= T; lT va = Some T |]
      ==> G,h |- l(va |-> v) [::<=] lT

lemma lconf_init_vars_lemma:

      [| ∀x. P x --> R (dv x) x; ∀x. map_of fs f = Some x --> P x;
         map_of fs f = Some T |]
      ==> ∃v. map_of (map (%(f, ft). (f, dv ft)) fs) f = Some v ∧ R v T

lemma lconf_init_vars:

      ∀n T. map_of fs n = Some T --> is_type G T
      ==> G,h |- init_vars fs [::<=] map_of fs

lemma lconf_ext:

      [| G,s |- l [::<=] L; G,s |- v ::<= T |]
      ==> G,s |- l(vn |-> v) [::<=] L(vn |-> T)

lemma lconf_ext_list:

      [| G,h |- l [::<=] L; distinct vns; length Ts = length vns;
         list_all2 (conf G h) vs Ts |]
      ==> G,h |- l(vns [|->] vs) [::<=] L(vns [|->] Ts)

lemma lconf_restr:

      [| lT vn = None; G,h |- l [::<=] lT(vn |-> T) |] ==> G,h |- l [::<=] lT

## oconf

lemma oconf_hext:

      [| G,h |- obj [ok]; h <=| h' |] ==> G,h' |- obj [ok]

lemma oconf_obj:

      (G,h |- (C, fs) [ok]) =
      (∀T f. map_of (fields (G, C)) f = Some T -->
             (∃v. fs f = Some v ∧ G,h |- v ::<= T))

lemmas oconf_objD:

      [| G4,h4 |- (C4, fs4) [ok]; map_of (fields (G4, C4)) x1 = Some x2 |]
      ==> ∃v. fs4 x1 = Some v ∧ G4,h4 |- v ::<= x2

lemmas oconf_objD:

      [| G4,h4 |- (C4, fs4) [ok]; map_of (fields (G4, C4)) x1 = Some x2 |]
      ==> ∃v. fs4 x1 = Some v ∧ G4,h4 |- v ::<= x2

## hconf

lemma hconfD:

      [| G |-h h [ok]; h a = Some obj |] ==> G,h |- obj [ok]

lemma hconfI:

      ∀a obj. h a = Some obj --> G,h |- obj [ok] ==> G |-h h [ok]

## xconf

lemma xconf_raise_if:

      xconf h x ==> xconf h (raise_if b xcn x)

## conforms

lemma conforms_heapD:

      (x, h, l) ::<= (G, lT) ==> G |-h h [ok]

lemma conforms_localD:

      (x, h, l) ::<= (G, lT) ==> G,h |- l [::<=] lT

lemma conforms_xcptD:

      (x, h, l) ::<= (G, lT) ==> xconf h x

lemma conformsI:

      [| G |-h h [ok]; G,h |- l [::<=] lT; xconf h x |] ==> (x, h, l) ::<= (G, lT)

lemma conforms_restr:

      [| lT vn = None; s ::<= (G, lT(vn |-> T)) |] ==> s ::<= (G, lT)

lemma conforms_xcpt_change:

      [| (x, h, l) ::<= (G, lT); xconf h x --> xconf h x' |]
      ==> (x', h, l) ::<= (G, lT)

lemma preallocated_hext:

      [| preallocated h; h <=| h' |] ==> preallocated h'

lemma xconf_hext:

      [| xconf h vo; h <=| h' |] ==> xconf h' vo

lemma conforms_hext:

      [| (x, h, l) ::<= (G, lT); h <=| h'; G |-h h' [ok] |]
      ==> (x, h', l) ::<= (G, lT)

lemma conforms_upd_obj:

      [| (x, h, l) ::<= (G, lT); G,h(a |-> obj) |- obj [ok]; h <=| h(a |-> obj) |]
      ==> (x, h(a |-> obj), l) ::<= (G, lT)

lemma conforms_upd_local:

      [| (x, h, l) ::<= (G, lT); G,h |- v ::<= T; lT va = Some T |]
      ==> (x, h, l(va |-> v)) ::<= (G, lT)