src/ZF/OrderArith.thy
changeset 46821 ff6b0c1087f2
parent 46820 c656222c4dc1
child 46953 2b6e55924af3
     1.1 --- a/src/ZF/OrderArith.thy	Tue Mar 06 15:15:49 2012 +0000
     1.2 +++ b/src/ZF/OrderArith.thy	Tue Mar 06 16:06:52 2012 +0000
     1.3 @@ -39,19 +39,19 @@
     1.4  subsubsection{*Rewrite rules.  Can be used to obtain introduction rules*}
     1.5  
     1.6  lemma radd_Inl_Inr_iff [iff]: 
     1.7 -    "<Inl(a), Inr(b)> \<in> radd(A,r,B,s)  <->  a:A & b:B"
     1.8 +    "<Inl(a), Inr(b)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a:A & b:B"
     1.9  by (unfold radd_def, blast)
    1.10  
    1.11  lemma radd_Inl_iff [iff]: 
    1.12 -    "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r"
    1.13 +    "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a':A & a:A & <a',a>:r"
    1.14  by (unfold radd_def, blast)
    1.15  
    1.16  lemma radd_Inr_iff [iff]: 
    1.17 -    "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) <->  b':B & b:B & <b',b>:s"
    1.18 +    "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) \<longleftrightarrow>  b':B & b:B & <b',b>:s"
    1.19  by (unfold radd_def, blast)
    1.20  
    1.21  lemma radd_Inr_Inl_iff [simp]: 
    1.22 -    "<Inr(b), Inl(a)> \<in> radd(A,r,B,s) <-> False"
    1.23 +    "<Inr(b), Inl(a)> \<in> radd(A,r,B,s) \<longleftrightarrow> False"
    1.24  by (unfold radd_def, blast)
    1.25  
    1.26  declare radd_Inr_Inl_iff [THEN iffD1, dest!] 
    1.27 @@ -163,7 +163,7 @@
    1.28  subsubsection{*Rewrite rule.  Can be used to obtain introduction rules*}
    1.29  
    1.30  lemma  rmult_iff [iff]: 
    1.31 -    "<<a',b'>, <a,b>> \<in> rmult(A,r,B,s) <->        
    1.32 +    "<<a',b'>, <a,b>> \<in> rmult(A,r,B,s) \<longleftrightarrow>        
    1.33              (<a',a>: r  & a':A & a:A & b': B & b: B) |   
    1.34              (<b',b>: s  & a'=a & a:A & b': B & b: B)"
    1.35  
    1.36 @@ -307,7 +307,7 @@
    1.37  
    1.38  subsubsection{*Rewrite rule*}
    1.39  
    1.40 -lemma rvimage_iff: "<a,b> \<in> rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A"
    1.41 +lemma rvimage_iff: "<a,b> \<in> rvimage(A,f,r)  \<longleftrightarrow>  <f`a,f`b>: r & a:A & b:A"
    1.42  by (unfold rvimage_def, blast)
    1.43  
    1.44  subsubsection{*Type checking*}
    1.45 @@ -450,7 +450,7 @@
    1.46  done
    1.47  
    1.48  theorem wf_iff_subset_rvimage:
    1.49 -  "relation(r) ==> wf(r) <-> (\<exists>i f A. Ord(i) & r \<subseteq> rvimage(A, f, Memrel(i)))"
    1.50 +  "relation(r) ==> wf(r) \<longleftrightarrow> (\<exists>i f A. Ord(i) & r \<subseteq> rvimage(A, f, Memrel(i)))"
    1.51  by (blast dest!: relation_field_times_field wf_imp_subset_rvimage
    1.52            intro: wf_rvimage_Ord [THEN wf_subset])
    1.53  
    1.54 @@ -496,7 +496,7 @@
    1.55  lemma wf_measure [iff]: "wf(measure(A,f))"
    1.56  by (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage)
    1.57  
    1.58 -lemma measure_iff [iff]: "<x,y> \<in> measure(A,f) <-> x:A & y:A & f(x)<f(y)"
    1.59 +lemma measure_iff [iff]: "<x,y> \<in> measure(A,f) \<longleftrightarrow> x:A & y:A & f(x)<f(y)"
    1.60  by (simp (no_asm) add: measure_def)
    1.61  
    1.62  lemma linear_measure: