Theory TypeRel

(*  Title:      Jinja/Common/TypeRel.thy
    ID:         $Id: TypeRel.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

header {* \isaheader{Relations between Jinja Types} *}

theory TypeRel = Decl:

subsection{* The subclass relations *}

consts
  subcls1 :: "'m prog => (cname × cname) set"  -- "subclass"

(*<*)
syntax (xsymbols)
  subcls1 :: "'m prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>1 _" [71,71,71] 70)
  subcls  :: "'m prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>* _"  [71,71,71] 70)
(*>*)

translations
  "P \<turnstile> C  \<prec>1 D"  ==  "(C,D) ∈ subcls1 P"
  "P \<turnstile> C  \<preceq>*  D"  ==  "(C,D) ∈ (subcls1 P)*"
 (*<*)
  "¬ P \<turnstile> C  \<preceq>*  D" <= "(C,D) ∉ (subcls1 P)*"
(*>*)

inductive "subcls1 P"
intros subcls1I: "[|class P C = Some (D,rest); C ≠ Object|] ==> P \<turnstile> C \<prec>1 D"

lemma subcls1D: "P \<turnstile> C \<prec>1 D ==> C ≠ Object ∧ (∃fs ms. class P C = Some (D,fs,ms))"
(*<*)by(erule subcls1.induct)(fastsimp simp add:is_class_def)(*>*)

lemma [iff]: "¬ P \<turnstile> Object \<prec>1 C"
(*<*)by(fastsimp dest:subcls1D)(*>*)

lemma [iff]: "(P \<turnstile> Object \<preceq>* C) = (C = Object)"
(*<*)
apply(rule iffI)
 apply(erule converse_rtranclE)
  apply simp_all
done
(*>*)

