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

chapter ‹Type System›

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

section ‹Subtyping›

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

inductive subtype :: "Θ → B → Γ → τ → τ → bool"  (‹_ ; _ ; _ ⊨ _ < _› [50, 50, 50] 50) where
  subtype_baseI: "[
   atom x ♯ (Θ, B, Γ, z,c,z',c') ;
   Θ; B; Γ ⊨_wf { z : b | c };
   Θ; B; Γ ⊨_wf { z' : b | c' };
   Θ; B ; (x,b, c[z::=[x]^v]_v) #_\<Gamma> Γ ⊨ c'[z'::=[x]^v]_v
\<rbrakk> ==>
   Θ; B; Γ ⊨ { z : b | c } < { z' : b | c' }"

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

inductive_cases subtype_elims: 
  "Θ; B; Γ ⊨ { z : b | c } < { z' : b | c' }"
  "Θ; B; Γ ⊨ τ₁ < τ₂"

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]^ce == [[L_true]^v]^ce }"
| infer_falseI: " ⊨ L_false → { z : B_bool | [[z]^v]^ce == [[L_false]^v]^ce }"
| infer_natI:   " ⊨ L_num n → { z : B_int | [[z]^v]^ce == [[L_num n]^v]^ce }"
| infer_unitI:  " ⊨ L_unit → { z : B_unit | [[z]^v]^ce == [[L_unit]^v]^ce }"
| infer_bitvecI:  " ⊨ L_bitvec bv → { z : B_bitvec | [[z]^v]^ce == [[L_bitvec bv]^v]^ce }"

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]^ce == [[l]^v]^ce })"
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 :: "Θ → B → Γ → v → τ → bool" (‹ _ ; _ ; _ ⊨ _ → _› [50, 50, 50] 50) where

infer_v_varI: "[
      Θ; B ⊨_wf Γ ;
      Some (b,c) = lookup Γ x;
      atom z ♯ x ; atom z ♯ (Θ, B, Γ)
\<rbrakk> ==>
      Θ; B; Γ ⊨ [x]^v → { z : b | [[z]^v]^ce == [[x]^v]^ce }"

| infer_v_litI: "[
      Θ; B ⊨_wf Γ ;
      ⊨ l → τ
\<rbrakk> ==>
      Θ; B; Γ ⊨ [l]^v → τ"

| infer_v_pairI: "[
      atom z ♯ (v1, v2); atom z ♯ (Θ, B, Γ) ;
      Θ; B; Γ ⊨ (v1::v) → t1 ;
      Θ; B ; Γ ⊨ (v2::v) → t2
\<rbrakk> ==>
      Θ; B; Γ ⊨ V_pair v1 v2 → ({ z : B_pair (b_of t1) (b_of t2) | [[z]^v]^ce == [[v1,v2]^v]^ce }) "

| infer_v_consI: "[
      AF_typedef s dclist ∈ set Θ;
      (dc, tc) ∈ set dclist ;
      Θ; B; Γ ⊨ v → tv ;
      Θ; B; Γ ⊨ tv < tc ;
      atom z ♯ v ; atom z ♯ (Θ, B, Γ)
\<rbrakk> ==>
      Θ; B; Γ ⊨ V_cons s dc v → ({ z : B_id s | [[z]^v]^ce == [ V_cons s dc v ]^ce })"

| infer_v_conspI: "[
      AF_typedef_poly s bv dclist ∈ set Θ;
      (dc, tc) ∈ set dclist ;
      Θ; B; Γ ⊨ v → tv;
      Θ; B; Γ ⊨ tv < tc[bv::=b]_\<tau>_b ;
      atom z ♯ (Θ, B, Γ, v, b);
      atom bv ♯ (Θ, B, Γ, v, b);
      Θ; B ⊨_wf b
