Theory TypeRel

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

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

theory TypeRel imports 
  "~~/src/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" ("_ \<turnstile> _ \<prec>⇧1 _" [71,71,71] 70)
  for P :: "'m prog"
where
  "P \<turnstile> C  \<prec>⇧1 D ≡ (C,D) ∈ subcls1 P"
| subcls1I: "[|class P C = Some (D,rest); C ≠ Object|] ==> P \<turnstile> C \<prec>⇧1 D"

abbreviation
  subcls  :: "'m prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>⇧* _"  [71,71,71] 70)
  where "P \<turnstile> C  \<preceq>⇧*  D ≡ (C,D) ∈ (subcls1 P)⇧*"

lemma subcls1D: "P \<turnstile> C \<prec>⇧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 \<turnstile> Object \<prec>⇧1 C"
(*<*)by(fastforce dest:subcls1D)(*>*)

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

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

lemma finite_subcls1: "finite (subcls1 P)"
(*<*)
apply (simp add: subcls1_def2)
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 *}

inductive
  widen   :: "'m prog => ty => ty => bool" ("_ \<turnstile> _ ≤ _"   [71,71,71] 70)
  for P :: "'m prog"
where
  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"

abbreviation (xsymbols)
  widens :: "'m prog => ty list => ty list => bool"
    ("_ \<turnstile> _ [≤] _" [71,71,71] 70) where
  "widens P Ts Ts' ≡ list_all2 (widen P) Ts Ts'"

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

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

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

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

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

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


lemma Class_widen: "P \<turnstile> Class C ≤ T  ==>  ∃D. T = Class D"
(*<*)
apply (ind_cases "P \<turnstile> Class C ≤ 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> Class C ≤ Class D")
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 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 \<rightharpoonup> (ty list × ty × 'm) × cname] => bool"
                    ("_ \<turnstile> _ sees'_methods _" [51,51,51] 50)
  for P :: "'m prog"
where
  sees_methods_Object:
 "[| class P Object = Some(D,fs,ms); Mm = Option.map (λm. (m,Object)) o 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)) o 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 fs ms Dres Cres 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)) o map_of ms)"
   and Cmethods': "P \<turnstile> C sees_methods Cres'" by fact+
  from Cmethods' notObj "class" obtain Dres'
    where Dmethods': "P \<turnstile> D sees_methods Dres'"
     and Cres': "Cres' = Dres' ++ (Option.map (λm. (m,C)) o 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 \<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(fastforce 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(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 \<turnstile> C' \<preceq>⇧* C"
shows "P \<turnstile> C sees_methods Mm ==>
       ∃Mm' Mm⇣2. P \<turnstile> C' sees_methods Mm' ∧ Mm' = Mm ++ Mm⇣2 ∧
                 (∀M m D. Mm⇣2 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'')) o 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
(*>*)


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

definition has_method :: "'m prog => cname => mname => bool" ("_ \<turnstile> _ has _" [51,0,51] 50)
where
  "P \<turnstile> C has M ≡ ∃Ts T m D. P \<turnstile> C sees M:Ts->T = m in 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(fastforce 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(fastforce 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(fastforce 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 *}

inductive
  Fields :: "['m prog, cname, ((vname × cname) × ty) list] => bool"
                  ("_ \<turnstile> _ has'_fields _" [51,51,51] 50)
  for P :: "'m prog"
where
  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 fs ms Dres Cres 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'" by fact+
  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.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 \<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 fastforce
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 fastforce
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(fastforce dest: tranclD)
apply clarsimp
apply(erule disjE)
 apply(clarsimp simp add:image_def)
 apply(drule tranclD)
 apply clarify
 apply(frule subcls1D)
 apply(fastforce dest: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_conv_image_fst image_def)
done
(*>*)

(* FIXME why is Field not displayed correctly? TypeRel qualifier seems to confuse printer*)
definition has_field :: "'m prog => cname => vname => ty => cname => bool"
                   ("_ \<turnstile> _ has _:_ in _" [51,51,51,51,51] 50)
where
  "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(fastforce simp: map_add_def split:option.splits)
done
(*>*)


definition sees_field :: "'m prog => cname => vname => ty => cname => bool"
                  ("_ \<turnstile> _ sees _:_ in _" [51,51,51,51,51] 50)
where
  "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(fastforce 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 (fastforce intro: has_fields_rec)
  apply clarsimp
  apply (frule map_of_SomeD)
  apply clarsimp
  apply (fastforce intro: has_fields_Object)
  done
(*>*)

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 \<turnstile> 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 \<turnstile> C sees F:T in D"
                                                        
definition fields :: "'m prog => cname => ((vname × cname) × ty) list" 
where
  "fields P C  ≡  THE FDTs. P \<turnstile> C has_fields FDTs"                

lemma fields_def2 [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)(*>*)

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 \<turnstile> C has_fields FDTs; map_of FDTs (F, D) = ⌊T⌋ |]
  ==> P \<turnstile> 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 \<turnstile> C has_fields FDTs; map_of (map (λ((F, D), T). (F, D, T)) FDTs) F = ⌊(D, T)⌋ |]
  ==> P \<turnstile> 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 \<turnstile> C sees_methods Mm; Mm M = ⌊((Ts, T, m), D)⌋ |]
  ==> P \<turnstile> C sees M: Ts->T = 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 \<turnstile> C sees M:Ts->T=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_def Sup_fun_def Sup_bool_def fun_eq_iff)
done

lemma eval_Fields_conv:
  "Predicate.eval (Fields_i_i_o P C) = (λFDTs. P \<turnstile> 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 \<turnstile> 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 \<turnstile> 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_def Sup_fun_def Sup_bool_def fun_eq_iff)
done

(*<*)
end
(*>*)