lemma finite_subcls1: "finite (subcls1 P)"
(*<*)
apply(subgoal_tac "subcls1 P =
 (Σ C∈{C. is_class P C} . {D. C≠Object ∧ fst (the (class P C))=D})")
 prefer 2
 apply(fastsimp simp:is_class_def dest: subcls1D elim: subcls1I)
apply simp
apply(rule finite_SigmaI [OF finite_is_class])
apply(rule_tac B = "{fst (the (class P C))}" in finite_subset)
apply  auto
done
(*>*)
(*
lemma subcls_is_class: "(C,D) ∈ (subcls1 P)+ ==> is_class P C"
apply (unfold is_class_def)
apply(erule trancl_trans_induct)
apply (auto dest!: subcls1D)
done

lemma subcls_is_class: "P \<turnstile> C \<preceq>* D ==> is_class P D --> is_class P C"
apply (unfold is_class_def)
apply (erule rtrancl_induct)
apply  (drule_tac [2] subcls1D)
apply  auto
done
*)


subsection{* The subtype relations *}

consts
  widen   :: "'m prog => (ty × ty) set"  -- "widening"

(*<*)
syntax (xsymbols)
  widen   :: "'m prog => ty => ty => bool" ("_ \<turnstile> _ ≤ _"   [71,71,71] 70)
  widens  :: "'m prog => ty list => ty list => bool" ("_ \<turnstile> _ [≤] _" [71,71,71] 70)
(*>*)

translations
  "P \<turnstile> S ≤ T"  ==  "(S,T) ∈ widen P"
  "P \<turnstile> Ts [≤] Ts'"  ==  "list_all2 (fun_of (widen P)) Ts Ts'"

inductive "widen P"
intros
  widen_refl[iff]: "P \<turnstile> T ≤ T"
  widen_subcls: "P \<turnstile> C \<preceq>* D  ==>  P \<turnstile> Class C ≤ Class D"
  widen_null[iff]: "P \<turnstile> NT ≤ Class C"

lemma [iff]: "(P \<turnstile> T ≤ Void) = (T = Void)"
(*<*)by (auto elim: widen.elims)(*>*)

lemma [iff]: "(P \<turnstile> T ≤ Boolean) = (T = Boolean)"
(*<*)by (auto elim: widen.elims)(*>*)

lemma [iff]: "(P \<turnstile> T ≤ Integer) = (T = Integer)"
(*<*)by (auto elim: widen.elims)(*>*)

lemma [iff]: "(P \<turnstile> Void ≤ T) = (T = Void)"
(*<*)by (auto elim: widen.elims)(*>*)

lemma [iff]: "(P \<turnstile> Boolean ≤ T) = (T = Boolean)"
(*<*)by (auto elim: widen.elims)(*>*)

lemma [iff]: "(P \<turnstile> Integer ≤ T) = (T = Integer)"
(*<*)by (auto elim: widen.elims)(*>*)


lemma Class_widen: "P \<turnstile> Class C ≤ T  ==>  ∃D. T = Class D"
(*<*)
apply (ind_cases "P\<turnstile>S≤T")
apply auto
done
(*>*)

lemma [iff]: "(P \<turnstile> T ≤ NT) = (T = NT)"
(*<*)
apply(cases T)
apply(auto dest:Class_widen)
done
(*>*)

lemma Class_widen_Class [iff]: "(P \<turnstile> Class C ≤ Class D) = (P \<turnstile> C \<preceq>* D)"
(*<*)
apply (rule iffI)
apply (ind_cases " P \<turnstile> S ≤ T")
apply (auto elim: widen_subcls)
done
(*>*)

lemma widen_Class: "(P \<turnstile> T ≤ Class C) = (T = NT ∨ (∃D. T = Class D ∧ P \<turnstile> D \<preceq>* C))"
(*<*)by(induct T, auto)(*>*)


lemma widen_trans[trans]: "[|P \<turnstile> S ≤ U; P \<turnstile> U ≤ T|] ==> P \<turnstile> S ≤ T"
(*<*)
proof -
  assume "P\<turnstile>S ≤ U" thus "!!T. P \<turnstile> U ≤ T ==> P \<turnstile> S ≤ T"
  proof induct
    case (widen_refl T T') thus "P \<turnstile> T ≤ T'" .
  next
    case (widen_subcls C D T)
    then obtain E where "T = Class E" by (blast dest: Class_widen)
    with widen_subcls show "P \<turnstile> Class C ≤ T" by (auto elim: rtrancl_trans)
  next
    case (widen_null C RT)
    then obtain D where "RT = Class D" by (blast dest: Class_widen)
    thus "P \<turnstile> NT ≤ RT" by auto
  qed
qed
(*>*)

lemma widens_trans [trans]: "[|P \<turnstile> Ss [≤] Ts; P \<turnstile> Ts [≤] Us|] ==> P \<turnstile> Ss [≤] Us"
(*<*)by (rule rel_list_all2_trans, rule widen_trans)(*>*)


(*<*)
lemmas widens_refl [iff] = rel_list_all2_refl [OF widen_refl]
lemmas widens_Cons [iff] = rel_list_all2_Cons1 [of "widen P", standard]
(*>*)


subsection{* Method lookup *}

consts
  Methods :: "'m prog => (cname × (mname => (ty list × ty × 'm) × cname))set"

(*<*)
syntax
  "_sees_methods" :: "['m prog, cname, mname => (ty list × ty × 'm) × cname] => bool"
                    ("_ \<turnstile> _ sees'_methods _" [51,51,51] 50)
(*>*)

translations "P \<turnstile> C sees_methods Mm"  ==  "(C,Mm) ∈ Methods P"

inductive "Methods P"
intros
sees_methods_Object:
 "[| class P Object = Some(D,fs,ms); Mm = option_map (λm. (m,Object)) ˆ map_of ms |]
  ==> P \<turnstile> Object sees_methods Mm"
sees_methods_rec:
 "[| class P C = Some(D,fs,ms); C ≠ Object; P \<turnstile> D sees_methods Mm;
    Mm' = Mm ++ (option_map (λm. (m,C)) ˆ map_of ms) |]
  ==> P \<turnstile> C sees_methods Mm'";

lemma sees_methods_fun:
assumes 1: "P \<turnstile> C sees_methods Mm"
shows "!!Mm'. P \<turnstile> C sees_methods Mm' ==> Mm' = Mm"
 (*<*)
using 1
proof induct
  case (sees_methods_rec C D Dres Cres fs ms Cres')
  have class: "class P C = Some (D, fs, ms)"
   and notObj: "C ≠ Object" and Dmethods: "P \<turnstile> D sees_methods Dres"
   and IH: "!!Dres'. P \<turnstile> D sees_methods Dres' ==> Dres' = Dres"
   and Cres: "Cres = Dres ++ (option_map (λm. (m,C)) ˆ map_of ms)"
   and Cmethods': "P \<turnstile> C sees_methods Cres'" .
  from Cmethods' notObj class obtain Dres'
    where Dmethods': "P \<turnstile> D sees_methods Dres'"
     and Cres': "Cres' = Dres' ++ (option_map (λm. (m,C)) ˆ map_of ms)"
    by(auto elim: Methods.elims)
  from Cres Cres' IH[OF Dmethods'] show "Cres' = Cres" by simp
next
  case sees_methods_Object thus ?case by(auto elim: Methods.elims)
qed
(*>*)

lemma visible_methods_exist:
  "P \<turnstile> C sees_methods Mm ==> Mm M = Some(m,D) ==>
   (∃D' fs ms. class P D = Some(D',fs,ms) ∧ map_of ms M = Some m)"
 (*<*)by(induct rule:Methods.induct) auto(*>*)

lemma sees_methods_decl_above:
assumes Csees: "P \<turnstile> C sees_methods Mm"
shows "Mm M = Some(m,D) ==> P \<turnstile> C \<preceq>* D"
 (*<*)
using Csees
proof induct
  case sees_methods_Object thus ?case by auto
next
  case sees_methods_rec thus ?case
    by(fastsimp simp:option_map_def split:option.splits
                elim:converse_rtrancl_into_rtrancl[OF subcls1I])
qed
(*>*)

lemma sees_methods_idemp:
assumes Cmethods: "P \<turnstile> C sees_methods Mm"
shows "!!m D. Mm M = Some(m,D) ==>
              ∃Mm'. (P \<turnstile> D sees_methods Mm') ∧ Mm' M = Some(m,D)"
