Theory Typing

(*<*)
theory Typing
  imports  RCLogic WellformedL
begin
  (*>*)

chapter ‹Type System›

text ‹The MiniSail type system. We define subtyping judgement first and then typing judgement
for the term forms›

section ‹Subtyping›

text ‹ Subtyping is defined on top of refinement constraint logic (RCL). 
A subtyping check is converted into an RCL validity check. ›

inductive subtype :: "Θ ⇒ ℬ ⇒ Γ ⇒ τ ⇒ τ ⇒ bool"  (‹_ ; _ ; _  ⊢ _ ≲ _› [50, 50, 50] 50) where
  subtype_baseI: "⟦  
   atom x ♯ (Θ, ℬ, Γ, z,c,z',c') ; 
   Θ; ℬ; Γ ⊢⇩_w⇩_f  ⦃ z : b | c ⦄;  
   Θ; ℬ; Γ ⊢⇩_w⇩_f  ⦃ z' : b | c' ⦄;                    
   Θ; ℬ ; (x,b, c[z::=[x]⇧^v]⇩_v) #⇩_Γ Γ ⊨ c'[z'::=[x]⇧^v]⇩_v  
⟧ ⟹  
   Θ; ℬ; Γ ⊢  ⦃ z : b | c ⦄ ≲  ⦃ z' : b | c' ⦄"

equivariance subtype
nominal_inductive subtype 
  avoids subtype_baseI: x
proof(goal_cases)
  case (1 Θ ℬ Γ z b c z' c' x)
  then show ?case using  fresh_star_def 1 by force
next
  case (2 Θ ℬ Γ z b c z' c' x)
  then show ?case by auto
qed

inductive_cases subtype_elims: 
  "Θ; ℬ; Γ ⊢ ⦃ z : b | c ⦄ ≲  ⦃ z' : b | c' ⦄"
  "Θ; ℬ; Γ ⊢ τ⇩₁ ≲  τ⇩₂"

section ‹Literals›

text ‹The type synthesised has the constraint that z equates to the literal›

inductive infer_l  :: "l ⇒ τ ⇒ bool" (‹ ⊢ _ ⇒ _› [50, 50] 50) where
  infer_trueI:   " ⊢ L_true  ⇒ ⦃ z : B_bool | [[z]⇧^v]⇧^c⇧^e ==  [[L_true]⇧^v]⇧^c⇧^e ⦄"
| infer_falseI: " ⊢ L_false ⇒ ⦃ z : B_bool | [[z]⇧^v]⇧^c⇧^e == [[L_false]⇧^v]⇧^c⇧^e ⦄"
| infer_natI:   " ⊢ L_num n ⇒ ⦃ z : B_int  | [[z]⇧^v]⇧^c⇧^e == [[L_num n]⇧^v]⇧^c⇧^e ⦄"
| infer_unitI:  " ⊢ L_unit  ⇒ ⦃ z : B_unit | [[z]⇧^v]⇧^c⇧^e == [[L_unit]⇧^v]⇧^c⇧^e ⦄"
| infer_bitvecI:  " ⊢ L_bitvec bv ⇒ ⦃ z : B_bitvec | [[z]⇧^v]⇧^c⇧^e ==  [[L_bitvec bv]⇧^v]⇧^c⇧^e ⦄"

nominal_inductive infer_l  .
equivariance infer_l 

inductive_cases infer_l_elims[elim!]:
  "⊢ L_true ⇒ τ"
  "⊢ L_false ⇒ τ"
  "⊢ L_num n ⇒ τ"
  "⊢ L_unit ⇒ τ"
  "⊢ L_bitvec x ⇒ τ"
  "⊢ l ⇒ τ"

lemma infer_l_form2[simp]:
  shows "∃z. ⊢ l ⇒ (⦃ z : base_for_lit l | [[z]⇧^v]⇧^c⇧^e == [[l]⇧^v]⇧^c⇧^e ⦄)"
proof (nominal_induct l rule: l.strong_induct)
  case (L_num x)
  then show ?case using infer_l.intros base_for_lit.simps has_fresh_z by metis
next
  case L_true
  then show ?case using infer_l.intros base_for_lit.simps has_fresh_z by metis
next
  case L_false
  then show ?case using infer_l.intros base_for_lit.simps has_fresh_z by metis
next
  case L_unit
  then show ?case using infer_l.intros base_for_lit.simps has_fresh_z by metis
next
  case (L_bitvec x)
  then show ?case using infer_l.intros base_for_lit.simps has_fresh_z by metis
qed

section ‹Values›

inductive infer_v :: "Θ ⇒ ℬ ⇒ Γ ⇒ v ⇒ τ ⇒ bool" (‹ _ ; _ ; _ ⊢ _ ⇒ _› [50, 50, 50] 50) where

infer_v_varI: "⟦
      Θ; ℬ ⊢⇩_w⇩_f Γ ; 
      Some (b,c) = lookup Γ x; 
      atom z ♯ x ; atom z ♯  (Θ, ℬ, Γ) 
⟧ ⟹ 
      Θ; ℬ; Γ ⊢ [x]⇧^v ⇒ ⦃ z : b | [[z]⇧^v]⇧^c⇧^e == [[x]⇧^v]⇧^c⇧^e ⦄"

