Theory Prop_Logic

theory Prop_Logic
imports Main
begin

chapter ‹Normalisation›

text ‹We define here the normalisation from formula towards conjunctive and disjunctive normal form,
  including normalisation towards multiset of multisets to represent CNF.›

section ‹Logics›

text ‹In this section we define the syntax of the formula and an abstraction over it to have simpler
  proofs. After that we define some properties like subformula and rewriting.›

subsection ‹Definition and Abstraction›

text ‹The propositional logic is defined inductively. The type parameter is the type of the
  variables. ›
datatype 'v propo =
  FT | FF | FVar "'v" | FNot "'v propo" | FAnd "'v propo" "'v propo" | FOr "'v propo" "'v propo"
  | FImp "'v propo" "'v propo" | FEq "'v propo" "'v propo"

text ‹We do not define any notation for the formula, to distinguish properly between the formulas
  and Isabelle's logic.›


text ‹To ease the proofs, we will write the the formula on a homogeneous manner, namely a connecting
  argument and a list of arguments.›
datatype 'v connective = CT | CF | CVar "'v" | CNot | CAnd | COr | CImp | CEq

abbreviation "nullary_connective ≡ {CF} ∪ {CT} ∪ {CVar x | x. True}"
definition "binary_connectives ≡ {CAnd, COr, CImp, CEq}"


text ‹We define our own induction principal: instead of distinguishing every constructor, we group
  them by arity.›

lemma propo_induct_arity[case_names nullary unary binary]:
  fixes φ ψ :: "'v propo"
  assumes nullary: "⋀φ x. φ = FF ∨ φ = FT ∨ φ = FVar x ⟹ P φ"
  and unary: "⋀ψ. P ψ ⟹ P (FNot ψ)"
  and binary: "⋀φ ψ1 ψ2. P ψ1 ⟹ P ψ2 ⟹ φ = FAnd ψ1 ψ2 ∨ φ = FOr ψ1 ψ2 ∨ φ = FImp ψ1 ψ2
    ∨ φ = FEq ψ1 ψ2 ⟹ P φ"
  shows "P ψ"
  apply (induct rule: propo.induct)
  using assms by metis+

text ‹The function @{term conn} is the interpretation of our representation (connective and list of
  arguments). We define any thing that has no sense to be false›
fun conn :: "'v connective ⇒ 'v propo list ⇒ 'v propo" where
"conn CT [] = FT" |
"conn CF [] = FF" |
"conn (CVar v) [] = FVar v" |
"conn CNot [φ] = FNot φ" |
"conn CAnd (φ # [ψ]) = FAnd φ ψ" |
"conn COr (φ # [ψ]) = FOr φ ψ" |
"conn CImp (φ # [ψ]) = FImp φ ψ" |
"conn CEq (φ # [ψ]) = FEq φ ψ" |
"conn _ _ = FF"

text ‹We will often use case distinction, based on the arity of the @{typ "'v connective"}, thus we
  define our own splitting principle.›
lemma connective_cases_arity[case_names nullary binary unary]:
  assumes nullary: "⋀x. c = CT ∨ c = CF ∨ c = CVar x ⟹ P"
  and binary: "c ∈ binary_connectives ⟹ P"
  and unary: "c = CNot ⟹ P"
  shows "P"
  using assms by (cases c) (auto simp: binary_connectives_def)

(*Maybe is this version better, by adding nullary_connective[simp] *)
lemma connective_cases_arity_2[case_names nullary unary binary]:
  assumes nullary: "c ∈ nullary_connective ⟹ P"
  and unary: "c = CNot ⟹ P"
  and binary: "c ∈ binary_connectives ⟹ P"
  shows "P"
  using assms by (cases c, auto simp add: binary_connectives_def)


text ‹Our previous definition is not necessary correct (connective and list of arguments), so we
  define an inductive predicate.›