(*<*)
using Cmethods
proof induct
  case sees_methods_Object thus ?case
    by(fastsimp dest: Methods.sees_methods_Object)
next
  case sees_methods_rec thus ?case
    by(fastsimp split:option.splits dest: Methods.sees_methods_rec)
qed
(*>*)

(*FIXME something wrong with induct: need to attache [consumes 1]
directly to proof of thm, declare does not work. *)

lemma sees_methods_decl_mono:
assumes sub: "P \<turnstile> C' \<preceq>* C"
shows "P \<turnstile> C sees_methods Mm ==>
       ∃Mm' Mm2. P \<turnstile> C' sees_methods Mm' ∧ Mm' = Mm ++ Mm2 ∧
                 (∀M m D. Mm2 M = Some(m,D) --> P \<turnstile> D \<preceq>* C)"
(*<*)
      (is "_ ==> ∃Mm' Mm2. ?Q C' C Mm' Mm2")
using sub
proof (induct rule:converse_rtrancl_induct)
  assume "P \<turnstile> C sees_methods Mm"
  hence "?Q C C Mm empty" by simp
  thus "∃Mm' Mm2. ?Q C C Mm' Mm2" by blast
next
  fix C'' C'
  assume sub1: "P \<turnstile> C'' \<prec>1 C'" and sub: "P \<turnstile> C' \<preceq>* C"
  and IH: "P \<turnstile> C sees_methods Mm ==>
           ∃Mm' Mm2. P \<turnstile> C' sees_methods Mm' ∧
                Mm' = Mm ++ Mm2 ∧ (∀M m D. Mm2 M = Some(m,D) --> P \<turnstile> D \<preceq>* C)"
  and Csees: "P \<turnstile> C sees_methods Mm"
  from IH[OF Csees] obtain Mm' Mm2 where C'sees: "P \<turnstile> C' sees_methods Mm'"
    and Mm': "Mm' = Mm ++ Mm2"
    and subC:"∀M m D. Mm2 M = Some(m,D) --> P \<turnstile> D \<preceq>* C" by blast
  obtain fs ms where class: "class P C'' = Some(C',fs,ms)" "C'' ≠ Object"
    using subcls1D[OF sub1] by blast
  let ?Mm3 = "option_map (λm. (m,C'')) ˆ map_of ms"
  have "P \<turnstile> C'' sees_methods (Mm ++ Mm2) ++ ?Mm3"
    using sees_methods_rec[OF class C'sees refl] Mm' by simp
  hence "?Q C'' C ((Mm ++ Mm2) ++ ?Mm3) (Mm2++?Mm3)"
    using converse_rtrancl_into_rtrancl[OF sub1 sub]
    by simp (simp add:map_add_def subC split:option.split)
  thus "∃Mm' Mm2. ?Q C'' C Mm' Mm2" by blast
qed
(*>*)


constdefs
  Method :: "'m prog => cname => mname => ty list => ty => 'm => cname => bool"
            ("_ \<turnstile> _ sees _: _->_ = _ in _" [51,51,51,51,51,51,51] 50)
  "P \<turnstile> C sees M: Ts->T = m in D  ≡
  ∃Mm. P \<turnstile> C sees_methods Mm ∧ Mm M = Some((Ts,T,m),D)";

lemma sees_method_fun:
  "[|P \<turnstile> C sees M:TS->T = m in D; P \<turnstile> C sees M:TS'->T' = m' in D' |]
   ==> TS' = TS ∧ T' = T ∧ m' = m ∧ D' = D"
 (*<*)by(fastsimp dest: sees_methods_fun simp:Method_def)(*>*)

lemma sees_method_decl_above:
  "P \<turnstile> C sees M:Ts->T = m in D ==> P \<turnstile> C \<preceq>* D"
 (*<*)by(clarsimp simp:Method_def sees_methods_decl_above)(*>*)

lemma visible_method_exists:
  "P \<turnstile> C sees M:Ts->T = m in D ==>
  ∃D' fs ms. class P D = Some(D',fs,ms) ∧ map_of ms M = Some(Ts,T,m)"