\<rbrakk> ==>
      Θ; B; Γ ⊨ V_consp s dc b v → ({ z : B_app s b | [[z]^v]^ce == (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 Γ b c x z)
  hence "atom z ♯ { z : b | [ [ z ]^v ]^ce == [ [ x ]^v ]^ce }" using τ.fresh by simp
  then show ?case unfolding fresh_star_def using 1 by simp
next
  case (2 Θ B Γ b c x z)
  then show ?case by auto
next
  case (3 z v1 v2 Θ B Γ t1 t2)
  hence "atom z ♯ { z : [ b_of t1 , b_of t2 ]^b | [ [ z ]^v ]^ce == [ [ v1 , v2 ]^v ]^ce }" using τ.fresh by simp
  then show ?case unfolding fresh_star_def using 3 by simp
next
  case (4 z v1 v2 Θ B Γ t1 t2)
  then show ?case by auto
next
  case (5 s dclist Θ dc tc B Γ v tv z)
  hence "atom z ♯ { z : B_id s | [ [ z ]^v ]^ce == [ V_cons s dc v ]^ce }" 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 B Γ v tv z)
  then show ?case by auto
next
  case (7 s bv dclist Θ dc tc B Γ 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 ]^ce == [ V_consp s dc b v ]^ce }" 
    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 ]^ce == [ V_consp s dc b v ]^ce }" 
    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 B Γ v tv b z)
  then show ?case by auto
qed

inductive_cases infer_v_elims[elim!]:
  "Θ; B; Γ ⊨ V_var x → τ"
  "Θ; B; Γ ⊨ V_lit l → τ"
  "Θ; B; Γ ⊨ V_pair v1 v2 → τ"
  "Θ; B; Γ ⊨ V_cons s dc v → τ"
  "Θ; B; Γ ⊨ V_pair v1 v2 → ({ z : b | c }) "
  "Θ; B; Γ ⊨ V_pair v1 v2 → ({ z : [ b1 , b2 ]^b | [[z]^v]^ce == [[v1,v2]^v]^ce }) "
  "Θ; B; Γ ⊨ V_consp s dc b v → τ "

inductive check_v :: "Θ → B → Γ → v → τ → bool"  (‹_ ; _ ; _ ⊨ _ ← _› [50, 50, 50] 50) where
  check_v_subtypeI:  "[ Θ; B; Γ ⊨ τ1 < τ2; Θ; B; Γ ⊨ v → τ1 ] ==> Θ; B ; Γ ⊨ v ← τ2"
equivariance check_v
nominal_inductive check_v  .

inductive_cases check_v_elims[elim!]:
  "Θ; B ; Γ ⊨ v ← τ"

section ‹Expressions›

text ‹ Type synthesis for expressions ›

inductive infer_e :: "Θ → Φ → B → Γ → Δ → e → τ → bool"  (‹_ ; _ ; _ ; _ ; _ ⊨ _ → _› [50, 50, 50,50] 50) where

infer_e_valI:  "[
         (Θ; B; Γ ⊨_wf Δ) ;
         (Θ ⊨_wf (Φ::Φ)) ;
         (Θ; B; Γ ⊨ v → τ) ] ==>
         Θ; Φ; B; Γ; Δ ⊨ (AE_val v) → τ"

| infer_e_plusI: "[
        Θ; B; Γ ⊨_wf Δ ;
        Θ ⊨_wf (Φ::Φ) ;
        Θ; B; Γ ⊨ v1 → { z1 : B_int | c1 } ;
        Θ; B; Γ ⊨ v2 → { z2 : B_int | c2 };
        atom z3 ♯ (AE_op Plus v1 v2); atom z3 ♯ Γ ] ==>
        Θ; Φ; B; Γ; Δ ⊨ AE_op Plus v1 v2 → { z3 : B_int | [[z3]^v]^ce == (CE_op Plus [v1]^ce [v2]^ce) }"

| infer_e_leqI: "[
        Θ; B; Γ ⊨_wf Δ;
        Θ ⊨_wf (Φ::Φ) ;
        Θ; B; Γ ⊨ v1 → { z1 : B_int | c1 } ;
        Θ; B; Γ ⊨ v2 → { z2 : B_int | c2 };
        atom z3 ♯ (AE_op LEq v1 v2); atom z3 ♯ Γ
\<rbrakk> ==>
        Θ; Φ; B; Γ; Δ ⊨ AE_op LEq v1 v2 → { z3 : B_bool | [[z3]^v]^ce == (CE_op LEq [v1]^ce [v2]^ce) }"

| infer_e_eqI: "[
        Θ; B; Γ ⊨_wf Δ;
        Θ ⊨_wf (Φ::Φ) ;
        Θ; B; Γ ⊨ v1 → { z1 : b | c1 } ;
        Θ; B; Γ ⊨ v2 → { z2 : b | c2 };
        atom z3 ♯ (AE_op Eq v1 v2); atom z3 ♯ Γ ;
        b ∈ { B_bool, B_int, B_unit }
