Theory Instance

section ‹Instantiation of Syntax-Independent Logic Infrastructure›

(*<*)
theory Instance
imports "Syntax_Independent_Logic.Standard_Model" "Syntax_Independent_Logic.Deduction_Q" Robinson_Arithmetic
begin
(*>*)

subsection ‹Preliminaries›

inductive_set num :: "trm set" where
 zer[intro!,simp]: "zer ∈ num"
|suc[simp]: "t ∈ num ⟹ suc t ∈ num"

definition ground_aux :: "trm ⇒ atom set ⇒ bool"
  where "ground_aux t S ≡ (supp t ⊆ S)"

abbreviation ground :: "trm ⇒ bool"
  where "ground t ≡ ground_aux t {}"

definition ground_fmla_aux :: "fmla ⇒ atom set ⇒ bool"
  where "ground_fmla_aux A S ≡ (supp A ⊆ S)"

abbreviation ground_fmla :: "fmla ⇒ bool"
  where "ground_fmla A ≡ ground_fmla_aux A {}"

lemma ground_aux_simps[simp]:
  "ground_aux zer S = True"
  "ground_aux (Var k) S = (if atom k ∈ S then True else False)"
  "ground_aux (suc t) S = (ground_aux t S)"
  "ground_aux (pls t u) S = (ground_aux t S ∧ ground_aux u S)"
  "ground_aux (tms t u) S = (ground_aux t S ∧ ground_aux u S)"
unfolding ground_aux_def
by (simp_all add: supp_at_base)

lemma ground_fmla_aux_simps[simp]:
  "ground_fmla_aux fls S = True"
  "ground_fmla_aux (t EQ u) S = (ground_aux t S ∧ ground_aux u S)"
  "ground_fmla_aux (A OR B) S = (ground_fmla_aux A S ∧ ground_fmla_aux B S)"
  "ground_fmla_aux (A AND B) S = (ground_fmla_aux A S ∧ ground_fmla_aux B S)"
  "ground_fmla_aux (A IFF B) S = (ground_fmla_aux A S ∧ ground_fmla_aux B S)"
  "ground_fmla_aux (neg A) S =  (ground_fmla_aux A S)"
  "ground_fmla_aux (exi x A) S = (ground_fmla_aux A (S ∪ {atom x}))"
by (auto simp: ground_fmla_aux_def ground_aux_def supp_conv_fresh)

lemma ground_fresh[simp]:
  "ground t ⟹ atom i ♯ t"
  "ground_fmla A ⟹ atom i ♯ A"
unfolding ground_aux_def ground_fmla_aux_def fresh_def
by simp_all

(* This applies to all nominal types, including terms and formulas: *)
definition "Fvars t = {a :: name. ¬ atom a ♯ t}"

lemma Fvars_trm_simps[simp]:
  "Fvars zer = {}"
  "Fvars (Var a) = {a}"
  "Fvars (suc x ) = Fvars x"
  "Fvars (pls x y) = Fvars x ∪ Fvars y"
  "Fvars (tms x y) = Fvars x ∪ Fvars y"
  by (auto simp: Fvars_def fresh_at_base(2))

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

lemma Fvars_fmla_simps[simp]:
  "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 (exi a A) = Fvars A - {a}"
  "Fvars (all a A) = Fvars A - {a}"
  by (auto simp: Fvars_def fresh_at_base(2))

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

lemma subst_trm_subst_trm[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: trm.induct) auto

lemma subst_fmla_subst_fmla[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: fmla.strong_induct) auto

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

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

lemma ground_Fvars: "ground t ⟷ Fvars t = {}"
  apply (rule iffI)
  subgoal by (auto simp only: Fvars_def ground_fresh) []
  by auto

lemma Fvars_ground_fmla_aux: "Fvars A ⊆ B ⟹ ground_fmla_aux A (atom ` B)"
  apply (induct A arbitrary: B rule: fmla.induct)
  subgoal by (auto simp: Diff_subset_conv Fvars_ground_aux)
  subgoal by (auto simp: Diff_subset_conv Fvars_ground_aux)
  subgoal by (auto simp: Diff_subset_conv Fvars_ground_aux)
  subgoal by (metis Diff_subset_conv Fvars_fmla_simps(7) Un_insert_left
              Un_insert_right ground_fmla_aux_simps(7)
              image_insert sup_bot.left_neutral sup_bot.right_neutral) .