| infer_v_litI: "⟦
      Θ; ℬ ⊢⇩_w⇩_f Γ ; 
      ⊢ l ⇒ τ 
⟧ ⟹ 
      Θ; ℬ; Γ ⊢ [l]⇧^v ⇒ τ"

| infer_v_pairI: "⟦ 
      atom z ♯ (v1, v2); atom z ♯  (Θ, ℬ, Γ) ;
      Θ; ℬ; Γ ⊢ (v1::v) ⇒ t1 ; 
      Θ; ℬ ;  Γ ⊢ (v2::v) ⇒ t2
⟧ ⟹ 
      Θ; ℬ; Γ ⊢ V_pair v1 v2 ⇒ (⦃ z : B_pair (b_of t1) (b_of t2)  | [[z]⇧^v]⇧^c⇧^e == [[v1,v2]⇧^v]⇧^c⇧^e ⦄) "

| infer_v_consI: "⟦ 
      AF_typedef s dclist ∈ set Θ;
      (dc, tc) ∈ set dclist ; 
      Θ;  ℬ; Γ ⊢ v ⇒ tv ; 
      Θ; ℬ; Γ ⊢ tv ≲ tc ;
      atom z ♯ v ;  atom z ♯ (Θ, ℬ, Γ) 
⟧ ⟹ 
      Θ;  ℬ; Γ  ⊢ V_cons s dc v ⇒ (⦃ z : B_id s |  [[z]⇧^v]⇧^c⇧^e == [ V_cons s dc v ]⇧^c⇧^e ⦄)"

| infer_v_conspI: "⟦ 
      AF_typedef_poly s bv dclist ∈ set Θ;
      (dc, tc) ∈ set dclist ; 
      Θ; ℬ; Γ ⊢ v ⇒ tv; 
      Θ; ℬ; Γ ⊢ tv ≲ tc[bv::=b]⇩_τ⇩_b ;
      atom z ♯ (Θ, ℬ, Γ, v, b);
      atom bv ♯ (Θ, ℬ, Γ, v, b);
      Θ; ℬ ⊢⇩_w⇩_f b
⟧ ⟹ 
      Θ; ℬ; Γ ⊢ V_consp s dc b v ⇒ (⦃ z : B_app s b |  [[z]⇧^v]⇧^c⇧^e == (CE_val (V_consp s dc b v)) ⦄)"

equivariance infer_v
nominal_inductive infer_v
  avoids infer_v_conspI: bv and z | infer_v_varI: z | infer_v_pairI: z | infer_v_consI:  z 
proof(goal_cases)
  case (1 Θ ℬ Γ b c x z)
  hence "atom z ♯ ⦃ z : b  | [ [ z ]⇧^v ]⇧^c⇧^e  ==  [ [ x ]⇧^v ]⇧^c⇧^e  ⦄" using τ.fresh by simp
  then show ?case unfolding fresh_star_def using 1 by simp
next
  case (2 Θ ℬ Γ b c x z)
  then show ?case by auto
next
  case (3 z v1 v2 Θ ℬ Γ t1 t2)
  hence "atom z ♯ ⦃ z : [ b_of t1 , b_of t2 ]⇧^b  | [ [ z ]⇧^v ]⇧^c⇧^e  ==  [ [ v1 , v2 ]⇧^v ]⇧^c⇧^e  ⦄" using τ.fresh by simp
  then show ?case unfolding fresh_star_def using 3 by simp
next
  case (4 z v1 v2 Θ ℬ Γ t1 t2)
  then show ?case by auto
next
  case (5 s dclist Θ dc tc ℬ Γ v tv z)
  hence "atom z ♯ ⦃ z : B_id s  | [ [ z ]⇧^v ]⇧^c⇧^e  ==  [ V_cons s dc v ]⇧^c⇧^e  ⦄" using τ.fresh b.fresh pure_fresh by auto
  moreover have "atom z ♯ V_cons s dc v" using v.fresh 5 using v.fresh fresh_prodN pure_fresh  by metis
  then show ?case unfolding fresh_star_def using 5 by simp
next
  case (6 s dclist Θ dc tc ℬ Γ v tv z)
  then show ?case by auto
next
  case (7 s bv dclist Θ dc tc ℬ Γ v tv b z)
  hence "atom bv ♯ V_consp s dc b v" using v.fresh fresh_prodN pure_fresh by metis
  moreover then have "atom bv ♯ ⦃ z : B_id s  | [ [ z ]⇧^v ]⇧^c⇧^e  ==  [ V_consp s dc b v ]⇧^c⇧^e  ⦄" 
    using τ.fresh ce.fresh v.fresh by auto
  moreover have "atom z ♯ V_consp s dc b v" using v.fresh fresh_prodN pure_fresh 7 by metis
  moreover then have "atom z ♯ ⦃ z : B_id s  | [ [ z ]⇧^v ]⇧^c⇧^e  ==  [ V_consp s dc b v ]⇧^c⇧^e  ⦄" 
    using τ.fresh ce.fresh v.fresh by auto
  ultimately show ?case using fresh_star_def 7 by force
next
  case (8 s bv dclist Θ dc tc ℬ Γ v tv b z)
  then show ?case by auto
qed

