Какие функции сохраняют свойства замыкания?

Question

Я пытаюсь доказать следующие леммы:

lemma tranclp_fun_preserve:
  "(⋀x y. x ≠ y ⟹ f x ≠ f y) ⟹
   (⋀x y. f x ≠ f y ⟹ x ≠ y) ⟹
   (⋀x y. f x = f y ⟹ x = y) ⟹
   (λ x y. P x y)⇧+⇧+ (f x) (f y) ⟹ (λ x y. P (f x) (f y))⇧+⇧+ x y"
  apply (erule tranclp.cases)
  apply blast

lemma tranclp_fun_preserve2:
  "(⋀x y. x ≠ y ⟹ f x ≠ f y) ⟹
   (⋀x y. f x ≠ f y ⟹ x ≠ y) ⟹
   (⋀x y. f x = f y ⟹ x = y) ⟹
   (λ x y. P (f x) (f y))⇧+⇧+ x y ⟹ (λ x y. P x y)⇧+⇧+ (f x) (f y)"
  apply (erule tranclp.cases)
  apply blast

Однако я застрял.Стоит ли выбирать другой набор предположений для функции f?Не могли бы вы предложить, как доказать леммы tranclp_fun_preserve и tranclp_fun_preserve2?

---

ОБНОВЛЕНИЕ

Моя функция инъективна со специальным свойством, описанным в конце,Боюсь, что следующий пример слишком длинный.Тем не менее, я хочу сделать это немного более реалистичным.Вот два вспомогательных типа errorable и nullable:

(*** errorable ***)

notation
  bot ("⊥")

typedef 'a errorable ("_⇩⊥" [21] 21) = "UNIV :: 'a option set" ..

definition errorable :: "'a ⇒ 'a errorable" ("_⇩⊥" [1000] 1000) where
  "errorable x = Abs_errorable (Some x)"

instantiation errorable :: (type) bot
begin
definition "⊥ ≡ Abs_errorable None"
instance ..
end

free_constructors case_errorable for
  errorable
| "⊥ :: 'a errorable"
  apply (metis Rep_errorable_inverse bot_errorable_def errorable_def not_Some_eq)
  apply (metis Abs_errorable_inverse UNIV_I errorable_def option.inject)
  by (simp add: Abs_errorable_inject bot_errorable_def errorable_def)

(*** nullable ***)

class opt =
  fixes null :: "'a" ("ε")

typedef 'a nullable ("_⇩□" [21] 21) = "UNIV :: 'a option set" ..

definition nullable :: "'a ⇒ 'a nullable" ("_⇩□" [1000] 1000) where
  "nullable x = Abs_nullable (Some x)"

instantiation nullable :: (type) opt
begin
definition "ε ≡ Abs_nullable None"
instance ..
end

free_constructors case_nullable for
  nullable
| "ε :: 'a nullable"
  apply (metis Rep_nullable_inverse null_nullable_def nullable_def option.collapse)
  apply (simp add: Abs_nullable_inject nullable_def)
  by (metis Abs_nullable_inverse UNIV_I null_nullable_def nullable_def option.distinct(1))

Два вида значений:

datatype any = BoolVal "bool⇩⊥" | NatVal "nat⇩⊥" | RealVal "real⇩⊥" | InvalidAny unit

datatype oany = OBoolVal "bool⇩⊥⇩□" | ONatVal "nat⇩⊥⇩□" | ORealVal "real⇩⊥⇩□" | OInvalidAny "unit⇩□"

Вот конкретный пример функции f (any_to_oany), это инъективно:

inductive any_oany :: "any ⇒ oany ⇒ bool" where
  "any_oany (BoolVal x) (OBoolVal x⇩□)"
| "any_oany (NatVal x) (ONatVal x⇩□)"
| "any_oany (RealVal x) (ORealVal x⇩□)"
| "any_oany (InvalidAny x) (OInvalidAny x⇩□)"

fun any_to_oany :: "any ⇒ oany" where
  "any_to_oany (BoolVal x) = (OBoolVal x⇩□)"
