Theory TypePreservation

subsection‹Type preservation›

theory TypePreservation
imports
    ContextFacts
begin

text‹Shifting lambda variables preserves well-typedness.›
  
lemma liftL_type: 
  "Γ, Δ ⊢⇩T t : T ⟹ ∀k. Γ⟨k:U⟩, Δ ⊢⇩T (liftL_trm t k) : T"
  "Γ, Δ ⊢⇩C c ⟹ ∀k. Γ⟨k:U⟩, Δ ⊢⇩C (liftL_cmd c k)"
  by (induct rule: typing_trm_typing_cmd.inducts) auto

text‹Shifting mu variables preserves well-typedness.›
  
lemma liftM_type: 
  "Γ, Δ ⊢⇩T t : T ⟹ ∀k. Γ, Δ⟨k:U⟩ ⊢⇩T (liftM_trm t k) : T"
  "Γ, Δ ⊢⇩C c ⟹ ∀k. Γ, Δ⟨k:U⟩ ⊢⇩C (liftM_cmd c k)"
  by(induct rule: typing_trm_typing_cmd.inducts) auto
    
lemma dropM_type:
  "Γ , Δ1 ⊢⇩T t : T ⟹ k ∉ fmv_trm t 0 ⟹ (∀x. x<k ⟶ Δ1 x = Δ x) 
    ⟹ (∀x. x>k ⟶ Δ1 x = Δ (x-1)) ⟹ Γ , Δ ⊢⇩T dropM_trm t k : T"
  "Γ , Δ1 ⊢⇩C c ⟹ k ∉ fmv_cmd c 0 ⟹ (∀x. x<k ⟶ Δ1 x = Δ x) 
    ⟹ (∀x. x>k ⟶ Δ1 x = Δ (x-1)) ⟹ Γ , Δ ⊢⇩C dropM_cmd c k"
proof (induct arbitrary: k Δ and k Δ rule: typing_trm_typing_cmd.inducts)
  case (activate Γ Δ T c)
  then show ?case
    apply(erule_tac x = "Suc k" in meta_allE)
    apply(insert fmv_suc(1))
    apply(clarsimp simp add: shift_def)
    done
qed fastforce+

  
text‹Lifting $\lambda$ and $\mu$-variables in contexts preserves contextual typing judgements.›
  
lemma liftL_ctxt_type:
  assumes "Γ, Δ ⊢⇩c⇩t⇩x⇩t E : T ⇐ U"
  shows   "∀k. Γ⟨k:T1⟩, Δ ⊢⇩c⇩t⇩x⇩t (liftL_ctxt E k) : T ⇐ U"
using assms by (induct rule: typing_ctxt.induct) (auto simp add: liftL_type)

lemma liftM_ctxt_type:
  assumes "Γ, Δ ⊢⇩c⇩t⇩x⇩t E : T ⇐ U"
  shows   "Γ, Δ⟨k:T1⟩ ⊢⇩c⇩t⇩x⇩t (liftM_ctxt E k) : T ⇐ U"
using assms by(induct rule: typing_ctxt.induct) (auto simp add: liftM_type)

text‹Substitution lemma for logical substitution.›
  
theorem subst_type:
  "Γ1, Δ ⊢⇩T t : T ⟹ Γ, Δ ⊢⇩T r : T1 ⟹ Γ1 = Γ⟨k:T1⟩ ⟹ Γ, Δ ⊢⇩T t[r/k]⇧T : T"
  "Γ1, Δ ⊢⇩C c ⟹ Γ, Δ ⊢⇩T r : T1 ⟹ Γ1 = Γ⟨k:T1⟩ ⟹ Γ, Δ ⊢⇩C c[r/k]⇧C "
proof(induct arbitrary: Γ k T1 r and Γ k r T1 rule: typing_trm_typing_cmd.inducts)
  case (lambda Γ T1 Δ t T2)
  then show ?case
    by -(rotate_tac 2, drule liftL_type(1), fastforce)
next
  case (activate Γ Δ T c)
  then show ?case
    by -(rotate_tac 2, drule liftM_type(1), fastforce)
qed force+

text‹Substitution lemma for structural substitution. The proof is by induction on the first typing judgement.›
  
