Theory SemiType

(*  Title:      JinjaThreads/BV/SemiType.thy
    Author:     Tobias Nipkow, Gerwin Klein, Andreas Lochbihler
*)

header {* 
  \chapter{Bytecode verifier}
  \isaheader{The Jinja Type System as a Semilattice} 
*}

theory SemiType
imports "../Common/WellForm" "../../Jinja/DFA/Semilattices"
begin

inductive_set
  widen1 :: "'a prog => (ty × ty) set"
  and widen1_syntax :: "'a prog => ty => ty => bool" ("_ \<turnstile> _ <1 _" [71,71,71] 70)
  for P :: "'a prog"
where
  "P \<turnstile> C <1 D ≡ (C, D) ∈ widen1 P"

| widen1_Array_Object:
  "(* is_class P Object ==> *) P \<turnstile> Array (Class Object) <1 Class Object"

| widen1_Array_Integer:
  "P \<turnstile> Array Integer <1 Class Object"

| widen1_Array_Boolean:
  "P \<turnstile> Array Boolean <1 Class Object"

| widen1_Array_Void:
  "P \<turnstile> Array Void <1 Class Object"

| widen1_Class: 
  "P \<turnstile> C \<prec>1 D ==> P \<turnstile> Class C <1 Class D"

| widen1_Array_Array:
  "[| P \<turnstile> T <1 U; ¬ is_NT_Array T |] ==> P \<turnstile> Array T <1 Array U"

| widen1_NT_Object:
  "is_NT_Array T ==> P \<turnstile> Array T <1 Class Object"

abbreviation widen1_trancl :: "'a prog => ty => ty => bool" ("_ \<turnstile> _ <+ _" [71,71,71] 70) where
  "P \<turnstile> T <+ U ≡ (T, U) ∈ trancl (widen1 P)"

lemma widen1_Integer [iff]:
  "¬ P \<turnstile> Integer <1 T"
  by(auto elim: widen1.cases)

lemma widen1_Boolean [iff]:
  "¬ P \<turnstile> Boolean <1 T"
  by(auto elim: widen1.cases)

lemma widen1_Void [iff]:
  "¬ P \<turnstile> Void <1 T"
  by(auto elim: widen1.cases)

lemma widen1_Class_Object [iff]:
  "¬ P \<turnstile> Class Object <1 T"
  by(auto elim: widen1.cases)

lemma widen1_NT [simp]: "¬ P \<turnstile> NT <1 U"
by(auto elim: widen1.cases)

lemma is_type_widen1: 
  assumes icO: "is_class P Object"
  shows "P \<turnstile> T <1 U ==> is_type P T"
apply(induct rule: widen1.induct)
apply(auto intro: subcls_is_class NT_Array_is_type icO)
done


lemma widen1_NT_Array:
  assumes NT: "is_NT_Array T"
  shows "P \<turnstile> T⌊⌉ <1 U <-> U = Class Object"
proof(rule iffI)
  assume "P \<turnstile> T⌊⌉ <1 U"
  moreover
  { fix T'
    have "[| P \<turnstile> T' <1 U; T' = T⌊⌉; is_NT_Array T' |] ==> U = Class Object"
      by(induct arbitrary: T rule: widen1.induct, auto) }
  ultimately show "U = Class Object" using NT by auto
next
  assume "U = Class Object"
  with NT show "P \<turnstile> T⌊⌉ <1 U"
    by(auto intro: widen1_NT_Object)
qed

lemma widen1_is_type:
  assumes wfP: "wf_prog wfmd P"
  shows "(A, B) ∈ widen1 P ==> is_type P B"
proof(induct rule: widen1.induct)
  case (widen1_Class C D)
  note CD = `P \<turnstile> C \<prec>1 D`
  hence "is_class P C"
    by(auto intro: subcls_is_class)
  with CD have "is_class P D"
    by(auto intro: converse_subcls_is_class[OF wfP])
  thus ?case by simp
qed(insert wfP, auto intro: NT_Array_is_type)

lemma widen1_trancl_is_type:
  assumes wfP: "wf_prog wfmd P"
  shows "(A, B) ∈ (widen1 P)^+ ==> is_type P B"
apply(induct rule: trancl_induct)
apply(auto intro: widen1_is_type[OF wfP])
done

lemma single_valued_widen1:
  assumes wf: "wf_prog wf_md P"
  shows "single_valued (widen1 P)"