inductive_cases infer_v_elims[elim!]:
  "Θ; ℬ; Γ ⊢ V_var x ⇒ τ"
  "Θ; ℬ; Γ ⊢ V_lit l ⇒ τ"
  "Θ; ℬ; Γ ⊢ V_pair v1 v2 ⇒ τ"
  "Θ; ℬ; Γ ⊢ V_cons s dc v ⇒ τ"
  "Θ; ℬ; Γ ⊢ V_pair v1 v2 ⇒ (⦃ z : b |  c  ⦄) "
  "Θ; ℬ; Γ ⊢ V_pair v1 v2 ⇒ (⦃ z : [ b1 , b2 ]⇧^b |  [[z]⇧^v]⇧^c⇧^e == [[v1,v2]⇧^v]⇧^c⇧^e ⦄) "
  "Θ; ℬ; Γ ⊢ V_consp s dc b v  ⇒ τ "

inductive check_v :: "Θ ⇒ ℬ ⇒ Γ ⇒ v ⇒ τ ⇒ bool"  (‹_ ; _ ; _  ⊢ _ ⇐ _› [50, 50, 50] 50) where
  check_v_subtypeI:  "⟦  Θ; ℬ; Γ ⊢ τ1 ≲ τ2; Θ; ℬ; Γ ⊢ v ⇒ τ1 ⟧ ⟹ Θ; ℬ ;  Γ ⊢  v ⇐ τ2"
equivariance check_v
nominal_inductive check_v  .

inductive_cases check_v_elims[elim!]:
  "Θ; ℬ ; Γ ⊢ v ⇐ τ"

section ‹Expressions›

text ‹ Type synthesis for expressions ›

inductive infer_e :: "Θ ⇒ Φ ⇒ ℬ ⇒ Γ ⇒ Δ ⇒ e ⇒ τ ⇒ bool"  (‹_ ; _ ; _ ; _ ; _  ⊢ _ ⇒ _› [50, 50, 50,50] 50) where

infer_e_valI:  "⟦
         (Θ; ℬ; Γ ⊢⇩_w⇩_f Δ) ; 
         (Θ ⊢⇩_w⇩_f (Φ::Φ)) ; 
         (Θ; ℬ; Γ ⊢ v ⇒ τ) ⟧ ⟹ 
         Θ; Φ; ℬ; Γ; Δ ⊢ (AE_val v) ⇒ τ"

| infer_e_plusI: "⟦ 
        Θ; ℬ; Γ ⊢⇩_w⇩_f Δ ;
        Θ ⊢⇩_w⇩_f (Φ::Φ) ; 
        Θ; ℬ; Γ ⊢ v1 ⇒ ⦃ z1 : B_int | c1 ⦄ ; 
        Θ; ℬ; Γ ⊢  v2 ⇒ ⦃ z2 : B_int | c2 ⦄;
        atom z3 ♯ (AE_op Plus v1 v2); atom z3 ♯ Γ ⟧ ⟹ 
        Θ; Φ; ℬ; Γ; Δ ⊢ AE_op Plus v1 v2 ⇒ ⦃ z3 : B_int | [[z3]⇧^v]⇧^c⇧^e == (CE_op Plus [v1]⇧^c⇧^e [v2]⇧^c⇧^e) ⦄"

| infer_e_leqI: "⟦ 
        Θ; ℬ; Γ ⊢⇩_w⇩_f Δ; 
        Θ ⊢⇩_w⇩_f (Φ::Φ) ; 
        Θ; ℬ; Γ ⊢ v1 ⇒ ⦃ z1 : B_int | c1 ⦄ ; 
        Θ; ℬ; Γ ⊢ v2 ⇒ ⦃ z2 : B_int | c2 ⦄;
        atom z3 ♯ (AE_op LEq v1 v2); atom z3 ♯ Γ  
⟧ ⟹ 
        Θ; Φ; ℬ; Γ; Δ ⊢ AE_op LEq v1 v2 ⇒  ⦃ z3 : B_bool | [[z3]⇧^v]⇧^c⇧^e == (CE_op LEq [v1]⇧^c⇧^e [v2]⇧^c⇧^e) ⦄"

| infer_e_eqI: "⟦ 
        Θ; ℬ; Γ ⊢⇩_w⇩_f Δ; 
        Θ ⊢⇩_w⇩_f (Φ::Φ) ; 
        Θ; ℬ; Γ ⊢ v1 ⇒ ⦃ z1 : b | c1 ⦄ ; 
        Θ; ℬ; Γ ⊢ v2 ⇒ ⦃ z2 : b | c2 ⦄;     
        atom z3 ♯ (AE_op Eq v1 v2); atom z3 ♯ Γ  ;
        b ∈ { B_bool, B_int, B_unit }
⟧ ⟹ 
        Θ; Φ; ℬ; Γ; Δ ⊢ AE_op Eq v1 v2 ⇒  ⦃ z3 : B_bool | [[z3]⇧^v]⇧^c⇧^e == (CE_op Eq [v1]⇧^c⇧^e [v2]⇧^c⇧^e) ⦄"

| infer_e_appI: "⟦ 
        Θ; ℬ; Γ ⊢⇩_w⇩_f Δ ;
        Θ ⊢⇩_w⇩_f (Φ::Φ) ; 
        Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c τ' s'))) = lookup_fun Φ f;        
        Θ; ℬ; Γ ⊢ v ⇐ ⦃  x : b | c ⦄; 
        atom x ♯ (Θ, Φ, ℬ, Γ, Δ,v , τ);
        τ'[x::=v]⇩_v = τ 