\<rbrakk> ==>
        Θ; Φ; B; Γ; Δ ⊨ AE_op Eq v1 v2 → { z3 : B_bool | [[z3]^v]^ce == (CE_op Eq [v1]^ce [v2]^ce) }"

| infer_e_appI: "[
        Θ; B; Γ ⊨_wf Δ ;
        Θ ⊨_wf (Φ::Φ) ;
        Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c τ' s'))) = lookup_fun Φ f;
        Θ; B; Γ ⊨ v ← { x : b | c };
        atom x ♯ (Θ, Φ, B, Γ, Δ,v , τ);
        τ'[x::=v]_v = τ
\<rbrakk> ==>
        Θ; Φ; B; Γ; Δ ⊨ AE_app f v → τ"

| infer_e_appPI: "[
        Θ; B; Γ ⊨_wf Δ ;
        Θ ⊨_wf (Φ::Φ) ;
        Θ; B ⊨_wf b' ;
        Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c τ' s'))) = lookup_fun Φ f;
        Θ; B; Γ ⊨ v ← { x : b[bv::=b']_b | c[bv::=b']_b }; atom x ♯ Γ;
        (τ'[bv::=b']_b[x::=v]_v) = τ ;
        atom bv ♯ (Θ, Φ, B, Γ, Δ, b', v, τ)
\<rbrakk> ==>
        Θ; Φ; B; Γ; Δ ⊨ AE_appP f b' v → τ"

| infer_e_fstI:  "[
        Θ; B; Γ ⊨_wf Δ ;
        Θ ⊨_wf (Φ::Φ) ;
        Θ; B; Γ ⊨ v → { z' : [b1,b2]^b | c };
        atom z ♯ AE_fst v ; atom z ♯ Γ ] ==>
        Θ; Φ; B; Γ; Δ ⊨ AE_fst v → { z : b1 | [[z]^v]^ce == ((CE_fst [v]^ce)) }"

| infer_e_sndI: "[
        Θ; B; Γ ⊨_wf Δ ;
        Θ ⊨_wf (Φ::Φ) ;
        Θ; B; Γ ⊨ v → { z' : [ b1, b2]^b | c };
        atom z ♯ AE_snd v ; atom z ♯ Γ ] ==>
        Θ; Φ; B; Γ; Δ ⊨ AE_snd v → { z : b2 | [[z]^v]^ce == ((CE_snd [v]^ce)) }"

| infer_e_lenI: "[
        Θ; B; Γ ⊨_wf Δ ;
        Θ ⊨_wf (Φ::Φ) ;
        Θ; B; Γ ⊨ v → { z' : B_bitvec | c };
        atom z ♯ AE_len v ; atom z ♯ Γ] ==>
        Θ; Φ; B; Γ; Δ ⊨ AE_len v → { z : B_int | [[z]^v]^ce == ((CE_len [v]^ce)) }"

| infer_e_mvarI: "[
        Θ; B ⊨_wf Γ ;
        Θ ⊨_wf (Φ::Φ) ;
        Θ; B; Γ ⊨_wf Δ;
        (u,τ) ∈ setD Δ ] ==>
        Θ; Φ; B; Γ; Δ ⊨ AE_mvar u → τ"

| infer_e_concatI: "[
        Θ; B; Γ ⊨_wf Δ ;
        Θ ⊨_wf (Φ::Φ) ;
        Θ; B; Γ ⊨ v1 → { z1 : B_bitvec | c1 } ;
        Θ; B; Γ ⊨ v2 → { z2 : B_bitvec | c2 };
        atom z3 ♯ (AE_concat v1 v2); atom z3 ♯ Γ ] ==>
        Θ; Φ; B; Γ; Δ ⊨ AE_concat v1 v2 → { z3 : B_bitvec | [[z3]^v]^ce == (CE_concat [v1]^ce [v2]^ce) }"

| infer_e_splitI: "[
        Θ; B; Γ ⊨_wf Δ ;
        Θ ⊨_wf (Φ::Φ);
        Θ ; B ; Γ ⊨ v1 → { z1 : B_bitvec | c1 } ;
        Θ ; B ; Γ ⊨ 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 ♯ Γ