proof(rule single_valuedI)
  { fix x y z
    have "[| P \<turnstile> x <1 y; P \<turnstile> x <1 z |] ==> y = z"
    proof(induct arbitrary: z rule: widen1.induct)
      case widen1_Class
      with single_valued_subcls1[OF wf] show ?case
        by(auto dest: single_valuedD elim!: widen1.cases)
    next
      case (widen1_Array_Array T U z)
      from `P \<turnstile> T⌊⌉ <1 z` `P \<turnstile> T <1 U` `¬ is_NT_Array T`
      obtain z'
        where z': "z = z'⌊⌉"
        and Tz': "P \<turnstile> T <1 z'"
        by(auto elim: widen1.cases)
      with `!!z. P \<turnstile> T <1 z ==> U = z` have "U = z'" by blast
      with z' show ?case by simp
    qed(auto elim: widen1.cases) }
  thus "∀x y. P \<turnstile> x <1 y --> (∀z. P \<turnstile> x <1 z --> y = z)" by blast
qed

function class_numbering :: "'a prog => cname => nat" where
  "class_numbering P C =
   (if acyclicP (subcls1 P) ∧ is_class P C ∧ C ≠ Object
    then Suc (class_numbering P (fst (the (class P C))))
    else 0)"
by(pat_completeness, auto)
termination
proof(relation "{((P, C), (P', C')). P = P' ∧ acyclicP (subcls1 P) ∧ P \<turnstile> C' \<prec>1 C}")
  show "wf {((P, C), P', C'). P = P' ∧ acyclicP (subcls1 P) ∧ P \<turnstile> C' \<prec>1 C}"
  proof(rule wfUNIVI)
    fix Q x
    assume "∀x. (∀y. (y, x) ∈ {((P, C), P', C'). P = P' ∧ acyclicP (subcls1 P) ∧ P \<turnstile> C' \<prec>1 C} --> Q y) --> Q x"
    hence wf: "!!x. (!!y. (y, x) ∈ {((P, C), P', C'). P = P' ∧ acyclicP (subcls1 P) ∧ P \<turnstile> C' \<prec>1 C} ==> Q y) ==> Q x" by blast
    obtain P C where PC: "(x :: 'c prog × cname) = (P, C)" by(cases x, auto)
    show "Q x"
    proof(cases "acyclicP (subcls1 P)")
      case False
      with PC show "Q x"
        by(auto intro: wf)
    next
      case True
      from True
      have wf'': "!!x. (!!y. (subcls1 P)¯¯ y x ==> Q (P, y)) ==> Q (P, x)"
        by(auto intro: wf)
      show ?thesis
      proof(unfold PC, rule wf_induct[where P="λC. Q (P, C)"])
        from True finite_subcls1'[of P] show "wf {(D, C). P \<turnstile> C \<prec>1 D}"
          apply -
          apply(erule finite_acyclic_wf)
          apply(subst acyclic_converse[symmetric])
          by(simp add: converse_def del: acyclic_converse)
      next
        fix x
        assume "∀y. (y, x) ∈ {(D, C). P \<turnstile> C \<prec>1 D} --> Q (P, y)"
        thus "Q (P, x)"
          by(auto intro: wf'')
      qed
    qed
  qed
next
  fix P C
  assume "acyclicP (subcls1 P) ∧ is_class P C ∧ C ≠ Object"
  then obtain ac: "acyclicP (subcls1 P)"
    and ic: "is_class P C"
    and CObj: "C ≠ Object" by blast
  from ic CObj have "P \<turnstile> C \<prec>1 fst (the (class P C))"
    by(auto simp add: is_class_def intro: subcls1I)
  with ac show "((P, fst (the (class P C))), P, C) ∈ {((P, C), P', C'). P = P' ∧ acyclicP (subcls1 P) ∧ P \<turnstile> C' \<prec>1 C}"
    by(simp)
qed

fun wf_measure_widen1 :: "'a prog => ty => nat" where
  "wf_measure_widen1 P (Class C) = class_numbering P C"
| "wf_measure_widen1 P (Array T) = length P + wf_measure_widen1 P T"
| "wf_measure_widen1 P T = 0"

lemma wf_converse_widen1:
  assumes wfP: "wf_prog wfmc P"
  shows "wf ((widen1 P)^-1)"