| "any_to_oany (NatVal x) = (ONatVal x⇩□)"
| "any_to_oany (RealVal x) = (ORealVal x⇩□)"
| "any_to_oany (InvalidAny x) = (OInvalidAny x⇩□)"

lemma any_oany_eq_fun:
  "any_oany x y ⟷ any_to_oany x = y"
  by (cases x; cases y; auto simp: any_oany.simps)

Вот конкретный пример отношения P (cast_oany):

inductive cast_any :: "any ⇒ any ⇒ bool" where
  "cast_any (BoolVal ⊥) (InvalidAny ())"
| "cast_any (NatVal ⊥) (RealVal ⊥)"
| "cast_any (NatVal x⇩⊥) (RealVal (real x)⇩⊥)"
| "cast_any (RealVal ⊥) (InvalidAny ())"

inductive cast_oany :: "oany ⇒ oany ⇒ bool" where
  "cast_any x y ⟹ any_oany x ox ⟹ any_oany y oy ⟹
   cast_oany ox oy"
| "cast_oany (OBoolVal ε) (OInvalidAny ε)"
| "cast_oany (ONatVal ε) (ORealVal ε)"
| "cast_oany (ORealVal ε) (OInvalidAny ε)"

Я доказал эквивалентность cast_any и cast_oany on any:

lemma cast_any_implies_cast_oany:
  "cast_any x y ⟹ cast_oany (any_to_oany x) (any_to_oany y)"
  by (simp add: any_oany_eq_fun cast_oany.intros(1))

lemma cast_oany_implies_cast_any:
  "cast_oany (any_to_oany x) (any_to_oany y) ⟹ cast_any x y"
  by (cases x; cases y; simp add: any_oany.simps cast_oany.simps)

И моя конечная цель - доказать аналогичные леммы для транзитивных замыканий этих отношений:

lemma trancl_cast_oany_implies_cast_any:
  "cast_oany⇧+⇧+ (any_to_oany x) (any_to_oany y) ⟹ cast_any⇧+⇧+ x y"

lemma trancl_cast_any_implies_cast_oany:
  "cast_any⇧+⇧+ x y ⟹ cast_oany⇧+⇧+ (any_to_oany x) (any_to_oany y)"

Я доказал следующие промежуточные леммы:

lemma trancl_cast_oany_implies_cast_any':
  "(λx y. cast_oany (any_to_oany x) (any_to_oany y))⇧+⇧+ x y ⟹
   cast_any⇧+⇧+ x y"
  apply (erule tranclp_trans_induct)
  apply (simp add: cast_oany_implies_cast_any tranclp.r_into_trancl)
  by auto

lemma trancl_cast_any_implies_cast_oany':
  "cast_any⇧+⇧+ x y ⟹
   (λx y. cast_oany (any_to_oany x) (any_to_oany y))⇧+⇧+ x y"
  apply (erule tranclp_trans_induct)
  apply (simp add: cast_any_implies_cast_oany tranclp.r_into_trancl)
  by auto

Наконец, если бы я смог доказать следующие леммы из исходного вопроса, тогда я смогу доказать свои целевые леммы.

lemma tranclp_fun_preserve:
  "cast_oany⇧+⇧+ (any_to_oany x) (any_to_oany y) ⟹
   (λx y. cast_oany (any_to_oany x) (any_to_oany y))⇧+⇧+ x y"

lemma tranclp_fun_preserve2:
  "(λx y. cast_oany (any_to_oany x) (any_to_oany y))⇧+⇧+ x y ⟹
   cast_oany⇧+⇧+ (any_to_oany x) (any_to_oany y)"

В этом пункте я даю важное свойствофункции any_to_oany.Набор значений oany состоит из двух частей:

1. null (OBoolVal ε, ONatVal ε, ORealVal ε, OInvalidAny ε)
2. все остальные значения.

Отношение cast_oany связывает значения внутри первой части и внутри второй части отдельно.Не существует связи между значениями из разных частей.Функция any_to_oany отображает значения только для второй части.Я не знаю, как правильно назвать это свойство: подмножества 1 и 2 «закрыты» по отношению cast_oany.И функция any_to_oany отображает значения только в одно подмножество, и это биективно для этого подмножества.