inductive wf_conn :: "'v connective ⇒ 'v propo list ⇒ bool" for c :: "'v connective" where
wf_conn_nullary[simp]: "(c = CT ∨ c = CF ∨ c = CVar v) ⟹ wf_conn c []" |
wf_conn_unary[simp]: "c = CNot ⟹ wf_conn c [ψ]" |
wf_conn_binary[simp]: "c ∈ binary_connectives ⟹ wf_conn c (ψ # ψ' # [])"
thm wf_conn.induct
lemma wf_conn_induct[consumes 1, case_names CT CF CVar CNot COr CAnd CImp CEq]:
  assumes "wf_conn c x" and
    "⋀v. c = CT ⟹ P []" and
    "⋀v. c = CF ⟹ P []" and
    "⋀v. c = CVar v ⟹ P []" and
    "⋀ψ. c = CNot ⟹ P [ψ]" and
    "⋀ψ ψ'. c = COr ⟹ P [ψ, ψ']" and
    "⋀ψ ψ'. c = CAnd ⟹ P [ψ, ψ']" and
    "⋀ψ ψ'. c = CImp ⟹ P [ψ, ψ']" and
    "⋀ψ ψ'. c = CEq ⟹ P [ψ, ψ']"
  shows "P x"
  using assms by induction (auto simp: binary_connectives_def)


subsection ‹Properties of the Abstraction›

text ‹First we can define simplification rules.›
lemma wf_conn_conn[simp]:
  "wf_conn CT l ⟹ conn CT l = FT"
  "wf_conn CF l ⟹ conn CF l = FF"
  "wf_conn (CVar x) l ⟹ conn (CVar x) l = FVar x"
  apply (simp_all add: wf_conn.simps)
  unfolding binary_connectives_def by simp_all


lemma wf_conn_list_decomp[simp]:
  "wf_conn CT l ⟷ l = []"
  "wf_conn CF l ⟷ l = []"
  "wf_conn (CVar x) l ⟷ l = []"
  "wf_conn CNot (ξ @ φ # ξ') ⟷ ξ = [] ∧ ξ' = []"
  apply (simp_all add: wf_conn.simps)
       unfolding binary_connectives_def apply simp_all
  by (metis append_Nil append_is_Nil_conv list.distinct(1) list.sel(3) tl_append2)


lemma wf_conn_list:
  "wf_conn c l ⟹ conn c l = FT ⟷ (c = CT ∧ l = [])"
  "wf_conn c l ⟹ conn c l = FF ⟷ (c = CF ∧ l = [])"
  "wf_conn c l ⟹ conn c l = FVar x ⟷ (c = CVar x ∧ l = [])"
  "wf_conn c l ⟹ conn c l = FAnd a b ⟷ (c = CAnd ∧ l = a # b # [])"
  "wf_conn c l ⟹ conn c l = FOr a b ⟷ (c = COr ∧ l = a # b # [])"
  "wf_conn c l ⟹ conn c l = FEq a b ⟷ (c = CEq ∧ l = a # b # [])"
  "wf_conn c l ⟹ conn c l = FImp a b ⟷ (c = CImp ∧ l = a # b # [])"
  "wf_conn c l ⟹ conn c l = FNot a ⟷ (c = CNot ∧ l = a # [])"
  apply (induct l rule: wf_conn.induct)
  unfolding binary_connectives_def by auto

text ‹In the binary connective cases, we will often decompose the list of arguments (of length 2)
  into two elements.›
lemma list_length2_decomp: "length l = 2 ⟹ (∃ a b. l = a # b # [])"
  apply (induct l, auto)
  by (rename_tac l, case_tac l, auto)

text ‹@{term wf_conn} for binary operators means that there are two arguments.›
lemma wf_conn_bin_list_length:
  fixes l :: "'v propo list"
  assumes conn: "c ∈ binary_connectives"
  shows "length l = 2 ⟷ wf_conn c l"
proof
  assume "length l = 2"
  then show "wf_conn c l" using wf_conn_binary list_length2_decomp using conn by metis
next
  assume "wf_conn c l"
  then show "length l = 2" (is "?P l")
    proof (cases rule: wf_conn.induct)
      case wf_conn_nullary
      then show "?P []" using conn binary_connectives_def
        using connective.distinct(11) connective.distinct(13) connective.distinct(9) by blast
    next
      fix ψ :: "'v propo"
      case wf_conn_unary
      then show "?P [ψ]" using conn binary_connectives_def
        using connective.distinct by blast
    next
      fix ψ ψ':: "'v propo"
      show "?P [ψ, ψ']" by auto
    qed
