Как поднять транзитивное отношение к конечным картам?

Question

Я пытаюсь доказать, что транзитивное отношение на элементах конечных отображений эквивалентно транзитивному отношению на самих конечных отображениях.

Вот вспомогательная лемма, которая показывает, что отношения на конечных отображениях транзитивныесли отношения на их элементах транзитивны:

lemma fmrel_trans:
  "(⋀x y z. x ∈ fmran' xm ⟹ P x y ⟹ Q y z ⟹ R x z) ⟹
   fmrel P xm ym ⟹ fmrel Q ym zm ⟹ fmrel R xm zm"
  unfolding fmrel_iff
  by (metis fmdomE fmdom_notD fmran'I option.rel_inject(2) option.rel_sel)

Вот первая лемма, которую я успешно доказал:

lemma trancl_to_fmrel:
  "(fmrel f)⇧+⇧+ xm ym ⟹ fmrel f⇧+⇧+ xm ym"
  apply (induct rule: tranclp_induct)
  apply (simp add: fmap.rel_mono_strong)
  apply (rule_tac ?P="f⇧+⇧+" and ?Q="f" and ?ym="y" in fmrel_trans; auto)
  done

А вот симметричная лемма, которую я не могу доказать:

lemma fmrel_to_trancl:
  "fmrel r⇧+⇧+ xm ym ⟹
   (⋀x. r x x) ⟹
   (fmrel r)⇧+⇧+ xm ym"

Эквивалентно эту лемму можно сформулировать как

lemma fmrel_tranclp_induct:
  "fmrel r⇧+⇧+ a b ⟹
   (⋀x. r x x) ⟹
   (⋀y. fmrel r a y ⟹ P y) ⟹
   (⋀y z. fmrel r⇧+⇧+ a y ⟹ fmrel r y z ⟹ P y ⟹ P z) ⟹ P b"

или

lemma fmrel_tranclp_trans_induct:
  "fmrel r⇧+⇧+ a b ⟹
   (⋀x. r x x) ⟹
   (⋀x y. fmrel r x y ⟹ P x y) ⟹
   (⋀x y z. fmrel r⇧+⇧+ x y ⟹ P x y ⟹ fmrel r⇧+⇧+ y z ⟹ P y z ⟹ P x z) ⟹ P a b"

Доказывая любую из этих 3 лемм, я могу доказать остальное.

Вопрос очень похож на Как поднять транзитивное отношение от элементов к спискам? Но доказательство в этом вопросе основано на правиле индукции list_all2_induct.Я не могу найти подобное правило для fmrel.Я пытался доказать что-то подобное, но безуспешно:

lemma fmrel_induct
  [consumes 1, case_names Nil Cons, induct set: fmrel]:
  assumes P: "fmrel P xs ys"
  assumes Nil: "R fmempty fmempty"
  assumes Cons: "⋀k x xs y ys.
    ⟦P x y; fmrel P xs ys; fmlookup xs k = None; fmlookup ys k = None; R xs ys⟧ ⟹
    R (fmupd k x xs) (fmupd k y ys)"
  shows "R xs ys"

Я также пытался заменить fmrel на list_all2 в леммах, но безуспешно:

lemma fmrel_to_list_all2:
  "fmrel f xm ym ⟹
   xs = map snd (sorted_list_of_fmap xm) ⟹
   ys = map snd (sorted_list_of_fmap ym) ⟹
   list_all2 f xs ys"

Идея состоит в том, что ключи (домены) xm и ym равны.И fmrel эквивалентно list_all2 на отсортированных значениях (диапазонах) карт.

Не могли бы вы помочь мне доказать fmrel_to_trancl?

Answer 1

ОБНОВЛЕНИЕ

Этот вопрос и некоторые из предыдущих вопросов, на которые я ответил на этом сайте, побудили меня начать сбор дополнительных результатов о list, alist и fmap внезависимая библиотека.Работа выполняется в контексте GitHub хранилище .Хранилище содержит все теоремы в этом ответе.Эти теоремы можно найти в теории Quotient_FMap.

Несколько других теорем из моих предыдущих ответов (в обновленном виде) также можно найти в хранилище.Надеемся, что репозиторий содержит другие полезные результаты о вышеупомянутых типах.

---

Оригинальный ответ (включая незначительные поправки) можно найти ниже (наследие).Тем не менее, важно отметить, что ответ содержит несколько плохих методов кодирования Изабель.

theory so_htlartfm
imports 
  Complex_Main
  "HOL-Library.Finite_Map"
begin


lemma fmap_eqdom_Cons1:
  assumes as_1: "fmlookup xm i = None"
    and as_2: "fmrel R (fmupd i x xm) ym" 
  shows 
    "(∃z zm. 
    fmlookup zm i = None ∧ ym = (fmupd i z zm) ∧ R x z ∧ fmrel R xm zm)"