Answer 1

Ответ на первоначальный вопрос

Этот ответ обеспечивает (мягкие) достаточные условия для функции, чтобы сохранить свойства замыкания на основе определения, выведенного из лемм tranclp_fun_preserveи tranclp_fun_preserve2 в вашем вопросе.

В частности, если функция биективна, то она сохраняет свойства замыкания.Доказательство в Изабель приведено ниже.Тем не менее, обратите внимание, что вполне вероятно, что доказательство может быть пересмотрено в лучшую сторону.

theory so_wkfppc_1
imports 
  Complex_Main
  "HOL-Library.FuncSet"

begin

lemma tranclp_fun_preserve_1:
  fixes f:: "'a ⇒ 'b"
    and R :: "'b ⇒ 'b ⇒ bool"
    and x x'::'a
  assumes as_f: "bij f"
    and prem: "R⇧+⇧+ (f x) (f x')"
  shows "(λ x x'. R (f x) (f x'))⇧+⇧+ x x'"
proof -
  define g where g: "g = the_inv_into UNIV f"
  define P where P: "P = (λ y y'. (λ x x'. R (f x) (f x'))⇧+⇧+ (g y) (g y'))" 
  define y where y: "y = f x"
  define y' where y': "y' = f x'" 
  from prem y y' have major: "R⇧+⇧+ y y'" by blast
  from P as_f g have cases_1: "⋀y y'. R y y' ⟹ P y y'"
    using bij_betw_imp_surj_on bij_is_inj f_the_inv_into_f by fastforce
  from P have cases_2: 
    "⋀x y z. R⇧+⇧+ x y ⟹ P x y ⟹ R⇧+⇧+ y z ⟹ P y z ⟹ P x z"
    by auto
  from major cases_1 cases_2 have "P y y'" by (rule tranclp_trans_induct)
  with P as_f y y' g show ?thesis by (simp add: bij_is_inj the_inv_f_f)    
qed

lemma tranclp_fun_preserve_2:
  fixes f:: "'a ⇒ 'b"
    and R :: "'b ⇒ 'b ⇒ bool"
    and x x'::'a
  assumes as_f: "bij f"
    and prem: "(λ x x'. R (f x) (f x'))⇧+⇧+ x x'"
  shows "R⇧+⇧+ (f x) (f x')"
proof -
  define P where P: "P = (λ x x'. (λ y y'. R y y')⇧+⇧+ (f x) (f x'))" 
  define r where r: "r = (λ x x'. R (f x) (f x'))"
  define y where y: "y = f x"
  define y' where y': "y' = f x'"
  from prem r y y' have major: "r⇧+⇧+ x x'" by blast
  from P as_f r have cases_1: "⋀y y'. r y y' ⟹ P y y'"
    using bij_betw_imp_surj_on bij_is_inj f_the_inv_into_f by fastforce
  from P have cases_2: 
    "⋀x y z. r⇧+⇧+ x y ⟹ P x y ⟹ r⇧+⇧+ y z ⟹ P y z ⟹ P x z"
    by auto
  from major cases_1 cases_2 have inv_conc: "P x x'"
    by (rule tranclp_trans_induct) 
  with P as_f y y' show ?thesis by (simp add: bij_is_inj the_inv_f_f)
qed

end

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

• Леммы, представленные в этом ответе, просто демонстрируют, что биективность f является достаточным условием для сохранениясвойств замыкания.
• В леммах, изложенных в вашем вопросе, есть излишняя предпосылка.В частности, можно показать, что (⋀x y. x ≠ y ⟹ f x ≠ f y) ⟺ (⋀x y. f x = f y ⟹ x = y).Конечно, любая из этих предпосылок может использоваться для указания, что f является инъективной функцией.Однако, может быть лучше использовать сокращение inj (HOL/Fun.thy), чтобы указать, что f является инъективной функцией.
• Лемма tranclp_fun_preserve в вашем вопросе содержит контрпример, который можно найти, например, с помощью nitpick.В частности, контрпример демонстрирует, что если f не является сюръективным, то он может не сохранить свойства замыкания.