qed

lemma wf_conn_not_list_length[iff]:
  fixes l :: "'v propo list"
  shows "wf_conn CNot l ⟷ length l = 1"
  apply auto
  apply (metis append_Nil connective.distinct(5,17,27) length_Cons list.size(3) wf_conn.simps
    wf_conn_list_decomp(4))
  by (simp add: length_Suc_conv wf_conn.simps)


text ‹Decomposing the Not into an element is moreover very useful.›
lemma wf_conn_Not_decomp:
  fixes l :: "'v propo list" and a :: "'v"
  assumes corr: "wf_conn CNot l"
  shows "∃ a. l = [a]"
  by (metis (no_types, lifting) One_nat_def Suc_length_conv corr length_0_conv
    wf_conn_not_list_length)


text ‹The @{term wf_conn} remains correct if the length of list does not change. This lemma is very
  useful when we do one rewriting step›
lemma wf_conn_no_arity_change:
  "length l = length l' ⟹ wf_conn c l ⟷ wf_conn c l'"
proof -
  {
    fix l l'
    have "length l = length l' ⟹ wf_conn c l ⟹ wf_conn c l'"
      apply (cases c l rule: wf_conn.induct, auto)
      by (metis wf_conn_bin_list_length)
  }
  then show "length l = length l' ⟹ wf_conn c l = wf_conn c l'" by metis
qed

lemma wf_conn_no_arity_change_helper:
  "length (ξ @ φ # ξ') = length (ξ @ φ' # ξ') "
  by auto

text ‹The injectivity of @{term conn} is useful to prove equality of the connectives and the lists.›
lemma conn_inj_not:
  assumes correct: "wf_conn c l"
  and conn: "conn c l = FNot ψ"
  shows "c = CNot" and "l = [ψ]"
  apply (cases c l rule: wf_conn.cases)
  using correct conn unfolding binary_connectives_def apply auto
  apply (cases c l rule: wf_conn.cases)
  using correct conn unfolding binary_connectives_def by auto


lemma conn_inj:
  fixes c ca :: "'v connective" and l ψs :: "'v propo list"
  assumes corr: "wf_conn ca l"
  and corr': "wf_conn c ψs"
  and eq: "conn ca l = conn c ψs"
  shows "ca = c ∧ ψs = l"
  using corr
proof (cases ca l rule: wf_conn.cases)
  case (wf_conn_nullary v)
  then show "ca = c ∧ ψs = l" using assms
      by (metis conn.simps(1) conn.simps(2) conn.simps(3) wf_conn_list(1-3))
