Theory Ground_Reduction_on_GTRS

section โ€นReducing Rewrite Properties to Properties on Ground Terms over Ground Systemsโ€บ
theory Ground_Reduction_on_GTRS
  imports
    Rewriting_Properties
    Rewriting_GTRS
    Rewriting_LLRG_LV_Mondaic
begin

lemma ground_sys_nf_eq_lift:
  fixes โ„› :: "('f, 'v) term rel" 
  assumes gtrs: "ground_sys โ„›" "ground_sys ๐’ฎ"
    and nf: "NF (gsrstep โ„ฑ โ„›) = NF (gsrstep โ„ฑ ๐’ฎ)"
  shows "NF (srstep โ„ฑ โ„›) = NF (srstep โ„ฑ ๐’ฎ)"
proof -
  {fix s ๐’ฐ ๐’ฑ assume ass: "ground_sys (๐’ฐ :: ('f, 'v) term rel)" "ground_sys ๐’ฑ"
    "NF (gsrstep โ„ฑ ๐’ฐ) = NF (gsrstep โ„ฑ ๐’ฑ)" "s โˆˆ NF (srstep โ„ฑ ๐’ฐ)"
    have "s โˆˆ NF (srstep โ„ฑ ๐’ฑ)"
    proof (rule ccontr)
      assume "s โˆ‰ NF (srstep โ„ฑ ๐’ฑ)"
      then obtain C l r ฯƒ where step: "(l, r) โˆˆ ๐’ฑ" and rep: "s = CโŸจl โ‹… ฯƒโŸฉ"
        and funas: "funas_ctxt C โŠ† โ„ฑ" "funas_term l โŠ† โ„ฑ" "funas_term r โŠ† โ„ฑ" using ass(2)
        by (auto simp: funas_term_subst NF_def sig_step_def dest!: rstep_imp_C_s_r) blast
      from step ass(2) rep have rep: "s = CโŸจlโŸฉ" "ground l" "ground r"
        by (auto intro: ground_subst_apply)
      from step rep(2-) funas have "l โˆ‰ NF (gsrstep โ„ฑ ๐’ฑ)"
        by (auto simp: NF_def sig_step_def Image_def)
      from this ass(3) have "l โˆ‰ NF (srstep โ„ฑ ๐’ฐ)" by auto
      then obtain t where "(l, t) โˆˆ srstep โ„ฑ ๐’ฐ" by auto
      from srstep_ctxt_closed[OF funas(1) this, unfolded rep(1)[symmetric]]
      show False using ass(4) 
        by auto
    qed}
    then show ?thesis using assms
      by (smt (verit, best) equalityI subsetI)
qed

lemma ground_sys_inv:
 "ground_sys โ„› โŸน ground_sys (โ„›ยฏ)" by auto

lemma ground_sys_symcl:
 "ground_sys โ„› โŸน ground_sys (โ„›โ†”)" by auto

lemma ground_sys_comp_rrstep_rel'_ground:
  assumes "ground_sys โ„›" "ground_sys ๐’ฎ"
   and "(s, t) โˆˆ comp_rrstep_rel' โ„ฑ โ„› ๐’ฎ"
 shows "ground s" "ground t"
proof -
  from assms(3) consider (a) "(s, t) โˆˆ srsteps_with_root_step โ„ฑ โ„› O (srstep โ„ฑ ๐’ฎ)+" |
    (b) "(s, t) โˆˆ (srstep โ„ฑ โ„›)+ O srsteps_with_root_step โ„ฑ ๐’ฎ"
    by auto
  then have "ground s โˆง ground t"
  proof cases
    case a
    then show ?thesis using srsteps_with_root_step_ground(1)[OF assms(1)]
      using srsteps_with_root_step_ground(2)[OF assms(1), THEN srsteps_pres_ground_l[OF assms(2)]]
      by blast
  next
    case b
    then show ?thesis using srsteps_with_root_step_ground(2)[OF assms(2)]
      using srsteps_with_root_step_ground(1)[OF assms(2), THEN srsteps_pres_ground_r[OF assms(1)]]
      by blast
  qed
  then show "ground s" "ground t" by simp_all
qed

lemma GTRS_commute:
  assumes "ground_sys โ„›" "ground_sys ๐’ฎ"
   and com: "commute (gsrstep โ„ฑ โ„›) (gsrstep โ„ฑ ๐’ฎ)"
  shows "commute (srstep โ„ฑ โ„›) (srstep โ„ฑ ๐’ฎ)"
