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 "Γ, Δ ctxt E : T  U"
  shows   "k. Γk:T1, Δ ctxt (liftL_ctxt E k) : T  U"
using assms by (induct rule: typing_ctxt.induct) (auto simp add: liftL_type)

lemma liftM_ctxt_type:
  assumes "Γ, Δ ctxt E : T  U"
  shows   "Γ, Δk:T1 ctxt (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" "Γ , Δ' ctxt E : U  T1" "Δ = Δ'α:T1"
          "(Γ , Δ' ctxt 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  Γ, Δ ctxt E : U  T1  Δ1 = Δα:T1  Γ, Δβ:U T t[α=β (liftM_ctxt E β)]T : T"
  "Γ, Δ1 C c  Γ, Δ ctxt 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  Γ, Δ ctxt 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) (μ(T1T2) : 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