next
  case (wf_conn_unary ψ')
  then have *: "FNot ψ' = conn c ψs" using conn_inj_not eq assms by auto
  then have "c = ca" by (metis conn_inj_not(1) corr' wf_conn_unary(2))
  moreover have "ψs = l" using * conn_inj_not(2) corr' wf_conn_unary(1) by force
  ultimately show "ca = c ∧ ψs = l" by auto
next
  case (wf_conn_binary ψ' ψ'')
  then show "ca = c ∧ ψs = l"
    using eq corr' unfolding binary_connectives_def apply (cases ca, auto simp add: wf_conn_list)
    using wf_conn_list(4-7) corr' by metis+
qed



subsection ‹Subformulas and Properties›

text ‹A characterization using sub-formulas is interesting for rewriting: we will define our
  relation on the sub-term level, and then lift the rewriting on the term-level. So the rewriting
  takes place on a subformula.›


inductive subformula :: "'v propo ⇒ 'v propo ⇒ bool" (infix "≼" 45) for φ where
subformula_refl[simp]: "φ ≼ φ" |
subformula_into_subformula: "ψ ∈ set l ⟹ wf_conn c l ⟹ φ ≼ ψ ⟹ φ ≼ conn c l"

text ‹On the @{prop subformula_into_subformula}, we can see why we use our @{term conn}
  representation: one case is enough to express the subformulas property instead of listing all
  the cases.›

text ‹This is an example of a property related to subformulas.›
lemma subformula_in_subformula_not:
shows b: "FNot φ ≼ ψ ⟹ φ ≼ ψ"
  apply (induct rule: subformula.induct)
  using subformula_into_subformula wf_conn_unary subformula_refl list.set_intros(1) subformula_refl
    by (fastforce intro: subformula_into_subformula)+

lemma subformula_in_binary_conn:
  assumes conn: "c ∈ binary_connectives"
  shows "f ≼ conn c [f, g]"
  and "g ≼ conn c [f, g]"
proof -
  have a: "wf_conn c (f# [g])" using conn wf_conn_binary binary_connectives_def by auto
  moreover have b: "f ≼ f" using subformula_refl by auto
  ultimately show "f ≼ conn c [f, g]"
    by (metis append_Nil in_set_conv_decomp subformula_into_subformula)
next
  have a: "wf_conn c ([f] @ [g])" using conn wf_conn_binary binary_connectives_def by auto
  moreover have b: "g ≼ g" using subformula_refl by auto
  ultimately show "g ≼ conn c [f, g]" using subformula_into_subformula by force
qed

lemma subformula_trans:
 "ψ ≼ ψ' ⟹ φ ≼ ψ ⟹ φ ≼ ψ'"
  apply (induct ψ' rule: subformula.inducts)
  by (auto simp: subformula_into_subformula)

lemma subformula_leaf:
  fixes φ ψ :: "'v propo"
  assumes incl: "φ ≼  ψ"
  and simple: "ψ = FT ∨ ψ = FF ∨ ψ = FVar x"
  shows "φ = ψ"
  using incl simple
  by (induct rule: subformula.induct, auto simp: wf_conn_list)

lemma subfurmula_not_incl_eq:
  assumes "φ ≼ conn c l"
  and "wf_conn c l"
  and "∀ψ. ψ ∈ set l ⟶ ¬ φ ≼ ψ"
  shows "φ = conn c l"
  using assms apply (induction "conn c l" rule: subformula.induct, auto)
  using conn_inj by blast

lemma wf_subformula_conn_cases:
  "wf_conn c l ⟹ φ ≼ conn c l ⟷ (φ = conn c l ∨ (∃ψ. ψ ∈ set l ∧ φ ≼ ψ))"
  apply standard
    using subfurmula_not_incl_eq apply metis
  by (auto simp add: subformula_into_subformula)

lemma subformula_decomp_explicit[simp]:
  "φ ≼ FAnd ψ ψ' ⟷ (φ = FAnd ψ ψ' ∨ φ ≼ ψ ∨ φ ≼ ψ')" (is "?P FAnd")
  "φ ≼ FOr ψ ψ' ⟷ (φ = FOr ψ ψ' ∨ φ ≼ ψ ∨ φ ≼ ψ')"
  "φ ≼ FEq ψ ψ' ⟷ (φ = FEq ψ ψ' ∨ φ ≼ ψ ∨ φ ≼ ψ')"
  "φ ≼ FImp ψ ψ' ⟷ (φ = FImp ψ ψ' ∨ φ ≼ ψ ∨ φ ≼ ψ')"
proof -
  have "wf_conn CAnd [ψ, ψ']" by (simp add: binary_connectives_def)
  then have "φ ≼ conn CAnd [ψ, ψ'] ⟷
    (φ = conn CAnd [ψ, ψ'] ∨ (∃ψ''. ψ'' ∈ set [ψ, ψ'] ∧ φ ≼ ψ''))"
    using wf_subformula_conn_cases by metis
  then show "?P FAnd" by auto
next
  have "wf_conn COr [ψ, ψ']" by (simp add: binary_connectives_def)
  then have "φ ≼ conn COr [ψ, ψ'] ⟷
    (φ = conn COr [ψ, ψ'] ∨ (∃ψ''. ψ'' ∈ set [ψ, ψ'] ∧ φ ≼ ψ''))"
    using wf_subformula_conn_cases by metis
  then show "?P FOr" by auto
next
  have "wf_conn CEq [ψ, ψ']" by (simp add: binary_connectives_def)
  then have "φ ≼ conn CEq [ψ, ψ'] ⟷
    (φ = conn CEq [ψ, ψ'] ∨ (∃ψ''. ψ'' ∈ set [ψ, ψ'] ∧ φ ≼ ψ''))"
    using wf_subformula_conn_cases by metis
  then show "?P FEq" by auto
next
  have "wf_conn CImp [ψ, ψ']" by (simp add: binary_connectives_def)
  then have "φ ≼ conn CImp [ψ, ψ'] ⟷
    (φ = conn CImp [ψ, ψ'] ∨ (∃ψ''. ψ'' ∈ set [ψ, ψ'] ∧ φ ≼ ψ''))"
    using wf_subformula_conn_cases by metis
  then show "?P FImp" by auto
