Theory Logic
section "Logic"
theory Logic
imports Theory Term_Subst SortConstants Name BetaNormProof EtaNormProof
begin
term proves
abbreviation "inst_ok Θ insts ≡
distinct (map fst insts)
∧ list_all (typ_ok Θ) (map snd insts)
∧ list_all (λ((idn, S), T) . has_sort (osig (sig Θ)) T S) insts"
lemma inst_ok_imp_wf_inst:
"inst_ok Θ insts ⟹ wf_inst Θ (λidn S .the_default (Tv idn S) (lookup (λx. x=(idn, S)) insts))"
by (induction insts) (auto split: if_splits prod.splits)
lemma term_ok'_eta_norm: "term_ok' Σ t ⟹ term_ok' Σ (eta_norm t)"
by (induction t rule: eta_norm.induct)
(auto split: term.splits nat.splits simp add: term_ok'_decr is_dependent_def)
corollary term_ok_eta_norm: "term_ok thy t ⟹ term_ok thy (eta_norm t)"
using wt_term_def typ_of_eta_norm term_ok'_eta_norm by auto
abbreviation "beta_eta_norm t ≡ map_option eta_norm (beta_norm t)"
lemma "beta_eta_norm t = Some t' ⟹ ¬ eta_reducible t'"
using not_eta_reducible_eta_norm by auto
lemma term_ok_beta_eta_norm: "term_ok thy t ⟹ beta_eta_norm t = Some t' ⟹ term_ok thy t'"
using term_ok_eta_norm term_ok_beta_norm by blast
lemma typ_of_beta_eta_norm:
"typ_of t = Some T ⟹ beta_eta_norm t = Some t' ⟹ typ_of t' = Some T"
using beta_norm_imp_beta_reds beta_star_preserves_typ_of1 typ_of1_eta_norm typ_of_def by fastforce
lemma inst_ok_nil[simp]: "inst_ok Θ []" by simp
lemma axiom_subst_typ':
assumes "wf_theory Θ" "A∈axioms Θ" "inst_ok Θ insts"
shows "Θ, Γ ⊢ subst_typ' insts A"
proof-
have "wf_inst Θ (λidn S . the_default (Tv idn S) (lookup (λx. x=(idn, S)) insts))"
using inst_ok_imp_wf_inst assms(3) by blast
moreover have "subst_typ' insts A
= tsubst A (λidn S . the_default (Tv idn S) (lookup (λx. x=(idn, S)) insts))"
by (simp add: tsubst_simulates_subst_typ')
ultimately show ?thesis
using assms axiom by simp
qed
corollary axiom': "wf_theory Θ ⟹ A ∈ axioms Θ ⟹ Θ, Γ ⊢ A"
apply (subst subst_typ'_nil[symmetric])
using axiom_subst_typ' inst_ok_nil by metis
lemma has_sort_Tv_refl: "wf_osig oss ⟹ sort_ex (subclass oss) S ⟹ has_sort oss (Tv v S) S"
by (cases oss) (simp add: osig_subclass_loc wf_subclass_loc.intro has_sort_Tv wf_subclass_loc.sort_leq_refl)
lemma has_sort_Tv_refl':
"wf_theory Θ ⟹ typ_ok Θ (Tv v S) ⟹ has_sort (osig (sig Θ)) (Tv v S) S"
using has_sort_Tv_refl
by (metis wf_sig.simps osig.elims wf_theory_imp_wf_sig typ_ok_def
wf_type_imp_typ_ok_sig typ_ok_sig.simps(2) wf_sort_def)
lemma wf_inst_imp_inst_ok:
"wf_theory Θ ⟹ distinct l ⟹ ∀(v, S) ∈ set l . typ_ok Θ (Tv v S) ⟹ wf_inst Θ ρ
⟹ inst_ok Θ (map (λ(v, S) . ((v, S), ρ v S)) l)"
proof (induction l)
case Nil
then show ?case by simp
next
case (Cons a l)
have I: "inst_ok Θ (map (λ(v,S) . ((v, S), ρ v S)) l)"
using Cons by fastforce
have "a ∉ set l"
using Cons.prems(2) by auto
hence "(a, case_prod ρ a) ∉ set (map (λ(v,S) . ((v, S), ρ v S)) l)"
by (simp add: image_iff prod.case_eq_if)
moreover have "distinct (map (λ(v,S) . ((v, S), ρ v S)) l)"
using I distinct_kv_list distinct_map by fast
ultimately have "distinct (map (λ(v,S) . ((v, S), ρ v S)) (a#l))"
by (auto split: prod.splits)
moreover have "wf_type (sig Θ) (case_prod ρ a)"
using Cons.prems(3-4) by auto (metis typ_ok_Tv wf_type_imp_typ_ok_sig)
moreover hence "typ_ok Θ (case_prod ρ a)"
by simp
moreover hence "has_sort (osig (sig Θ)) (case_prod ρ a) (snd a)"
using Cons.prems by (metis (full_types) has_sort_Tv_refl' prod.case_eq_if wf_inst_def)
ultimately show ?case
using I by (auto simp del: typ_ok_def split: prod.splits)
qed
lemma typs_of_fv_subset_Types: "snd ` fv t ⊆ Types t"
by (induction t) auto
lemma osig_tvsT_subset_SortsT: "snd ` tvsT T ⊆ SortsT T"
by (induction T) auto
lemma osig_tvs_subset_Sorts: "snd ` tvs t ⊆ Sorts t"
by (induction t) (use osig_tvsT_subset_SortsT in ‹auto simp add: image_subset_iff›)
lemma term_ok_Types_imp_typ_ok_pre:
"is_std_sig Σ ⟹ term_ok' Σ t ⟹ τ ∈ Types t ⟹ typ_ok_sig Σ τ"
by (induction t arbitrary: τ) (auto split: option.splits)
lemma term_ok_Types_typ_ok: "wf_theory Θ ⟹ term_ok Θ t ⟹ τ ∈ Types t ⟹ typ_ok Θ τ"
by (cases Θ rule: theory_full_exhaust) (fastforce simp add: wt_term_def
intro: term_ok_Types_imp_typ_ok_pre)
lemma term_ok_fv_imp_typ_ok_pre:
"is_std_sig Σ ⟹ term_ok' Σ t ⟹ (x,τ) ∈ fv t ⟹ typ_ok_sig Σ τ"
using typs_of_fv_subset_Types term_ok_Types_imp_typ_ok_pre
by (metis image_subset_iff snd_conv)
lemma term_ok_vars_typ_ok: "wf_theory Θ ⟹ term_ok Θ t ⟹ (x, τ) ∈ fv t ⟹ typ_ok Θ τ"
using term_ok_Types_typ_ok typs_of_fv_subset_Types by (metis image_subset_iff snd_conv)
lemma typ_ok_TFreesT_imp_sort_ok_pre:
"is_std_sig Σ ⟹ typ_ok_sig Σ T ⟹ (x, S) ∈ tvsT T ⟹ wf_sort (subclass (osig Σ)) S"
proof (induction T)
case (Ty n Ts)
then show ?case by (induction Ts) (fastforce dest: split_list split: option.split_asm)+
qed (auto simp add: wf_sort_def)
lemma term_ok_TFrees_imp_sort_ok_pre:
"is_std_sig Σ ⟹ term_ok' Σ t ⟹ (x, S) ∈ tvs t ⟹ wf_sort (subclass (osig Σ)) S"
proof (induction t arbitrary: S)
case (Ct n T)
then show ?case
apply (clarsimp split: option.splits)
by (use typ_ok_TFreesT_imp_sort_ok_pre wf_sort_def in auto)
next
case (Fv n T)
then show ?case
apply (clarsimp split: option.splits)
by (use typ_ok_TFreesT_imp_sort_ok_pre wf_sort_def in auto)
next
case (Bv n)
then show ?case
by (clarsimp split: option.splits)
next
case (Abs T t)
then show ?case
apply simp
using typ_ok_TFreesT_imp_sort_ok_pre wf_sort_def
by meson
next
case (App t1 t2)
then show ?case
by auto
qed
lemma typ_ok_tvsT_imp_sort_ok_pre:
"is_std_sig Σ ⟹ typ_ok_sig Σ T ⟹ (x,S) ∈ tvsT T ⟹ wf_sort (subclass (osig Σ)) S"
proof (induction T)
case (Ty n Ts)
then show ?case by (induction Ts) (fastforce dest: split_list split: option.split_asm)+
qed (auto simp add: wf_sort_def)
lemma term_ok_tvars_sort_ok:
assumes "wf_theory Θ" "term_ok Θ t" "(x, S) ∈ tvs t"
shows "wf_sort (subclass (osig (sig Θ))) S"
proof-
have "term_ok' (sig Θ) t"
using assms(2) by (simp add: wt_term_def)
moreover have "is_std_sig (sig Θ)"
using assms by (cases Θ rule: theory_full_exhaust) simp
ultimately show ?thesis
using assms(3) term_ok_TFrees_imp_sort_ok_pre by simp
qed
lemma term_ok'_bind_fv2:
assumes "term_ok' Σ t"
shows "term_ok' Σ (bind_fv2 (v,T) lev t)"
using assms by (induction "(v,T)" lev t rule: bind_fv2.induct) auto
lemma term_ok'_bind_fv:
assumes "term_ok' Σ t"
shows "term_ok' Σ (bind_fv (v,τ) t)"
using term_ok'_bind_fv2 bind_fv_def assms by metis
lemma term_ok'_Abs_fv:
assumes "term_ok' Σ t" "typ_ok_sig Σ τ"
shows "term_ok' Σ (Abs τ (bind_fv (v,τ) t))"
using term_ok'_bind_fv assms by simp
lemma term_ok'_mk_all:
assumes "wf_theory Θ" and "term_ok' (sig Θ) B" and "typ_of B = Some propT"
and "typ_ok Θ τ"
shows "term_ok' (sig Θ) (mk_all x τ B)"
using assms term_ok'_bind_fv
by (cases Θ rule: wf_theory.cases) (auto simp add: typ_of_def tinstT_def)
lemma term_ok_mk_all:
assumes "wf_theory Θ" and "term_ok' (sig Θ) B" and "typ_of B = Some propT" and "typ_ok Θ τ"
shows "term_ok Θ (mk_all x τ B)"
using typ_of_mk_all term_ok'_mk_all assms by (auto simp add: wt_term_def)
lemma term_ok'_incr_boundvars:
"term_ok' (sig Θ) t ⟹ term_ok' (sig Θ) (incr_boundvars lev t)"
using term_ok'_incr_bv incr_boundvars_def by simp
lemma term_ok'_subst_bv1:
assumes "term_ok' (sig Θ) f" and "term_ok' (sig Θ) u"
shows "term_ok' (sig Θ) (subst_bv1 f lev u)"
using assms by (induction f lev u rule: subst_bv1.induct) (use term_ok'_incr_boundvars in auto)
lemma term_ok'_subst_bv:
assumes "term_ok' (sig Θ) f" and "term_ok' (sig Θ) u"
shows "term_ok' (sig Θ) (subst_bv f u)"
using assms term_ok'_subst_bv1 subst_bv_def by simp
lemma term_ok'_betapply:
assumes "term_ok' (sig Θ) f" "term_ok' (sig Θ) u"
shows "term_ok' (sig Θ) (f ∙ u)"
proof(cases "f")
case (Abs T t)
then show ?thesis
using assms term_ok'_subst_bv1 by (simp add: subst_bv_def)
qed (use assms in auto)
lemma term_ok_betapply:
assumes "term_ok Θ f" "term_ok Θ u"
assumes "typ_of f = Some (uty → tty)" "typ_of u = Some uty"
shows "term_ok Θ (f ∙ u)"
using assms term_ok'_betapply wt_term_def typ_of_betaply assms by auto
lemma typ_ok_sig_subst_typ:
assumes "is_std_sig Σ" and "typ_ok_sig Σ ty" and "distinct (map fst insts)"
and "list_all (typ_ok_sig Σ) (map snd insts)"
shows "typ_ok_sig Σ (subst_typ insts ty)"
using assms proof (induction insts ty rule: subst_typ.induct)
case (1 inst a Ts)
have "typ_ok_sig Σ (subst_typ inst ty)" if "ty ∈ set Ts" for ty
using that 1 by (auto simp add: list_all_iff split: option.splits)
hence "∀ty ∈ set (map (subst_typ inst) Ts) . typ_ok_sig Σ ty"
by simp
hence "list_all (typ_ok_sig Σ) (map (subst_typ inst) Ts)"
using list_all_iff by blast
moreover have "length (map (subst_typ inst) Ts) = length Ts" by simp
ultimately show ?case using "1.prems" by (auto split: option.splits)
next
case (2 inst idn S)
then show ?case
proof(cases "lookup (λx. x = (idn, S)) inst ≠ None")
case True
from this 2 obtain res where res: "lookup (λx. x = (idn, S)) inst = Some res" by auto
have "res ∈ set (map snd inst)" using 2 res by (induction inst) (auto split: if_splits)
hence "typ_ok_sig Σ res" using 2(4) res
by (induction inst) (auto split: if_splits simp add: rev_image_eqI)
then show ?thesis using res by simp
next
case False
hence rewr: "subst_typ inst (Tv idn S) = Tv idn S" by auto
then show ?thesis using "2.prems"(2) by simp
qed
qed
corollary subst_typ_tinstT: "tinstT (subst_typ insts ty) ty"
unfolding tinstT_def using tsubstT_simulates_subst_typ by fastforce
lemma tsubstT_trans: "tsubstT ty ρ1 = ty1 ⟹ tsubstT ty1 ρ2 = ty2
⟹ tsubstT ty (λidx s . case ρ1 idx s of Tv idx' s' ⇒ ρ2 idx' s'
| Ty s Ts ⇒ Ty s (map (λT. tsubstT T ρ2) Ts)) = ty2"
unfolding tinstT_def proof (induction ty arbitrary: ty1 ty2)
case (Tv idx s)
then show ?case by (cases "ρ1 idx s") auto
qed auto
corollary tinstT_trans: "tinstT ty1 ty ⟹ tinstT ty2 ty1 ⟹ tinstT ty2 ty"
unfolding tinstT_def using tsubstT_trans by blast
lemma term_ok'_subst_typ':
assumes "is_std_sig Σ" and "term_ok' Σ t" and "distinct (map fst insts)"
and "list_all (typ_ok_sig Σ) (map snd insts)"
shows "term_ok' Σ (subst_typ' insts t)"
using assms by (induction t)
(use typ_ok_sig_subst_typ subst_typ_tinstT tinstT_trans in ‹auto split: option.splits›)
lemma
term_ok'_occs:
"is_std_sig Σ ⟹ term_ok' Σ t ⟹ occs u t ⟹ term_ok' Σ u"
by (induction t) auto
lemma typ_of1_tsubst:
"typ_of1 Ts t = Some ty ⟹ typ_of1 (map (λT . tsubstT T ρ) Ts) (tsubst t ρ) = Some (tsubstT ty ρ)"
proof (induction Ts t arbitrary: ty rule: typ_of1.induct)
case (2 Ts i)
then show ?case by (auto split: if_splits)
next
case (4 Ts T body)
then show ?case by (auto simp add: bind_eq_Some_conv)
next
case (5 Ts f u)
from "5.prems" obtain u_ty where u_ty: "typ_of1 Ts u = Some u_ty" by (auto simp add: bind_eq_Some_conv)
from this "5.prems" have f_ty: "typ_of1 Ts f = Some (u_ty → ty)"
by (auto simp add: bind_eq_Some_conv typ_of1_arg_typ[OF "5.prems"(1)]
split: if_splits typ.splits option.splits)
from u_ty "5.IH"(1) have "typ_of1 (map (λT. tsubstT T ρ) Ts) (tsubst u ρ) = Some (tsubstT u_ty ρ)"
by simp
moreover from u_ty f_ty "5.IH"(2) have "typ_of1 (map (λT. tsubstT T ρ) Ts) (tsubst f ρ)
= Some (tsubstT (u_ty → ty) ρ)"
by simp
ultimately show ?case by simp
qed auto
corollary typ_of1_tsubst_weak:
assumes "typ_of1 Ts t = Some ty"
assumes "typ_of1 (map (λT . tsubstT T ρ) Ts) (tsubst t ρ) = Some ty'"
shows "tsubstT ty ρ = ty'"
using assms typ_of1_tsubst by auto
lemma tsubstT_no_change[simp]: "tsubstT T Tv = T"
by (induction T) (auto simp add: map_idI)
lemma term_ok_mk_eq_same_typ:
assumes "wf_theory Θ"
assumes "term_ok Θ (mk_eq s t)"
shows "typ_of s = typ_of t"
using assms by (cases Θ rule: theory_full_exhaust)
(fastforce simp add: wt_term_def typ_of_def bind_eq_Some_conv tinstT_def)
lemma typ_of_eta_expand: "typ_of f = Some (τ → τ') ⟹ typ_of (Abs τ (f $ Bv 0)) = Some (τ → τ')"
using typ_of1_weaken by (fastforce simp add: bind_eq_Some_conv typ_of_def)
lemma term_okI: "term_ok' (sig Θ) t ⟹ typ_of t ≠ None ⟹ term_ok Θ t"
by (simp add: wt_term_def)
lemma term_okD1: "term_ok Θ t ⟹ term_ok' (sig Θ) t"
by (simp add: wt_term_def)
lemma term_okD2: "term_ok Θ t ⟹ typ_of t ≠ None"
by (simp add: wt_term_def)
lemma term_ok_imp_typ_ok': assumes "wf_theory Θ" "term_ok Θ t" shows "typ_ok Θ (the (typ_of t))"
proof-
obtain ty where ty: "typ_of t = Some ty"
by (meson assms option.exhaust term_okD2)
hence "typ_ok Θ ty"
using term_ok_imp_typ_ok assms by blast
thus ?thesis using ty by simp
qed
lemma term_ok_mk_eqI:
assumes "wf_theory Θ" "term_ok Θ s" "term_ok Θ t" "typ_of s = typ_of t"
shows"term_ok Θ (mk_eq s t)"
proof (rule term_okI)
have "typ_ok Θ (the (typ_of t))"
using assms(1) assms(3) term_ok_imp_typ_ok' by blast
hence "typ_ok_sig (sig Θ) (the (typ_of t))"
by simp
then show "term_ok' (sig Θ) (mk_eq s t)"
using assms apply -
apply (drule term_okD1)+
apply (cases Θ rule: theory_full_exhaust)
by (auto split: option.splits simp add: tinstT_def)
next
show "typ_of (mk_eq s t) ≠ None"
using assms typ_of_def by (auto dest: term_okD2 simp add: wt_term_def)
qed
lemma typ_of1_decr': "¬ loose_bvar1 t 0 ⟹ typ_of1 (T#Ts) t = Some τ ⟹ typ_of1 Ts (decr 0 t) = Some τ"
proof (induction Ts t arbitrary: T τ rule: typ_of1.induct)
case (4 Ts B body)
then show ?case
using typ_of1_decr_gen
apply (simp add: bind_eq_Some_conv split: if_splits option.splits)
by (metis append_Cons append_Nil length_Cons list.size(3) typ_of1_decr_gen)
next
case (5 Ts f u)
then show ?case apply (simp add: bind_eq_Some_conv split: if_splits option.splits)
by (smt no_loose_bvar1_subst_bv2_decr subst_bv_def substn_subst_0' typ_of1.simps(3) typ_of1_subst_bv_gen')
qed (auto simp add: bind_eq_Some_conv split: if_splits option.splits)
lemma typ_of1_eta_red_step_pre: "¬ loose_bvar1 t 0 ⟹
typ_of1 Ts (Abs τ (t $ Bv 0)) = Some (τ → τ') ⟹ typ_of1 Ts (decr 0 t) = Some (τ → τ')"
using typ_of1_decr'
by (smt length_Cons nth_Cons_0 typ_of1.simps(2) typ_of1_arg_typ typ_of_Abs_body_typ' zero_less_Suc)
lemma typ_of1_eta_red_step: "¬ is_dependent t ⟹
typ_of (Abs τ (t $ Bv 0)) = Some (τ → τ') ⟹ typ_of (decr 0 t) = Some (τ → τ')"
using typ_of_def is_dependent_def typ_of1_eta_red_step_pre by simp
lemma distinct_add_vars': "distinct acc ⟹ distinct (add_vars' t acc)"
unfolding add_vars'_def
by (induction t arbitrary: acc) auto
lemma distinct_add_tvarsT': "distinct acc ⟹ distinct (add_tvarsT' T acc)"
proof (induction T arbitrary: acc)
case (Ty n Ts)
then show ?case
by (induction Ts rule: rev_induct) (auto simp add: add_tvarsT'_def)
qed (simp add: add_tvarsT'_def)
lemma distinct_add_tvars': "distinct acc ⟹ distinct (add_tvars' t acc)"
by (induction t arbitrary: acc) (simp_all add: add_tvars'_def fold_types_def distinct_add_tvarsT')
lemma proved_terms_well_formed_pre: "Θ, Γ ⊢ p ⟹ typ_of p = Some propT ∧ term_ok Θ p"
proof (induction Γ p rule: proves.induct)
case (axiom A ρ)
from axiom have ty: "typ_of1 [] A = Some propT"
by (cases Θ rule: theory_full_exhaust) (simp add: wt_term_def typ_of_def)
let ?l = "add_tvars' A []"
let ?l' = "map (λ(v, S) . ((v, S), ρ v S)) ?l"
have dist: "distinct ?l"
using distinct_add_tvars' by simp
moreover have "∀(v, S) ∈ set ?l . typ_ok Θ (Tv v S)"
proof-
have "typ_ok Θ (Tv v T)" if "(v, T) ∈ tvs A" for v T
using axiom.hyps(1) axiom.hyps(2) axioms_terms_ok
term_ok_tvars_sort_ok that typ_ok_def typ_ok_Tv
by (meson wf_sort_def)
moreover have "set ?l = tvs A"
by auto
ultimately show ?thesis
by auto
qed
moreover hence "∀(v, S) ∈ set ?l . has_sort (osig (sig Θ)) (Tv v S) S"
using axiom.hyps(1) has_sort_Tv_refl' by blast
ultimately have "inst_ok Θ ?l'"
apply - apply (rule wf_inst_imp_inst_ok)
using axiom.hyps(1) axiom.hyps(3) by blast+
have simp: "tsubst A ρ = subst_typ' ?l' A"
using dist subst_typ'_simulates_tsubst_gen' by auto
have "typ_of1 [] (tsubst A ρ) = Some propT"
using tsubst_simulates_subst_typ' axioms_typ_of_propT typ_of1_tsubst ty by fastforce
hence 1: "typ_of1 [] (subst_typ' ?l' A) = Some propT"
using simp by simp
from axiom have "term_ok' (sig Θ) A"
by (cases Θ rule: theory_full_exhaust) (simp add: wt_term_def)
hence 2: "term_ok' (sig Θ) (subst_typ' ?l' A)"
using axiom term_ok'_subst_typ' apply (cases Θ rule: theory_full_exhaust)
apply (simp add: list_all_iff wt_term_def typ_of_def)
by (metis (no_types, lifting) ‹inst_ok Θ (map (λ(v, S). ((v, S), ρ v S)) (add_tvars' A []))›
axiom.hyps(1) list.pred_mono_strong sig.simps term_ok'_subst_typ' wf_theory.simps
typ_ok_def wf_type_imp_typ_ok_sig)
from 1 2 show ?case using simp by (simp add: wt_term_def typ_of_def)
next
case ("assume" A)
then show ?case by (simp add: wt_term_def)
next
case (forall_intro Γ B x τ)
hence "term_ok' (sig Θ) B" and "typ_of B = Some propT"
by (simp_all add: wt_term_def)
show ?case using typ_of_mk_all forall_intro
term_ok_mk_all[OF ‹wf_theory Θ› ‹term_ok' (sig Θ) B›
‹typ_of B = Some propT› _, of _ x] ‹wf_type (sig Θ) τ›
by auto
next
case (forall_elim Γ τ B a)
thus ?case using term_ok'_subst_bv1
by (auto simp add: typ_of_def term_ok'_subst_bv tinstT_def
wt_term_def bind_eq_Some_conv subst_bv_def typ_of1_subst_bv_gen'
split: if_splits option.splits)
next
case (implies_intro Γ B A)
then show ?case
by (cases Θ rule: wf_theory.cases) (auto simp add: typ_of_def wt_term_def tinstT_def)
next
case (implies_elim Γ⇩1 A B Γ⇩2)
then show ?case
by (auto simp add: bind_eq_Some_conv typ_of_def wt_term_def tinstT_def
split: option.splits if_splits)
next
case (of_class c iT T)
then show ?case
by (cases Θ rule: theory_full_exhaust)
(auto simp add: bind_eq_Some_conv typ_of_def wt_term_def
tinstT_def mk_of_class_def mk_type_def)
next
case (β_conversion T t x)
hence 1: "typ_of (mk_eq (Abs T t $ x) (subst_bv x t)) = Some propT"
by (auto simp add: typ_of_def wt_term_def subst_bv_def bind_eq_Some_conv
typ_of1_subst_bv_gen')
moreover have "term_ok Θ (mk_eq (Abs T t $ x) (subst_bv x t))"
proof-
have "typ_of (mk_eq (Abs T t $ x) (subst_bv x t)) ≠ None"
using 1 by simp
moreover have "term_ok' (sig Θ) (mk_eq (Abs T t $ x) (subst_bv x t))"
proof-
have "term_ok' (sig Θ) (Abs T t $ x)"
using β_conversion.hyps(2) β_conversion.hyps(3) term_ok'.simps(4) wt_term_def term_ok_def by blast
moreover hence "term_ok' (sig Θ) (subst_bv x t)"
using subst_bv_def term_ok'_subst_bv1 by auto
moreover have "const_type (sig Θ) STR ''Pure.eq''
= Some ((Tv (Var (STR '''a'', 0)) full_sort) → ((Tv (Var (STR '''a'', 0)) full_sort) → propT))"
using β_conversion.hyps(1) by (cases Θ) fastforce
moreover obtain t' where "typ_of (Abs T t $ x) = Some t'"
by (smt "1" typ_of1_split_App typ_of_def)
moreover hence "typ_of (subst_bv x t) = Some t'"
by (smt list.simps(1) subst_bv_def typ.simps(1) typ_of1_split_App typ_of1_subst_bv_gen' typ_of_Abs_body_typ' typ_of_def)
moreover have "typ_ok_sig (sig Θ) t'"
using β_conversion.hyps(1) calculation(2) calculation(5) wt_term_def term_ok_imp_typ_ok typ_ok_def by auto
moreover hence "typ_ok_sig (sig Θ) (t' → propT) "
using ‹wf_theory Θ› by (cases Θ rule: theory_full_exhaust) auto
moreover have "tinstT (T → (T → propT)) ((Tv (Var (STR '''a'', 0)) full_sort) → ((Tv (Var (STR '''a'', 0)) full_sort) → propT))"
unfolding tinstT_def by auto
moreover have "tinstT (t' → (t' → propT)) ((Tv (Var (STR '''a'', 0)) full_sort) → ((Tv (Var (STR '''a'', 0)) full_sort) → propT))"
unfolding tinstT_def by auto
ultimately show ?thesis using ‹wf_theory Θ› by (cases Θ rule: theory_full_exhaust) auto
qed
ultimately show ?thesis using wt_term_def by simp
qed
ultimately show ?case by simp
next
case (eta t τ τ')
hence tyeta: "typ_of (Abs τ (t $ Bv 0)) = Some (τ → τ')"
using typ_of_eta_expand by auto
moreover have "¬ is_dependent t"
proof-
have "is_closed t"
using eta.hyps(3) typ_of_imp_closed by blast
thus ?thesis
using is_dependent_def is_open_def loose_bvar1_imp_loose_bvar by blast
qed
ultimately have ty_decr: "typ_of (decr 0 t) = Some (τ → τ')"
using typ_of1_eta_red_step by blast
hence 1: "typ_of (mk_eq (Abs τ (t $ Bv 0)) (decr 0 t)) = Some propT"
using eta tyeta by (auto simp add: typ_of_def)
have "typ_ok Θ (τ → τ')"
using eta term_ok_imp_typ_ok by (simp add: wt_term_def del: typ_ok_def)
hence tyok: "typ_ok Θ τ" "typ_ok Θ τ'"
unfolding typ_ok_def by (auto split: option.splits)
hence "term_ok Θ (Abs τ (t $ Bv 0))"
using eta(2) tyeta by (simp add: wt_term_def)
moreover have "term_ok Θ (decr 0 t)"
using eta term_ok'_decr tyeta ty_decr wt_term_def typ_ok_def tyok
by (cases Θ rule: theory_full_exhaust) (auto split: option.splits simp add: tinstT_def)
ultimately have "term_ok Θ (mk_eq (Abs τ (t $ Bv 0)) (decr 0 t))"
using eta.hyps ty_decr tyeta tyok 1 term_ok_mk_eqI
by metis
then show ?case using 1
using eta.hyps(2) eta.hyps(3) has_typ_imp_closed term_ok_subst_bv_no_change
closed_subst_bv_no_change by auto
qed
corollary proved_terms_well_formed:
assumes "Θ, Γ ⊢ p"
shows "typ_of p = Some propT" "term_ok Θ p"
using assms proved_terms_well_formed_pre by auto
lemma forall_intros:
"wf_theory Θ ⟹ Θ,Γ ⊢ B ⟹ ∀(x, τ)∈set frees . (x,τ) ∉ FV Γ ∧ typ_ok Θ τ
⟹ Θ,Γ ⊢ mk_all_list frees B"
by (induction frees arbitrary: B)
(auto intro: proves.forall_intro simp add: mk_all_list_def simp del: FV_def split: prod.splits)
lemma term_ok_var[simp]: "term_ok Θ (Fv idn τ) = typ_ok Θ τ"
by (simp add: wt_term_def typ_of_def)
lemma typ_of_var[simp]: "typ_of (Fv idn τ) = Some τ"
by (simp add: typ_of_def)
lemma is_closed_Fv[simp]: "is_closed (Fv idn τ)" by (simp add: is_open_def)
corollary proved_terms_closed: "Θ, Γ ⊢ B ⟹ is_closed B"
by (simp add: proved_terms_well_formed(1) typ_of_imp_closed)
lemma not_loose_bvar_bind_fv2:
"¬ loose_bvar t lev ⟹ ¬ loose_bvar (bind_fv2 v lev t) (Suc lev)"
by (induction t arbitrary: lev) auto
lemma not_loose_bvar_bind_fv2_:
"¬ loose_bvar (bind_fv2 v lev t) lev ⟹ ¬ loose_bvar t lev"
by (induction t arbitrary: lev) (auto split: if_splits)
lemma fold_add_vars'_FV_pre: "set (fold add_vars' Hs acc) = set acc ∪ FV (set Hs)"
by (induction Hs arbitrary: acc) (auto simp add: add_vars'_fv_pre)
corollary fold_add_vars'_FV[simp]: "set (fold (add_vars') Hs []) = FV (set Hs)"
using fold_add_vars'_FV_pre by simp
lemma forall_intro_vars:
assumes "wf_theory Θ" "Θ, set Hs ⊢ B"
shows "Θ, set Hs ⊢ forall_intro_vars B Hs"
apply (rule forall_intros)
using assms apply simp_all apply clarsimp
using add_vars'_fv proved_terms_well_formed_pre term_ok_vars_typ_ok
by (metis term_ok_vars_typ_ok typ_ok_def wf_type_imp_typ_ok_sig)
lemma mk_all_list'_preserves_term_ok_typ_of:
assumes "wf_theory Θ" "term_ok Θ B" "typ_of B = Some propT" "∀(idn,ty)∈set vs . typ_ok Θ ty"
shows "term_ok Θ (mk_all_list vs B) ∧ typ_of (mk_all_list vs B) = Some propT"
using assms proof (induction vs rule: rev_induct)
case Nil
then show ?case by simp
next
case (snoc v vs)
hence I: "term_ok Θ (mk_all_list vs B)" "typ_of (mk_all_list vs B) = Some propT" by simp_all
obtain idn ty where v: "v=(idn,ty)" by fastforce
hence s: "(mk_all_list (vs @ [v]) B) = mk_all idn ty (mk_all_list (vs) B)"
by (simp add: mk_all_list_def)
have "typ_ok Θ ty" using v snoc.prems by simp
then show ?case using I s term_ok_mk_all snoc.prems(1) wt_term_def typ_of_mk_all by auto
qed
corollary forall_intro_vars_preserves_term_ok_typ_of:
assumes "wf_theory Θ" "term_ok Θ B" "typ_of B = Some propT"
shows "term_ok Θ (forall_intro_vars B Hs) ∧ typ_of (forall_intro_vars B Hs) = Some propT"
proof-
have 1: "∀(idn,ty)∈set (add_vars' B []) . typ_ok Θ ty"
using add_vars'_fv assms(1) assms(2) term_ok_vars_typ_ok by blast
thus ?thesis using assms mk_all_list'_preserves_term_ok_typ_of by simp
qed
lemma bind_fv_remove_var_from_fv: "fv (bind_fv (idn, τ) t) = fv t - {(idn, τ)}"
using bind_fv2_Fv_fv bind_fv_def by simp
lemma forall_intro_vars_remove_fv[simp]: "fv (forall_intro_vars t []) = {}"
using mk_all_list_fv_unchanged add_vars'_fv by simp
lemma term_ok_mk_all_list:
assumes "wf_theory Θ"
assumes "term_ok Θ B"
assumes "typ_of B = Some propT"
assumes "∀(idn, τ) ∈ set l . typ_ok Θ τ"
shows "term_ok Θ (mk_all_list l B) ∧ typ_of (mk_all_list l B) = Some propT"
using assms proof(induction l rule: rev_induct)
case Nil
then show ?case by simp
next
case (snoc v vs)
obtain idn τ where v: "v = (idn, τ)" by fastforce
hence simp: "mk_all_list (vs@[v]) B = mk_all idn τ (mk_all_list vs B)"
by (auto simp add: mk_all_list_def)
have I: "term_ok Θ (mk_all_list vs B)" "typ_of (mk_all_list vs B) = Some propT"
using snoc by auto
have "term_ok Θ (mk_all idn τ (mk_all_list vs B))"
using term_ok_mk_all snoc.prems I v by (auto simp add: wt_term_def)
moreover have "typ_of (mk_all idn τ (mk_all_list vs B)) = Some propT"
using I(2) v typ_of_mk_all by simp
ultimately show ?case by (simp add: simp)
qed
lemma tvs_bind_fv2: "tvs (bind_fv2 (v, T) lev t) ∪ tvsT T = tvs t ∪ tvsT T"
by (induction "(v, T)" lev t rule: bind_fv2.induct) auto
lemma tvs_bind_fv: "tvs (bind_fv (v,T) t) ∪ tvsT T = tvs t ∪ tvsT T"
using tvs_bind_fv2 bind_fv_def by simp
lemma tvs_mk_all': "tvs (mk_all idn ty B) = tvs B ∪ tvsT ty"
using tvs_bind_fv typ_of_def is_variable.simps(2) by fastforce
lemma tvs_mk_all_list:
"tvs (mk_all_list vs B) = tvs B ∪ tvsT_Set (snd ` set vs)"
proof(induction vs rule: rev_induct)
case Nil
then show ?case by simp
next
case (snoc v vs)
obtain idn τ where v: "v = (idn, τ)" by fastforce
show ?case using snoc v tvs_mk_all' by (auto simp add: mk_all_list_def)
qed
lemma tvs_occs: "occs v t ⟹ tvs v ⊆ tvs t"
by (induction t) auto
lemma tvs_forall_intro_vars: "tvs (forall_intro_vars B Hs) = tvs B"
proof-
have "∀(idn, ty)∈fv B . occs (Fv idn ty) B"
using fv_occs by blast
hence "∀(idn, ty)∈fv B . tvs (Fv idn ty) ⊆ tvs B"
using tvs_occs by blast
hence "∀(idn, ty)∈fv B . tvsT ty ⊆ tvs B"
by simp
hence "tvsT_Set (snd ` fv B) ⊆ tvs B"
by fastforce
hence "tvsT_Set (snd ` set (add_vars' B [])) ⊆ tvs B"
by (simp add: add_vars'_fv)
thus ?thesis using tvs_mk_all_list by auto
qed
lemma "strip_all_single_var B = Some τ ⟹ strip_all_single_body B ≠ B"
using strip_all_vars_step by fastforce
lemma strip_all_body_unchanged_iff_strip_all_single_body_unchanged:
"strip_all_body B = B ⟷ strip_all_single_body B = B"
by (metis not_Cons_self2 not_None_eq not_is_all_imp_strip_all_body_unchanged
strip_all_body_single_simp' strip_all_single_var_is_all strip_all_vars_step)
lemma strip_all_body_unchanged_imp_strip_all_vars_no:
assumes "strip_all_body B = B"
shows "strip_all_vars B = []"
by (smt assms not_Cons_self2 strip_all_body_single_simp' strip_all_single_body.simps(1) strip_all_vars.elims)
lemma strip_all_body_unchanged_imp_strip_all_single_body_unchanged:
"strip_all_body B = B ⟹ strip_all_single_body B = B"
by (smt (z3) not_Cons_self2 strip_all_body_single_simp' strip_all_single_body.simps(1) strip_all_vars.simps(1))
lemma strip_all_single_body_unchanged_imp_strip_all_body_unchanged:
"strip_all_single_body B = B ⟹ strip_all_body B = B"
by (auto elim!: strip_all_single_body.elims)
lemma strip_all_single_var_np_imp_strip_all_body_single_unchanged:
"strip_all_single_var B = None ⟹ strip_all_single_body B = B"
by (auto elim!: strip_all_single_var.elims)
lemma strip_all_single_form: "strip_all_single_var B = Some τ
⟹ Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ (strip_all_single_body B) = B"
by (auto elim!: strip_all_single_var.elims split: if_splits)
lemma proves_strip_all_single:
assumes "Θ, Γ ⊢ B" "strip_all_single_var B = Some τ"
"typ_of t = Some τ" "term_ok Θ t"
shows "Θ, Γ ⊢ subst_bv t (strip_all_single_body B)"
proof-
have 1: "Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ (strip_all_single_body B) = B"
using assms(2) strip_all_single_form by blast
hence "Θ, Γ ⊢ Abs τ (strip_all_single_body B) ∙ t"
using assms forall_elim
proof -
have "has_typ t τ"
by (meson ‹typ_of t = Some τ› has_typ_iff_typ_of)
then show ?thesis
by (metis "1" assms(1) assms(4) betapply.simps(1) forall_elim term_ok_def wt_term_def)
qed
thus ?thesis by simp
qed
corollary proves_strip_all_single_Fv:
assumes "Θ, Γ ⊢ B" "strip_all_single_var B = Some τ"
shows "Θ, Γ ⊢ subst_bv (Fv x τ) (strip_all_single_body B)"
proof -
have ok: "term_ok Θ B"
using assms(1) proved_terms_well_formed(2) by auto
thm strip_all_single_form
wt_term_def term_ok_var typ_of_var typ_ok_def proves_strip_all_single
strip_all_single_form
have s: "B = Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ (strip_all_single_body B)"
using assms(2) strip_all_single_form[symmetric] by simp
have "τ ∈ Types B"
by (subst s, simp)
hence "typ_ok Θ τ"
by (metis ok s term_ok'.simps(4) term_ok'.simps(5) term_okD1 typ_ok_def typ_ok_sig_imp_wf_type)
hence "term_ok Θ (Fv x τ)"
using term_ok_var by blast
then show ?thesis
using assms proves_strip_all_single[where τ=τ] by auto
qed
lemma strip_all_vars_no_strip_all_body_unchanged[simp]:
"strip_all_vars B = [] ⟹ strip_all_body B = B"
by (auto elim!: strip_all_vars.elims)
lemma "strip_all_vars B = (τs@[τ]) ⟹ strip_all_body B
= strip_all_single_body (Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ (strip_all_body B))"
by simp
lemma strip_all_vars_incr_bv: "strip_all_vars (incr_bv inc lev t) = strip_all_vars t"
by (induction t arbitrary: lev rule: strip_all_vars.induct) auto
lemma strip_all_vars_incr_boundvars: "strip_all_vars (incr_boundvars inc t) = strip_all_vars t"
using incr_boundvars_def strip_all_vars_incr_bv by simp
lemma strip_all_vars_subst_bv1_Fv:
"strip_all_vars (subst_bv1 B lev (Fv x τ)) = strip_all_vars B"
by (induction B arbitrary: lev rule: strip_all_vars.induct) (auto simp add: incr_boundvars_def)
lemma strip_all_vars_subst_bv_Fv:
"strip_all_vars (subst_bv (Fv x τ) B) = strip_all_vars B"
by (simp add: strip_all_vars_subst_bv1_Fv subst_bv_def)
lemma "strip_all_single_var B = Some τ
⟹ strip_all_vars (subst_bv (Fv x τ) (strip_all_single_body B)) = tl (strip_all_vars B)"
by (metis list.sel(3) strip_all_vars_step strip_all_vars_subst_bv_Fv)
corollary proves_strip_all_vars_Fv:
assumes "length xs = length (strip_all_vars B)" "Θ, Γ ⊢ B"
shows "Θ, Γ ⊢ fold (λ(x,τ). subst_bv (Fv x τ) o strip_all_single_body)
(zip xs (strip_all_vars B)) B"
using assms proof (induction xs "strip_all_vars B" arbitrary: B rule: list_induct2)
case Nil
then show ?case by simp
next
case (Cons x xs τ τs)
have st: "strip_all_single_var B = Some τ"
by (metis Cons.hyps(3) is_all_iff_strip_all_vars_not_empty list.distinct(1) list.inject
option.exhaust strip_all_single_var_is_all strip_all_vars_step)
moreover have "term_ok Θ (Fv x τ)"
proof-
obtain B' where "Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ B' = B"
using st strip_all_single_form by blast
moreover have "term_ok Θ B"
using Cons.prems proved_terms_well_formed(2) by auto
ultimately have "typ_ok Θ τ"
using term_ok'.simps(5) term_ok'.simps(4) term_ok_def wt_term_def typ_ok_def by blast
thus ?thesis unfolding term_ok_def wt_term_def typ_ok_def by simp
qed
ultimately have 1: "Θ,Γ ⊢ subst_bv (Fv x τ) (strip_all_single_body B)"
using proves_strip_all_single
by (simp add: Cons.prems proves_strip_all_single_Fv)
have "Θ,Γ ⊢ fold (λ(x, τ). subst_bv (Fv x τ) ∘ strip_all_single_body)
(zip xs (strip_all_vars (subst_bv (Fv x τ) (strip_all_single_body B))))
(subst_bv (Fv x τ) (strip_all_single_body B))"
apply (rule Cons.hyps)
apply (metis Cons.hyps(3) list.inject st strip_all_vars_step strip_all_vars_subst_bv_Fv)
using 1 by simp
moreover have "strip_all_vars B = τ # τs"
using Cons.hyps(3) by auto
ultimately show ?case
using st strip_all_vars_step strip_all_vars_subst_bv_Fv by fastforce
qed
lemma trivial_pre_depr: "term_ok Θ c ⟹ typ_of c = Some propT ⟹ Θ, {c} ⊢ c"
by (rule "assume") (simp_all add: wt_term_def)
lemma trivial_pre:
assumes "wf_theory Θ" "term_ok Θ c" "typ_of c = Some propT"
shows "Θ, {} ⊢ c ⟼ c"
proof-
have s: "{} = {c} - {c}" by simp
show ?thesis
apply (subst s)
apply (rule "implies_intro")
using assms by (auto simp add: wt_term_def intro: "assume")
qed
lemma inst_var:
assumes wf_theory: "wf_theory Θ"
assumes B: "Θ, Γ ⊢ B"
assumes a_ok: "term_ok Θ a"
assumes typ_a: "typ_of a = Some τ"
assumes free: "(x,τ) ∉ FV Γ"
shows "Θ, Γ ⊢ subst_term [((x, τ), a)] B"
proof-
have s1: "mk_all x τ B = Ct STR ''Pure.all'' ((τ → propT) → propT) $
Abs τ (bind_fv (x, τ) B)"
by (simp add: typ_of_def)
have closed_B: "is_closed B" using B proved_terms_well_formed_pre
using typ_of_imp_closed by blast
have "typ_ok Θ τ" using wt_term_def typ_ok_def term_ok_imp_typ_ok
using a_ok wf_theory typ_a by blast
hence p1: "Θ, Γ ⊢ mk_all x τ B"
using forall_intro[OF wf_theory B] B typ_a wt_term_def wf_theory
term_ok_imp_typ_ok free by simp
have "Θ, Γ ⊢ subst_bv a (bind_fv (x, τ) B)"
using forall_elim[of _ _ τ] p1 typ_a a_ok proves_strip_all_single
by (meson has_typ_iff_typ_of term_ok_def wt_term_def)
have "Θ, Γ ⊢ subst_bv a ((bind_fv (x, τ) B))"
using forall_elim[of _ _ τ] p1 typ_a a_ok proves_strip_all_single
by (meson has_typ_iff_typ_of term_ok_def wt_term_def)
thus "Θ, Γ ⊢ subst_term [((x, τ), a)] B"
using instantiate_var_same_type'' assms closed_B by simp
qed
lemma subst_term_single_no_change[simp]:
assumes nvar: "(x,τ)∉fv B"
shows "subst_term [((x,τ), t)] B = B"
using assms by (induction B) auto
lemma fv_subst_term_single:
assumes var: "(x,τ)∈fv B"
assumes "⋀p . p ∈ fv t ⟹ p ~= (x,τ)"
shows "fv (subst_term [((x,τ), t)] B) = fv B - {(x,τ)} ∪ fv t"
using assms proof (induction B)
case (App B1 B2)
then show ?case
by (cases "(x,τ)∈fv B1"; cases "(x,τ)∈fv B2") auto
qed simp_all
lemma inst_vars_pre:
assumes wf_theory: "wf_theory Θ"
assumes B: "Θ, Γ ⊢ B"
assumes vars_ok: "list_all (term_ok Θ) (map snd insts)"
assumes typs_ok: "list_all (λ((idx, ty), t) . typ_of t = Some ty) insts"
assumes free: "list_all (λ((idx, ty), t) . (idx, ty) ∉ FV Γ) insts"
assumes typ_a: "typ_of a = Some τ"
assumes distinct: "distinct (map fst insts)"
assumes no_overlap: "⋀x . x ∈ (⋃t ∈ snd ` (set insts) . fv t) ⟹ x ∉ fst ` (set insts)"
shows "Θ, Γ ⊢ fold (λsingle. subst_term [single]) insts B"
using assms proof(induction insts arbitrary: B)
case Nil
then show ?case using B by simp
next
case (Cons x xs)
from this obtain idn ty t where x: "x = ((idn, ty), t)" by (metis prod.collapse)
have "Θ, Γ ⊢ fold (λsingle. subst_term [single]) (x # xs) B
⟷ Θ, Γ ⊢ fold (λsingle. subst_term [single]) xs (subst_term [x] B)"
by simp
moreover have "Θ, Γ ⊢ fold (λsingle. subst_term [single]) xs (subst_term [x] B)"
proof-
have single: "Θ, Γ ⊢ (subst_term [x] B)" using inst_var Cons by (simp add: x)
show ?thesis using Cons single by simp
qed
ultimately show ?case by simp
qed
lemma subterm_term_ok':
"is_std_sig Σ ⟹ term_ok' Σ t ⟹ is_closed st ⟹ occs st t ⟹ term_ok' Σ st"
proof (induction t arbitrary: st)
case (Abs T t)
then show ?case by (auto simp add: is_open_def)
next
case (App t1 t2)
then show ?case using term_ok'_occs by blast
qed auto
lemma infinite_fv_UNIV: "infinite (UNIV :: (indexname × typ) set)"
by (simp add: finite_prod)
lemma implies_intro'_pre:
assumes "wf_theory Θ" "Θ, Γ ⊢ B" "term_ok Θ A" "typ_of A = Some propT" "A ∉ Γ"
shows "Θ, Γ ⊢ A ⟼ B"
using assms proves.implies_intro apply (simp add: wt_term_def)
by (metis Diff_empty Diff_insert0)
lemma implies_intro'_pre2:
assumes "wf_theory Θ" "Θ, Γ ⊢ B" "term_ok Θ A" "typ_of A = Some propT" "A ∈ Γ"
shows "Θ, Γ ⊢ A ⟼ B"
proof-
have 1: "Θ, Γ - {A} ⊢ A ⟼ B"
using assms proves.implies_intro by (simp add: wt_term_def)
have "Θ, Γ - {A} - {A} ⊢ A ⟼ (A ⟼ B)"
using assms proves.implies_intro
by (simp add: 1 implies_intro'_pre)
moreover have "Θ, {A} ⊢ A"
using proves.assume assms
by (simp add: trivial_pre_depr)
moreover have "Γ = (Γ - {A} - {A}) ∪ {A}"
using assms by auto
ultimately show ?thesis using proves.implies_elim by metis
qed
lemma subst_term_preserves_typ_of1[simp]:
"typ_of1 Ts (subst_term [((x, τ), Fv y τ)] t) = typ_of1 Ts t"
by (induction Ts t rule: typ_of1.induct) (fastforce)+
lemma subst_term_preserves_typ_of[simp]:
"typ_of (subst_term [((x, τ), Fv y τ)] t) = typ_of t"
using typ_of_def by simp
lemma subst_term_preserves_term_ok'[simp]:
"term_ok' Σ (subst_term [((x, τ), Fv y τ)] t) ⟷ term_ok' Σ t"
by (induction t) auto
lemma subst_term_preserves_term_ok[simp]:
"term_ok Θ (subst_term [((x, τ), Fv y τ)] A) ⟷ term_ok Θ A"
by (simp add: wt_term_def)
lemma not_in_FV_in_fv_not_in: "(x,τ) ∉ FV Γ ⟹ (x,τ) ∈ fv t ⟹ t ∉ Γ"
by auto
lemma subst_term_fv: "fv (subst_term [((x, τ), Fv y τ)] t)
= (if (x,τ) ∈ fv t then insert (y,τ) else id) (fv t - {(x,τ)})"
by (induction t) auto
lemma rename_free:
assumes wf_theory: "wf_theory Θ"
assumes B: "Θ, Γ ⊢ B"
assumes free: "(x,τ)∉ FV Γ"
shows "Θ, Γ ⊢ subst_term [((x, τ), Fv y τ)] B"
by (metis B free inst_var proved_terms_well_formed(2) subst_term_single_no_change
term_ok_vars_typ_ok term_ok_var wf_theory typ_of_var)
lemma tvs_subst_term_single[simp]: "tvs (subst_term [((x, τ), Fv y τ)] A) = tvs A"
by (induction A) auto
lemma weaken_proves': "Θ, Γ ⊢ B ⟹ term_ok Θ A ⟹ typ_of A = Some propT ⟹ A ∉ Γ
⟹ finite Γ
⟹ Θ, insert A Γ ⊢ B"
proof (induction Γ B arbitrary: A rule: proves.induct)
case (axiom A insts Γ A')
then show ?case using proves.axiom axiom by metis
next
case ("assume" A Γ A')
then show ?case using proves.intros by blast
next
case (forall_intro Γ B x τ)
have "∃y . y∉fst ` (fv A ∪ fv B ∪ FV Γ)"
proof-
have "finite (FV Γ)"
using finite_fv forall_intro.prems by auto
hence "finite (fv A ∪ fv B ∪ FV Γ)" by simp
hence "finite (fst ` (fv A ∪ fv B ∪ FV Γ))" by simp
thus ?thesis using variant_variable_fresh by blast
qed
from this obtain y where "y∉fst ` (fv A ∪ fv B ∪ FV Γ)" by auto
have not_in_ren: "subst_term [((x, τ), Fv y τ)] A ∉ Γ"
proof(cases "(x, τ) ∈ fv A")
case True
show ?thesis
apply (rule not_in_FV_in_fv_not_in[of y τ])
apply (metis (full_types) Un_iff ‹y ∉ fst ` (fv A ∪ fv B ∪ FV Γ)› fst_conv image_eqI)
using True subst_term_fv by auto
next
case False
hence "subst_term [((x, τ), Fv y τ)] A = A"
by simp
then show ?thesis
by (simp add: forall_intro.prems(3))
qed
have term_ok_ren: "term_ok Θ (subst_term [((x, τ), Fv y τ)] A)"
using forall_intro.prems(1) subst_term_preserves_term_ok by blast
have typ_of_ren: "typ_of (subst_term [((x, τ), Fv y τ)] A) = Some propT"
using forall_intro.prems by auto
hence "Θ, insert (subst_term [((x, τ), Fv y τ)] A) Γ ⊢ B"
using forall_intro.IH forall_intro.prems(3) forall_intro.prems(4)
not_in_ren term_ok_ren typ_of_ren by blast
have "Θ, insert (subst_term [((x, τ), Fv y τ)] A) Γ ⊢ mk_all x τ B"
apply (rule proves.forall_intro)
apply (simp add: forall_intro.hyps(1))
using ‹Θ, insert (subst_term [((x, τ), Fv y τ)] A) Γ ⊢ B› apply blast
subgoal using subst_term_fv ‹(x, τ) ∉ FV Γ› apply simp
by (metis Un_iff ‹y ∉ fst ` (fv A ∪ fv B ∪ FV Γ)› fst_conv image_eqI)
using forall_intro.hyps(4) by blast
hence "Θ, Γ ⊢ subst_term [((x, τ), Fv y τ)] A ⟼ mk_all x τ B"
using forall_intro.hyps(1) forall_intro.hyps(2) forall_intro.hyps(4)
forall_intro.prems(1) forall_intro.prems(3)
implies_intro'_pre local.forall_intro not_in_ren proves.forall_intro
subst_term_preserves_typ_of term_ok_ren by auto
hence "Θ, Γ ⊢ subst_term [((y, τ), Fv x τ)]
(subst_term [((x, τ), Fv y τ)] A ⟼ mk_all x τ B)"
by (smt Un_iff ‹y ∉ fst ` (fv A ∪ fv B ∪ FV Γ)› forall_intro.hyps(1)
fst_conv image_eqI rename_free)
hence "Θ, Γ ⊢ A ⟼ mk_all x τ B"
using forall_intro proves.forall_intro implies_intro'_pre by auto
moreover have "Θ, {A} ⊢ A"
using forall_intro.prems(1) local.forall_intro(7) trivial_pre_depr by blast
ultimately show ?case
using implies_elim by fastforce
next
case (forall_elim Γ τ B a)
then show ?case using proves.forall_elim by blast
next
case (implies_intro Γ B N)
then show ?case
proof (cases "A=N")
case True
hence "Θ,Γ - {N} ⊢ N ⟼ B"
using implies_intro.hyps(1) implies_intro.hyps(2) implies_intro.hyps(3)
implies_intro.hyps(4) proves.implies_intro by blast
hence "Θ,Γ - {N} ⊢ A ⟼ N ⟼ B"
using True implies_intro'_pre implies_intro.hyps(1) implies_intro.hyps(3)
implies_intro.hyps(4) implies_intro.prems(1) by blast
hence "Θ,insert N Γ ⊢ B"
using True implies_elim implies_intro insert_absorb by fastforce
then show ?thesis
using True implies_elim implies_intro.hyps(3) implies_intro.hyps(4) implies_intro.prems(1)
trivial_pre_depr by (simp add: implies_intro'_pre2 implies_intro.hyps(1))
next
case False
hence s: "insert A (Γ - {N}) = insert A Γ - {N}" by auto
have I: "Θ,insert A Γ ⊢ B"
using implies_intro.prems False by (auto intro!: implies_intro.IH)
show ?thesis
apply (subst s)
apply (rule proves.implies_intro)
using implies_intro.hyps I by auto
qed
next
case (implies_elim Γ⇩1 A' B Γ⇩2)
show ?case
using proves.implies_elim implies_elim by (metis UnCI Un_insert_left finite_Un)
next
case (β_conversion Γ s T t x)
then show ?case using proves.β_conversion by blast
next
case (eta t τ τ')
then show ?case using proves.eta by simp
next
case (of_class c T' T Γ)
then show ?case
by (simp add: proves.of_class)
qed
corollary weaken_proves: "Θ, Γ ⊢ B ⟹ term_ok Θ A ⟹ typ_of A = Some propT
⟹ finite Γ
⟹ Θ, insert A Γ ⊢ B"
using weaken_proves' by (metis insert_absorb)
lemma weaken_proves_set: "finite Γ2 ⟹ Θ, Γ ⊢ B ⟹ ∀A∈Γ2 . term_ok Θ A ⟹ ∀A∈Γ2 . typ_of A = Some propT
⟹ finite Γ
⟹ Θ, Γ ∪ Γ2 ⊢ B"
by (induction Γ2 arbitrary: Γ rule: finite_induct) (use weaken_proves in auto)
lemma no_tvsT_imp_subst_typ_unchanged: "tvsT T = empty ⟹ subst_typ insts T = T"
by (simp add: no_tvsT_imp_tsubsT_unchanged tsubstT_simulates_subst_typ)
lemma subst_typ_fv:
shows "apsnd (subst_typ insts) ` fv B = fv (subst_typ' insts B)"
by (induction B) auto
lemma subst_typ_fv_point:
assumes "(x, τ) ∈ fv B"
shows "(x, subst_typ insts τ) ∈ fv (subst_typ' insts B)"
using subst_typ_fv by (metis apsnd_conv assms image_eqI)
lemma subst_typ_typ_ok:
assumes "typ_ok_sig Σ τ"
assumes "list_all (typ_ok_sig Σ) (map snd insts)"
shows "typ_ok_sig Σ (subst_typ insts τ)"
using assms proof (induction τ)
case (Tv idn τ)
then show ?case
by (cases "lookup (λx. x = (idn, τ)) insts")
(fastforce simp add: list_all_iff dest: lookup_present_eq_key' split: prod.splits)+
qed (auto simp add: list_all_iff lookup_present_eq_key' split: option.splits)
lemma subst_typ_comp_single_left: "subst_typ [single] (subst_typ insts T)
= subst_typ (map (apsnd (subst_typ [single])) insts@[single]) T"
proof (induction T)
case (Tv idn ty)
then show ?case by (induction insts) auto
qed auto
lemma subst_typ_comp_single_left_stronger: "subst_typ [single] (subst_typ insts T)
= subst_typ (map (apsnd (subst_typ [single])) insts
@ (if fst single ∈ set (map fst insts) then [] else [single])) T"
proof (induction T)
case (Tv idn S)
then show ?case
proof (cases "lookup (λx. x = (idn,S)) insts")
case None
hence "lookup (λx. x = (idn, S)) (map (apsnd (subst_typ [single])) insts) = None"
by (induction insts) (auto split: if_splits)
then show ?thesis
using None apply simp
by (metis eq_fst_iff list.set_map lookup.simps(2) lookup_None_iff subst_typ.simps(2)
subst_typ_comp subst_typ_nil the_default.simps(1))
next
case (Some a)
hence "lookup (λx. x = (idn, S)) (map (apsnd (subst_typ [single])) insts) = Some (subst_typ [single] a)"
by (induction insts) (auto split: if_splits)
then show ?thesis
using Some apply simp
by (metis subst_typ.simps(2) subst_typ_comp_single_left the_default.simps(2))
qed
qed auto
lemma subst_typ'_comp_single_left: "subst_typ' [single] (subst_typ' insts t)
= subst_typ' (map (apsnd (subst_typ [single])) insts@[single]) t"
by (induction t) (use subst_typ_comp_single_left in auto)
lemma subst_typ'_comp_single_left_stronger: "subst_typ' [single] (subst_typ' insts t)
= subst_typ' (map (apsnd (subst_typ [single])) insts
@ (if fst single ∈ set (map fst insts) then [] else [single])) t"
by (induction t) (use subst_typ_comp_single_left_stronger in auto)
lemma subst_typ_preserves_typ_ok:
assumes "wf_theory Θ"
assumes "typ_ok Θ T"
assumes "list_all (typ_ok Θ) (map snd insts)"
shows "typ_ok Θ (subst_typ insts T)"
using assms proof (induction T)
case (Ty n Ts)
have I: "∀x ∈ set Ts . typ_ok Θ (subst_typ insts x)"
using Ty by (auto simp add: typ_ok_def list_all_iff split: option.splits)
moreover have "(∀x ∈ set Ts . typ_ok Θ (subst_typ insts x)) =
(∀x ∈ set (map (subst_typ insts) Ts) . typ_ok Θ x)" by (induction Ts) auto
ultimately have "list_all (wf_type (sig Θ)) (map (subst_typ insts) Ts)"
using list_allI typ_ok_def Ball_set typ_ok_def by fastforce
then show ?case using Ty list.pred_mono_strong by (force split: option.splits)
next
case (Tv idn τ)
then show ?case by (induction insts) auto
qed
lemma typ_ok_Ty[simp]: "typ_ok Θ (Ty n Ts) ⟹ list_all (typ_ok Θ) Ts"
by (auto simp add: typ_ok_def list.pred_mono_strong split: option.splits)
lemma typ_ok_sig_Ty[simp]: "typ_ok_sig Σ (Ty n Ts) ⟹ list_all (typ_ok_sig Σ) Ts"
by (auto simp add: list.pred_mono_strong split: option.splits)
lemma wf_theory_imp_wf_osig: "wf_theory Θ ⟹ wf_osig (osig (sig Θ))"
by (cases Θ rule: theory_full_exhaust) simp
lemma the_lift2_option_Somes[simp]: "the (lift2_option f (Some a) (Some b)) = f a b" by simp
lemma class_les_mgd:
assumes "wf_osig oss"
assumes "tcsigs oss type = Some mgd"
assumes "mgd C' = Some Ss'"
assumes "class_les (subclass oss) C' C"
shows "mgd C ≠ None"
proof-
have "complete_tcsigs (subclass oss) (tcsigs oss)"
using assms(1) by (cases oss) simp
thus ?thesis
using assms(2-4) by (auto simp add: class_les_def class_leq_def complete_tcsigs_def intro!: domI ranI)
qed
lemma has_sort_sort_leq_osig:
assumes "wf_osig (sub, tcs)" "has_sort (sub,tcs) T S" "sort_leq sub S S'"
shows "has_sort (sub,tcs) T S'"
using assms(2,3,1) proof (induction "(sub,tcs)" T S arbitrary: S' rule: has_sort.induct)
case (has_sort_Tv S S' tcs a)
then show ?case
using wf_osig.simps wf_subclass_loc.intro wf_subclass_loc.sort_leq_trans by blast
next
case (has_sort_Ty κ K S Ts)
show ?case
proof (rule has_sort.has_sort_Ty[where dm=K])
show "tcs κ = Some K"
using has_sort_Ty.hyps(1) .
next
show "∀C∈S'. ∃Ss. K C = Some Ss ∧ list_all2 (has_sort (sub, tcs)) Ts Ss"
proof (rule ballI)
fix C assume C: "C ∈ S'"
show "∃Ss. K C = Some Ss ∧ list_all2 (has_sort (sub, tcs)) Ts Ss"
proof (cases "C ∈ S")
case True
then show ?thesis
using list_all2_mono has_sort_Ty.hyps(2) by fastforce
next
case False
from this obtain C' where C':
"C' ∈ S" "class_les sub C' C"
by (metis C class_les_def has_sort_Ty.prems(1) has_sort_Ty.prems(2) sort_leq_def
subclass.simps wf_osig_imp_wf_subclass_loc wf_subclass_loc.class_leq_antisym)
from this obtain Ss' where Ss':
"K C' = Some Ss'" "list_all2 (has_sort (sub,tcs)) Ts Ss'"
using list_all2_mono has_sort_Ty.hyps(2) by fastforce
from this obtain Ss where Ss: "K C = Some Ss"
using has_sort_Ty.prems class_les_mgd C'(2) has_sort_Ty.hyps(1) wf_theory_imp_wf_osig
by force
have lengthSs': "length Ts = length Ss'"
using Ss'(2) list_all2_lengthD by auto
have coregular:
"coregular_tcsigs sub tcs"
using has_sort_Ty.prems(2) wf_theory_imp_wf_osig wf_tcsigs_def
by (metis wf_osig.simps)
hence leq: "list_all2 (sort_leq sub) Ss' Ss"
using C'(2) Ss'(1) Ss has_sort_Ty.hyps(1) ranI
by (metis class_les_def coregular_tcsigs_def domI option.sel)
have "list_all2 (has_sort (sub,tcs)) Ts Ss"
proof(rule list_all2_all_nthI)
show "length Ts = length Ss"
using Ss Ss'(1) lengthSs' wf_theory_imp_wf_osig leq list_all2_lengthD by auto
next
fix n assume n: "n < length Ts"
hence "sort_leq sub (Ss' ! n) (Ss ! n)"
using leq by (simp add: lengthSs' list_all2_nthD)
thus "has_sort (sub,tcs) (Ts ! n) (Ss ! n)"
using has_sort_Ty.hyps(2) has_sort_Ty.prems(2) C'(1) Ss'(1) n list_all2_nthD
by fastforce
qed
thus "∃Ss. K C = Some Ss ∧ list_all2 (has_sort (sub, tcs)) Ts Ss"
using Ss by (simp)
qed
qed
qed
qed
lemma has_sort_sort_leq: "wf_theory Θ ⟹ has_sort (osig (sig Θ)) T S
⟹ sort_leq (subclass (osig (sig Θ))) S S'
⟹ has_sort (osig (sig Θ)) T S'"
by (metis has_sort_sort_leq_osig subclass.elims wf_theory_imp_wf_osig)
lemma subst_typ_preserves_has_sort:
assumes "wf_theory Θ"
assumes "has_sort (osig (sig Θ)) T S"
assumes "list_all (λ((idn, S), T). has_sort (osig (sig Θ)) T S) insts"
shows "has_sort (osig (sig Θ)) (subst_typ insts T) S"
using assms proof(induction T arbitrary: S)
case (Ty κ Ts)
obtain cl tcs where cltcs: "osig (sig Θ) = (cl, tcs)"
by fastforce
moreover obtain K where "tcsigs (osig (sig Θ)) κ = Some K"
using Ty.prems(2) has_sort.simps by auto
ultimately have mgd: "tcs κ = Some K"
by simp
have "has_sort (osig (sig Θ)) (subst_typ insts (Ty κ Ts)) S
= has_sort (osig (sig Θ)) (Ty κ (map (subst_typ insts) Ts)) S"
by simp
moreover have "has_sort (osig (sig Θ)) (Ty κ (map (subst_typ insts) Ts)) S"
proof (subst cltcs, rule has_sort_Ty[of tcs, OF mgd], rule ballI)
fix C assume C: "C ∈ S"
obtain Ss where Ss: "K C = Some Ss"
using C Ty.prems(2) mgd has_sort.simps cltcs by auto
have "list_all2 (has_sort (osig (sig Θ))) (map (subst_typ insts) Ts) Ss"
proof (rule list_all2_all_nthI)
show "length (map (subst_typ insts) Ts) = length Ss"
using C Ss Ty.prems(2) list_all2_lengthD mgd has_sort.simps cltcs by fastforce
next
fix n assume n: "n < length (map (subst_typ insts) Ts)"
have "list_all2 (has_sort (cl, tcs)) Ts Ss"
using C Ss Ty.prems(2) cltcs has_sort.simps mgd by auto
hence 1: "has_sort (osig (sig Θ)) (Ts ! n) (Ss ! n)"
using cltcs list_all2_conv_all_nth n by auto
have "has_sort (osig (sig Θ)) (subst_typ insts (Ts ! n)) (Ss ! n)"
using 1 n Ty.prems cltcs C Ss mgd Ty.IH by auto
then show "has_sort (osig (sig Θ)) (map (subst_typ insts) Ts ! n) (Ss ! n)"
using n by auto
qed
thus "∃Ss. K C = Some Ss ∧ list_all2 (has_sort (cl, tcs)) (map (subst_typ insts) Ts) Ss"
using Ss cltcs by simp
qed
ultimately show ?case
by simp
next
case (Tv idn S')
show ?case
proof(cases "(lookup (λx. x = (idn, S')) insts)")
case None
then show ?thesis using Tv by simp
next
case (Some res)
hence "((idn, S'), res) ∈ set insts" using lookup_present_eq_key' by fast
hence "has_sort (osig (sig Θ)) res S'" using Tv
using split_list by fastforce
moreover have 1: "sort_leq (subclass (osig (sig Θ))) S' S"
using Tv.prems(2) has_sort_Tv_imp_sort_leq by blast
ultimately show ?thesis
using Some Tv(2) has_sort_Tv_imp_sort_leq apply simp
using assms(1) 1 has_sort_sort_leq by blast
qed
qed
lemma subst_typ_preserves_Some_typ_of1:
assumes "typ_of1 Ts t = Some T"
shows "typ_of1 (map (subst_typ insts) Ts) (subst_typ' insts t)
= Some (subst_typ insts T)"
using assms proof (induction t arbitrary: T Ts)
next
case (App t1 t2)
from this obtain RT where "typ_of1 Ts t1 = Some (RT → T)"
using typ_of1_split_App_obtains by blast
hence "typ_of1 (map (subst_typ insts) Ts) (subst_typ' insts t1) =
Some (subst_typ insts (RT → T))" using App.IH(1) by blast
moreover have "typ_of1 (map (subst_typ insts) Ts) (subst_typ' insts t2) = Some (subst_typ insts RT)"
using App ‹typ_of1 Ts t1 = Some (RT → T)› typ_of1_fun_typ by blast
ultimately show ?case by simp
qed (fastforce split: if_splits simp add: bind_eq_Some_conv)+
corollary subst_typ_preserves_Some_typ_of:
assumes "typ_of t = Some T"
shows "typ_of (subst_typ' insts t)
= Some (subst_typ insts T)"
using assms subst_typ_preserves_Some_typ_of1 typ_of_def by fastforce
lemma subst_typ'_incr_bv:
"subst_typ' insts (incr_bv inc lev t) = incr_bv inc lev (subst_typ' insts t)"
by (induction inc lev t rule: incr_bv.induct) auto
lemma subst_typ'_incr_boundvars:
"subst_typ' insts (incr_boundvars lev t) = incr_boundvars lev (subst_typ' insts t)"
using subst_typ'_incr_bv incr_boundvars_def by simp
lemma subst_typ'_subst_bv1: "subst_typ' insts (subst_bv1 t n u)
= subst_bv1 (subst_typ' insts t) n (subst_typ' insts u)"
by (induction t n u rule: subst_bv1.induct) (auto simp add: subst_typ'_incr_boundvars)
lemma subst_typ'_subst_bv: "subst_typ' insts (subst_bv t u)
= subst_bv (subst_typ' insts t) (subst_typ' insts u)"
using subst_typ'_subst_bv1 subst_bv_def by simp
lemma subst_typ_no_tvsT_unchanged:
"∀(f, s) ∈ set insts . f ∉ tvsT T ⟹ subst_typ insts T = T"
proof (induction T)
case (Ty n Ts)
then show ?case by (induction Ts) (fastforce split: prod.splits)+
next
case (Tv idn S)
then show ?case
by simp (smt case_prodD case_prodE find_None_iff lookup_None_iff_find_None the_default.simps(1))
qed
lemma subst_typ'_no_tvs_unchanged:
"∀(f, s) ∈ set insts . f ∉ tvs t ⟹ subst_typ' insts t = t"
by (induction t) (use subst_typ_no_tvsT_unchanged in ‹fastforce+›)
lemma subst_typ'_preserves_term_ok':
assumes "wf_theory Θ"
assumes "inst_ok Θ insts"
assumes "term_ok' (sig Θ) t"
shows "term_ok' (sig Θ) (subst_typ' insts t)"
using assms term_ok'_subst_typ' typ_ok_def
by (metis list.pred_mono_strong wf_theory_imp_is_std_sig wf_type_imp_typ_ok_sig)
lemma subst_typ'_preserves_term_ok:
assumes "wf_theory Θ"
assumes "inst_ok Θ insts"
assumes "term_ok Θ t"
shows "term_ok Θ (subst_typ' insts t)"
using assms subst_typ_preserves_Some_typ_of wt_term_def subst_typ'_preserves_term_ok' by auto
lemma subst_typ_rename_vars_cancel:
assumes "y ∉ fst ` tvsT T"
shows "subst_typ [((y,S), Tv x S)] (subst_typ [((x,S), Tv y S)] T) = T"
using assms proof (induction T)
case (Ty n Ts)
then show ?case by (induction Ts) auto
qed auto
lemma subst_typ'_rename_tvars_cancel:
assumes "y ∉ fst ` tvs t" assumes "y ∉ fst ` tvsT τ"
shows "subst_typ' [((y,S), Tv x S)] ((bind_fv2 (x, subst_typ [((x,S), Tv y S)] τ))
lev (subst_typ' [((x,S), Tv y S)] t))
= bind_fv2 (x, τ) lev t"
using assms proof (induction t arbitrary: lev)
case (Ct n T)
then show ?case
by (simp add: subst_typ_rename_vars_cancel)
next
case (Fv idn T)
then show ?case
by (clarsimp simp add: subst_typ_rename_vars_cancel) (metis subst_typ_rename_vars_cancel)
next
case (Abs T t)
thus ?case
by (simp add: image_Un subst_typ_rename_vars_cancel)
next
case (App t1 t2)
then show ?case
by (simp add: image_Un)
qed auto
lemma bind_fv2_renamed_var:
assumes "y ∉ fst ` fv t"
shows "bind_fv2 (y, τ) i (subst_term [((x, τ), Fv y τ)] t)
= bind_fv2 (x, τ) i t"
using assms proof (induction t arbitrary: i)
qed auto
lemma bind_fv_renamed_var:
assumes "y ∉ fst ` fv t"
shows "bind_fv (y, τ) (subst_term [((x, τ), Fv y τ)] t)
= bind_fv (x, τ) t"
using bind_fv2_renamed_var bind_fv_def assms by auto
lemma subst_typ'_rename_tvar_bind_fv2:
assumes "y ∉ fst ` fv t"
assumes "(b, S) ∉ tvs t"
assumes "(b, S) ∉ tvsT τ"
shows "bind_fv2 (y, subst_typ [((a, S), Tv b S)] τ) i
(subst_typ' [((a,S), Tv b S)] (subst_term [((x, τ), Fv y τ)] t))
= subst_typ' [((a,S), Tv b S)] (bind_fv2 (x, τ) i t)"
using assms proof (induction t arbitrary: i)
qed auto
lemma subst_typ'_rename_tvar_bind_fv:
assumes "y ∉ fst ` fv t"
assumes "(b, S) ∉ tvs t"
assumes "(b, S) ∉ tvsT τ"
shows "bind_fv (y, subst_typ [((a,S), Tv b S)] τ)
(subst_typ' [((a,S), Tv b S)] (subst_term [((x, τ), Fv y τ)] t))
= subst_typ' [((a,S), Tv b S)] (bind_fv (x, τ) t)"
using bind_fv_def assms subst_typ'_rename_tvar_bind_fv2 by auto
lemma tvar_in_fv_in_tvs: "(a, τ) ∈ fv B ⟹ (x, S) ∈ tvsT τ ⟹ (x, S) ∈ tvs B"
by (induction B) auto
lemma tvs_bind_fv2_subset: "tvs (bind_fv2 (a, τ) i B) ⊆ tvs B"
by (induction B arbitrary: i) auto
lemma tvs_bind_fv_subset: "tvs (bind_fv (a, τ) B) ⊆ tvs B"
using tvs_bind_fv2_subset bind_fv_def by simp
lemma subst_typ_rename_tvar_preserves_eq:
"(y, S) ∉ tvsT T ⟹ (y, S) ∉ tvsT τ ⟹
subst_typ [((x, S), Tv y S)] T = subst_typ [((x, S), Tv y S)] τ ⟹ T=τ"
proof (induction T arbitrary: τ)
case (Ty n Ts)
then show ?case
proof (induction τ)
case (Ty n Ts)
then show ?case
by simp (smt list.inj_map_strong)
next
case (Tv n S)
then show ?case
by (auto split: if_splits)
qed
next
case (Tv n S)
then show ?case by (induction τ) (auto split: if_splits)
qed
lemma subst_typ'_subst_term_rename_var_swap:
assumes "b ∉ fst ` fv B"
assumes "(y, S) ∉ tvs B"
assumes "(y, S) ∉ tvsT τ"
shows "subst_typ' [((x, S), Tv y S)] (subst_term [((a, τ), Fv b τ)] B)
= subst_term [((a, (subst_typ [((x, S), Tv y S)] τ)), Fv b (subst_typ [((x, S), Tv y S)] τ))]
(subst_typ' [((x, S), Tv y S)] B)"
using assms proof (induction B)
case (Fv idn T)
then show ?case using subst_typ_rename_tvar_preserves_eq by auto
qed auto
lemma tvar_not_in_term_imp_free_not_in_term:
"(y, S) ∈ tvsT τ ⟹ (y,S) ∉ tvs t ⟹ (a, τ) ∉ fv t"
by (induction t) auto
lemma tvar_not_in_term_imp_free_not_in_term_set:
"finite Γ ⟹ (y, S) ∈ tvsT τ ⟹ (y,S) ∉ tvs_Set Γ ⟹ (a, τ) ∉ FV Γ"
using tvar_not_in_term_imp_free_not_in_term by simp
lemma inst_var_multiple:
assumes wf_theory: "wf_theory Θ"
assumes B: "Θ, Γ ⊢ B"
assumes vars: "∀(x,τ)∈fst ` set insts . term_ok Θ (Fv x τ)"
assumes a_ok: "∀a∈snd ` set insts . term_ok Θ a"
assumes typ_a: "∀((_,τ), a)∈set insts . typ_of a = Some τ"
assumes free: "∀(v, _)∈set insts . v ∉ FV Γ"
assumes distinct: "distinct (map fst insts)"
assumes finite: "finite Γ"
shows "Θ, Γ ⊢ subst_term insts B"
proof-
obtain fresh_idns where fresh_idns:
"length fresh_idns = length insts"
"∀idn ∈ set fresh_idns .
idn ∉ fst ` (fv B ∪ (⋃t∈snd ` set insts . (fv t)) ∪ (fst ` set insts)) ∪ fst ` (FV Γ)"
"distinct fresh_idns"
using distinct_fresh_rename_idns fresh_fresh_rename_idns length_fresh_rename_idns finite_FV finite
by (metis finite_imageI)
have 0: "subst_term insts B
= fold (λsingle acc . subst_term [single] acc) (zip (zip fresh_idns (map snd (map fst insts))) (map snd insts))
(fold (λsingle acc . subst_term [single] acc) (zip (map fst insts) (map2 Fv fresh_idns (map snd (map fst insts)))) B)"
using fresh_idns distinct subst_term_combine' by simp
from fresh_idns vars a_ok typ_a free distinct have 1:
"Θ, Γ ⊢ (fold (λsingle acc . subst_term [single] acc)
(zip (map fst insts) (map2 Fv fresh_idns (map snd (map fst insts)))) B)"
proof (induction fresh_idns insts rule: rev_induct2)
case Nil
then show ?case using B by simp
next
case (snoc x xs y ys)
from snoc have term_oky: "term_ok Θ (Fv (fst (fst y)) (snd (fst y)))"
by (auto simp add: wt_term_def split: prod.splits)
have 1: "Θ, Γ ⊢ fold (λsingle. subst_term [single])
(zip (map fst ys) (map2 Fv xs (map snd (map fst ys)))) B"
apply (rule snoc.IH)
subgoal using snoc.prems(1) by (clarsimp split: prod.splits) (smt UN_I Un_iff fst_conv image_iff)
using snoc.prems(2-7) by auto
moreover obtain yn n where ynn: "fst y = (yn, n)" by fastforce
moreover have "Θ,Γ ⊢ subst_term [(fst y, Fv x n)]
(fold (λsingle. subst_term [single]) (zip (map fst (ys))
(map2 Fv (xs) (map snd (map fst (ys))))) B)"
apply (simp only: ynn)
apply (rule inst_var[of "Θ" Γ "(fold (λsingle. subst_term [single]) (zip (map fst (ys))
(map2 Fv (xs) (map snd (map fst (ys))))) B)" "(Fv x n)" "n" "yn"])
using snoc.prems ‹wf_theory Θ› 1 apply (solves simp)+
using term_oky ynn apply (simp add: wt_term_def typ_of_def)
using term_oky ynn apply (simp add: wt_term_def typ_of_def)
using snoc.prems(6) ynn by auto
moreover have "fold (λsingle. subst_term [single]) (zip (map fst (ys @ [y]))
(map2 Fv (xs @ [x]) (map snd (map fst (ys @ [y]))))) B
= subst_term [(fst y, Fv x (snd (fst y)))]
(fold (λsingle. subst_term [single]) (zip (map fst (ys))
(map2 Fv (xs) (map snd (map fst (ys))))) B)"
using snoc.hyps by (induction xs ys rule: list_induct2) simp_all
ultimately show ?case by simp
qed
define point where "point ≡ (fold (λsingle acc . subst_term [single] acc)
(zip (map fst insts) (map2 Fv fresh_idns (map snd (map fst insts)))) B)"
from fresh_idns vars a_ok typ_a free distinct have 2:
"Θ, Γ ⊢ fold (λsingle acc . subst_term [single] acc)
(zip (zip fresh_idns (map snd (map fst insts))) (map snd insts))
point"
proof (induction fresh_idns insts rule: rev_induct2)
case Nil
then show ?case using B
using 1 point_def by auto
next
case (snoc x xs y ys)
from snoc have typ_ofy: "typ_of (snd y) = Some (snd (fst y))" by auto
have 1: " Θ,Γ ⊢ fold (λsingle. subst_term [single])
(zip (zip xs (map snd (map fst ys))) (map snd ys))
point"
apply (rule snoc.IH)
subgoal using snoc.prems(1) by (clarsimp split: prod.splits) (smt UN_I Un_iff fst_conv image_iff)
using snoc.prems(2-7) by auto
moreover obtain yn n where ynn: "fst y = (yn, n)" by fastforce
moreover have "Θ,Γ ⊢ subst_term [((x, snd (fst y)), snd y)] (fold (λsingle. subst_term [single])
(zip (zip (xs) (map snd (map fst (ys))))
(map snd (ys)))
point)"
apply (simp only: ynn) apply (rule inst_var)
using snoc.prems ‹wf_theory Θ› 1 apply (solves simp)+
using typ_ofy ynn apply (simp add: wt_term_def typ_of_def)
using snoc.prems apply simp
by (metis (full_types, opaque_lifting) UN_I fst_conv image_eqI)
moreover have "fold (λsingle. subst_term [single])
(zip (zip (xs @ [x]) (map snd (map fst (ys @ [y]))))
(map snd (ys @ [y])))
point = subst_term [((x, snd (fst y)), snd y)] (fold (λsingle. subst_term [single])
(zip (zip (xs) (map snd (map fst (ys))))
(map snd (ys)))
point)"
using snoc.hyps by (induction xs ys rule: list_induct2) simp_all
ultimately show ?case by simp
qed
from 0 1 2 show ?thesis using point_def by simp
qed
lemma term_ok_eta_red_step:
"¬ is_dependent t ⟹ term_ok Θ (Abs T (t $ Bv 0)) ⟹ term_ok Θ (decr 0 t)"
unfolding term_ok_def wt_term_def using term_ok'_decr eta_preserves_typ_of by simp blast
end