lemma ground_fmla_Fvars: "ground_fmla A ⟷ Fvars A = {}"
  apply (rule iffI)
  subgoal by (auto simp only: Fvars_def ground_fresh)
  by (auto intro: Fvars_ground_fmla_aux[of A "{}", simplified])

lemma obtain_const_trm:
obtains t where "eval_trm e t = x" "t ∈ num"
apply (induct x)
using eval_trm.simps(1) eval_trm.simps(3) num.suc by blast+

lemma ex_eval_fmla_iff_exists_num:
  "eval_fmla e (exi k A) ⟷ (∃t. eval_fmla e (A(k::=t)) ∧ t ∈ num)"
by (auto simp: eval_subst_fmla) (metis obtain_const_trm)

lemma exi_ren: "y ∉ Fvars φ ⟹ exi x φ = exi y (φ(x::=Var y))"
using exi_ren_subst_fresh Fvars_def by blast

lemma all_ren: "y ∉ Fvars φ ⟹ all x φ = all y (φ(x::=Var y))"
by (simp add: exi_ren)

lemma Fvars_num[simp]: "t ∈ num ⟹ Fvars t = {}"
by (induct t rule: trm.induct) (auto elim: num.cases)

subsection ‹Instantiation of the generic syntax and deduction relation›

interpretation Generic_Syntax where
      var = "UNIV :: name set"
  and trm = "UNIV :: trm set"
  and fmla = "UNIV :: fmla 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_fmla 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: trm.induct) auto
  subgoal by simp
  subgoal by simp
  subgoal by simp
  subgoal unfolding Fvars_def fresh_subst_fmla_if by auto
  subgoal unfolding Fvars_def by auto
  subgoal unfolding Fvars_def by simp
  subgoal by simp
  subgoal unfolding Fvars_def by simp .

interpretation Syntax_with_Numerals where
      var = "UNIV :: name set"
  and trm = "UNIV :: trm set"
  and fmla = "UNIV :: fmla set"
  and num = num
  and Var = Var
  and FvarsT = Fvars
  and substT = "λt u x. subst x u t"
  and Fvars = Fvars
  and subst = "λA u x. subst_fmla A x u"
  apply unfold_locales
  subgoal by (auto intro!: exI[of _ zer])
  subgoal by simp
  subgoal by (simp add: ground_Fvars) .

interpretation Deduct_with_False where
      var = "UNIV :: name set"
  and trm = "UNIV :: trm set"
  and fmla = "UNIV :: fmla set"
  and num = num
  and Var = Var
  and FvarsT = Fvars
  and substT = "λt u x. subst x u t"
  and Fvars = Fvars
  and subst = "λA u x. subst_fmla A x u"
  and eql = eql and cnj = cnj and imp = imp and all = all
  and exi = exi and fls = fls
  and prv = "(⊢) {}"
  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) .
  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: exi_I)
  subgoal by simp
  subgoal by (metis cnj_E2 Iff_def imp_I Var_eql_subst_Iff)
  subgoal by blast .

interpretation Deduct_with_False_Disj where
      var = "UNIV :: name set"
  and trm = "UNIV :: trm set"
  and fmla = "UNIV :: fmla set"
  and num = num
  and Var = Var
  and FvarsT = Fvars
  and substT = "λt u x. subst x u t"
  and Fvars = Fvars
  and subst = "λA u x. subst_fmla A x u"
  and eql = eql and cnj = cnj and dsj = dsj and imp = imp
  and all = all and exi = exi and fls = fls
  and prv = "(⊢) {}"
  apply unfold_locales
  subgoal by simp
  subgoal by simp
  subgoal by simp
  subgoal by (auto intro: dsj_I1)
  subgoal by (auto intro: dsj_I2)
  subgoal by (auto intro: ContraAssume) .


subsection ‹Instantiation of the arithmetic-enriched generic syntax and deduction relation›

interpretation Syntax_Arith_aux where
      var = "UNIV :: name set"
  and trm = "UNIV :: trm set"
  and fmla = "UNIV :: fmla set"
  and num = num
  and Var = Var
  and FvarsT = Fvars
  and substT = "λt u x. subst x u t"
  and Fvars = Fvars
  and subst = "λA u x. subst_fmla A x u"
  and eql = eql and cnj = cnj and imp = imp and all = all
  and exi = exi and dsj = dsj and fls = fls
  and zer = zer and suc = suc and pls = pls and tms = tms
  by unfold_locales (auto simp: exi_ren all_ren)

lemma num_range_Num: "num = range Num"
proof-
  {fix t assume "t ∈ num"
   then have "∃n. t = Num n"
   apply(induct t rule: trm.induct)
   subgoal by (auto intro: exI[of _ 0])
   subgoal by (auto elim: num.cases)
   subgoal by (metis Num.simps(2) num.cases trm.distinct(3) trm.eq_iff(3))
   by (auto elim: num.cases)
  }
  moreover
  {fix n have "Num n ∈ num"
   by (induct n) auto
  }
  ultimately show ?thesis by auto
qed

lemma [simp]: "{} ⊢ neg (zer EQ suc (Var xx))"
proof-
  have 0: "{} ⊢ Robinson_Arithmetic.neg (zer EQ suc (Var xx))"
  by (intro nprv.Q) (auto intro!: exI[of _ zz] simp: Q_axioms_def)
  show ?thesis unfolding neg_def
  by (simp add: 0 dsj_I1)
qed

lemma [simp]: "{} ⊢ Var yy EQ zer OR exi xx (Var yy EQ suc (Var xx))"
by (intro nprv.Q) (auto intro!: exI[of _ zz] simp: Q_axioms_def)

lemma [simp]: "{} ⊢ pls (Var xx) zer EQ Var xx"
by (intro nprv.Q) (auto intro!: exI[of _ zz] simp: Q_axioms_def)

lemma [simp]: "{} ⊢ tms (Var xx) zer EQ zer"
by (intro nprv.Q) (auto intro!: exI[of _ zz] simp: Q_axioms_def)

interpretation S: Syntax_Arith where
      var = "UNIV :: name set"
  and trm = "UNIV :: trm set"
  and fmla = "UNIV :: fmla set"
  and num = num
  and Var = Var
  and FvarsT = Fvars
  and substT = "λt u x. subst x u t"
  and Fvars = Fvars
  and subst = "λA u x. subst_fmla A x u"
  and eql = eql and cnj = cnj and imp = imp and all = all
  and exi = exi and dsj = dsj and fls = fls and zer = zer
  and suc = suc and pls = pls and tms = tms
  using num_range_Num by unfold_locales auto

interpretation Deduct_Q where
      var = "UNIV :: name set"
  and trm = "UNIV :: trm set"
  and fmla = "UNIV :: fmla set"
  and num = num
  and Var = Var
  and FvarsT = Fvars
  and substT = "λt u x. subst x u t"
  and Fvars = Fvars
  and subst = "λA u x. subst_fmla A x u"
  and eql = eql and cnj = cnj and imp = imp and all = all
  and exi = exi and dsj = dsj and fls = fls and zer = zer
  and suc = suc and pls = pls and tms = tms
  and prv = "(⊢) {}"
  by unfold_locales (auto simp add: Q Q_axioms_def)

subsection ‹Instantiation of the abstract notion of standard model and truth›

interpretation Minimal_Truth_Soundness where
      var = "UNIV :: name set"
  and trm = "UNIV :: trm set"
  and fmla = "UNIV :: fmla set"
  and num = num
  and Var = Var
  and FvarsT = Fvars
  and substT = "λt u x. subst x u t"
  and Fvars = Fvars
  and subst = "λA u x. subst_fmla A x u"
  and eql = eql and cnj = cnj and dsj = dsj and imp = imp
  and all = all and exi = exi and fls = fls
  and prv = "(⊢) {}"
  and isTrue = "eval_fmla e0"
  apply unfold_locales
  subgoal by (auto simp: fls_def)
  subgoal by simp
  subgoal by (auto simp only: ex_eval_fmla_iff_exists_num eval_fmla.simps  subst_fmla.simps)
  subgoal by (auto simp only: ex_eval_fmla_iff_exists_num)
  subgoal by (simp add: neg_def)
  subgoal by (auto dest: nprv_sound) .

(*<*)
end
(*>*)