qed

lemma wf_conn_helper_facts[iff]:
  "wf_conn CNot [φ]"
  "wf_conn CT []"
  "wf_conn CF []"
  "wf_conn (CVar x) []"
  "wf_conn CAnd [φ, ψ]"
  "wf_conn COr [φ, ψ]"
  "wf_conn CImp [φ, ψ]"
  "wf_conn CEq [φ, ψ]"
  using wf_conn.intros unfolding binary_connectives_def by fastforce+

lemma exists_c_conn: "∃ c l. φ = conn c l ∧ wf_conn c l"
  by (cases φ) force+

lemma subformula_conn_decomp[simp]:
  assumes wf: "wf_conn c l"
  shows "φ ≼ conn c l ⟷ (φ = conn c l ∨ (∃ ψ∈ set l. φ ≼ ψ))" (is "?A ⟷ ?B")
proof (rule iffI)
  {
    fix ξ
    have "φ ≼ ξ ⟹ ξ = conn c l ⟹ wf_conn c l ⟹ ∀x::'a propo∈set l. ¬ φ ≼ x ⟹ φ = conn c l"
      apply (induct rule: subformula.induct)
        apply simp
      using conn_inj by blast
  }
  moreover assume ?A
  ultimately show ?B using wf by metis
next
  assume ?B
  then show "φ ≼ conn c l" using wf wf_subformula_conn_cases by blast
qed

lemma subformula_leaf_explicit[simp]:
  "φ ≼ FT ⟷ φ = FT"
  "φ ≼ FF ⟷ φ = FF"
  "φ ≼ FVar x ⟷ φ = FVar x"
  apply auto
  using subformula_leaf by metis +

text ‹The variables inside the formula gives precisely the variables that are needed for the
  formula.›
primrec vars_of_prop:: "'v propo ⇒ 'v set" where
"vars_of_prop FT = {}" |
"vars_of_prop FF = {}" |
"vars_of_prop (FVar x) = {x}" |
"vars_of_prop (FNot φ) = vars_of_prop φ" |
"vars_of_prop (FAnd φ ψ) = vars_of_prop φ ∪ vars_of_prop ψ" |
"vars_of_prop (FOr φ ψ) = vars_of_prop φ ∪ vars_of_prop ψ" |
"vars_of_prop (FImp φ ψ) = vars_of_prop φ ∪ vars_of_prop ψ" |
"vars_of_prop (FEq φ ψ) = vars_of_prop φ ∪ vars_of_prop ψ"

lemma vars_of_prop_incl_conn:
  fixes ξ ξ' :: "'v propo list" and ψ :: "'v propo" and c :: "'v connective"
  assumes corr: "wf_conn c l" and incl: "ψ ∈ set l"
  shows "vars_of_prop ψ ⊆ vars_of_prop (conn c l)"
proof (cases c rule: connective_cases_arity_2)
  case nullary
  then have False using corr incl by auto
  then show "vars_of_prop ψ ⊆ vars_of_prop (conn c l)" by blast
next
  case binary note c = this
  then obtain a b where ab: "l = [a, b]"
    using wf_conn_bin_list_length list_length2_decomp corr by metis
  then have "ψ = a ∨ ψ = b" using incl by auto
  then show "vars_of_prop ψ ⊆ vars_of_prop (conn c l)"
    using ab c unfolding binary_connectives_def by auto
next
  case unary note c = this
  fix φ :: "'v propo"
  have "l = [ψ]" using corr c incl split_list by force
  then show "vars_of_prop ψ ⊆ vars_of_prop (conn c l)" using c by auto
qed

