src/HOL/Nonstandard_Analysis/CStar.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64604 2bf8cfc98c4d
permissions -rw-r--r--
executable domain membership checks
wenzelm@62479
     1
(*  Title:      HOL/Nonstandard_Analysis/CStar.thy
wenzelm@62479
     2
    Author:     Jacques D. Fleuriot
wenzelm@62479
     3
    Copyright:  2001 University of Edinburgh
huffman@27468
     4
*)
huffman@27468
     5
wenzelm@64604
     6
section \<open>Star-transforms in NSA, Extending Sets of Complex Numbers and Complex Functions\<close>
huffman@27468
     7
huffman@27468
     8
theory CStar
wenzelm@64604
     9
  imports NSCA
huffman@27468
    10
begin
huffman@27468
    11
wenzelm@64604
    12
subsection \<open>Properties of the \<open>*\<close>-Transform Applied to Sets of Reals\<close>
huffman@27468
    13
wenzelm@64604
    14
lemma STARC_hcomplex_of_complex_Int: "*s* X \<inter> SComplex = hcomplex_of_complex ` X"
wenzelm@64604
    15
  by (auto simp: Standard_def)
huffman@27468
    16
wenzelm@64604
    17
lemma lemma_not_hcomplexA: "x \<notin> hcomplex_of_complex ` A \<Longrightarrow> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"
wenzelm@64604
    18
  by auto
wenzelm@64604
    19
huffman@27468
    20
wenzelm@64604
    21
subsection \<open>Theorems about Nonstandard Extensions of Functions\<close>
huffman@27468
    22
wenzelm@64604
    23
lemma starfunC_hcpow: "\<And>Z. ( *f* (\<lambda>z. z ^ n)) Z = Z pow hypnat_of_nat n"
wenzelm@64604
    24
  by transfer (rule refl)
huffman@27468
    25
huffman@27468
    26
lemma starfunCR_cmod: "*f* cmod = hcmod"
wenzelm@64604
    27
  by transfer (rule refl)
huffman@27468
    28
wenzelm@64604
    29
wenzelm@64604
    30
subsection \<open>Internal Functions - Some Redundancy With \<open>*f*\<close> Now\<close>
huffman@27468
    31
huffman@27468
    32
(** subtraction: ( *fn) - ( *gn) = *(fn - gn) **)
huffman@27468
    33
(*
huffman@27468
    34
lemma starfun_n_diff:
wenzelm@64604
    35
   "( *fn* f) z - ( *fn* g) z = ( *fn* (\<lambda>i x. f i x - g i x)) z"
huffman@27468
    36
apply (cases z)
huffman@27468
    37
apply (simp add: starfun_n star_n_diff)
huffman@27468
    38
done
huffman@27468
    39
*)
huffman@27468
    40
(** composition: ( *fn) o ( *gn) = *(fn o gn) **)
huffman@27468
    41
huffman@27468
    42
lemma starfun_Re: "( *f* (\<lambda>x. Re (f x))) = (\<lambda>x. hRe (( *f* f) x))"
wenzelm@64604
    43
  by transfer (rule refl)
huffman@27468
    44
huffman@27468
    45
lemma starfun_Im: "( *f* (\<lambda>x. Im (f x))) = (\<lambda>x. hIm (( *f* f) x))"
wenzelm@64604
    46
  by transfer (rule refl)
huffman@27468
    47
huffman@27468
    48
lemma starfunC_eq_Re_Im_iff:
wenzelm@64604
    49
  "( *f* f) x = z \<longleftrightarrow> ( *f* (\<lambda>x. Re (f x))) x = hRe z \<and> ( *f* (\<lambda>x. Im (f x))) x = hIm z"
wenzelm@64604
    50
  by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im)
huffman@27468
    51
huffman@27468
    52
lemma starfunC_approx_Re_Im_iff:
wenzelm@64604
    53
  "( *f* f) x \<approx> z \<longleftrightarrow> ( *f* (\<lambda>x. Re (f x))) x \<approx> hRe z \<and> ( *f* (\<lambda>x. Im (f x))) x \<approx> hIm z"
wenzelm@64604
    54
  by (simp add: hcomplex_approx_iff starfun_Re starfun_Im)
huffman@27468
    55
huffman@27468
    56
end