Theory Annotate

(*  Title:      Jinja/J/Annotate.thy
    Author:     Tobias Nipkow, Andreas Lochbihler
*)

section ‹Program annotation›

theory Annotate
imports
  WellType
begin

abbreviation (output)
  unanFAcc :: "'addr expr ⇒ vname ⇒ 'addr expr" (‹(_∙_)› [10,10] 90)
where
  "unanFAcc e F ≡ FAcc e F (STR '''')"

abbreviation (output)
  unanFAss :: "'addr expr ⇒ vname ⇒ 'addr expr ⇒ 'addr expr" (‹(_∙_ := _)› [10,0,90] 90)
where
  "unanFAss e F e' ≡ FAss e F (STR '''') e'"

definition array_length_field_name :: vname
where "array_length_field_name = STR ''length''"

notation (output) array_length_field_name (‹length›)

definition super :: vname
where "super = STR ''super''"

lemma super_neq_this [simp]: "super ≠ this" "this ≠ super"
by(simp_all add: this_def super_def)

inductive Anno :: "(ty ⇒ ty ⇒ ty ⇒ bool) ⇒ 'addr J_prog ⇒ env ⇒ 'addr expr ⇒ 'addr expr ⇒ bool" 
  (‹_,_,_ ⊢ _ ↝ _›   [51,51,0,0,51]50)
  and Annos :: "(ty ⇒ ty ⇒ ty ⇒ bool) ⇒ 'addr J_prog ⇒ env ⇒ 'addr expr list ⇒ 'addr expr list ⇒ bool"
  (‹_,_,_ ⊢ _ [↝] _› [51,51,0,0,51]50)
for is_lub :: "ty ⇒ ty ⇒ ty ⇒ bool" and P :: "'addr J_prog"
where
  AnnoNew: "is_lub,P,E ⊢ new C ↝ new C"
| AnnoNewArray: "is_lub,P,E ⊢ i ↝ i' ⟹ is_lub,P,E ⊢ newA T⌊i⌉ ↝ newA T⌊i'⌉"
| AnnoCast: "is_lub,P,E ⊢ e ↝ e' ⟹ is_lub,P,E ⊢ Cast C e ↝ Cast C e'"
| AnnoInstanceOf: "is_lub,P,E ⊢ e ↝ e' ⟹ is_lub,P,E ⊢ e instanceof T ↝ e' instanceof T"
| AnnoVal: "is_lub,P,E ⊢ Val v ↝ Val v"
| AnnoVarVar: "⟦ E V = ⌊T⌋; V ≠ super ⟧ ⟹ is_lub,P,E ⊢ Var V ↝ Var V"
| AnnoVarField:
  ― ‹There is no need to handle access of array fields explicitly,
    because arrays do not implement methods, i.e. @{term "this"} is
    always of a @{term "Class"} type.›
  "⟦ E V = None; V ≠ super; E this = ⌊Class C⌋; P ⊢ C sees V:T (fm) in D ⟧
  ⟹ is_lub,P,E ⊢ Var V ↝ Var this∙V{D}"
| AnnoBinOp:
  "⟦ is_lub,P,E ⊢ e1 ↝ e1';  is_lub,P,E ⊢ e2 ↝ e2' ⟧
   ⟹ is_lub,P,E ⊢ e1 «bop» e2 ↝ e1' «bop» e2'"
| AnnoLAssVar:
  "⟦ E V = ⌊T⌋; V ≠ super; is_lub,P,E ⊢ e ↝ e' ⟧ ⟹ is_lub,P,E ⊢ V:=e ↝ V:=e'"
| AnnoLAssField:
  "⟦ E V = None; V ≠ super; E this = ⌊Class C⌋; P ⊢ C sees V:T (fm) in D; is_lub,P,E ⊢ e ↝ e' ⟧
   ⟹ is_lub,P,E ⊢ V:=e ↝ Var this∙V{D} := e'"
