src/ZF/Arith.thy

   There are no negative numbers; we have
      m #- n = 0  iff  m<=n   and     m #- n = succ(k) iff m>n.
   Also, rec(m, 0, %z w.z) is pred(m).
 *)
 
-section{*Arithmetic Operators and Their Definitions*}
+section\<open>Arithmetic Operators and Their Definitions\<close>
 
 theory Arith imports Univ begin
 
-text{*Proofs about elementary arithmetic: addition, multiplication, etc.*}
+text\<open>Proofs about elementary arithmetic: addition, multiplication, etc.\<close>
 
 definition
   pred   :: "i=>i"    (*inverse of succ*)  where
     "pred(y) == nat_case(0, %x. x, y)"
 

 
 (* @{term"[| 0 < k; k \<in> nat; !!j. [| j \<in> nat; k = succ(j) |] ==> Q |] ==> Q"} *)
 lemmas zero_lt_natE = zero_lt_lemma [THEN bexE]
 
 
-subsection{*@{text natify}, the Coercion to @{term nat}*}
+subsection\<open>@{text natify}, the Coercion to @{term nat}\<close>
 
 lemma pred_succ_eq [simp]: "pred(succ(y)) = y"
 by (unfold pred_def, auto)
 
 lemma natify_succ: "natify(succ(x)) = succ(natify(x))"

 
 lemma div_natify2 [simp]: "m div natify(n) = m div n"
 by (simp add: div_def)
 
 
-subsection{*Typing rules*}
+subsection\<open>Typing rules\<close>
 
 (** Addition **)
 
 lemma raw_add_type: "[| m\<in>nat;  n\<in>nat |] ==> raw_add (m, n) \<in> nat"
 by (induct_tac "m", auto)

 apply (erule_tac [6] leE)
 apply (simp_all add: le_iff)
 done
 
 
-subsection{*Addition*}
+subsection\<open>Addition\<close>
 
 (*Natify has weakened this law, compared with the older approach*)
 lemma add_0_natify [simp]: "0 #+ m = natify(m)"
 by (simp add: add_def)
 

 
 lemma zero_less_add: "[| n \<in> nat; m \<in> nat |] ==> 0 < m #+ n \<longleftrightarrow> (0<m | 0<n)"
 by (induct_tac "n", auto)
 
 
-subsection{*Monotonicity of Addition*}
+subsection\<open>Monotonicity of Addition\<close>
 
 (*strict, in 1st argument; proof is by rule induction on 'less than'.
   Still need j\<in>nat, for consider j = omega.  Then we can have i<omega,
   which is the same as i\<in>nat, but natify(j)=0, so the conclusion fails.*)
 lemma add_lt_mono1: "[| i<j; j\<in>nat |] ==> i#+k < j#+k"
 apply (frule lt_nat_in_nat, assumption)
 apply (erule succ_lt_induct)
 apply (simp_all add: leI)
 done
 
-text{*strict, in second argument*}
+text\<open>strict, in second argument\<close>
 lemma add_lt_mono2: "[| i<j; j\<in>nat |] ==> k#+i < k#+j"
 by (simp add: add_commute [of k] add_lt_mono1)
 
-text{*A [clumsy] way of lifting < monotonicity to @{text "\<le>"} monotonicity*}
+text\<open>A [clumsy] way of lifting < monotonicity to @{text "\<le>"} monotonicity\<close>
 lemma Ord_lt_mono_imp_le_mono:
   assumes lt_mono: "!!i j. [| i<j; j:k |] ==> f(i) < f(j)"
       and ford:    "!!i. i:k ==> Ord(f(i))"
       and leij:    "i \<le> j"
       and jink:    "j:k"
   shows "f(i) \<le> f(j)"
 apply (insert leij jink)
 apply (blast intro!: leCI lt_mono ford elim!: leE)
 done
 
-text{*@{text "\<le>"} monotonicity, 1st argument*}
+text\<open>@{text "\<le>"} monotonicity, 1st argument\<close>
 lemma add_le_mono1: "[| i \<le> j; j\<in>nat |] ==> i#+k \<le> j#+k"
 apply (rule_tac f = "%j. j#+k" in Ord_lt_mono_imp_le_mono, typecheck)
 apply (blast intro: add_lt_mono1 add_type [THEN nat_into_Ord])+
 done
 
-text{*@{text "\<le>"} monotonicity, both arguments*}
+text\<open>@{text "\<le>"} monotonicity, both arguments\<close>
 lemma add_le_mono: "[| i \<le> j; k \<le> l; j\<in>nat; l\<in>nat |] ==> i#+k \<le> j#+l"
 apply (rule add_le_mono1 [THEN le_trans], assumption+)
 apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+)
 done
 
-text{*Combinations of less-than and less-than-or-equals*}
+text\<open>Combinations of less-than and less-than-or-equals\<close>
 
 lemma add_lt_le_mono: "[| i<j; k\<le>l; j\<in>nat; l\<in>nat |] ==> i#+k < j#+l"
 apply (rule add_lt_mono1 [THEN lt_trans2], assumption+)
 apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+)
 done
 
 lemma add_le_lt_mono: "[| i\<le>j; k<l; j\<in>nat; l\<in>nat |] ==> i#+k < j#+l"
 by (subst add_commute, subst add_commute, erule add_lt_le_mono, assumption+)
 
-text{*Less-than: in other words, strict in both arguments*}
+text\<open>Less-than: in other words, strict in both arguments\<close>
 lemma add_lt_mono: "[| i<j; k<l; j\<in>nat; l\<in>nat |] ==> i#+k < j#+l"
 apply (rule add_lt_le_mono)
 apply (auto intro: leI)
 done
 

 
 lemma diff_Un_distrib:
     "[|i\<in>nat; j\<in>nat|] ==> (i \<union> j) #- k = (i#-k) \<union> (j#-k)"
 by (insert nat_diff_Un_distrib [of i j "natify(k)"], simp)
 
-text{*We actually prove @{term "i #- j #- k = i #- (j #+ k)"}*}
+text\<open>We actually prove @{term "i #- j #- k = i #- (j #+ k)"}\<close>
 lemma diff_diff_left [simplified]:
      "natify(i)#-natify(j)#-k = natify(i) #- (natify(j)#+k)"
 by (rule_tac m="natify(i)" and n="natify(j)" in diff_induct, auto)
 
 

 
 lemma iff_cong2: "u \<longleftrightarrow> u' ==> (t==u) == (t==u')"
 by auto
 
 
-subsection{*Multiplication*}
+subsection\<open>Multiplication\<close>
 
 lemma mult_0 [simp]: "0 #* m = 0"
 by (simp add: mult_def)
 
 lemma mult_succ [simp]: "succ(m) #* n = n #+ (m #* n)"