proof -
  {fix s t assume ass: "(s, t) โˆˆ comp_rrstep_rel' โ„ฑ (โ„›ยฏ) ๐’ฎ"
    then obtain u where steps: "(s, u) โˆˆ (srstep โ„ฑ (โ„›ยฏ))+" "(u, t) โˆˆ (srstep โ„ฑ ๐’ฎ)+"
      by (auto simp: sig_step_converse_rstep dest: srsteps_with_root_step_srstepsD)
    have gr: "ground s" "ground t" "ground u"
      using ground_sys_comp_rrstep_rel'_ground[OF ground_sys_inv[OF assms(1)] assms(2) ass]
      using srsteps_pres_ground_r[OF assms(2) _ steps(2)] by auto
    then have "(s, u) โˆˆ  (gsrstep โ„ฑ (โ„›ยฏ))*" "(u, t) โˆˆ (gsrstep โ„ฑ ๐’ฎ)*" using steps
      by (auto dest!: trancl_into_rtrancl intro: ground_srsteps_eq_gsrsteps_eq)
    then have "(s, t) โˆˆ (gsrstep โ„ฑ ๐’ฎ)* O (gsrstep โ„ฑ (โ„›ยฏ))*" using com steps
      by (auto simp: commute_def rew_converse_inwards)
    from gsrsteps_eq_relcomp_srsteps_relcompD[OF this]
    have "commute_redp โ„ฑ โ„› ๐’ฎ s t" unfolding commute_redp_def
      by (simp add: rew_converse_inwards)}
  then show ?thesis by (intro commute_rrstep_intro) simp
qed

lemma GTRS_CR:
  assumes "ground_sys โ„›"
   and "CR (gsrstep โ„ฑ โ„›)"
  shows "CR (srstep โ„ฑ โ„›)" using GTRS_commute assms
  unfolding CR_iff_self_commute
  by blast


lemma GTRS_SCR:
  assumes gtrs: "ground_sys โ„›"
   and scr: "SCR (gsrstep โ„ฑ โ„›)"
  shows "SCR (srstep โ„ฑ โ„›)"
proof -
  {fix s t u assume ass: "(s, t) โˆˆ srstep โ„ฑ โ„›" "(s, u) โˆˆ srstep โ„ฑ โ„›"
    and root: "(s, t) โˆˆ sig_step โ„ฑ (rrstep โ„›) โˆจ (s, u) โˆˆ sig_step โ„ฑ (rrstep โ„›)"
    from ass have funas: "funas_term s โŠ† โ„ฑ" "funas_term t โŠ† โ„ฑ" "funas_term u โŠ† โ„ฑ" by blast+
    from root have gr: "ground s" "ground t" "ground u" using ass gtrs
      using srrstep_ground srstep_pres_ground_l srstep_pres_ground_r
      by metis+
    from scr obtain v where v: "(t, v) โˆˆ (gsrstep โ„ฑ โ„›)= โˆง (u, v) โˆˆ (gsrstep โ„ฑ โ„›)*"
      using gr unfolding SCR_on_def
      by (metis Int_iff UNIV_I ass mem_Collect_eq mem_Sigma_iff)
    then have "SCRp โ„ฑ โ„› t u"
    by (metis (full_types) Int_iff Un_iff gsrsteps_eq_to_srsteps_eq)}
  then show ?thesis by (intro SCR_rrstep_intro) (metis srrstep_to_srestep)+ 
qed

lemma GTRS_WCR:
  assumes gtrs: "ground_sys โ„›"
   and wcr: "WCR (gsrstep โ„ฑ โ„›)"
  shows "WCR (srstep โ„ฑ โ„›)"
proof -
  {fix s t u assume ass: "(s, t) โˆˆ sig_step โ„ฑ (rrstep โ„›)" "(s, u) โˆˆ srstep โ„ฑ โ„›"
    from ass have funas: "funas_term s โŠ† โ„ฑ" "funas_term t โŠ† โ„ฑ" "funas_term u โŠ† โ„ฑ" by blast+
    from srrstep_ground[OF gtrs ass(1)] have gr: "ground s" "ground t" "ground u"
      using srstep_pres_ground_l[OF gtrs _ ass(2)]
      by simp_all
    from this wcr have w: "(t, u) โˆˆ (gsrstep โ„ฑ โ„›)โ†“" using ass funas
      unfolding WCR_on_def
      by (metis IntI SigmaI UNIV_I mem_Collect_eq srrstep_to_srestep)
    then have "(t, u) โˆˆ (srstep โ„ฑ โ„›)โ†“" unfolding join_def
      by (metis (full_types) gsrsteps_eq_to_srsteps_eq joinD joinI join_def)}
  then show ?thesis by (intro WCR_rrstep_intro) simp
qed

lemma GTRS_UNF:
  assumes gtrs: "ground_sys โ„›"
   and unf: "UNF (gsrstep โ„ฑ โ„›)"
  shows "UNF (srstep โ„ฑ โ„›)"
proof -
  {fix s t assume ass: "(s, t) โˆˆ comp_rrstep_rel' โ„ฑ (โ„›ยฏ) โ„›"
    then obtain u where steps: "(s, u) โˆˆ (srstep โ„ฑ (โ„›ยฏ))+" "(u, t) โˆˆ (srstep โ„ฑ โ„›)+"
      by (auto simp: sig_step_converse_rstep dest: srsteps_with_root_step_srstepsD)
    have gr: "ground s" "ground t" "ground u"
      using ground_sys_comp_rrstep_rel'_ground[OF ground_sys_inv[OF gtrs] gtrs ass]
      using srsteps_pres_ground_r[OF gtrs  _ steps(2)] by auto
    from steps(1) have f: "funas_term s โŠ† โ„ฑ" by (simp add: srstepsD) 
    let ?ฯƒ = "ฮป _. s"
    from steps gr have "(s, u โ‹… ?ฯƒ) โˆˆ (gsrstep โ„ฑ (โ„›ยฏ))+" "(u โ‹… ?ฯƒ, t) โˆˆ (gsrstep โ„ฑ โ„›)+"
      unfolding srstep_converse_dist Restr_converse trancl_converse
      using srsteps_subst_closed[where ?ฯƒ = ?ฯƒ and ?s = u, of _ โ„ฑ] f
      by (force simp: ground_subst_apply intro: ground_srsteps_gsrsteps)+
    then have "UN_redp โ„ฑ โ„› s t" using unf ground_NF_srstep_gsrstep[OF gr(1), of โ„ฑ โ„›]
      using ground_NF_srstep_gsrstep[OF gr(2), of โ„ฑ โ„›]
        by (auto simp: UNF_on_def UN_redp_def normalizability_def rew_converse_outwards)
           (meson trancl_into_rtrancl)}
  then show ?thesis by (intro UNF_rrstep_intro) simp
qed


lemma GTRS_UNC:
  assumes gtrs: "ground_sys โ„›"
   and unc: "UNC (gsrstep โ„ฑ โ„›)"
  shows "UNC (srstep โ„ฑ โ„›)"
proof -
  {fix s t assume ass: "(s, t) โˆˆ srsteps_with_root_step โ„ฑ (โ„›โ†”)"
    from ass have funas: "funas_term s โŠ† โ„ฑ" "funas_term t โŠ† โ„ฑ"
      by (meson srstepsD srsteps_with_root_step_srstepsD)+
    from ass have "ground s" "ground t" using srsteps_with_root_step_ground[OF ground_sys_symcl[OF gtrs]]
      by auto
    then have "UN_redp โ„ฑ โ„› s t" unfolding UN_redp_def using ass unc unfolding UNC_def
      by (simp add: ground_NF_srstep_gsrstep ground_srsteps_eq_gsrsteps_eq gsrstep_conversion_dist srsteps_with_root_step_sresteps_eqD)}
  then show ?thesis by (intro UNC_rrstep_intro) simp
qed


lemma GTRS_NFP:
  assumes "ground_sys โ„›"
   and nfp: "NFP (gsrstep โ„ฑ โ„›)"
  shows "NFP (srstep โ„ฑ โ„›)"
