Theory JinjaDCI.WellForm

(*  Title:      JinjaDCI/Common/WellForm.thy

    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory J/WellForm.thy by Tobias Nipkow
*)

section ‹ Generic Well-formedness of programs ›

theory WellForm imports TypeRel SystemClasses begin

text ‹\noindent This theory defines global well-formedness conditions
for programs but does not look inside method bodies.  Hence it works
for both Jinja and JVM programs. Well-typing of expressions is defined
elsewhere (in theory @{text WellType}).

Because Jinja does not have method overloading, its policy for method
overriding is the classical one: \emph{covariant in the result type
but contravariant in the argument types.} This means the result type
of the overriding method becomes more specific, the argument types
become more general.
›

type_synonym 'm wf_mdecl_test = "'m prog  cname  'm mdecl  bool"

definition wf_fdecl :: "'m prog  fdecl  bool"
where
  "wf_fdecl P  λ(F,b,T). is_type P T"

definition wf_mdecl :: "'m wf_mdecl_test  'm wf_mdecl_test"
where
  "wf_mdecl wf_md P C  λ(M,b,Ts,T,m).
  (Tset Ts. is_type P T)  is_type P T  wf_md P C (M,b,Ts,T,m)"

definition wf_clinit :: "'m mdecl list  bool" where
"wf_clinit ms = (m. (clinit,Static,[],Void,m)set ms)"

definition wf_cdecl :: "'m wf_mdecl_test  'm prog  'm cdecl  bool"
where
  "wf_cdecl wf_md P    λ(C,(D,fs,ms)).
  (fset fs. wf_fdecl P f)   distinct_fst fs 
  (mset ms. wf_mdecl wf_md P C m)   distinct_fst ms 
  (C  Object 
   is_class P D  ¬ P  D * C 
   ((M,b,Ts,T,m)set ms.
      D' b' Ts' T' m'. P  D sees M,b':Ts'  T' = m' in D' 
                       b = b'  P  Ts' [≤] Ts  P  T  T')) 
  wf_clinit ms"

definition wf_syscls :: "'m prog  bool"
where
  "wf_syscls P    {Object}  sys_xcpts  set(map fst P)"

definition wf_prog :: "'m wf_mdecl_test  'm prog  bool"
where
  "wf_prog wf_md P    wf_syscls P  (c  set P. wf_cdecl wf_md P c)  distinct_fst P"


subsection‹ Well-formedness lemmas ›

lemma class_wf: 
  "class P C = Some c; wf_prog wf_md P  wf_cdecl wf_md P (C,c)"
(*<*)by (unfold wf_prog_def class_def) (fast dest: map_of_SomeD)(*>*)


lemma class_Object [simp]: 
  "wf_prog wf_md P  C fs ms. class P Object = Some (C,fs,ms)"
(*<*)by (unfold wf_prog_def wf_syscls_def class_def)
        (auto simp: map_of_SomeI)
(*>*)


lemma is_class_Object [simp]:
  "wf_prog wf_md P  is_class P Object"
(*<*)by (simp add: is_class_def)(*>*)

lemma is_class_supclass:
assumes wf: "wf_prog wf_md P" and sub: "P  C * D"
shows "is_class P C  is_class P D"
(*<*)
using sub proof(induct)
  case step then show ?case
    by(auto simp:wf_cdecl_def is_class_def dest!:class_wf[OF _ wf] subcls1D)
qed simp
(*>*)

lemma is_class_xcpt:
  " C  sys_xcpts; wf_prog wf_md P   is_class P C"
(*<*)
by (fastforce intro!: map_of_SomeI
              simp add: wf_prog_def wf_syscls_def is_class_def class_def)
(*>*)


lemma subcls1_wfD:
assumes sub1: "P  C 1 D" and wf: "wf_prog wf_md P"
shows "D  C  (D,C)  (subcls1 P)+"
(*<*)
proof -
  obtain fs ms where "C  Object" and cls: "class P C = (D, fs, ms)"
    using subcls1D[OF sub1] by clarify
  then show ?thesis using wf class_wf[OF cls wf] r_into_trancl[OF sub1]
    by(force simp add: wf_cdecl_def reflcl_trancl [THEN sym]
             simp del: reflcl_trancl)
qed
(*>*)


lemma wf_cdecl_supD: 
  "wf_cdecl wf_md P (C,D,r); C  Object  is_class P D"
(*<*)by (auto simp: wf_cdecl_def)(*>*)


lemma subcls_asym:
  " wf_prog wf_md P; (C,D)  (subcls1 P)+   (D,C)  (subcls1 P)+"
(*<*)by(erule tranclE; fast dest!: subcls1_wfD intro: trancl_trans)(*>*)


lemma subcls_irrefl:
  " wf_prog wf_md P; (C,D)  (subcls1 P)+   C  D"
(*<*)by (erule trancl_trans_induct) (auto dest: subcls1_wfD subcls_asym)(*>*)


lemma acyclic_subcls1:
  "wf_prog wf_md P  acyclic (subcls1 P)"
(*<*)by (unfold acyclic_def) (fast dest: subcls_irrefl)(*>*)


lemma wf_subcls1:
  "wf_prog wf_md P  wf ((subcls1 P)¯)"
(*<*)
proof -
  assume wf: "wf_prog wf_md P"
  have "finite (subcls1 P)" by(rule finite_subcls1)
  then have fin': "finite ((subcls1 P)¯)" by(subst finite_converse)

  from wf have "acyclic (subcls1 P)" by(rule acyclic_subcls1)
  then have acyc': "acyclic ((subcls1 P)¯)" by (subst acyclic_converse)

  from fin' acyc' show ?thesis by (rule finite_acyclic_wf)
qed
(*>*)


lemma single_valued_subcls1:
  "wf_prog wf_md G  single_valued (subcls1 G)"
(*<*)
by(auto simp:wf_prog_def distinct_fst_def single_valued_def dest!:subcls1D)
(*>*)


lemma subcls_induct: 
  " wf_prog wf_md P; C. D. (C,D)  (subcls1 P)+  Q D  Q C   Q C"
(*<*)
  (is "?A  PROP ?P  _")
proof -
  assume p: "PROP ?P"
  assume ?A then have wf: "wf_prog wf_md P" by assumption
  have wf':"wf (((subcls1 P)+)¯)" using wf_trancl[OF wf_subcls1[OF wf]]
    by(simp only: trancl_converse)
  show ?thesis using wf_induct[where a = C and P = Q, OF wf' p] by simp
qed
(*>*)


lemma subcls1_induct_aux:
assumes "is_class P C" and wf: "wf_prog wf_md P" and QObj: "Q Object"
shows
 " C D fs ms.
     C  Object; is_class P C; class P C = Some (D,fs,ms) 
      wf_cdecl wf_md P (C,D,fs,ms)  P  C 1 D  is_class P D  Q D  Q C 
   Q C"
(*<*)
  (is "PROP ?P  _")
proof -
  assume p: "PROP ?P"
  have "class P C  None  Q C"
  proof(induct rule: subcls_induct[OF wf])
    case (1 C)
    have "class P C  None  Q C"
    proof(cases "C = Object")
      case True
      then show ?thesis using QObj by fast
    next
      case False
      assume nNone: "class P C  None"
      then have is_cls: "is_class P C" by(simp add: is_class_def)
      obtain D fs ms where cls: "class P C = (D, fs, ms)" using nNone by safe
      also have wfC: "wf_cdecl wf_md P (C, D, fs, ms)" by(rule class_wf[OF cls wf])
      moreover have D: "is_class P D" by(rule wf_cdecl_supD[OF wfC False])
      moreover have "P  C 1 D" by(rule subcls1I[OF cls False])
      moreover have "class P D  None" using D by(simp add: is_class_def)
      ultimately show ?thesis using 1 by (auto intro: p[OF False is_cls])
    qed
  then show "class P C  None  Q C" by simp
  qed
  thus ?thesis using assms by(unfold is_class_def) simp
qed
(*>*)

(* FIXME can't we prove this one directly?? *)
lemma subcls1_induct [consumes 2, case_names Object Subcls]:
  " wf_prog wf_md P; is_class P C; Q Object;
    C D. C  Object; P  C 1 D; is_class P D; Q D  Q C 
   Q C"
(*<*)by (erule (2) subcls1_induct_aux) blast(*>*)


lemma subcls_C_Object:
assumes "class": "is_class P C" and wf: "wf_prog wf_md P"
shows "P  C * Object"
(*<*)
using wf "class"
proof(induct rule: subcls1_induct)
  case Subcls
  then show ?case by(simp add: converse_rtrancl_into_rtrancl)
qed fast
(*>*)


lemma is_type_pTs:
assumes "wf_prog wf_md P" and "(C,S,fs,ms)  set P" and "(M,b,Ts,T,m)  set ms"
shows "set Ts  types P"
(*<*)
proof
  from assms have "wf_mdecl wf_md P C (M,b,Ts,T,m)" 
    by (unfold wf_prog_def wf_cdecl_def) auto
  hence "t  set Ts. is_type P t" by (unfold wf_mdecl_def) auto
  moreover fix t assume "t  set Ts"
  ultimately have "is_type P t" by blast
  thus "t  types P" ..
qed
(*>*)

lemma wf_supercls_distinct_app:
assumes wf:"wf_prog wf_md P"
  and nObj: "C  Object" and cls: "class P C = (D, fs, ms)"
  and super: "supercls_lst P (C#Cs)" and dist: "distinct (C#Cs)"
shows "distinct (D#C#Cs)"
proof -
  have "¬ P  D * C" using subcls1_wfD[OF subcls1I[OF cls nObj] wf]
    by (simp add: rtrancl_eq_or_trancl)
  then show ?thesis using assms by auto
qed


subsection‹ Well-formedness and method lookup ›

lemma sees_wf_mdecl:
assumes wf: "wf_prog wf_md P" and sees: "P  C sees M,b:TsT = m in D"
shows "wf_mdecl wf_md P D (M,b,Ts,T,m)"
(*<*)
using wf visible_method_exists[OF sees] proof(cases b)
qed (fastforce simp:wf_cdecl_def dest!:class_wf dest:map_of_SomeD)+
(*>*)

lemma sees_method_mono [rule_format (no_asm)]: 
assumes sub: "P  C' * C" and wf: "wf_prog wf_md P"
shows "D b Ts T m. P  C sees M,b:TsT = m in D 
     (D' Ts' T' m'. P  C' sees M,b:Ts'T' = m' in D'  P  Ts [≤] Ts'  P  T'  T)"
(*<*)
  (is "D b Ts T m. ?P C D b Ts T m  ?Q C' D b Ts T m")
proof(rule disjE[OF rtranclD[OF sub]])
  assume "C' = C"
  then show ?thesis using assms by fastforce
next
  assume "C'  C  (C', C)  (subcls1 P)+"
  then have neq: "C'  C" and subcls1: "(C', C)  (subcls1 P)+" by simp+
  show ?thesis proof(induct rule: trancl_trans_induct[OF subcls1])
    case (2 x y z)
    then have zy: "D b Ts T m. ?P z D b Ts T m  ?Q y D b Ts T m" by blast
    have "D b Ts T m. ?P z D b Ts T m  ?Q x D b Ts T m"
    proof -
      fix D b Ts T m assume P: "?P z D b Ts T m"
      then show "?Q x D b Ts T m" using zy[OF P] 2(2)
        by(fast elim: widen_trans widens_trans)
    qed
    then show ?case by blast
  next
    case (1 x y)
    have "D b Ts T m. ?P y D b Ts T m  ?Q x D b Ts T m"
    proof -
      fix D b Ts T m assume P: "?P y D b Ts T m"
      then obtain Mm where sees: "P  y sees_methods Mm" and
                           M: "Mm M = ((b, Ts, T, m), D)"
        by(clarsimp simp:Method_def)
      obtain fs ms where nObj: "x  Object" and
                         cls: "class P x = (y, fs, ms)"
        using subcls1D[OF 1] by clarsimp
      have x_meth: "P  x sees_methods Mm ++ (map_option (λm. (m, x))  map_of ms)"
        using sees_methods_rec[OF cls nObj sees] by simp
      show "?Q x D b Ts T m" proof(cases "map_of ms M")
        case None
        then have "m'. P  x sees M, b :  TsT = m' in D" using M x_meth
          by(fastforce simp add:Method_def map_add_def split:option.split)
        then show ?thesis by auto
      next
        case (Some a)
        then obtain b' Ts' T' m' where a: "a = (b',Ts',T',m')" by(cases a)
        then have "(m' Mm. P  y sees_methods Mm  Mm M = ((b, Ts, T, m'), D))
               b' = b  P  Ts [≤] Ts'  P  T'  T"
          using nObj class_wf[OF cls wf] map_of_SomeD[OF Some]
          by(clarsimp simp: wf_cdecl_def Method_def) fast
        then show ?thesis using Some a sees M x_meth
          by(fastforce simp:Method_def map_add_def split:option.split)
      qed
    qed
    then show ?case by simp
  qed
qed
(*>*)


lemma sees_method_mono2:
  " P  C' * C; wf_prog wf_md P;
     P  C sees M,b:TsT = m in D; P  C' sees M,b':Ts'T' = m' in D' 
   b = b'  P  Ts [≤] Ts'  P  T'  T"
(*<*)by(blast dest:sees_method_mono sees_method_fun)(*>*)

lemma mdecls_visible:
assumes wf: "wf_prog wf_md P" and "class": "is_class P C"
shows "D fs ms. class P C = Some(D,fs,ms)
          Mm. P  C sees_methods Mm  ((M,b,Ts,T,m)  set ms. Mm M = Some((b,Ts,T,m),C))"
(*<*)
using wf "class"
proof (induct rule:subcls1_induct)
  case Object
  with wf have dfst:"distinct_fst ms"
    by (unfold class_def wf_prog_def wf_cdecl_def) (fastforce dest:map_of_SomeD)
  with dfst have "distinct_fst ms"
    by(blast dest: distinct_fst_appendD)
  with Object show ?case by(fastforce intro!: sees_methods_Object map_of_SomeI)
next
  case Subcls
  with wf have dfst:"distinct_fst ms"
    by (unfold class_def wf_prog_def wf_cdecl_def) (fastforce dest:map_of_SomeD)
  with dfst have "distinct_fst ms"
    by(blast dest: distinct_fst_appendD)
  with Subcls show ?case
    by(fastforce elim:sees_methods_rec dest:subcls1D map_of_SomeI
                simp:is_class_def)
qed
(*>*)

lemma mdecl_visible:
assumes wf: "wf_prog wf_md P" and C: "(C,S,fs,ms)  set P" and  m: "(M,b,Ts,T,m)  set ms"
shows "P  C sees M,b:TsT = m in C"
(*<*)
proof -
  from wf C have "class": "class P C = Some (S,fs,ms)"
    by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
  from "class" have "is_class P C" by(auto simp:is_class_def)                   
  with assms "class" show ?thesis
    by(bestsimp simp:Method_def dest:mdecls_visible)
qed
(*>*)


lemma Call_lemma:
assumes sees: "P  C sees M,b:TsT = m in D" and sub: "P  C' * C" and wf: "wf_prog wf_md P"
shows "D' Ts' T' m'.
       P  C' sees M,b:Ts'T' = m' in D'  P  Ts [≤] Ts'  P  T'  T  P  C' * D'
        is_type P T'  (Tset Ts'. is_type P T)  wf_md P D' (M,b,Ts',T',m')"
(*<*)
using assms sees_method_mono[OF sub wf sees]
by(fastforce intro:sees_method_decl_above dest:sees_wf_mdecl
             simp: wf_mdecl_def)
(*>*)


lemma wf_prog_lift:
  assumes wf: "wf_prog (λP C bd. A P C bd) P"
  and rule:
  "wf_md C M b Ts C T m bd.
   wf_prog wf_md P 
   P  C sees M,b:TsT = m in C 
   set Ts   types P 
   bd = (M,b,Ts,T,m) 
   A P C bd 
   B P C bd"
  shows "wf_prog (λP C bd. B P C bd) P"
(*<*)
proof -
  have "c. cset P  wf_cdecl A P c  wf_cdecl B P c"
  proof -
    fix c assume "cset P" and "wf_cdecl A P c"
    then show "wf_cdecl B P c"
     using rule[OF wf mdecl_visible[OF wf] is_type_pTs[OF wf]]
     by (auto simp: wf_cdecl_def wf_mdecl_def)
  qed
  then show ?thesis using wf by (clarsimp simp: wf_prog_def)
qed
(*>*)

lemma wf_sees_clinit:
assumes wf:"wf_prog wf_md P" and ex: "class P C = Some a"
shows "m. P  C sees clinit,Static:[]  Void = m in C"
proof -
  from ex obtain D fs ms where "a = (D,fs,ms)" by(cases a)
  then have sP: "(C, D, fs, ms)  set P" using ex map_of_SomeD[of P C a] by(simp add: class_def)
  then have "wf_clinit ms" using assms by(unfold wf_prog_def wf_cdecl_def, auto)
  then obtain m where sm: "(clinit, Static, [], Void, m)  set ms" by (meson wf_clinit_def)
  then have "P  C sees clinit,Static:[]  Void = m in C"
    using mdecl_visible[OF wf sP sm] by simp
  then show ?thesis by(rule exI)
qed
(*>*)

lemma wf_sees_clinit1:
assumes wf:"wf_prog wf_md P" and ex: "class P C = Some a"
and "P  C sees clinit,b:Ts  T = m in D"
shows "b = Static  Ts = []  T = Void  D = C"
proof -
  obtain m' where sees: "P  C sees clinit,Static:[]  Void = m' in C"
    using wf_sees_clinit[OF wf ex] by clarify
  then show ?thesis using sees wf by (meson assms(3) sees_method_fun)
qed

lemma wf_NonStatic_nclinit:
assumes wf: "wf_prog wf_md P" and meth: "P  C sees M,NonStatic:TsT=(mxs,mxl,ins,xt) in D"
shows "M  clinit"
proof -
  from sees_method_is_class[OF meth] obtain a where cls: "class P C = Some a"
    by(clarsimp simp: is_class_def)
  with wf wf_sees_clinit[OF wf cls]
   obtain m where "P  C sees clinit,Static:[]Void=m in C" by clarsimp
  with meth show ?thesis by(auto dest: sees_method_fun)
qed

subsection‹ Well-formedness and field lookup ›

lemma wf_Fields_Ex:
assumes wf: "wf_prog wf_md P" and "is_class P C"
shows "FDTs. P  C has_fields FDTs"
(*<*)
using assms proof(induct rule:subcls1_induct)
  case Object
  then show ?case using class_Object[OF wf]
    by(blast intro:has_fields_Object)
next
  case Subcls
  then show ?case by(blast intro:has_fields_rec dest:subcls1D)
qed
(*>*)


lemma has_fields_types:
  " P  C has_fields FDTs; (FD,b,T)  set FDTs; wf_prog wf_md P   is_type P T"
(*<*)
proof(induct rule:Fields.induct)
qed(fastforce dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)+
(*>*)

lemma sees_field_is_type:
  " P  C sees F,b:T in D; wf_prog wf_md P   is_type P T"
(*<*)
  by (meson has_field_def has_fields_types has_visible_field map_of_SomeD)
(*>*)


lemma wf_syscls:
  "set SystemClasses  set P  wf_syscls P"
(*<*)
by (force simp: image_def SystemClasses_def wf_syscls_def sys_xcpts_def
                ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def
                NoClassDefFoundC_def
                IncompatibleClassChangeC_def NoSuchFieldC_def NoSuchMethodC_def)
(*>*)


subsection‹ Well-formedness and subclassing ›

lemma wf_subcls_nCls:
assumes wf: "wf_prog wf_md P" and ns: "¬ is_class P C"
shows " P  D * D'; D  C   D'  C"
proof(induct rule: rtrancl.induct)
  case (rtrancl_into_rtrancl a b c)
  with ns show ?case by(clarsimp dest!: subcls1D wf_cdecl_supD[OF class_wf[OF _ wf]])
qed(simp)

lemma wf_subcls_nCls':
assumes wf: "wf_prog wf_md P" and ns: "¬is_class P C0"
shows "cd D'. cd  set P  ¬P  fst cd * C0"
proof -
  fix cd D' assume cd: "cd  set P"
  then have cls: "is_class P (fst cd)" using class_exists_equiv is_class_def by blast
  with wf_subcls_nCls[OF wf ns] ns show "¬P  fst cd * C0" by(cases "fst cd = D'", auto)
qed

lemma wf_nclass_nsub:
 " wf_prog wf_md P; is_class P C; ¬is_class P C'   ¬P  C * C'"
 by(rule notI, auto dest: wf_subcls_nCls[where C=C' and D=C])

lemma wf_sys_xcpt_nsub_Start:
assumes wf: "wf_prog wf_md P" and ns: "¬is_class P Start" and sx: "C  sys_xcpts"
shows "¬P  C * Start"
proof -
  have Cns: "C  Start" using Start_nsys_xcpts sx by clarsimp
  show ?thesis using wf_subcls_nCls[OF wf ns _ Cns] by auto
qed

end