⟧ ⟹
        Θ; Φ; ℬ; Γ; Δ ⊢ AE_app f v ⇒ τ"

| infer_e_appPI: "⟦ 
        Θ; ℬ; Γ ⊢⇩_w⇩_f Δ ;
        Θ ⊢⇩_w⇩_f (Φ::Φ) ; 
        Θ; ℬ ⊢⇩_w⇩_f b' ; 
        Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c τ' s'))) = lookup_fun Φ f;       
        Θ; ℬ; Γ ⊢ v ⇐ ⦃  x : b[bv::=b']⇩_b | c[bv::=b']⇩_b ⦄; atom x ♯ Γ;
        (τ'[bv::=b']⇩_b[x::=v]⇩_v) = τ ;
        atom bv ♯ (Θ, Φ, ℬ, Γ, Δ, b', v, τ)
⟧ ⟹
        Θ; Φ; ℬ; Γ; Δ ⊢ AE_appP f b' v ⇒ τ"

| infer_e_fstI:  "⟦ 
        Θ; ℬ; Γ ⊢⇩_w⇩_f Δ ; 
        Θ ⊢⇩_w⇩_f (Φ::Φ) ; 
        Θ; ℬ; Γ ⊢ v ⇒ ⦃ z' : [b1,b2]⇧^b | c ⦄;
        atom z ♯ AE_fst v ; atom z ♯ Γ ⟧ ⟹ 
        Θ; Φ; ℬ; Γ; Δ ⊢ AE_fst v ⇒ ⦃ z : b1 | [[z]⇧^v]⇧^c⇧^e == ((CE_fst [v]⇧^c⇧^e)) ⦄"

| infer_e_sndI: "⟦ 
        Θ; ℬ; Γ ⊢⇩_w⇩_f Δ ; 
        Θ ⊢⇩_w⇩_f (Φ::Φ) ; 
        Θ; ℬ; Γ ⊢ v ⇒ ⦃ z' : [ b1, b2]⇧^b | c ⦄;
        atom z ♯ AE_snd v ; atom z ♯ Γ ⟧ ⟹  
        Θ; Φ; ℬ; Γ; Δ ⊢ AE_snd v ⇒ ⦃ z : b2 | [[z]⇧^v]⇧^c⇧^e == ((CE_snd [v]⇧^c⇧^e))  ⦄"

| infer_e_lenI: "⟦ 
        Θ; ℬ; Γ ⊢⇩_w⇩_f Δ ; 
        Θ ⊢⇩_w⇩_f (Φ::Φ) ; 
        Θ; ℬ; Γ ⊢ v ⇒ ⦃ z' : B_bitvec | c ⦄;
        atom z ♯ AE_len v ; atom z ♯ Γ⟧ ⟹  
        Θ; Φ; ℬ; Γ; Δ ⊢ AE_len v ⇒ ⦃ z : B_int | [[z]⇧^v]⇧^c⇧^e == ((CE_len [v]⇧^c⇧^e))  ⦄"

| infer_e_mvarI: "⟦  
        Θ; ℬ ⊢⇩_w⇩_f Γ ; 
        Θ ⊢⇩_w⇩_f (Φ::Φ) ; 
        Θ; ℬ; Γ ⊢⇩_w⇩_f Δ;
        (u,τ) ∈ setD Δ ⟧ ⟹ 
        Θ; Φ; ℬ; Γ; Δ ⊢  AE_mvar u ⇒ τ"

| infer_e_concatI: "⟦ 
        Θ; ℬ; Γ ⊢⇩_w⇩_f Δ ;
        Θ ⊢⇩_w⇩_f (Φ::Φ) ; 
        Θ; ℬ; Γ ⊢ v1 ⇒ ⦃ z1 : B_bitvec | c1 ⦄ ; 
        Θ; ℬ; Γ ⊢  v2 ⇒ ⦃ z2 : B_bitvec | c2 ⦄;
        atom z3 ♯ (AE_concat v1 v2); atom z3 ♯ Γ ⟧ ⟹ 
        Θ; Φ; ℬ; Γ; Δ ⊢ AE_concat  v1 v2 ⇒ ⦃ z3 : B_bitvec | [[z3]⇧^v]⇧^c⇧^e == (CE_concat [v1]⇧^c⇧^e [v2]⇧^c⇧^e) ⦄"

| infer_e_splitI: "⟦
        Θ; ℬ; Γ ⊢⇩_w⇩_f Δ ;
        Θ ⊢⇩_w⇩_f (Φ::Φ);
        Θ ; ℬ ; Γ ⊢ v1 ⇒ ⦃ z1 : B_bitvec | c1 ⦄ ;
        Θ ; ℬ ; Γ ⊢ v2 ⇐ ⦃ z2 : B_int | (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var z2))) == (CE_val (V_lit L_true)) AND 
                                         (CE_op LEq (CE_val (V_var z2)) (CE_len (CE_val (v1)))) == (CE_val (V_lit L_true)) ⦄;
        atom z1 ♯ (AE_split v1 v2); atom z1 ♯ Γ;
        atom z2 ♯ (AE_split v1 v2); atom z2 ♯ Γ;
        atom z3 ♯ (AE_split v1 v2); atom z3 ♯ Γ
⟧ ⟹ 
        Θ; Φ; ℬ; Γ; Δ ⊢ (AE_split  v1 v2) ⇒ ⦃ z3 : B_pair B_bitvec B_bitvec  | 
                      ((CE_val v1) == (CE_concat (CE_fst (CE_val (V_var z3))) (CE_snd (CE_val (V_var z3)))))
                  AND (((CE_len (CE_fst (CE_val (V_var z3))))) == (CE_val ( v2))) ⦄"

equivariance infer_e
nominal_inductive infer_e 
  avoids  infer_e_appI: x |infer_e_appPI: bv |  infer_e_splitI: z3 and z1 and z2 
proof(goal_cases)
  case (1 Θ ℬ Γ Δ Φ f x b c τ' s' v τ)
  moreover hence "atom x ♯ [ f  v  ]⇧^e" using fresh_prodN pure_fresh e.fresh by force
  ultimately show ?case unfolding fresh_star_def using fresh_prodN e.fresh pure_fresh by simp
next
  case (2 Θ ℬ Γ Δ Φ f x b c τ' s' v τ)
  then show ?case by auto
next
  case (3 Θ ℬ Γ Δ Φ b' f bv x b c τ' s' v τ)
  moreover hence "atom bv ♯ AE_appP f b' v"  using fresh_prodN pure_fresh e.fresh by force
  ultimately show ?case unfolding fresh_star_def using fresh_prodN  e.fresh pure_fresh fresh_Pair by auto
next
  case (4 Θ ℬ Γ Δ Φ b' f bv x b c τ' s' v τ)
  then show ?case by auto
next
  case (5 Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 z3)
  have "atom z3 ♯ ⦃ z3 : [ B_bitvec , B_bitvec ]⇧^b  | [ v1 ]⇧^c⇧^e  ==  [ [#1[ [ z3 ]⇧^v ]⇧^c⇧^e]⇧^c⇧^e @@ [#2[ [ z3 ]⇧^v ]⇧^c⇧^e]⇧^c⇧^e ]⇧^c⇧^e   AND  [| [#1[ [ z3 ]⇧^v ]⇧^c⇧^e]⇧^c⇧^e |]⇧^c⇧^e  ==  [ v2 ]⇧^c⇧^e   ⦄"
    using τ.fresh by simp
  then show ?case unfolding fresh_star_def fresh_prod7 using wfG_fresh_x2 5 by auto
next
  case (6 Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 z3)
  then show ?case by auto
qed

inductive_cases infer_e_elims[elim!]:
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op Plus v1 v2) ⇒ ⦃ z3 : B_int | [[z3]⇧^v]⇧^c⇧^e == (CE_op Plus [v1]⇧^c⇧^e [v2]⇧^c⇧^e) ⦄"
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op LEq v1 v2) ⇒ ⦃ z3 : B_bool | [[z3]⇧^v]⇧^c⇧^e == (CE_op LEq [v1]⇧^c⇧^e [v2]⇧^c⇧^e) ⦄"
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op Plus v1 v2) ⇒ ⦃ z3 : B_int | c ⦄" 
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op Plus v1 v2) ⇒ ⦃ z3 : b | c ⦄" 
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op LEq v1 v2) ⇒ ⦃ z3 : b | c ⦄" 
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_app f v ) ⇒ τ"     
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_val v) ⇒ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_fst v) ⇒ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_snd v) ⇒ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_mvar u) ⇒ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op Plus v1 v2) ⇒ τ" 
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op LEq v1 v2) ⇒ τ" 
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op LEq v1 v2) ⇒ ⦃ z3 : B_bool | c ⦄" 
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_app f v )  ⇒ τ[x::=v]⇩_τ⇩_v"  
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op opp v1 v2) ⇒  τ" 
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_len v) ⇒ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_len v) ⇒ ⦃ z : B_int | [[z]⇧^v]⇧^c⇧^e == ((CE_len [v]⇧^c⇧^e))⦄ "
  "Θ; Φ; ℬ; Γ; Δ ⊢ AE_concat v1 v2 ⇒ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ AE_concat v1 v2 ⇒ (⦃ z : b |  c  ⦄) "
  "Θ; Φ; ℬ; Γ; Δ ⊢ AE_concat v1 v2 ⇒ (⦃ z : B_bitvec |  [[z]⇧^v]⇧^c⇧^e == (CE_concat [v1]⇧^c⇧^e [v1]⇧^c⇧^e) ⦄) "
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_appP f b v )  ⇒ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ AE_split v1 v2 ⇒ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op Eq v1 v2) ⇒ ⦃ z3 : b | c ⦄" 
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op Eq v1 v2) ⇒ ⦃ z3 : B_bool | c ⦄" 
  "Θ; Φ; ℬ; Γ; Δ ⊢ (AE_op Eq v1 v2) ⇒ τ" 
nominal_termination (eqvt)  by lexicographic_order

section ‹Statements›