proof(rule wf_subset)
  show "wf (measure (wf_measure_widen1 P))"
    by auto
next
  from wfP have lengthP: "length P > 0"
    by(auto simp add: wf_prog_def wf_syscls_def)
  { fix x y
    have "P \<turnstile> x <1 y ==> wf_measure_widen1 P y < wf_measure_widen1 P x"
    proof(induct rule: widen1.induct)
      case (widen1_Class C D)
      note PCD = `P \<turnstile> C \<prec>1 D`
      from wfP have "acyclicP (subcls1 P)"
        by(rule acyclic_subcls1)
      moreover from PCD have "is_class P C" "C ≠ Object"
        by(auto elim: subcls1.cases simp: is_class_def)
      moreover from PCD obtain rest
        where "class P C = ⌊(D, rest)⌋"
        by(auto elim!: subcls1.cases)
      ultimately show ?case 
        by(simp del: class_numbering.simps add: class_numbering.simps[where C=C])
    qed(insert lengthP, simp_all) }
  thus "(widen1 P)¯ ⊆ measure (wf_measure_widen1 P)" by auto
qed

fun super :: "'a prog => ty => ty"
where
  "super P (Array Integer) = Class Object"
| "super P (Array Boolean) = Class Object"
| "super P (Array Void) = Class Object"
| "super P (Array (Class C)) = (if C = Object then Class Object else Array (super P (Class C)))"
| "super P (Array NT) = Class Object"
| "super P (Array (Array T)) = (if is_NT_Array T then Class Object else Array (super P (Array T)))"
| "super P (Class C) = Class (fst (the (class P C)))"

lemma superI:
  "P \<turnstile> T <1 U ==> super P T = U"
proof(induct rule: widen1.induct)
  case (widen1_Array_Array T U)
  thus ?case by(cases T, auto elim: widen1.cases)
next
  case (widen1_NT_Object T)
  thus ?case by(cases T, auto)
qed(auto dest: subcls1D)

lemma super_widen1:
  assumes icO: "is_class P Object"
  shows "P \<turnstile> T <1 U <-> is_type P T ∧ (case T of Class C  => (C ≠ Object ∧ U = super P T) 
                                              | Array T' => U = super P T 
                                              | _        => False)"
proof(induct T arbitrary: U)
  case (Class C' U')
  have "P \<turnstile> Class C' <1 U' <-> is_class P C' ∧ C' ≠ Object ∧ U' = super P (Class C')"
  proof(rule iffI)
    assume wd: "P \<turnstile> Class C' <1 U'"
    hence "is_type P (Class C')"
      by(auto elim!: widen1.cases intro: subcls_is_class)
    moreover from wd have "C' ≠ Object" by(auto)
    moreover from wd have "super P (Class C') = U'"
      by(rule superI)
    ultimately show "is_class P C' ∧ C' ≠ Object ∧ U' = super P (Class C')"
      by simp
  next
    assume "is_class P C' ∧ C' ≠ Object ∧ U' = super P (Class C')"
    then obtain "is_class P C'" "C' ≠ Object" "U' = super P (Class C')" by blast
    from `U' = super P (Class C')` obtain D where "U' = Class D" by(auto)
    moreover with `is_class P C'` `U' = super P (Class C')` `C' ≠ Object`
    have "P \<turnstile> C' \<prec>1 D" by(auto simp add: is_class_def intro!: subcls1.intros)
    hence "P \<turnstile> Class C' <1 Class D" by(rule widen1_Class)
    ultimately show "P \<turnstile> Class C' <1 U'" by simp
  qed
  thus ?case by simp
