What kind of functions preserve properties of clos

2019-06-25 09:28发布

站内文章 / 前端开发

39 0

仙女界的扛把子

女 | 书童

私信

可以将文章内容翻译成中文,广告屏蔽插件可能会导致该功能失效(如失效，请关闭广告屏蔽插件后再试):

问题:

I'm trying to prove the following lemmas:

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

However, I'm stuck. Should I choose another set of assumptions for the function f? Could you suggest how to prove the lemmas tranclp_fun_preserve and tranclp_fun_preserve2?

UPDATE

My function is injective with a special property described at the end. I'm afraid that the following example is too long. However, I want to make it a little bit more realistic. Here are two auxiliary types errorable and 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))

Two kinds of values:

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

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

Here is a concrete example of the function f (any_to_oany), it's injective:

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)

Here is a concrete example of the relation 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 ε)"

I proved equivalence of cast_any and 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)

And my final goal is to prove similar lemmas for the transitive closures of these relations:

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)"

I proved the following intermediate lemmas:

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

At last, if I could prove the following lemmas from the original question, then I will able to prove my goal lemmas.

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)"

In this paragraph I provide an important property of the function any_to_oany. The set of oany values consists of two parts:

nulls (OBoolVal ε, ONatVal ε, ORealVal ε, OInvalidAny ε)
all other values.

The relation cast_oany relates the values inside the first part and inside the second part separately. There is no relation between the values from different parts. The function any_to_oany maps values only to the second part. I don't know what is the right name of this property: subsets 1 and 2 are "closed" with respect to the relation cast_oany. And the function any_to_oany maps values only to one subset, and it's bijective on this subset.

回答1:

Response to the original question

This answer provides (mild) sufficient conditions for a function to preserve the properties of closure based on the definition that was inferred from the lemmas tranclp_fun_preserve and tranclp_fun_preserve2 in your question.

In particular, if a function is bijective, then it preserves the properties of closure. The proof in Isabelle is given below. However, please note that it is likely that the proof can be restated in a better way.

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

I believe that several remarks are in order:

The lemmas that are presented in this answer merely demonstrate that bijectivity of f is a sufficient condition for the preservation of the properties of closure.
There is a redundant premise in the lemmas that are stated in your question. In particular, it can be shown that (⋀x y. x ≠ y ⟹ f x ≠ f y) ⟺ (⋀x y. f x = f y ⟹ x = y). Of course, either of these premises can be used to state that f is an injective function. However, it may be better to use the abbreviation inj (HOL/Fun.thy) to indicate that f is an injective function.
The lemma tranclp_fun_preserve in your question has a counterexample that can be found, for example, using nitpick. In particular, the counterexample demonstrates that if f is not surjective, then it may not preserve the properties of closure.

Response to the update

Thank you for providing further details. Please find the proof of the lemmas tranclp_fun_preserve and tranclp_fun_preserve2 (as stated in your update) below:

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

Remarks:

The predicate rel_closed_under identifies whether or not the relation is closed under a given set. Lemma rel_tcl_closed_under shows that if a relation is closed under a given set, then the transitive closure of this relation is also closed under this set. The lemmas tranclp_fun_preserve_1 and tranclp_fun_preserve_2 from the response to the original question were modified and renamed to tranclp_fun_preserve_gen_1 and tranclp_fun_preserve_gen_2, respectively. The lemmas tranclp_fun_preserve_gen_1 and tranclp_fun_preserve_gen_2 show that f preserves the properties of closure if f is a bijection between its domain and a set B and the relation is closed under the set B. Lemma cast_oany_closed_under_range shows that cast_oany is closed under the range of any_to_oany. The lemma bij_any_to_oany shows that any_to_oany is bijective between its domain and range. The proofs of lemmas tranclp_fun_preserve and tranclp_fun_preserve2 follow directly from tranclp_fun_preserve_gen_1 and tranclp_fun_preserve_gen_2.
As previously, I have not made any attempts to ensure that the proofs are written in the best possible manner.
The proofs were written in Isabelle2018 and may not be compatible with the previous versions of Isabelle.
In the future, please provide a minimal example instead of your working code.