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