(*<*)by(fastsimp simp:Method_def dest!: visible_methods_exist)(*>*)


lemma sees_method_idemp:
  "P \<turnstile> C sees M:Ts->T=m in D ==> P \<turnstile> D sees M:Ts->T=m in D"
 (*<*)by(fastsimp simp: Method_def intro:sees_methods_idemp)(*>*)

lemma sees_method_decl_mono:
  "[| P \<turnstile> C' \<preceq>* C; P \<turnstile> C sees M:Ts->T = m in D;
     P \<turnstile> C' sees M:Ts'->T' = m' in D' |] ==> P \<turnstile> D' \<preceq>* D"
 (*<*)
apply(frule sees_method_decl_above)
apply(unfold Method_def)
apply clarsimp
apply(drule (1) sees_methods_decl_mono)
apply clarsimp
apply(drule (1) sees_methods_fun)
apply clarsimp
apply(blast intro:rtrancl_trans)
done
(*>*)

lemma sees_method_is_class:
  "[| P \<turnstile> C sees M:Ts->T = m in D |] ==> is_class P C"
(*<*)by (auto simp add: is_class_def Method_def elim: Methods.induct)(*>*)


subsection{* Field lookup *}

consts
  Fields :: "'m prog => (cname × ((vname × cname) × ty) list)set"

(*<*)
syntax
  "_has_fields" :: "['m prog, cname, ((vname × cname) × ty) list] => bool"
                  ("_ \<turnstile> _ has'_fields _" [51,51,51] 50)
(*>*)

translations
  "P \<turnstile> C has_fields FDTs"  ==  "(C,FDTs) ∈ Fields P"

inductive "Fields P"
intros
has_fields_rec:
"[| class P C = Some(D,fs,ms); C ≠ Object; P \<turnstile> D has_fields FDTs;
   FDTs' = map (λ(F,T). ((F,C),T)) fs @ FDTs |]
 ==> P \<turnstile> C has_fields FDTs'"
has_fields_Object:
"[| class P Object = Some(D,fs,ms); FDTs = map (λ(F,T). ((F,Object),T)) fs |]
 ==> P \<turnstile> Object has_fields FDTs"

