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