Theory EqualityProof
section "Derived rules on equality and normalization"
theory EqualityProof
imports Logic
begin
lemma proves_eq_reflexive_pre:
assumes "wf_theory Θ"
assumes "term_ok Θ t"
shows "Θ, {} ⊢ mk_eq t t"
proof-
have "eq_reflexive_ax ∈ axioms Θ"
using assms by (cases Θ rule: theory_full_exhaust) auto
moreover obtain τ where τ: "typ_of t = Some τ" using assms wt_term_def by auto
moreover hence "typ_ok Θ τ" using assms term_ok_imp_typ_ok by blast
ultimately have "Θ, {} ⊢ subst_typ' [((Var (STR '''a'', 0), full_sort), τ)] eq_reflexive_ax"
using axiom_subst_typ' assms by (simp del: term_ok_def)
hence "Θ, {} ⊢ subst_term [((Var (STR ''x'', 0), τ), t)]
(subst_typ' [((Var (STR '''a'', 0), full_sort), τ)] eq_reflexive_ax)"
using τ assms(1) assms(2) inst_var by auto
moreover have "subst_term [((Var (STR ''x'', 0), τ), t)]
(subst_typ' [((Var (STR '''a'', 0), full_sort), τ)] eq_reflexive_ax)
= mk_eq t t"
using τ by (simp add: eq_axs_def typ_of_def)
ultimately show ?thesis
by simp
qed
lemma unsimp_context: "Γ = {} ∪ Γ"
by simp
lemma proves_eq_reflexive:
assumes "wf_theory Θ"
assumes "term_ok Θ t"
assumes "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq t t"
by (subst unsimp_context) (use assms proves_eq_reflexive_pre weaken_proves_set in blast)
lemma proves_eq_symmetric_pre:
assumes "wf_theory Θ"
assumes "term_ok Θ t"
assumes "term_ok Θ s"
assumes "typ_of s = typ_of t"
shows "Θ, {} ⊢ mk_eq s t ⟼ mk_eq t s"
proof-
have "eq_symmetric_ax ∈ axioms Θ"
using assms by (cases Θ rule: theory_full_exhaust) auto
moreover obtain τ where τ: "typ_of t = Some τ" using assms wt_term_def by auto
moreover hence "typ_ok Θ τ" using assms term_ok_imp_typ_ok by blast
ultimately have "Θ, {} ⊢ subst_typ' [((Var (STR '''a'', 0), full_sort), τ)] eq_symmetric_ax"
using assms axiom_subst_typ' by (auto simp del: term_ok_def)
hence "Θ, {} ⊢ subst_term [((Var (STR ''x'', 0), τ), s), ((Var (STR ''y'', 0), τ), t)]
(subst_typ' [((Var (STR '''a'', 0), full_sort), τ)] eq_symmetric_ax)"
using τ ‹typ_ok Θ τ› term_ok_var assms by (fastforce intro!: inst_var_multiple simp add: eq_symmetric_ax_def)
thus ?thesis
using τ assms(4) by (simp add: eq_axs_def typ_of_def)
qed
lemma proves_eq_symmetric:
assumes "wf_theory Θ"
assumes "term_ok Θ t"
assumes "term_ok Θ s"
assumes "typ_of s = typ_of t"
assumes "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq s t ⟼ mk_eq t s"
by (subst unsimp_context) (use assms proves_eq_symmetric_pre weaken_proves_set in blast)
lemma proves_eq_symmetric2':
assumes "wf_theory Θ"
assumes "term_ok Θ (mk_eq s t)"
assumes "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq s t ⟼ mk_eq t s"
proof-
have "term_ok Θ s" "term_ok Θ t"
using assms wt_term_def term_ok_mk_eqD by blast+
moreover have "typ_of s = typ_of t"
using assms by (cases Θ rule: theory_full_exhaust)
(auto simp add: tinstT_def typ_of_def wt_term_def bind_eq_Some_conv)
ultimately show ?thesis
using proves_eq_symmetric assms by blast
qed
lemma proves_eq_symmetric_rule:
assumes "wf_theory Θ"
assumes "term_ok Θ t"
assumes "term_ok Θ s"
assumes "typ_of s = typ_of t"
assumes "Θ, Γ ⊢ mk_eq s t"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq t s"
using proves.implies_elim[OF proves_eq_symmetric[OF assms(1-4), of Γ] assms(5), OF ctxt] by simp
lemma proves_eq_transitive_pre:
assumes "wf_theory Θ"
assumes "term_ok Θ s"
assumes "term_ok Θ t"
assumes "term_ok Θ u"
assumes "typ_of s = typ_of t" "typ_of t = typ_of u"
shows "Θ, {} ⊢ mk_eq s t ⟼ mk_eq t u ⟼ mk_eq s u"
proof-
have "eq_transitive_ax ∈ axioms Θ"
using assms by (cases Θ rule: theory_full_exhaust) auto
moreover obtain τ where τ: "typ_of t = Some τ" using assms wt_term_def by auto
moreover hence ok: "typ_ok Θ τ" using assms term_ok_imp_typ_ok by blast
ultimately have "Θ, {} ⊢ subst_typ' [((Var (STR '''a'', 0), full_sort), τ)] eq_transitive_ax"
using assms axiom_subst_typ' by (auto simp del: term_ok_def)
hence "Θ, {} ⊢ subst_term [((Var (STR ''x'', 0), τ), s), ((Var (STR ''y'', 0), τ), t),
((Var (STR ''z'', 0), τ), u)]
(subst_typ' [((Var (STR '''a'', 0), full_sort), τ)] eq_transitive_ax)"
using τ assms ok term_ok_var by (fastforce intro!: inst_var_multiple simp add: eq_transitive_ax_def)
moreover have "subst_term [((Var (STR ''x'', 0), τ), s), ((Var (STR ''y'', 0), τ), t),
((Var (STR ''z'', 0), τ), u)]
(subst_typ' [((Var (STR '''a'', 0), full_sort), τ)] eq_transitive_ax)
= mk_eq s t ⟼ mk_eq t u ⟼ mk_eq s u"
using τ assms(5-6) apply (simp add: eq_axs_def typ_of_def)
by (metis option.sel the_default.simps(2))
ultimately show ?thesis
by simp
qed
lemma proves_eq_transitive:
assumes "wf_theory Θ"
assumes "term_ok Θ s"
assumes "term_ok Θ t"
assumes "term_ok Θ u"
assumes "typ_of s = typ_of t" "typ_of t = typ_of u"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq s t ⟼ mk_eq t u ⟼ mk_eq s u"
by (subst unsimp_context) (use assms proves_eq_transitive_pre weaken_proves_set in blast)
lemma proves_eq_transitive2:
assumes "wf_theory Θ"
assumes "term_ok Θ (mk_eq s t)"
assumes "term_ok Θ (mk_eq t u)"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq s t ⟼ mk_eq t u ⟼ mk_eq s u"
proof-
have "term_ok Θ s" "term_ok Θ t" "term_ok Θ u"
using assms wt_term_def term_ok_mk_eqD by blast+
moreover have "typ_of s = typ_of t"
using assms by (cases Θ rule: theory_full_exhaust)
(auto simp add: tinstT_def typ_of_def wt_term_def bind_eq_Some_conv)
moreover have "typ_of t = typ_of u"
using assms by (cases Θ rule: theory_full_exhaust)
(auto simp add: tinstT_def typ_of_def wt_term_def bind_eq_Some_conv)
ultimately show ?thesis using proves_eq_transitive assms by blast
qed
lemma proves_eq_transitive_rule:
assumes "wf_theory Θ"
assumes "term_ok Θ s"
assumes "term_ok Θ t"
assumes "term_ok Θ u"
assumes "typ_of s = typ_of t" "typ_of t = typ_of u"
assumes "Θ, Γ ⊢ mk_eq s t" "Θ, Γ ⊢ mk_eq t u"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq s u"
proof-
note 1 = proves_eq_transitive[OF assms(1-6), of Γ]
note 2 = proves.implies_elim[OF 1 assms(7)]
note 3 = proves.implies_elim[OF 2 assms(8)]
thus ?thesis using ctxt by simp
qed
lemma proves_eq_intr_pre:
assumes thy: "wf_theory Θ"
assumes A: "term_ok Θ A" "typ_of A = Some propT"
assumes B: "term_ok Θ B" "typ_of B = Some propT"
shows "Θ, {} ⊢ (A ⟼ B) ⟼ (B ⟼ A) ⟼ mk_eq A B"
proof-
have closed: "is_closed A" "is_closed B"
using assms(3) assms(5) typ_of_imp_closed by auto
have "eq_intr_ax ∈ axioms Θ"
using thy by (cases Θ rule: theory_full_exhaust) auto
hence 1: "Θ, {} ⊢ eq_intr_ax"
by (simp add: axiom' thy)
hence "Θ, {} ⊢ subst_term [((Var (STR ''A'', 0), propT), A), ((Var (STR ''B'', 0), propT), B)]
eq_intr_ax"
using assms term_ok_var propT_ok by (fastforce intro!: inst_var_multiple simp add: eq_intr_ax_def)
thus ?thesis using assms by (simp add: eq_axs_def typ_of_def)
qed
lemma proves_eq_intr:
assumes thy: "wf_theory Θ"
assumes A: "term_ok Θ A" "typ_of A = Some propT"
assumes B: "term_ok Θ B" "typ_of B = Some propT"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ (A ⟼ B) ⟼ (B ⟼ A) ⟼ mk_eq A B"
by (subst unsimp_context) (use assms proves_eq_intr_pre weaken_proves_set in blast)
lemma proves_eq_intr_rule:
assumes thy: "wf_theory Θ"
assumes A: "term_ok Θ A" "typ_of A = Some propT"
assumes B: "term_ok Θ B" "typ_of B = Some propT"
assumes "Θ, Γ ⊢ (A ⟼ B)" "Θ, Γ ⊢ (B ⟼ A)"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq A B"
proof-
note 1 = proves_eq_intr[OF assms(1-5), of Γ]
note 2 = proves.implies_elim[OF 1 assms(6)]
note 3 = proves.implies_elim[OF 2 assms(7)]
thus ?thesis using ctxt by simp
qed
lemma proves_eq_elim_pre:
assumes thy: "wf_theory Θ"
assumes A: "term_ok Θ A" "typ_of A = Some propT"
assumes B: "term_ok Θ B" "typ_of B = Some propT"
shows "Θ, {} ⊢ mk_eq A B ⟼ A ⟼ B"
proof-
have closed: "is_closed A" "is_closed B"
by (simp_all add: assms(3) assms(5) typ_of_imp_closed)
have "eq_elim_ax ∈ axioms Θ"
using thy by (cases Θ rule: theory_full_exhaust) auto
hence 1: "Θ, {} ⊢ eq_elim_ax"
by (simp add: axiom' thy)
hence "Θ, {} ⊢ subst_term [((Var (STR ''A'', 0), propT), A), ((Var (STR ''B'', 0), propT), B)]
eq_elim_ax"
using assms term_ok_var propT_ok by (fastforce intro!: inst_var_multiple simp add: eq_elim_ax_def)
thus ?thesis
using assms by (simp add: eq_axs_def typ_of_def)
qed
lemma proves_eq_elim:
assumes thy: "wf_theory Θ"
assumes A: "term_ok Θ A" "typ_of A = Some propT"
assumes B: "term_ok Θ B" "typ_of B = Some propT"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq A B ⟼ A ⟼ B"
by (subst unsimp_context) (use assms proves_eq_elim_pre weaken_proves_set in blast)
lemma proves_eq_elim_rule:
assumes thy: "wf_theory Θ"
assumes A: "term_ok Θ A" "typ_of A = Some propT"
assumes B: "term_ok Θ B" "typ_of B = Some propT"
assumes "Θ, Γ ⊢ mk_eq A B"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ A ⟼ B"
using proves.implies_elim[OF proves_eq_elim[OF assms(1-5)] assms(6), of Γ, OF ctxt] by simp
lemma proves_eq_elim2_rule:
assumes thy: "wf_theory Θ"
assumes A: "term_ok Θ A" "typ_of A = Some propT"
assumes B: "term_ok Θ B" "typ_of B = Some propT"
assumes "Θ, Γ ⊢ mk_eq A B"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ B ⟼ A"
proof-
have "Θ, Γ ⊢ mk_eq B A"
by (rule proves_eq_symmetric_rule) (use assms in simp_all)
thus ?thesis by (intro proves_eq_elim_rule) (use assms in simp_all)
qed
lemma proves_eq_combination_pre:
assumes thy: "wf_theory Θ"
assumes f: "term_ok Θ f" "typ_of f = Some (τ → τ')"
assumes g: "term_ok Θ g" "typ_of g = Some (τ → τ')"
assumes x: "term_ok Θ x" "typ_of x = Some τ"
assumes y: "term_ok Θ y" "typ_of y = Some τ"
shows "Θ, {} ⊢ mk_eq f g ⟼ mk_eq x y ⟼ mk_eq (f $ x) (g $ y)"
proof-
have ok: "typ_ok Θ τ" "typ_ok Θ (τ → τ')" "typ_ok Θ τ'"
using term_ok_betapply term_ok_imp_typ_ok thy typ_of_betaply thy x f by blast+
have "eq_combination_ax ∈ axioms Θ"
using thy by (cases Θ rule: theory_full_exhaust) auto
moreover have "typ_ok Θ τ" "typ_ok Θ τ'"
using assms term_ok_imp_typ_ok thy term_ok_betapply typ_of_betaply by meson+
ultimately have 1: "Θ, {} ⊢ subst_typ'
[((Var (STR '''a'', 0), full_sort), τ), ((Var (STR '''b'', 0), full_sort), τ')] eq_combination_ax"
using assms axiom_subst_typ' by (simp del: term_ok_def)
hence "Θ, {} ⊢ subst_term
[((Var (STR ''f'', 0), τ → τ'), f), ((Var (STR ''g'', 0), τ → τ'), g),
((Var (STR ''x'', 0), τ), x), ((Var (STR ''y'', 0), τ), y)]
(subst_typ' [((Var (STR '''a'', 0), full_sort), τ), ((Var (STR '''b'', 0), full_sort), τ')]
eq_combination_ax)"
using assms term_ok_var ok by (fastforce intro!: inst_var_multiple simp add: eq_combination_ax_def)
thus ?thesis
using assms by (simp add: eq_axs_def typ_of_def)
qed
lemma proves_eq_combination:
assumes thy: "wf_theory Θ"
assumes f: "term_ok Θ f" "typ_of f = Some (τ → τ')"
assumes g: "term_ok Θ g" "typ_of g = Some (τ → τ')"
assumes x: "term_ok Θ x" "typ_of x = Some τ"
assumes y: "term_ok Θ y" "typ_of y = Some τ"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq f g ⟼ mk_eq x y ⟼ mk_eq (f $ x) (g $ y)"
by (subst unsimp_context) (use assms proves_eq_combination_pre weaken_proves_set in blast)
lemma proves_eq_combination_rule:
assumes thy: "wf_theory Θ"
assumes f: "term_ok Θ f" "typ_of f = Some (τ → τ')"
assumes g: "term_ok Θ g" "typ_of g = Some (τ → τ')"
assumes x: "term_ok Θ x" "typ_of x = Some τ"
assumes y: "term_ok Θ y" "typ_of y = Some τ"
assumes "Θ, Γ ⊢ mk_eq f g" "Θ, Γ ⊢ mk_eq x y"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq (f $ x) (g $ y)"
proof-
note 1 = proves_eq_combination[OF assms(1-9), of Γ]
note 2 = proves.implies_elim[OF 1 assms(10)]
note 3 = proves.implies_elim[OF 2 assms(11)]
thus ?thesis using ctxt by simp
qed
lemma proves_eq_combination_rule_better:
assumes thy: "wf_theory Θ"
assumes "Θ, Γ ⊢ mk_eq f g" "Θ, Γ ⊢ mk_eq x y"
assumes f: "typ_of f = Some (τ → τ')"
assumes x: "typ_of x = Some τ"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq (f $ x) (g $ y)"
proof-
have ok_Apps: "term_ok Θ (mk_eq f g)" "term_ok Θ (mk_eq x y)"
using assms(2-3) proved_terms_well_formed_pre by auto
hence tyy: "typ_of y = Some τ" and tyg: "typ_of g = Some (τ → τ')"
using term_ok_mk_eq_same_typ thy x f term_okD1 by metis+
moreover have "term_ok Θ x" "term_ok Θ y" "term_ok Θ f" "term_ok Θ g"
using ok_Apps term_ok_mk_eqD by blast+
ultimately show ?thesis using proves_eq_combination_rule assms by simp
qed
lemma proves_eq_mp_rule:
assumes thy: "wf_theory Θ"
assumes A: "term_ok Θ A" "typ_of A = Some propT"
assumes B: "term_ok Θ B" "typ_of B = Some propT"
assumes eq: "Θ, Γ ⊢ mk_eq A B"
assumes pA: "Θ, Γ ⊢ A"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ B"
proof-
have "Θ, Γ ⊢ A ⟼ B" using proves_eq_elim_rule[OF assms(1-5) eq ctxt] .
thus "Θ, Γ ⊢ B" using proves.implies_elim pA by fastforce
qed
lemma proves_eq_mp_rule_better:
assumes thy: "wf_theory Θ"
assumes eq: "Θ, Γ ⊢ mk_eq A B"
assumes pA: "Θ, Γ ⊢ A"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ B"
by (metis ctxt eq pA proved_terms_well_formed(1) proved_terms_well_formed(2)
proves_eq_mp_rule term_ok_mk_eqD term_ok_mk_eq_same_typ thy)
lemma proves_subst_rule:
assumes thy: "wf_theory Θ"
assumes x: "term_ok Θ x" "typ_of x = Some τ"
assumes y: "term_ok Θ y" "typ_of y = Some τ"
assumes P: "term_ok Θ P" "typ_of P = Some (τ → propT)"
assumes ctxt: "finite Γ" "∀A∈Γ . term_ok Θ A" "∀A∈Γ . typ_of A = Some propT"
assumes eq: "Θ, Γ ⊢ mk_eq x y"
shows "Θ, Γ ⊢ mk_eq (P $ x) (P $ y)"
proof-
have "Θ, Γ ⊢ mk_eq P P" using assms proves_eq_reflexive by blast
thus ?thesis using proves_eq_combination_rule assms by blast
qed
lemma proves_beta_step_rule:
assumes thy: "wf_theory Θ"
assumes abs: "term_ok Θ (Abs T t)" "Θ, Γ ⊢ (Abs T t) $ x"
assumes x: "term_ok Θ x" "typ_of x = Some T"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ subst_bv x t"
proof-
have "Θ, Γ ⊢ mk_eq ((Abs T t) $ x) (subst_bv x t)"
using proves.β_conversion assms by (simp add: term_okD1)
moreover have "term_ok Θ (Abs T t $ x)" and tyAbs: "typ_of (Abs T t $ x) = Some propT"
using abs(2) proved_terms_well_formed by simp_all
moreover have tySub: "typ_of (subst_bv x t) = Some propT"
using tyAbs unfolding subst_bv_def typ_of_def
using typ_of1_subst_bv_gen' by (auto simp add: bind_eq_Some_conv split: if_splits)
moreover have "term_ok Θ (subst_bv x t)"
proof-
have "term_ok' (sig Θ) t"
using assms(2) term_ok'.simps(5) wt_term_def term_ok_def by blast
hence "term_ok' (sig Θ) (subst_bv x t)"
using term_ok'_subst_bv1 x(1) by (simp add: term_okD1 subst_bv_def)
thus ?thesis
using x(1) wt_term_def term_ok'_subst_bv1 subst_bv_def tySub term_okD1 by simp
qed
ultimately show ?thesis apply -
apply (rule proves_eq_mp_rule[where A="(Abs T t) $ x"])
using assms by simp_all
qed
lemma proves_add_param_rule:
assumes thy: "wf_theory Θ"
assumes ctxt: "finite Γ"
assumes eq: "Θ, Γ ⊢ mk_eq f g" "typ_of f = Some (τ → τ')"
assumes type: "typ_ok Θ τ"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ (Ct STR ''Pure.all'' ((τ → propT) → propT) $
(Abs τ (mk_eq' τ' (f $ Bv 0) (g $ Bv 0))))"
proof-
have term_ok: "term_ok Θ (mk_eq f g)"
using eq(1) proved_terms_well_formed_pre by blast
hence term_ok': "term_ok Θ f" "term_ok Θ g"
apply (simp add: eq(2) wt_term_def)
using ‹term_ok Θ (mk_eq f g)› wt_term_def typ_of_def term_ok_app_eqD by blast
hence "typ_of f = typ_of g"
using thy term_ok by (cases Θ rule: theory_full_exhaust)
(auto simp add: tinstT_def typ_of_def wt_term_def bind_eq_Some_conv)
hence type': "typ_of g = Some (τ → τ')"
using eq(2) by simp
obtain x where "x ∉ fst ` (fv (mk_eq f g) ∪ FV Γ)"
using finite_fv finite_FV infinite_fv_UNIV variant_variable_fresh ctxt
by (meson finite_Un finite_imageI)
hence free: "(x,τ) ∉ fv (mk_eq f g) ∪ FV Γ"
by force
hence "Θ, Γ ⊢ mk_eq (Fv x τ) (Fv x τ)"
using ctxt proves_eq_reflexive term_ok_var thy type by presburger
hence "Θ, Γ ⊢ mk_eq (f $ Fv x τ) (g $ Fv x τ)"
apply -
apply (rule proves_eq_combination_rule[where τ'=τ'])
using assms term_ok' type' by (simp_all del: term_ok_def)
hence "Θ, Γ ⊢ mk_all x τ (mk_eq (f $ Fv x τ) (g $ Fv x τ))"
apply -
apply (rule proves.forall_intro)
using thy eq type free by simp_all
moreover have "mk_all x τ (mk_eq (f $ Fv x τ) (g $ Fv x τ))
= (Ct STR ''Pure.all'' ((τ → propT) → propT) $
(Abs τ (mk_eq' τ' (f $ Bv 0) (g $ Bv 0))))"
using free eq type type' bind_fv2_changed
by (fastforce simp add: bind_fv_def bind_fv_unchanged typ_of_def)
ultimately show ?thesis
by simp
qed
lemma proves_add_abs_rule:
assumes thy: "wf_theory Θ"
assumes ctxt: "finite Γ"
assumes eq: "Θ, Γ ⊢ mk_eq f g" "typ_of f = Some (τ → τ')"
assumes type: "typ_ok Θ τ"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq (Abs τ (f $ Bv 0)) (Abs τ (g $ Bv 0))"
proof-
have ok: "term_ok Θ f" "term_ok Θ g"
using eq(1) proved_terms_well_formed(2) term_ok_mk_eqD by blast+
have g_ty: "typ_of g = Some (τ → τ')"
by (metis eq(1) eq(2) proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy)
hence closed: "is_closed f" "is_closed g"
using eq(2) typ_of_imp_closed by blast+
have ok': "term_ok Θ (Abs τ (f $ Bv 0))" "term_ok Θ (Abs τ (g $ Bv 0))"
using type term_ok_eta_expand ok thy eq(2) g_ty by blast+
have ok_ind: "wf_term (sig Θ) f" "wf_term (sig Θ) g"
using ok wt_term_def by simp_all
note 1 = proves.eta[OF thy ok_ind(1) typ_of_imp_has_typ[OF eq(2)], of Γ]
note 2 = proves.eta[OF thy ok_ind(2) typ_of_imp_has_typ[OF g_ty], of Γ]
have simp': "subst_bv x f = f" "subst_bv x g = g" for x
using ok term_ok_subst_bv_no_change by auto
have s2: "Θ,Γ ⊢ mk_eq g (Abs τ (g $ Bv 0))"
apply (rule proves_eq_symmetric_rule)
using "2" ok'(2) ok(2) thy typ_of_eta_expand[OF g_ty] g_ty ctxt by (simp_all add: simp'(2))
have tr1: "Θ,Γ ⊢ mk_eq (Abs τ (f $ Bv 0)) g"
using 1 eq(1) g_ty ok'(1) ok(1) ok(2) proves_eq_transitive_rule[OF thy _ _ _ _ _ _ _ ctxt]
typ_of_eta_expand[OF eq(2)] eq(2) by (fastforce simp add: simp'(1))
show ?thesis
using tr1 s2 proves_eq_transitive_rule[OF thy ok'(1) ok(2) ok'(2)] typ_of_eta_expand eq(2) g_ty
ctxt
by simp
qed
lemma proves_inst_bound_rule:
assumes thy: "wf_theory Θ"
assumes ctxt: "finite Γ" "∀A∈Γ . term_ok Θ A" "∀A∈Γ . typ_of A = Some propT"
assumes eq: "Θ, Γ ⊢ mk_eq (Abs τ f) (Abs τ g)" "typ_of (Abs τ f) = Some (τ → τ')"
assumes x: "term_ok Θ x" "typ_of x = Some τ"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq (subst_bv x f) (subst_bv x g)"
proof-
have "term_ok Θ (mk_eq (Abs τ f) (Abs τ g))"
using eq(1) proved_terms_well_formed(2) by blast
hence "term_ok Θ (Abs τ f)" "term_ok Θ (Abs τ g)"
using term_ok_mk_eqD by blast+
hence "typ_of (Abs τ f) = typ_of (Abs τ g)"
using thy ‹term_ok Θ (mk_eq (Abs τ f) (Abs τ g))› by (cases Θ rule: theory_full_exhaust)
(auto simp add: tinstT_def typ_of_def wt_term_def bind_eq_Some_conv)
hence "typ_of (Abs τ g) = Some (τ → τ')"
using eq(2) by simp
have "Θ, Γ ⊢ mk_eq x x"
by (simp add: ctxt proves_eq_reflexive thy x(1) del: term_ok_def)
hence 1: "Θ, Γ ⊢ mk_eq (Abs τ f $ x) (Abs τ g $ x)"
using proves_eq_combination_rule[OF thy ‹term_ok Θ (Abs τ f)› eq(2) ‹term_ok Θ (Abs τ g)›
‹typ_of (Abs τ g) = Some (τ → τ')› x x eq(1) _ ctxt]
by blast
have "Θ, Γ ⊢ mk_eq (Abs τ f $ x) (subst_bv x f)"
apply (rule β_conversion)
using thy x ‹term_ok Θ (Abs τ f)› by (simp_all add: wt_term_def)
have "term_ok Θ (Abs τ f $ x)" using ‹term_ok Θ (Abs τ f)› x
‹Θ,Γ ⊢ mk_eq (Abs τ f $ x) (Abs τ g $ x)› proved_terms_well_formed(1)
wt_term_def typ_of1_split_App_obtains typ_of_def
by (meson proved_terms_well_formed(2) term_ok_mk_eqD)
have "term_ok Θ (Abs τ g $ x)" using ‹term_ok Θ (Abs τ g)› x
‹Θ,Γ ⊢ mk_eq (Abs τ f $ x) (Abs τ g $ x)› proved_terms_well_formed(1)
wt_term_def typ_of1_split_App_obtains typ_of_def
by (meson proved_terms_well_formed(2) term_ok_mk_eqD)
have "typ_of (subst_bv x f) = Some τ'"
using ‹typ_of (Abs τ f) = Some (τ → τ')› x(2) typ_of_def typ_of_betapply by auto
moreover have "term_ok' (sig Θ) (subst_bv x f)"
using ‹term_ok Θ (Abs τ f)› substn_subst_0' term_ok'_subst_bv2 wt_term_def x(1) by auto
ultimately have "term_ok Θ (subst_bv x f)"
by (simp add: wt_term_def)
have "typ_of (Abs τ f $ x) = typ_of (subst_bv x f)"
using ‹typ_of (Abs τ f) = typ_of (Abs τ g)› typ_of_def ‹typ_of (Abs τ g) = Some (τ → τ')›
‹typ_of (subst_bv x f) = Some τ'› typ_of_Abs_body_typ' x(2) by fastforce
have "typ_of (Abs τ f $ x) = typ_of (Abs τ g $ x)"
using ‹typ_of (Abs τ f) = typ_of (Abs τ g)› typ_of_def by auto
have 2: "Θ, Γ ⊢ mk_eq (subst_bv x f) (Abs τ f $ x)"
apply - apply (rule proves_eq_symmetric_rule)
using thy apply blast
using ‹term_ok Θ (subst_bv x f)› apply blast
using ‹term_ok Θ (Abs τ f $ x)› apply blast
using ‹typ_of (Abs τ f $ x) = typ_of (subst_bv x f)› apply blast
using ‹Θ,Γ ⊢ mk_eq (Abs τ f $ x) (subst_bv x f)› apply blast
using ctxt by blast+
have 3: "Θ, Γ ⊢ mk_eq (Abs τ g $ x) (subst_bv x g)"
apply (rule β_conversion)
using thy x ‹term_ok Θ (Abs τ g)› by (simp_all add: wt_term_def)
have "term_ok Θ (subst_bv x g)"
using ‹term_ok Θ (Abs τ g $ x)› ‹term_ok Θ (Abs τ g)› ‹typ_of (Abs τ f $ x) = typ_of (Abs τ g $ x)›
‹typ_of (Abs τ f $ x) = typ_of (subst_bv x f)› ‹typ_of (Abs τ g) = Some (τ → τ')›
‹typ_of (subst_bv x f) = Some τ'› betapply.simps(1) subst_bv_def term_ok'.simps(5)
term_ok'_subst_bv1 wt_term_def typ_of_betaply x(1) x(2)
by (meson "3" proved_terms_well_formed(2) term_ok_mk_eqD)
have "typ_of (subst_bv x f) = typ_of (Abs τ g $ x)"
using ‹typ_of (Abs τ f $ x) = typ_of (Abs τ g $ x)›
‹typ_of (Abs τ f $ x) = typ_of (subst_bv x f)› by auto
have "typ_of (Abs τ g $ x) = typ_of (subst_bv x g)"
using ‹typ_of (Abs τ f) = typ_of (Abs τ g)› eq(2) typ_of_betapply typ_of_def x(2) by auto
have c1: "Θ, Γ ⊢ mk_eq (subst_bv x f) (Abs τ g $ x)"
apply (rule proves_eq_transitive_rule[where t="Abs τ f $ x"];
(use assms 1 2 ‹term_ok Θ (subst_bv x f)› in ‹solves simp›)?)
using ‹term_ok Θ (Abs τ f $ x)› apply blast
using ‹term_ok Θ (Abs τ g $ x)› apply blast
using ‹typ_of (Abs τ f $ x) = typ_of (subst_bv x f)› apply simp
using ‹typ_of (Abs τ f $ x) = typ_of (Abs τ g $ x)› apply blast
done
show ?thesis
apply (rule proves_eq_transitive_rule[where t="Abs τ g $ x"];
(use assms 1 2 ‹term_ok Θ (subst_bv x f)› in ‹solves simp›)?)
using ‹term_ok Θ (Abs τ g $ x)›
‹term_ok Θ (subst_bv x g)›
‹typ_of (subst_bv x f) = typ_of (Abs τ g $ x)›
‹typ_of (Abs τ g $ x) = typ_of (subst_bv x g)›
‹Θ,Γ ⊢ mk_eq (subst_bv x f) (Abs τ g $ x)›
‹Θ,Γ ⊢ mk_eq (Abs τ g $ x) (subst_bv x g)› by simp_all
qed
lemma proves_descend_abs_rule:
assumes thy: "wf_theory Θ"
assumes eq: "Θ, Γ ⊢ mk_eq (Abs τ' (bind_fv (x, τ') s)) (Abs τ' (bind_fv (x, τ') t))"
"is_closed s" "is_closed t"
assumes x: "(x, τ') ∉ FV Γ" "typ_ok Θ τ'"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq s t"
proof-
have abs_ok: "term_ok Θ (Abs_fv x τ' s)" "term_ok Θ (Abs_fv x τ' t)"
using eq proved_terms_well_formed wt_term_def typ_of1_split_App typ_of_def
by (meson term_ok_mk_eqD)+
obtain τ where τ1: "typ_of (Abs_fv x τ' s) = Some (τ' → τ)"
by (smt eq proved_terms_well_formed_pre typ_of1_split_App_obtains typ_of_Abs_body_typ' typ_of_def)
hence τ2: "typ_of (Abs_fv x τ' t) = Some (τ' → τ)"
by (metis eq(1) proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy)
have add_param: "Θ, Γ ⊢ mk_eq
(Abs τ' (bind_fv (x, τ') s) $ Fv x τ')
(Abs τ' (bind_fv (x, τ') t) $ Fv x τ')"
apply(rule proves_eq_combination_rule; use assms abs_ok τ1 τ2 in ‹(solves simp)?›)
using proves_eq_reflexive term_ok_var thy x(2) wt_term_def ctxt by blast+
have βs: "Θ, Γ ⊢ mk_eq
(Abs τ' (bind_fv (x, τ') s) $ Fv x τ')
(subst_bv (Fv x τ') (bind_fv (x, τ') s))"
by (rule proves.β_conversion; use assms abs_ok τ1 τ2 in ‹(solves ‹simp add: wt_term_def›)?›)
moreover have simps: "subst_bv (Fv x τ') (bind_fv (x, τ') s) = s"
using subst_bv_bind_fv typ_of_imp_closed eq(2) by blast
ultimately have βs: "Θ, Γ ⊢ mk_eq (Abs τ' (bind_fv (x, τ') s) $ Fv x τ') s"
by simp
have t1: "term_ok Θ s"
using βs proved_terms_well_formed(2) wt_term_def typ_of_def
using term_ok_app_eqD by blast
have t2: "term_ok Θ (Abs_fv x τ' s $ term.Fv x τ')"
using βs ‹term_ok Θ s› proved_terms_well_formed(2) term_ok'.simps(4)
wt_term_def term_ok_mk_eq_same_typ thy
by (meson term_ok_mk_eqD)
have βs_rev: "Θ, Γ ⊢ mk_eq s (Abs τ' (bind_fv (x, τ') s) $ Fv x τ')"
apply (rule proves_eq_symmetric_rule; use assms abs_ok τ1 τ2 t1 t2 in ‹(solves simp)?›)
using βs proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy apply blast
using βs by simp
have βt: "Θ, Γ ⊢ mk_eq
(Abs τ' (bind_fv (x, τ') t) $ Fv x τ')
(subst_bv (Fv x τ') (bind_fv (x, τ') t))"
by (rule proves.β_conversion; use assms abs_ok τ1 τ2 t1 t2 in ‹(solves ‹simp add: wt_term_def›)?›)
moreover have simpt: "subst_bv (Fv x τ') (bind_fv (x, τ') t) = t"
using subst_bv_bind_fv typ_of_imp_closed eq(3) by blast
ultimately have βt: "Θ, Γ ⊢ mk_eq (Abs τ' (bind_fv (x, τ') t) $ Fv x τ') t"
by simp
have t3: "term_ok Θ (Abs_fv x τ' t $ term.Fv x τ')"
using βs add_param proved_terms_well_formed(2) t1 term_ok'.simps(4)
wt_term_def term_ok_mk_eq_same_typ thy
by (meson term_ok_mk_eqD)
have t4: "typ_of s = typ_of (Abs_fv x τ' t $ term.Fv x τ')"
by (metis βs add_param proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy)
have t5: "typ_of s = typ_of (Abs_fv x τ' s $ Fv x τ')"
using βs_rev proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy by blast
have t6: "typ_of (Abs_fv x τ' s $ Fv x τ') = typ_of (Abs_fv x τ' t $ term.Fv x τ')"
using t4 t5 by auto
have half: "Θ, Γ ⊢ mk_eq s (Abs τ' (bind_fv (x, τ') t) $ Fv x τ')"
apply (rule proves_eq_transitive_rule[where t="Abs τ' (bind_fv (x, τ') s) $ Fv x τ'"]
; use assms abs_ok τ1 τ2 t1 t2 t3 t4 t5 t6 in ‹(solves simp)?›)
using βs_rev apply blast
using add_param by blast
have t7: "term_ok Θ t"
using βt proved_terms_well_formed(2) t1 t4 term_ok'.simps(4) wt_term_def term_ok_mk_eq_same_typ thy
by (meson term_ok_app_eqD)
have t8: "typ_of (Abs_fv x τ' t $ term.Fv x τ') = typ_of t"
using βt proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy by blast
show ?thesis
apply (rule proves_eq_transitive_rule[where t="Abs τ' (bind_fv (x, τ') t) $ Fv x τ'"]
; use assms abs_ok τ1 τ2 t1 t2 t3 t4 t5 t6 t7 t8 in ‹(solves simp)?›)
using half apply blast
using βt by blast
qed
lemma obtain_fresh_variable:
assumes "finite Γ"
obtains x where "(x,τ) ∉ fv t ∪ FV Γ"
using assms finite_fv finite_FV
by (metis finite_Un finite_imageI fst_conv image_eqI variant_variable_fresh)
lemma obtain_fresh_variable':
assumes "finite Γ"
obtains x where "(x,τ) ∉ fv t ∪ fv u ∪ FV Γ"
using assms finite_fv finite_FV
by (metis finite_Un finite_imageI fst_conv image_eqI variant_variable_fresh)
lemma proves_eq_abstract_rule_pre:
assumes thy: "wf_theory Θ"
assumes A: "term_ok Θ f" "typ_of f = Some (τ → τ')"
assumes B: "term_ok Θ g" "typ_of g = Some (τ → τ')"
shows "Θ, {} ⊢ (Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ (mk_eq' τ' (f $ Bv 0) (g $ Bv 0)))
⟼ mk_eq (Abs τ (f $ Bv 0)) (Abs τ (g $ Bv 0))"
proof-
have "eq_abstract_rule_ax ∈ axioms Θ"
using thy by (cases Θ rule: theory_full_exhaust) auto
moreover have ok2: "typ_ok Θ (τ → τ')"
using assms(2) assms(3) term_ok_imp_typ_ok thy by blast
moreover hence ok3: "typ_ok Θ τ'"
using thy A(2) by (cases Θ rule: theory_full_exhaust) auto
moreover have ok1: "typ_ok Θ τ"
using thy A(2) ok2 by (cases Θ rule: theory_full_exhaust) auto
ultimately have 1: "Θ, {} ⊢ subst_typ'
[((Var (STR '''a'', 0), full_sort), τ), ((Var (STR '''b'', 0), full_sort), τ')] eq_abstract_rule_ax"
using assms axiom_subst_typ' by (simp del: term_ok_def)
hence "Θ, {} ⊢ subst_term [((Var (STR ''g'', 0), τ → τ'), g),
((Var (STR ''f'', 0), τ → τ'), f)] (subst_typ'
[((Var (STR '''a'', 0), full_sort), τ), ((Var (STR '''b'', 0), full_sort), τ')] eq_abstract_rule_ax)"
using ok1 ok2 ok3 assms term_ok_var by (fastforce intro!: inst_var_multiple simp add: eq_abstract_rule_ax_def)
moreover have "subst_term [((Var (STR ''g'', 0), τ → τ'), g),
((Var (STR ''f'', 0), τ → τ'), f)] (subst_typ'
[((Var (STR '''a'', 0), full_sort), τ), ((Var (STR '''b'', 0), full_sort), τ')] eq_abstract_rule_ax)
= (Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ (mk_eq' τ' (f $ Bv 0) (g $ Bv 0)))
⟼ mk_eq (Abs τ (f $ Bv 0)) (Abs τ (g $ Bv 0))"
using assms typ_of1_weaken_Ts by (fastforce simp add: eq_axs_def typ_of_def)
ultimately show ?thesis
using assms by simp
qed
lemma proves_eq_abstract_rule:
assumes thy: "wf_theory Θ"
assumes A: "term_ok Θ f" "typ_of f = Some (τ → τ')"
assumes B: "term_ok Θ g" "typ_of g = Some (τ → τ')"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ (Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ (mk_eq' τ' (f $ Bv 0) (g $ Bv 0)))
⟼ mk_eq (Abs τ (f $ Bv 0)) (Abs τ (g $ Bv 0))"
by (subst unsimp_context) (use assms proves_eq_abstract_rule_pre weaken_proves_set in blast)
lemma proves_eq_abstract_rule_rule:
assumes thy: "wf_theory Θ"
assumes A: "term_ok Θ f" "typ_of f = Some (τ → τ')"
assumes B: "term_ok Θ g" "typ_of g = Some (τ → τ')"
assumes "Θ, Γ ⊢ (Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ (mk_eq' τ' (f $ Bv 0) (g $ Bv 0)))"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq (Abs τ (f $ Bv 0)) (Abs τ (g $ Bv 0))"
proof-
note 1 = proves_eq_abstract_rule[where Γ=Γ, OF assms(1-5) ctxt]
note 2 = proves.implies_elim[OF 1 assms(6)]
thus ?thesis using ctxt by simp
qed
lemma proves_eq_ext_rule:
assumes thy: "wf_theory Θ"
assumes f: "term_ok Θ f" "typ_of f = Some (τ → τ')"
assumes g: "term_ok Θ g" "typ_of g = Some (τ → τ')"
assumes prem: "Θ, Γ ⊢ Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ (mk_eq' τ' (f $ Bv 0) (g $ Bv 0))"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq f g"
proof-
obtain x where x: "(x,τ) ∉ FV Γ" "(x,τ) ∉ fv f" "(x,τ) ∉ fv g"
by (meson Un_iff ctxt(1) obtain_fresh_variable')
have closed: "is_closed f" "is_closed g"
using f g has_typ_imp_closed term_ok_def wt_term_def by blast+
have "term_ok Θ (Abs τ (mk_eq' τ' (f $ Bv 0) (g $ Bv 0)))"
using prem proved_terms_well_formed(2) term_ok_app_eqD by blast
have "subst_bv (Fv x τ) (f $ Bv 0) = f $ Fv x τ"
using Core.subst_bv_def f(1) term_ok_subst_bv_no_change by auto
moreover have "subst_bv (Fv x τ) (g $ Bv 0) = g $ Fv x τ"
using Core.subst_bv_def g(1) term_ok_subst_bv_no_change by auto
ultimately have "subst_bv (Fv x τ) (mk_eq' τ' (f $ Bv 0) (g $ Bv 0))
= mk_eq' τ' (f $ Fv x τ) (g $ Fv x τ)"
by (simp add: Core.subst_bv_def)
hence simp: "Abs τ (mk_eq' τ' (f $ Bv 0) (g $ Bv 0)) ∙ Fv x τ = mk_eq (f $ Fv x τ) (g $ Fv x τ)"
using f g by (auto simp add: typ_of_def)
hence simp': "subst_bv (Fv x τ) (mk_eq' τ' (f $ Bv 0) (g $ Bv 0)) = mk_eq' τ' (f $ Fv x τ) (g $ Fv x τ)"
using f g by (auto simp add: typ_of_def)
have "Θ, Γ ⊢ mk_eq' τ' (f $ Fv x τ) (g $ Fv x τ)"
apply (subst simp'[symmetric])
apply (rule forall_elim[where τ=τ])
using prem apply blast
apply simp
using ‹term_ok Θ (Abs τ (mk_eq' τ' (f $ Bv 0) (g $ Bv 0)))› term_ok'.simps(1) term_ok'.simps(5) term_okD1 by blast
moreover have "typ_of (f $ Fv x τ) = Some τ'" "typ_of (g $ Fv x τ) = Some τ'"
using f(2) g(2) by (simp_all add: typ_of_def)
ultimately have 1: "Θ, Γ ⊢ mk_eq (f $ Fv x τ) (g $ Fv x τ)"
by simp
have core: "Θ, Γ ⊢ mk_eq (Abs τ (f $ Bv 0)) (Abs τ (g $ Bv 0))"
apply (rule proves_eq_abstract_rule_rule[OF thy f g _ ctxt])
using prem by blast
have "Θ, Γ ⊢ mk_eq (Abs τ (f $ Bv 0)) f"
using f proves.eta term_okD1 thy by blast
have left: "Θ, Γ ⊢ mk_eq f (Abs τ (f $ Bv 0))"
apply (rule proves_eq_symmetric_rule[OF thy f(1) _ _ _ ctxt])
using ‹Θ,Γ ⊢ mk_eq (Abs τ (f $ Bv 0)) (Abs τ (g $ Bv 0))› proved_terms_well_formed(2) term_ok_mk_eqD apply blast
apply (simp add: Logic.typ_of_eta_expand f(2))
using ‹Θ,Γ ⊢ mk_eq (Abs τ (f $ Bv 0)) f› by blast
have right: "Θ, Γ ⊢ mk_eq (Abs τ (g $ Bv 0)) g"
using g proves.eta term_okD1 thy by blast
show ?thesis
apply (rule proves_eq_transitive_rule[where t="Abs τ (f $ Bv 0)", OF thy f(1) _ g(1) _ _ left _ ctxt])
using ‹Θ,Γ ⊢ mk_eq (Abs τ (f $ Bv 0)) f› proved_terms_well_formed(2) term_ok_mk_eqD apply blast
apply (simp add: Logic.typ_of_eta_expand f(2))
apply (simp add: Logic.typ_of_eta_expand f(2) g(2))
apply (rule proves_eq_transitive_rule[where t="Abs τ (g $ Bv 0)", OF thy _ _ g(1) _ _ core right ctxt])
using ‹Θ,Γ ⊢ mk_eq (Abs τ (f $ Bv 0)) f› proved_terms_well_formed(2) term_ok_mk_eqD apply blast
using ‹Θ,Γ ⊢ mk_eq (Abs τ (g $ Bv 0)) g› proved_terms_well_formed(2) term_ok_mk_eqD apply blast
by (simp add: Logic.typ_of_eta_expand f(2) g(2))+
qed
lemma bind_fv2_idem[simp]:
"bind_fv2 (x, τ) lev1 (bind_fv2 (x, τ) lev2 t) = bind_fv2 (x, τ) lev2 t "
by (induction "(x,τ)" lev2 t arbitrary: lev1 rule: bind_fv2.induct) auto
corollary bind_fv_idem[simp]:
"bind_fv (x, τ) (bind_fv (x, τ) t) = bind_fv (x, τ) t "
using bind_fv_def bind_fv2_idem by simp
corollary bind_fv_Abs_fv[simp]: "bind_fv (x, τ) (Abs_fv x τ t) = Abs_fv x τ t"
by (simp add: bind_fv_def)
lemma "bind_fv2 (x,τ) lev (mk_eq' τ' s t) = mk_eq' τ' (bind_fv2 (x,τ) lev s) (bind_fv2 (x,τ) lev t)"
by simp
lemma "bind_fv (x,τ) (mk_eq' τ' s t) = mk_eq' τ' (bind_fv (x,τ) s) (bind_fv (x,τ) t)"
by (simp add: bind_fv_def)
lemma term_ok_Abs_fvI: "term_ok Θ s ⟹ typ_ok Θ τ ⟹ term_ok Θ (Abs_fv x τ s)"
by (auto simp add: wt_term_def term_ok'_bind_fv typ_of_Abs_bind_fv)
lemma proves_eq_abstract_rule_derived_rule:
assumes thy: "wf_theory Θ"
assumes x: "(x, τ) ∉ FV Γ" "typ_ok Θ τ"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
assumes eq: "Θ, Γ ⊢ mk_eq s t"
shows "Θ, Γ ⊢ mk_eq (Abs τ (bind_fv (x, τ) s)) (Abs τ (bind_fv (x, τ) t))"
proof-
obtain τ' where s: "typ_of s = Some τ'"
by (meson eq option.exhaust_sel proved_terms_well_formed(2) term_okD2 term_ok_app_eqD)
have t: "typ_of t = Some τ'"
by (metis eq proved_terms_well_formed(2) s term_ok_mk_eq_same_typ thy)
have ok: "term_ok Θ s" "term_ok Θ t"
using eq proved_terms_well_formed(2) term_ok_mk_eqD by blast+
have closed: "is_closed s" "is_closed t"
using eq has_typ_imp_closed proved_terms_well_formed(2) term_ok_def term_ok_mk_eqD wt_term_def by blast+
have "is_closed (mk_eq s t)"
using eq proved_terms_closed by blast
hence "Abs τ (bind_fv (x, τ) (mk_eq s t)) ∙ Fv x τ = mk_eq s t"
using betapply_Abs_fv by auto
have "Θ, Γ ⊢ mk_all x τ (mk_eq s t)"
using eq forall_intro thy typ_ok_def x(1) x(2) by blast
have "Θ, Γ ⊢ mk_eq (Abs τ (bind_fv (x, τ) s) $ Fv x τ) (subst_bv (Fv x τ) (bind_fv (x, τ) s))"
using term_ok_Abs_fvI[OF ok(1) x(2)] wf_term.intros(1) typ_ok_def x(2)
by (auto intro!: β_conversion[OF thy])
moreover have "subst_bv (Fv x τ) (bind_fv (x, τ) s) = s"
by (simp add: closed(1) subst_bv_bind_fv)
ultimately have unfs: "Θ, Γ ⊢ mk_eq (Abs τ (bind_fv (x, τ) s) $ Fv x τ) s"
by simp
have "Θ, Γ ⊢ mk_eq (Abs τ (bind_fv (x, τ) t) $ Fv x τ) (subst_bv (Fv x τ) (bind_fv (x, τ) t))"
using term_ok_Abs_fvI[OF ok(2) x(2)] wf_term.intros(1) typ_ok_def x(2)
by (auto intro!: β_conversion[OF thy])
moreover have "subst_bv (Fv x τ) (bind_fv (x, τ) t) = t"
by (simp add: closed(2) subst_bv_bind_fv)
ultimately have unft: "Θ, Γ ⊢ mk_eq (Abs τ (bind_fv (x, τ) t) $ Fv x τ) t"
by simp
have prem:
"Θ, Γ ⊢ mk_eq (Abs τ (bind_fv (x, τ) s) $ Fv x τ) (Abs τ (bind_fv (x, τ) t) $ Fv x τ)"
apply (rule proves_eq_transitive_rule[where t=s, OF thy _ _ _ _ _ _ _ ctxt])
using ok(1) term_ok_mk_eqD unfs unft proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy
apply (all blast)[4]
apply (metis proved_terms_well_formed(2) s t term_ok_mk_eq_same_typ thy unft)
using unfs apply blast
subgoal
apply (rule proves_eq_transitive_rule[where t=t, OF thy ok _ _ _ _ _ ctxt])
using proved_terms_well_formed(2) term_ok_mk_eqD unft apply blast
apply (simp add: s t)
apply (metis proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy unft)
using eq apply simp
subgoal apply (rule proves_eq_symmetric_rule[OF thy ok(2) _ _ _ ctxt])
using proved_terms_well_formed(2) term_ok_mk_eqD unft apply blast
using proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy unft apply blast
using unft apply blast
done
done
done
hence "Θ, Γ ⊢ mk_all x τ
(mk_eq (Abs τ (bind_fv (x, τ) s) $ Fv x τ) (Abs τ (bind_fv (x, τ) t) $ Fv x τ))"
using forall_intro thy typ_ok_def x(1) x(2) by blast
moreover have "mk_all x τ
(mk_eq (Abs τ (bind_fv (x, τ) s) $ Fv x τ) (Abs τ (bind_fv (x, τ) t) $ Fv x τ))
= mk_all x τ
(mk_eq' τ' (Abs τ (bind_fv (x, τ) s) $ Fv x τ) (Abs τ (bind_fv (x, τ) t) $ Fv x τ))"
using bind_fv2_preserves_type s t typ_of_def by (fastforce simp add: bind_fv_def typ_of_def)+
moreover have "mk_all x τ
(mk_eq' τ' (Abs τ (bind_fv (x, τ) s) $ Fv x τ) (Abs τ (bind_fv (x, τ) t) $ Fv x τ)) =
Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ
(mk_eq' τ' (Abs τ (bind_fv (x, τ) s) $ Bv 0) (Abs τ (bind_fv (x, τ) t) $ Bv 0))"
by (simp add: bind_fv_def)
ultimately have pre_ext: "Θ, Γ ⊢ Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ
(mk_eq' τ' (Abs τ (bind_fv (x, τ) s) $ Bv 0) (Abs τ (bind_fv (x, τ) t) $ Bv 0))"
by simp
show ?thesis
apply (rule proves_eq_ext_rule[where τ=τ and τ'=τ', OF thy _ _ _ _ _ ctxt])
using proved_terms_well_formed(2) term_ok_app_eqD unfs apply blast
apply (simp add: s typ_of_Abs_bind_fv)
using proved_terms_well_formed(2) term_ok_app_eqD unft apply blast
apply (simp add: t typ_of_Abs_bind_fv)
using pre_ext by blast
qed
lemma proves_descend_abs_rule_iff:
assumes thy: "wf_theory Θ"
assumes ok: "is_closed s" "is_closed t"
assumes x: "(x, τ') ∉ FV Γ" "typ_ok Θ τ'"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq s t
⟷ Θ, Γ ⊢ mk_eq (Abs τ' (bind_fv (x, τ') s)) (Abs τ' (bind_fv (x, τ') t))"
proof (rule iffI)
assume asm: "Θ,Γ ⊢ mk_eq s t"
hence "term_ok Θ s" "term_ok Θ t"
using proved_terms_well_formed(2) term_ok_mk_eqD by blast+
show "Θ,Γ ⊢ mk_eq (Abs_fv x τ' s) (Abs_fv x τ' t)"
by (rule proves_eq_abstract_rule_derived_rule[OF thy x ctxt asm])
next
assume asm: "Θ,Γ ⊢ mk_eq (Abs_fv x τ' s) (Abs_fv x τ' t)"
show "Θ,Γ ⊢ mk_eq s t"
using assms asm proves_descend_abs_rule by blast
qed
lemma proves_descend_abs_rule':
assumes thy: "wf_theory Θ"
assumes eq: "Θ, Γ ⊢ mk_eq (Abs τ' s) (Abs τ' t)"
assumes x: "(x, τ') ∉ FV Γ" "typ_ok Θ τ'"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq (subst_bv (Fv x τ') s) (subst_bv (Fv x τ') t)"
proof-
have abs_ok: "term_ok Θ (Abs τ' s)" "term_ok Θ (Abs τ' t)"
using eq(1) option.distinct(1) proved_terms_well_formed term_ok'.simps(4)
wt_term_def typ_of1_split_App typ_of_def
by (smt term_ok_mk_eqD)+
obtain τ where τ1: "typ_of (Abs τ' s) = Some (τ' → τ)"
by (smt eq proved_terms_well_formed_pre typ_of1_split_App_obtains typ_of_Abs_body_typ' typ_of_def)
hence τ2: "typ_of (Abs τ' t)= Some (τ' → τ)"
by (metis eq(1) proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy)
have add_param: "Θ, Γ ⊢ mk_eq
(Abs τ' s $ Fv x τ')
(Abs τ' t $ Fv x τ')"
apply (rule proves_eq_combination_rule; use assms abs_ok τ1 τ2 in ‹(solves ‹simp del: term_ok_def›)?›)
using proves_eq_reflexive term_ok_var thy x(2) ctxt by blast
have βs: "Θ, Γ ⊢ mk_eq
(Abs τ' s $ Fv x τ')
(subst_bv (Fv x τ') s)"
by (rule proves.β_conversion; use assms abs_ok τ1 τ2 in ‹(solves ‹simp add: wt_term_def›)?›)
have t1: "term_ok Θ (subst_bv (Fv x τ') s)"
using βs proved_terms_well_formed(2) wt_term_def typ_of_def
using term_ok_mk_eqD by blast
have t2: "term_ok Θ (Abs τ' s $ term.Fv x τ')"
using βs proved_terms_well_formed(2) t1 term_ok'.simps(4) wt_term_def term_ok_mk_eq_same_typ thy
term_ok_mk_eqD by blast
have βs_rev: "Θ, Γ ⊢ mk_eq (subst_bv (Fv x τ') s) (Abs τ' s $ Fv x τ')"
apply (rule proves_eq_symmetric_rule; use assms abs_ok τ1 τ2 t1 t2 in ‹(solves simp)?›)
using βs proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy apply blast
using βs by simp
have βt: "Θ, Γ ⊢ mk_eq
(Abs τ' t $ Fv x τ')
(subst_bv (Fv x τ') t)"
by (rule proves.β_conversion; use assms abs_ok τ1 τ2 t1 in ‹(solves ‹simp add: wt_term_def›)?›)
have t3: "term_ok Θ (Abs τ' t $ term.Fv x τ')"
using βs add_param proved_terms_well_formed(2) t1 term_ok'.simps(4)
wt_term_def term_ok_mk_eq_same_typ thy term_ok_mk_eqD
by meson
have t4: "typ_of (subst_bv (Fv x τ') s) = typ_of (Abs τ' t $ term.Fv x τ')"
by (metis βs add_param proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy)
have t5: "typ_of (subst_bv (Fv x τ') s) = typ_of (Abs τ' s $ Fv x τ')"
using βs_rev proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy by blast
have t6: "typ_of (Abs τ' s $ Fv x τ') = typ_of (Abs τ' t $ term.Fv x τ')"
using t4 t5 by auto
have half: "Θ, Γ ⊢ mk_eq (subst_bv (Fv x τ') s) (Abs τ' t $ Fv x τ')"
apply (rule proves_eq_transitive_rule[where t="Abs τ' s $ Fv x τ'"]
; use assms abs_ok τ1 τ2 t1 t2 t3 t4 t5 t6 in ‹(solves simp)?›)
using βs_rev apply blast
using add_param by blast
have t7: "term_ok Θ (subst_bv (Fv x τ') t)"
using βt proved_terms_well_formed(2) t1 t4 term_ok'.simps(4) wt_term_def term_ok_mk_eq_same_typ thy
by (meson term_ok_app_eqD)
have t8: "typ_of (Abs τ' t $ term.Fv x τ') = typ_of (subst_bv (Fv x τ') t)"
using βt proved_terms_well_formed(2) term_ok_mk_eq_same_typ thy by blast
show ?thesis
apply (rule proves_eq_transitive_rule[where t="Abs τ' t $ Fv x τ'"]
; use assms abs_ok τ1 τ2 t1 t2 t3 t4 t5 t6 t7 t8 in ‹(solves simp)?›)
using half apply blast
using βt by blast
qed
lemma proves_ascend_abs_rule':
assumes thy: "wf_theory Θ"
assumes x: "(x, τ') ∉ FV Γ" "(x,τ') ∉ fv (mk_eq (Abs τ' s) (Abs τ' t))" "typ_ok Θ τ'"
assumes eq: "Θ, Γ ⊢ mk_eq (subst_bv (Fv x τ') s) (subst_bv (Fv x τ') t)"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq (Abs τ' s) (Abs τ' t)"
proof-
have ok_ind: "wf_type (sig Θ) τ'"
using x(3) by simp
note 1 = proves_eq_abstract_rule_derived_rule[OF thy]
have "term_ok Θ (subst_bv (Fv x τ') s)"
using eq proved_terms_well_formed(2) wt_term_def typ_of_def
by (meson term_ok_app_eqD)
hence "is_closed (subst_bv (Fv x τ') s)"
using wt_term_def typ_of_imp_closed by auto
hence loose_s: "¬ loose_bvar s 1"
using is_closed_subst_bv by simp
hence loose_s': "(⋀x. 1 < x ⟹ ¬ loose_bvar1 s x) "
by (simp add: not_loose_bvar_imp_not_loose_bvar1_all_greater)
moreover have " ¬ occs (case_prod Fv (x,τ')) s"
proof-
have "(x,τ') ∉ fv s"
using x(2) by auto
thus ?thesis
by (simp add: fv_iff_occs)
qed
ultimately have s: "Abs_fv x τ' (subst_bv (term.Fv x τ') s) = Abs τ' s"
unfolding subst_bv_def bind_fv_def
using bind_fv2_subst_bv1_cancel
by (metis (full_types) case_prod_conv less_one linorder_neqE_nat
loose_bvar1_imp_loose_bvar loose_s not_less_zero)
have "term_ok Θ (subst_bv (Fv x τ') t)"
using eq proved_terms_well_formed(2) wt_term_def typ_of_def
by (meson term_ok_app_eqD)
hence "is_closed (subst_bv (Fv x τ') t)"
using wt_term_def typ_of_imp_closed by auto
hence loose_s: "¬ loose_bvar t 1"
using is_closed_subst_bv by simp
hence loose_s': "(⋀x. 1 < x ⟹ ¬ loose_bvar1 t x) "
by (simp add: not_loose_bvar_imp_not_loose_bvar1_all_greater)
moreover have " ¬ occs (case_prod Fv (x,τ')) t"
proof-
have "(x,τ') ∉ fv t"
using x(2) by auto
thus ?thesis
by (simp add: fv_iff_occs)
qed
ultimately have t: "Abs_fv x τ' (subst_bv (term.Fv x τ') t) = Abs τ' t"
unfolding subst_bv_def bind_fv_def
using bind_fv2_subst_bv1_cancel
by (metis (full_types) case_prod_conv less_one linorder_neqE_nat loose_bvar1_imp_loose_bvar
loose_s not_less_zero)
from 1 s t show ?thesis
using ctxt eq x(1) x(3) by fastforce
qed
lemma proves_descend_abs_rule_iff':
assumes thy: "wf_theory Θ"
assumes x: "(x, τ') ∉ FV Γ" "(x, τ') ∉ fv (mk_eq (Abs τ' s) (Abs τ' t))" "typ_ok Θ τ'"
assumes ctxt: "finite Γ" "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq (subst_bv (Fv x τ') s) (subst_bv (Fv x τ') t)
⟷ Θ, Γ ⊢ mk_eq (Abs τ' s) (Abs τ' t)"
apply (rule iffI)
using assms proves_ascend_abs_rule' apply simp
using assms proves_descend_abs_rule' by simp
lemma proves_beta_step_pre:
assumes thy: "wf_theory Θ"
assumes finite: "finite Γ"
assumes free: "∀(x,τ) ∈ set vs . (x,τ) ∉ fv t ∪ FV Γ"
assumes term_ok': "term_ok Θ (subst_bvs (map (case_prod Fv) vs) t)"
assumes beta: "t →⇩β u"
assumes ctxt: "∀A∈Γ. term_ok Θ A" "∀A∈Γ. typ_of A = Some propT"
shows "Θ, Γ ⊢ mk_eq
(subst_bvs (map (case_prod Fv) vs) t)
(subst_bvs (map (case_prod Fv) vs) u)"
using beta term_ok' free proof(induction t u arbitrary: vs rule: beta.induct)
case (beta T s t)
have ok: "term_ok Θ (subst_bvs (map (case_prod Fv) vs) (Abs T s))"
"term_ok Θ (subst_bvs (map (case_prod Fv) vs) t)"
using beta.prems(1) apply simp_all
using term_ok_app_eqD term_ok_def by blast+
have "∀x ∈ set (map (case_prod Fv) vs) . is_closed x"
using beta.prems(2) by auto
hence simp: "subst_bvs (map (case_prod Fv) vs) (Abs T s)
= Abs T (subst_bvs1' s 1 (map (case_prod Fv) vs))"
by auto
hence ok': "term_ok Θ (Abs T (subst_bvs1' s 1 (map (case_prod Fv) vs)))"
using ok by simp
have T: "typ_of (subst_bvs (map (case_prod Fv) vs) t) = Some T"
using ok(2) wt_term_def typ_of_beta_redex_arg simp
using beta.prems(1) subst_bvs_App
by (metis term_okD2)
have ok_unf: "wt_term (sig Θ) (Abs T (subst_bvs1' s 1 (map (case_prod Fv) vs)))"
"wf_term (sig Θ) (subst_bvs (map (case_prod Fv) vs) t)"
using ok(2) ok' wt_term_def by simp_all
have "subst_bvs (map (λa. case a of (a, b) ⇒ term.Fv a b) vs)
(Abs T s $ t) =
Abs T (subst_bvs1' s 1 (map (case_prod Fv) vs)) $ subst_bvs (map (case_prod Fv) vs) t"
by (simp add: simp)
moreover have "subst_bvs (map (case_prod Fv) vs) (subst_bv2 s 0 t)
= (subst_bv (subst_bvs (map (case_prod Fv) vs) t)
(subst_bvs1' s 1 (map (case_prod Fv) vs)))"
using subst_bvs1'_subst_bv2[symmetric] subst_bvs_subst_bvs1'
by simp (metis One_nat_def Suc_eq_plus1 map_map simp subst_bvs1.simps(2) subst_bvs1_subst_bvs1'
subst_bvs_def substn_subst_0' term.inject(4))
ultimately show ?case
using β_conversion[OF thy ok_unf, of Γ] T by simp
next
case (appL s t u)
hence ok: "term_ok Θ (subst_bvs (map (case_prod Fv) vs) s)"
"term_ok Θ (subst_bvs (map (case_prod Fv) vs) u)"
by (metis subst_bvs_App term_ok_app_eqD)+
moreover have "∀a ∈ set vs. case a of (x, τ) ⇒ (x, τ) ∉ fv s ∪ FV Γ"
using appL by simp
ultimately have "Θ,Γ ⊢ mk_eq (subst_bvs (map (case_prod Fv) vs) s)
(subst_bvs (map (case_prod Fv) vs) t)"
using appL.IH by blast
moreover have "Θ,Γ ⊢ mk_eq (subst_bvs (map (case_prod Fv) vs) u)
(subst_bvs (map (case_prod Fv) vs) u)"
using proves_eq_reflexive[OF thy ok(2), of Γ, OF finite ctxt] by blast
moreover obtain τ where τ: "typ_of
(subst_bvs (map (case_prod Fv) vs) u) = Some τ"
using ok wt_term_def by auto
moreover obtain τ' where "typ_of
(subst_bvs (map (case_prod Fv) vs) s) = Some (τ → τ')"
using τ appL.prems(1) not_None_eq subst_bvs_App wt_term_def typ_of1_arg_typ typ_of_def
by (metis term_okD2)
ultimately show ?case
using proves_eq_combination_rule_better thy finite ctxt by simp
next
case (appR s t u)
hence ok: "term_ok Θ (subst_bvs (map (case_prod Fv) vs) s)"
"term_ok Θ (subst_bvs (map (case_prod Fv) vs) u)"
by (metis subst_bvs_App term_ok_app_eqD)+
moreover have "∀a ∈ set vs. case a of (x, τ) ⇒ (x, τ) ∉ fv s ∪ FV Γ"
using appR by simp
ultimately have "Θ,Γ ⊢ mk_eq (subst_bvs (map (case_prod Fv) vs) s)
(subst_bvs (map (case_prod Fv) vs) t)"
using appR.IH by blast
moreover have "Θ,Γ ⊢ mk_eq (subst_bvs (map (case_prod Fv) vs) u)
(subst_bvs (map (case_prod Fv) vs) u)"
using proves_eq_reflexive[OF thy ok(2), of Γ, OF finite ctxt] by blast
moreover obtain τ where τ: "typ_of
(subst_bvs (map (case_prod Fv) vs) s) = Some τ"
using ok wt_term_def by auto
moreover obtain τ' where "typ_of
(subst_bvs (map (case_prod Fv) vs) u) = Some (τ → τ')"
using τ appR.prems(1) not_None_eq subst_bvs_App wt_term_def typ_of1_arg_typ typ_of_def
by (metis term_okD2)
ultimately show ?case
using proves_eq_combination_rule_better thy finite ctxt by simp
next
case (abs s t T)
have "∀a ∈ set vs. case a of (x, τ) ⇒ (x, τ) ∉ fv s ∪ FV Γ"
using abs.prems(2) by auto
have "∀v∈set (map (case_prod Fv) vs) . is_closed v"
by auto
hence simp: "mk_eq (subst_bvs (map (case_prod Fv) vs) (Abs T s))
(subst_bvs (map (case_prod Fv) vs) (Abs T t))
= mk_eq (Abs T (subst_bvs1' s 1 (map (case_prod Fv) vs)))
(Abs T (subst_bvs1' t 1 (