lemma has_fields_fun:
assumes 1: "P \<turnstile> C has_fields FDTs"
shows "!!FDTs'. P \<turnstile> C has_fields FDTs' ==> FDTs' = FDTs"
 (*<*)
using 1
proof induct
  case (has_fields_rec C D Dres Cres fs ms Cres')
  have class: "class P C = Some (D, fs, ms)"
   and notObj: "C ≠ Object" and DFields: "P \<turnstile> D has_fields Dres"
   and IH: "!!Dres'. P \<turnstile> D has_fields Dres' ==> Dres' = Dres"
   and Cres: "Cres = map (λ(F,T). ((F,C),T)) fs @ Dres"
   and CFields': "P \<turnstile> C has_fields Cres'" .
  from CFields' notObj class obtain Dres'
    where DFields': "P \<turnstile> D has_fields Dres'"
     and Cres': "Cres' = map (λ(F,T). ((F,C),T)) fs @ Dres'"
    by(auto elim: Fields.elims)
  from Cres Cres' IH[OF DFields'] show "Cres' = Cres" by simp
next
  case has_fields_Object thus ?case by(auto elim: Fields.elims)
qed
(*>*)

lemma all_fields_in_has_fields:
assumes sub: "P \<turnstile> C has_fields FDTs"
shows "[| P \<turnstile> C \<preceq>* D; class P D = Some(D',fs,ms); (F,T) ∈ set fs |]
       ==> ((F,D),T) ∈ set FDTs"
(*<*)
using sub apply(induct)
 apply(simp add:image_def)
 apply(erule converse_rtranclE)
  apply(force)
 apply(drule subcls1D)
 apply fastsimp
apply(force simp:image_def)
done
(*>*)


lemma has_fields_decl_above:
assumes fields: "P \<turnstile> C has_fields FDTs"
shows "((F,D),T) ∈ set FDTs ==> P \<turnstile> C \<preceq>* D"
(*<*)
using fields apply(induct)
 prefer 2 apply(fastsimp dest: tranclD)
apply clarsimp
apply(erule disjE)
 apply(clarsimp simp add:image_def)
apply simp
apply(blast dest:subcls1I converse_rtrancl_into_rtrancl)
done
(*>*)


lemma subcls_notin_has_fields:
assumes fields: "P \<turnstile> C has_fields FDTs"
shows "((F,D),T) ∈ set FDTs ==> (D,C) ∉ (subcls1 P)+"
(*<*)
using fields apply(induct)
 prefer 2 apply(fastsimp dest: tranclD)
apply clarsimp
apply(erule disjE)
 apply(clarsimp simp add:image_def)
 apply(drule tranclD)
 apply clarify
 apply(frule subcls1D)
 apply(fastsimp dest:tranclD all_fields_in_has_fields)
apply simp
apply(blast dest:subcls1I trancl_into_trancl)
done
(*>*)


lemma has_fields_mono_lem:
assumes sub: "P \<turnstile> D \<preceq>* C"
shows "P \<turnstile> C has_fields FDTs
         ==> ∃pre. P \<turnstile> D has_fields pre@FDTs ∧ dom(map_of pre) ∩ dom(map_of FDTs) = {}"
(*<*)
using sub apply(induct rule:converse_rtrancl_induct)
 apply(rule_tac x = "[]" in exI)
 apply simp