lemma struct_subst_command:
  assumes "Γ, Δ ⊢⇩T t : T" "Δ x = T" "Γ , Δ' ⊢⇩c⇩t⇩x⇩t E : U ⇐ T1" "Δ = Δ'⟨α:T1⟩"
          "(Γ , Δ' ⊢⇩c⇩t⇩x⇩t E : U ⇐ T1 ⟹ Δ = Δ'⟨α:T1⟩ ⟹ Γ , Δ'⟨β:U⟩ ⊢⇩T t[α=β (liftM_ctxt E β)]⇧T : T)"
  shows   "Γ,( Δ'⟨β:U⟩) ⊢⇩C (<x> t)[α=β (liftM_ctxt E β)]⇧C"
  using assms apply clarsimp
  apply (rule conjI, force, clarsimp)+
  apply (rule conjI)
   apply (metis liftM_ctxt_type passivate shift_eq typing_ctxt_correct2)
  apply force
  done

theorem struct_subst_type:
  "Γ, Δ1 ⊢⇩T t : T ⟹ Γ, Δ ⊢⇩c⇩t⇩x⇩t E : U ⇐ T1 ⟹ Δ1 = Δ⟨α:T1⟩ ⟹ Γ, Δ⟨β:U⟩ ⊢⇩T t[α=β (liftM_ctxt E β)]⇧T : T"
  "Γ, Δ1 ⊢⇩C c ⟹ Γ, Δ ⊢⇩c⇩t⇩x⇩t E : U ⇐ T1  ⟹ Δ1 = Δ⟨α:T1⟩ ⟹ Γ, Δ⟨β:U⟩ ⊢⇩C c[α=β (liftM_ctxt E β)]⇧C"
proof (induct arbitrary: Δ T1 E U β α and Δ T1 E U β α rule: typing_trm_typing_cmd.inducts)
  case (lambda Γ T1 Δ t T2)
  then show ?case
    by -(drule liftL_ctxt_type, fastforce simp: liftLM_comm_ctxt)
next
  case (activate Γ Δ T c)
  then show ?case
    by -(drule liftM_ctxt_type, fastforce simp: liftMM_comm_ctxt)
next
  case (passivate Γ Δ t T x)
  then show ?case
    using struct_subst_command by force
qed fastforce+

lemma struct_subst_type_command:  "Γ, Δ1 ⊢⇩C c ⟹ Γ, Δ ⊢⇩c⇩t⇩x⇩t E : U ⇐ T1 
    ⟹ Δ1 = Δ⟨α:T1⟩
    ⟹ Γ, Δ⟨β:U⟩ ⊢⇩C c[α=β (liftM_ctxt E β)]⇧C"
using struct_subst_type by force
  

lemma dropM_env:
  "Γ, Δ1 ⊢⇩T t[k=x ◇]⇧T : T ⟹ Δ1 = Δ⟨x:(Δ x)⟩ ⟹ Γ , Δ ⊢⇩T dropM_trm (t[k=x ◇]⇧T) x : T" 
  "Γ, Δ1 ⊢⇩C c[k=x ◇]⇧C ⟹ Δ1 = Δ⟨x:(Δ x)⟩ ⟹ Γ , Δ ⊢⇩C dropM_cmd (c[k=x ◇]⇧C) x"
  by (induct t and c arbitrary: Γ T Δ1 x k Δ and Γ T Δ1 x k Δ) fastforce+
    
theorem type_preservation:
  "Γ, Δ ⊢⇩T t : T ⟹ t ⇢ s ⟹ Γ, Δ ⊢⇩T s : T"
  "Γ, Δ ⊢⇩C c ⟹ c ⇩C⇢ d ⟹ Γ, Δ ⊢⇩C d"
proof(induct arbitrary: s and d rule: typing_trm_typing_cmd.inducts)
  case (app Γ Δ t T1 T2 s s')
  then show ?case
    apply -
    apply (erule redE; clarsimp simp: subst_type(1))
      apply (subgoal_tac "Γ , Δ ⊢⇩T ctxt_subst (◇ ⇧∙ s) (μ(T1→T2) : c) : T2")
       apply (drule typing_ctxt_correct1, clarsimp)
       apply (subgoal_tac "Γ , Δ⟨0:T2⟩ ⊢⇩C c[0=0 (liftM_ctxt (◇ ⇧∙ s) 0)]⇧C")
        apply (clarsimp, rule struct_subst_type_command)
         apply force+
    done
next
  case (passivate Γ Δ t T x)
  then show ?case
    apply clarsimp
    apply (erule redE, clarsimp)
     apply (drule struct_subst_type_command [where β = x])
       apply (fastforce simp: dropM_env(2))+                  
    done
qed (force simp: dropM_type)+

end