# Theory Instance

```chapter ‹The Instantiation›

(*<*)
theory Instance
imports Goedel_Incompleteness.Abstract_Second_Goedel Quote Goedel_I
begin
(*>*)

definition "Fvars t = {a :: name. ¬ atom a ♯ t}"

lemma Fvars_tm_simps[simp]:
"Fvars Zero = {}"
"Fvars (Var a) = {a}"
"Fvars (Eats x y) = Fvars x ∪ Fvars y"
by (auto simp: Fvars_def fresh_at_base(2))

lemma finite_Fvars_tm[simp]:
fixes t :: tm
shows "finite (Fvars t)"
by (induct t rule: tm.induct) auto

lemma Fvars_fm_simps[simp]:
"Fvars (x IN y) = Fvars x ∪ Fvars y"
"Fvars (x EQ y) = Fvars x ∪ Fvars y"
"Fvars (A OR B) = Fvars A ∪ Fvars B"
"Fvars (A AND B) = Fvars A ∪ Fvars B"
"Fvars (A IMP B) = Fvars A ∪ Fvars B"
"Fvars Fls = {}"
"Fvars (Neg A) = Fvars A"
"Fvars (Ex a A) = Fvars A - {a}"
"Fvars (All a A) = Fvars A - {a}"
by (auto simp: Fvars_def fresh_at_base(2))

lemma finite_Fvars_fm[simp]:
fixes A :: fm
shows "finite (Fvars A)"
by (induct A rule: fm.induct) auto

lemma subst_tm_subst_tm[simp]:
"x ≠ y ⟹ atom x ♯ u ⟹ subst y u (subst x t v) = subst x (subst y u t) (subst y u v)"
by (induct v rule: tm.induct) auto

lemma subst_fm_subst_fm[simp]:
"x ≠ y ⟹ atom x ♯ u ⟹ (A(x::=t))(y::=u) = (A(y::=u))(x::=subst y u t)"
by (nominal_induct A avoiding: x t y u rule: fm.strong_induct) auto

lemma Fvars_ground_aux: "Fvars t ⊆ B ⟹ ground_aux t (atom ` B)"
by (induct t rule: tm.induct) auto

lemma ground_Fvars: "ground t ⟷ Fvars t = {}"
apply (rule iffI)
apply (auto simp only: Fvars_def ground_fresh) []
apply (auto intro: Fvars_ground_aux[of t "{}", simplified])
done

lemma Fvars_ground_fm_aux: "Fvars A ⊆ B ⟹ ground_fm_aux A (atom ` B)"
apply (induct A arbitrary: B rule: fm.induct)
apply (auto simp: Diff_subset_conv Fvars_ground_aux)
apply (drule meta_spec, drule meta_mp, assumption)
apply auto
done

lemma ground_fm_Fvars: "ground_fm A ⟷ Fvars A = {}"
apply (rule iffI)
apply (auto simp only: Fvars_def ground_fresh) []
apply (auto intro: Fvars_ground_fm_aux[of A "{}", simplified])
done

interpretation Generic_Syntax where
var = "UNIV :: name set"
and trm = "UNIV :: tm set"
and fmla = "UNIV :: fm set"
and Var = Var
and FvarsT = Fvars
and substT = "λt u x. subst x u t"
and Fvars = Fvars
and subst = "λA u x. subst_fm A x u"
apply unfold_locales
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal for t by (induct t rule: tm.induct) auto
subgoal by simp
subgoal by simp
subgoal by simp
subgoal unfolding Fvars_def fresh_subst_fm_if by auto
subgoal unfolding Fvars_def by auto
subgoal unfolding Fvars_def by simp
subgoal by simp
subgoal unfolding Fvars_def by simp
done

lemma coding_tm_Fvars_empty[simp]: "coding_tm t ⟹ Fvars t = {}"
by (induct t rule: coding_tm.induct) (auto simp: Fvars_def)

lemma Fvars_empty_ground[simp]: "Fvars t = {} ⟹ ground t"
by (induct t rule: tm.induct) auto

interpretation Syntax_with_Numerals where
var = "UNIV :: name set"
and trm = "UNIV :: tm set"
and fmla = "UNIV :: fm set"
and num = "{t. ground t}"
and Var = Var
and FvarsT = Fvars
and substT = "λt u x. subst x u t"
and Fvars = Fvars
and subst = "λA u x. subst_fm A x u"
apply unfold_locales
subgoal by (auto intro!: exI[of _ Zero])
subgoal by simp
(*subgoal by simp*)
done

declare FvarsT_num[simp del]

