时间戳

首页 > 解决方案 > 什么样的函数保留了闭包的性质？

isabelle - 什么样的函数保留了闭包的性质？

问题描述

我试图证明以下引理：

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_oanyon的等价性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. 空值 ( OBoolVal ε, ONatVal ε, ORealVal ε, OInvalidAny ε)
  2. 所有其他值。

该关系cast_oany将第一部分内的值和第二部分内的值分别关联起来。不同部分的值之间没有关系。该函数any_to_oany仅将值映射到第二部分。我不知道这个属性的正确名称是什么：子集 1 和 2 相对于关系是“封闭的” cast_oany。并且该函数any_to_oany仅将值映射到一个子集，并且在该子集上是双射的。

标签： isabelletheorem-proving

解决方案

下面给出的答案是对原始答案的实质性修改。原始答案可通过修订历史获得。

实际上，在最初的修订过程中，问题归结为仅仅证明两个集合之间的双射函数保留了闭包的属性。下面的解决方案提供了没有特定于应用程序上下文的相关证明（答案还结合了线程作者对原始答案所做的一些修改）：

section ‹Extension of the theory @{text Transitive_Closure}›
theory Transitive_Closure_Ext
  imports 
    Complex_Main
    "HOL-Library.FuncSet"
begin

lemma trancl_subset_trancl: "r ⊆ s⇧+ ⟹ r⇧+ ⊆ s⇧+"
  by (metis subsetI trancl_id trancl_mono trans_trancl)

lemma mono_tranclp[mono]: "(⋀a b. R a b ⟶ S a b) ⟹ R⇧+⇧+ a b ⟶ S⇧+⇧+ a b"
  apply(rule) using trancl_mono[to_pred] by blast

lemma tranclp_mono: "R ≤ S ⟹ R⇧+⇧+ ≤ S⇧+⇧+"
  by (metis (full_types) mono_tranclp predicate2D predicate2I)

lemma preserve_tranclp:
  assumes "⋀x y. R x y ⟹ S (f x) (f y)"
  shows "R⇧+⇧+ x y ⟹ S⇧+⇧+ (f x) (f y)"
proof -
  assume Rpp: "R⇧+⇧+ x y"
  define P where P: "P = (λx y. S⇧+⇧+ (f x) (f y))" 
  define r where r: "r = (λx y. S (f x) (f y))"
  have major: "r⇧+⇧+ x y" 
    by (insert assms Rpp r; erule tranclp_trans_induct; auto)
  have cases_1: "r x y ⟹ P x y" for x y unfolding r P by simp
  have cases_2: "r⇧+⇧+ x y ⟹ P x y ⟹ r⇧+⇧+ y z ⟹ P y z ⟹ P x z" for x y z
    unfolding P by simp
  from major cases_1 cases_2 have "P x y" by (rule tranclp_trans_induct)
  thus "S⇧+⇧+ (f x) (f y)" unfolding P . 
qed

lemma preserve_trancl:
  assumes "map_prod f f ` r ⊆ s"
  shows "map_prod f f ` r⇧+ ⊆ s⇧+"
proof -
  from assms have "(x, y) ∈ r ⟶ (f x, f y) ∈ s" for x y by auto
  then have "(x, y) ∈ r⇧+ ⟶ (f x, f y) ∈ s⇧+" for x y
  by (metis preserve_tranclp[to_set])
  thus "map_prod f f ` r⇧+ ⊆ s⇧+" by clarsimp
qed

lemma preserve_tranclp_inv:
  assumes bij_f: "bij_betw f a b"
    and R: "⋀x y. R x y ⟹ (x, y) ∈ a × a"
    and S: "⋀x y. S x y ⟹ (x, y) ∈ b × b"
    and S_R: "⋀x y. (x, y) ∈ a × a ⟹ S (f x) (f y) ⟹ R x y"
  shows "(x, y) ∈ a × a ⟹ S⇧+⇧+ (f x) (f y) ⟹ R⇧+⇧+ x y"
proof -
  assume x_y_in_aa: "(x, y) ∈ a × a"
  assume Spp: "S⇧+⇧+ (f x) (f y)"
  define g where g: "g = the_inv_into a f"
  define gr where gr: "gr = restrict g b"
  define P where P: "P = (λx y. (x, y) ∈ b × b ⟶ R⇧+⇧+ (gr x) (gr y))"
  from Spp have fx_fy_in_bb: "(f x, f y) ∈ b × b"  
    using S by (metis converse_tranclpE mem_Sigma_iff tranclp.cases)
  have cases_1: "S x y ⟹ P x y" for x y unfolding P
  proof(rule impI)
    assume Sxy: "S x y" and xy_in_bb: "(x, y) ∈ b × b"
    with bij_f have gr_in_aa: "(gr x, gr y) ∈ a × a" 
      unfolding gr g apply(auto)
      using bij_betwE bij_betw_the_inv_into by blast+
    from bij_f xy_in_bb have "x = f (gr x)" and "y = f (gr y)"
      unfolding gr g using f_the_inv_into_f_bij_betw by fastforce+
    with Sxy have S_fgrx_fgry: "S (f (gr x)) (f (gr y))" by simp
    from gr_in_aa S_fgrx_fgry have "R (gr x) (gr y)" by (rule S_R)
    thus "R⇧+⇧+ (gr x) (gr y)" ..
  qed
  with bij_f S have 
    "S⇧+⇧+ x y ⟹ S⇧+⇧+ y z ⟹ x ∈ b ⟹ z ∈ b ⟹ y ∈ b" for x y z
    by (auto dest: SigmaD1 tranclpD)
  with P have cases_2: 
    "S⇧+⇧+ x y ⟹ P x y ⟹ S⇧+⇧+ y z ⟹ P y z ⟹ P x z" for x y z
    by auto
  from Spp cases_1 cases_2 have "P (f x) (f y)" by (rule tranclp_trans_induct)
  with bij_f fx_fy_in_bb x_y_in_aa show "R⇧+⇧+ x y" 
    unfolding P gr g restrict_def bij_betw_def by (simp add: the_inv_into_f_f)