\<rbrakk> ==>
        Θ; Φ; B; Γ; Δ ⊨ (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 Θ B Γ Δ Φ 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 Θ B Γ Δ Φ f x b c τ' s' v τ)
  then show ?case by auto
next
  case (3 Θ B Γ Δ Φ 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 Γ Δ Φ b' f bv x b c τ' s' v τ)
  then show ?case by auto
next
  case (5 Θ B Γ Δ Φ v1 z1 c1 v2 z2 z3)
  have "atom z3 ♯ { z3 : [ B_bitvec , B_bitvec ]^b | [ v1 ]^ce == [ [#1[ [ z3 ]^v ]^ce]^ce @@ [#2[ [ z3 ]^v ]^ce]^ce ]^ce AND [| [#1[ [ z3 ]^v ]^ce]^ce |]^ce == [ v2 ]^ce }"
    using τ.fresh by simp
  then show ?case unfolding fresh_star_def fresh_prod7 using wfG_fresh_x2 5 by auto
next
  case (6 Θ B Γ Δ Φ v1 z1 c1 v2 z2 z3)
  then show ?case by auto
qed

inductive_cases infer_e_elims[elim!]:
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op Plus v1 v2) → { z3 : B_int | [[z3]^v]^ce == (CE_op Plus [v1]^ce [v2]^ce) }"
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op LEq v1 v2) → { z3 : B_bool | [[z3]^v]^ce == (CE_op LEq [v1]^ce [v2]^ce) }"
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op Plus v1 v2) → { z3 : B_int | c }" 
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op Plus v1 v2) → { z3 : b | c }" 
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op LEq v1 v2) → { z3 : b | c }" 
  "Θ; Φ; B; Γ; Δ ⊨ (AE_app f v ) → τ"     
  "Θ; Φ; B; Γ; Δ ⊨ (AE_val v) → τ"
  "Θ; Φ; B; Γ; Δ ⊨ (AE_fst v) → τ"
  "Θ; Φ; B; Γ; Δ ⊨ (AE_snd v) → τ"
  "Θ; Φ; B; Γ; Δ ⊨ (AE_mvar u) → τ"
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op Plus v1 v2) → τ" 
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op LEq v1 v2) → τ" 
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op LEq v1 v2) → { z3 : B_bool | c }" 
  "Θ; Φ; B; Γ; Δ ⊨ (AE_app f v ) → τ[x::=v]_\<tau>_v"  
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op opp v1 v2) → τ" 
  "Θ; Φ; B; Γ; Δ ⊨ (AE_len v) → τ"
  "Θ; Φ; B; Γ; Δ ⊨ (AE_len v) → { z : B_int | [[z]^v]^ce == ((CE_len [v]^ce))} "
  "Θ; Φ; B; Γ; Δ ⊨ AE_concat v1 v2 → τ"
  "Θ; Φ; B; Γ; Δ ⊨ AE_concat v1 v2 → ({ z : b | c }) "
  "Θ; Φ; B; Γ; Δ ⊨ AE_concat v1 v2 → ({ z : B_bitvec | [[z]^v]^ce == (CE_concat [v1]^ce [v1]^ce) }) "
  "Θ; Φ; B; Γ; Δ ⊨ (AE_appP f b v ) → τ"
  "Θ; Φ; B; Γ; Δ ⊨ AE_split v1 v2 → τ"
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op Eq v1 v2) → { z3 : b | c }" 
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op Eq v1 v2) → { z3 : B_bool | c }" 
  "Θ; Φ; B; Γ; Δ ⊨ (AE_op Eq v1 v2) → τ" 
nominal_termination (eqvt)  by lexicographic_order

section ‹Statements›

