Theory JinjaDCI.SemiType

(*  Title:      Jinja/BV/SemiType.thy

    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM
*)

section ‹ The Jinja Type System as a Semilattice ›

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

definition super :: "'a prog ⇒ cname ⇒ cname"
where "super P C ≡ fst (the (class P C))"

lemma superI:
  "(C,D) ∈ subcls1 P ⟹ super P C = D"
  by (unfold super_def) (auto dest: subcls1D)


primrec the_Class :: "ty ⇒ cname"
where
  "the_Class (Class C) = C"

definition sup :: "'c prog ⇒ ty ⇒ ty ⇒ ty err"
where
  "sup P T⇩1 T⇩2 ≡
  if is_refT T⇩1 ∧ is_refT T⇩2 then 
  OK (if T⇩1 = NT then T⇩2 else
      if T⇩2 = NT then T⇩1 else
      (Class (exec_lub (subcls1 P) (super P) (the_Class T⇩1) (the_Class T⇩2))))
  else 
  (if T⇩1 = T⇩2 then OK T⇩1 else Err)"

lemma sup_def':
  "sup P = (λT⇩1 T⇩2.
  if is_refT T⇩1 ∧ is_refT T⇩2 then 
  OK (if T⇩1 = NT then T⇩2 else
      if T⇩2 = NT then T⇩1 else
      (Class (exec_lub (subcls1 P) (super P) (the_Class T⇩1) (the_Class T⇩2))))
  else 
  (if T⇩1 = T⇩2 then OK T⇩1 else Err))"
  by (simp add: sup_def fun_eq_iff)

abbreviation
  subtype :: "'c prog ⇒ ty ⇒ ty ⇒ bool"
  where "subtype P ≡ widen P"

definition esl :: "'c prog ⇒ ty esl"
where
  "esl P ≡ (types P, subtype P, sup P)"


(* FIXME: move to wellform *)
lemma is_class_is_subcls:
  "wf_prog m P ⟹ is_class P C = P ⊢ C ≼⇧* Object"
(*<*)by (fastforce simp:is_class_def
                  elim: subcls_C_Object converse_rtranclE subcls1I
                  dest: subcls1D)
(*>*)


(* FIXME: move to wellform *)
lemma subcls_antisym:
  "⟦wf_prog m P; P ⊢ C ≼⇧* D; P ⊢ D ≼⇧* C⟧ ⟹ C = D"
  (*<*) by (auto dest: acyclic_subcls1 acyclic_impl_antisym_rtrancl antisymD) (*>*)

(* FIXME: move to wellform *)
lemma widen_antisym:
  "⟦ wf_prog m P; P ⊢ T ≤ U; P ⊢ U ≤ T ⟧ ⟹ T = U"
(*<*)
apply (cases T)
 apply (cases U)
 apply auto
apply (cases U)
 apply (auto elim!: subcls_antisym)
done
(*>*)

lemma order_widen [intro,simp]: 
  "wf_prog m P ⟹ order (subtype P)  (types P)"
(*<*)
  apply (unfold Semilat.order_def lesub_def)
  apply (auto intro: widen_trans widen_antisym)
  done
(*>*)

(* FIXME: move to TypeRel *)
lemma NT_widen:
  "P ⊢ NT ≤ T = (T = NT ∨ (∃C. T = Class C))"
(*<*) by (cases T) auto (*>*)

(* FIXME: move to TypeRel *)
lemma Class_widen2: "P ⊢ Class C ≤ T = (∃D. T = Class D ∧ P ⊢ C ≼⇧* D)"
(*<*) by (cases T) auto (*>*)
 
lemma wf_converse_subcls1_impl_acc_subtype:
  "wf ((subcls1 P)^-1) ⟹ acc (subtype P)"
(*<*)
apply (unfold Semilat.acc_def lesssub_def)
apply (drule_tac p = "(subcls1 P)^-1 - Id" in wf_subset)
 apply blast
apply (drule wf_trancl)
apply (simp add: wf_eq_minimal)
apply clarify
apply (unfold lesub_def)
apply (rename_tac M T) 
apply (case_tac "∃C. Class C ∈ M")
 prefer 2
 apply (case_tac T)
     apply fastforce
    apply fastforce
   apply fastforce
  apply simp
  apply (rule_tac x = NT in bexI)
   apply (rule allI)
   apply (rule impI, erule conjE) 
   apply (clarsimp simp add: NT_widen)
  apply simp
 apply clarsimp
apply (erule_tac x = "{C. Class C : M}" in allE)
apply auto
apply (rename_tac D)
apply (rule_tac x = "Class D" in bexI)
 prefer 2
 apply assumption
apply clarify
apply (clarsimp simp: Class_widen2)
apply (insert rtrancl_r_diff_Id [symmetric, of "subcls1 P"])
apply simp
apply (erule rtranclE)
 apply blast
apply (drule rtrancl_converseI)
apply (subgoal_tac "((subcls1 P)-Id)^-1 = ((subcls1 P)^-1 - Id)")
 prefer 2
 apply blast
apply simp
apply (blast intro: rtrancl_into_trancl2)
done
(*>*)

lemma wf_subtype_acc [intro, simp]:
  "wf_prog wf_mb P ⟹ acc (subtype P)"
(*<*) by (rule wf_converse_subcls1_impl_acc_subtype, rule wf_subcls1) (*>*)

lemma exec_lub_refl [simp]: "exec_lub r f T T = T"
(*<*) by (simp add: exec_lub_def while_unfold) (*>*)