apply clarsimp
apply(rename_tac D' D pre)
apply(subgoal_tac "(D',C) : (subcls1 P)^+")
 prefer 2 apply(erule (1) rtrancl_into_trancl2)
apply(drule subcls1D)
apply clarsimp
apply(rename_tac fs ms)
apply(drule (2) has_fields_rec)
 apply(rule refl)
apply(rule_tac x = "map (λ(F,T). ((F,D'),T)) fs @ pre" in exI)
apply simp
apply(simp add:Int_Un_distrib2)
apply(rule equals0I)
apply(auto dest: subcls_notin_has_fields simp:dom_map_of image_def)
done
(*>*)

(* FIXME why is Field not displayed correctly? TypeRel qualifier seems to confuse printer*)
constdefs
  has_field :: "'m prog => cname => vname => ty => cname => bool"
                   ("_ \<turnstile> _ has _:_ in _" [51,51,51,51,51] 50)
  "P \<turnstile> C has F:T in D  ≡
  ∃FDTs. P \<turnstile> C has_fields FDTs ∧ map_of FDTs (F,D) = Some T"

lemma has_field_mono:
  "[| P \<turnstile> C has F:T in D; P \<turnstile> C' \<preceq>* C |] ==> P \<turnstile> C' has F:T in D"
(*<*)
apply(clarsimp simp:has_field_def)
apply(drule (1) has_fields_mono_lem)
apply(fastsimp simp: map_add_def split:option.splits)
done
(*>*)


constdefs
  sees_field :: "'m prog => cname => vname => ty => cname => bool"
                  ("_ \<turnstile> _ sees _:_ in _" [51,51,51,51,51] 50)
  "P \<turnstile> C sees F:T in D  ≡
  ∃FDTs. P \<turnstile> C has_fields FDTs ∧
            map_of (map (λ((F,D),T). (F,(D,T))) FDTs) F = Some(D,T)"

lemma map_of_remap_SomeD:
  "map_of (map (λ((k,k'),x). (k,(k',x))) t) k = Some (k',x) ==> map_of t (k, k') = Some x"
(*<*)by (induct t) (auto simp:fun_upd_apply split: split_if_asm)(*>*)


lemma has_visible_field:
  "P \<turnstile> C sees F:T in D ==> P \<turnstile> C has F:T in D"
(*<*)by(auto simp add:has_field_def sees_field_def map_of_remap_SomeD)(*>*)


lemma sees_field_fun:
  "[|P \<turnstile> C sees F:T in D; P \<turnstile> C sees F:T' in D'|] ==> T' = T ∧ D' = D"
(*<*)by(fastsimp simp:sees_field_def dest:has_fields_fun)(*>*)


lemma sees_field_decl_above:
  "P \<turnstile> C sees F:T in D ==> P \<turnstile> C \<preceq>* D"
(*<*)
apply(auto simp:sees_field_def)
apply(blast  intro: has_fields_decl_above map_of_SomeD map_of_remap_SomeD)
done
(*>*)

(* FIXME ugly *)  
lemma sees_field_idemp:
  "P \<turnstile> C sees F:T in D ==> P \<turnstile> D sees F:T in D"
(*<*)
  apply (unfold sees_field_def)
  apply clarsimp
  apply (rule_tac P = "map_of ?xs F = ?y" in mp)
   prefer 2 
   apply assumption 
  apply (thin_tac "map_of ?xs F = ?y")
  apply (erule Fields.induct)
   apply clarsimp
   apply (frule map_of_SomeD)
   apply clarsimp
   apply (fastsimp intro: has_fields_rec)
  apply clarsimp
  apply (frule map_of_SomeD)
  apply clarsimp
  apply (fastsimp intro: has_fields_Object)
  done
(*>*)

subsection "Functional lookup"

constdefs
  method :: "'m prog => cname => mname => cname × ty list × ty × 'm"
  "method P C M  ≡  THE (D,Ts,T,m). P \<turnstile> C sees M:Ts -> T = m in D"

  field  :: "'m prog => cname => vname => cname × ty"
  "field P C F  ≡  THE (D,T). P \<turnstile> C sees F:T in D"
                                                        
  fields :: "'m prog => cname => ((vname × cname) × ty) list" 
  "fields P C  ≡  THE FDTs. P \<turnstile> C has_fields FDTs"                

lemma [simp]: "P \<turnstile> C has_fields FDTs ==> fields P C = FDTs"
(*<*)by (unfold fields_def) (auto dest: has_fields_fun)(*>*)

lemma field_def2 [simp]: "P \<turnstile> C sees F:T in D ==> field P C F = (D,T)"
(*<*)by (unfold field_def) (auto dest: sees_field_fun)(*>*)

lemma method_def2 [simp]: "P \<turnstile> C sees M: Ts->T = m in D ==> method P C M = (D,Ts,T,m)"
(*<*)by (unfold method_def) (auto dest: sees_method_fun)(*>*)
(*<*)
end
(*>*)