inductive check_s ::  "Θ ⇒ Φ ⇒ ℬ ⇒ Γ ⇒ Δ ⇒ s ⇒ τ ⇒ bool" (‹ _ ; _ ; _ ; _ ; _  ⊢ _ ⇐ _› [50, 50, 50,50,50] 50) and
  check_branch_s ::  "Θ ⇒ Φ ⇒ ℬ ⇒ Γ ⇒ Δ  ⇒ tyid ⇒ string ⇒ τ ⇒ v ⇒ branch_s ⇒ τ ⇒ bool" (‹ _ ;  _ ; _ ; _ ; _ ; _ ; _ ; _ ; _ ⊢ _ ⇐ _› [50, 50, 50,50,50] 50) and
  check_branch_list ::  "Θ ⇒ Φ ⇒ ℬ ⇒ Γ ⇒ Δ  ⇒ tyid ⇒ (string * τ) list ⇒ v ⇒ branch_list ⇒ τ ⇒ bool" (‹ _ ;  _ ; _ ; _ ; _ ; _ ; _ ; _ ⊢ _ ⇐ _› [50, 50, 50,50,50] 50) where 
  check_valI:  "⟦ 
       Θ; ℬ; Γ ⊢⇩_w⇩_f Δ ;   
       Θ ⊢⇩_w⇩_f Φ ;
       Θ; ℬ; Γ ⊢ v ⇒ τ'; 
       Θ; ℬ; Γ ⊢ τ' ≲ τ ⟧ ⟹ 
       Θ; Φ; ℬ; Γ; Δ ⊢ (AS_val v) ⇐ τ"