lemma closed_err_types:
  "wf_prog wf_mb P ⟹ closed (err (types P)) (lift2 (sup P))"
(*<*)
  apply (unfold closed_def plussub_def lift2_def sup_def')
  apply (frule acyclic_subcls1)
  apply (frule single_valued_subcls1)
  apply (auto simp: is_type_def is_refT_def is_class_is_subcls split: err.split ty.splits)
  apply (blast dest!: is_lub_exec_lub is_lubD is_ubD intro!: is_ubI superI)
  done
(*>*)


lemma sup_subtype_greater:
  "⟦ wf_prog wf_mb P; is_type P t1; is_type P t2; sup P t1 t2 = OK s ⟧ 
  ⟹ subtype P t1 s ∧ subtype P t2 s"
(*<*)
proof -
  assume wf_prog: "wf_prog wf_mb P"
 
  { fix c1 c2
    assume is_class: "is_class P c1" "is_class P c2"
    with wf_prog 
    obtain 
      "P ⊢ c1 ≼⇧* Object"
      "P ⊢ c2 ≼⇧* Object"
      by (blast intro: subcls_C_Object)
    with single_valued_subcls1[OF wf_prog]
    obtain u where
      "is_lub ((subcls1 P)^* ) c1 c2 u"      
      by (blast dest: single_valued_has_lubs)
    moreover
    note acyclic_subcls1[OF wf_prog]
    moreover
    have "∀x y. (x, y) ∈ subcls1 P ⟶ super P x = y"
      by (blast intro: superI)
    ultimately
    have "P ⊢ c1 ≼⇧* exec_lub (subcls1 P) (super P) c1 c2 ∧
          P ⊢ c2 ≼⇧* exec_lub (subcls1 P) (super P) c1 c2"
      by (simp add: exec_lub_conv) (blast dest: is_lubD is_ubD)
  } note this [simp]

  assume "is_type P t1" "is_type P t2" "sup P t1 t2 = OK s"
  thus ?thesis
    apply (unfold sup_def) 
    apply (cases s)
    apply (auto simp add: is_refT_def split: if_split_asm)
    done
qed
(*>*)

lemma sup_subtype_smallest:
  "⟦ wf_prog wf_mb P; is_type P a; is_type P b; is_type P c; 
      subtype P a c; subtype P b c; sup P a b = OK d ⟧
  ⟹ subtype P d c"
(*<*)
proof -
  assume wf_prog: "wf_prog wf_mb P"

  { fix c1 c2 D
    assume is_class: "is_class P c1" "is_class P c2"
    assume le: "P ⊢ c1 ≼⇧* D" "P ⊢ c2 ≼⇧* D"
    from wf_prog is_class
    obtain 
      "P ⊢ c1 ≼⇧* Object"
      "P ⊢ c2 ≼⇧* Object"
      by (blast intro: subcls_C_Object)
    with single_valued_subcls1[OF wf_prog]
    obtain u where
      lub: "is_lub ((subcls1 P)^* ) c1 c2 u"
      by (blast dest: single_valued_has_lubs)   
    with acyclic_subcls1[OF wf_prog]
    have "exec_lub (subcls1 P) (super P) c1 c2 = u"
      by (blast intro: superI exec_lub_conv)
    moreover
    from lub le
    have "P ⊢ u ≼⇧* D" 
      by (simp add: is_lub_def is_ub_def)
    ultimately     
    have "P ⊢ exec_lub (subcls1 P) (super P) c1 c2 ≼⇧* D"
      by blast
  } note this [intro]

  have [dest!]:
    "⋀C T. P ⊢ Class C ≤ T ⟹ ∃D. T=Class D ∧ P ⊢ C ≼⇧* D"
    by (frule Class_widen, auto)

  assume "is_type P a" "is_type P b" "is_type P c"
         "subtype P a c" "subtype P b c" "sup P a b = OK d"
  thus ?thesis
    by (auto simp add: sup_def is_refT_def
             split: if_split_asm)
qed
(*>*)

lemma sup_exists:
  "⟦ subtype P a c; subtype P b c ⟧ ⟹ ∃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
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 (subtype P) (types P)"..
  moreover from wf_prog
  have "closed (err (types P)) (lift2 (sup P))"
    by (rule closed_err_types)
  moreover
  from wf_prog have
    "(∀x∈err (types P). ∀y∈err (types P). x ⊑⇘Err.le (subtype P)⇙ x ⊔⇘lift2 (sup P)⇙ y) ∧ 
     (∀x∈err (types P). ∀y∈err (types P). y ⊑⇘Err.le (subtype P)⇙ x ⊔⇘lift2 (sup P)⇙ y)"
    by (auto simp add: lesub_def plussub_def Err.le_def lift2_def sup_subtype_greater split: err.split)
  moreover from wf_prog have
    "∀x∈err (types P). ∀y∈err (types P). ∀z∈err (types P). 
    x ⊑⇘Err.le (subtype P)⇙ z ∧ y ⊑⇘Err.le (subtype P)⇙ z ⟶ x ⊔⇘lift2 (sup P)⇙ y ⊑⇘Err.le (subtype P)⇙ z"
    by (unfold lift2_def plussub_def lesub_def Err.le_def)
       (auto intro: sup_subtype_smallest dest:sup_exists split: err.split)
  ultimately show ?thesis by (simp add: esl_def semilat_def sl_def Err.sl_def)
qed
(*>*)


end