text ‹The set of variables is compatible with the subformula order.›
lemma subformula_vars_of_prop:
  "φ ≼ ψ ⟹ vars_of_prop φ ⊆ vars_of_prop ψ"
  apply (induct rule: subformula.induct)
  apply simp
  using vars_of_prop_incl_conn by blast


subsection ‹Positions›

text ‹Instead of 1 or 2 we use @{term L} or @{term R}›
datatype sign = L | R

text ‹We use @{term nil} instead of @{term ε}.›
fun pos :: "'v propo ⇒ sign list set" where
"pos FF = {[]}" |
"pos FT = {[]}" |
"pos (FVar x) = {[]}" |
"pos (FAnd φ ψ) = {[]} ∪ { L # p | p. p∈ pos φ} ∪ { R # p | p. p∈ pos ψ}" |
"pos (FOr φ ψ) = {[]} ∪ { L # p | p. p∈ pos φ} ∪ { R # p | p. p∈ pos ψ}" |
"pos (FEq φ ψ) = {[]} ∪ { L # p | p. p∈ pos φ} ∪ { R # p | p. p∈ pos ψ}" |
"pos (FImp φ ψ) = {[]} ∪ { L # p | p. p∈ pos φ} ∪ { R # p | p. p∈ pos ψ}" |
"pos (FNot φ) = {[]} ∪ { L # p | p. p∈ pos φ}"

lemma finite_pos: "finite (pos φ)"
  by (induct φ, auto)

lemma finite_inj_comp_set:
  fixes s :: "'v set"
  assumes finite: "finite s"
  and inj: "inj f"
  shows "card ({f p |p. p ∈ s}) = card s"
  using finite
proof (induct s rule: finite_induct)
  show "card {f p |p. p ∈ {}} = card {}" by auto
next
  fix x :: "'v" and s:: "'v set"
  assume f: "finite s" and notin: "x ∉ s"
  and IH: "card {f p |p. p ∈ s} = card s"
  have f': "finite {f p |p. p ∈ insert x s}" using f by auto
  have notin': "f x ∉ {f p |p. p ∈ s}" using notin inj injD by fastforce
  have "{f p |p. p ∈ insert x s} = insert (f x) {f p |p. p∈ s}" by auto
  then have "card {f p |p. p ∈ insert x s} = 1 + card {f p |p. p ∈ s}"
    using finite card_insert_disjoint f' notin' by auto
  moreover have "… = card (insert x s)" using notin f IH by auto
  finally show "card {f p |p. p ∈ insert x s} = card (insert x s)" .
qed

lemma cons_inject:
  "inj ((#) s)"
  by (meson injI list.inject)

lemma finite_insert_nil_cons:
  "finite s ⟹ card (insert [] {L # p |p. p ∈ s}) = 1 + card {L # p |p. p ∈ s}"
  using card_insert_disjoint by auto


lemma cord_not[simp]:
  "card (pos (FNot φ)) = 1 + card (pos φ)"
by (simp add: cons_inject finite_inj_comp_set finite_pos)