inductive check_s ::  "Θ → Φ → B → Γ → Δ → s → τ → bool" (‹ _ ; _ ; _ ; _ ; _ ⊨ _ ← _› [50, 50, 50,50,50] 50) and
  check_branch_s ::  "Θ → Φ → B → Γ → Δ → tyid → string → τ → v → branch_s → τ → bool" (‹ _ ; _ ; _ ; _ ; _ ; _ ; _ ; _ ; _ ⊨ _ ← _› [50, 50, 50,50,50] 50) and
  check_branch_list ::  "Θ → Φ → B → Γ → Δ → tyid → (string * τ) list → v → branch_list → τ → bool" (‹ _ ; _ ; _ ; _ ; _ ; _ ; _ ; _ ⊨ _ ← _› [50, 50, 50,50,50] 50) where 
  check_valI:  "[
       Θ; B; Γ ⊨_wf Δ ;
       Θ ⊨_wf Φ ;
       Θ; B; Γ ⊨ v → τ';
       Θ; B; Γ ⊨ τ' < τ ] ==>
       Θ; Φ; B; Γ; Δ ⊨ (AS_val v) ← τ"

| check_letI: "[
       atom x ♯ (Θ, Φ, B, Γ, Δ, e, τ);
       atom z ♯ (x, Θ, Φ, B, Γ, Δ, e, τ, s);
       Θ; Φ; B; Γ; Δ ⊨ e → { z : b | c } ;
       Θ; Φ ; B ; ((x,b,c[z::=V_var x]_v)#_\<Gamma>Γ) ; Δ ⊨ s ← τ
\<rbrakk> ==>
       Θ; Φ; B; Γ; Δ ⊨ (AS_let x e s) ← τ"

| check_assertI: "[
       atom x ♯ (Θ, Φ, B, Γ, Δ, c, τ, s);
       Θ; Φ ; B ; ((x,B_bool,c)#_\<Gamma>Γ) ; Δ ⊨ s ← τ ;
       Θ; B; Γ ⊨ c;
       Θ; B; Γ ⊨_wf Δ
\<rbrakk> ==>
       Θ; Φ; B; Γ; Δ ⊨ (AS_assert c s) ← τ"

|check_branch_s_branchI: "[
       Θ; B; Γ ⊨_wf Δ ;
        ⊨_wf Θ ;
       Θ; B; Γ ⊨_wf τ ;
       Θ ; {||} ; GNil ⊨_wf const;
       atom x ♯ (Θ, Φ, B, Γ, Δ, tid, cons , const, v, τ);
       Θ; Φ; B; ((x,b_of const, ([v]^ce == [ V_cons tid cons [x]^v]^ce ) AND (c_of const x))#_\<Gamma>Γ) ; Δ ⊨ s ← τ
\<rbrakk> ==>
       Θ; Φ; B; Γ; Δ ; tid ; cons ; const ; v ⊨ (AS_branch cons x s) ← τ"

|check_branch_list_consI: "[
       Θ; Φ; B; Γ; Δ; tid; cons; const; v ⊨ cs ← τ ;
       Θ; Φ; B; Γ; Δ; tid; dclist; v ⊨ css ← τ
\<rbrakk> ==>
       Θ; Φ; B; Γ; Δ ; tid ; (cons,const)#dclist ; v ⊨ AS_cons cs css ← τ"

|check_branch_list_finalI: "[
       Θ; Φ;B; Γ; Δ; tid ; cons ; const ; v ⊨ cs ← τ
\<rbrakk> ==>
       Θ; Φ; B; Γ; Δ ; tid ; [(cons,const)] ; v ⊨ AS_final cs ← τ"

| check_ifI: "[
       atom z ♯ (Θ, Φ, B, Γ, Δ, v , s1 , s2 , τ );
       (Θ; B; Γ ⊨ v ← ({ z : B_bool | TRUE })) ;
       Θ; Φ; B; Γ; Δ ⊨ s1 ← ({ z : b_of τ | ([v]^ce == [[L_true]^v]^ce) IMP (c_of τ z) }) ;
       Θ; Φ; B; Γ; Δ ⊨ s2 ← ({ z : b_of τ | ([v]^ce == [[L_false]^v]^ce) IMP (c_of τ z) })
\<rbrakk> ==>
       Θ; Φ; B; Γ; Δ ⊨ IF v THEN s1 ELSE s2 ← τ"

| check_let2I: "[
       atom x ♯ (Θ, Φ, B, G, Δ, t, s1, τ) ;
       Θ; Φ ; B ; G; Δ ⊨ s1 ← t;
       Θ; Φ ; B ; ((x,b_of t,c_of t x)#_\<Gamma>G) ; Δ ⊨ s2 ← τ
\<rbrakk> ==>
       Θ; Φ ; B ; G ; Δ ⊨ (LET x : t = s1 IN s2) ← τ"

| check_varI: "[
       atom u ♯ (Θ, Φ, B, Γ, Δ, τ', v, τ) ;
       Θ; B; Γ ⊨ v ← τ';
       Θ; Φ; B; Γ ; ((u,τ') #_\<Delta> Δ) ⊨ s ← τ
\<rbrakk> ==>
       Θ; Φ; B; Γ; Δ ⊨ (VAR u : τ' = v IN s) ← τ"

| check_assignI: "[
       Θ ⊨_wf Φ ;
       Θ; B; Γ ⊨_wf Δ ;
       (u,τ) ∈ setD Δ ;
       Θ; B; Γ ⊨ v ← τ;
       Θ; B; Γ ⊨ ({ z : B_unit | TRUE }) < τ'
\<rbrakk> ==>
       Θ; Φ; B; Γ; Δ ⊨ (u ::= v) ← τ'" 

| check_whileI: "[
        Θ; Φ; B; Γ; Δ ⊨ s1 ← { z : B_bool | TRUE };
        Θ; Φ; B; Γ; Δ ⊨ s2 ← { z : B_unit | TRUE };
        Θ; B; Γ ⊨ ({ z : B_unit | TRUE }) < τ'
\<rbrakk> ==>
        Θ; Φ; B; Γ; Δ ⊨ WHILE s1 DO { s2 } ← τ'"

| check_seqI: "[
       Θ; Φ; B; Γ; Δ ⊨ s1 ← { z : B_unit | TRUE };
       Θ; Φ; B; Γ; Δ ⊨ s2 ← τ
\<rbrakk> ==>
       Θ; Φ; B; Γ; Δ ⊨ s1 ;; s2 ← τ"

| check_caseI: "[
      Θ; Φ; B; Γ; Δ; tid ; dclist ; v ⊨ cs ← τ ;
       (AF_typedef tid dclist ) ∈ set Θ ;
       Θ; B; Γ ⊨ v ← { z : B_id tid | TRUE };
       ⊨_wf Θ
\<rbrakk> ==>
      Θ; Φ; B; Γ; Δ ⊨ 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 Θ Φ B Γ Δ 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 Θ Φ B Γ Δ 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 Θ B Γ Δ τ 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 Θ Φ B Γ Δ 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 Θ Φ B 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 Θ Φ B Γ Δ τ' 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!]:
  "Θ; Φ; B; Γ; Δ ⊨ AS_val v ← τ"
  "Θ; Φ; B; Γ; Δ ⊨ AS_let x e s ← τ"
  "Θ; Φ; B; Γ; Δ ⊨ AS_if v s1 s2 ← τ"
  "Θ; Φ; B; Γ; Δ ⊨ AS_let2 x t s1 s2 ← τ"
  "Θ; Φ; B; Γ; Δ ⊨ AS_while s1 s2 ← τ"
  "Θ; Φ; B; Γ; Δ ⊨ AS_var u t v s ← τ"
  "Θ; Φ; B; Γ; Δ ⊨ AS_seq s1 s2 ← τ"
  "Θ; Φ; B; Γ; Δ ⊨ AS_assign u v ← τ"
  "Θ; Φ; B; Γ; Δ ⊨ AS_match v cs ← τ"
  "Θ; Φ; B; Γ; Δ ⊨ AS_assert c s ← τ"

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

section ‹Programs›

text ‹Type check function bodies›

inductive check_funtyp :: "Θ → Φ → B → fun_typ → bool" ( ‹ _ ; _ ; _ ⊨ _ › ) where
  check_funtypI: "[
  atom x ♯ (Θ, Φ, B , b );
  Θ; Φ ; B ; ((x,b,c) #_\<Gamma> GNil) ; []_\<Delta> ⊨ s ← τ
\<rbrakk> ==>
  Θ; Φ ; 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)
\<rbrakk> ==>
  Θ; Φ ⊨ ((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)
\<rbrakk> ==>
  Θ; Φ ⊨ (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
\<rbrakk> ==>
  Θ; Φ ⊨ (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) #_\<Delta> (Δ_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 G ⊨ s ← τ
\<rbrakk> ==> ⊨ (AP_prog Θ Φ G s) ← τ"

inductive_cases check_prog_elims[elim!]:
  "⊨ (AP_prog Θ Φ G s) ← τ"

end