| check_letI: "⟦
       atom x ♯ (Θ, Φ, ℬ, Γ, Δ, e, τ);  
       atom z ♯ (x, Θ, Φ, ℬ, Γ, Δ, e, τ, s);  
       Θ; Φ; ℬ; Γ; Δ ⊢ e ⇒ ⦃ z : b | c ⦄ ; 
       Θ; Φ ; ℬ ; ((x,b,c[z::=V_var x]⇩_v)#⇩_ΓΓ) ; Δ ⊢ s ⇐ τ 
⟧ ⟹ 
       Θ; Φ; ℬ; Γ; Δ ⊢ (AS_let x e s) ⇐ τ"

| check_assertI: "⟦
       atom x ♯ (Θ, Φ, ℬ, Γ, Δ, c, τ, s);  
       Θ; Φ ; ℬ ; ((x,B_bool,c)#⇩_ΓΓ) ; Δ ⊢ s ⇐ τ ;
       Θ; ℬ; Γ  ⊨ c;
       Θ; ℬ; Γ ⊢⇩_w⇩_f Δ 
⟧ ⟹ 
       Θ; Φ; ℬ; Γ; Δ ⊢ (AS_assert c s) ⇐ τ"

|check_branch_s_branchI: "⟦ 
       Θ; ℬ; Γ ⊢⇩_w⇩_f Δ ; 
        ⊢⇩_w⇩_f Θ ; 
       Θ; ℬ; Γ ⊢⇩_w⇩_f τ ;
       Θ ; {||} ; GNil ⊢⇩_w⇩_f const;
       atom x ♯ (Θ, Φ, ℬ, Γ, Δ, tid, cons , const, v, τ);
       Θ; Φ; ℬ; ((x,b_of const,  ([v]⇧^c⇧^e == [ V_cons tid cons [x]⇧^v]⇧^c⇧^e ) AND (c_of const x))#⇩_ΓΓ) ; Δ ⊢ s ⇐ τ  
⟧ ⟹ 
       Θ; Φ; ℬ; Γ; Δ ; tid ; cons ; const ; v ⊢ (AS_branch cons x s) ⇐ τ"

|check_branch_list_consI: "⟦ 
       Θ; Φ; ℬ; Γ; Δ; tid; cons; const; v ⊢ cs ⇐ τ ; 
       Θ; Φ; ℬ; Γ; Δ; tid; dclist; v ⊢ css ⇐ τ  
⟧ ⟹ 
       Θ; Φ; ℬ; Γ; Δ ; tid ; (cons,const)#dclist ; v ⊢ AS_cons cs css ⇐ τ"

|check_branch_list_finalI: "⟦ 
       Θ; Φ;ℬ; Γ; Δ; tid ; cons ; const ; v ⊢ cs ⇐ τ  
⟧ ⟹ 
       Θ; Φ; ℬ; Γ; Δ ; tid ; [(cons,const)] ; v ⊢ AS_final cs  ⇐ τ"

| check_ifI: "⟦ 
       atom z ♯ (Θ, Φ, ℬ, Γ, Δ, v , s1 , s2 , τ ); 
       (Θ; ℬ; Γ ⊢ v ⇐ (⦃ z : B_bool | TRUE ⦄)) ; 
       Θ; Φ; ℬ; Γ; Δ ⊢ s1 ⇐ (⦃ z : b_of τ | ([v]⇧^c⇧^e == [[L_true]⇧^v]⇧^c⇧^e) IMP (c_of τ z) ⦄) ;
       Θ; Φ; ℬ; Γ; Δ ⊢ s2 ⇐ (⦃ z : b_of τ | ([v]⇧^c⇧^e == [[L_false]⇧^v]⇧^c⇧^e) IMP (c_of τ z) ⦄) 
⟧ ⟹ 
       Θ; Φ; ℬ; Γ; Δ ⊢ IF v THEN s1 ELSE s2 ⇐ τ"

| check_let2I: "⟦    
       atom x ♯ (Θ, Φ, ℬ, G, Δ, t, s1, τ) ;     
       Θ; Φ ; ℬ ; G; Δ ⊢ s1 ⇐ t; 
       Θ; Φ ; ℬ ; ((x,b_of t,c_of t x)#⇩_ΓG) ; Δ ⊢ s2 ⇐ τ 
⟧ ⟹ 
       Θ; Φ ; ℬ ; G ; Δ ⊢ (LET x : t  = s1 IN s2) ⇐ τ"

| check_varI: "⟦ 
       atom u ♯ (Θ, Φ, ℬ, Γ, Δ, τ', v, τ) ; 
       Θ; ℬ; Γ ⊢  v ⇐ τ'; 
       Θ; Φ; ℬ; Γ ; ((u,τ') #⇩_Δ Δ)  ⊢ s ⇐ τ 
⟧ ⟹ 
       Θ; Φ; ℬ; Γ; Δ ⊢ (VAR u : τ' = v  IN s) ⇐ τ"

| check_assignI: "⟦ 
       Θ ⊢⇩_w⇩_f Φ ;
       Θ; ℬ; Γ ⊢⇩_w⇩_f Δ ; 
       (u,τ) ∈ setD Δ ; 
       Θ; ℬ; Γ ⊢  v ⇐ τ;
       Θ; ℬ; Γ ⊢ (⦃ z : B_unit | TRUE ⦄) ≲ τ'  
⟧ ⟹ 
       Θ; Φ; ℬ; Γ; Δ ⊢  (u ::= v) ⇐ τ'" 

| check_whileI: "⟦ 
        Θ; Φ; ℬ; Γ; Δ ⊢ s1 ⇐ ⦃ z : B_bool | TRUE ⦄; 
        Θ; Φ; ℬ; Γ; Δ ⊢ s2 ⇐ ⦃ z : B_unit | TRUE ⦄;
        Θ; ℬ; Γ ⊢ (⦃ z : B_unit | TRUE ⦄) ≲ τ' 
⟧ ⟹  
        Θ; Φ; ℬ; Γ; Δ ⊢ WHILE s1 DO { s2 } ⇐ τ'"

| check_seqI: "⟦ 
       Θ; Φ; ℬ; Γ; Δ ⊢ s1 ⇐ ⦃ z : B_unit | TRUE ⦄; 
       Θ; Φ; ℬ; Γ; Δ ⊢ s2 ⇐ τ 
⟧ ⟹ 
       Θ; Φ; ℬ; Γ; Δ ⊢ s1 ;; s2 ⇐ τ"

| check_caseI: "⟦ 
      Θ; Φ; ℬ; Γ; Δ; tid ; dclist ; v ⊢  cs ⇐ τ ;  
       (AF_typedef tid dclist ) ∈ set Θ ;                 
       Θ; ℬ; Γ ⊢ v ⇐ ⦃ z : B_id tid | TRUE ⦄;
       ⊢⇩_w⇩_f Θ  
⟧ ⟹
      Θ; Φ; ℬ; Γ; Δ ⊢ AS_match v cs ⇐ τ"

equivariance check_s

text ‹We only need avoidance for cases where a variable is added to a context›
nominal_inductive check_s 
  avoids check_letI: x and z  |  check_branch_s_branchI: x | check_let2I: x  | check_varI: u | check_ifI: z | check_assertI: x
proof(goal_cases)
  case (1 x Θ Φ ℬ Γ Δ e τ z s b c)
  hence "atom x ♯ AS_let x e s" using s_branch_s_branch_list.fresh(2) by auto 
  moreover have "atom z ♯ AS_let x e s" using s_branch_s_branch_list.fresh(2) 1 fresh_prod8 by auto
  then show ?case using fresh_star_def 1 by force
next
  case (3 x Θ Φ ℬ Γ Δ c τ s)
  hence "atom x ♯ AS_assert c s" using fresh_prodN s_branch_s_branch_list.fresh pure_fresh  by auto 
  then show ?case using fresh_star_def 3 by force
next
  case (5 Θ ℬ Γ Δ τ const x Φ tid cons v s)
  hence "atom x ♯ AS_branch cons x s" using fresh_prodN s_branch_s_branch_list.fresh pure_fresh  by auto 
  then show ?case using fresh_star_def 5 by force
next
  case (7 z Θ Φ ℬ Γ Δ v s1 s2 τ)
  hence "atom z ♯ AS_if v s1 s2 " using s_branch_s_branch_list.fresh by auto
  then show ?case using 7 fresh_prodN fresh_star_def by fastforce
next
  case (9 x Θ Φ ℬ G Δ t s1 τ s2)
  hence "atom x ♯ AS_let2 x t s1 s2" using s_branch_s_branch_list.fresh by auto
  thus ?case  using fresh_star_def 9 by force
next
  case (11 u Θ Φ ℬ Γ Δ τ' v τ s)
  hence "atom u ♯ AS_var u τ' v s" using s_branch_s_branch_list.fresh by auto
  then show ?case  using fresh_star_def 11 by force

qed(auto+)

inductive_cases check_s_elims[elim!]:
  "Θ; Φ; ℬ; Γ; Δ ⊢ AS_val v ⇐ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ AS_let x e s ⇐ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ AS_if v s1 s2 ⇐ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ AS_let2 x t s1 s2 ⇐ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ AS_while s1 s2 ⇐ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ AS_var u t v s ⇐ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ AS_seq s1 s2 ⇐ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ AS_assign u v ⇐ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ AS_match v cs ⇐ τ"
  "Θ; Φ; ℬ; Γ; Δ ⊢ AS_assert c s ⇐ τ"

inductive_cases check_branch_s_elims[elim!]:
  "Θ; Φ; ℬ; Γ; Δ; tid ; dclist ; v ⊢ (AS_final cs) ⇐ τ"
  "Θ; Φ; ℬ; Γ; Δ; tid ; dclist ; v ⊢ (AS_cons cs css) ⇐ τ"
  "Θ; Φ; ℬ; Γ; Δ; tid ; cons ; const ; v ⊢ (AS_branch dc x s ) ⇐ τ"

section ‹Programs›

text ‹Type check function bodies›

inductive check_funtyp :: "Θ ⇒ Φ ⇒  ℬ ⇒ fun_typ ⇒ bool" ( ‹ _ ; _ ; _ ⊢ _ › ) where
  check_funtypI: "⟦
  atom x ♯ (Θ, Φ, B , b );
  Θ; Φ ;  B ; ((x,b,c) #⇩_Γ GNil) ; []⇩_Δ ⊢ s ⇐ τ
⟧  ⟹ 
  Θ; Φ ; B ⊢ (AF_fun_typ x b c τ s)"

equivariance check_funtyp
nominal_inductive check_funtyp
  avoids check_funtypI: x
proof(goal_cases)
  case (1 x Θ Φ B b c s τ  )
  hence "atom x ♯ (AF_fun_typ x b c τ s)"  using fun_def.fresh fun_typ_q.fresh fun_typ.fresh by simp
  then show ?case using fresh_star_def 1 fresh_prodN by fastforce
next
  case (2 Θ Φ x b c s τ f)
  then show ?case by auto
qed

inductive check_funtypq :: "Θ ⇒ Φ ⇒ fun_typ_q ⇒ bool"  ( ‹ _ ; _ ⊢ _ › ) where 
  check_fundefq_simpleI: "⟦
  Θ; Φ ; {||} ⊢ (AF_fun_typ x b c t s)
⟧  ⟹ 
  Θ; Φ ⊢ ((AF_fun_typ_none (AF_fun_typ x b c t s)))"

|check_funtypq_polyI: "⟦
  atom bv ♯ (Θ, Φ, (AF_fun_typ x b c t s));
  Θ; Φ; {|bv|} ⊢ (AF_fun_typ x b c t s)
⟧  ⟹ 
  Θ; Φ ⊢ (AF_fun_typ_some bv (AF_fun_typ x b c t s))"

equivariance check_funtypq
nominal_inductive check_funtypq
  avoids check_funtypq_polyI: bv
proof(goal_cases)
  case (1 bv Θ Φ x b c t s )
  hence "atom bv ♯ (AF_fun_typ_some bv (AF_fun_typ x b c t s))"  using fun_def.fresh fun_typ_q.fresh fun_typ.fresh by simp
  thus ?case using fresh_star_def 1 fresh_prodN by fastforce
next
  case (2 bv Θ Φ ft )
  then show ?case by auto
qed

inductive check_fundef :: "Θ ⇒ Φ ⇒ fun_def ⇒ bool" ( ‹ _ ; _ ⊢ _ › ) where
  check_fundefI: "⟦
  Θ; Φ ⊢ ft 
⟧  ⟹ 
  Θ; Φ ⊢ (AF_fundef f ft)"

equivariance check_fundef
nominal_inductive check_fundef .

text ‹Temporarily remove this simproc as it produces untidy eliminations›
declare[[ simproc del: alpha_lst]]

inductive_cases check_funtyp_elims[elim!]:
  "check_funtyp Θ Φ B ft"

inductive_cases check_funtypq_elims[elim!]:
  "check_funtypq Θ Φ (AF_fun_typ_none (AF_fun_typ x b c τ s))"
  "check_funtypq Θ Φ (AF_fun_typ_some bv (AF_fun_typ x b c τ s))"

inductive_cases check_fundef_elims[elim!]:
  "check_fundef Θ Φ (AF_fundef f ftq)"

declare[[ simproc add: alpha_lst]]

nominal_function Δ_of :: "var_def list ⇒ Δ" where
  "Δ_of [] = DNil"
| "Δ_of ((AV_def u t v)#vs) = (u,t) #⇩_Δ  (Δ_of vs)" 
  apply auto
  using  eqvt_def Δ_of_graph_aux_def neq_Nil_conv old.prod.exhaust apply force
  using  eqvt_def Δ_of_graph_aux_def neq_Nil_conv old.prod.exhaust 
  by (metis var_def.strong_exhaust)
nominal_termination (eqvt) by lexicographic_order

inductive check_prog :: "p ⇒ τ ⇒ bool" ( ‹⊢ _ ⇐ _›)  where 
  "⟦
   Θ; Φ; {||}; GNil ; Δ_of 𝒢 ⊢ s ⇐ τ
⟧ ⟹  ⊢ (AP_prog Θ Φ 𝒢 s) ⇐ τ"

inductive_cases check_prog_elims[elim!]:
  "⊢ (AP_prog Θ Φ 𝒢 s) ⇐ τ"

end