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.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.108
1.110 @@ -422,7 +422,7 @@
1.111         intrel `` {<x1#+x2, y1#+y2>}"
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.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.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)
```