qed

lemma preserve_trancl_inv:
  assumes bij_f: "bij_betw f a b"
    and r_in_aa: "r ⊆ a × a"
    and s_in_bb: "s ⊆ b × b"
    and s_r: "(map_prod f f -` s) ∩ (a × a) ⊆ r ∩ (a × a)"
  shows "(map_prod f f -` s⇧+) ∩ (a × a) ⊆ r⇧+ ∩ (a × a)"
proof -
  from r_in_aa have r_in_aa_set: 
    "(x, y) ∈ r ⟹ (x, y) ∈ a × a" for x y by auto
  from s_in_bb have s_in_bb_set: "⋀x y. (x, y) ∈ s ⟹ (x, y) ∈ b × b" by auto
  from s_r have s_r_set: 
    "(x, y) ∈ a × a ⟹ (f x, f y) ∈ s ⟹ (x, y) ∈ r" for x y
    unfolding map_prod_def by auto
  from bij_f r_in_aa_set s_in_bb_set s_r_set have 
    "(x, y) ∈ a × a ⟹ (f x, f y) ∈ s⇧+ ⟹ (x, y) ∈ r⇧+" for x y
    by (rule preserve_tranclp_inv[to_set])
  thus ?thesis unfolding map_prod_def by clarsimp
qed

lemma preserve_rtranclp:
  assumes "⋀x y. R x y ⟹ S (f x) (f y)"
  shows "R⇧*⇧* x y ⟹ S⇧*⇧* (f x) (f y)"
  by (insert assms, metis Nitpick.rtranclp_unfold preserve_tranclp)

lemma preserve_rtrancl:
  assumes "map_prod f f ` r ⊆ s"
  shows "map_prod f f ` r⇧* ⊆ s⇧*"
proof -
  from assms have "(x, y) ∈ r ⟶ (f x, f y) ∈ s" for x y by auto
  then have "(x, y) ∈ r⇧* ⟶ (f x, f y) ∈ s⇧*" for x y 
    by (metis preserve_rtranclp[to_set])
  thus "map_prod f f ` r⇧* ⊆ s⇧*" by clarsimp
qed

lemma preserve_rtranclp_inv:
  assumes bij_f: "bij_betw f a b"
    and "⋀x y. R x y ⟹ (x, y) ∈ a × a"
    and "⋀x y. S x y ⟹ (x, y) ∈ b × b"
    and "⋀x y. (x, y) ∈ a × a ⟹ S (f x) (f y) ⟹ R x y"
  shows "(x, y) ∈ a × a ⟹ S⇧*⇧* (f x) (f y) ⟹ R⇧*⇧* x y"
proof -
  assume xy_in_aa: "(x, y) ∈ a × a" and Spp: "S⇧*⇧* (f x) (f y)" 
  show "R⇧*⇧* x y"
  proof(cases "f x ≠ f y")
    case True show ?thesis
    proof -
      from True Spp obtain z where "S⇧*⇧* (f x) z" and "S z (f y)" 
        by (auto elim: rtranclp.cases)
      then have "S⇧+⇧+ (f x) (f y)" by (rule rtranclp_into_tranclp1)
      with assms xy_in_aa have "R⇧+⇧+ x y" by (rule preserve_tranclp_inv)
      thus ?thesis by simp
    qed
  next
    case False show ?thesis
    proof -
      from False xy_in_aa bij_f have "x = y" 
        unfolding bij_betw_def by (auto dest: SigmaD1 SigmaD2 inj_onD)
      thus "R⇧*⇧* x y" by simp 
    qed
  qed
qed

lemma preserve_rtrancl_inv:
  assumes bij_f: "bij_betw f a b"
    and r_in_aa: "r ⊆ a × a"
    and s_in_bb: "s ⊆ b × b"
    and as_s_r: "(map_prod f f -` s) ∩ (a × a) ⊆ r ∩ (a × a)"
  shows "(map_prod f f -` s⇧*) ∩ (a × a) ⊆ r⇧* ∩ (a × a)"
proof -
  from r_in_aa have r_in_aa_set: 
    "(x, y) ∈ r ⟹ (x, y) ∈ a × a" for x y by auto
  from s_in_bb have s_in_bb_set: 
    "(x, y) ∈ s ⟹ (x, y) ∈ b × b" for x y by auto
  from as_s_r have s_r: 
    "(x, y) ∈ a × a ⟹ (f x, f y) ∈ s ⟹ (x, y) ∈ r" for x y 
    unfolding map_prod_def by auto
  from bij_f r_in_aa_set s_in_bb_set s_r have 
    "(x, y) ∈ a × a ⟹ (f x, f y) ∈ s⇧* ⟹ (x, y) ∈ r⇧*" for x y
    by (rule preserve_rtranclp_inv[to_set])
  thus ?thesis unfolding map_prod_def by clarsimp
qed

end

推荐阅读