lemma card_seperate:
  assumes "finite s1" and "finite s2"
  shows "card ({L # p |p. p ∈ s1} ∪ {R # p |p. p ∈ s2}) = card ({L # p |p. p ∈ s1})
           + card({R # p |p. p ∈ s2})" (is "card (?L∪?R) = card ?L + card ?R")
proof -
  have "finite ?L" using assms by auto
  moreover have "finite ?R" using assms by auto
  moreover have "?L ∩ ?R = {}" by blast
  ultimately show ?thesis using assms card_Un_disjoint by blast
qed

definition prop_size where "prop_size φ = card (pos φ)"

lemma prop_size_vars_of_prop:
  fixes φ :: "'v propo"
  shows "card (vars_of_prop φ) ≤ prop_size φ"
  (* TODO Tune proof *)
  unfolding prop_size_def apply (induct φ, auto simp add: cons_inject finite_inj_comp_set finite_pos)
proof -
  fix φ1 φ2 :: "'v propo"
  assume IH1: "card (vars_of_prop φ1) ≤ card (pos φ1)"
  and IH2: "card (vars_of_prop φ2) ≤ card (pos φ2)"
  let ?L = "{L # p |p. p ∈ pos φ1}"
  let ?R = "{R # p |p. p ∈ pos φ2}"
  have "card (?L ∪ ?R) = card ?L +  card ?R"
    using card_seperate finite_pos by blast
  moreover have "… = card (pos φ1) + card (pos φ2)"
    by (simp add: cons_inject finite_inj_comp_set finite_pos)
  moreover have "… ≥ card (vars_of_prop φ1) + card (vars_of_prop φ2)" using IH1 IH2 by arith
  then have "… ≥ card (vars_of_prop φ1 ∪ vars_of_prop φ2)" using card_Un_le le_trans by blast
  ultimately
    show "card (vars_of_prop φ1 ∪ vars_of_prop φ2) ≤ Suc (card (?L ∪ ?R))"
         "card (vars_of_prop φ1 ∪ vars_of_prop φ2) ≤ Suc (card (?L ∪ ?R))"
         "card (vars_of_prop φ1 ∪ vars_of_prop φ2) ≤ Suc (card (?L ∪ ?R))"
         "card (vars_of_prop φ1 ∪ vars_of_prop φ2) ≤ Suc (card (?L ∪ ?R))"
    by auto
qed

value "pos (FImp (FAnd (FVar P) (FVar Q)) (FOr (FVar P) (FVar Q)))"

inductive path_to :: "sign list ⇒ 'v propo ⇒ 'v propo ⇒ bool" where
path_to_refl[intro]: "path_to [] φ φ" |
path_to_l: "c∈binary_connectives ∨ c = CNot ⟹ wf_conn c (φ#l) ⟹ path_to p φ φ'⟹
  path_to (L#p) (conn c (φ#l)) φ'" |
path_to_r: "c∈binary_connectives ⟹ wf_conn c (ψ#φ#[]) ⟹ path_to p φ φ' ⟹
  path_to (R#p) (conn c (ψ#φ#[])) φ'"

text ‹There is a deep link between subformulas and pathes: a (correct) path leads to a subformula
  and a subformula is associated to a given path.›
lemma path_to_subformula:
  "path_to p φ φ' ⟹ φ' ≼ φ"
  apply (induct rule: path_to.induct)
    apply simp
   apply (metis list.set_intros(1) subformula_into_subformula)
  using subformula_trans subformula_in_binary_conn(2) by metis

lemma subformula_path_exists:
  fixes φ φ':: "'v propo"
  shows "φ' ≼ φ ⟹ ∃p. path_to p φ φ'"
proof (induct rule: subformula.induct)
  case subformula_refl
  have "path_to [] φ' φ'" by auto
  then show "∃p. path_to p φ' φ'" by metis
next
  case (subformula_into_subformula ψ l c)
  note wf = this(2) and IH = this(4) and ψ = this(1)
  then obtain p where p: "path_to p ψ φ'" by metis
  {
    fix x :: "'v"
    assume "c = CT ∨ c = CF ∨ c = CVar x"
    then have "False" using subformula_into_subformula by auto
    then have "∃p. path_to p (conn c l) φ'" by blast
  }
  moreover {
    assume c: "c = CNot"
    then have "l = [ψ]" using wf ψ wf_conn_Not_decomp by fastforce
    then have "path_to (L # p) (conn c l) φ'" by (metis c wf_conn_unary p path_to_l)
   then have "∃p. path_to p (conn c l) φ'" by blast
  }
  moreover {
    assume c: "c∈ binary_connectives"
    obtain a b where ab: "[a, b] = l" using subformula_into_subformula c wf_conn_bin_list_length
      list_length2_decomp by metis
    then have "a = ψ ∨ b = ψ" using ψ by auto
    then have "path_to (L # p) (conn c l) φ' ∨ path_to (R # p) (conn c l) φ'" using c path_to_l
      path_to_r p ab by (metis wf_conn_binary)
    then have "∃p. path_to p (conn c l) φ'" by blast
  }
  ultimately show "∃p. path_to p (conn c l) φ'" using connective_cases_arity by metis
qed

fun replace_at :: "sign list ⇒ 'v propo ⇒ 'v propo ⇒ 'v propo" where
"replace_at [] _ ψ = ψ" |
"replace_at (L # l) (FAnd φ φ') ψ = FAnd (replace_at l φ ψ) φ'"|
"replace_at (R # l) (FAnd φ φ') ψ = FAnd φ (replace_at l φ' ψ)" |
"replace_at (L # l) (FOr φ φ') ψ = FOr (replace_at l φ ψ) φ'" |
"replace_at (R # l) (FOr φ φ') ψ = FOr φ (replace_at l φ' ψ)" |
"replace_at (L # l) (FEq φ φ') ψ = FEq (replace_at l φ ψ) φ'"|
"replace_at (R # l) (FEq φ φ') ψ = FEq φ (replace_at l φ' ψ)" |
"replace_at (L # l) (FImp φ φ') ψ = FImp (replace_at l φ ψ) φ'"|
"replace_at (R # l) (FImp φ φ') ψ = FImp φ (replace_at l φ' ψ)" |
"replace_at (L # l) (FNot φ) ψ = FNot (replace_at l φ ψ)"


section ‹Semantics over the Syntax›

text ‹Given the syntax defined above, we define a semantics, by defining an evaluation function
  @{term eval}. This function is the bridge between the logic as we define it here and the built-in
  logic of Isabelle.›
fun eval :: "('v ⇒ bool) ⇒ 'v propo ⇒ bool" (infix "⊨" 50) where
"𝒜 ⊨ FT = True" |
"𝒜 ⊨ FF = False" |
"𝒜 ⊨ FVar v = (𝒜 v)" |
"𝒜 ⊨ FNot φ = (¬(𝒜⊨ φ))" |
"𝒜 ⊨ FAnd φ⇩1 φ⇩2 = (𝒜⊨φ⇩1 ∧ 𝒜⊨φ⇩2)" |
"𝒜 ⊨ FOr φ⇩1 φ⇩2 = (𝒜⊨φ⇩1 ∨ 𝒜⊨φ⇩2)" |
"𝒜 ⊨ FImp φ⇩1 φ⇩2 = (𝒜⊨φ⇩1 ⟶ 𝒜⊨φ⇩2)" |
"𝒜 ⊨ FEq φ⇩1 φ⇩2 = (𝒜⊨φ⇩1 ⟷ 𝒜 ⊨φ⇩2)"

definition evalf (infix "⊨f" 50) where
"evalf φ ψ = (∀A. A ⊨ φ ⟶ A ⊨ ψ)"

text ‹The deduction rule is in the book. And the proof looks like to the one of the book.›
theorem deduction_theorem:
  "φ ⊨f ψ ⟷ (∀A. A ⊨ FImp φ ψ)"
proof
  assume H: "φ ⊨f ψ"
  {
    fix A
    have "A ⊨ FImp φ ψ"
      proof (cases "A ⊨ φ")
        case True
        then have "A ⊨ ψ" using H unfolding evalf_def by metis
        then show "A ⊨ FImp φ ψ" by auto
      next
        case False
        then show "A ⊨ FImp φ ψ" by auto
      qed
  }
  then show "∀A. A ⊨ FImp φ ψ" by blast
next
  assume A: "∀A. A ⊨ FImp φ ψ"
  show "φ ⊨f ψ"
    proof (rule ccontr)
      assume "¬ φ ⊨f ψ"
      then obtain A where "A ⊨ φ" and "¬ A ⊨ ψ" using evalf_def by metis
      then have "¬ A ⊨ FImp φ ψ" by auto
      then show False using A by blast
    qed
qed

text ‹A shorter proof:›
lemma "φ ⊨f ψ ⟷ (∀A. A⊨ FImp φ ψ)"
  by (simp add: evalf_def)

definition same_over_set:: "('v ⇒ bool) ⇒('v ⇒ bool) ⇒ 'v set ⇒ bool" where
"same_over_set A B S = (∀c∈S. A c = B c)"

text ‹If two mapping @{term A} and @{term B} have the same value over the variables, then the same
  formula are satisfiable.›
lemma same_over_set_eval:
  assumes "same_over_set A B (vars_of_prop φ)"
  shows "A ⊨ φ ⟷ B ⊨ φ"
  using assms unfolding same_over_set_def by (induct φ, auto)

end