src/ZF/Int_ZF.thy
changeset 46820 c656222c4dc1
parent 45602 2a858377c3d2
child 46821 ff6b0c1087f2
     1.1 --- a/src/ZF/Int_ZF.thy	Sun Mar 04 23:20:43 2012 +0100
     1.2 +++ b/src/ZF/Int_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  definition
     1.6    intrel :: i  where
     1.7 -    "intrel == {p : (nat*nat)*(nat*nat).                 
     1.8 +    "intrel == {p \<in> (nat*nat)*(nat*nat).                 
     1.9                  \<exists>x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    1.10  
    1.11  definition
    1.12 @@ -22,7 +22,7 @@
    1.13  
    1.14  definition
    1.15    intify :: "i=>i" --{*coercion from ANYTHING to int*}  where
    1.16 -    "intify(m) == if m : int then m else $#0"
    1.17 +    "intify(m) == if m \<in> int then m else $#0"
    1.18  
    1.19  definition
    1.20    raw_zminus :: "i=>i"  where
    1.21 @@ -135,7 +135,7 @@
    1.22  apply (fast elim!: sym int_trans_lemma)
    1.23  done
    1.24  
    1.25 -lemma image_intrel_int: "[| m\<in>nat; n\<in>nat |] ==> intrel `` {<m,n>} : int"
    1.26 +lemma image_intrel_int: "[| m\<in>nat; n\<in>nat |] ==> intrel `` {<m,n>} \<in> int"
    1.27  by (simp add: int_def)
    1.28  
    1.29  declare equiv_intrel [THEN eq_equiv_class_iff, simp]
    1.30 @@ -145,7 +145,7 @@
    1.31  
    1.32  (** int_of: the injection from nat to int **)
    1.33  
    1.34 -lemma int_of_type [simp,TC]: "$#m : int"
    1.35 +lemma int_of_type [simp,TC]: "$#m \<in> int"
    1.36  by (simp add: int_def quotient_def int_of_def, auto)
    1.37  
    1.38  lemma int_of_eq [iff]: "($# m = $# n) <-> natify(m)=natify(n)"
    1.39 @@ -157,10 +157,10 @@
    1.40  
    1.41  (** intify: coercion from anything to int **)
    1.42  
    1.43 -lemma intify_in_int [iff,TC]: "intify(x) : int"
    1.44 +lemma intify_in_int [iff,TC]: "intify(x) \<in> int"
    1.45  by (simp add: intify_def)
    1.46  
    1.47 -lemma intify_ident [simp]: "n : int ==> intify(n) = n"
    1.48 +lemma intify_ident [simp]: "n \<in> int ==> intify(n) = n"
    1.49  by (simp add: intify_def)
    1.50  
    1.51  
    1.52 @@ -220,12 +220,12 @@
    1.53  lemma zminus_congruent: "(%<x,y>. intrel``{<y,x>}) respects intrel"
    1.54  by (auto simp add: congruent_def add_ac)
    1.55  
    1.56 -lemma raw_zminus_type: "z : int ==> raw_zminus(z) : int"
    1.57 +lemma raw_zminus_type: "z \<in> int ==> raw_zminus(z) \<in> int"
    1.58  apply (simp add: int_def raw_zminus_def)
    1.59  apply (typecheck add: UN_equiv_class_type [OF equiv_intrel zminus_congruent])
    1.60  done
    1.61  
    1.62 -lemma zminus_type [TC,iff]: "$-z : int"
    1.63 +lemma zminus_type [TC,iff]: "$-z \<in> int"
    1.64  by (simp add: zminus_def raw_zminus_type)
    1.65  
    1.66  lemma raw_zminus_inject: 
    1.67 @@ -253,7 +253,7 @@
    1.68       ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}"
    1.69  by (simp add: zminus_def raw_zminus image_intrel_int)
    1.70  
    1.71 -lemma raw_zminus_zminus: "z : int ==> raw_zminus (raw_zminus(z)) = z"
    1.72 +lemma raw_zminus_zminus: "z \<in> int ==> raw_zminus (raw_zminus(z)) = z"
    1.73  by (auto simp add: int_def raw_zminus)
    1.74  
    1.75  lemma zminus_zminus_intify [simp]: "$- ($- z) = intify(z)"
    1.76 @@ -262,7 +262,7 @@
    1.77  lemma zminus_int0 [simp]: "$- ($#0) = $#0"
    1.78  by (simp add: int_of_def zminus)
    1.79  
    1.80 -lemma zminus_zminus: "z : int ==> $- ($- z) = z"
    1.81 +lemma zminus_zminus: "z \<in> int ==> $- ($- z) = z"
    1.82  by simp
    1.83  
    1.84  
    1.85 @@ -352,7 +352,7 @@
    1.86       "[| znegative(z); z: int |] ==> $# (zmagnitude(z)) = $- z"
    1.87  by (drule zneg_int_of, auto)
    1.88  
    1.89 -lemma int_cases: "z : int ==> \<exists>n\<in>nat. z = $# n | z = $- ($# succ(n))"
    1.90 +lemma int_cases: "z \<in> int ==> \<exists>n\<in>nat. z = $# n | z = $- ($# succ(n))"
    1.91  apply (case_tac "znegative (z) ")
    1.92  prefer 2 apply (blast dest: not_zneg_mag sym)
    1.93  apply (blast dest: zneg_int_of)
    1.94 @@ -398,13 +398,13 @@
    1.95  apply (simp (no_asm_simp) add: add_assoc [symmetric])
    1.96  done
    1.97  
    1.98 -lemma raw_zadd_type: "[| z: int;  w: int |] ==> raw_zadd(z,w) : int"
    1.99 +lemma raw_zadd_type: "[| z: int;  w: int |] ==> raw_zadd(z,w) \<in> int"
   1.100  apply (simp add: int_def raw_zadd_def)
   1.101  apply (rule UN_equiv_class_type2 [OF equiv_intrel zadd_congruent2], assumption+)
   1.102  apply (simp add: Let_def)
   1.103  done
   1.104  
   1.105 -lemma zadd_type [iff,TC]: "z $+ w : int"
   1.106 +lemma zadd_type [iff,TC]: "z $+ w \<in> int"
   1.107  by (simp add: zadd_def raw_zadd_type)
   1.108  
   1.109  lemma raw_zadd: 
   1.110 @@ -422,7 +422,7 @@
   1.111         intrel `` {<x1#+x2, y1#+y2>}"
   1.112  by (simp add: zadd_def raw_zadd image_intrel_int)
   1.113  
   1.114 -lemma raw_zadd_int0: "z : int ==> raw_zadd ($#0,z) = z"
   1.115 +lemma raw_zadd_int0: "z \<in> int ==> raw_zadd ($#0,z) = z"
   1.116  by (auto simp add: int_def int_of_def raw_zadd)
   1.117  
   1.118  lemma zadd_int0_intify [simp]: "$#0 $+ z = intify(z)"
   1.119 @@ -469,13 +469,13 @@
   1.120  by (simp add: int_of_add [symmetric] natify_succ)
   1.121  
   1.122  lemma int_of_diff: 
   1.123 -     "[| m\<in>nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)"
   1.124 +     "[| m\<in>nat;  n \<le> m |] ==> $# (m #- n) = ($#m) $- ($#n)"
   1.125  apply (simp add: int_of_def zdiff_def)
   1.126  apply (frule lt_nat_in_nat)
   1.127  apply (simp_all add: zadd zminus add_diff_inverse2)
   1.128  done
   1.129  
   1.130 -lemma raw_zadd_zminus_inverse: "z : int ==> raw_zadd (z, $- z) = $#0"
   1.131 +lemma raw_zadd_zminus_inverse: "z \<in> int ==> raw_zadd (z, $- z) = $#0"
   1.132  by (auto simp add: int_def int_of_def zminus raw_zadd add_commute)
   1.133  
   1.134  lemma zadd_zminus_inverse [simp]: "z $+ ($- z) = $#0"
   1.135 @@ -511,13 +511,13 @@
   1.136  done
   1.137  
   1.138  
   1.139 -lemma raw_zmult_type: "[| z: int;  w: int |] ==> raw_zmult(z,w) : int"
   1.140 +lemma raw_zmult_type: "[| z: int;  w: int |] ==> raw_zmult(z,w) \<in> int"
   1.141  apply (simp add: int_def raw_zmult_def)
   1.142  apply (rule UN_equiv_class_type2 [OF equiv_intrel zmult_congruent2], assumption+)
   1.143  apply (simp add: Let_def)
   1.144  done
   1.145  
   1.146 -lemma zmult_type [iff,TC]: "z $* w : int"
   1.147 +lemma zmult_type [iff,TC]: "z $* w \<in> int"
   1.148  by (simp add: zmult_def raw_zmult_type)
   1.149  
   1.150  lemma raw_zmult: 
   1.151 @@ -533,19 +533,19 @@
   1.152            intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
   1.153  by (simp add: zmult_def raw_zmult image_intrel_int)
   1.154  
   1.155 -lemma raw_zmult_int0: "z : int ==> raw_zmult ($#0,z) = $#0"
   1.156 +lemma raw_zmult_int0: "z \<in> int ==> raw_zmult ($#0,z) = $#0"
   1.157  by (auto simp add: int_def int_of_def raw_zmult)
   1.158  
   1.159  lemma zmult_int0 [simp]: "$#0 $* z = $#0"
   1.160  by (simp add: zmult_def raw_zmult_int0)
   1.161  
   1.162 -lemma raw_zmult_int1: "z : int ==> raw_zmult ($#1,z) = z"
   1.163 +lemma raw_zmult_int1: "z \<in> int ==> raw_zmult ($#1,z) = z"
   1.164  by (auto simp add: int_def int_of_def raw_zmult)
   1.165  
   1.166  lemma zmult_int1_intify [simp]: "$#1 $* z = intify(z)"
   1.167  by (simp add: zmult_def raw_zmult_int1)
   1.168  
   1.169 -lemma zmult_int1: "z : int ==> $#1 $* z = z"
   1.170 +lemma zmult_int1: "z \<in> int ==> $#1 $* z = z"
   1.171  by simp
   1.172  
   1.173  lemma raw_zmult_commute:
   1.174 @@ -603,7 +603,7 @@
   1.175  
   1.176  (*** Subtraction laws ***)
   1.177  
   1.178 -lemma zdiff_type [iff,TC]: "z $- w : int"
   1.179 +lemma zdiff_type [iff,TC]: "z $- w \<in> int"
   1.180  by (simp add: zdiff_def)
   1.181  
   1.182  lemma zminus_zdiff_eq [simp]: "$- (z $- y) = y $- z"
   1.183 @@ -644,10 +644,10 @@
   1.184  lemma zless_not_refl [iff]: "~ (z$<z)"
   1.185  by (auto simp add: zless_def znegative_def int_of_def zdiff_def)
   1.186  
   1.187 -lemma neq_iff_zless: "[| x: int; y: int |] ==> (x ~= y) <-> (x $< y | y $< x)"
   1.188 +lemma neq_iff_zless: "[| x: int; y: int |] ==> (x \<noteq> y) <-> (x $< y | y $< x)"
   1.189  by (cut_tac z = x and w = y in zless_linear, auto)
   1.190  
   1.191 -lemma zless_imp_intify_neq: "w $< z ==> intify(w) ~= intify(z)"
   1.192 +lemma zless_imp_intify_neq: "w $< z ==> intify(w) \<noteq> intify(z)"
   1.193  apply auto
   1.194  apply (subgoal_tac "~ (intify (w) $< intify (z))")
   1.195  apply (erule_tac [2] ssubst)
   1.196 @@ -672,7 +672,7 @@
   1.197  done
   1.198  
   1.199  lemma zless_succ_zadd_lemma: 
   1.200 -    "w : int ==> w $< w $+ $# succ(n)"
   1.201 +    "w \<in> int ==> w $< w $+ $# succ(n)"
   1.202  apply (simp add: zless_def znegative_def zdiff_def int_def)
   1.203  apply (auto simp add: zadd zminus int_of_def image_iff)
   1.204  apply (rule_tac x = 0 in exI, auto)
   1.205 @@ -695,7 +695,7 @@
   1.206  done
   1.207  
   1.208  lemma zless_trans_lemma: 
   1.209 -    "[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z"
   1.210 +    "[| x $< y; y $< z; x: int; y \<in> int; z: int |] ==> x $< z"
   1.211  apply (simp add: zless_def znegative_def zdiff_def int_def)
   1.212  apply (auto simp add: zadd zminus image_iff)
   1.213  apply (rename_tac x1 x2 y1 y2)