src/HOL/NSA/StarDef.thy
author wenzelm
Thu, 12 Apr 2012 18:39:19 +0200
changeset 47432 e1576d13e933
parent 47328 9f11a3cd84b1
child 48891 c0eafbd55de3
permissions -rw-r--r--
more standard method setup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     1
(*  Title       : HOL/Hyperreal/StarDef.thy
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot and Brian Huffman
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     3
*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     4
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     5
header {* Construction of Star Types Using Ultrafilters *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     6
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     7
theory StarDef
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     8
imports Filter
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     9
uses ("transfer.ML")
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    10
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    11
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    12
subsection {* A Free Ultrafilter over the Naturals *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    13
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    14
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    15
  FreeUltrafilterNat :: "nat set set"  ("\<U>") where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    16
  "\<U> = (SOME U. freeultrafilter U)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    17
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    18
lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    19
apply (unfold FreeUltrafilterNat_def)
46008
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 45694
diff changeset
    20
apply (rule someI_ex)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    21
apply (rule freeultrafilter_Ex)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    22
apply (rule nat_infinite)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    23
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    24
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30198
diff changeset
    25
interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    26
by (rule freeultrafilter_FreeUltrafilterNat)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    27
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    28
text {* This rule takes the place of the old ultra tactic *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    29
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    30
lemma ultra:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    31
  "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    32
by (simp add: Collect_imp_eq
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    33
    FreeUltrafilterNat.Un_iff FreeUltrafilterNat.Compl_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    34
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    35
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    36
subsection {* Definition of @{text star} type constructor *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    37
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    38
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    39
  starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    40
  "starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    41
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45605
diff changeset
    42
definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45605
diff changeset
    43
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45605
diff changeset
    44
typedef (open) 'a star = "star :: (nat \<Rightarrow> 'a) set set"
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45605
diff changeset
    45
  unfolding star_def by (auto intro: quotientI)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    46
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    47
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    48
  star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star" where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    49
  "star_n X = Abs_star (starrel `` {X})"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    50
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    51
theorem star_cases [case_names star_n, cases type: star]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    52
  "(\<And>X. x = star_n X \<Longrightarrow> P) \<Longrightarrow> P"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    53
by (cases x, unfold star_n_def star_def, erule quotientE, fast)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    54
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    55
lemma all_star_eq: "(\<forall>x. P x) = (\<forall>X. P (star_n X))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    56
by (auto, rule_tac x=x in star_cases, simp)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    57
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    58
lemma ex_star_eq: "(\<exists>x. P x) = (\<exists>X. P (star_n X))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    59
by (auto, rule_tac x=x in star_cases, auto)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    60
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    61
text {* Proving that @{term starrel} is an equivalence relation *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    62
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    63
lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    64
by (simp add: starrel_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    65
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    66
lemma equiv_starrel: "equiv UNIV starrel"
40815
6e2d17cc0d1d equivI has replaced equiv.intro
haftmann
parents: 39302
diff changeset
    67
proof (rule equivI)
30198
922f944f03b2 name changes
nipkow
parents: 29904
diff changeset
    68
  show "refl starrel" by (simp add: refl_on_def)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    69
  show "sym starrel" by (simp add: sym_def eq_commute)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    70
  show "trans starrel" by (auto intro: transI elim!: ultra)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    71
qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    72
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    73
lemmas equiv_starrel_iff =
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    74
  eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    75
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    76
lemma starrel_in_star: "starrel``{x} \<in> star"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    77
by (simp add: star_def quotientI)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    78
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    79
lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    80
by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    81
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    82
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    83
subsection {* Transfer principle *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    84
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    85
text {* This introduction rule starts each transfer proof. *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    86
lemma transfer_start:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    87
  "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    88
by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    89
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    90
text {*Initialize transfer tactic.*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    91
use "transfer.ML"
47328
9f11a3cd84b1 rename ML structure to avoid shadowing earlier name
huffman
parents: 47108
diff changeset
    92
setup Transfer_Principle.setup
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    93
47432
e1576d13e933 more standard method setup;
wenzelm
parents: 47328
diff changeset
    94
method_setup transfer = {*
e1576d13e933 more standard method setup;
wenzelm
parents: 47328
diff changeset
    95
  Attrib.thms >> (fn ths => fn ctxt =>
e1576d13e933 more standard method setup;
wenzelm
parents: 47328
diff changeset
    96
    SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))
e1576d13e933 more standard method setup;
wenzelm
parents: 47328
diff changeset
    97
*} "transfer principle"
e1576d13e933 more standard method setup;
wenzelm
parents: 47328
diff changeset
    98
e1576d13e933 more standard method setup;
wenzelm
parents: 47328
diff changeset
    99
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   100
text {* Transfer introduction rules. *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   101
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   102
lemma transfer_ex [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   103
  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   104
    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   105
by (simp only: ex_star_eq FreeUltrafilterNat.Collect_ex)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   106
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   107
lemma transfer_all [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   108
  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   109
    \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   110
by (simp only: all_star_eq FreeUltrafilterNat.Collect_all)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   111
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   112
lemma transfer_not [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   113
  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   114
by (simp only: FreeUltrafilterNat.Collect_not)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   115
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   116
lemma transfer_conj [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   117
  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   118
    \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   119
by (simp only: FreeUltrafilterNat.Collect_conj)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   120
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   121
lemma transfer_disj [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   122
  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   123
    \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   124
by (simp only: FreeUltrafilterNat.Collect_disj)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   125
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   126
lemma transfer_imp [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   127
  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   128
    \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   129
by (simp only: imp_conv_disj transfer_disj transfer_not)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   130
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   131
lemma transfer_iff [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   132
  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   133
    \<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   134
by (simp only: iff_conv_conj_imp transfer_conj transfer_imp)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   135
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   136
lemma transfer_if_bool [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   137
  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   138
    \<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   139
by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   140
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   141
lemma transfer_eq [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   142
  "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   143
by (simp only: star_n_eq_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   144
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   145
lemma transfer_if [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   146
  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   147
    \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   148
apply (rule eq_reflection)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   149
apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   150
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   151
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   152
lemma transfer_fun_eq [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   153
  "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   154
    \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   155
      \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   156
by (simp only: fun_eq_iff transfer_all)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   157
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   158
lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   159
by (rule reflexive)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   160
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   161
lemma transfer_bool [transfer_intro]: "p \<equiv> {n. p} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   162
by (simp add: atomize_eq)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   163
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   164
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   165
subsection {* Standard elements *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   166
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   167
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   168
  star_of :: "'a \<Rightarrow> 'a star" where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   169
  "star_of x == star_n (\<lambda>n. x)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   170
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   171
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   172
  Standard :: "'a star set" where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   173
  "Standard = range star_of"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   174
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   175
text {* Transfer tactic should remove occurrences of @{term star_of} *}
47328
9f11a3cd84b1 rename ML structure to avoid shadowing earlier name
huffman
parents: 47108
diff changeset
   176
setup {* Transfer_Principle.add_const "StarDef.star_of" *}
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   177
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   178
declare star_of_def [transfer_intro]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   179
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   180
lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   181
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   182
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   183
lemma Standard_star_of [simp]: "star_of x \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   184
by (simp add: Standard_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   185
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   186
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   187
subsection {* Internal functions *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   188
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   189
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   190
  Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300) where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   191
  "Ifun f \<equiv> \<lambda>x. Abs_star
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   192
       (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   193
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   194
lemma Ifun_congruent2:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   195
  "congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   196
by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   197
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   198
lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   199
by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   200
    UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   201
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   202
text {* Transfer tactic should remove occurrences of @{term Ifun} *}
47328
9f11a3cd84b1 rename ML structure to avoid shadowing earlier name
huffman
parents: 47108
diff changeset
   203
setup {* Transfer_Principle.add_const "StarDef.Ifun" *}
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   204
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   205
lemma transfer_Ifun [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   206
  "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   207
by (simp only: Ifun_star_n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   208
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   209
lemma Ifun_star_of [simp]: "star_of f \<star> star_of x = star_of (f x)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   210
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   211
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   212
lemma Standard_Ifun [simp]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   213
  "\<lbrakk>f \<in> Standard; x \<in> Standard\<rbrakk> \<Longrightarrow> f \<star> x \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   214
by (auto simp add: Standard_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   215
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   216
text {* Nonstandard extensions of functions *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   217
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   218
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   219
  starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)"  ("*f* _" [80] 80) where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   220
  "starfun f == \<lambda>x. star_of f \<star> x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   221
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   222
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   223
  starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   224
    ("*f2* _" [80] 80) where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   225
  "starfun2 f == \<lambda>x y. star_of f \<star> x \<star> y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   226
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   227
declare starfun_def [transfer_unfold]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   228
declare starfun2_def [transfer_unfold]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   229
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   230
lemma starfun_star_n: "( *f* f) (star_n X) = star_n (\<lambda>n. f (X n))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   231
by (simp only: starfun_def star_of_def Ifun_star_n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   232
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   233
lemma starfun2_star_n:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   234
  "( *f2* f) (star_n X) (star_n Y) = star_n (\<lambda>n. f (X n) (Y n))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   235
by (simp only: starfun2_def star_of_def Ifun_star_n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   236
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   237
lemma starfun_star_of [simp]: "( *f* f) (star_of x) = star_of (f x)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   238
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   239
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   240
lemma starfun2_star_of [simp]: "( *f2* f) (star_of x) = *f* f x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   241
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   242
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   243
lemma Standard_starfun [simp]: "x \<in> Standard \<Longrightarrow> starfun f x \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   244
by (simp add: starfun_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   245
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   246
lemma Standard_starfun2 [simp]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   247
  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> starfun2 f x y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   248
by (simp add: starfun2_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   249
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   250
lemma Standard_starfun_iff:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   251
  assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   252
  shows "(starfun f x \<in> Standard) = (x \<in> Standard)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   253
proof
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   254
  assume "x \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   255
  thus "starfun f x \<in> Standard" by simp
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   256
next
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   257
  have inj': "\<And>x y. starfun f x = starfun f y \<Longrightarrow> x = y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   258
    using inj by transfer
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   259
  assume "starfun f x \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   260
  then obtain b where b: "starfun f x = star_of b"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   261
    unfolding Standard_def ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   262
  hence "\<exists>x. starfun f x = star_of b" ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   263
  hence "\<exists>a. f a = b" by transfer
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   264
  then obtain a where "f a = b" ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   265
  hence "starfun f (star_of a) = star_of b" by transfer
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   266
  with b have "starfun f x = starfun f (star_of a)" by simp
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   267
  hence "x = star_of a" by (rule inj')
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   268
  thus "x \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   269
    unfolding Standard_def by auto
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   270
qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   271
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   272
lemma Standard_starfun2_iff:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   273
  assumes inj: "\<And>a b a' b'. f a b = f a' b' \<Longrightarrow> a = a' \<and> b = b'"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   274
  shows "(starfun2 f x y \<in> Standard) = (x \<in> Standard \<and> y \<in> Standard)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   275
proof
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   276
  assume "x \<in> Standard \<and> y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   277
  thus "starfun2 f x y \<in> Standard" by simp
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   278
next
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   279
  have inj': "\<And>x y z w. starfun2 f x y = starfun2 f z w \<Longrightarrow> x = z \<and> y = w"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   280
    using inj by transfer
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   281
  assume "starfun2 f x y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   282
  then obtain c where c: "starfun2 f x y = star_of c"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   283
    unfolding Standard_def ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   284
  hence "\<exists>x y. starfun2 f x y = star_of c" by auto
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   285
  hence "\<exists>a b. f a b = c" by transfer
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   286
  then obtain a b where "f a b = c" by auto
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   287
  hence "starfun2 f (star_of a) (star_of b) = star_of c"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   288
    by transfer
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   289
  with c have "starfun2 f x y = starfun2 f (star_of a) (star_of b)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   290
    by simp
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   291
  hence "x = star_of a \<and> y = star_of b"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   292
    by (rule inj')
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   293
  thus "x \<in> Standard \<and> y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   294
    unfolding Standard_def by auto
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   295
qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   296
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   297
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   298
subsection {* Internal predicates *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   299
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   300
definition unstar :: "bool star \<Rightarrow> bool" where
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 36414
diff changeset
   301
  "unstar b \<longleftrightarrow> b = star_of True"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   302
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   303
lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   304
by (simp add: unstar_def star_of_def star_n_eq_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   305
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   306
lemma unstar_star_of [simp]: "unstar (star_of p) = p"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   307
by (simp add: unstar_def star_of_inject)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   308
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   309
text {* Transfer tactic should remove occurrences of @{term unstar} *}
47328
9f11a3cd84b1 rename ML structure to avoid shadowing earlier name
huffman
parents: 47108
diff changeset
   310
setup {* Transfer_Principle.add_const "StarDef.unstar" *}
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   311
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   312
lemma transfer_unstar [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   313
  "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   314
by (simp only: unstar_star_n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   315
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   316
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   317
  starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool"  ("*p* _" [80] 80) where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   318
  "*p* P = (\<lambda>x. unstar (star_of P \<star> x))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   319
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   320
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   321
  starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool"  ("*p2* _" [80] 80) where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   322
  "*p2* P = (\<lambda>x y. unstar (star_of P \<star> x \<star> y))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   323
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   324
declare starP_def [transfer_unfold]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   325
declare starP2_def [transfer_unfold]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   326
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   327
lemma starP_star_n: "( *p* P) (star_n X) = ({n. P (X n)} \<in> \<U>)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   328
by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   329
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   330
lemma starP2_star_n:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   331
  "( *p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} \<in> \<U>)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   332
by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   333
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   334
lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   335
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   336
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   337
lemma starP2_star_of [simp]: "( *p2* P) (star_of x) = *p* P x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   338
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   339
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   340
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   341
subsection {* Internal sets *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   342
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   343
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   344
  Iset :: "'a set star \<Rightarrow> 'a star set" where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   345
  "Iset A = {x. ( *p2* op \<in>) x A}"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   346
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   347
lemma Iset_star_n:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   348
  "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   349
by (simp add: Iset_def starP2_star_n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   350
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   351
text {* Transfer tactic should remove occurrences of @{term Iset} *}
47328
9f11a3cd84b1 rename ML structure to avoid shadowing earlier name
huffman
parents: 47108
diff changeset
   352
setup {* Transfer_Principle.add_const "StarDef.Iset" *}
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   353
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   354
lemma transfer_mem [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   355
  "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   356
    \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   357
by (simp only: Iset_star_n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   358
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   359
lemma transfer_Collect [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   360
  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   361
    \<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   362
by (simp add: atomize_eq set_eq_iff all_star_eq Iset_star_n)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   363
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   364
lemma transfer_set_eq [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   365
  "\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   366
    \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   367
by (simp only: set_eq_iff transfer_all transfer_iff transfer_mem)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   368
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   369
lemma transfer_ball [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   370
  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   371
    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   372
by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   373
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   374
lemma transfer_bex [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   375
  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   376
    \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   377
by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   378
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   379
lemma transfer_Iset [transfer_intro]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   380
  "\<lbrakk>a \<equiv> star_n A\<rbrakk> \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   381
by simp
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   382
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   383
text {* Nonstandard extensions of sets. *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   384
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   385
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   386
  starset :: "'a set \<Rightarrow> 'a star set" ("*s* _" [80] 80) where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   387
  "starset A = Iset (star_of A)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   388
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   389
declare starset_def [transfer_unfold]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   390
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   391
lemma starset_mem: "(star_of x \<in> *s* A) = (x \<in> A)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   392
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   393
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   394
lemma starset_UNIV: "*s* (UNIV::'a set) = (UNIV::'a star set)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   395
by (transfer UNIV_def, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   396
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   397
lemma starset_empty: "*s* {} = {}"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   398
by (transfer empty_def, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   399
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   400
lemma starset_insert: "*s* (insert x A) = insert (star_of x) ( *s* A)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   401
by (transfer insert_def Un_def, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   402
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   403
lemma starset_Un: "*s* (A \<union> B) = *s* A \<union> *s* B"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   404
by (transfer Un_def, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   405
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   406
lemma starset_Int: "*s* (A \<inter> B) = *s* A \<inter> *s* B"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   407
by (transfer Int_def, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   408
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   409
lemma starset_Compl: "*s* -A = -( *s* A)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   410
by (transfer Compl_eq, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   411
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   412
lemma starset_diff: "*s* (A - B) = *s* A - *s* B"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   413
by (transfer set_diff_eq, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   414
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   415
lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   416
by (transfer image_def, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   417
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   418
lemma starset_vimage: "*s* (f -` A) = ( *f* f) -` ( *s* A)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   419
by (transfer vimage_def, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   420
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   421
lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   422
by (transfer subset_eq, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   423
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   424
lemma starset_eq: "( *s* A = *s* B) = (A = B)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   425
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   426
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   427
lemmas starset_simps [simp] =
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   428
  starset_mem     starset_UNIV
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   429
  starset_empty   starset_insert
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   430
  starset_Un      starset_Int
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   431
  starset_Compl   starset_diff
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   432
  starset_image   starset_vimage
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   433
  starset_subset  starset_eq
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   434
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   435
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   436
subsection {* Syntactic classes *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   437
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   438
instantiation star :: (zero) zero
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   439
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   440
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   441
definition
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 36414
diff changeset
   442
  star_zero_def:    "0 \<equiv> star_of 0"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   443
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   444
instance ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   445
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   446
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   447
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   448
instantiation star :: (one) one
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   449
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   450
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   451
definition
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 36414
diff changeset
   452
  star_one_def:     "1 \<equiv> star_of 1"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   453
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   454
instance ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   455
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   456
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   457
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   458
instantiation star :: (plus) plus
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   459
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   460
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   461
definition
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 36414
diff changeset
   462
  star_add_def:     "(op +) \<equiv> *f2* (op +)"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   463
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   464
instance ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   465
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   466
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   467
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   468
instantiation star :: (times) times
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   469
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   470
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   471
definition
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 36414
diff changeset
   472
  star_mult_def:    "(op *) \<equiv> *f2* (op *)"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   473
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   474
instance ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   475
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   476
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   477
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   478
instantiation star :: (uminus) uminus
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   479
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   480
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   481
definition
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 36414
diff changeset
   482
  star_minus_def:   "uminus \<equiv> *f* uminus"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   483
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   484
instance ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   485
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   486
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   487
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   488
instantiation star :: (minus) minus
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   489
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   490
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   491
definition
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 36414
diff changeset
   492
  star_diff_def:    "(op -) \<equiv> *f2* (op -)"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   493
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   494
instance ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   495
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   496
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   497
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   498
instantiation star :: (abs) abs
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   499
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   500
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   501
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   502
  star_abs_def:     "abs \<equiv> *f* abs"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   503
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   504
instance ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   505
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   506
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   507
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   508
instantiation star :: (sgn) sgn
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   509
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   510
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   511
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   512
  star_sgn_def:     "sgn \<equiv> *f* sgn"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   513
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   514
instance ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   515
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   516
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   517
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   518
instantiation star :: (inverse) inverse
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   519
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   520
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   521
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   522
  star_divide_def:  "(op /) \<equiv> *f2* (op /)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   523
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   524
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   525
  star_inverse_def: "inverse \<equiv> *f* inverse"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   526
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   527
instance ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   528
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   529
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   530
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35043
diff changeset
   531
instance star :: (Rings.dvd) Rings.dvd ..
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27468
diff changeset
   532
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   533
instantiation star :: (Divides.div) Divides.div
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   534
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   535
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   536
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   537
  star_div_def:     "(op div) \<equiv> *f2* (op div)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   538
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   539
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   540
  star_mod_def:     "(op mod) \<equiv> *f2* (op mod)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   541
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   542
instance ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   543
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   544
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   545
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   546
instantiation star :: (ord) ord
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   547
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   548
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   549
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   550
  star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   551
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   552
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   553
  star_less_def:    "(op <) \<equiv> *p2* (op <)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   554
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   555
instance ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   556
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   557
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   558
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   559
lemmas star_class_defs [transfer_unfold] =
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   560
  star_zero_def     star_one_def
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   561
  star_add_def      star_diff_def     star_minus_def
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   562
  star_mult_def     star_divide_def   star_inverse_def
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   563
  star_le_def       star_less_def     star_abs_def       star_sgn_def
30968
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   564
  star_div_def      star_mod_def
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   565
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   566
text {* Class operations preserve standard elements *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   567
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   568
lemma Standard_zero: "0 \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   569
by (simp add: star_zero_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   570
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   571
lemma Standard_one: "1 \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   572
by (simp add: star_one_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   573
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   574
lemma Standard_add: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x + y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   575
by (simp add: star_add_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   576
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   577
lemma Standard_diff: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x - y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   578
by (simp add: star_diff_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   579
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   580
lemma Standard_minus: "x \<in> Standard \<Longrightarrow> - x \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   581
by (simp add: star_minus_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   582
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   583
lemma Standard_mult: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x * y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   584
by (simp add: star_mult_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   585
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   586
lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x / y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   587
by (simp add: star_divide_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   588
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   589
lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   590
by (simp add: star_inverse_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   591
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   592
lemma Standard_abs: "x \<in> Standard \<Longrightarrow> abs x \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   593
by (simp add: star_abs_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   594
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   595
lemma Standard_div: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x div y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   596
by (simp add: star_div_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   597
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   598
lemma Standard_mod: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x mod y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   599
by (simp add: star_mod_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   600
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   601
lemmas Standard_simps [simp] =
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   602
  Standard_zero  Standard_one
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   603
  Standard_add  Standard_diff  Standard_minus
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   604
  Standard_mult  Standard_divide  Standard_inverse
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   605
  Standard_abs  Standard_div  Standard_mod
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   606
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   607
text {* @{term star_of} preserves class operations *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   608
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   609
lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   610
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   611
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   612
lemma star_of_diff: "star_of (x - y) = star_of x - star_of y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   613
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   614
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   615
lemma star_of_minus: "star_of (-x) = - star_of x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   616
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   617
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   618
lemma star_of_mult: "star_of (x * y) = star_of x * star_of y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   619
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   620
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   621
lemma star_of_divide: "star_of (x / y) = star_of x / star_of y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   622
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   623
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   624
lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   625
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   626
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   627
lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   628
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   629
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   630
lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   631
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   632
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   633
lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   634
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   635
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   636
text {* @{term star_of} preserves numerals *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   637
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   638
lemma star_of_zero: "star_of 0 = 0"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   639
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   640
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   641
lemma star_of_one: "star_of 1 = 1"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   642
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   643
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   644
text {* @{term star_of} preserves orderings *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   645
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   646
lemma star_of_less: "(star_of x < star_of y) = (x < y)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   647
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   648
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   649
lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   650
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   651
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   652
lemma star_of_eq: "(star_of x = star_of y) = (x = y)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   653
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   654
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   655
text{*As above, for 0*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   656
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   657
lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   658
lemmas star_of_0_le   = star_of_le   [of 0, simplified star_of_zero]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   659
lemmas star_of_0_eq   = star_of_eq   [of 0, simplified star_of_zero]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   660
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   661
lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   662
lemmas star_of_le_0   = star_of_le   [of _ 0, simplified star_of_zero]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   663
lemmas star_of_eq_0   = star_of_eq   [of _ 0, simplified star_of_zero]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   664
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   665
text{*As above, for 1*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   666
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   667
lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   668
lemmas star_of_1_le   = star_of_le   [of 1, simplified star_of_one]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   669
lemmas star_of_1_eq   = star_of_eq   [of 1, simplified star_of_one]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   670
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   671
lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   672
lemmas star_of_le_1   = star_of_le   [of _ 1, simplified star_of_one]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   673
lemmas star_of_eq_1   = star_of_eq   [of _ 1, simplified star_of_one]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   674
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   675
lemmas star_of_simps [simp] =
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   676
  star_of_add     star_of_diff    star_of_minus
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   677
  star_of_mult    star_of_divide  star_of_inverse
30968
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   678
  star_of_div     star_of_mod     star_of_abs
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   679
  star_of_zero    star_of_one
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   680
  star_of_less    star_of_le      star_of_eq
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   681
  star_of_0_less  star_of_0_le    star_of_0_eq
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   682
  star_of_less_0  star_of_le_0    star_of_eq_0
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   683
  star_of_1_less  star_of_1_le    star_of_1_eq
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   684
  star_of_less_1  star_of_le_1    star_of_eq_1
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   685
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   686
subsection {* Ordering and lattice classes *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   687
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   688
instance star :: (order) order
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   689
apply (intro_classes)
27682
25aceefd4786 added class preorder
haftmann
parents: 27651
diff changeset
   690
apply (transfer, rule less_le_not_le)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   691
apply (transfer, rule order_refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   692
apply (transfer, erule (1) order_trans)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   693
apply (transfer, erule (1) order_antisym)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   694
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   695
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   696
instantiation star :: (semilattice_inf) semilattice_inf
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   697
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   698
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   699
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   700
  star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   701
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   702
instance
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   703
  by default (transfer star_inf_def, auto)+
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   704
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   705
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   706
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   707
instantiation star :: (semilattice_sup) semilattice_sup
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   708
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   709
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   710
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   711
  star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   712
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   713
instance
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   714
  by default (transfer star_sup_def, auto)+
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   715
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   716
end
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   717
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   718
instance star :: (lattice) lattice ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   719
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   720
instance star :: (distrib_lattice) distrib_lattice
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   721
  by default (transfer, auto simp add: sup_inf_distrib1)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   722
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   723
lemma Standard_inf [simp]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   724
  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   725
by (simp add: star_inf_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   726
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   727
lemma Standard_sup [simp]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   728
  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   729
by (simp add: star_sup_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   730
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   731
lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   732
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   733
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   734
lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   735
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   736
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   737
instance star :: (linorder) linorder
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   738
by (intro_classes, transfer, rule linorder_linear)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   739
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   740
lemma star_max_def [transfer_unfold]: "max = *f2* max"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   741
apply (rule ext, rule ext)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   742
apply (unfold max_def, transfer, fold max_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   743
apply (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   744
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   745
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   746
lemma star_min_def [transfer_unfold]: "min = *f2* min"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   747
apply (rule ext, rule ext)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   748
apply (unfold min_def, transfer, fold min_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   749
apply (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   750
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   751
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   752
lemma Standard_max [simp]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   753
  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> max x y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   754
by (simp add: star_max_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   755
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   756
lemma Standard_min [simp]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   757
  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> min x y \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   758
by (simp add: star_min_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   759
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   760
lemma star_of_max [simp]: "star_of (max x y) = max (star_of x) (star_of y)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   761
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   762
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   763
lemma star_of_min [simp]: "star_of (min x y) = min (star_of x) (star_of y)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   764
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   765
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   766
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   767
subsection {* Ordered group classes *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   768
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   769
instance star :: (semigroup_add) semigroup_add
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   770
by (intro_classes, transfer, rule add_assoc)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   771
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   772
instance star :: (ab_semigroup_add) ab_semigroup_add
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   773
by (intro_classes, transfer, rule add_commute)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   774
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   775
instance star :: (semigroup_mult) semigroup_mult
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   776
by (intro_classes, transfer, rule mult_assoc)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   777
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   778
instance star :: (ab_semigroup_mult) ab_semigroup_mult
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   779
by (intro_classes, transfer, rule mult_commute)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   780
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   781
instance star :: (comm_monoid_add) comm_monoid_add
28059
295a8fc92684 fixed names of class assumptions
haftmann
parents: 27682
diff changeset
   782
by (intro_classes, transfer, rule comm_monoid_add_class.add_0)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   783
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   784
instance star :: (monoid_mult) monoid_mult
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   785
apply (intro_classes)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   786
apply (transfer, rule mult_1_left)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   787
apply (transfer, rule mult_1_right)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   788
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   789
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   790
instance star :: (comm_monoid_mult) comm_monoid_mult
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   791
by (intro_classes, transfer, rule mult_1)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   792
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   793
instance star :: (cancel_semigroup_add) cancel_semigroup_add
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   794
apply (intro_classes)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   795
apply (transfer, erule add_left_imp_eq)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   796
apply (transfer, erule add_right_imp_eq)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   797
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   798
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   799
instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   800
by (intro_classes, transfer, rule add_imp_eq)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   801
29904
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29234
diff changeset
   802
instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29234
diff changeset
   803
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   804
instance star :: (ab_group_add) ab_group_add
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   805
apply (intro_classes)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   806
apply (transfer, rule left_minus)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   807
apply (transfer, rule diff_minus)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   808
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   809
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   810
instance star :: (ordered_ab_semigroup_add) ordered_ab_semigroup_add
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   811
by (intro_classes, transfer, rule add_left_mono)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   812
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   813
instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   814
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   815
instance star :: (ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   816
by (intro_classes, transfer, rule add_le_imp_le_left)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   817
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   818
instance star :: (ordered_comm_monoid_add) ordered_comm_monoid_add ..
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   819
instance star :: (ordered_ab_group_add) ordered_ab_group_add ..
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   820
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   821
instance star :: (ordered_ab_group_add_abs) ordered_ab_group_add_abs 
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   822
  by intro_classes (transfer,
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   823
    simp add: abs_ge_self abs_leI abs_triangle_ineq)+
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   824
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   825
instance star :: (linordered_cancel_ab_semigroup_add) linordered_cancel_ab_semigroup_add ..
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   826
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   827
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   828
subsection {* Ring and field classes *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   829
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   830
instance star :: (semiring) semiring
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   831
apply (intro_classes)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   832
apply (transfer, rule left_distrib)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   833
apply (transfer, rule right_distrib)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   834
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   835
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   836
instance star :: (semiring_0) semiring_0 
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   837
by intro_classes (transfer, simp)+
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   838
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   839
instance star :: (semiring_0_cancel) semiring_0_cancel ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   840
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   841
instance star :: (comm_semiring) comm_semiring 
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   842
by (intro_classes, transfer, rule left_distrib)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   843
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   844
instance star :: (comm_semiring_0) comm_semiring_0 ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   845
instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   846
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   847
instance star :: (zero_neq_one) zero_neq_one
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   848
by (intro_classes, transfer, rule zero_neq_one)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   849
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   850
instance star :: (semiring_1) semiring_1 ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   851
instance star :: (comm_semiring_1) comm_semiring_1 ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   852
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   853
instance star :: (no_zero_divisors) no_zero_divisors
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   854
by (intro_classes, transfer, rule no_zero_divisors)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   855
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   856
instance star :: (semiring_1_cancel) semiring_1_cancel ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   857
instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   858
instance star :: (ring) ring ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   859
instance star :: (comm_ring) comm_ring ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   860
instance star :: (ring_1) ring_1 ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   861
instance star :: (comm_ring_1) comm_ring_1 ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   862
instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   863
instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   864
instance star :: (idom) idom .. 
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   865
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   866
instance star :: (division_ring) division_ring
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   867
apply (intro_classes)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   868
apply (transfer, erule left_inverse)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   869
apply (transfer, erule right_inverse)
35083
3246e66b0874 division ring assumes divide_inverse
haftmann
parents: 35050
diff changeset
   870
apply (transfer, fact divide_inverse)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   871
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   872
36412
9245942dcc5b instances for *_inverse_zero classes
haftmann
parents: 36349
diff changeset
   873
instance star :: (division_ring_inverse_zero) division_ring_inverse_zero
9245942dcc5b instances for *_inverse_zero classes
haftmann
parents: 36349
diff changeset
   874
by (intro_classes, transfer, rule inverse_zero)
9245942dcc5b instances for *_inverse_zero classes
haftmann
parents: 36349
diff changeset
   875
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   876
instance star :: (field) field
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   877
apply (intro_classes)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   878
apply (transfer, erule left_inverse)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   879
apply (transfer, rule divide_inverse)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   880
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   881
36412
9245942dcc5b instances for *_inverse_zero classes
haftmann
parents: 36349
diff changeset
   882
instance star :: (field_inverse_zero) field_inverse_zero
9245942dcc5b instances for *_inverse_zero classes
haftmann
parents: 36349
diff changeset
   883
apply intro_classes
9245942dcc5b instances for *_inverse_zero classes
haftmann
parents: 36349
diff changeset
   884
apply (rule inverse_zero)
9245942dcc5b instances for *_inverse_zero classes
haftmann
parents: 36349
diff changeset
   885
done
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   886
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   887
instance star :: (ordered_semiring) ordered_semiring
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   888
apply (intro_classes)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   889
apply (transfer, erule (1) mult_left_mono)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   890
apply (transfer, erule (1) mult_right_mono)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   891
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   892
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   893
instance star :: (ordered_cancel_semiring) ordered_cancel_semiring ..
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   894
35043
07dbdf60d5ad dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents: 35035
diff changeset
   895
instance star :: (linordered_semiring_strict) linordered_semiring_strict
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   896
apply (intro_classes)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   897
apply (transfer, erule (1) mult_strict_left_mono)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   898
apply (transfer, erule (1) mult_strict_right_mono)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   899
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   900
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   901
instance star :: (ordered_comm_semiring) ordered_comm_semiring
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 38621
diff changeset
   902
by (intro_classes, transfer, rule mult_left_mono)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   903
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   904
instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   905
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   906
instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 38621
diff changeset
   907
by (intro_classes, transfer, rule mult_strict_left_mono)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   908
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   909
instance star :: (ordered_ring) ordered_ring ..
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   910
instance star :: (ordered_ring_abs) ordered_ring_abs
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   911
  by intro_classes  (transfer, rule abs_eq_mult)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   912
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   913
instance star :: (abs_if) abs_if
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   914
by (intro_classes, transfer, rule abs_if)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   915
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   916
instance star :: (sgn_if) sgn_if
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   917
by (intro_classes, transfer, rule sgn_if)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   918
35043
07dbdf60d5ad dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents: 35035
diff changeset
   919
instance star :: (linordered_ring_strict) linordered_ring_strict ..
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   920
instance star :: (ordered_comm_ring) ordered_comm_ring ..
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   921
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   922
instance star :: (linordered_semidom) linordered_semidom
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   923
by (intro_classes, transfer, rule zero_less_one)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   924
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   925
instance star :: (linordered_idom) linordered_idom ..
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 31021
diff changeset
   926
instance star :: (linordered_field) linordered_field ..
36414
a19ba9bbc8dc tuned class linordered_field_inverse_zero
haftmann
parents: 36412
diff changeset
   927
instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero ..
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   928
30968
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   929
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   930
subsection {* Power *}
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   931
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   932
lemma star_power_def [transfer_unfold]:
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   933
  "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   934
proof (rule eq_reflection, rule ext, rule ext)
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   935
  fix n :: nat
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   936
  show "\<And>x::'a star. x ^ n = ( *f* (\<lambda>x. x ^ n)) x" 
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   937
  proof (induct n)
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   938
    case 0
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   939
    have "\<And>x::'a star. ( *f* (\<lambda>x. 1)) x = 1"
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   940
      by transfer simp
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   941
    then show ?case by simp
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   942
  next
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   943
    case (Suc n)
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   944
    have "\<And>x::'a star. x * ( *f* (\<lambda>x\<Colon>'a. x ^ n)) x = ( *f* (\<lambda>x\<Colon>'a. x * x ^ n)) x"
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   945
      by transfer simp
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   946
    with Suc show ?case by simp
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   947
  qed
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   948
qed
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   949
30968
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   950
lemma Standard_power [simp]: "x \<in> Standard \<Longrightarrow> x ^ n \<in> Standard"
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   951
  by (simp add: star_power_def)
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   952
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   953
lemma star_of_power [simp]: "star_of (x ^ n) = star_of x ^ n"
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   954
  by transfer (rule refl)
10fef94f40fc adaptions due to rearrangment of power operation
haftmann
parents: 30729
diff changeset
   955
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   956
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   957
subsection {* Number classes *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   958
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   959
instance star :: (numeral) numeral ..
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   960
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   961
lemma star_numeral_def [transfer_unfold]:
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   962
  "numeral k = star_of (numeral k)"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   963
by (induct k, simp_all only: numeral.simps star_of_one star_of_add)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   964
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   965
lemma Standard_numeral [simp]: "numeral k \<in> Standard"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   966
by (simp add: star_numeral_def)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   967
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   968
lemma star_of_numeral [simp]: "star_of (numeral k) = numeral k"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   969
by transfer (rule refl)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   970
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   971
lemma star_neg_numeral_def [transfer_unfold]:
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   972
  "neg_numeral k = star_of (neg_numeral k)"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   973
by (simp only: neg_numeral_def star_of_minus star_of_numeral)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   974
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   975
lemma Standard_neg_numeral [simp]: "neg_numeral k \<in> Standard"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   976
by (simp add: star_neg_numeral_def)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   977
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   978
lemma star_of_neg_numeral [simp]: "star_of (neg_numeral k) = neg_numeral k"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   979
by transfer (rule refl)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   980
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   981
lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   982
by (induct n, simp_all)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   983
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   984
lemmas star_of_compare_numeral [simp] =
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   985
  star_of_less [of "numeral k", simplified star_of_numeral]
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   986
  star_of_le   [of "numeral k", simplified star_of_numeral]
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   987
  star_of_eq   [of "numeral k", simplified star_of_numeral]
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   988
  star_of_less [of _ "numeral k", simplified star_of_numeral]
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   989
  star_of_le   [of _ "numeral k", simplified star_of_numeral]
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   990
  star_of_eq   [of _ "numeral k", simplified star_of_numeral]
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   991
  star_of_less [of "neg_numeral k", simplified star_of_numeral]
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   992
  star_of_le   [of "neg_numeral k", simplified star_of_numeral]
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   993
  star_of_eq   [of "neg_numeral k", simplified star_of_numeral]
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   994
  star_of_less [of _ "neg_numeral k", simplified star_of_numeral]
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   995
  star_of_le   [of _ "neg_numeral k", simplified star_of_numeral]
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   996
  star_of_eq   [of _ "neg_numeral k", simplified star_of_numeral] for k
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46008
diff changeset
   997
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   998
lemma Standard_of_nat [simp]: "of_nat n \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   999
by (simp add: star_of_nat_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1000
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1001
lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1002
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1003
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1004
lemma star_of_int_def [transfer_unfold]: "of_int z = star_of (of_int z)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1005
by (rule_tac z=z in int_diff_cases, simp)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1006
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1007
lemma Standard_of_int [simp]: "of_int z \<in> Standard"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1008
by (simp add: star_of_int_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1009
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1010
lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1011
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1012
38621
d6cb7e625d75 more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents: 37765
diff changeset
  1013
instance star :: (semiring_char_0) semiring_char_0 proof
d6cb7e625d75 more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents: 37765
diff changeset
  1014
  have "inj (star_of :: 'a \<Rightarrow> 'a star)" by (rule injI) simp
d6cb7e625d75 more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents: 37765
diff changeset
  1015
  then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" using inj_of_nat by (rule inj_comp)
d6cb7e625d75 more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents: 37765
diff changeset
  1016
  then show "inj (of_nat :: nat \<Rightarrow> 'a star)" by (simp add: comp_def)
d6cb7e625d75 more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents: 37765
diff changeset
  1017
qed
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1018
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1019
instance star :: (ring_char_0) ring_char_0 ..
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1020
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1021
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1022
subsection {* Finite class *}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1023
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1024
lemma starset_finite: "finite A \<Longrightarrow> *s* A = star_of ` A"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1025
by (erule finite_induct, simp_all)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1026
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1027
instance star :: (finite) finite
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1028
apply (intro_classes)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1029
apply (subst starset_UNIV [symmetric])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1030
apply (subst starset_finite [OF finite])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1031
apply (rule finite_imageI [OF finite])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1032
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1033
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
  1034
end