next
  case (Array T' U')
  have "P \<turnstile> T'⌊⌉ <1 U' = (is_type P T' ∧ U' = super P (T'⌊⌉))"
  proof(rule iffI)
    assume wd: "P \<turnstile> T'⌊⌉ <1 U'"
    hence "is_type P T'" using icO
      by(auto dest: is_type_widen1)
    moreover from wd have "super P (T'⌊⌉) = U'" by(rule superI)
    ultimately show "is_type P T' ∧ U' = super P (T'⌊⌉)" by simp
  next
    assume "is_type P T' ∧ U' = super P (T'⌊⌉)"
    then obtain "is_type P T'"
      and U': "U' = super P (T'⌊⌉)" by blast
    from U' show "P \<turnstile> T'⌊⌉ <1 U'"
    proof(cases T')
      case (Class D)
      show ?thesis
      proof(cases "D = Object")
        case True
        with Class U' icO
        show ?thesis by(auto intro: widen1_Array_Object)
      next
        case False
        with Class U' obtain D' where "U' = (Class D')⌊⌉" by auto
        with U' Class False `is_type P T'` have "P \<turnstile> D \<prec>1 D'"
          by(auto simp add: is_class_def intro: subcls1.intros)
        hence "P \<turnstile> Class D <1 Class D'" by(rule widen1_Class)
        with `U' = (Class D')⌊⌉` Class show ?thesis
          by(auto intro: widen1_Array_Array)
      qed
    next
      case (Array V)
      show ?thesis
      proof(cases "is_NT_Array V")
        case True
        with Array U' have "U' = Class Object" by(simp)
        with True Array show ?thesis by(auto intro: widen1_NT_Object)
      next
        case False
        with Array U' obtain V' where "U' = V'⌊⌉" by(auto)
        with Array `is_type P T'` U' False 
        have "P \<turnstile> T' <1 V'"
          unfolding `!!U. P \<turnstile> T' <1 U = (is_type P T' ∧ (case T' of Class C => C ≠ Object ∧ U = super P T' | T⌊⌉ => U = super P T' | _ => False))`
          by(simp)
        with `U' = V'⌊⌉` False Array show ?thesis 
          by(auto intro: widen1_Array_Array)
      qed
    qed(auto intro: widen1.intros)
  qed    
  thus ?case by(simp)
qed(simp_all)


definition sup :: "'c prog => ty => ty => ty err" where
  "sup P T U ≡
   if is_refT T ∧ is_refT U
   then OK (if U = NT then T
            else if T = NT then U
            else exec_lub (widen1 P) (super P) T U)
   else if (T = U) then OK T else Err"

constdefs
  esl :: "'c prog => ty esl"
  "esl P ≡ (is_type P, widen P, sup P)"



lemma order_widen [intro,simp]: 
  "wf_prog m P ==> order (widen P)"
unfolding Semilat.order_def lesub_def
by (auto intro: widen_trans widen_antisym)



lemma subcls1_trancl_widen1_trancl:
  "(subcls1 P)^++ C D ==> (Class C, Class D) ∈ (widen1 P)^+"
proof(induct rule: tranclp_induct[consumes 1, case_names base step])
  case base thus ?case
    by -(rule r_into_trancl, rule widen1.intros)
next
  case (step D E)
  from `P \<turnstile> D \<prec>1 E` have "(Class D, Class E) ∈ widen1 P"
    by(rule widen1.intros)
  with `(Class C, Class D) ∈ (widen1 P)+` show ?case
    by(rule trancl_into_trancl)
qed

lemma subcls_into_widen1_rtrancl:
  "P \<turnstile> C \<preceq>* D ==> (Class C, Class D) ∈ (widen1 P)*"
by(induct rule: rtranclp.induct)(auto intro: rtrancl_refl widen1_Class elim: rtrancl_into_rtrancl)

lemma not_widen1_NT_Array:
  "[| P \<turnstile> U <1 T; is_NT_Array T |] ==> False"
by(induct rule: widen1.induct)(auto)

lemma not_widen1_trancl_NT_Array:
  "[| (U, T) ∈ (widen1 P)^+; is_NT_Array T |] ==> False"
by(induct rule: trancl.induct)(auto intro: not_widen1_NT_Array)

lemma widen1_trancl_into_Array_widen1_trancl:
  "[| (A, B) ∈ (widen1 P)+; ¬ is_NT_Array A |] ==> (A⌊⌉, B⌊⌉) ∈ (widen1 P)+"
apply(induct rule: trancl.induct)
 apply(rule r_into_trancl)
 apply(erule widen1_Array_Array, assumption)
apply(clarsimp)
apply(case_tac "is_NT_Array b")
 apply(fastsimp dest: not_widen1_trancl_NT_Array)
apply(auto dest: widen1_Array_Array)
done

lemma widen1_rtrancl_into_Array_widen1_rtrancl:
  "[| (A, B) ∈ (widen1 P)*; ¬ is_NT_Array A |] ==> (A⌊⌉, B⌊⌉) ∈ (widen1 P)*"
apply(erule rtranclE)
 apply(simp)
apply(rule trancl_into_rtrancl)
apply(rule widen1_trancl_into_Array_widen1_trancl)
by(rule rtrancl_into_trancl1)

lemma Array_Object_widen1_trancl:
  assumes wf: "wf_prog wmdc P"
  and itA: "is_type P A"
  shows "(A⌊⌉, Class Object) ∈ (widen1 P)+"
proof(cases "is_NT_Array A")
  case True thus ?thesis
    by(auto intro: r_into_trancl widen1_NT_Object)
next
  case False
  show ?thesis using itA False
  proof(induct A)
    case (Class C)
    from `is_type P (Class C)`
    have "is_class P C" by simp
    hence "P \<turnstile> C \<preceq>* Object"
      by(rule subcls_C_Object[OF _ wf])
    hence "(Class C, Class Object) ∈ (widen1 P)*"
      by(rule subcls_into_widen1_rtrancl)
    hence "(Class C⌊⌉, Class Object⌊⌉) ∈ (widen1 P)*"
      by(auto intro: widen1_rtrancl_into_Array_widen1_rtrancl)
    with widen1_Array_Object[where P=P] is_class_Object[OF wf] 
    show ?case by(blast intro: rtrancl_into_trancl1)
  next
    case (Array A)
    note IH = `[| is_type P A; ¬ is_NT_Array A |] ==> (A⌊⌉, Class Object) ∈ (widen1 P)+`
    from `is_type P (A⌊⌉)` `¬ is_NT_Array (A⌊⌉)`
    have "(A⌊⌉, Class Object) ∈ (widen1 P)+"
      by(auto intro: IH)
    hence "(A⌊⌉, Class Object) ∈ (widen1 P)*"
      by(rule trancl_into_rtrancl)
    hence "(A⌊⌉⌊⌉, Class Object⌊⌉) ∈ (widen1 P)*" using `¬ is_NT_Array (A⌊⌉)`
      by(rule widen1_rtrancl_into_Array_widen1_rtrancl)
    with widen1_Array_Object[where P=P] is_class_Object[OF wf]
    show ?case by (blast intro: rtrancl_into_trancl1)
  qed(auto intro: widen1.intros)
qed

lemma widen_into_widen1_trancl:
  assumes wf: "wf_prog wfmd P"
  shows "[| P \<turnstile> A ≤ B; A ≠ B; A ≠ NT |] ==> (A, B) ∈ (widen1 P)^+"
proof(induct rule: widen.induct)
  case (widen_subcls C D)
  from `Class C ≠ Class D` `P \<turnstile> C \<preceq>* D`
  have "(subcls1 P)++ C D"
    by(auto elim: rtranclp.cases intro: rtranclp_into_tranclp1)
  thus ?case
    by(rule subcls1_trancl_widen1_trancl)
next
  case (widen_array_object A)
  thus ?case
    by - (rule Array_Object_widen1_trancl[OF wf])
next
  case (widen_array_array A B)
  hence "(A, B) ∈ (widen1 P)+" by(cases A, auto)
  with `¬ is_NT_Array A` show "(A⌊⌉, B⌊⌉) ∈ (widen1 P)+"
    by -(rule widen1_trancl_into_Array_widen1_trancl)
qed(fastsimp)+


lemma wf_prog_impl_acc_widen:
  assumes wfP: "wf_prog wfmd P"
  shows "acc (widen P)"
proof -
  from wf_converse_widen1[OF wfP]
  have "wf (((widen1 P)^-1)^+)"
    by(rule wf_trancl)
  hence wfw1t: "!!M T. T ∈ M ==> (∃z∈M. ∀y. (y, z) ∈ ((widen1 P)¯)+ --> y ∉ M)"
    by(auto simp only: wf_eq_minimal)
  { fix M T
    assume TM: "(T :: ty) ∈ M"
    have "∃z∈M. ∀y. (y, z) ∈ {(y, T). widen P T y ∧ T ≠ y} --> y ∉ M"
    proof(cases "(∃C. Class C ∈ M) ∨ (∃U. U⌊⌉ ∈ M)")
      case False
      thus ?thesis
        by -(rule bexI[OF _ TM], cases T, auto simp: NT_widen Class_widen2 dest: Array_widen)
    next
      case True
      have BNTthesis: "!!B. B ∈ M - {NT} ==> ?thesis"
      proof -
        fix B
        assume BM: "B ∈ M - {NT}"
        from wfw1t[OF BM] obtain z
          where zM: "z ∈ M"
          and znnt: "z ≠ NT"
          and y: "!!y. (y, z) ∈ ((widen1 P)¯)+ ==> y ∉ M - {NT}" by blast
        show "?thesis B"
        proof(rule bexI[OF _ zM], rule allI, rule impI)
          fix y
          assume "(y, z) ∈ {(y, T). widen P T y ∧ T ≠ y}"
          hence Pzy: "P \<turnstile> z ≤ y" and zy: "z ≠ y" by auto
          hence "(z, y) ∈ (widen1 P)^+" using znnt
            by(rule widen_into_widen1_trancl[OF wfP])
          hence ynM: "y ∉ M - {NT}"
            by -(rule y, simp add: trancl_converse)
          with Pzy znnt show "y ∉ M" by(auto)
        qed
      qed
      from True show ?thesis
        by -(erule disjE, (erule exE, rule BNTthesis, fastsimp)+)
    qed }
  hence "wf {(y, x). widen P x y ∧ x ≠ y}"
    by(clarsimp simp only: wf_eq_minimal)
  thus ?thesis
    by(unfold Semilat.acc_def lesssub_def lesub_def)
qed


lemmas wf_widen_acc = wf_prog_impl_acc_widen
declare wf_widen_acc [intro, simp]

lemma acyclic_widen1:
  "wf_prog wfmc P ==> acyclic (widen1 P)"
by(auto dest: wf_converse_widen1 wf_acyclic simp add: acyclic_converse)


lemma widen1_into_widen:
  assumes wf: "wf_prog wf_mb P"
  shows "(A, B) ∈ widen1 P ==> P \<turnstile> A ≤ B"
apply(induct rule: widen1.induct)
apply(insert is_class_Object[OF wf])
apply(auto intro: widen.intros NT_Array_is_type elim: widen1.cases)
done

lemma widen1_rtrancl_into_widen:
  assumes wf: "wf_prog wf_mb P"
  shows "(A, B) ∈ (widen1 P)^* ==> P \<turnstile> A ≤ B"
apply(induct rule: rtrancl_induct)
apply(insert wf)
by(auto dest!: widen1_into_widen elim: widen_trans)

lemma widen_eq_widen1_trancl:
  "[| wf_prog wf_md P; T ≠ NT; T ≠ U |] ==> P \<turnstile> T ≤ U <-> P \<turnstile> T <+ U"
apply(rule iffI)
 apply(rule widen_into_widen1_trancl, assumption+)
apply(erule widen1_rtrancl_into_widen)
by(rule trancl_into_rtrancl)

lemma closed_err_types:
  assumes wfP: "wf_prog wf_mb P"
  shows "closed (err (is_type P)) (lift2 (sup P))"
proof -
  { fix A B
    assume itA: "is_type P A"
      and itB: "is_type P B"
      and ANT: "A ≠ NT"
      and BNT: "B ≠ NT"
      and AnB: "A ≠ B"
      and RTA: "is_refT A"
      and RTB: "is_refT B"
    hence AObject: "P \<turnstile> A ≤ Class Object"
      and BObject: "P \<turnstile> B ≤ Class Object"
      by(auto intro: is_refType_widen_Object[OF wfP])
    have "is_type P (exec_lub (widen1 P) (super P) A B)"
    proof(cases "A = Class Object ∨ B = Class Object")
      case True
      hence "exec_lub (widen1 P) (super P) A B = Class Object"
      proof(rule disjE)
        assume A: "A = Class Object"
        moreover
        from BObject BNT
        have "(B, Class Object) ∈ (widen1 P)*"
          by(cases "B = Class Object", auto intro: trancl_into_rtrancl widen_into_widen1_trancl[OF wfP])
        hence "is_ub ((widen1 P)*) (Class Object) B (Class Object)"
          by(auto intro: is_ubI)
        hence "is_lub ((widen1 P)*) (Class Object) B (Class Object)"
          by(auto simp add: is_lub_def dest: is_ubD)
        with acyclic_widen1[OF wfP]
        have "exec_lub (widen1 P) (super P) (Class Object) B = Class Object"
          by(auto intro: exec_lub_conv superI)
        ultimately show "exec_lub (widen1 P) (super P) A B = Class Object" by simp
      next
        assume B: "B = Class Object"
        moreover
        from AObject ANT
        have "(A, Class Object) ∈ (widen1 P)*"
          by(cases "A = Class Object", auto intro: trancl_into_rtrancl widen_into_widen1_trancl[OF wfP])
        hence "is_ub ((widen1 P)*) (Class Object) A (Class Object)"
          by(auto intro: is_ubI)
        hence "is_lub ((widen1 P)*) (Class Object) A (Class Object)"
          by(auto simp add: is_lub_def dest: is_ubD)
        with acyclic_widen1[OF wfP]
        have "exec_lub (widen1 P) (super P) A (Class Object) = Class Object"
          by(auto intro: exec_lub_conv superI)
        ultimately show "exec_lub (widen1 P) (super P) A B = Class Object" by simp
      qed
      with wfP show ?thesis by(simp)
    next
      case False
      hence AnObject: "A ≠ Class Object"
        and BnObject: "B ≠ Class Object" by auto
      from widen_into_widen1_trancl[OF wfP AObject AnObject ANT]
      have "(A, Class Object) ∈ (widen1 P)*"
        by(rule trancl_into_rtrancl)
      moreover from widen_into_widen1_trancl[OF wfP BObject BnObject BNT]
      have "(B, Class Object) ∈ (widen1 P)*"
        by(rule trancl_into_rtrancl)
      ultimately have "is_lub ((widen1 P)*) A B (exec_lub (widen1 P) (super P) A B)"
        apply(rule is_lub_exec_lub[OF single_valued_widen1[OF wfP] acyclic_widen1[OF wfP]])
        by(auto intro: superI)
      hence Aew1: "(A, exec_lub (widen1 P) (super P) A B) ∈ (widen1 P)*"
        by(auto simp add: is_lub_def dest!: is_ubD)
      thus ?thesis
      proof(rule rtranclE)
        assume "A = exec_lub (widen1 P) (super P) A B"
        with itA show ?thesis by simp
      next
        fix A'
        assume "P \<turnstile> A' <1 exec_lub (widen1 P) (super P) A B"
        thus ?thesis by(rule widen1_is_type[OF wfP])
      qed
    qed }
  with is_class_Object[OF wfP] show ?thesis
    unfolding closed_def plussub_def lift2_def sup_def
    by(auto split: err.split ty.splits)(auto simp add: mem_def exec_lub_refl)
qed

lemma widen_into_widen1_rtrancl:
  "[|wf_prog wfmd P; widen P A B; A ≠ NT|] ==> (A, B) ∈ (widen1 P)*"
apply(cases "A = B", auto intro: trancl_into_rtrancl widen_into_widen1_trancl)
done


lemma sup_widen_greater:
  assumes wfP: "wf_prog wf_mb P"
  and it1: "is_type P t1"
  and it2: "is_type P t2"
  and sup: "sup P t1 t2 = OK s"
  shows "widen P t1 s ∧ widen P t2 s"
proof -
  have "[| is_refT t1; is_refT t2; t1 ≠ NT; t2 ≠ NT |]
    ==> P \<turnstile> t1 ≤ exec_lub (widen1 P) (super P) t1 t2
     ∧ P \<turnstile> t2 ≤ exec_lub (widen1 P) (super P) t1 t2"
  proof -
    assume t1: "is_refT t1"
      and t2: "is_refT t2"
      and t1NT: "t1 ≠ NT"
      and t2NT: "t2 ≠ NT"
    with it1 it2 wfP have "P \<turnstile> t1 ≤ Class Object" "P \<turnstile> t2 ≤ Class Object"
      by(auto intro: is_refType_widen_Object)
    with t1NT t2NT have "(t1, Class Object) ∈ (widen1 P)^*" "(t2, Class Object) ∈ (widen1 P)^*"
      by(auto intro: widen_into_widen1_rtrancl[OF wfP])
    with single_valued_widen1[OF wfP]
    obtain u where
      "is_lub ((widen1 P)^* ) t1 t2 u" 
      by (blast dest: single_valued_has_lubs)
    moreover
    note acyclic_widen1[OF wfP]
    moreover
    have "∀x y. (x, y) ∈ widen1 P --> super P x = y"
      by (blast intro: superI)
    ultimately
    show "P \<turnstile> t1 ≤ exec_lub (widen1 P) (super P) t1 t2 ∧
          P \<turnstile> t2 ≤ exec_lub (widen1 P) (super P) t1 t2"
      by (simp add: exec_lub_conv) (blast dest: is_lubD is_ubD intro: widen1_rtrancl_into_widen[OF wfP])
  qed
  with it1 it2 sup show ?thesis
    by(cases s, auto simp add: sup_def split: split_if_asm elim: refTE)
qed

lemma sup_widen_smallest:
  assumes wfP: "wf_prog wf_mb P"
  and itT: "is_type P T"
  and itU: "is_type P U"
  and itV: "is_type P V"
  and TwV: "P \<turnstile> T ≤ V"
  and UwV: "P \<turnstile> U ≤ V"
  and sup: "sup P T U = OK W"
  shows "widen P W V"
proof -
  { assume rT: "is_refT T"
      and rU: "is_refT U"
      and UNT: "U ≠ NT"
      and TNT: "T ≠ NT"
      and W: "exec_lub (widen1 P) (super P) T U = W"
    from itU itT rT rU UNT TNT have "P \<turnstile> T ≤ Class Object" "P \<turnstile> U ≤ Class Object"
      by(auto intro:is_refType_widen_Object[OF wfP])
    with UNT TNT have "(T, Class Object) ∈ (widen1 P)^*" "(U, Class Object) ∈ (widen1 P)^*"
      by(auto intro: widen_into_widen1_rtrancl[OF wfP])
    with single_valued_widen1[OF wfP]
    obtain X where
      lub: "is_lub ((widen1 P)^* ) T U X"
      by (blast dest: single_valued_has_lubs)   
    with acyclic_widen1[OF wfP]
    have "exec_lub (widen1 P) (super P) T U = X"
      by (blast intro: superI exec_lub_conv)
    moreover
    from TwV TNT UwV UNT have "(T, V) ∈ (widen1 P)^*" "(U, V) ∈ (widen1 P)^*"
      by(auto intro: widen_into_widen1_rtrancl[OF wfP])
    with lub have "(X, V) ∈ (widen1 P)^*" 
      by (clarsimp simp add: is_lub_def is_ub_def)
    ultimately
    have "(exec_lub (widen1 P) (super P) T U, V) ∈ (widen1 P)^*"
      by blast
    hence "P \<turnstile> exec_lub (widen1 P) (super P) T U ≤ V"
      by(rule widen1_rtrancl_into_widen[OF wfP])
    with W have "P \<turnstile> W ≤ V" by simp }
  with sup itT itU itV TwV UwV show ?thesis
    by(simp add: sup_def split: split_if_asm)
qed

lemma sup_exists:
  "[| widen P a c; widen P b c |] ==> EX T. sup P a b = OK T"
(*<*)
apply (unfold sup_def)
apply (cases b)
apply auto
apply (cases a)
apply auto
apply (cases a)
apply auto
apply(cases a)
apply(auto)
done
(*>*)

lemma err_semilat_JType_esl:
  "wf_prog wf_mb P ==> err_semilat (esl P)"
proof -
  assume wf_prog: "wf_prog wf_mb P"  
  hence "order (widen P)"..
  moreover from wf_prog
  have "closed (err (is_type P)) (lift2 (sup P))"
    by (rule closed_err_types)
  moreover
  from wf_prog have
    "(∀x∈err (is_type P). ∀y∈err (is_type P). x \<sqsubseteq>Err.le (widen P) x \<squnion>lift2 (sup P) y) ∧ 
     (∀x∈err (is_type P). ∀y∈err (is_type P). y \<sqsubseteq>Err.le (widen P) x \<squnion>lift2 (sup P) y)"
    by(auto simp add: lesub_def plussub_def Err.le_def lift2_def sup_widen_greater mem_def split: err.split)
  moreover from wf_prog have
    "∀x∈err (is_type P). ∀y∈err (is_type P). ∀z∈err (is_type P). 
    x \<sqsubseteq>Err.le (widen P) z ∧ y \<sqsubseteq>Err.le (widen P) z --> x \<squnion>lift2 (sup P) y \<sqsubseteq>Err.le (widen P) z"
    by (unfold lift2_def plussub_def lesub_def Err.le_def)
       (auto intro: sup_widen_smallest dest:sup_exists simp add: mem_def split: err.split)
  ultimately show ?thesis by (simp add: esl_def semilat_def sl_def Err.sl_def)
qed

end