src/HOL/NSA/StarDef.thy
changeset 60041 6c86d58ab0ca
parent 60036 218fcc645d22
child 60352 d46de31a50c4
     1.1 --- a/src/HOL/NSA/StarDef.thy	Sun Apr 12 11:34:09 2015 +0200
     1.2 +++ b/src/HOL/NSA/StarDef.thy	Sun Apr 12 11:34:16 2015 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  subsection {* A Free Ultrafilter over the Naturals *}
     1.5  
     1.6  definition
     1.7 -  FreeUltrafilterNat :: "nat set set"  ("\<U>") where
     1.8 +  FreeUltrafilterNat :: "nat filter"  ("\<U>") where
     1.9    "\<U> = (SOME U. freeultrafilter U)"
    1.10  
    1.11  lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
    1.12 @@ -24,19 +24,11 @@
    1.13  interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat
    1.14  by (rule freeultrafilter_FreeUltrafilterNat)
    1.15  
    1.16 -text {* This rule takes the place of the old ultra tactic *}
    1.17 -
    1.18 -lemma ultra:
    1.19 -  "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>"
    1.20 -by (simp add: Collect_imp_eq
    1.21 -    FreeUltrafilterNat.Un_iff FreeUltrafilterNat.Compl_iff)
    1.22 -
    1.23 -
    1.24  subsection {* Definition of @{text star} type constructor *}
    1.25  
    1.26  definition
    1.27    starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where
    1.28 -  "starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}"
    1.29 +  "starrel = {(X,Y). eventually (\<lambda>n. X n = Y n) \<U>}"
    1.30  
    1.31  definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
    1.32  
    1.33 @@ -59,14 +51,14 @@
    1.34  
    1.35  text {* Proving that @{term starrel} is an equivalence relation *}
    1.36  
    1.37 -lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)"
    1.38 +lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = (eventually (\<lambda>n. X n = Y n) \<U>)"
    1.39  by (simp add: starrel_def)
    1.40  
    1.41  lemma equiv_starrel: "equiv UNIV starrel"
    1.42  proof (rule equivI)
    1.43    show "refl starrel" by (simp add: refl_on_def)
    1.44    show "sym starrel" by (simp add: sym_def eq_commute)
    1.45 -  show "trans starrel" by (auto intro: transI elim!: ultra)
    1.46 +  show "trans starrel" by (intro transI) (auto elim: eventually_elim2)
    1.47  qed
    1.48  
    1.49  lemmas equiv_starrel_iff =
    1.50 @@ -75,7 +67,7 @@
    1.51  lemma starrel_in_star: "starrel``{x} \<in> star"
    1.52  by (simp add: star_def quotientI)
    1.53  
    1.54 -lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)"
    1.55 +lemma star_n_eq_iff: "(star_n X = star_n Y) = (eventually (\<lambda>n. X n = Y n) \<U>)"
    1.56  by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff)
    1.57  
    1.58  
    1.59 @@ -83,8 +75,8 @@
    1.60  
    1.61  text {* This introduction rule starts each transfer proof. *}
    1.62  lemma transfer_start:
    1.63 -  "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
    1.64 -by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
    1.65 +  "P \<equiv> eventually (\<lambda>n. Q) \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
    1.66 +  by (simp add: FreeUltrafilterNat.proper)
    1.67  
    1.68  text {*Initialize transfer tactic.*}
    1.69  ML_file "transfer.ML"
    1.70 @@ -98,66 +90,66 @@
    1.71  text {* Transfer introduction rules. *}
    1.72  
    1.73  lemma transfer_ex [transfer_intro]:
    1.74 -  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
    1.75 -    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
    1.76 -by (simp only: ex_star_eq FreeUltrafilterNat.Collect_ex)
    1.77 +  "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
    1.78 +    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> eventually (\<lambda>n. \<exists>x. P n x) \<U>"
    1.79 +by (simp only: ex_star_eq eventually_ex)
    1.80  
    1.81  lemma transfer_all [transfer_intro]:
    1.82 -  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
    1.83 -    \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
    1.84 -by (simp only: all_star_eq FreeUltrafilterNat.Collect_all)
    1.85 +  "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
    1.86 +    \<Longrightarrow> \<forall>x::'a star. p x \<equiv> eventually (\<lambda>n. \<forall>x. P n x) \<U>"
    1.87 +by (simp only: all_star_eq FreeUltrafilterNat.eventually_all_iff)
    1.88  
    1.89  lemma transfer_not [transfer_intro]:
    1.90 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
    1.91 -by (simp only: FreeUltrafilterNat.Collect_not)
    1.92 +  "\<lbrakk>p \<equiv> eventually P \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> eventually (\<lambda>n. \<not> P n) \<U>"
    1.93 +by (simp only: FreeUltrafilterNat.eventually_not_iff)
    1.94  
    1.95  lemma transfer_conj [transfer_intro]:
    1.96 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
    1.97 -    \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
    1.98 -by (simp only: FreeUltrafilterNat.Collect_conj)
    1.99 +  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
   1.100 +    \<Longrightarrow> p \<and> q \<equiv> eventually (\<lambda>n. P n \<and> Q n) \<U>"
   1.101 +by (simp only: eventually_conj_iff)
   1.102  
   1.103  lemma transfer_disj [transfer_intro]:
   1.104 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   1.105 -    \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
   1.106 -by (simp only: FreeUltrafilterNat.Collect_disj)
   1.107 +  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
   1.108 +    \<Longrightarrow> p \<or> q \<equiv> eventually (\<lambda>n. P n \<or> Q n) \<U>"
   1.109 +by (simp only: FreeUltrafilterNat.eventually_disj_iff)
   1.110  
   1.111  lemma transfer_imp [transfer_intro]:
   1.112 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   1.113 -    \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
   1.114 -by (simp only: imp_conv_disj transfer_disj transfer_not)
   1.115 +  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
   1.116 +    \<Longrightarrow> p \<longrightarrow> q \<equiv> eventually (\<lambda>n. P n \<longrightarrow> Q n) \<U>"
   1.117 +by (simp only: FreeUltrafilterNat.eventually_imp_iff)
   1.118  
   1.119  lemma transfer_iff [transfer_intro]:
   1.120 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   1.121 -    \<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
   1.122 -by (simp only: iff_conv_conj_imp transfer_conj transfer_imp)
   1.123 +  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
   1.124 +    \<Longrightarrow> p = q \<equiv> eventually (\<lambda>n. P n = Q n) \<U>"
   1.125 +by (simp only: FreeUltrafilterNat.eventually_iff_iff)
   1.126  
   1.127  lemma transfer_if_bool [transfer_intro]:
   1.128 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
   1.129 -    \<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
   1.130 +  "\<lbrakk>p \<equiv> eventually P \<U>; x \<equiv> eventually X \<U>; y \<equiv> eventually Y \<U>\<rbrakk>
   1.131 +    \<Longrightarrow> (if p then x else y) \<equiv> eventually (\<lambda>n. if P n then X n else Y n) \<U>"
   1.132  by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
   1.133  
   1.134  lemma transfer_eq [transfer_intro]:
   1.135 -  "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
   1.136 +  "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> eventually (\<lambda>n. X n = Y n) \<U>"
   1.137  by (simp only: star_n_eq_iff)
   1.138  
   1.139  lemma transfer_if [transfer_intro]:
   1.140 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
   1.141 +  "\<lbrakk>p \<equiv> eventually (\<lambda>n. P n) \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
   1.142      \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
   1.143  apply (rule eq_reflection)
   1.144 -apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
   1.145 +apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_elim1)
   1.146  done
   1.147  
   1.148  lemma transfer_fun_eq [transfer_intro]:
   1.149    "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
   1.150 -    \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
   1.151 -      \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
   1.152 +    \<equiv> eventually (\<lambda>n. F n (X n) = G n (X n)) \<U>\<rbrakk>
   1.153 +      \<Longrightarrow> f = g \<equiv> eventually (\<lambda>n. F n = G n) \<U>"
   1.154  by (simp only: fun_eq_iff transfer_all)
   1.155  
   1.156  lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)"
   1.157  by (rule reflexive)
   1.158  
   1.159 -lemma transfer_bool [transfer_intro]: "p \<equiv> {n. p} \<in> \<U>"
   1.160 -by (simp add: atomize_eq)
   1.161 +lemma transfer_bool [transfer_intro]: "p \<equiv> eventually (\<lambda>n. p) \<U>"
   1.162 +by (simp add: FreeUltrafilterNat.proper)
   1.163  
   1.164  
   1.165  subsection {* Standard elements *}
   1.166 @@ -191,7 +183,7 @@
   1.167  
   1.168  lemma Ifun_congruent2:
   1.169    "congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})"
   1.170 -by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra)
   1.171 +by (auto simp add: congruent2_def equiv_starrel_iff elim!: eventually_rev_mp)
   1.172  
   1.173  lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
   1.174  by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
   1.175 @@ -298,7 +290,7 @@
   1.176  definition unstar :: "bool star \<Rightarrow> bool" where
   1.177    "unstar b \<longleftrightarrow> b = star_of True"
   1.178  
   1.179 -lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
   1.180 +lemma unstar_star_n: "unstar (star_n P) = (eventually P \<U>)"
   1.181  by (simp add: unstar_def star_of_def star_n_eq_iff)
   1.182  
   1.183  lemma unstar_star_of [simp]: "unstar (star_of p) = p"
   1.184 @@ -308,7 +300,7 @@
   1.185  setup {* Transfer_Principle.add_const @{const_name unstar} *}
   1.186  
   1.187  lemma transfer_unstar [transfer_intro]:
   1.188 -  "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
   1.189 +  "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> eventually P \<U>"
   1.190  by (simp only: unstar_star_n)
   1.191  
   1.192  definition
   1.193 @@ -322,11 +314,11 @@
   1.194  declare starP_def [transfer_unfold]
   1.195  declare starP2_def [transfer_unfold]
   1.196  
   1.197 -lemma starP_star_n: "( *p* P) (star_n X) = ({n. P (X n)} \<in> \<U>)"
   1.198 +lemma starP_star_n: "( *p* P) (star_n X) = (eventually (\<lambda>n. P (X n)) \<U>)"
   1.199  by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n)
   1.200  
   1.201  lemma starP2_star_n:
   1.202 -  "( *p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} \<in> \<U>)"
   1.203 +  "( *p2* P) (star_n X) (star_n Y) = (eventually (\<lambda>n. P (X n) (Y n)) \<U>)"
   1.204  by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n)
   1.205  
   1.206  lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x"
   1.207 @@ -343,7 +335,7 @@
   1.208    "Iset A = {x. ( *p2* op \<in>) x A}"
   1.209  
   1.210  lemma Iset_star_n:
   1.211 -  "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
   1.212 +  "(star_n X \<in> Iset (star_n A)) = (eventually (\<lambda>n. X n \<in> A n) \<U>)"
   1.213  by (simp add: Iset_def starP2_star_n)
   1.214  
   1.215  text {* Transfer tactic should remove occurrences of @{term Iset} *}
   1.216 @@ -351,27 +343,27 @@
   1.217  
   1.218  lemma transfer_mem [transfer_intro]:
   1.219    "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
   1.220 -    \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
   1.221 +    \<Longrightarrow> x \<in> a \<equiv> eventually (\<lambda>n. X n \<in> A n) \<U>"
   1.222  by (simp only: Iset_star_n)
   1.223  
   1.224  lemma transfer_Collect [transfer_intro]:
   1.225 -  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
   1.226 +  "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
   1.227      \<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
   1.228  by (simp add: atomize_eq set_eq_iff all_star_eq Iset_star_n)
   1.229  
   1.230  lemma transfer_set_eq [transfer_intro]:
   1.231    "\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
   1.232 -    \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
   1.233 +    \<Longrightarrow> a = b \<equiv> eventually (\<lambda>n. A n = B n) \<U>"
   1.234  by (simp only: set_eq_iff transfer_all transfer_iff transfer_mem)
   1.235  
   1.236  lemma transfer_ball [transfer_intro]:
   1.237 -  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
   1.238 -    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>"
   1.239 +  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
   1.240 +    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> eventually (\<lambda>n. \<forall>x\<in>A n. P n x) \<U>"
   1.241  by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
   1.242  
   1.243  lemma transfer_bex [transfer_intro]:
   1.244 -  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
   1.245 -    \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
   1.246 +  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
   1.247 +    \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> eventually (\<lambda>n. \<exists>x\<in>A n. P n x) \<U>"
   1.248  by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
   1.249  
   1.250  lemma transfer_Iset [transfer_intro]: