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

There are 3 boolean types in my theory:

bool = {True,False}
bool3 = {True,False,⊥}
bool4 = {True,False,⊥,ε}

bool3 is based on 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 is based on 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)

Here is some type conversions:

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

I defined logical conjunctions for bool3 and 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 _ ε = ε"

And proved that they are equivalent:

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

The problem is that bool3_and and bool4_and are very similar. There are a lot of such functions in my theory. And I don't want to duplicate the same logic twice. Also I don't want to prove equivalence of similar functions. Is it possible to define bool3_and by restriction of bool4_and? Or to define bool4_and by extension of bool3_and?

Solution

The answer is very simple. I should define bool4 constructor as follows:

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 thanks to coercion can be simplified as follows:

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 _ ⊥ = ⊥"

And here is bool4_and extending bool3_and:

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

Equivalence of bool3_and and bool4_and on bool3 domain can be proven by simplification:

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