interpretation Deduct2_with_False where
var = "UNIV :: name set"
and trm = "UNIV :: tm set"
and fmla = "UNIV :: fm set"
and num = "{t. ground t}"
and Var = Var
and FvarsT = Fvars
and substT = "λt u x. subst x u t"
and Fvars = Fvars
and subst = "λA u x. subst_fm A x u"
and eql = "(EQ)"
and cnj = "(AND)"
and imp = "(IMP)"
and all = "All"
and exi = "Ex"
and fls = "Fls"
and prv = "(⊢) {}"
and bprv = "(⊢) {}"
apply unfold_locales
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal unfolding Fvars_def by simp
subgoal unfolding Fvars_def by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal using MP_null by blast
subgoal by blast
subgoal for A B C
apply (rule Imp_I)+
apply (rule MP_same[of _ B])
apply (rule MP_same[of _ C])
apply (auto intro: Neg_D)
done
subgoal by blast
subgoal by blast
subgoal by blast
subgoal unfolding Fvars_def by (auto intro: MP_null)
subgoal unfolding Fvars_def by (auto intro: MP_null)
subgoal by (auto intro: All_D)
subgoal by (auto intro: Ex_I)
subgoal by simp
subgoal by (metis Conj_E2 Iff_def Imp_I Var_Eq_subst_Iff)
subgoal by blast
subgoal by simp
done

interpretation HBL1 where
var = "UNIV :: name set"
and trm = "UNIV :: tm set"
and fmla = "UNIV :: fm set"
and num = "{t. ground t}"
and Var = Var
and FvarsT = Fvars
and substT = "λt u x. subst x u t"
and Fvars = Fvars
and subst = "λA u x. subst_fm A x u"
and eql = "(EQ)"
and cnj = "(AND)"
and imp = "(IMP)"
and all = "All"
and exi = "Ex"
and prv = "(⊢) {}"
and bprv = "(⊢) {}"
and enc = "quot"
and P = "PfP (Var xx)"
apply unfold_locales
subgoal by simp
subgoal unfolding Fvars_def by (auto simp: fresh_at_base(2))
subgoal by (auto simp: proved_imp_proved_PfP)
done

interpretation Goedel_Form where
var = "UNIV :: name set"
and trm = "UNIV :: tm set"
and fmla = "UNIV :: fm set"
and num = "{t. ground t}"
and Var = Var
and FvarsT = Fvars
and substT = "λt u x. subst x u t"
and Fvars = Fvars
and subst = "λA u x. subst_fm A x u"
and eql = "(EQ)"
and cnj = "(AND)"
and imp = "(IMP)"
and all = "All"
and exi = "Ex"
and fls = "Fls"
and prv = "(⊢) {}"
and bprv = "(⊢) {}"
and enc = "quot"
and S = "KRP (quot (Var xx)) (Var xx) (Var yy)"
and P = "PfP (Var xx)"
apply unfold_locales
subgoal by simp
subgoal unfolding Fvars_def by (auto simp: fresh_at_base(2))
subgoal
unfolding Let_def
by (subst psubst_eq_rawpsubst2)
(auto simp: quot_fm_coding prove_KRP Fvars_def)
subgoal
unfolding Let_def
by (subst (1 2) psubst_eq_rawpsubst2)
(auto simp: quot_fm_coding KRP_unique[THEN Sym] Fvars_def)
done

interpretation g2: Goedel_Second_Assumptions where
var = "UNIV :: name set"
and trm = "UNIV :: tm set"
and fmla = "UNIV :: fm set"
and num = "{t. ground t}"
and Var = Var
and FvarsT = Fvars
and substT = "λt u x. subst x u t"
and Fvars = Fvars
and subst = "λA u x. subst_fm A x u"
and eql = "(EQ)"
and cnj = "(AND)"
and imp = "(IMP)"
and all = "All"
and exi = "Ex"
and fls = "Fls"
and prv = "(⊢) {}"
and bprv = "(⊢) {}"
and enc = "quot"
and S = "KRP (quot (Var xx)) (Var xx) (Var yy)"
and P = "PfP (Var xx)"
apply unfold_locales
subgoal by (auto simp: PP_def intro: PfP_implies_ModPon_PfP_quot)
subgoal by (auto simp: PP_def quot_fm_coding Provability)
done

theorem "¬ {} ⊢ Fls ⟹ ¬ {} ⊢ neg (PfP (quot Fls))"
by (rule g2.goedel_second[unfolded consistent_def PP_def PfP_subst subst.simps simp_thms if_True])

(*<*)
end
(*>*)
```