proof -
  {fix s t assume ass: "(s, t) โˆˆ comp_rrstep_rel' โ„ฑ (โ„›ยฏ) โ„›"
    from ass have funas: "funas_term s โŠ† โ„ฑ" "funas_term t โŠ† โ„ฑ"
      by (meson Un_iff relcompEpair srstepsD srsteps_with_root_step_srstepsD)+
    from ass have "ground s" "ground t"
      by (metis assms(1) ground_sys_comp_rrstep_rel'_ground ground_sys_inv)+
    from this ass have "(s, t) โˆˆ (gsrstep โ„ฑ (โ„›ยฏ))* O (gsrstep โ„ฑ โ„›)*"
      by (intro srsteps_eq_relcomp_gsrsteps_relcomp) (auto dest!: srsteps_with_root_step_sresteps_eqD)
    then have "t โˆˆ NF (gsrstep โ„ฑ  โ„›) โŸน (s, t) โˆˆ (gsrstep โ„ฑ โ„›)*" using NFP_stepD[OF nfp]
      by (auto simp: rew_converse_outwards)
    then have "NFP_redp โ„ฑ โ„› s t" unfolding NFP_redp_def
      by (simp add: โ€นground tโ€บ ground_NF_srstep_gsrstep gsrsteps_eq_to_srsteps_eq)}
  then show ?thesis by (intro NFP_rrstep_intro) simp
qed


lemma GTRS_NE_aux:
  assumes "(s, t) โˆˆ srsteps_with_root_step โ„ฑ โ„›"
   and gtrs: "ground_sys โ„›" "ground_sys ๐’ฎ"
   and ne: "NE (gsrstep โ„ฑ โ„›) (gsrstep โ„ฑ ๐’ฎ)"
  shows "NE_redp โ„ฑ โ„› ๐’ฎ s t"
proof -
  from assms(1) have gr: "ground s" "ground t"
    using srsteps_with_root_step_ground[OF gtrs(1)] by simp_all
  have "(s, t) โˆˆ (gsrstep โ„ฑ โ„›)+" using gr assms(1)
    by (auto dest: srsteps_with_root_step_srstepsD intro: ground_srsteps_gsrsteps)
  then have "t โˆˆ NF (srstep โ„ฑ โ„›) โŸน (s, t) โˆˆ (gsrstep โ„ฑ ๐’ฎ)*"
    using gr ne unfolding NE_on_def
    by (auto simp: normalizability_def ground_subst_apply dest!: trancl_into_rtrancl) blast
  then show "NE_redp โ„ฑ โ„› ๐’ฎ s t" unfolding NE_redp_def
    by (simp add: gsrsteps_eq_to_srsteps_eq)
qed

lemma GTRS_NE:
  assumes gtrs: "ground_sys โ„›" "ground_sys ๐’ฎ"
   and ne: "NE (gsrstep โ„ฑ โ„›) (gsrstep โ„ฑ ๐’ฎ)"
  shows "NE (srstep โ„ฑ โ„›) (srstep โ„ฑ ๐’ฎ)"
proof -
  {fix s t assume "(s, t) โˆˆ srsteps_with_root_step โ„ฑ โ„›"
    from GTRS_NE_aux[OF this gtrs ne] have "NE_redp โ„ฑ โ„› ๐’ฎ s t"
      by simp}
  moreover
  {fix s t assume "(s, t) โˆˆ srsteps_with_root_step โ„ฑ ๐’ฎ"
    from GTRS_NE_aux[OF this gtrs(2, 1) NE_symmetric[OF ne]]
    have "NE_redp โ„ฑ ๐’ฎ โ„› s t" by simp}
  ultimately show ?thesis
    using ground_sys_nf_eq_lift[OF gtrs NE_NF_eq[OF ne]]
    by (intro NE_rrstep_intro) auto
qed


lemma gtrs_CE_aux:
  assumes step:"(s, t) โˆˆ srsteps_with_root_step โ„ฑ (โ„›โ†”)"
   and gtrs: "ground_sys โ„›" "ground_sys ๐’ฎ"
   and ce: "CE (gsrstep โ„ฑ โ„›) (gsrstep โ„ฑ ๐’ฎ)"
  shows "(s, t) โˆˆ (srstep โ„ฑ ๐’ฎ)โ†”*"
proof -
  from step gtrs(1) have "ground s" "ground t"
    by (metis ground_sys_symcl srsteps_with_root_step_ground)+
  then have "(s, t) โˆˆ (gsrstep โ„ฑ โ„›)โ†”*" using step
    by (simp add: ground_srsteps_eq_gsrsteps_eq gsrstep_conversion_dist srsteps_with_root_step_sresteps_eqD)
  then have "(s, t) โˆˆ (gsrstep โ„ฑ ๐’ฎ)โ†”*" using ce unfolding CE_on_def
    by blast
  then show "(s, t) โˆˆ (srstep โ„ฑ ๐’ฎ)โ†”*"
    by (simp add: gsrstep_conversion_dist gsrsteps_eq_to_srsteps_eq symcl_srsteps_conversion)
qed


lemma gtrs_CE:
  assumes gtrs: "ground_sys โ„›" "ground_sys ๐’ฎ"
   and ce: "CE (gsrstep โ„ฑ โ„›) (gsrstep โ„ฑ ๐’ฎ)"
  shows "CE (srstep โ„ฑ โ„›) (srstep โ„ฑ ๐’ฎ)"
proof -
  {fix s t assume "(s, t) โˆˆ srsteps_with_root_step โ„ฑ (โ„›โ†”)"
    from gtrs_CE_aux[OF this gtrs ce] have "(s, t) โˆˆ (srstep โ„ฑ ๐’ฎ)โ†”*" by simp}
  moreover
  {fix s t assume "(s, t) โˆˆ srsteps_with_root_step โ„ฑ (๐’ฎโ†”)"
    from gtrs_CE_aux[OF this gtrs(2, 1) CE_symmetric[OF ce]]
    have "(s, t) โˆˆ (srstep โ„ฑ โ„›)โ†”*" by simp}
  ultimately show ?thesis
    by (intro CE_rrstep_intro) auto
qed

end