# Theory TypeInf

Up to index of Isabelle/HOL/MicroJava

theory TypeInf
imports WellType
begin

    (*  Title:      HOL/MicroJava/Comp/TypeInf.thy
        ID:         $Id: TypeInf.thy,v 1.4 2005/06/17 14:13:09 haftmann Exp $
        Author:     Martin Strecker
    *)

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

    (**********************************************************************)
    ;

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

    lemma NewC_invers: "E\<turnstile>NewC C::T
      ==> T = Class C ∧ is_class (prg E) C"
    by (erule ty_expr.cases, auto)

    lemma Cast_invers: "E\<turnstile>Cast D e::T
      ==> ∃ C. T = Class D ∧ E\<turnstile>e::C ∧ is_class (prg E) D ∧ prg E\<turnstile>C\<preceq>? Class D"
    by (erule ty_expr.cases, auto)

    lemma Lit_invers: "E\<turnstile>Lit x::T
      ==> typeof (λv. None) x = Some T"
    by (erule ty_expr.cases, auto)

    lemma LAcc_invers: "E\<turnstile>LAcc v::T
      ==> localT E v = Some T ∧ is_type (prg E) T"
    by (erule ty_expr.cases, auto)

    lemma BinOp_invers: "E\<turnstile>BinOp bop e1 e2::T'
      ==> ∃ T. E\<turnstile>e1::T ∧ E\<turnstile>e2::T ∧
                (if bop = Eq then T' = PrimT Boolean
                            else T' = T ∧ T = PrimT Integer)"
    by (erule ty_expr.cases, auto)

    lemma LAss_invers: "E\<turnstile>v::=e::T'
      ==> ∃ T. v ~= This ∧ E\<turnstile>LAcc v::T ∧ E\<turnstile>e::T' ∧ prg E\<turnstile>T'\<preceq>T"
    by (erule ty_expr.cases, auto)

    lemma FAcc_invers: "E\<turnstile>{fd}a..fn::fT
      ==> ∃ C. E\<turnstile>a::Class C ∧ field (prg E,C) fn = Some (fd,fT)"
    by (erule ty_expr.cases, auto)

    lemma FAss_invers: "E\<turnstile>{fd}a..fn:=v::T'
    ==> ∃ T. E\<turnstile>{fd}a..fn::T ∧ E\<turnstile>v ::T' ∧ prg E\<turnstile>T'\<preceq>T"
    by (erule ty_expr.cases, auto)

    lemma Call_invers: "E\<turnstile>{C}a..mn({pTs'}ps)::rT
      ==> ∃ pTs md.
      E\<turnstile>a::Class C ∧ E\<turnstile>ps[::]pTs ∧ max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}"
    by (erule ty_expr.cases, auto)

    lemma Nil_invers: "E\<turnstile>[] [::] Ts ==> Ts = []"
    by (erule ty_exprs.cases, auto)

    lemma Cons_invers: "E\<turnstile>e#es[::]Ts ==>
      ∃ T Ts'. Ts = T#Ts' ∧ E \<turnstile>e::T ∧ E \<turnstile>es[::]Ts'"
    by (erule ty_exprs.cases, auto)

    lemma Expr_invers: "E\<turnstile>Expr e\<surd> ==> ∃ T. E\<turnstile>e::T"
    by (erule wt_stmt.cases, auto)

    lemma Comp_invers: "E\<turnstile>s1;; s2\<surd> ==> E\<turnstile>s1\<surd> ∧ E\<turnstile>s2\<surd>"
    by (erule wt_stmt.cases, auto)

    lemma Cond_invers: "E\<turnstile>If(e) s1 Else s2\<surd>
      ==> E\<turnstile>e::PrimT Boolean ∧ E\<turnstile>s1\<surd> ∧ E\<turnstile>s2\<surd>"
    by (erule wt_stmt.cases, auto)

    lemma Loop_invers: "E\<turnstile>While(e) s\<surd>
      ==> E\<turnstile>e::PrimT Boolean ∧ E\<turnstile>s\<surd>"
    by (erule wt_stmt.cases, auto)

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

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

    (* Uniqueness of types property *)

    lemma uniqueness_of_types: "
      (∀ (E::'a prog × (vname => ty option)) T1 T2.
      E\<turnstile>e :: T1 --> E\<turnstile>e :: T2 --> T1 = T2) ∧
      (∀ (E::'a prog × (vname => ty option)) Ts1 Ts2.
      E\<turnstile>es [::] Ts1 --> E\<turnstile>es [::] Ts2 --> Ts1 = Ts2)"
    apply (rule expr.induct)

    (* NewC *)
    apply (intro strip)
    apply (erule ty_expr.cases) apply simp+
    apply (erule ty_expr.cases) apply simp+

    (* Cast *)
    apply (intro strip)
    apply (erule ty_expr.cases) apply simp+
    apply (erule ty_expr.cases) apply simp+

    (* Lit *)
    apply (intro strip)
    apply (erule ty_expr.cases) apply simp+
    apply (erule ty_expr.cases) apply simp+

    (* BinOp *)
    apply (intro strip)
    apply (case_tac binop)
    (* Eq *)
    apply (erule ty_expr.cases) apply simp+
    apply (erule ty_expr.cases) apply simp+
    (* Add *)
    apply (erule ty_expr.cases) apply simp+
    apply (erule ty_expr.cases) apply simp+

    (* LAcc *)
    apply (intro strip)
    apply (erule ty_expr.cases) apply simp+
    apply (erule ty_expr.cases) apply simp+

    (* LAss *)
    apply (intro strip)
    apply (erule ty_expr.cases) apply simp+
    apply (erule ty_expr.cases) apply simp+

    (* FAcc *)
    apply (intro strip)
    apply (drule FAcc_invers)+ apply (erule exE)+
      apply (subgoal_tac "C = Ca", simp) apply blast

    (* FAss *)
    apply (intro strip)
    apply (drule FAss_invers)+ apply (erule exE)+ apply (erule conjE)+
    apply (drule FAcc_invers)+ apply (erule exE)+ apply blast

    (* Call *)
    apply (intro strip)
    apply (drule Call_invers)+ apply (erule exE)+ apply (erule conjE)+
    apply (subgoal_tac "pTs = pTsa", simp) apply blast

    (* expression lists *)
    apply (intro strip)
    apply (erule ty_exprs.cases)+ apply simp+

    apply (intro strip)
    apply (erule ty_exprs.cases, simp)
    apply (erule ty_exprs.cases, simp)
    apply (subgoal_tac "e = ea", simp) apply simp
    done

    lemma uniqueness_of_types_expr [rule_format (no_asm)]: "
      (∀ E T1 T2. E\<turnstile>e :: T1 --> E\<turnstile>e :: T2 --> T1 = T2)"
    by (rule uniqueness_of_types [THEN conjunct1])

    lemma uniqueness_of_types_exprs [rule_format (no_asm)]: "
      (∀ E Ts1 Ts2. E\<turnstile>es [::] Ts1 --> E\<turnstile>es [::] Ts2 --> Ts1 = Ts2)"
    by (rule uniqueness_of_types [THEN conjunct2])

    constdefs
      inferred_tp  :: "[java_mb env, expr] => ty"
      "inferred_tp E e == (SOME T. E\<turnstile>e :: T)"
      inferred_tps :: "[java_mb env, expr list] => ty list"
      "inferred_tps E es == (SOME Ts. E\<turnstile>es [::] Ts)"

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

    lemma inferred_tps_wt: "E\<turnstile>es [::] Ts ==> (inferred_tps E es) = Ts"
    by (auto simp: inferred_tps_def intro: uniqueness_of_types_exprs)

    end

lemma NewC_invers:

      E |- NewC C :: T ==> T = Class C ∧ is_class (fst E) C

lemma Cast_invers:

      E |- Cast D e :: T
      ==> ∃C. T = Class D ∧ E |- e :: C ∧ is_class (fst E) D ∧ fst E |- C <=? Class D

lemma Lit_invers:

      E |- Lit x :: T ==> typeof empty x = Some T

lemma LAcc_invers:

      E |- LAcc v :: T ==> snd E v = Some T ∧ is_type (fst E) T

lemma BinOp_invers:

      E |- BinOp bop e1.0 e2.0 :: T'
      ==> ∃T. E |- e1.0 :: T ∧
              E |- e2.0 :: T ∧
              (if bop = Eq then T' = PrimT Boolean else T' = T ∧ T = PrimT Integer)

lemma LAss_invers:

      E |- v::=e :: T'
      ==> ∃T. v ≠ This ∧ E |- LAcc v :: T ∧ E |- e :: T' ∧ fst E |- T' <= T

lemma FAcc_invers:

      E |- {fd}a..fn :: fT
      ==> ∃C. E |- a :: Class C ∧ field (fst E, C) fn = Some (fd, fT)

lemma FAss_invers:

      E |- {fd}a..fn:=v :: T'
      ==> ∃T. E |- {fd}a..fn :: T ∧ E |- v :: T' ∧ fst E |- T' <= T

lemma Call_invers:

      E |- {C}a..mn( {pTs'}ps) :: rT
      ==> ∃pTs md.
             E |- a :: Class C ∧
             E |- ps [::] pTs ∧ max_spec (fst E) C (mn, pTs) = {((md, rT), pTs')}

lemma Nil_invers:

      E |- [] [::] Ts ==> Ts = []

lemma Cons_invers:

      E |- e # es [::] Ts ==> ∃T Ts'. Ts = T # Ts' ∧ E |- e :: T ∧ E |- es [::] Ts'

lemma Expr_invers:

      E |- Expr e [ok] ==> ∃T. E |- e :: T

lemma Comp_invers:

      E |- s1.0;; s2.0 [ok] ==> E |- s1.0 [ok] ∧ E |- s2.0 [ok]

lemma Cond_invers:

      E |- If (e) s1.0 Else s2.0 [ok]
      ==> E |- e :: PrimT Boolean ∧ E |- s1.0 [ok] ∧ E |- s2.0 [ok]

lemma Loop_invers:

      E |- While (e) s [ok] ==> E |- e :: PrimT Boolean ∧ E |- s [ok]

lemma uniqueness_of_types:

      (∀E T1 T2. E |- e :: T1 --> E |- e :: T2 --> T1 = T2) ∧
      (∀E Ts1 Ts2. E |- es [::] Ts1 --> E |- es [::] Ts2 --> Ts1 = Ts2)

lemma uniqueness_of_types_expr:

      [| E |- e :: T1.0; E |- e :: T2.0 |] ==> T1.0 = T2.0

lemma uniqueness_of_types_exprs:

      [| E |- es [::] Ts1.0; E |- es [::] Ts2.0 |] ==> Ts1.0 = Ts2.0

lemma inferred_tp_wt:

      E |- e :: T ==> inferred_tp E e = T

lemma inferred_tps_wt:

      E |- es [::] Ts ==> inferred_tps E es = Ts