proof - 
  from as_2 have eq_dom: "fmdom (fmupd i x xm) = fmdom ym" 
    using fmrel_fmdom_eq by blast
  from as_1 eq_dom as_2 obtain y where y: "fmlookup ym i = Some y"
    by force
  obtain z zm where z_zm: "ym = (fmupd i z zm) ∧ fmlookup zm i = None"
    using y by (smt fmap_ext fmlookup_drop fmupd_lookup)
  {
    assume "¬R x z"
    with as_1 z_zm have "¬fmrel R (fmupd i x xm) ym"
      by (metis fmrel_iff fmupd_lookup option.simps(11))
  }
  with as_2 have c3: "R x z" by auto
  {
    assume "¬fmrel R xm zm"
    with as_1 have "¬fmrel R (fmupd i x xm) ym" 
      by (metis fmrel_iff fmupd_lookup option.rel_sel z_zm)
  }
  with as_2 have c4: "fmrel R xm zm" by auto
  from z_zm c3 c4 show ?thesis by auto
qed

lemma fmap_eqdom_induct [consumes 1, case_names nil step]:
  assumes R: "fmrel R xm ym"
    and nil: "P fmempty fmempty"
    and step: 
    "⋀x xm y ym i. ⟦R x y; fmrel R xm ym; P xm ym⟧ ⟹ 
    P (fmupd i x xm) (fmupd i y ym)"
  shows "P xm ym"
  using R 
proof(induct xm arbitrary: ym)
  case fmempty
  then show ?case
    by (metis fempty_iff fmdom_empty fmfilter_alt_defs(5) 
      fmfilter_false fmrel_fmdom_eq fmrestrict_fset_dom nil)
next
  case (fmupd i x xm) show ?case 
  proof -
    from fmupd.prems(1) obtain y where y: "fmlookup ym i = Some y"
      by (metis fmupd.prems(1) fmrel_cases fmupd_lookup option.discI)
    from fmupd.hyps(2) fmupd.prems(1) fmupd.prems(1) obtain z zm where 
      zm_i_none: "fmlookup zm i = None" and
      ym_eq_z_zm: "ym = (fmupd i z zm)" and 
      R_x_z: "R x z" and
      R_xm_zm: "fmrel R xm zm"
      using fmap_eqdom_Cons1 by metis
    with R_xm_zm fmupd.hyps(1) have P_xm_zm: "P xm zm" by blast
    from R_x_z R_xm_zm P_xm_zm have "P (fmupd i x xm) (fmupd i z zm)" 
      by (rule step)
    then show ?thesis by (simp add: ym_eq_z_zm)
  qed
qed

lemma fmrel_to_rtrancl:
  assumes as_r: "(⋀x. r x x)" 
    and rel_rpp_xm_ym: "(fmrel r⇧*⇧*) xm ym" 
  shows "(fmrel r)⇧*⇧* xm ym"
proof-
  from rel_rpp_xm_ym show "(fmrel r)⇧*⇧* xm ym"
  proof(induct rule: fmap_eqdom_induct)
    case nil then show ?case by auto
  next
    case (step x xm y ym i) show ?case
    proof -
      from as_r have lp_xs_xs: "fmrel r xm xm" by (simp add: fmap.rel_refl)
      from step.hyps(1) have x_xs_y_zs: 
        "(fmrel r)⇧*⇧* (fmupd i x xm) (fmupd i y xm)"
      proof(induction rule: rtranclp_induct)
        case base then show ?case by simp
      next
        case (step y z) then show ?case 
        proof -
          have rt_step_2: "(fmrel r)⇧*⇧* (fmupd i y xm) (fmupd i z xm)" 
            by (rule r_into_rtranclp, simp add: fmrel_upd lp_xs_xs step.hyps(2))
          from step.IH rt_step_2 show ?thesis by (rule rtranclp_trans) 
        qed      
      qed
      from step.hyps(3) have "(fmrel r)⇧*⇧* (fmupd i y xm) (fmupd i y ym)"
      proof(induction rule: rtranclp_induct)
        case base then show ?case by simp
      next
        case (step ya za) show ?case
        proof -
          have rt_step_2: "(fmrel r)⇧*⇧* (fmupd i y ya) (fmupd i y za)" 
            by (rule r_into_rtranclp, simp add: as_r fmrel_upd step.hyps(2)) 
          from step.IH rt_step_2 show ?thesis by (rule rtranclp_trans)
        qed
      qed
      with x_xs_y_zs show ?thesis by simp
    qed
  qed
qed

lemma fmrel_to_trancl:
  assumes as_r: "(⋀x. r x x)" 
    and rel_rpp_xm_ym: "(fmrel r⇧+⇧+) xm ym" 
  shows "(fmrel r)⇧+⇧+ xm ym" 
  by (metis as_r fmrel_to_rtrancl fmap.rel_mono_strong fmap.rel_refl 
      r_into_rtranclp reflclp_tranclp rel_rpp_xm_ym rtranclpD rtranclp_idemp 
      rtranclp_reflclp tranclp.r_into_trancl)

end