Theory Prop_Abstract_Transformation

theory Prop_Abstract_Transformation
imports Entailment_Definition.Prop_Logic Weidenbach_Book_Base.Wellfounded_More

begin

text ‹This file is devoted to abstract properties of the transformations, like consistency
  preservation and lifting from terms to proposition. ›


section ‹Rewrite Systems and Properties›

subsection ‹Lifting of Rewrite Rules›

text ‹We can lift a rewrite relation r over a full1 formula: the relation ‹r› works on terms,
  while ‹propo_rew_step› works on formulas.›

inductive propo_rew_step :: "('v propo ⇒ 'v propo ⇒ bool) ⇒ 'v propo ⇒ 'v propo ⇒ bool"
  for r :: "'v propo ⇒ 'v propo ⇒ bool" where
global_rel: "r φ ψ ⟹ propo_rew_step r φ ψ" |
propo_rew_one_step_lift: "propo_rew_step r φ φ' ⟹ wf_conn c (ψs @ φ # ψs')
  ⟹ propo_rew_step r (conn c (ψs @ φ # ψs')) (conn c (ψs @ φ'# ψs'))"

text ‹Here is a more precise link between the lifting and the subformulas: if a rewriting takes
  place between @{term φ} and @{term φ'}, then there are two subformulas @{term ψ} in @{term φ} and
  @{term ψ'} in @{term φ'}, @{term ψ'} is the result of the rewriting of @{term r} on @{term ψ}. ›

text ‹This lemma is only a health condition:›
lemma propo_rew_step_subformula_imp:
shows "propo_rew_step r φ φ' ⟹ ∃ ψ ψ'. ψ ≼ φ ∧ ψ' ≼ φ' ∧ r ψ ψ'"
  apply (induct rule: propo_rew_step.induct)
    using subformula.simps subformula_into_subformula apply blast
  using wf_conn_no_arity_change subformula_into_subformula wf_conn_no_arity_change_helper
  in_set_conv_decomp by metis


text ‹The converse is moreover true: if there is a @{term ψ} and @{term ψ'}, then every formula
  @{term φ} containing @{term ψ}, can be rewritten into a formula @{term φ'}, such that it contains
  @{term φ'}. ›
lemma propo_rew_step_subformula_rec:
  fixes ψ ψ' φ :: "'v propo"
  shows "ψ ≼ φ ⟹ r ψ ψ' ⟹ (∃φ'. ψ' ≼ φ' ∧ propo_rew_step r φ φ')"
proof (induct φ rule: subformula.induct)
  case subformula_refl
  then have "propo_rew_step r ψ ψ'" using propo_rew_step.intros by auto
  moreover have "ψ' ≼ ψ'" using Prop_Logic.subformula_refl by auto
  ultimately show "∃φ'. ψ' ≼ φ' ∧ propo_rew_step r ψ φ'" by fastforce
next
  case (subformula_into_subformula ψ'' l c)
  note IH = this(4) and r = this(5) and ψ'' = this(1) and wf = this(2) and incl = this(3)
  then obtain φ' where *: "ψ' ≼ φ' ∧ propo_rew_step r ψ'' φ'" by metis
  moreover obtain ξ ξ' :: "'v propo list" where
    l: "l = ξ @ ψ'' # ξ'" using List.split_list ψ'' by metis
  ultimately have "propo_rew_step r (conn c l) (conn c (ξ @ φ' # ξ'))"
    using propo_rew_step.intros(2) wf by metis
  moreover have "ψ' ≼ conn c (ξ @ φ' # ξ')"
    using wf * wf_conn_no_arity_change Prop_Logic.subformula_into_subformula
    by (metis (no_types) in_set_conv_decomp l wf_conn_no_arity_change_helper)
  ultimately show "∃φ'. ψ' ≼ φ' ∧ propo_rew_step r (conn c l) φ'" by metis
qed

lemma propo_rew_step_subformula:
  "(∃ψ ψ'. ψ ≼ φ ∧ r ψ ψ') ⟷ (∃φ'. propo_rew_step r φ φ')"
  using propo_rew_step_subformula_imp propo_rew_step_subformula_rec by metis+

lemma consistency_decompose_into_list:
  assumes wf: "wf_conn c l" and wf': "wf_conn c l'"
  and same: "∀n. A ⊨ l ! n ⟷ (A ⊨ l' ! n)"
  shows "A ⊨ conn c l ⟷ A ⊨ conn c l'"
proof (cases c rule: connective_cases_arity_2)
  case nullary
  then show "(A ⊨ conn c l) ⟷ (A ⊨ conn c l')" using wf wf' by auto
next
  case unary note c = this
  then obtain a where l: "l = [a]" using wf_conn_Not_decomp wf by metis
  obtain a' where l': "l' = [a']" using wf_conn_Not_decomp wf' c by metis
  have "A ⊨ a ⟷ A ⊨ a'" using l l' by (metis nth_Cons_0 same)
  then show "A ⊨ conn c l ⟷ A ⊨ conn c l'" using l l' c by auto
next
  case binary note c = this
  then obtain a b where l: "l = [a, b]"
    using wf_conn_bin_list_length list_length2_decomp wf by metis
  obtain a' b' where l': "l' = [a', b']"
    using wf_conn_bin_list_length list_length2_decomp wf' c by metis

  have p: "A ⊨ a ⟷ A ⊨ a'" "A ⊨ b ⟷ A ⊨ b'"
    using l l' same by (metis diff_Suc_1 nth_Cons' nat.distinct(2))+
  show "A ⊨ conn c l ⟷ A ⊨ conn c l'"
    using wf c p unfolding binary_connectives_def l l' by auto
qed

text ‹Relation between @{term propo_rew_step} and the rewriting we have seen before:
  @{term "propo_rew_step r φ φ'"} means that we rewrite @{term ψ} inside @{term φ}
  (ie at a path @{term p}) into @{term ψ'}.›
lemma propo_rew_step_rewrite:
  fixes φ φ' :: "'v propo" and r :: "'v propo ⇒ 'v propo ⇒ bool"
  assumes "propo_rew_step r φ φ'"
  shows "∃ψ ψ' p. r ψ ψ' ∧ path_to p φ ψ ∧ replace_at p φ ψ' = φ'"
  using assms
proof (induct rule: propo_rew_step.induct)
  case(global_rel φ ψ)
  moreover have "path_to [] φ φ" by auto
  moreover have "replace_at [] φ ψ = ψ" by auto
  ultimately show ?case by metis
next
  case (propo_rew_one_step_lift φ φ' c ξ ξ') note rel = this(1) and IH0 = this(2) and corr = this(3)
  obtain ψ ψ' p where IH: "r ψ ψ' ∧ path_to p φ ψ ∧ replace_at p φ ψ' = φ'" using IH0 by metis

  {
     fix x :: "'v"
     assume "c = CT ∨ c = CF ∨ c = CVar x"
     then have False using corr by auto
     then have "∃ψ ψ' p. r ψ ψ' ∧ path_to p (conn c (ξ@ (φ # ξ'))) ψ
                       ∧ replace_at p (conn c (ξ@ (φ # ξ'))) ψ' = conn c (ξ@ (φ' # ξ')) "
       by fast
  }
  moreover {
     assume c: "c = CNot"
     then have empty: "ξ =[]" "ξ'=[]" using corr by auto
     have "path_to (L#p) (conn c (ξ@ (φ # ξ'))) ψ"
       using c empty IH wf_conn_unary path_to_l by fastforce
     moreover have "replace_at (L#p) (conn c (ξ@ (φ # ξ'))) ψ' = conn c (ξ@ (φ' # ξ'))"
       using c empty IH by auto
     ultimately have "∃ψ ψ' p. r ψ ψ' ∧ path_to p (conn c (ξ@ (φ # ξ'))) ψ
                               ∧ replace_at p (conn c (ξ@ (φ # ξ'))) ψ' = conn c (ξ@ (φ' # ξ'))"
     using IH by metis
  }
  moreover {
     assume c: "c ∈ binary_connectives"
     have "length (ξ@ φ # ξ') = 2" using wf_conn_bin_list_length corr c by metis
     then have "length ξ + length ξ' = 1" by auto
     then have ld: "(length ξ = 1 ∧ length ξ' = 0) ∨ (length ξ = 0 ∧ length ξ' = 1) " by arith
     obtain a b where ab: "(ξ=[] ∧ ξ'=[b]) ∨ (ξ=[a] ∧ ξ'=[])"
       using ld by (case_tac ξ, case_tac ξ', auto)
     {
        assume φ: "ξ=[] ∧ ξ'=[b]"
        have "path_to (L#p) (conn c (ξ@ (φ # ξ'))) ψ"
          using φ c IH ab corr by (simp add: path_to_l)
        moreover have "replace_at (L#p) (conn c (ξ@ (φ # ξ'))) ψ' = conn c (ξ@ (φ' # ξ'))"
          using c IH ab φ unfolding binary_connectives_def by auto
        ultimately have "∃ψ ψ' p. r ψ ψ' ∧ path_to p (conn c (ξ@ (φ # ξ'))) ψ
          ∧ replace_at p (conn c (ξ@ (φ # ξ'))) ψ' = conn c (ξ@ (φ' # ξ')) "
          using IH by metis
     }
     moreover {
        assume φ: "ξ=[a]" " ξ'=[]"
        then have "path_to (R#p) (conn c (ξ@ (φ # ξ'))) ψ"
          using c IH corr path_to_r corr φ  by (simp add: path_to_r)
        moreover have "replace_at (R#p) (conn c (ξ@ (φ # ξ'))) ψ' = conn c (ξ@ (φ' # ξ'))"
          using c IH ab φ unfolding binary_connectives_def by auto
        ultimately have ?case using IH by metis
     }
     ultimately have ?case using ab by blast
  }
  ultimately show ?case using connective_cases_arity by blast
qed



subsection ‹Consistency Preservation›

text ‹We define ‹preserve_models›: it means that a relation preserves consistency.›
definition preserve_models where
"preserve_models r ⟷ (∀φ ψ. r φ ψ ⟶ (∀A. A ⊨ φ ⟷ A ⊨ ψ))"


lemma propo_rew_step_preservers_val_explicit:
"propo_rew_step r φ ψ ⟹ preserve_models r ⟹ propo_rew_step r φ ψ ⟹ (∀A. A ⊨φ ⟷ A⊨ψ)"
  unfolding preserve_models_def
proof (induction rule: propo_rew_step.induct)
  case global_rel
  then show ?case by simp
next
  case (propo_rew_one_step_lift φ φ' c ξ ξ') note rel = this(1) and wf = this(2)
    and IH = this(3)[OF this(4) this(1)]  and consistent = this(4)
  {
    fix A
    from IH have "∀n. (A ⊨ (ξ @ φ # ξ') ! n) = (A ⊨ (ξ @ φ' # ξ') ! n)"
      by (metis (mono_tags, hide_lams) list_update_length nth_Cons_0 nth_append_length_plus
        nth_list_update_neq)
    then have " (A ⊨ conn c (ξ @ φ # ξ')) = (A ⊨ conn c (ξ @ φ' # ξ'))"
      by (meson consistency_decompose_into_list wf wf_conn_no_arity_change_helper
        wf_conn_no_arity_change)
  }
  then show "∀A. A ⊨ conn c (ξ @ φ # ξ') ⟷ A ⊨ conn c (ξ @ φ' # ξ')" by auto
qed


lemma propo_rew_step_preservers_val':
  assumes "preserve_models r"
  shows "preserve_models (propo_rew_step r)"
  using assms by (simp add: preserve_models_def propo_rew_step_preservers_val_explicit)


lemma preserve_models_OO[intro]:
"preserve_models f ⟹ preserve_models g ⟹ preserve_models (f OO g) "
  unfolding preserve_models_def by auto


lemma star_consistency_preservation_explicit:
  assumes "(propo_rew_step r)^** φ ψ" and "preserve_models r"
  shows "∀A. A ⊨ φ ⟷ A ⊨ ψ"
  using assms by (induct rule: rtranclp_induct)
    (auto simp add: propo_rew_step_preservers_val_explicit)

lemma star_consistency_preservation:
"preserve_models r ⟹  preserve_models (propo_rew_step r)^**"
  by (simp add: star_consistency_preservation_explicit preserve_models_def)

subsection "Full Lifting"
text ‹In the previous a relation was lifted to a formula, now we define the relation such it is
  applied as long as possible. The definition is thus simply: it can be derived and nothing more can
  be derived.›

lemma full_ropo_rew_step_preservers_val[simp]:
"preserve_models r ⟹ preserve_models (full (propo_rew_step r))"
  by (metis full_def preserve_models_def star_consistency_preservation)

lemma full_propo_rew_step_subformula:
"full (propo_rew_step r) φ' φ ⟹ ¬(∃ ψ ψ'. ψ ≼ φ ∧ r ψ ψ')"
  unfolding full_def using propo_rew_step_subformula_rec by metis


section ‹Transformation testing›

subsection ‹Definition and first Properties›
text ‹To prove correctness of our transformation, we create a @{term all_subformula_st} predicate.
  It tests recursively all subformulas. At each step, the actual formula is tested. The aim of this
  @{term test_symb} function is to test locally some properties of the formulas (i.e. at the level
  of the connective or at first level). This allows a clause description between the rewrite
  relation and the @{term test_symb}›


definition all_subformula_st :: "('a propo ⇒ bool) ⇒ 'a propo ⇒ bool" where
"all_subformula_st test_symb φ ≡ ∀ψ. ψ ≼ φ ⟶ test_symb ψ"


lemma test_symb_imp_all_subformula_st[simp]:
  "test_symb FT ⟹ all_subformula_st test_symb FT"
  "test_symb FF ⟹ all_subformula_st test_symb FF"
  "test_symb (FVar x) ⟹ all_subformula_st test_symb (FVar x)"
  unfolding all_subformula_st_def using subformula_leaf by metis+


lemma all_subformula_st_test_symb_true_phi:
  "all_subformula_st test_symb φ ⟹ test_symb φ"
  unfolding all_subformula_st_def by auto

lemma all_subformula_st_decomp_imp:
  "wf_conn c l ⟹ (test_symb (conn c l) ∧ (∀φ∈ set l. all_subformula_st test_symb φ))
  ⟹ all_subformula_st test_symb (conn c l)"
  unfolding all_subformula_st_def by auto


text ‹To ease the finding of proofs, we give some explicit theorem about the decomposition.›
lemma all_subformula_st_decomp_rec:
  "all_subformula_st test_symb (conn c l) ⟹ wf_conn c l
    ⟹ (test_symb (conn c l) ∧ (∀φ∈ set l. all_subformula_st test_symb φ))"
  unfolding all_subformula_st_def by auto

lemma all_subformula_st_decomp:
  fixes c :: "'v connective" and l :: "'v propo list"
  assumes "wf_conn c l"
  shows "all_subformula_st test_symb (conn c l)
    ⟷ (test_symb (conn c l) ∧ (∀φ∈ set l. all_subformula_st test_symb φ))"
  using assms all_subformula_st_decomp_rec all_subformula_st_decomp_imp by metis

lemma helper_fact: "c ∈ binary_connectives ⟷ (c = COr ∨ c = CAnd ∨ c = CEq ∨ c = CImp)"
  unfolding binary_connectives_def by auto
lemma all_subformula_st_decomp_explicit[simp]:
  fixes φ ψ :: "'v propo"
  shows "all_subformula_st test_symb (FAnd φ ψ)
      ⟷ (test_symb (FAnd φ ψ) ∧ all_subformula_st test_symb φ ∧ all_subformula_st test_symb ψ)"
  and "all_subformula_st test_symb (FOr φ ψ)
     ⟷ (test_symb (FOr φ ψ) ∧  all_subformula_st test_symb φ ∧ all_subformula_st test_symb ψ)"
  and "all_subformula_st test_symb (FNot φ)
     ⟷ (test_symb (FNot φ) ∧  all_subformula_st test_symb φ)"
  and "all_subformula_st test_symb (FEq φ ψ)
     ⟷ (test_symb (FEq φ ψ) ∧  all_subformula_st test_symb φ ∧ all_subformula_st test_symb ψ)"
  and "all_subformula_st test_symb (FImp φ ψ)
     ⟷ (test_symb (FImp φ ψ) ∧ all_subformula_st test_symb φ ∧ all_subformula_st test_symb ψ)"
proof -
  have "all_subformula_st test_symb (FAnd φ ψ) ⟷ all_subformula_st test_symb (conn CAnd [φ, ψ])"
    by auto
  moreover have "… ⟷test_symb (conn CAnd [φ, ψ])∧(∀ξ∈ set [φ, ψ]. all_subformula_st test_symb ξ)"
    using all_subformula_st_decomp wf_conn_helper_facts(5) by metis
  finally show "all_subformula_st test_symb (FAnd φ ψ)
    ⟷ (test_symb (FAnd φ ψ) ∧ all_subformula_st test_symb φ ∧ all_subformula_st test_symb ψ)"
    by simp

  have "all_subformula_st test_symb (FOr φ ψ) ⟷ all_subformula_st test_symb (conn COr [φ, ψ])"
    by auto
  moreover have "…⟷
    (test_symb (conn COr [φ, ψ]) ∧ (∀ξ∈ set [φ, ψ]. all_subformula_st test_symb ξ))"
    using all_subformula_st_decomp wf_conn_helper_facts(6) by metis
  finally show "all_subformula_st test_symb (FOr φ ψ)
    ⟷ (test_symb (FOr φ ψ) ∧ all_subformula_st test_symb φ ∧ all_subformula_st test_symb ψ)"
    by simp

  have "all_subformula_st test_symb (FEq φ ψ) ⟷ all_subformula_st test_symb (conn CEq [φ, ψ])"
    by auto
  moreover have "…
    ⟷ (test_symb (conn CEq [φ, ψ]) ∧ (∀ξ∈ set [φ, ψ]. all_subformula_st test_symb ξ))"
    using all_subformula_st_decomp wf_conn_helper_facts(8) by metis
  finally show "all_subformula_st test_symb (FEq φ ψ)
    ⟷ (test_symb (FEq φ ψ) ∧ all_subformula_st test_symb φ ∧ all_subformula_st test_symb ψ)"
    by simp

  have "all_subformula_st test_symb (FImp φ ψ) ⟷ all_subformula_st test_symb (conn CImp [φ, ψ])"
    by auto
  moreover have "…
    ⟷(test_symb (conn CImp [φ, ψ]) ∧ (∀ξ∈ set [φ, ψ]. all_subformula_st test_symb ξ))"
    using all_subformula_st_decomp wf_conn_helper_facts(7) by metis
  finally show "all_subformula_st test_symb (FImp φ ψ)
    ⟷ (test_symb (FImp φ ψ) ∧ all_subformula_st test_symb φ ∧ all_subformula_st test_symb ψ)"
    by simp

  have "all_subformula_st test_symb (FNot φ) ⟷ all_subformula_st test_symb (conn CNot [φ])"
    by auto
  moreover have "… = (test_symb (conn CNot [φ]) ∧ (∀ξ∈ set [φ]. all_subformula_st test_symb ξ))"
    using all_subformula_st_decomp wf_conn_helper_facts(1) by metis
  finally show "all_subformula_st test_symb (FNot φ)
    ⟷ (test_symb (FNot φ) ∧ all_subformula_st test_symb φ)" by simp
qed



text ‹As @{term all_subformula_st} tests recursively, the function is true on every subformula. ›
lemma subformula_all_subformula_st:
  "ψ ≼ φ ⟹ all_subformula_st test_symb φ ⟹ all_subformula_st test_symb ψ"
  by (induct rule: subformula.induct, auto simp add: all_subformula_st_decomp)


text ‹The following theorem @{prop no_test_symb_step_exists} shows the link between the
  @{term test_symb} function and the corresponding rewrite relation @{term r}: if we assume that if
  every time @{term test_symb} is true, then a @{term r} can be applied, finally as long as
  @{term "¬ all_subformula_st test_symb φ"}, then something can be rewritten in @{term φ}.›
lemma no_test_symb_step_exists:
  fixes r:: "'v propo ⇒ 'v propo ⇒ bool" and test_symb:: "'v propo ⇒ bool" and x :: "'v"
  and φ :: "'v propo"
  assumes
    test_symb_false_nullary: "∀x. test_symb FF ∧ test_symb FT ∧ test_symb (FVar x)" and
    "∀φ'. φ' ≼ φ ⟶ (¬test_symb φ') ⟶  (∃ ψ. r φ' ψ)" and
    "¬ all_subformula_st test_symb φ"
  shows "∃ψ ψ'. ψ ≼ φ ∧ r ψ ψ'"
  using assms
proof (induct φ rule: propo_induct_arity)
  case (nullary φ x)
  then show "∃ψ ψ'. ψ ≼ φ ∧ r ψ ψ'"
    using wf_conn_nullary test_symb_false_nullary by fastforce
next
  case (unary φ) note IH = this(1)[OF this(2)] and r = this(2)  and nst = this(3) and subf = this(4)
  from r IH nst have H: " ¬ all_subformula_st test_symb φ ⟹ ∃ψ. ψ ≼ φ ∧ (∃ψ'. r ψ ψ')"
    by (metis subformula_in_subformula_not subformula_refl subformula_trans)
  {
    assume n: "¬test_symb (FNot φ)"
    obtain ψ where "r (FNot φ) ψ" using subformula_refl r n nst by blast
    moreover have "FNot φ ≼ FNot φ" using subformula_refl by auto
    ultimately have "∃ψ ψ'. ψ ≼ FNot φ ∧ r ψ ψ'" by metis
  }
  moreover {
    assume n: "test_symb (FNot φ)"
    then have "¬ all_subformula_st test_symb φ"
      using all_subformula_st_decomp_explicit(3) nst subf by blast
    then have "∃ψ ψ'. ψ ≼ FNot φ ∧ r ψ ψ'"
      using H subformula_in_subformula_not subformula_refl subformula_trans by blast
  }
  ultimately show "∃ψ ψ'. ψ ≼ FNot φ ∧ r ψ ψ'" by blast
next
  case (binary φ φ1 φ2)
  note IHφ1_0 = this(1)[OF this(4)] and IHφ2_0 = this(2)[OF this(4)] and r = this(4)
    and φ = this(3) and le = this(5) and nst = this(6)

  obtain c :: "'v connective" where
    c: "(c = CAnd ∨ c = COr ∨ c = CImp ∨ c = CEq) ∧ conn c [φ1, φ2] = φ"
    using φ by fastforce

  then have corr: "wf_conn c [φ1, φ2]" using wf_conn.simps unfolding binary_connectives_def by auto
  have inc: "φ1 ≼ φ" "φ2 ≼ φ" using binary_connectives_def c subformula_in_binary_conn by blast+
  from r IHφ1_0 have IHφ1: "¬ all_subformula_st test_symb φ1 ⟹ ∃ψ ψ'. ψ ≼ φ1 ∧ r ψ ψ'"
    using inc(1) subformula_trans le by blast
  from r IHφ2_0 have IHφ2: "¬ all_subformula_st test_symb φ2 ⟹ ∃ψ. ψ ≼ φ2 ∧ (∃ψ'. r ψ ψ')"
    using inc(2) subformula_trans le by blast
  have cases: "¬test_symb φ ∨ ¬all_subformula_st test_symb φ1 ∨ ¬all_subformula_st test_symb φ2"
    using c nst by auto
  show "∃ψ ψ'. ψ ≼ φ ∧ r ψ ψ'"
    using IHφ1 IHφ2 subformula_trans inc subformula_refl cases le by blast
qed

subsection ‹Invariant conservation›
text ‹If two rewrite relation are independant (or at least independant enough), then the property
  characterizing the first relation @{term "all_subformula_st test_symb"} remains true. The next
  show the same property, with changes in the assumptions.›

text ‹The assumption @{term "∀φ' ψ. φ' ≼ Φ ⟶ r φ' ψ ⟶ all_subformula_st test_symb φ'
  ⟶ all_subformula_st test_symb ψ"} means that rewriting with @{term r} does not mess up the
  property we want to preserve locally.›

text ‹The previous assumption is not enough to go from @{term r} to @{term "propo_rew_step r"}: we
  have to add the assumption that rewriting inside does not mess up the term:
  @{term "∀(c:: 'v connective) ξ φ ξ' φ'. φ ≼ Φ ⟶ propo_rew_step r φ φ'
  ⟶ wf_conn c (ξ @ φ # ξ') ⟶ test_symb (conn c (ξ @ φ # ξ')) ⟶ test_symb φ'
  ⟶ test_symb (conn c (ξ @ φ' # ξ'))"}›


subsubsection ‹Invariant while lifting of the Rewriting Relation›

text ‹The condition @{term "φ ≼ Φ"} (that will by used with @{term "Φ = φ"} most of the time) is
  here to ensure that the recursive conditions on @{term "Φ"} will moreover hold for the subterm
  we are rewriting. For example if there is no equivalence symbol in @{term "Φ"}, we do not have to
  care about equivalence symbols in the two previous assumptions.›

lemma propo_rew_step_inv_stay':
  fixes r:: "'v propo ⇒ 'v propo ⇒ bool" and test_symb:: "'v propo ⇒ bool" and x :: "'v"
  and φ ψ Φ:: "'v propo"
  assumes H: "∀φ' ψ. φ' ≼ Φ ⟶ r φ' ψ ⟶ all_subformula_st test_symb φ'
    ⟶ all_subformula_st test_symb ψ"
  and H': "∀(c:: 'v connective) ξ φ ξ' φ'. φ ≼ Φ ⟶ propo_rew_step r φ φ'
    ⟶ wf_conn c (ξ @ φ # ξ') ⟶ test_symb (conn c (ξ @ φ # ξ')) ⟶ test_symb φ'
    ⟶ test_symb (conn c (ξ @ φ' # ξ'))" and
    "propo_rew_step r φ ψ" and
    "φ ≼ Φ" and
    "all_subformula_st test_symb φ"
  shows "all_subformula_st test_symb ψ"
  using assms(3-5)
proof (induct rule: propo_rew_step.induct)
  case global_rel
  then show ?case using H by simp
next
  case (propo_rew_one_step_lift φ φ' c ξ ξ')
  note rel = this(1) and φ = this(2) and corr = this(3) and Φ = this(4) and nst = this(5)
  have sq: "φ ≼ Φ"
    using Φ corr subformula_into_subformula subformula_refl subformula_trans
    by (metis in_set_conv_decomp)
  from corr have "∀ ψ. ψ ∈ set (ξ @ φ # ξ') ⟶ all_subformula_st test_symb ψ"
    using all_subformula_st_decomp nst by blast
  then have *: "∀ψ. ψ ∈ set (ξ @ φ' # ξ') ⟶ all_subformula_st test_symb ψ" using φ sq by fastforce
  then have "test_symb φ'" using all_subformula_st_test_symb_true_phi by auto
  moreover from corr nst have "test_symb (conn c (ξ @ φ # ξ'))"
    using all_subformula_st_decomp by blast
  ultimately have test_symb: "test_symb (conn c (ξ @ φ' # ξ'))" using H' sq corr rel by blast

  have "wf_conn c (ξ @ φ' # ξ')"
    by (metis wf_conn_no_arity_change_helper corr wf_conn_no_arity_change)
  then show "all_subformula_st test_symb (conn c (ξ @ φ' # ξ'))"
    using * test_symb by (metis all_subformula_st_decomp)
qed


text ‹The need for @{term "φ ≼ Φ"} is not always necessary, hence we moreover have a version
  without inclusion. ›
lemma propo_rew_step_inv_stay:
  fixes r:: "'v propo ⇒ 'v propo ⇒ bool" and test_symb:: "'v propo ⇒ bool" and x :: "'v"
  and φ ψ :: "'v propo"
  assumes
    H: "∀φ' ψ. r φ' ψ ⟶ all_subformula_st test_symb φ' ⟶ all_subformula_st test_symb ψ" and
    H': "∀(c:: 'v connective) ξ φ ξ' φ'. wf_conn c (ξ @ φ # ξ') ⟶ test_symb (conn c (ξ @ φ # ξ'))
      ⟶ test_symb φ' ⟶ test_symb (conn c (ξ @ φ' # ξ'))" and
    "propo_rew_step r φ ψ" and
    "all_subformula_st test_symb φ"
  shows "all_subformula_st test_symb ψ"
  using propo_rew_step_inv_stay'[of φ r test_symb φ ψ] assms subformula_refl by metis


text ‹The lemmas can be lifted to @{term "full (propo_rew_step r)"} instead of
  @{term propo_rew_step}›

subsubsection ‹Invariant after all Rewriting›

lemma full_propo_rew_step_inv_stay_with_inc:
  fixes r:: "'v propo ⇒ 'v propo ⇒ bool" and test_symb:: "'v propo ⇒ bool" and x :: "'v"
  and φ ψ :: "'v propo"
  assumes
    H: "∀ φ ψ. propo_rew_step r φ ψ ⟶ all_subformula_st test_symb φ
      ⟶ all_subformula_st test_symb ψ" and
    H': "∀(c:: 'v connective) ξ φ ξ' φ'. φ ≼ Φ ⟶ propo_rew_step r φ φ'
      ⟶ wf_conn c (ξ @ φ # ξ') ⟶ test_symb (conn c (ξ @ φ # ξ')) ⟶ test_symb φ'
      ⟶ test_symb (conn c (ξ @ φ' # ξ'))" and
      "φ ≼ Φ" and
    full: "full (propo_rew_step r) φ ψ" and
    init: "all_subformula_st test_symb φ"
  shows "all_subformula_st test_symb ψ"
  using assms unfolding full_def
proof -
  have rel: "(propo_rew_step r)⇧*⇧* φ ψ"
    using full unfolding full_def by auto
  then show "all_subformula_st test_symb ψ "
    using init
    proof (induct rule: rtranclp_induct)
      case base
      then show "all_subformula_st test_symb φ" by blast
    next
      case (step b c) note star = this(1) and IH = this(3) and one = this(2) and all = this(4)
      then have "all_subformula_st test_symb b" by metis
      then show "all_subformula_st test_symb c" using propo_rew_step_inv_stay' H H' rel one by auto
    qed
qed

lemma full_propo_rew_step_inv_stay':
  fixes r:: "'v propo ⇒ 'v propo ⇒ bool" and test_symb:: "'v propo ⇒ bool" and x :: "'v"
  and φ ψ :: "'v propo"
  assumes
    H: "∀ φ ψ. propo_rew_step r φ ψ ⟶ all_subformula_st test_symb φ
      ⟶ all_subformula_st test_symb ψ" and
    H': "∀(c:: 'v connective) ξ φ ξ' φ'. propo_rew_step r φ φ' ⟶ wf_conn c (ξ @ φ # ξ')
      ⟶ test_symb (conn c (ξ @ φ # ξ')) ⟶ test_symb φ' ⟶ test_symb (conn c (ξ @ φ' # ξ'))" and
    full: "full (propo_rew_step r) φ ψ" and
    init: "all_subformula_st test_symb φ"
  shows "all_subformula_st test_symb ψ"
  using full_propo_rew_step_inv_stay_with_inc[of r test_symb φ] assms subformula_refl by metis

lemma full_propo_rew_step_inv_stay:
  fixes r:: "'v propo ⇒ 'v propo ⇒ bool" and test_symb:: "'v propo ⇒ bool" and x :: "'v"
  and φ ψ :: "'v propo"
  assumes
    H: "∀φ ψ. r φ ψ ⟶ all_subformula_st test_symb φ ⟶ all_subformula_st test_symb ψ" and
    H': "∀(c:: 'v connective) ξ φ ξ' φ'. wf_conn c (ξ @ φ # ξ') ⟶ test_symb (conn c (ξ @ φ # ξ'))
      ⟶ test_symb φ' ⟶ test_symb (conn c (ξ @ φ' # ξ'))" and
    full: "full (propo_rew_step r) φ ψ" and
    init: "all_subformula_st test_symb φ"
  shows "all_subformula_st test_symb ψ"
  unfolding full_def
proof -
  have rel: "(propo_rew_step r)^** φ ψ"
    using full unfolding full_def by auto
  then show "all_subformula_st test_symb ψ"
    using init
    proof (induct rule: rtranclp_induct)
      case base
      then show "all_subformula_st test_symb φ" by blast
    next
      case (step b c)
      note star = this(1) and IH = this(3) and one = this(2) and all = this(4)
      then have "all_subformula_st test_symb b" by metis
      then show "all_subformula_st test_symb c"
        using propo_rew_step_inv_stay subformula_refl H H' rel one by auto
    qed
qed


lemma full_propo_rew_step_inv_stay_conn:
  fixes r:: "'v propo ⇒ 'v propo ⇒ bool" and test_symb:: "'v propo ⇒ bool" and x :: "'v"
  and φ ψ :: "'v propo"
  assumes
    H: "∀φ ψ. r φ ψ ⟶ all_subformula_st test_symb φ ⟶ all_subformula_st test_symb ψ" and
    H': "∀(c:: 'v connective) l l'. wf_conn c l ⟶ wf_conn c l'
      ⟶ (test_symb (conn c l) ⟷ test_symb (conn c l'))" and
    full: "full (propo_rew_step r) φ ψ" and
    init: "all_subformula_st test_symb φ"
  shows "all_subformula_st test_symb ψ"
proof -
  have "⋀(c:: 'v connective) ξ φ ξ' φ'. wf_conn c (ξ @ φ # ξ')
    ⟹ test_symb (conn c (ξ @ φ # ξ')) ⟹ test_symb φ' ⟹ test_symb (conn c (ξ @ φ' # ξ'))"
    using H'  by (metis wf_conn_no_arity_change_helper wf_conn_no_arity_change)
  then show "all_subformula_st test_symb ψ"
    using H full init full_propo_rew_step_inv_stay by blast
qed

end