Theory TypeRel

(*  Title:      Jinja/Common/TypeRel.thy
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Relations between Jinja Types›

theory TypeRel imports 
  "HOL-Library.Transitive_Closure_Table"
  Decl 
begin

subsection‹The subclass relations›

inductive_set
  subcls1 :: "'m prog  (cname × cname) set"
  and subcls1' :: "'m prog  [cname, cname]  bool" ("_  _ 1 _" [71,71,71] 70)
  for P :: "'m prog"
where
  "P  C  1 D  (C,D)  subcls1 P"
| subcls1I: "class P C = Some (D,rest); C  Object  P  C 1 D"

abbreviation
  subcls  :: "'m prog  [cname, cname]  bool" ("_  _ * _"  [71,71,71] 70)
  where "P  C  *  D  (C,D)  (subcls1 P)*"

lemma subcls1D: "P  C 1 D  C  Object  (fs ms. class P C = Some (D,fs,ms))"
(*<*)by(erule subcls1.induct)(fastforce simp add:is_class_def)(*>*)

lemma [iff]: "¬ P  Object 1 C"
(*<*)by(fastforce dest:subcls1D)(*>*)

lemma [iff]: "(P  Object * C) = (C = Object)"
(*<*)
proof(rule iffI)
 assume "P  Object * C" then show "C = Object"
  by(auto elim: converse_rtranclE)
qed simp
(*>*)

lemma subcls1_def2:
  "subcls1 P =
     (SIGMA C:{C. is_class P C}. {D. CObject  fst (the (class P C))=D})"
(*<*)
  by (fastforce simp:is_class_def dest: subcls1D elim: subcls1I)
(*>*)

lemma finite_subcls1: "finite (subcls1 P)"
(*<*)
proof -
  let ?SIG = "SIGMA C:{C. is_class P C}. {D. fst (the (class P C)) = D  C  Object}"
  have "subcls1 P = ?SIG" by(simp add: subcls1_def2)
  also have "finite ?SIG"
  proof(rule finite_SigmaI [OF finite_is_class])
    fix C assume C_in: "C  {C. is_class P C}"
    then show "finite {D. fst (the (class P C)) = D  C  Object}"
     by(rule_tac finite_subset[where B = "{fst (the (class P C))}"]) auto
  qed
  ultimately show ?thesis by simp
qed
(*>*)
(*
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 ⊢ C ≼* 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›

inductive
  widen   :: "'m prog  ty  ty  bool" ("_  _  _"   [71,71,71] 70)
  for P :: "'m prog"
where
  widen_refl[iff]: "P  T  T"
| widen_subcls: "P  C * D    P  Class C  Class D"
| widen_null[iff]: "P  NT  Class C"

abbreviation
  widens :: "'m prog  ty list  ty list  bool"
    ("_  _ [≤] _" [71,71,71] 70) where
  "widens P Ts Ts'  list_all2 (widen P) Ts Ts'"

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

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

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

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

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

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


lemma Class_widen: "P  Class C  T    D. T = Class D"
(*<*)
by (ind_cases "P  Class C  T") auto
(*>*)

lemma [iff]: "(P  T  NT) = (T = NT)"
(*<*)
by(cases T) (auto dest:Class_widen)
(*>*)

lemma Class_widen_Class [iff]: "(P  Class C  Class D) = (P  C * D)"
(*<*)
proof(rule iffI)
  show "P  Class C  Class D  P  C * D"
  proof(ind_cases "P  Class C  Class D") qed(auto)
qed(auto elim: widen_subcls)
(*>*)

lemma widen_Class: "(P  T  Class C) = (T = NT  (D. T = Class D  P  D * C))"
(*<*)by(induct T, auto)(*>*)


lemma widen_trans[trans]: "P  S  U; P  U  T  P  S  T"
(*<*)
proof -
  assume "PS  U" thus "T. P  U  T  P  S  T"
  proof induct
    case (widen_refl T T') thus "P  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  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  NT  RT" by auto
  qed
qed
(*>*)

lemma widens_trans [trans]: "P  Ss [≤] Ts; P  Ts [≤] Us  P  Ss [≤] Us"
(*<*)by (rule list_all2_trans, rule widen_trans)(*>*)


(*<*)
lemmas widens_refl [iff] = list_all2_refl [of "widen P", OF widen_refl] for P
lemmas widens_Cons [iff] = list_all2_Cons1 [of "widen P"] for P
(*>*)


subsection‹Method lookup›

inductive
  Methods :: "['m prog, cname, mname  (ty list × ty × 'm) × cname]  bool"
                    ("_  _ sees'_methods _" [51,51,51] 50)
  for P :: "'m prog"
where
  sees_methods_Object:
 " class P Object = Some(D,fs,ms); Mm = map_option (λm. (m,Object))  map_of ms 
   P  Object sees_methods Mm"
| sees_methods_rec:
 " class P C = Some(D,fs,ms); C  Object; P  D sees_methods Mm;
    Mm' = Mm ++ (map_option (λm. (m,C))  map_of ms) 
   P  C sees_methods Mm'"

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

lemma visible_methods_exist:
  "P  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  C sees_methods Mm"
shows "Mm M = Some(m,D)  P  C * D"
 (*<*)
using Csees
proof induct
  case sees_methods_Object thus ?case by auto
next
  case sees_methods_rec thus ?case
    by(fastforce simp:map_option_case split:option.splits
                elim:converse_rtrancl_into_rtrancl[OF subcls1I])
qed
(*>*)

lemma sees_methods_idemp:
assumes Cmethods: "P  C sees_methods Mm"
shows "m D. Mm M = Some(m,D) 
              Mm'. (P  D sees_methods Mm')  Mm' M = Some(m,D)"
(*<*)
using Cmethods
proof induct
  case sees_methods_Object thus ?case
    by(fastforce dest: Methods.sees_methods_Object)
next
  case sees_methods_rec thus ?case
    by(fastforce 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  C' * C"
shows "P  C sees_methods Mm 
       Mm' Mm2. P  C' sees_methods Mm'  Mm' = Mm ++ Mm2 
                 (M m D. Mm2 M = Some(m,D)  P  D * C)"
(*<*)
      (is "_  Mm' Mm2. ?Q C' C Mm' Mm2")
using sub
proof (induct rule:converse_rtrancl_induct)
  assume "P  C sees_methods Mm"
  hence "?Q C C Mm Map.empty" by simp
  thus "Mm' Mm2. ?Q C C Mm' Mm2" by blast
next
  fix C'' C'
  assume sub1: "P  C'' 1 C'" and sub: "P  C' * C"
  and IH: "P  C sees_methods Mm 
           Mm' Mm2. P  C' sees_methods Mm' 
                Mm' = Mm ++ Mm2  (M m D. Mm2 M = Some(m,D)  P  D * C)"
  and Csees: "P  C sees_methods Mm"
  from IH[OF Csees] obtain Mm' Mm2 where C'sees: "P  C' sees_methods Mm'"
    and Mm': "Mm' = Mm ++ Mm2"
    and subC:"M m D. Mm2 M = Some(m,D)  P  D * 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 = "map_option (λm. (m,C''))  map_of ms"
  have "P  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
(*>*)


definition Method :: "'m prog  cname  mname  ty list  ty  'm  cname  bool"
            ("_  _ sees _: __ = _ in _" [51,51,51,51,51,51,51] 50)
where
  "P  C sees M: TsT = m in D  
  Mm. P  C sees_methods Mm  Mm M = Some((Ts,T,m),D)"

definition has_method :: "'m prog  cname  mname  bool" ("_  _ has _" [51,0,51] 50)
where
  "P  C has M  Ts T m D. P  C sees M:TsT = m in D"

lemma sees_method_fun:
  "P  C sees M:TST = m in D; P  C sees M:TS'T' = m' in D' 
    TS' = TS  T' = T  m' = m  D' = D"
 (*<*)by(fastforce dest: sees_methods_fun simp:Method_def)(*>*)

lemma sees_method_decl_above:
  "P  C sees M:TsT = m in D  P  C * D"
 (*<*)by(clarsimp simp:Method_def sees_methods_decl_above)(*>*)

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


lemma sees_method_idemp:
  "P  C sees M:TsT=m in D  P  D sees M:TsT=m in D"
 (*<*)by(fastforce simp: Method_def intro:sees_methods_idemp)(*>*)

lemma sees_method_decl_mono:
assumes sub: "P  C' * C" and
        C_sees: "P  C sees M:TsT=m in D" and
        C'_sees: "P  C' sees M:Ts'T'=m' in D'"
shows   "P  D' * D"
 (*<*)
proof -
  obtain Ms where Ms: "P  C sees_methods Ms"
    using C_sees by(auto simp: Method_def)
  obtain Ms' Ms2 where Ms': "P  C' sees_methods Ms'" and
     Ms'_def: "Ms' = Ms ++ Ms2" and
     Ms2_imp: "(M m D. Ms2 M = (m, D)  P  D * C)"
    using sees_methods_decl_mono[OF sub Ms] by clarsimp
  have "(Ms ++ Ms2) M = ((Ts', T', m'), D')"
    using C'_sees sees_methods_fun[OF Ms'] Ms'_def by(clarsimp simp: Method_def)
  then have "Ms2 M = ((Ts', T', m'), D') 
             Ms2 M = None  Ts = Ts'  T = T'  m = m'  D = D'"
    using C_sees sees_methods_fun[OF Ms] by(clarsimp simp: Method_def)
  also have "Ms2 M = ((Ts', T', m'), D')  P  D' * C"
    using Ms2_imp by simp
  ultimately show ?thesis using sub sees_method_decl_above[OF C_sees] by auto
qed
(*>*)

lemma sees_method_is_class:
  " P  C sees M:TsT = m in D   is_class P C"
(*<*)by (auto simp add: is_class_def Method_def elim: Methods.induct)(*>*)


subsection‹Field lookup›

inductive
  Fields :: "['m prog, cname, ((vname × cname) × ty) list]  bool"
                  ("_  _ has'_fields _" [51,51,51] 50)
  for P :: "'m prog"
where
  has_fields_rec:
  " class P C = Some(D,fs,ms); C  Object; P  D has_fields FDTs;
     FDTs' = map (λ(F,T). ((F,C),T)) fs @ FDTs 
    P  C has_fields FDTs'"
| has_fields_Object:
  " class P Object = Some(D,fs,ms); FDTs = map (λ(F,T). ((F,Object),T)) fs 
    P  Object has_fields FDTs"

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

lemma all_fields_in_has_fields:
assumes sub: "P  C has_fields FDTs"
shows " P  C * D; class P D = Some(D',fs,ms); (F,T)  set fs 
        ((F,D),T)  set FDTs"
(*<*)
using sub proof(induct)
  case (has_fields_rec C D' fs ms FDTs FDTs')
  then have C_D: "P  C * D" by simp
  then show ?case proof(rule converse_rtranclE)
    assume "C = D"
    then show ?case using has_fields_rec by force
  next
    fix y assume sub1: "P  C 1 y" and sub2: "P  y * D"
    then show ?case using has_fields_rec subcls1D[OF sub1] by simp
  qed
next
  case (has_fields_Object D fs ms FDTs)
  then show ?case by force
qed
(*>*)


lemma has_fields_decl_above:
assumes fields: "P  C has_fields FDTs"
shows "((F,D),T)  set FDTs  P  C * D"
(*<*)
using fields proof(induct)
  case (has_fields_rec C D' fs ms FDTs FDTs')
  then have "((F, D), T)  (λx. case x of (F, x)  ((F, C), x)) ` set fs 
    ((F, D), T)  set FDTs" by clarsimp
  then show ?case proof(rule disjE)
    assume "((F, D), T)  (λx. case x of (F, x)  ((F, C), x)) ` set fs"
    then show ?case using has_fields_rec by clarsimp
  next
    assume "((F, D), T)  set FDTs"
    then show ?case using has_fields_rec
     by(blast dest:subcls1I converse_rtrancl_into_rtrancl)
  qed
next
  case (has_fields_Object D fs ms FDTs)
  then show ?case by fastforce
qed
(*>*)


lemma subcls_notin_has_fields:
assumes fields: "P  C has_fields FDTs"
shows "((F,D),T)  set FDTs  (D,C)  (subcls1 P)+"
(*<*)
using fields proof(induct)
  case (has_fields_rec C D' fs ms FDTs FDTs')
  then have "((F, D), T)  (λx. case x of (F, x)  ((F, C), x)) ` set fs
                ((F, D), T)  set FDTs" by clarsimp
  then show ?case proof(rule disjE)
    assume "((F, D), T)  (λx. case x of (F, x)  ((F, C), x)) ` set fs"
    then have CD[simp]: "C = D" and fs: "(F, T)  set fs" by clarsimp+
    then have "(D, D)  (subcls1 P)+  False" proof -
      assume DD: "(D, D)  (subcls1 P)+"
      obtain z where z1: "P  D 1 z" and z_s: "P  z * D"
        using tranclD[OF DD] by clarsimp
      have [simp]: "z = D'" using subcls1D[OF z1] has_fields_rec.hyps(1) by clarsimp
      then have "((F, D), T)  set FDTs"
        using z_s all_fields_in_has_fields[OF has_fields_rec.hyps(3) _ has_fields_rec.hyps(1) fs]
         by simp
      then have "(D, z)  (subcls1 P)+" using has_fields_rec.hyps(4) by simp
      then show False using z1 by auto
    qed
    then show ?case by clarsimp
  next
    assume "((F, D), T)  set FDTs"
    then show ?case using has_fields_rec by(blast dest:subcls1I trancl_into_trancl)
  qed
next
  case (has_fields_Object D fs ms FDTs)
  then show ?case by(fastforce dest: tranclD)
qed
(*>*)


lemma has_fields_mono_lem:
assumes sub: "P  D * C"
shows "P  C has_fields FDTs
          pre. P  D has_fields pre@FDTs  dom(map_of pre)  dom(map_of FDTs) = {}"
(*<*)
using sub proof(induct rule:converse_rtrancl_induct)
  case base
  then show ?case by(rule_tac x = "[]" in exI) simp
next
  case (step D' D)
  then obtain pre where D_flds: "P  D has_fields pre @ FDTs" and
    dom: "dom (map_of pre)  dom (map_of FDTs) = {}" by clarsimp
  have "(D',C)  (subcls1 P)^+" by (rule rtrancl_into_trancl2[OF step.hyps(1,2)])
  obtain fs ms where D'_cls: "class P D' = (D, fs, ms)" "D'  Object"
    using subcls1D[OF step.hyps(1)] by clarsimp+
  have "P  D' has_fields map (λ(F, T). ((F, D'), T)) fs @ pre @ FDTs"
    using has_fields_rec[OF D'_cls D_flds] by simp
  also have "dom (map_of (map (λ(F, T). ((F, D'), T)) fs @ pre))
                  dom (map_of FDTs) = {}"
    using dom subcls_notin_has_fields[OF D_flds, where D=D'] step.hyps(1)
      by(auto simp:dom_map_of_conv_image_fst) fast
  ultimately show ?case
    by(rule_tac x = "map (λ(F,T). ((F,D'),T)) fs @ pre" in exI) simp
qed
(*>*)

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

lemma has_field_mono:
assumes has: " P  C has F:T in D" and sub: "P  C' * C"
shows "P  C' has F:T in D"
(*<*)
proof -
  obtain FDTs where FDTs:"P  C has_fields FDTs" and "map_of FDTs (F, D) = T"
    using has by(clarsimp simp: has_field_def)
  also obtain pre where "P  C' has_fields pre @ FDTs"
     and "dom (map_of pre)  dom (map_of FDTs) = {}"
    using has_fields_mono_lem[OF sub FDTs] by clarify
  ultimately show ?thesis by(fastforce simp: has_field_def map_add_def split:option.splits)
qed
(*>*)


definition sees_field :: "'m prog  cname  vname  ty  cname  bool"
                  ("_  _ sees _:_ in _" [51,51,51,51,51] 50)
where
  "P  C sees F:T in D  
  FDTs. P  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: if_split_asm)(*>*)


lemma has_visible_field:
  "P  C sees F:T in D  P  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  C sees F:T in D; P  C sees F:T' in D'  T' = T  D' = D"
(*<*)by(fastforce simp:sees_field_def dest:has_fields_fun)(*>*)


lemma sees_field_decl_above:
  "P  C sees F:T in D  P  C * D"
(*<*)
by(auto simp:sees_field_def
        intro: has_fields_decl_above map_of_SomeD map_of_remap_SomeD)
(*>*)

lemma sees_field_idemp:
assumes sees: "P  C sees F:T in D"
shows "P  D sees F:T in D"
(*<*)
proof -
  obtain FDTs where C_flds: "P  C has_fields FDTs"
     and FDTs: "map_of (map (λ((F, D), T). (F, D, T)) FDTs) F = (D, T)"
     (is "?FDTs")
   using sees by(clarsimp simp: sees_field_def)
  have map: "C' fs. map_of (map ((λ((F, D), a). (F, D, a))  (λ(F, y). ((F, C'), y))) fs) F 
              = (D, T)  C' = D  (F, T)  set fs"
    by(frule map_of_SomeD) clarsimp
  have "?FDTs  P  D sees F:T in D"
  using C_flds proof induct
    case NObj: has_fields_rec
    then show ?case using map by (fastforce intro: has_fields_rec simp: sees_field_def)
  next
    case Obj: has_fields_Object
    then show ?case using map by(fastforce intro: has_fields_Object simp: sees_field_def)
  qed
  then show ?thesis using FDTs by(rule mp)
qed
(*>*)

subsection "Functional lookup"

definition "method" :: "'m prog  cname  mname  cname × ty list × ty × 'm"
where
  "method P C M    THE (D,Ts,T,m). P  C sees M:Ts  T = m in D"

definition field  :: "'m prog  cname  vname  cname × ty"
where
  "field P C F    THE (D,T). P  C sees F:T in D"
                                                        
definition fields :: "'m prog  cname  ((vname × cname) × ty) list" 
where
  "fields P C    THE FDTs. P  C has_fields FDTs"                

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

lemma field_def2 [simp]: "P  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  C sees M: TsT = m in D  method P C M = (D,Ts,T,m)"
(*<*)by (unfold method_def) (auto dest: sees_method_fun)(*>*)

subsection "Code generator setup"

code_pred 
  (modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
  subcls1p 
.
declare subcls1_def [code_pred_def]

code_pred 
  (modes: i ⇒ i × o ⇒ bool, i ⇒ i × i ⇒ bool)
  [inductify]
  subcls1 
.
definition subcls' where "subcls' G = (subcls1p G)^**"
code_pred
  (modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
  [inductify]
  subcls'
.

lemma subcls_conv_subcls' [code_unfold]:
  "(subcls1 G)^* = {(C, D). subcls' G C D}"
  by (simp add: subcls'_def subcls1_def rtrancl_def)

code_pred 
  (modes: i ⇒ i ⇒ i ⇒ bool)
  widen 
.

code_pred 
  (modes: i ⇒ i ⇒ o ⇒ bool)
  Fields
.

lemma has_field_code [code_pred_intro]:
  " P  C has_fields FDTs; map_of FDTs (F, D) = T 
   P  C has F:T in D"
by(auto simp add: has_field_def)

code_pred 
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  has_field
by(auto simp add: has_field_def)

lemma sees_field_code [code_pred_intro]:
  " P  C has_fields FDTs; map_of (map (λ((F, D), T). (F, D, T)) FDTs) F = (D, T) 
   P  C sees F:T in D"
by(auto simp add: sees_field_def)

code_pred 
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ bool, 
          i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  sees_field
by(auto simp add: sees_field_def)

code_pred
  (modes: i ⇒ i ⇒ o ⇒ bool)
  Methods 
.

lemma Method_code [code_pred_intro]:
  " P  C sees_methods Mm; Mm M = ((Ts, T, m), D) 
   P  C sees M: TsT = m in D"
by(auto simp add: Method_def)

code_pred
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ o ⇒ bool,
          i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  Method
by(auto simp add: Method_def)

lemma eval_Method_i_i_i_o_o_o_o_conv:
  "Predicate.eval (Method_i_i_i_o_o_o_o P C M) = (λ(Ts, T, m, D). P  C sees M:TsT=m in D)"
by(auto intro: Method_i_i_i_o_o_o_oI elim: Method_i_i_i_o_o_o_oE intro!: ext)

lemma method_code [code]:
  "method P C M = 
  Predicate.the (Predicate.bind (Method_i_i_i_o_o_o_o P C M) (λ(Ts, T, m, D). Predicate.single (D, Ts, T, m)))"
apply (rule sym, rule the_eqI)
apply (simp add: method_def eval_Method_i_i_i_o_o_o_o_conv)
apply (rule arg_cong [where f=The])
apply (auto simp add: Sup_fun_def Sup_bool_def fun_eq_iff)
done

lemma eval_Fields_conv:
  "Predicate.eval (Fields_i_i_o P C) = (λFDTs. P  C has_fields FDTs)"
by(auto intro: Fields_i_i_oI elim: Fields_i_i_oE intro!: ext)

lemma fields_code [code]:
  "fields P C = Predicate.the (Fields_i_i_o P C)"
by(simp add: fields_def Predicate.the_def eval_Fields_conv)

lemma eval_sees_field_i_i_i_o_o_conv:
  "Predicate.eval (sees_field_i_i_i_o_o P C F) = (λ(T, D). P  C sees F:T in D)"
by(auto intro!: ext intro: sees_field_i_i_i_o_oI elim: sees_field_i_i_i_o_oE)

lemma eval_sees_field_i_i_i_o_i_conv:
  "Predicate.eval (sees_field_i_i_i_o_i P C F D) = (λT. P  C sees F:T in D)"
by(auto intro!: ext intro: sees_field_i_i_i_o_iI elim: sees_field_i_i_i_o_iE)

lemma field_code [code]:
  "field P C F = Predicate.the (Predicate.bind (sees_field_i_i_i_o_o P C F) (λ(T, D). Predicate.single (D, T)))"
apply (rule sym, rule the_eqI)
apply (simp add: field_def eval_sees_field_i_i_i_o_o_conv)
apply (rule arg_cong [where f=The])
apply (auto simp add: Sup_fun_def Sup_bool_def fun_eq_iff)
done

(*<*)
end
(*>*)