src/ZF/Int_ZF.thy
changeset 46821 ff6b0c1087f2
parent 46820 c656222c4dc1
child 46841 49b91b716cbe
     1.1 --- a/src/ZF/Int_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
     1.2 +++ b/src/ZF/Int_ZF.thy	Tue Mar 06 16:06:52 2012 +0000
     1.3 @@ -107,7 +107,7 @@
     1.4  (** Natural deduction for intrel **)
     1.5  
     1.6  lemma intrel_iff [simp]: 
     1.7 -    "<<x1,y1>,<x2,y2>>: intrel <->  
     1.8 +    "<<x1,y1>,<x2,y2>>: intrel \<longleftrightarrow>  
     1.9       x1\<in>nat & y1\<in>nat & x2\<in>nat & y2\<in>nat & x1#+y2 = x2#+y1"
    1.10  by (simp add: intrel_def)
    1.11  
    1.12 @@ -148,7 +148,7 @@
    1.13  lemma int_of_type [simp,TC]: "$#m \<in> int"
    1.14  by (simp add: int_def quotient_def int_of_def, auto)
    1.15  
    1.16 -lemma int_of_eq [iff]: "($# m = $# n) <-> natify(m)=natify(n)"
    1.17 +lemma int_of_eq [iff]: "($# m = $# n) \<longleftrightarrow> natify(m)=natify(n)"
    1.18  by (simp add: int_of_def)
    1.19  
    1.20  lemma int_of_inject: "[| $#m = $#n;  m\<in>nat;  n\<in>nat |] ==> m=n"
    1.21 @@ -202,16 +202,16 @@
    1.22  
    1.23  (** Orderings **)
    1.24  
    1.25 -lemma zless_intify1 [simp]:"intify(x) $< y <-> x $< y"
    1.26 +lemma zless_intify1 [simp]:"intify(x) $< y \<longleftrightarrow> x $< y"
    1.27  by (simp add: zless_def)
    1.28  
    1.29 -lemma zless_intify2 [simp]:"x $< intify(y) <-> x $< y"
    1.30 +lemma zless_intify2 [simp]:"x $< intify(y) \<longleftrightarrow> x $< y"
    1.31  by (simp add: zless_def)
    1.32  
    1.33 -lemma zle_intify1 [simp]:"intify(x) $<= y <-> x $<= y"
    1.34 +lemma zle_intify1 [simp]:"intify(x) $<= y \<longleftrightarrow> x $<= y"
    1.35  by (simp add: zle_def)
    1.36  
    1.37 -lemma zle_intify2 [simp]:"x $<= intify(y) <-> x $<= y"
    1.38 +lemma zle_intify2 [simp]:"x $<= intify(y) \<longleftrightarrow> x $<= y"
    1.39  by (simp add: zle_def)
    1.40  
    1.41  
    1.42 @@ -268,7 +268,7 @@
    1.43  
    1.44  subsection{*@{term znegative}: the test for negative integers*}
    1.45  
    1.46 -lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) <-> x<y"
    1.47 +lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) \<longleftrightarrow> x<y"
    1.48  apply (cases "x<y") 
    1.49  apply (auto simp add: znegative_def not_lt_iff_le)
    1.50  apply (subgoal_tac "y #+ x2 < x #+ y2", force) 
    1.51 @@ -644,7 +644,7 @@
    1.52  lemma zless_not_refl [iff]: "~ (z$<z)"
    1.53  by (auto simp add: zless_def znegative_def int_of_def zdiff_def)
    1.54  
    1.55 -lemma neq_iff_zless: "[| x: int; y: int |] ==> (x \<noteq> y) <-> (x $< y | y $< x)"
    1.56 +lemma neq_iff_zless: "[| x: int; y: int |] ==> (x \<noteq> y) \<longleftrightarrow> (x $< y | y $< x)"
    1.57  by (cut_tac z = x and w = y in zless_linear, auto)
    1.58  
    1.59  lemma zless_imp_intify_neq: "w $< z ==> intify(w) \<noteq> intify(z)"
    1.60 @@ -682,14 +682,14 @@
    1.61  by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto)
    1.62  
    1.63  lemma zless_iff_succ_zadd:
    1.64 -     "w $< z <-> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
    1.65 +     "w $< z \<longleftrightarrow> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
    1.66  apply (rule iffI)
    1.67  apply (erule zless_imp_succ_zadd, auto)
    1.68  apply (rename_tac "n")
    1.69  apply (cut_tac w = w and n = n in zless_succ_zadd, auto)
    1.70  done
    1.71  
    1.72 -lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> ($#m $< $#n) <-> (m<n)"
    1.73 +lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> ($#m $< $#n) \<longleftrightarrow> (m<n)"
    1.74  apply (simp add: less_iff_succ_add zless_iff_succ_zadd int_of_add [symmetric])
    1.75  apply (blast intro: sym)
    1.76  done
    1.77 @@ -768,13 +768,13 @@
    1.78  apply (simp add: zless_def zdiff_def zminus_def)
    1.79  done
    1.80  
    1.81 -lemma not_zless_iff_zle: "~ (z $< w) <-> (w $<= z)"
    1.82 +lemma not_zless_iff_zle: "~ (z $< w) \<longleftrightarrow> (w $<= z)"
    1.83  apply (cut_tac z = z and w = w in zless_linear)
    1.84  apply (auto dest: zless_trans simp add: zle_def)
    1.85  apply (auto dest!: zless_imp_intify_neq)
    1.86  done
    1.87  
    1.88 -lemma not_zle_iff_zless: "~ (z $<= w) <-> (w $< z)"
    1.89 +lemma not_zle_iff_zless: "~ (z $<= w) \<longleftrightarrow> (w $< z)"
    1.90  by (simp add: not_zless_iff_zle [THEN iff_sym])
    1.91  
    1.92  
    1.93 @@ -786,32 +786,32 @@
    1.94  lemma zdiff_zdiff_eq2: "x $- (y $- z) = (x $+ z) $- y"
    1.95  by (simp add: zdiff_def zadd_ac)
    1.96  
    1.97 -lemma zdiff_zless_iff: "(x$-y $< z) <-> (x $< z $+ y)"
    1.98 +lemma zdiff_zless_iff: "(x$-y $< z) \<longleftrightarrow> (x $< z $+ y)"
    1.99  by (simp add: zless_def zdiff_def zadd_ac)
   1.100  
   1.101 -lemma zless_zdiff_iff: "(x $< z$-y) <-> (x $+ y $< z)"
   1.102 +lemma zless_zdiff_iff: "(x $< z$-y) \<longleftrightarrow> (x $+ y $< z)"
   1.103  by (simp add: zless_def zdiff_def zadd_ac)
   1.104  
   1.105 -lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)"
   1.106 +lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) \<longleftrightarrow> (x = z $+ y)"
   1.107  by (auto simp add: zdiff_def zadd_assoc)
   1.108  
   1.109 -lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)"
   1.110 +lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) \<longleftrightarrow> (x $+ y = z)"
   1.111  by (auto simp add: zdiff_def zadd_assoc)
   1.112  
   1.113  lemma zdiff_zle_iff_lemma:
   1.114 -     "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)"
   1.115 +     "[| x: int; z: int |] ==> (x$-y $<= z) \<longleftrightarrow> (x $<= z $+ y)"
   1.116  by (auto simp add: zle_def zdiff_eq_iff zdiff_zless_iff)
   1.117  
   1.118 -lemma zdiff_zle_iff: "(x$-y $<= z) <-> (x $<= z $+ y)"
   1.119 +lemma zdiff_zle_iff: "(x$-y $<= z) \<longleftrightarrow> (x $<= z $+ y)"
   1.120  by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp)
   1.121  
   1.122  lemma zle_zdiff_iff_lemma:
   1.123 -     "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)"
   1.124 +     "[| x: int; z: int |] ==>(x $<= z$-y) \<longleftrightarrow> (x $+ y $<= z)"
   1.125  apply (auto simp add: zle_def zdiff_eq_iff zless_zdiff_iff)
   1.126  apply (auto simp add: zdiff_def zadd_assoc)
   1.127  done
   1.128  
   1.129 -lemma zle_zdiff_iff: "(x $<= z$-y) <-> (x $+ y $<= z)"
   1.130 +lemma zle_zdiff_iff: "(x $<= z$-y) \<longleftrightarrow> (x $+ y $<= z)"
   1.131  by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp)
   1.132  
   1.133  text{*This list of rewrites simplifies (in)equalities by bringing subtractions
   1.134 @@ -828,41 +828,41 @@
   1.135       of the CancelNumerals Simprocs*}
   1.136  
   1.137  lemma zadd_left_cancel:
   1.138 -     "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)"
   1.139 +     "[| w: int; w': int |] ==> (z $+ w' = z $+ w) \<longleftrightarrow> (w' = w)"
   1.140  apply safe
   1.141  apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
   1.142  apply (simp add: zadd_ac)
   1.143  done
   1.144  
   1.145  lemma zadd_left_cancel_intify [simp]:
   1.146 -     "(z $+ w' = z $+ w) <-> intify(w') = intify(w)"
   1.147 +     "(z $+ w' = z $+ w) \<longleftrightarrow> intify(w') = intify(w)"
   1.148  apply (rule iff_trans)
   1.149  apply (rule_tac [2] zadd_left_cancel, auto)
   1.150  done
   1.151  
   1.152  lemma zadd_right_cancel:
   1.153 -     "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)"
   1.154 +     "[| w: int; w': int |] ==> (w' $+ z = w $+ z) \<longleftrightarrow> (w' = w)"
   1.155  apply safe
   1.156  apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
   1.157  apply (simp add: zadd_ac)
   1.158  done
   1.159  
   1.160  lemma zadd_right_cancel_intify [simp]:
   1.161 -     "(w' $+ z = w $+ z) <-> intify(w') = intify(w)"
   1.162 +     "(w' $+ z = w $+ z) \<longleftrightarrow> intify(w') = intify(w)"
   1.163  apply (rule iff_trans)
   1.164  apply (rule_tac [2] zadd_right_cancel, auto)
   1.165  done
   1.166  
   1.167 -lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) <-> (w' $< w)"
   1.168 +lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) \<longleftrightarrow> (w' $< w)"
   1.169  by (simp add: zdiff_zless_iff [THEN iff_sym] zdiff_def zadd_assoc)
   1.170  
   1.171 -lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) <-> (w' $< w)"
   1.172 +lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) \<longleftrightarrow> (w' $< w)"
   1.173  by (simp add: zadd_commute [of z] zadd_right_cancel_zless)
   1.174  
   1.175 -lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) <-> w' $<= w"
   1.176 +lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) \<longleftrightarrow> w' $<= w"
   1.177  by (simp add: zle_def)
   1.178  
   1.179 -lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) <->  w' $<= w"
   1.180 +lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) \<longleftrightarrow>  w' $<= w"
   1.181  by (simp add: zadd_commute [of z]  zadd_right_cancel_zle)
   1.182  
   1.183  
   1.184 @@ -887,26 +887,26 @@
   1.185  
   1.186  subsection{*Comparison laws*}
   1.187  
   1.188 -lemma zminus_zless_zminus [simp]: "($- x $< $- y) <-> (y $< x)"
   1.189 +lemma zminus_zless_zminus [simp]: "($- x $< $- y) \<longleftrightarrow> (y $< x)"
   1.190  by (simp add: zless_def zdiff_def zadd_ac)
   1.191  
   1.192 -lemma zminus_zle_zminus [simp]: "($- x $<= $- y) <-> (y $<= x)"
   1.193 +lemma zminus_zle_zminus [simp]: "($- x $<= $- y) \<longleftrightarrow> (y $<= x)"
   1.194  by (simp add: not_zless_iff_zle [THEN iff_sym])
   1.195  
   1.196  subsubsection{*More inequality lemmas*}
   1.197  
   1.198 -lemma equation_zminus: "[| x: int;  y: int |] ==> (x = $- y) <-> (y = $- x)"
   1.199 +lemma equation_zminus: "[| x: int;  y: int |] ==> (x = $- y) \<longleftrightarrow> (y = $- x)"
   1.200  by auto
   1.201  
   1.202 -lemma zminus_equation: "[| x: int;  y: int |] ==> ($- x = y) <-> ($- y = x)"
   1.203 +lemma zminus_equation: "[| x: int;  y: int |] ==> ($- x = y) \<longleftrightarrow> ($- y = x)"
   1.204  by auto
   1.205  
   1.206 -lemma equation_zminus_intify: "(intify(x) = $- y) <-> (intify(y) = $- x)"
   1.207 +lemma equation_zminus_intify: "(intify(x) = $- y) \<longleftrightarrow> (intify(y) = $- x)"
   1.208  apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus)
   1.209  apply auto
   1.210  done
   1.211  
   1.212 -lemma zminus_equation_intify: "($- x = intify(y)) <-> ($- y = intify(x))"
   1.213 +lemma zminus_equation_intify: "($- x = intify(y)) \<longleftrightarrow> ($- y = intify(x))"
   1.214  apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation)
   1.215  apply auto
   1.216  done
   1.217 @@ -914,16 +914,16 @@
   1.218  
   1.219  subsubsection{*The next several equations are permutative: watch out!*}
   1.220  
   1.221 -lemma zless_zminus: "(x $< $- y) <-> (y $< $- x)"
   1.222 +lemma zless_zminus: "(x $< $- y) \<longleftrightarrow> (y $< $- x)"
   1.223  by (simp add: zless_def zdiff_def zadd_ac)
   1.224  
   1.225 -lemma zminus_zless: "($- x $< y) <-> ($- y $< x)"
   1.226 +lemma zminus_zless: "($- x $< y) \<longleftrightarrow> ($- y $< x)"
   1.227  by (simp add: zless_def zdiff_def zadd_ac)
   1.228  
   1.229 -lemma zle_zminus: "(x $<= $- y) <-> (y $<= $- x)"
   1.230 +lemma zle_zminus: "(x $<= $- y) \<longleftrightarrow> (y $<= $- x)"
   1.231  by (simp add: not_zless_iff_zle [THEN iff_sym] zminus_zless)
   1.232  
   1.233 -lemma zminus_zle: "($- x $<= y) <-> ($- y $<= x)"
   1.234 +lemma zminus_zle: "($- x $<= y) \<longleftrightarrow> ($- y $<= x)"
   1.235  by (simp add: not_zless_iff_zle [THEN iff_sym] zless_zminus)
   1.236  
   1.237  end