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