# Theory TypeInf

theory TypeInf
imports WellType
```(*  Title:      HOL/MicroJava/Comp/TypeInf.thy
Author:     Martin Strecker
*)

(* Exact position in theory hierarchy still to be determined *)
theory TypeInf
imports "../J/WellType"
begin

(**********************************************************************)

(*** Inversion of typing rules -- to be moved into WellType.thy
Also modify the wtpd_expr_… proofs in CorrComp.thy ***)

lemma NewC_invers:
assumes "E⊢NewC C::T"
shows "T = Class C ∧ is_class (prg E) C"
using assms by cases auto

lemma Cast_invers:
assumes "E⊢Cast D e::T"
shows "∃C. T = Class D ∧ E⊢e::C ∧ is_class (prg E) D ∧ prg E⊢C≼? Class D"
using assms by cases auto

lemma Lit_invers:
assumes "E⊢Lit x::T"
shows "typeof (λv. None) x = Some T"
using assms by cases auto

lemma LAcc_invers:
assumes "E⊢LAcc v::T"
shows "localT E v = Some T ∧ is_type (prg E) T"
using assms by cases auto

lemma BinOp_invers:
assumes "E⊢BinOp bop e1 e2::T'"
shows "∃T. E⊢e1::T ∧ E⊢e2::T ∧
(if bop = Eq then T' = PrimT Boolean
else T' = T ∧ T = PrimT Integer)"
using assms by cases auto

lemma LAss_invers:
assumes  "E⊢v::=e::T'"
shows "∃T. v ~= This ∧ E⊢LAcc v::T ∧ E⊢e::T' ∧ prg E⊢T'≼T"
using assms by cases auto

lemma FAcc_invers:
assumes "E⊢{fd}a..fn::fT"
shows "∃C. E⊢a::Class C ∧ field (prg E,C) fn = Some (fd, fT)"
using assms by cases auto

lemma FAss_invers:
assumes "E⊢{fd}a..fn:=v::T'"
shows "∃T. E⊢{fd}a..fn::T ∧ E⊢v ::T' ∧ prg E⊢T'≼T"
using assms by cases auto

lemma Call_invers:
assumes "E⊢{C}a..mn({pTs'}ps)::rT"
shows "∃pTs md.
E⊢a::Class C ∧ E⊢ps[::]pTs ∧ max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}"
using assms by cases auto

lemma Nil_invers:
assumes "E⊢[] [::] Ts"
shows "Ts = []"
using assms by cases auto

lemma Cons_invers:
assumes "E⊢e#es[::]Ts"
shows "∃T Ts'. Ts = T#Ts' ∧ E ⊢e::T ∧ E ⊢es[::]Ts'"
using assms by cases auto

lemma Expr_invers:
assumes "E⊢Expr e√"
shows "∃ T. E⊢e::T"
using assms by cases auto

lemma Comp_invers:
assumes "E⊢s1;; s2√"
shows "E⊢s1√ ∧ E⊢s2√"
using assms by cases auto

lemma Cond_invers:
assumes "E⊢If(e) s1 Else s2√"
shows "E⊢e::PrimT Boolean ∧ E⊢s1√ ∧ E⊢s2√"
using assms by cases auto

lemma Loop_invers:
assumes "E⊢While(e) s√"
shows "E⊢e::PrimT Boolean ∧ E⊢s√"
using assms by cases auto

(**********************************************************************)

declare split_paired_All [simp del]
declare split_paired_Ex [simp del]

method ty_case_simp = ((erule ty_exprs.cases ty_expr.cases; simp)+)[]
method strip_case_simp = (intro strip, ty_case_simp)

(* Uniqueness of types property *)

lemma uniqueness_of_types: "
(∀ (E::'a prog × (vname ⇒ ty option)) T1 T2.
E⊢e :: T1 ⟶ E⊢e :: T2 ⟶ T1 = T2) ∧
(∀ (E::'a prog × (vname ⇒ ty option)) Ts1 Ts2.
E⊢es [::] Ts1 ⟶ E⊢es [::] Ts2 ⟶ Ts1 = Ts2)"
apply (rule compat_expr_expr_list.induct)
(* NewC *)
apply strip_case_simp

(* Cast *)
apply strip_case_simp

(* Lit *)
apply strip_case_simp

(* BinOp *)
apply (intro strip)
apply (rename_tac binop x2 x3 E T1 T2, case_tac binop)
(* Eq *)
apply ty_case_simp
apply ty_case_simp

(* LAcc *)
apply (strip_case_simp)

(* LAss *)
apply (strip_case_simp)

(* FAcc *)
apply (intro strip)
apply (drule FAcc_invers)+
apply fastforce

(* FAss *)
apply (intro strip)
apply (drule FAss_invers)+
apply (elim conjE exE)
apply (drule FAcc_invers)+
apply fastforce

(* Call *)
apply (intro strip)
apply (drule Call_invers)+
apply fastforce

(* expression lists *)
apply (strip_case_simp)

apply (strip_case_simp)
done

lemma uniqueness_of_types_expr [rule_format (no_asm)]: "
(∀E T1 T2. E⊢e :: T1 ⟶ E⊢e :: T2 ⟶ T1 = T2)"
by (rule uniqueness_of_types [THEN conjunct1])

lemma uniqueness_of_types_exprs [rule_format (no_asm)]: "
(∀E Ts1 Ts2. E⊢es [::] Ts1 ⟶ E⊢es [::] Ts2 ⟶ Ts1 = Ts2)"
by (rule uniqueness_of_types [THEN conjunct2])

definition inferred_tp :: "[java_mb env, expr] ⇒ ty" where
"inferred_tp E e == (SOME T. E⊢e :: T)"

definition inferred_tps :: "[java_mb env, expr list] ⇒ ty list" where
"inferred_tps E es == (SOME Ts. E⊢es [::] Ts)"

(* get inferred type(s) for well-typed term *)
lemma inferred_tp_wt: "E⊢e :: T ⟹ (inferred_tp E e) = T"
by (auto simp: inferred_tp_def intro: uniqueness_of_types_expr)

lemma inferred_tps_wt: "E⊢es [::] Ts ⟹ (inferred_tps E es) = Ts"
by (auto simp: inferred_tps_def intro: uniqueness_of_types_exprs)

end
```