Theory Set_Theory

section ‹Set Theory›

theory Set_Theory imports Main begin


subsection ‹CakeML License›

text ‹
CakeML Copyright Notice, License, and Disclaimer.

Copyright 2013-2023 by Anthony Fox, Google LLC, Ramana Kumar, Magnus Myreen,
Michael Norrish, Scott Owens, Yong Kiam Tan, and other contributors listed
at https://cakeml.org

All rights reserved.

CakeML is free software. Redistribution and use in source and binary forms,
with or without modification, are permitted provided that the following
conditions are met:

    * Redistributions of source code must retain the above copyright
      notice, this list of conditions and the following disclaimer.

    * Redistributions in binary form must reproduce the above copyright
      notice, this list of conditions and the following disclaimer in the
      documentation and/or other materials provided with the distribution.

    * The names of the copyright holders and contributors may not be
      used to endorse or promote products derived from this software without
      specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS''
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
›


subsection ‹Set theory specification›

text ‹
  This formal document is the set theory from 
  https://github.com/CakeML/cakeml/blob/master/candle/set-theory/setSpecScript.sml
  ported to Isabelle/HOL and extended.
›

(* Corresponds to CakeML's constant is_set_theory_def *)
locale set_theory =
  fixes mem :: "'s ⇒ 's ⇒ bool" (infix "∈:" 67)
  fixes sub :: "'s ⇒ ('s ⇒ bool) ⇒ 's" (infix "suchthat" 67)
  fixes pow :: "'s ⇒ 's"
  fixes uni :: "'s ⇒ 's" ("⋃:_" [900] 900)
  fixes upair :: "'s ⇒ 's ⇒ 's" (infix "+:" 67)
  assumes extensional: "⋀x y. x = y ⟷ (∀a. a ∈: x ⟷ a ∈: y)"
  assumes mem_sub[simp]: "⋀x P a. a ∈: (x suchthat P) ⟷ a ∈: x ∧ P a"
  assumes mem_pow[simp]: "⋀x a. a ∈: (pow x) ⟷ (∀b. b ∈: a ⟶ b ∈: x)"
  assumes mem_uni[simp]: "⋀x a. a ∈: ⋃:x ⟷ (∃b. a ∈: b ∧ b ∈: x)"
  assumes mem_upair[simp]: "⋀x y a. a ∈: (x +: y) ⟷ a = x ∨ a = y" 
begin

(* Corresponds to CakeML's theorem separation_unique *)
lemma seperation_unique:
  assumes "∀x P a. a ∈: (sub2 x P) ⟷ a ∈: x ∧ P a"
  shows "sub2 = sub"
proof
  fix x
  show "sub2 x = (suchthat) x"
    using assms extensional by auto
qed

(* Corresponds to CakeML's theorem power_unique *)
lemma pow_unique:
  assumes "∀x a. a ∈: (pow2 x) ⟷ (∀b. b ∈: a ⟶ b ∈: x)"
  shows "pow2 = pow"
  using assms extensional by auto

(* Corresponds to CakeML's theorem union_unique *)
lemma uni_unique:
  assumes "∀x a. a ∈: uni2 x ⟷ (∃b. a ∈: b ∧ b ∈: x)"
  shows "uni2 = uni"
  using assms extensional by auto

(* Corresponds to CakeML's theorem upair_unique *)
lemma upair_unique:
  assumes "∀x y a. a ∈: upair2 x y ⟷ a = x ∨ a = y"
  shows "upair2 = upair"
proof 
  fix x 
  show "upair2 x = (+:) x"
    using assms extensional by auto
qed

(* Corresponds to CakeML's Ø *)
definition empt :: 's ("Ø") where
 "Ø = undefined suchthat (λx. False)" 

(* Corresponds to CakeML's theorem mem_empty *)
lemma mem_empty[simp]: "¬x ∈: Ø"
  unfolding empt_def using mem_sub by auto

(* Corresponds to CakeML's constant unit *)
definition unit :: "'s ⇒ 's" where
  "unit x = x +: x"

(* Corresponds to CakeML's theorem mem_unit *)
lemma mem_unit[simp]: "x ∈: (unit y) ⟷ x = y"
  unfolding unit_def using mem_upair by auto

(* Corresponds to CakeML's theorem unit_inj *)
lemma unit_inj: "unit x = unit y ⟷ x = y"
  using extensional unfolding unit_def by auto 

(* Corresponds to CakeML's constant one *)
definition one :: 's where
  "one = unit Ø"

(* Corresponds to CakeML's theorem mem_one *)
lemma mem_one[simp]: "x ∈: one ⟷ x = Ø"
  unfolding one_def by auto

(* Corresponds to CakeML's constant two *)
definition two :: 's where
  "two = Ø +: one"

(* Corresponds to CakeML's theorem mem_two *)
lemma mem_two[simp]: "∀x. x ∈: two ⟷ x = Ø ∨ x = one"
  unfolding two_def by auto 

(* Corresponds to CakeML's constant pair *)
definition pair :: "'s ⇒ 's ⇒ 's" (infix ",:" 50) where
  "(x,:y) = (unit x) +: (x +: y)"

(* Corresponds to CakeML's theorem upair_inj *)
lemma upair_inj:
  "a +: b = c +: d ⟷ a = c ∧ b = d ∨ a = d ∧ b = c"
  using extensional by auto

(* Corresponds to CakeML's theorem unit_eq_upair *)
lemma unit_eq_upair:
  "unit x = y +: z ⟷ x = y ∧ y = z"
  using extensional mem_unit mem_upair by metis

(* Corresponds to CakeML's theorem pair_inj *)
lemma pair_inj:
  "(a,:b) = (c,:d) ⟷ a = c ∧ b = d"
  using pair_def upair_inj unit_inj unit_eq_upair by metis

(* Corresponds to CakeML's constant binary_uni *)
definition binary_uni (infix "∪:" 67) where
  "x ∪: y = ⋃: (x +: y)"

(* Corresponds to CakeML's theorem mem_binary_uni *)
lemma mem_binary_uni[simp]:
  "a ∈: (x ∪: y) ⟷ a ∈: x ∨ a ∈: y"
  unfolding binary_uni_def by auto

(* Corresponds to CakeML's constant product *)
definition product :: "'s ⇒ 's ⇒ 's" (infix "×:" 67) where
  "x ×: y = (pow (pow (x ∪: y)) suchthat (λa. ∃b c. b ∈: x ∧ c ∈: y ∧ a = (b,:c)))"

(* Corresponds to CakeML's theorem mem_product *)
lemma mem_product[simp]:
  "a ∈: (x ×: y) ⟷ (∃b c. a = (b,:c) ∧ b ∈: x ∧ c ∈: y)"
  using product_def pair_def by auto

(* Corresponds to CakeML's constant product *)
definition relspace where
  "relspace x y = pow (x ×: y)"

(* Corresponds to CakeML's constant funspace *)
definition funspace where
  "funspace x y =
    (relspace x y suchthat
     (λf. ∀a. a ∈: x ⟶ (∃!b. (a,:b) ∈: f)))"

(* Corresponds to CakeML's constant apply *)
definition "apply" :: "'s ⇒ 's ⇒ 's" (infixl "⋅" 68) where
  "(x⋅y) = (SOME a. (y,:a) ∈: x)"

(* Corresponds to CakeML's overloading of boolset *)
definition boolset where
  "boolset ≡ two"

(* Corresponds to CakeML's constant true *)
definition true where
  "true = Ø"

(* Corresponds to CakeML's constant false *)
definition false where
  "false = one"

(* Corresponds to CakeML's theorem true_neq_false *)
lemma true_neq_false:
  "true ≠ false"
  using true_def false_def extensional one_def by auto

(* Corresponds to CakeML's theorem mem_boolset *)
lemma mem_boolset[simp]:
  "x ∈: boolset ⟷ ((x = true) ∨ (x = false))"
  using true_def false_def boolset_def by auto

(* Corresponds to CakeML's constant boolean *)
definition boolean :: "bool ⇒ 's" where
  "boolean b = (if b then true else false)"

(* Corresponds to CakeML's theorem boolean_in_boolset *)
lemma boolean_in_boolset:
  "boolean b ∈: boolset"
  using boolean_def one_def true_def false_def by auto

(* Corresponds to CakeML's theorem boolean_eq_true *)
lemma boolean_eq_true:
  "boolean b = true ⟷ b"
  using boolean_def true_neq_false by auto

(* Corresponds to CakeML's constant holds *)
definition "holds s x ⟷ s ⋅ x = true"

(* Corresponds to CakeML's constant abstract *)
definition abstract where
  "abstract doma rang f = ((doma ×: rang) suchthat (λx. ∃a. x = (a,:f a)))"

(* Corresponds to CakeML's theorem apply_abstract *)
lemma apply_abstract[simp]:
  "x ∈: s ⟹ f x ∈: t ⟹ abstract s t f ⋅ x = f x"
  using apply_def abstract_def pair_inj by auto

(* Corresponds to CakeML's theorem apply_abstract_matchable *)
lemma apply_abstract_matchable:
  "x ∈: s ⟹ f x ∈: t ⟹ f x = u ⟹ abstract s t f ⋅ x = u"
  using apply_abstract by auto

(* Corresponds to CakeML's theorem apply_in_rng *)
lemma apply_in_rng:
  assumes "x ∈: s"
  assumes "f ∈: funspace s t"
  shows "f ⋅ x ∈: t"
proof -
  from assms have "f ∈: (relspace s t suchthat (λf. ∀a. a ∈: s ⟶ (∃!b. (a ,: b) ∈: f)))"
    unfolding funspace_def by auto
  then have f_p: "f ∈: relspace s t ∧ (∀a. a ∈: s ⟶ (∃!b. (a ,: b) ∈: f))"
    by auto
  then have fxf: "(x ,: f ⋅ x) ∈: f"
    using someI assms apply_def by metis
  from f_p have "f ∈: pow (s ×: t)"
    unfolding relspace_def by auto
  then have "(x ,: f ⋅ x) ∈: (s ×: t)"
    using fxf by auto
  then show ?thesis
    using pair_inj by auto
qed

(* Corresponds to CakeML's theorem abstract_in_funspace  *)
lemma abstract_in_funspace[simp]:
  "(∀x. x ∈: s ⟶ f x ∈: t) ⟹ abstract s t f ∈: funspace s t"
  using funspace_def relspace_def abstract_def pair_inj by auto

(* Corresponds to CakeML's theorem abstract_in_funspace_matchable *)
lemma abstract_in_funspace_matchable:
  "(∀x. x ∈: s ⟶ f x ∈: t) ⟹ fs = funspace s t ⟹ abstract s t f ∈: fs"
  using abstract_in_funspace by auto

(* Corresponds to CakeML's theorem abstract_eq *)
lemma abstract_eq:
  assumes "∀x. x ∈: s ⟶ f x ∈: t1 ∧ g x ∈: t2 ∧ f x = g x"
  shows "abstract s t1 f = abstract s t2 g"
proof (rule iffD2[OF extensional], rule)
  fix a
  from assms show "a ∈: abstract s t1 f = a ∈: abstract s t2 g"
    unfolding abstract_def using pair_inj by auto
qed

lemma abstract_extensional:
  assumes "∀x. x ∈: s ⟶ f x ∈: t ∧ f x = g x"
  shows "abstract s t f = abstract s t g"
proof (rule iffD2[OF extensional], rule)
  fix a
  from assms show "a ∈: abstract s t f = a ∈: abstract s t g"
    unfolding abstract_def using pair_inj by auto
qed

lemma abstract_extensional':
  assumes "⋀x. x ∈: s ⟹ f x ∈: t"
  assumes "⋀x. x ∈: s ⟹ f x = g x"
  shows "abstract s t f = abstract s t g"
proof (rule iffD2[OF extensional], rule)
  fix a
  from assms show "a ∈: abstract s t f = a ∈: abstract s t g"
    unfolding abstract_def using pair_inj by auto
qed

lemma abstract_cong:
  assumes "∀x. x ∈: s ⟶ f x ∈: t ∧ g x ∈: t"
  assumes "abstract s t f = abstract s t g"
  assumes "x ∈: s"
  shows "f x = g x"
  using assms
  by (metis apply_abstract_matchable)

lemma abstract_cong_specific:
  assumes "x ∈: s"
  assumes "f x ∈: t"
  assumes "abstract s t f = abstract s t g"
  assumes "g x ∈: t"
  shows "f x = g x"
proof -
  have "f x = abstract s t f ⋅ x"
    using apply_abstract[of x s f t]
    using assms by auto
  also have "... = abstract s t g ⋅ x"
    using assms by auto
  also have "... = g x"
    using apply_abstract[of x s g t]
    using assms by auto
  finally show ?thesis 
    by auto
qed

lemma abstract_iff_extensional:
  assumes "∀x. x ∈: s ⟶ f x ∈: t ∧ g x ∈: t"
  shows "(abstract s t f = abstract s t g) ⟷ (∀x. x ∈: s ⟶ f x ∈: t ∧ f x = g x)"
  using assms abstract_cong
    abstract_extensional by meson

(* Corresponds to CakeML's theorem in_funspace_abstract *)
lemma in_funspace_abstract[simp]:
  assumes "z ∈: funspace s t"
  shows "∃f. z = abstract s t f ∧ (∀x. x ∈: s ⟶ f x ∈: t)"
proof -
  define f where "f = (λx. SOME y. (x,:y) ∈: z)"
  have "∀x. x ∈: z ⟷ x ∈: (abstract s t f)"
  proof (rule, rule)
    fix x
    assume xz: "x ∈: z"
    moreover
    have "∀b. b ∈: z ⟶ (∃ba c. b = (ba ,: c) ∧ ba ∈: s ∧ c ∈: t)"
      using xz assms
      unfolding funspace_def relspace_def by (auto)
    moreover
    have "∀a. a ∈: s ⟶ (∃!b. (a ,: b) ∈: z)"
      using xz using assms
      unfolding funspace_def relspace_def by auto
    ultimately
    have "∃a. x = (a ,: f a)"
      using assms f_def someI_ex unfolding funspace_def relspace_def by (metis (no_types, lifting))
    then show "x ∈: abstract s t f"
      using xz assms unfolding funspace_def relspace_def abstract_def by auto
  next
    fix x 
    assume xf: "x ∈: abstract s t f"
    then have "(∃b c. x = (b ,: c) ∧ b ∈: s ∧ c ∈: t)"
      unfolding abstract_def by simp
    moreover
    have "(∃a. x = (a ,: (SOME y. (a ,: y) ∈: z)))"
      using xf f_def unfolding abstract_def by simp
    moreover
    have "(∀a. a ∈: s ⟶ (∃!b. (a ,: b) ∈: z))"
      using assms unfolding funspace_def by simp
    ultimately
    show "x ∈: z"
      using f_def by (metis pair_inj someI_ex)
  qed
  then have "z = abstract s t f"
    using extensional by auto
  moreover
  from f_def have "∀x. x ∈: s ⟶ f x ∈: t"
    using apply_in_rng assms local.apply_def by force
  ultimately
  show ?thesis
    by auto   
qed

(* Corresponds to CakeML's theorem axiom_of_choice *)
theorem axiom_of_choice:
  assumes "∀a. a ∈: x ⟶ (∃b. b ∈: a)"
  shows "∃f. ∀a. a ∈: x ⟶ f ⋅ a ∈: a"
proof -
  define f where "f = (λa. SOME b. mem b a)"
  define fa where "fa = abstract x (uni x) f"

  have "∀a. a ∈: x ⟶ fa ⋅ a ∈: a"
  proof (rule, rule)
    fix a
    assume "a ∈: x"
    moreover
    have "f a ∈: ⋃:x"
      by (metis (full_types) assms calculation f_def mem_uni someI_ex)
    moreover
    have "f a ∈: a"
      using assms calculation(1) f_def someI_ex by force
    ultimately
    show "fa ⋅ a ∈: a"
      unfolding fa_def using apply_abstract by auto
  qed
  then show ?thesis
    by auto
qed

(* Corresponds to CakeML's constant is_infinite *)
definition is_infinite where
  "is_infinite s = infinite {a. a ∈: s}"

(* Corresponds to CakeML's theorem funspace_inhabited *)
lemma funspace_inhabited:
  "(∃x. x ∈: s) ⟹ (∃x. x ∈: t) ⟹ (∃f. f ∈: funspace s t)"
  apply (rule exI[of _ "abstract s t (λx. SOME x. x ∈: t)"])
  using abstract_in_funspace
  using someI by metis 

(* Corresponds to CakeML's constant tuple *)
fun tuple where
  "tuple [] = Ø" |
  "tuple (a#as) = (a,: tuple as)"

(* Corresponds to CakeML's theorem pair_not_empty *)
lemma pair_not_empty:
  "(x,:y) ≠ Ø"
  apply rule
  unfolding extensional using mem_empty pair_def mem_upair by metis

(* Corresponds to CakeML's theorem tuple_empty *)
lemma tuple_empty:
  "tuple ls = Ø ⟷ ls = []"
  using pair_not_empty by (cases ls) auto

(* Corresponds to CakeML's theorem tuple_inj *)
lemma tuple_inj:
  "tuple l1 = tuple l2 ⟷ l1 = l2"
proof (induction l1 arbitrary: l2)
  case Nil
  then show ?case 
    using tuple_empty by metis
next
  case (Cons a l1)
  then show ?case
    using pair_not_empty pair_inj by (metis tuple.elims tuple.simps(2))
qed

(* Corresponds to CakeML's constant bigcross *)
fun bigcross where
  "bigcross [] = one" |
  "bigcross (a#as) = a ×: (bigcross as)"

(* Corresponds to CakeML's theorem mem_bigcross *)
lemma mem_bigcross[simp]:
  "x ∈: (bigcross ls) ⟷ (∃xs. x = tuple xs ∧ list_all2 mem xs ls)"
proof (induction ls arbitrary: x)
  case Nil
  then show ?case 
    using mem_one mem_product by simp
next
  case (Cons l ls)
  show ?case 
  proof
    assume "x ∈: bigcross (l # ls)"
    then obtain b c where bc_p: "x = (b ,: c) ∧ b ∈: l ∧ c ∈: bigcross ls " 
      by auto
    then obtain xs' where "c = tuple xs' ∧ list_all2 (∈:) xs' ls" 
      using Cons[of c] by auto
    then have "x = tuple (b#xs') ∧ list_all2 (∈:) (b#xs') (l # ls)"
      using bc_p by auto
    then show "∃xs. x = tuple xs ∧ list_all2 (∈:) xs (l # ls)"
      by metis
  next 
    assume "∃xs. x = tuple xs ∧ list_all2 (∈:) xs (l # ls)"
    then obtain xs where "x = tuple xs ∧ list_all2 (∈:) xs (l # ls)"
      by auto
    then obtain xs where "x = tuple xs ∧ list_all2 (∈:) xs (l # ls)"
      by auto
    then show "x ∈: bigcross (l # ls)"
      using Cons list.distinct(1) list.rel_cases mem_product by fastforce
  qed
qed

definition subs :: "'s ⇒ 's ⇒ bool" (infix "⊆:" 67) where
  "x ⊆: y ⟷ x ∈: pow y"


definition one_elem_fun :: "'s ⇒ 's ⇒ 's" where
  "one_elem_fun x d = abstract d boolset (λy. boolean (x=y))"

definition iden :: "'s ⇒ 's" where
  "iden D = abstract D (funspace D boolset) (λx. one_elem_fun x D)"

lemma apply_id[simp]:
  assumes A_in_D: "A ∈: D"
  assumes B_in_D: "B ∈: D"
  shows "iden D ⋅ A ⋅ B = boolean (A = B)"
proof -
  have abstract_D: "abstract D boolset (λy. boolean (A = y)) ∈: funspace D boolset"
    using boolean_in_boolset by auto
  have bool_in_two: "boolean (A = B) ∈: boolset"
    using boolean_in_boolset by blast
  have "(boolean (A = B)) = (abstract D boolset (λy. boolean (A = y)) ⋅ B)"
    using apply_abstract[of B D "λy. boolean (A = y)" two] B_in_D bool_in_two by auto
  also
  have "... = (abstract D (funspace D boolset) (λx. abstract D boolset (λy. boolean (x = y))) ⋅ A) ⋅ B" 
    using A_in_D abstract_D 
      apply_abstract[of A D "λx. abstract D boolset (λy. boolean (x = y))" "funspace D boolset"]
    by auto 
  also
  have "... = iden D ⋅ A ⋅ B"
    unfolding iden_def one_elem_fun_def ..
  finally
  show ?thesis
    by auto
qed

lemma apply_id_true[simp]:
  assumes A_in_D: "A ∈: D"
  assumes B_in_D: "B ∈: D"
  shows "iden D ⋅ A ⋅ B = true ⟷ A = B"
  using assms using boolean_def using true_neq_false by auto

lemma apply_if_pair_in:
  assumes "(a1,: a2) ∈: f"
  assumes "f ∈: funspace s t"
  shows "f ⋅ a1 = a2"
  using assms
  by (smt abstract_def apply_abstract mem_product pair_inj set_theory.in_funspace_abstract 
      set_theory.mem_sub set_theory_axioms)

lemma funspace_app_unique:
  assumes "f ∈: funspace s t"
  assumes "(a1,: a2) ∈: f"
  assumes "(a1,: a3) ∈: f"
  shows "a3 = a2"
  using assms apply_if_pair_in by blast

lemma funspace_extensional:
  assumes "f ∈: funspace s t"
  assumes "g ∈: funspace s t"
  assumes "∀x. x ∈: s ⟶ f ⋅ x = g ⋅ x"
  shows "f = g"
proof -
  have "⋀a. a ∈: f ⟹ a ∈: g"
  proof -
    fix a
    assume af: "a ∈: f"
    from af have "∃a1 a2. a1 ∈:s ∧ a2 ∈: t ∧ (a1 ,: a2) = a"
      using assms unfolding funspace_def apply_def using relspace_def by force
    then obtain a1 a2 where a12:
      "a1 ∈:s ∧ a2 ∈: t ∧ (a1 ,: a2) = a"
      by blast
    then have "∃a3. a2 ∈: t ∧ (a1 ,: a3) ∈: g"
      using assms(2) funspace_def by auto
    then obtain a3 where a3: "a2 ∈: t ∧ (a1 ,: a3) ∈: g"
      by auto
    then have "a3 = a2"
      using a12 af assms(1,2,3) apply_if_pair_in by auto
    then show "a ∈: g"
      using a12 a3 by blast
  qed
  moreover
  have "⋀a. a ∈: g ⟹ a ∈: f"
  proof -
    fix a
    assume ag: "a ∈: g"
    then have "∃a1 a2. a1 ∈:s ∧ a2 ∈: t ∧ (a1 ,: a2) = a"
      using assms unfolding funspace_def apply_def using relspace_def by force
    then obtain a1 a2 where a12:
      "a1 ∈:s ∧ a2 ∈: t ∧ (a1 ,: a2) = a"
      by blast
    then have "∃a3. a2 ∈: t ∧ (a1 ,: a3) ∈: f"
      using assms(1) funspace_def by auto
    then obtain a3 where a3: "a2 ∈: t ∧ (a1 ,: a3) ∈: f"
      by auto
    then have "a3 = a2"
      using a12 ag assms(1,2,3) apply_if_pair_in by auto
    then show "a ∈: f"
      using a3 a12 by blast
  qed
  ultimately
  show ?thesis 
    using iffD2[OF extensional] by metis
qed

lemma funspace_difference_witness:
  assumes "f ∈: funspace s t"
  assumes "g ∈: funspace s t"
  assumes "f ≠ g"
  shows "∃z. z ∈: s ∧ f ⋅ z ≠ g ⋅ z"
  using assms(1,2,3) funspace_extensional by blast


end

end