如何通过限制或扩展另一个功能来定义一个功能？

Question

我的理论中有 3 种布尔类型：

bool = {对，错}
bool3 = {真,假,⊥}
bool4 = {真,假,⊥,ε}

bool3 基于 bool:

typedef bool3 = "UNIV :: bool option set" ..

definition bool3 :: "bool ⇒ bool3" where
  "bool3 b = Abs_bool3 (Some b)"

notation bot ("⊥")

instantiation bool3 :: bot
begin
definition "⊥ ≡ Abs_bool3 None"
instance ..
end

free_constructors case_bool3 for
  bool3
| "⊥ :: bool3"
  apply (metis Rep_bool3_inverse bot_bool3_def bool3_def not_Some_eq)
  apply (smt Abs_bool3_inverse bool3_def iso_tuple_UNIV_I option.inject)
  by (simp add: Abs_bool3_inject bot_bool3_def bool3_def)

bool4 基于 bool3:

typedef bool4 = "UNIV :: bool3 option set" ..

definition bool4 :: "bool ⇒ bool4" where
  "bool4 b = Abs_bool4 (Some (bool3 b))"

class opt = bot +
  fixes void :: "'a" ("ε")

instantiation bool4 :: opt
begin
definition "⊥ = Abs_bool4 (Some ⊥)"
definition "ε = Abs_bool4 None"
instance ..
end

free_constructors case_bool4 for
  bool4
| "⊥ :: bool4"
| "ε :: bool4"
  apply (metis Rep_bool4_inverse bool3.exhaust bool4_def bot_bool4_def not_Some_eq void_bool4_def)
  apply (metis Abs_bool4_inverse UNIV_I bool3.inject bool4_def option.sel)
  apply (metis Abs_bool4_inverse UNIV_I bot_bool4_def bool3.distinct(1) bool4_def option.sel)
  apply (metis Abs_bool4_inverse UNIV_I bool4_def option.distinct(1) void_bool4_def)
  by (metis Abs_bool4_inverse UNIV_I bot_bool4_def option.distinct(1) void_bool4_def)

下面是一些类型转换：

fun bool3_to_bool4 :: "bool3 ⇒ bool4" where
  "bool3_to_bool4 ⊥ = ⊥"
| "bool3_to_bool4 (bool3 b) = bool4 b"

declare [[coercion_enabled]]
declare [[coercion "bool3 :: bool ⇒ bool3"]]
declare [[coercion "bool4 :: bool ⇒ bool4"]]
declare [[coercion "bool3_to_bool4 :: bool3 ⇒ bool4"]]

我为 bool3 和 bool4 定义了逻辑连词:

fun bool3_and :: "bool3 ⇒ bool3 ⇒ bool3" where
  "bool3_and (bool3 a) (bool3 b) = bool3 (a ∧ b)"
| "bool3_and (bool3 False) _ = bool3 False"
| "bool3_and _ (bool3 False) = bool3 False"
| "bool3_and ⊥ _ = ⊥"
| "bool3_and _ ⊥ = ⊥"

fun bool4_and :: "bool4 ⇒ bool4 ⇒ bool4" where
  "bool4_and (bool4 a) (bool4 b) = bool4 (a ∧ b)"
| "bool4_and (bool4 False) _ = bool4 False"
| "bool4_and _ (bool4 False) = bool4 False"
| "bool4_and ⊥ _ = ⊥"
| "bool4_and _ ⊥ = ⊥"
| "bool4_and ε _ = ε"
| "bool4_and _ ε = ε"

并证明它们是等价的：

lemma bool3_and_eq_bool4_and:
  "(bool3_and a b = c) =
   (bool4_and a b = c)"
  apply (cases a; cases b; cases c; simp)
  apply (metis (full_types) bool3.distinct(1) bool3_and.simps(2) bool3_and.simps(6) bool4.distinct(1) bool4_and.simps(2) bool4_and.simps(9))
  apply (metis (full_types) bool3.distinct(1) bool3_and.simps(2) bool3_and.simps(6) bool4.distinct(1) bool4_and.simps(2) bool4_and.simps(9))
  apply (metis (full_types) bool3.distinct(1) bool3_and.simps(3) bool3_and.simps(4) bool4.distinct(1) bool4_and.simps(4) bool4_and.simps(6))
  apply (metis (full_types) bool3.distinct(1) bool3_and.simps(3) bool3_and.simps(4) bool4.distinct(1) bool4_and.simps(4) bool4_and.simps(6))
  done

问题是 bool3_and 和 bool4_and 非常相似。在我的理论中有很多这样的功能。而且我不想重复相同的逻辑两次。我也不想证明类似功能的等价性。是否可以通过bool4_and的限制来定义bool3_and？或者通过扩展 bool3_and?

来定义 bool4_and

Answer 1

答案很简单。我应该定义 bool4 构造函数如下：

definition bool4 :: "bool3 ⇒ bool4" where
  "bool4 b = Abs_bool4 (Some b)"

free_constructors case_bool4 for
  bool4
| "ε :: bool4"
  apply (metis Abs_bool4_cases bool4_def not_None_eq void_bool4_def)
  apply (metis Abs_bool4_inverse UNIV_I bool4_def option.inject)
  by (simp add: Abs_bool4_inject bool4_def void_bool4_def)

declare [[coercion "bool4 :: bool3 ⇒ bool4"]]

bool3_and感谢强制转换可以简化为：

fun bool3_and :: "bool3 ⇒ bool3 ⇒ bool3" where
  "bool3_and a b = (a ∧ b)"
| "bool3_and False _ = False"
| "bool3_and _ False = False"
| "bool3_and ⊥ _ = ⊥"
| "bool3_and _ ⊥ = ⊥"

这里是 bool4_and 扩展 bool3_and:

fun bool4_and :: "bool4 ⇒ bool4 ⇒ bool4" where
  "bool4_and a b = bool3_and a b"
| "bool4_and ε _ = ε"
| "bool4_and _ ε = ε"

bool3_and 和 bool4_and 在 bool3 域上的等价性可以通过简化来证明：

lemma bool3_and_eq_bool4_and:
  "(bool3_and a b = c) =
   (bool4_and a b = c)"
  by simp

如何通过限制或扩展另一个功能来定义一个功能？

How to define a function by restriction or extension of another function?

isabelle