| AnnoAAcc:
  "⟦ is_lub,P,E ⊢ a ↝ a'; is_lub,P,E ⊢ i ↝ i' ⟧ ⟹ is_lub,P,E ⊢ a⌊i⌉ ↝ a'⌊i'⌉"
| AnnoAAss:
  "⟦ is_lub,P,E ⊢ a ↝ a'; is_lub,P,E ⊢ i ↝ i'; is_lub,P,E ⊢ e ↝ e' ⟧ ⟹ is_lub,P,E ⊢ a⌊i⌉ := e ↝ a'⌊i'⌉ := e'"
| AnnoALength:
  "is_lub,P,E ⊢ a ↝ a' ⟹ is_lub,P,E ⊢ a∙length ↝ a'∙length"
| ― ‹All arrays implicitly declare a final field called @{term "array_length_field_name"} to
    store the array length, which hides a potential field of the same name in @{term "Object"} (cf. JLS 6.4.5).
    The last premise implements the hiding because field lookup does does not model the implicit declaration.›
  AnnoFAcc:
  "⟦ is_lub,P,E ⊢ e ↝ e';  is_lub,P,E ⊢ e' :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees F:T (fm) in D; 
     is_Array U ⟶ F ≠ array_length_field_name ⟧
   ⟹ is_lub,P,E ⊢ e∙F{STR ''''} ↝ e'∙F{D}"
| AnnoFAccALength:
  "⟦ is_lub,P,E ⊢ e ↝ e'; is_lub,P,E ⊢ e' :: T⌊⌉ ⟧
  ⟹ is_lub,P,E ⊢ e∙array_length_field_name{STR ''''} ↝ e'∙length"
| AnnoFAccSuper:
  ― ‹In class C with super class D, "super" is syntactic sugar for "((D) this)" (cf. JLS, 15.11.2)›
  "⟦ E this = ⌊Class C⌋; C ≠ Object; class P C = ⌊(D, fs, ms)⌋; 
     P ⊢ D sees F:T (fm) in D' ⟧
  ⟹ is_lub,P,E ⊢ Var super∙F{STR ''''} ↝ (Cast (Class D) (Var this))∙F{D'}"
|  AnnoFAss:
  "⟦ is_lub,P,E ⊢ e1 ↝ e1';  is_lub,P,E ⊢ e2 ↝ e2';
     is_lub,P,E ⊢ e1' :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees F:T (fm) in D;
     is_Array U ⟶ F ≠ array_length_field_name ⟧
  ⟹ is_lub,P,E ⊢ e1∙F{STR ''''} := e2 ↝ e1'∙F{D} := e2'"
| AnnoFAssSuper:
  "⟦ E this = ⌊Class C⌋; C ≠ Object; class P C = ⌊(D, fs, ms)⌋;
     P ⊢ D sees F:T (fm) in D'; is_lub,P,E ⊢ e ↝ e' ⟧
  ⟹ is_lub,P,E ⊢ Var super∙F{STR ''''} := e ↝ (Cast (Class D) (Var this))∙F{D'} := e'"
| AnnoCAS:
  "⟦ is_lub,P,E ⊢ e1 ↝ e1'; is_lub,P,E ⊢ e2 ↝ e2'; is_lub,P,E ⊢ e3 ↝ e3' ⟧
  ⟹ is_lub,P,E ⊢ e1∙compareAndSwap(D∙F, e2, e3) ↝ e1'∙compareAndSwap(D∙F, e2', e3')"
| AnnoCall:
  "⟦ is_lub,P,E ⊢ e ↝ e';  is_lub,P,E ⊢ es [↝] es' ⟧
   ⟹ is_lub,P,E ⊢ Call e M es ↝ Call e' M es'"
| AnnoBlock:
  "is_lub,P,E(V ↦ T) ⊢ e ↝ e'  ⟹  is_lub,P,E ⊢ {V:T=vo; e} ↝ {V:T=vo; e'}"
| AnnoSync:
  "⟦ is_lub,P,E ⊢ e1 ↝ e1'; is_lub,P,E ⊢ e2 ↝ e2' ⟧
  ⟹ is_lub,P,E ⊢ sync(e1) e2 ↝ sync(e1') e2'"
| AnnoComp:
  "⟦ is_lub,P,E ⊢ e1 ↝ e1';  is_lub,P,E ⊢ e2 ↝ e2' ⟧
  ⟹  is_lub,P,E ⊢ e1;;e2 ↝ e1';;e2'"
| AnnoCond:
  "⟦ is_lub,P,E ⊢ e ↝ e'; is_lub,P,E ⊢ e1 ↝ e1';  is_lub,P,E ⊢ e2 ↝ e2' ⟧
   ⟹ is_lub,P,E ⊢ if (e) e1 else e2 ↝ if (e') e1' else e2'"
| AnnoLoop:
  "⟦ is_lub,P,E ⊢ e ↝ e';  is_lub,P,E ⊢ c ↝ c' ⟧
  ⟹ is_lub,P,E ⊢ while (e) c ↝ while (e') c'"
| AnnoThrow:
  "is_lub,P,E ⊢ e ↝ e' ⟹ is_lub,P,E ⊢ throw e ↝ throw e'"
| AnnoTry:
  "⟦ is_lub,P,E ⊢ e1 ↝ e1';  is_lub,P,E(V ↦ Class C) ⊢ e2 ↝ e2' ⟧
   ⟹ is_lub,P,E ⊢ try e1 catch(C V) e2 ↝ try e1' catch(C V) e2'"

| AnnoNil:
  "is_lub,P,E ⊢ [] [↝] []"
| AnnoCons:
  "⟦ is_lub,P,E ⊢ e ↝ e';  is_lub,P,E ⊢ es [↝] es' ⟧ ⟹  is_lub,P,E ⊢ e#es [↝] e'#es'"

inductive_cases Anno_cases [elim!]:
  "is_lub',P,E ⊢ new C ↝ e"
  "is_lub',P,E ⊢ newA T⌊e⌉ ↝ e'"
  "is_lub',P,E ⊢ Cast T e ↝ e'"
  "is_lub',P,E ⊢ e instanceof T ↝ e'"
  "is_lub',P,E ⊢ Val v ↝ e'"
  "is_lub',P,E ⊢ Var V ↝ e'"
  "is_lub',P,E ⊢ e1 «bop» e2 ↝ e'"
  "is_lub',P,E ⊢ V := e ↝ e'"
  "is_lub',P,E ⊢ e1⌊e2⌉ ↝ e'"
  "is_lub',P,E ⊢ e1⌊e2⌉ := e3 ↝ e'"
  "is_lub',P,E ⊢ e∙length ↝ e'"
  "is_lub',P,E ⊢ e∙F{D} ↝ e'"
  "is_lub',P,E ⊢ e1∙F{D} := e2 ↝ e'"
  "is_lub',P,E ⊢ e1∙compareAndSwap(D∙F, e2, e3) ↝ e'"
  "is_lub',P,E ⊢ e∙M(es) ↝ e'"
  "is_lub',P,E ⊢ {V:T=vo; e} ↝ e'"
  "is_lub',P,E ⊢ sync(e1) e2 ↝ e'"
  "is_lub',P,E ⊢ insync(a) e2 ↝ e'"
  "is_lub',P,E ⊢ e1;; e2 ↝ e'"
  "is_lub',P,E ⊢ if (e) e1 else e2 ↝ e'"
  "is_lub',P,E ⊢ while(e1) e2 ↝ e'"
  "is_lub',P,E ⊢ throw e ↝ e'"
  "is_lub',P,E ⊢ try e1 catch(C V) e2 ↝ e'"

inductive_cases Annos_cases [elim!]:
  "is_lub',P,E ⊢ [] [↝] es'"
  "is_lub',P,E ⊢ e # es [↝] es'"

abbreviation Anno' :: "'addr J_prog ⇒ env ⇒ 'addr expr ⇒ 'addr expr ⇒ bool"  (‹_,_ ⊢ _ ↝ _›   [51,0,0,51]50)
where "Anno' P ≡ Anno (TypeRel.is_lub P) P"

abbreviation Annos' :: "'addr J_prog ⇒ env ⇒ 'addr expr list ⇒ 'addr expr list ⇒ bool"  (‹_,_ ⊢ _ [↝] _› [51,0,0,51]50)
where "Annos' P ≡ Annos (TypeRel.is_lub P) P"

definition annotate :: "'addr J_prog ⇒ env ⇒ 'addr expr ⇒ 'addr expr"
where "annotate P E e = THE_default e (λe'. P,E ⊢ e ↝ e')"

lemma fixes is_lub :: "ty ⇒ ty ⇒ ty ⇒ bool" (‹⊢ lub'((_,/ _)') = _› [51,51,51] 50)
  assumes is_lub_unique: "⋀T1 T2 T3 T4. ⟦ ⊢ lub(T1, T2) = T3; ⊢ lub(T1, T2) = T4 ⟧ ⟹ T3 = T4"
  shows Anno_fun: "⟦ is_lub,P,E ⊢ e ↝ e'; is_lub,P,E ⊢ e ↝ e'' ⟧ ⟹ e' = e''"
  and Annos_fun: "⟦ is_lub,P,E ⊢ es [↝] es'; is_lub,P,E ⊢ es [↝] es'' ⟧ ⟹ es' = es''"
proof(induct arbitrary: e'' and es'' rule: Anno_Annos.inducts)
  case (AnnoFAcc E e e' U C F T fm D)
  from ‹is_lub,P,E ⊢ e∙F{STR ''''} ↝ e''› show ?case
  proof(rule Anno_cases)
    fix e''' U' C' T' fm' D'
    assume "is_lub,P,E ⊢ e ↝ e'''" "is_lub,P,E ⊢ e''' :: U'"
      and "class_type_of' U' = ⌊C'⌋"
      and "P ⊢ C' sees F:T' (fm') in D'" "e'' = e'''∙F{D'}"
    from ‹is_lub,P,E ⊢ e ↝ e'''› have "e' = e'''" by(rule AnnoFAcc)
    with ‹is_lub,P,E ⊢ e' :: U› ‹is_lub,P,E ⊢ e''' :: U'›
    have "U = U'" by(auto intro: WT_unique is_lub_unique)
    with ‹class_type_of' U = ⌊C⌋› ‹class_type_of' U' = ⌊C'⌋›
    have "C = C'" by(auto)
    with ‹P ⊢ C' sees F:T' (fm') in D'› ‹P ⊢ C sees F:T (fm) in D›
    have "D' = D" by(auto dest: sees_field_fun)
    with ‹e'' = e'''∙F{D'}› ‹e' = e'''› show ?thesis by simp
  next
    fix e''' T
    assume "e'' = e'''∙length"
      and "is_lub,P,E ⊢ e''' :: T⌊⌉"
      and "is_lub,P,E ⊢ e ↝ e'''"
      and "F = array_length_field_name"
    from ‹is_lub,P,E ⊢ e ↝ e'''› have "e' = e'''" by(rule AnnoFAcc)
    with ‹is_lub,P,E ⊢ e' :: U› ‹is_lub,P,E ⊢ e''' :: T⌊⌉› have "U = T⌊⌉" by(auto intro: WT_unique is_lub_unique)
    with ‹class_type_of' U = ⌊C⌋› ‹is_Array U ⟶ F ≠ array_length_field_name›
    show ?thesis using ‹F = array_length_field_name› by simp
  next
    fix C' D' fs ms T D''
    assume "E this = ⌊Class C'⌋"
      and "class P C' = ⌊(D', fs, ms)⌋"
      and "e = Var super"
      and "e'' = Cast (Class D') (Var this)∙F{D''}"
    with ‹is_lub,P,E ⊢ e ↝ e'› have False by(auto)
    thus ?thesis ..
  qed
next
  case AnnoFAccALength thus ?case by(fastforce intro: WT_unique[OF is_lub_unique])
next
  case (AnnoFAss E e1 e1' e2 e2' U C F T fm D)
  from ‹is_lub,P,E ⊢ e1∙F{STR ''''} := e2 ↝ e''› 
  show ?case
  proof(rule Anno_cases)
    fix e1'' e2'' U' C' T' fm' D'
    assume "is_lub,P,E ⊢ e1 ↝ e1''" "is_lub,P,E ⊢ e2 ↝ e2''"
      and "is_lub,P,E ⊢ e1'' :: U'" and "class_type_of' U' = ⌊C'⌋"
      and "P ⊢ C' sees F:T' (fm') in D'"
      and "e'' = e1''∙F{D'} := e2''"
    from ‹is_lub,P,E ⊢ e1 ↝ e1''› have "e1' = e1''" by(rule AnnoFAss)
    moreover with ‹is_lub,P,E ⊢ e1' :: U› ‹is_lub,P,E ⊢ e1'' :: U'›
    have "U = U'" by(auto intro: WT_unique is_lub_unique)
    with ‹class_type_of' U = ⌊C⌋› ‹class_type_of' U' = ⌊C'⌋›
    have "C = C'" by(auto)
    with ‹P ⊢ C' sees F:T' (fm') in D'› ‹P ⊢ C sees F:T (fm) in D›
    have "D' = D" by(auto dest: sees_field_fun)
    moreover from ‹is_lub,P,E ⊢ e2 ↝ e2''› have "e2' = e2''" by(rule AnnoFAss)
    ultimately show ?thesis using ‹e'' = e1''∙F{D'} := e2''› by simp
  next
    fix C' D' fs ms T' fm' D'' e'''
    assume "e'' = Cast (Class D') (Var this)∙F{D''} := e'''"
      and "E this = ⌊Class C'⌋"
      and "class P C' = ⌊(D', fs, ms)⌋"
      and "P ⊢ D' sees F:T' (fm') in D''"
      and "is_lub,P,E ⊢ e2 ↝ e'''"
      and "e1 = Var super"
    with ‹is_lub,P,E ⊢ e1 ↝ e1'› have False by(auto elim: Anno_cases)
    thus ?thesis ..
  qed
qed(fastforce dest: sees_field_fun)+

subsection ‹Code generation›

definition Anno_code :: "'addr J_prog ⇒ env ⇒ 'addr expr ⇒ 'addr expr ⇒ bool" (‹_,_ ⊢ _ ↝'' _›   [51,0,0,51]50)
where "Anno_code P = Anno (is_lub_sup P) P"

definition Annos_code :: "'addr J_prog ⇒ env ⇒ 'addr expr list ⇒ 'addr expr list ⇒ bool" (‹_,_ ⊢ _ [↝''] _› [51,0,0,51]50)
where "Annos_code P = Annos (is_lub_sup P) P"

primrec block_types :: "('a, 'b, 'addr) exp ⇒ ty list" 
  and blocks_types :: "('a, 'b, 'addr) exp list ⇒ ty list"
where 
  "block_types (new C) = []"
| "block_types (newA T⌊e⌉) = block_types e"
| "block_types (Cast U e) = block_types e"
| "block_types (e instanceof U) = block_types e"
| "block_types (e1«bop»e2) = block_types e1 @ block_types e2"
| "block_types (Val v) = []"
| "block_types (Var V) = []"
| "block_types (V := e) = block_types e"
| "block_types (a⌊i⌉) = block_types a @ block_types i"
| "block_types (a⌊i⌉ := e) = block_types a @ block_types i @ block_types e"
| "block_types (a∙length) = block_types a"
| "block_types (e∙F{D}) = block_types e"
| "block_types (e∙F{D} := e') = block_types e @ block_types e'"
| "block_types (e∙compareAndSwap(D∙F, e', e'')) = block_types e @ block_types e' @ block_types e''"
| "block_types (e∙M(es)) = block_types e @ blocks_types es"
| "block_types {V:T=vo; e} = T # block_types e"
| "block_types (sync⇘V⇙(e) e') = block_types e @ block_types e'"
| "block_types (insync⇘V⇙(a) e) = block_types e"
| "block_types (e;;e') = block_types e @ block_types e'"
| "block_types (if (e) e1 else e2) = block_types e @ block_types e1 @ block_types e2"
| "block_types (while (b) c) = block_types b @ block_types c"
| "block_types (throw e) = block_types e"
| "block_types (try e catch(C V) e') = block_types e @ Class C # block_types e'"

| "blocks_types [] = []"
| "blocks_types (e#es) = block_types e @ blocks_types es"

lemma fixes is_lub1 :: "ty ⇒ ty ⇒ ty ⇒ bool" (‹⊢1 lub'((_,/ _)') = _› [51,51,51] 50)
  and is_lub2 :: "ty ⇒ ty ⇒ ty ⇒ bool" (‹⊢2 lub'((_,/ _)') = _› [51,51,51] 50)
  assumes wf: "wf_prog wf_md P"
  and is_lub1_into_is_lub2: "⋀T1 T2 T3. ⟦ ⊢1 lub(T1, T2) = T3; is_type P T1; is_type P T2 ⟧ ⟹ ⊢2 lub(T1, T2) = T3"
  and is_lub2_is_type: "⋀T1 T2 T3. ⟦ ⊢2 lub(T1, T2) = T3; is_type P T1; is_type P T2 ⟧ ⟹ is_type P T3"
  shows Anno_change_is_lub:
  "⟦ is_lub1,P,E ⊢ e ↝ e'; ran E ∪ set (block_types e) ⊆ types P ⟧ ⟹ is_lub2,P,E ⊢ e ↝ e'"
  and Annos_change_is_lub:
  "⟦ is_lub1,P,E ⊢ es [↝] es'; ran E ∪ set (blocks_types es) ⊆ types P ⟧ ⟹ is_lub2,P,E ⊢ es [↝] es'"
proof(induct rule: Anno_Annos.inducts)
  case (AnnoBlock E V T e e' vo)
  from ‹ran E ∪ set (block_types {V:T=vo; e}) ⊆ types P›
  have "ran (E(V ↦ T)) ∪ set (block_types e) ⊆ types P"
    by(auto simp add: ran_def)
  thus ?case using AnnoBlock by(blast intro: Anno_Annos.intros)
next
  case (AnnoTry E e1 e1' V C e2 e2')
  from ‹ran E ∪ set (block_types (try e1 catch(C V) e2)) ⊆ types P›
  have "ran (E(V ↦ Class C)) ∪ set (block_types e2) ⊆ types P"
    by(auto simp add: ran_def)
  thus ?case using AnnoTry by(simp del: fun_upd_apply)(blast intro: Anno_Annos.intros)
qed(simp_all del: is_Array.simps is_Array_conv, (blast intro: Anno_Annos.intros WT_change_is_lub[OF wf, where ?is_lub1.0=is_lub1 and ?is_lub2.0=is_lub2] is_lub1_into_is_lub2 is_lub2_is_type)+)

lemma assumes wf: "wf_prog wf_md P"
  shows Anno_into_Anno_code: "⟦ P,E ⊢ e ↝ e'; ran E ∪ set (block_types e) ⊆ types P ⟧ ⟹ P,E ⊢ e ↝' e'"
  and Annos_into_Annos_code: "⟦ P,E ⊢ es [↝] es'; ran E ∪ set (blocks_types es) ⊆ types P ⟧ ⟹ P,E ⊢ es [↝'] es'"
proof -
  assume anno: "P,E ⊢ e ↝ e'" 
    and ran: "ran E ∪ set (block_types e) ⊆ types P"
  show "P,E ⊢ e ↝' e'" unfolding Anno_code_def
    by(rule Anno_change_is_lub[OF wf _ _ anno ran])(blast intro!: is_lub_sup.intros intro: is_lub_subD[OF wf] sup_is_type[OF wf] elim!: is_lub_sup.cases)+ 
next
  assume annos: "P,E ⊢ es [↝] es'"
    and ran: "ran E ∪ set (blocks_types es) ⊆ types P"
  show "P,E ⊢ es [↝'] es'" unfolding Annos_code_def
    by(rule Annos_change_is_lub[OF wf _ _ annos ran])(blast intro!: is_lub_sup.intros intro: is_lub_subD[OF wf] sup_is_type[OF wf] elim!: is_lub_sup.cases)+
qed 

lemma assumes wf: "wf_prog wf_md P"
  shows Anno_code_into_Anno: "⟦ P,E ⊢ e ↝' e'; ran E ∪ set (block_types e) ⊆ types P ⟧ ⟹ P,E ⊢ e ↝ e'"
  and Annos_code_into_Annos: "⟦ P,E ⊢ es [↝'] es'; ran E ∪ set (blocks_types es) ⊆ types P ⟧ ⟹ P,E ⊢ es [↝] es'"
proof -
  assume anno: "P,E ⊢ e ↝' e'" 
    and ran: "ran E ∪ set (block_types e) ⊆ types P"
  show "P,E ⊢ e ↝ e'"
    by(rule Anno_change_is_lub[OF wf _ _ anno[unfolded Anno_code_def] ran])(blast elim!: is_lub_sup.cases intro: sup_is_lubI[OF wf] is_lub_is_type[OF wf])+
next
  assume annos: "P,E ⊢ es [↝'] es'"
    and ran: "ran E ∪ set (blocks_types es) ⊆ types P"
  show "P,E ⊢ es [↝] es'"
    by(rule Annos_change_is_lub[OF wf _ _ annos[unfolded Annos_code_def] ran])(blast elim!: is_lub_sup.cases intro: sup_is_lubI[OF wf] is_lub_is_type[OF wf])+
qed

lemma fixes is_lub
  assumes wf: "wf_prog wf_md P"
  shows WT_block_types_is_type: "is_lub,P,E ⊢ e :: T ⟹ set (block_types e) ⊆ types P"
  and WTs_blocks_types_is_type: "is_lub,P,E ⊢ es [::] Ts ⟹ set (blocks_types es) ⊆ types P"
apply(induct rule: WT_WTs.inducts)
apply(auto intro: is_class_sub_Throwable[OF wf])
done

lemma fixes is_lub
  shows Anno_block_types: "is_lub,P,E ⊢ e ↝ e' ⟹ block_types e = block_types e'"
  and Annos_blocks_types: "is_lub,P,E ⊢ es [↝] es' ⟹ blocks_types es = blocks_types es'"
by(induct rule: Anno_Annos.inducts) auto

code_pred 
  (modes: (i ⇒ i ⇒ o ⇒ bool) ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool)
  [detect_switches, skip_proof]
  Anno
.

definition annotate_code :: "'addr J_prog ⇒ env ⇒ 'addr expr ⇒ 'addr expr"
where "annotate_code P E e = THE_default e (λe'. P,E ⊢ e ↝' e')"

code_pred
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ bool)
  [inductify]
  Anno_code 
.

lemma eval_Anno_i_i_i_o_conv:
  "Predicate.eval (Anno_code_i_i_i_o P E e) = (λe'. P,E ⊢ e ↝' e')"
by(auto intro!: ext intro: Anno_code_i_i_i_oI elim: Anno_code_i_i_i_oE)
 
lemma annotate_code [code]:
  "annotate_code P E e = Predicate.singleton (λ_. Code.abort (STR ''annotate'') (λ_. e)) (Anno_code_i_i_i_o P E e)"
by(simp add: THE_default_def Predicate.singleton_def annotate_code_def eval_Anno_i_i_i_o_conv)

end