---

Ответ на обновление

Спасибо за предоставленную дополнительную информацию.Пожалуйста, найдите доказательство лемм tranclp_fun_preserve и tranclp_fun_preserve2 (как указано в вашем обновлении) ниже:

theory so_wkfppc_2
imports 
  Complex_Main
  "HOL-Library.FuncSet"

begin

(*** general theory of functions that preserve properties of closure ***)

definition rel_closed_under :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"rel_closed_under R A = 
(∀x x'::'a. R x x' ⟶ (x ∈ A ∧ x' ∈ A) ∨ (x ∈ -A ∧ x' ∈ -A))"

lemma rel_tcl_closed_under:
  fixes R :: "'a ⇒ 'a ⇒ bool"
    and A :: "'a set"
  assumes as_ra: "rel_closed_under R A"
  shows "rel_closed_under R⇧+⇧+ A"
proof -
  define P where P: 
    "P = (λ x x' :: 'a. (x ∈ A ∧ x' ∈ A) ∨ (x ∈ -A ∧ x' ∈ -A))"
  {
    fix x x' :: 'a  
    assume as_major: "R⇧+⇧+ x x'"
    from as_ra P have cases_1: 
      "⋀x y. R x y ⟹ P x y" by (simp add: rel_closed_under_def)
    from P have "⋀x y z. R⇧+⇧+ x y ⟹ P x y ⟹ R⇧+⇧+ y z ⟹ P y z ⟹ P x z"
      by blast
    with as_major cases_1 have "P x x'" by (rule tranclp_trans_induct)    
  }
  then have "⋀x x'. R⇧+⇧+ x x' ⟹ P x x'" by blast
  with P rel_closed_under_def show ?thesis by blast 
qed

lemma tranclp_fun_preserve_gen_1:
  fixes f:: "'a ⇒ 'b"
    and R :: "'b ⇒ 'b ⇒ bool"
    and B :: "'b set"
    and x x'::'a
  assumes as_f: "bij_betw f UNIV B"
    and as_R: "rel_closed_under R B"
    and prem: "R⇧+⇧+ (f x) (f x')"
  shows "(λ x x'. R (f x) (f x'))⇧+⇧+ x x'"
proof -
  define g where g: "g = the_inv_into UNIV f"
  define gr where gr: "gr = restrict g (range f)"
  define P where P: 
    "P = 
    (λ y y'. y ∈ B ⟶ y' ∈ B ⟶ (λ x x'. R (f x) (f x'))⇧+⇧+ (gr y) (gr y'))" 
  define y where y: "y = f x" 
  with as_f have y_in_B: "y ∈ B" using bij_betw_imp_surj_on by blast
  define y' where y': "y' = f x'"
  with as_f have y'_in_B: "y' ∈ B" using bij_betw_imp_surj_on by blast   
  from prem y y' have major: "R⇧+⇧+ y y'" by blast
  from P as_f as_R g y_in_B y'_in_B have cases_1: "⋀y y'. R y y' ⟹ P y y'"
    by (metis (no_types, lifting) bij_betw_imp_inj_on bij_betw_imp_surj_on 
        f_the_inv_into_f gr restrict_apply' tranclp.r_into_trancl)
  from P have cases_2: 
    "⋀x y z. R⇧+⇧+ x y ⟹ P x y ⟹ R⇧+⇧+ y z ⟹ P y z ⟹ P x z"
    by (smt ComplD as_R rel_closed_under_def rel_tcl_closed_under tranclp_trans)
  from major cases_1 cases_2 have inv_conc: "P y y'" 
    by (rule tranclp_trans_induct)
  with P as_f y y' g gr y'_in_B y_in_B show ?thesis 
    by (metis (no_types, lifting) bij_betw_imp_inj_on bij_betw_imp_surj_on 
        restrict_apply' the_inv_f_f)   
qed

lemma tranclp_fun_preserve_gen_2:
  fixes f:: "'a ⇒ 'b"
    and R :: "'b ⇒ 'b ⇒ bool"
    and B :: "'b set"
    and x x'::'a
  assumes as_f: "bij_betw f UNIV B"
    and as_R: "rel_closed_under R B"
    and prem: "(λ x x'. R (f x) (f x'))⇧+⇧+ x x'"
  shows "R⇧+⇧+ (f x) (f x')"
proof -
  define P where P: "P = (λ x x'. (λ y y'. R y y')⇧+⇧+ (f x) (f x'))" 
  define r where r: "r = (λ x x'. R (f x) (f x'))"
  define y where y: "y = f x"
  define y' where y': "y' = f x'"
  from prem r y y' have major: "r⇧+⇧+ x x'" by blast
  from P as_f r have cases_1: "⋀y y'. r y y' ⟹ P y y'"
    using bij_betw_imp_surj_on bij_is_inj f_the_inv_into_f by fastforce
  from P have cases_2: 
    "⋀x y z. r⇧+⇧+ x y ⟹ P x y ⟹ r⇧+⇧+ y z ⟹ P y z ⟹ P x z"
    by auto
  from major cases_1 cases_2 have inv_conc: "P x x'" 
    by (rule tranclp_trans_induct) 
  with P as_f y y' show ?thesis by (simp add: bij_is_inj the_inv_f_f)
qed


(*** errorable ***)

notation
  bot ("⊥")

typedef 'a errorable ("_⇩⊥" [21] 21) = "UNIV :: 'a option set" ..

definition errorable :: "'a ⇒ 'a errorable" ("_⇩⊥" [1000] 1000) where
  "errorable x = Abs_errorable (Some x)"

instantiation errorable :: (type) bot
begin
definition "⊥ ≡ Abs_errorable None"
instance ..
end

free_constructors case_errorable for
  errorable
| "⊥ :: 'a errorable"
  apply (metis Rep_errorable_inverse bot_errorable_def errorable_def not_Some_eq)
  apply (metis Abs_errorable_inverse UNIV_I errorable_def option.inject)
  by (simp add: Abs_errorable_inject bot_errorable_def errorable_def)

(*** nullable ***)

class opt =
  fixes null :: "'a" ("ε")

typedef 'a nullable ("_⇩□" [21] 21) = "UNIV :: 'a option set" ..

definition nullable :: "'a ⇒ 'a nullable" ("_⇩□" [1000] 1000) where
  "nullable x = Abs_nullable (Some x)"

instantiation nullable :: (type) opt
begin
definition "ε ≡ Abs_nullable None"
instance ..
end

free_constructors case_nullable for
  nullable
| "ε :: 'a nullable"
  apply (metis Rep_nullable_inverse null_nullable_def nullable_def option.collapse)
  apply (simp add: Abs_nullable_inject nullable_def)
  by (metis Abs_nullable_inverse UNIV_I null_nullable_def nullable_def option.distinct(1))

datatype any = BoolVal "bool⇩⊥" | NatVal "nat⇩⊥" | RealVal "real⇩⊥" | InvalidAny unit

datatype oany = OBoolVal "bool⇩⊥⇩□" | ONatVal "nat⇩⊥⇩□" | ORealVal "real⇩⊥⇩□" | OInvalidAny "unit⇩□"

inductive any_oany :: "any ⇒ oany ⇒ bool" where
  "any_oany (BoolVal x) (OBoolVal x⇩□)"
| "any_oany (NatVal x) (ONatVal x⇩□)"
| "any_oany (RealVal x) (ORealVal x⇩□)"
| "any_oany (InvalidAny x) (OInvalidAny x⇩□)"

fun any_to_oany :: "any ⇒ oany" where
  "any_to_oany (BoolVal x) = (OBoolVal x⇩□)"
| "any_to_oany (NatVal x) = (ONatVal x⇩□)"
| "any_to_oany (RealVal x) = (ORealVal x⇩□)"
| "any_to_oany (InvalidAny x) = (OInvalidAny x⇩□)"

lemma any_oany_eq_fun:
  "any_oany x y ⟷ any_to_oany x = y"
  by (cases x; cases y; auto simp: any_oany.simps)

inductive cast_any :: "any ⇒ any ⇒ bool" where
  "cast_any (BoolVal ⊥) (InvalidAny ())"
| "cast_any (NatVal ⊥) (RealVal ⊥)"
| "cast_any (NatVal x⇩⊥) (RealVal (real x)⇩⊥)"
| "cast_any (RealVal ⊥) (InvalidAny ())"

inductive cast_oany :: "oany ⇒ oany ⇒ bool" where
  "cast_any x y ⟹ any_oany x ox ⟹ any_oany y oy ⟹
   cast_oany ox oy"
| "cast_oany (OBoolVal ε) (OInvalidAny ε)"
| "cast_oany (ONatVal ε) (ORealVal ε)"
| "cast_oany (ORealVal ε) (OInvalidAny ε)"

lemma cast_any_implies_cast_oany:
  "cast_any x y ⟹ cast_oany (any_to_oany x) (any_to_oany y)"
  by (simp add: any_oany_eq_fun cast_oany.intros(1))

lemma cast_oany_implies_cast_any:
  "cast_oany (any_to_oany x) (any_to_oany y) ⟹ cast_any x y"
  by (cases x; cases y; simp add: any_oany.simps cast_oany.simps)

lemma cast_oany_closed_under_range: 
  "rel_closed_under cast_oany (range any_to_oany)"
proof -
  define B where B: "B = range any_to_oany"
  define P where P: 
    "P = (λ x x'. (x ∈ B ∧ x' ∈ B) ∨ (x ∈ -B ∧ x' ∈ -B))"
  {
    fix x x'
    assume as_c: "cast_oany x x'"
    have obv_p: "(OBoolVal ε) ∉ range any_to_oany" 
    proof - 
      have "⋀x. any_to_oany x ≠ (OBoolVal ε)"
        using any_oany.simps any_oany_eq_fun by auto
      then show ?thesis by fastforce
    qed
    have oia_p: "(OInvalidAny ε) ∉ range any_to_oany"
    proof -
      have "⋀x. any_to_oany x ≠ (OInvalidAny ε)"
        using any_oany.simps any_oany_eq_fun by auto
      then show ?thesis by fastforce
    qed
    have onv_p: "(ONatVal ε) ∉ range any_to_oany"
    proof -
      have "⋀x. any_to_oany x ≠ (ONatVal ε)"
        using any_oany.simps any_oany_eq_fun by auto
      then show ?thesis by fastforce
    qed
    have orv_p: "(ORealVal ε) ∉ range any_to_oany"
    proof -
      have "⋀x. any_to_oany x ≠ (ORealVal ε)"
        using any_oany.simps any_oany_eq_fun by auto
      then show ?thesis by fastforce
    qed
    have "cast_oany x x' ⟹ P x x'"
    proof (induction rule: cast_oany.induct)
      case (1 x y ox oy) then show ?case using B P any_oany_eq_fun by auto
    next
      case 2 then show ?case
      proof - 
        from B obv_p have obv: "(OBoolVal ε) ∈ -B" by simp       
        from B oia_p have oia: "(OInvalidAny ε) ∈ -B" by simp
        from P obv oia show ?thesis by auto     
      qed
    next
      case 3 then show ?case
      proof -
        from onv_p B have onv: "(ONatVal ε) ∈ -B" by simp       
        from orv_p B have orv: "(ORealVal ε) ∈ -B" by simp
        from P onv orv show ?thesis by auto     
      qed
    next
      case 4 then show ?case
      proof -
        from orv_p B have orv: "(ORealVal ε) ∈ -B" by simp       
        from oia_p B have oia: "(OInvalidAny ε) ∈ -B" by simp
        from P orv oia show ?thesis by auto           
      qed
    qed
  }  
  with B P show ?thesis by (simp add: rel_closed_under_def)
qed

lemma inj_any_to_oany: "inj any_to_oany"
proof
  fix x x' :: any
  assume as_1: "x ∈ UNIV" 
  assume as_2: "x' ∈ UNIV" 
  assume as_3: "any_to_oany x = any_to_oany x'"
  show "x = x'"
  proof (case_tac x)
    show c_1: "⋀x1::bool⇩⊥. x = BoolVal x1 ⟹ x = x'"
      by (metis any.exhaust any_to_oany.simps(1) 
          any_to_oany.simps(2) any_to_oany.simps(3) any_to_oany.simps(4) 
          as_3 nullable.inject oany.distinct(2) oany.distinct(4) 
          oany.inject(1) oany.simps(10))
    show c_2: "⋀x2::nat⇩⊥. x = NatVal x2 ⟹ x = x'"
      by (metis any_to_oany.cases any_to_oany.simps(1) 
          any_to_oany.simps(2) any_to_oany.simps(3) any_to_oany.simps(4) 
          as_3 nullable.inject oany.distinct(1) oany.distinct(9) 
          oany.inject(2) oany.simps(12))
    show c_3: "⋀x3::real⇩⊥. x = RealVal x3 ⟹ x = x'"
      by (metis any.distinct(12) any.distinct(4) any.distinct(8) 
          any_oany.cases any_oany.intros(3) any_to_oany.elims 
          any_to_oany.simps(1) any_to_oany.simps(3) as_3 nullable.inject 
          oany.distinct(12) oany.distinct(3) oany.inject(3) oany.simps(12))
    show c_4: "⋀x4::unit. x = InvalidAny x4 ⟹ x = x'"
      by (metis any.distinct(5) any_to_oany.cases any_to_oany.simps(1) 
          any_to_oany.simps(2) any_to_oany.simps(3) any_to_oany.simps(4) as_3  
          nullable.inject oany.distinct(5) oany.inject(4) oany.simps(14) 
          oany.simps(16))
  qed
qed

lemma bij_any_to_oany: "bij_betw any_to_oany UNIV (range any_to_oany)"
  using inj_any_to_oany by (simp add: bij_betw_def)

lemma tranclp_fun_preserve:
  fixes x y :: any
  assumes "cast_oany⇧+⇧+ (any_to_oany x) (any_to_oany y)" 
  shows "(λx y. cast_oany (any_to_oany x) (any_to_oany y))⇧+⇧+ x y"
  using bij_any_to_oany cast_oany_closed_under_range assms 
    by (rule tranclp_fun_preserve_gen_1)

lemma tranclp_fun_preserve2:
  fixes x y :: any
  assumes as: "(λx y. cast_oany (any_to_oany x) (any_to_oany y))⇧+⇧+ x y" 
  shows "cast_oany⇧+⇧+ (any_to_oany x) (any_to_oany y)"
  using bij_any_to_oany cast_oany_closed_under_range assms 
    by (rule tranclp_fun_preserve_gen_2)

end

Примечания:

• Предикат rel_closed_under определяет, является лиили нет отношение закрыто под данным множеством.Лемма rel_tcl_closed_under показывает, что если отношение замкнуто для данного множества, то транзитивное замыкание этого отношения также замкнуто для этого множества.Леммы tranclp_fun_preserve_1 и tranclp_fun_preserve_2 из ответа на исходный вопрос были изменены и переименованы в tranclp_fun_preserve_gen_1 и tranclp_fun_preserve_gen_2 соответственно.Леммы tranclp_fun_preserve_gen_1 и tranclp_fun_preserve_gen_2 показывают, что f сохраняет свойства замыкания, если f является биекцией между его областью и множеством B и отношение закрыто под множеством B.Лемма cast_oany_closed_under_range показывает, что cast_oany закрывается в диапазоне any_to_oany.Лемма bij_any_to_oany показывает, что any_to_oany является биективным между своим доменом и диапазоном.Доказательства лемм tranclp_fun_preserve и tranclp_fun_preserve2 следуют непосредственно из tranclp_fun_preserve_gen_1 и tranclp_fun_preserve_gen_2.
• Как и ранее, я не делал никаких попыток обеспечить, чтобы доказательства были написаны наилучшим образом.
• Доказательства были написаны в Isabelle2018 и могут быть несовместимы с предыдущими версиями Isabelle.
• В будущем, пожалуйста, предоставьте минимальный пример вместо вашего рабочего кода.