A collection of Isabelle/HOL proofs that I cant throw away but are almost certainly useless

rtrancl.thy

lemma foobafafgw:
  assumes "∀ x. p x x"
      and "⋀ x y. (x, y) ∈ r ⟹ p x y"
      and "⋀ x y z. p x y ⟹ p y z ⟹ p x z"
    shows "(a, b) ∈ r⇧* ⟹ p a b"
proof (induct rule: rtrancl_induct)
  case base
  then show ?case
    using assms(1) by blast
next
  case (step y z)
  from `(y, z) ∈ r` have "p y z" 
    using assms(2) by blast
  then have "p a z"
    using `p a y` assms(3) by blast 
  then show ?case .
qed

lemma pair_predicate_over_rtranclp:
  assumes refl: "⋀ x. p x x"
      and relation_to_predicate: "⋀ x y. r x y ⟹ p x y"
      and trans: "⋀ x y z. p x y ⟹ p y z ⟹ p x z"
    shows "r⇧*⇧* a b ⟹ p a b"
proof (induct rule: rtranclp_induct)
  case base
  then show ?case
    using refl by blast
next
  case (step y z)
  from `r y z` have "p y z" 
    using relation_to_predicate by blast
  then have "p a z"
    using `p a y` trans by blast 
  then show ?case .
qed

lemma rtranclp_transfer: "∀ x y. r x y ⟶ t x y ⟹ r⇧*⇧* x y ⟶ t⇧*⇧* x y"
  by (metis predicate2D predicate2I rtranclp_mono)
  
lemma rtranclp_transfer2:
  assumes "⋀x. g x = h x"
      and "⋀ x y. r x y ⟹ r (g x) (h y)"
    shows "r⇧*⇧* x y ⟹ r⇧*⇧* (g x) (h y)"
proof (induct rule: rtranclp.induct)
  case (rtrancl_refl a)
  then show ?case
    by (simp add: assms(1))
next
  case (rtrancl_into_rtrancl a b c)
  then show ?case
    using assms(1) assms(2) by force
qed

lemma rtranclp_transfer3:
  assumes refl: "⋀x. g x x = h x x"
      and extd: "⋀ x y z. r⇧*⇧* (g x y) (h x y) ⟹ r y z ⟹ r⇧*⇧* (g x z) (h x z)"  
  shows "r⇧*⇧* x y ⟹ r⇧*⇧* (g x y) (h x y)"
proof (induct rule: rtranclp.induct)
  case (rtrancl_refl a)
  then show ?case
    by (simp add: assms(1))
next
  case (rtrancl_into_rtrancl a b c)
  then show ?case
    using extd by blast
qed