# Theory FunctionOrder

Up to index of Isabelle/HOL/HOL-Complex/HahnBanach

theory FunctionOrder
imports Subspace Linearform
begin

    (*  Title:      HOL/Real/HahnBanach/FunctionOrder.thy
        ID:         $Id: FunctionOrder.thy,v 1.19 2005/06/17 14:13:09 haftmann Exp $
        Author:     Gertrud Bauer, TU Munich
    *)

    header {* An order on functions *}

    theory FunctionOrder imports Subspace Linearform begin

    subsection {* The graph of a function *}

    text {*
      We define the \emph{graph} of a (real) function @{text f} with
      domain @{text F} as the set
      \begin{center}
      @{text "{(x, f x). x ∈ F}"}
      \end{center}
      So we are modeling partial functions by specifying the domain and
      the mapping function. We use the term ``function'' also for its
      graph.
    *}

    types 'a graph = "('a × real) set"

    constdefs
      graph :: "'a set => ('a => real) => 'a graph"
      "graph F f ≡ {(x, f x) | x. x ∈ F}"

    lemma graphI [intro]: "x ∈ F ==> (x, f x) ∈ graph F f"
      by (unfold graph_def) blast

    lemma graphI2 [intro?]: "x ∈ F ==> ∃t ∈ graph F f. t = (x, f x)"
      by (unfold graph_def) blast

    lemma graphE [elim?]:
        "(x, y) ∈ graph F f ==> (x ∈ F ==> y = f x ==> C) ==> C"
      by (unfold graph_def) blast

    subsection {* Functions ordered by domain extension *}

    text {*
      A function @{text h'} is an extension of @{text h}, iff the graph of
      @{text h} is a subset of the graph of @{text h'}.
    *}

    lemma graph_extI:
      "(!!x. x ∈ H ==> h x = h' x) ==> H ⊆ H'
        ==> graph H h ⊆ graph H' h'"
      by (unfold graph_def) blast

    lemma graph_extD1 [dest?]:
      "graph H h ⊆ graph H' h' ==> x ∈ H ==> h x = h' x"
      by (unfold graph_def) blast

    lemma graph_extD2 [dest?]:
      "graph H h ⊆ graph H' h' ==> H ⊆ H'"
      by (unfold graph_def) blast

    subsection {* Domain and function of a graph *}

    text {*
      The inverse functions to @{text graph} are @{text domain} and @{text
      funct}.
    *}

    constdefs
      "domain" :: "'a graph => 'a set"
      "domain g ≡ {x. ∃y. (x, y) ∈ g}"

      funct :: "'a graph => ('a => real)"
      "funct g ≡ λx. (SOME y. (x, y) ∈ g)"

    text {*
      The following lemma states that @{text g} is the graph of a function
      if the relation induced by @{text g} is unique.
    *}

    lemma graph_domain_funct:
      assumes uniq: "!!x y z. (x, y) ∈ g ==> (x, z) ∈ g ==> z = y"
      shows "graph (domain g) (funct g) = g"
    proof (unfold domain_def funct_def graph_def, auto)  (* FIXME !? *)
      fix a b assume "(a, b) ∈ g"
      show "(a, SOME y. (a, y) ∈ g) ∈ g" by (rule someI2)
      show "∃y. (a, y) ∈ g" ..
      show "b = (SOME y. (a, y) ∈ g)"
      proof (rule some_equality [symmetric])
        fix y assume "(a, y) ∈ g"
        show "y = b" by (rule uniq)
      qed
    qed

    subsection {* Norm-preserving extensions of a function *}

    text {*
      Given a linear form @{text f} on the space @{text F} and a seminorm
      @{text p} on @{text E}. The set of all linear extensions of @{text
      f}, to superspaces @{text H} of @{text F}, which are bounded by
      @{text p}, is defined as follows.
    *}

    constdefs
      norm_pres_extensions ::
        "'a::{plus, minus, zero} set => ('a => real) => 'a set => ('a => real)
          => 'a graph set"
        "norm_pres_extensions E p F f
          ≡ {g. ∃H h. g = graph H h
              ∧ linearform H h
              ∧ H \<unlhd> E
              ∧ F \<unlhd> H
              ∧ graph F f ⊆ graph H h
              ∧ (∀x ∈ H. h x ≤ p x)}"

    lemma norm_pres_extensionE [elim]:
      "g ∈ norm_pres_extensions E p F f
      ==> (!!H h. g = graph H h ==> linearform H h
            ==> H \<unlhd> E ==> F \<unlhd> H ==> graph F f ⊆ graph H h
            ==> ∀x ∈ H. h x ≤ p x ==> C) ==> C"
      by (unfold norm_pres_extensions_def) blast

    lemma norm_pres_extensionI2 [intro]:
      "linearform H h ==> H \<unlhd> E ==> F \<unlhd> H
        ==> graph F f ⊆ graph H h ==> ∀x ∈ H. h x ≤ p x
        ==> graph H h ∈ norm_pres_extensions E p F f"
      by (unfold norm_pres_extensions_def) blast

    lemma norm_pres_extensionI:  (* FIXME ? *)
      "∃H h. g = graph H h
        ∧ linearform H h
        ∧ H \<unlhd> E
        ∧ F \<unlhd> H
        ∧ graph F f ⊆ graph H h
        ∧ (∀x ∈ H. h x ≤ p x) ==> g ∈ norm_pres_extensions E p F f"
      by (unfold norm_pres_extensions_def) blast

    end

### The graph of a function

lemma graphI:

      x ∈ F ==> (x, f x) ∈ graph F f

lemma graphI2:

      x ∈ F ==> ∃t∈graph F f. t = (x, f x)

lemma graphE:

      [| (x, y) ∈ graph F f; [| x ∈ F; y = f x |] ==> C |] ==> C

### Functions ordered by domain extension

lemma graph_extI:

      [| !!x. x ∈ H ==> h x = h' x; H ⊆ H' |] ==> graph H h ⊆ graph H' h'

lemma graph_extD1:

      [| graph H h ⊆ graph H' h'; x ∈ H |] ==> h x = h' x

lemma graph_extD2:

      graph H h ⊆ graph H' h' ==> H ⊆ H'

### Domain and function of a graph

lemma graph_domain_funct:

      (!!x y z. [| (x, y) ∈ g; (x, z) ∈ g |] ==> z = y)
      ==> graph (domain g) (funct g) = g

### Norm-preserving extensions of a function

lemma norm_pres_extensionE:

      [| g ∈ norm_pres_extensions E p F f;
         !!H h. [| g = graph H h; linearform H h; subspace H E; subspace F H;
                   graph F f ⊆ graph H h; ∀x∈H. h x ≤ p x |]
                ==> C |]
      ==> C

lemma norm_pres_extensionI2:

      [| linearform H h; subspace H E; subspace F H; graph F f ⊆ graph H h;
         ∀x∈H. h x ≤ p x |]
      ==> graph H h ∈ norm_pres_extensions E p F f

lemma norm_pres_extensionI:

      ∃H h. g = graph H h ∧
            linearform H h ∧
            subspace H E ∧ subspace F H ∧ graph F f ⊆ graph H h ∧ (∀x∈H. h x ≤ p x)
      ==> g ∈ norm_pres_extensions E p F f