diff -r 0c18df79b1c8 -r a642599ffdea src/ZF/IntDiv.thy
--- a/src/ZF/IntDiv.thy	Tue Sep 27 17:03:23 2022 +0100
+++ b/src/ZF/IntDiv.thy	Tue Sep 27 17:46:52 2022 +0100
@@ -34,65 +34,65 @@
 begin
 
 definition
-  quorem :: "[i,i] => o"  where
-    "quorem \<equiv> %<a,b> <q,r>.
+  quorem :: "[i,i] \<Rightarrow> o"  where
+    "quorem \<equiv> \<lambda>\<langle>a,b\<rangle> \<langle>q,r\<rangle>.
                       a = b$*q $+ r \<and>
                       (#0$<b \<and> #0$\<le>r \<and> r$<b | \<not>(#0$<b) \<and> b$<r \<and> r $\<le> #0)"
 
 definition
-  adjust :: "[i,i] => i"  where
-    "adjust(b) \<equiv> %<q,r>. if #0 $\<le> r$-b then <#2$*q $+ #1,r$-b>
+  adjust :: "[i,i] \<Rightarrow> i"  where
+    "adjust(b) \<equiv> \<lambda>\<langle>q,r\<rangle>. if #0 $\<le> r$-b then <#2$*q $+ #1,r$-b>
                           else <#2$*q,r>"
 
 
 (** the division algorithm **)
 
 definition
-  posDivAlg :: "i => i"  where
+  posDivAlg :: "i \<Rightarrow> i"  where
 (*for the case a>=0, b>0*)
-(*recdef posDivAlg "inv_image less_than (%(a,b). nat_of(a $- b $+ #1))"*)
+(*recdef posDivAlg "inv_image less_than (\<lambda>\<langle>a,b\<rangle>. nat_of(a $- b $+ #1))"*)
     "posDivAlg(ab) \<equiv>
-       wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)),
+       wfrec(measure(int*int, \<lambda>\<langle>a,b\<rangle>. nat_of (a $- b $+ #1)),
              ab,
-             %<a,b> f. if (a$<b | b$\<le>#0) then <#0,a>
+             \<lambda>\<langle>a,b\<rangle> f. if (a$<b | b$\<le>#0) then <#0,a>
                        else adjust(b, f ` <a,#2$*b>))"
 
 
-(*for the case a<0, b>0*)
+(*for the case a\<langle>0, b\<rangle>0*)
 definition
-  negDivAlg :: "i => i"  where
-(*recdef negDivAlg "inv_image less_than (%(a,b). nat_of(- a $- b))"*)
+  negDivAlg :: "i \<Rightarrow> i"  where
+(*recdef negDivAlg "inv_image less_than (\<lambda>\<langle>a,b\<rangle>. nat_of(- a $- b))"*)
     "negDivAlg(ab) \<equiv>
-       wfrec(measure(int*int, %<a,b>. nat_of ($- a $- b)),
+       wfrec(measure(int*int, \<lambda>\<langle>a,b\<rangle>. nat_of ($- a $- b)),
              ab,
-             %<a,b> f. if (#0 $\<le> a$+b | b$\<le>#0) then <#-1,a$+b>
+             \<lambda>\<langle>a,b\<rangle> f. if (#0 $\<le> a$+b | b$\<le>#0) then <#-1,a$+b>
                        else adjust(b, f ` <a,#2$*b>))"
 
 (*for the general case @{term"b\<noteq>0"}*)
 
 definition
-  negateSnd :: "i => i"  where
-    "negateSnd \<equiv> %<q,r>. <q, $-r>"
+  negateSnd :: "i \<Rightarrow> i"  where
+    "negateSnd \<equiv> \<lambda>\<langle>q,r\<rangle>. <q, $-r>"
 
   (*The full division algorithm considers all possible signs for a, b
     including the special case a=0, b<0, because negDivAlg requires a<0*)
 definition
-  divAlg :: "i => i"  where
+  divAlg :: "i \<Rightarrow> i"  where
     "divAlg \<equiv>
-       %<a,b>. if #0 $\<le> a then
-                  if #0 $\<le> b then posDivAlg (<a,b>)
+       \<lambda>\<langle>a,b\<rangle>. if #0 $\<le> a then
+                  if #0 $\<le> b then posDivAlg (\<langle>a,b\<rangle>)
                   else if a=#0 then <#0,#0>
                        else negateSnd (negDivAlg (<$-a,$-b>))
                else
-                  if #0$<b then negDivAlg (<a,b>)
+                  if #0$<b then negDivAlg (\<langle>a,b\<rangle>)
                   else         negateSnd (posDivAlg (<$-a,$-b>))"
 
 definition
-  zdiv  :: "[i,i]=>i"                    (infixl \<open>zdiv\<close> 70)  where
+  zdiv  :: "[i,i]\<Rightarrow>i"                    (infixl \<open>zdiv\<close> 70)  where
     "a zdiv b \<equiv> fst (divAlg (<intify(a), intify(b)>))"
 
 definition
-  zmod  :: "[i,i]=>i"                    (infixl \<open>zmod\<close> 70)  where
+  zmod  :: "[i,i]\<Rightarrow>i"                    (infixl \<open>zmod\<close> 70)  where
     "a zmod b \<equiv> snd (divAlg (<intify(a), intify(b)>))"
 
 
@@ -380,7 +380,7 @@
 
 
 lemma unique_quotient:
-     "\<lbrakk>quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b \<noteq> #0;
+     "\<lbrakk>quorem (\<langle>a,b\<rangle>, \<langle>q,r\<rangle>);  quorem (\<langle>a,b\<rangle>, <q',r'>);  b \<in> int; b \<noteq> #0;
          q \<in> int; q' \<in> int\<rbrakk> \<Longrightarrow> q = q'"
 apply (simp add: split_ifs quorem_def neq_iff_zless)
 apply safe
@@ -391,7 +391,7 @@
 done
 
 lemma unique_remainder:
-     "\<lbrakk>quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b \<noteq> #0;
+     "\<lbrakk>quorem (\<langle>a,b\<rangle>, \<langle>q,r\<rangle>);  quorem (\<langle>a,b\<rangle>, <q',r'>);  b \<in> int; b \<noteq> #0;
          q \<in> int; q' \<in> int;
          r \<in> int; r' \<in> int\<rbrakk> \<Longrightarrow> r = r'"
 apply (subgoal_tac "q = q'")
@@ -404,7 +404,7 @@
            the Division Algorithm for \<open>a\<ge>0\<close> and \<open>b>0\<close>\<close>
 
 lemma adjust_eq [simp]:
-     "adjust(b, <q,r>) = (let diff = r$-b in
+     "adjust(b, \<langle>q,r\<rangle>) = (let diff = r$-b in
                           if #0 $\<le> diff then <#2$*q $+ #1,diff>
                                          else <#2$*q,r>)"
 by (simp add: Let_def adjust_def)
@@ -421,7 +421,7 @@
 
 lemma posDivAlg_eqn:
      "\<lbrakk>#0 $< b; a \<in> int; b \<in> int\<rbrakk> \<Longrightarrow>
-      posDivAlg(<a,b>) =
+      posDivAlg(\<langle>a,b\<rangle>) =
        (if a$<b then <#0,a> else adjust(b, posDivAlg (<a, #2$*b>)))"
 apply (rule posDivAlg_unfold [THEN trans])
 apply (simp add: vimage_iff not_zless_iff_zle [THEN iff_sym])
@@ -431,10 +431,10 @@
 lemma posDivAlg_induct_lemma [rule_format]:
   assumes prem:
         "\<And>a b. \<lbrakk>a \<in> int; b \<in> int;
-                   \<not> (a $< b | b $\<le> #0) \<longrightarrow> P(<a, #2 $* b>)\<rbrakk> \<Longrightarrow> P(<a,b>)"
-  shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
-using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)"]
-proof (induct "<u,v>" arbitrary: u v rule: wf_induct)
+                   \<not> (a $< b | b $\<le> #0) \<longrightarrow> P(<a, #2 $* b>)\<rbrakk> \<Longrightarrow> P(\<langle>a,b\<rangle>)"
+  shows "\<langle>u,v\<rangle> \<in> int*int \<Longrightarrow> P(\<langle>u,v\<rangle>)"
+using wf_measure [where A = "int*int" and f = "\<lambda>\<langle>a,b\<rangle>.nat_of (a $- b $+ #1)"]
+proof (induct "\<langle>u,v\<rangle>" arbitrary: u v rule: wf_induct)
   case (step x)
   hence uv: "u \<in> int" "v \<in> int" by auto
   thus ?case
@@ -452,7 +452,7 @@
       and ih: "\<And>a b. \<lbrakk>a \<in> int; b \<in> int;
                      \<not> (a $< b | b $\<le> #0) \<longrightarrow> P(a, #2 $* b)\<rbrakk> \<Longrightarrow> P(a,b)"
   shows "P(u,v)"
-apply (subgoal_tac "(%<x,y>. P (x,y)) (<u,v>)")
+apply (subgoal_tac "(\<lambda>\<langle>x,y\<rangle>. P (x,y)) (\<langle>u,v\<rangle>)")
 apply simp
 apply (rule posDivAlg_induct_lemma)
 apply (simp (no_asm_use))
@@ -526,7 +526,7 @@
 
 (*Typechecking for posDivAlg*)
 lemma posDivAlg_type [rule_format]:
-     "\<lbrakk>a \<in> int; b \<in> int\<rbrakk> \<Longrightarrow> posDivAlg(<a,b>) \<in> int * int"
+     "\<lbrakk>a \<in> int; b \<in> int\<rbrakk> \<Longrightarrow> posDivAlg(\<langle>a,b\<rangle>) \<in> int * int"
 apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
 apply assumption+
 apply (case_tac "#0 $< ba")
@@ -542,7 +542,7 @@
 (*Correctness of posDivAlg: it computes quotients correctly*)
 lemma posDivAlg_correct [rule_format]:
      "\<lbrakk>a \<in> int; b \<in> int\<rbrakk>
-      \<Longrightarrow> #0 $\<le> a \<longrightarrow> #0 $< b \<longrightarrow> quorem (<a,b>, posDivAlg(<a,b>))"
+      \<Longrightarrow> #0 $\<le> a \<longrightarrow> #0 $< b \<longrightarrow> quorem (\<langle>a,b\<rangle>, posDivAlg(\<langle>a,b\<rangle>))"
 apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
 apply auto
    apply (simp_all add: quorem_def)
@@ -576,7 +576,7 @@
 
 lemma negDivAlg_eqn:
      "\<lbrakk>#0 $< b; a \<in> int; b \<in> int\<rbrakk> \<Longrightarrow>
-      negDivAlg(<a,b>) =
+      negDivAlg(\<langle>a,b\<rangle>) =
        (if #0 $\<le> a$+b then <#-1,a$+b>
                        else adjust(b, negDivAlg (<a, #2$*b>)))"
 apply (rule negDivAlg_unfold [THEN trans])
@@ -588,10 +588,10 @@
   assumes prem:
         "\<And>a b. \<lbrakk>a \<in> int; b \<in> int;
                    \<not> (#0 $\<le> a $+ b | b $\<le> #0) \<longrightarrow> P(<a, #2 $* b>)\<rbrakk>
-                \<Longrightarrow> P(<a,b>)"
-  shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
-using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)"]
-proof (induct "<u,v>" arbitrary: u v rule: wf_induct)
+                \<Longrightarrow> P(\<langle>a,b\<rangle>)"
+  shows "\<langle>u,v\<rangle> \<in> int*int \<Longrightarrow> P(\<langle>u,v\<rangle>)"
+using wf_measure [where A = "int*int" and f = "\<lambda>\<langle>a,b\<rangle>.nat_of ($- a $- b)"]
+proof (induct "\<langle>u,v\<rangle>" arbitrary: u v rule: wf_induct)
   case (step x)
   hence uv: "u \<in> int" "v \<in> int" by auto
   thus ?case
@@ -609,7 +609,7 @@
                          \<not> (#0 $\<le> a $+ b | b $\<le> #0) \<longrightarrow> P(a, #2 $* b)\<rbrakk>
                       \<Longrightarrow> P(a,b)"
   shows "P(u,v)"
-apply (subgoal_tac " (%<x,y>. P (x,y)) (<u,v>)")
+apply (subgoal_tac " (\<lambda>\<langle>x,y\<rangle>. P (x,y)) (\<langle>u,v\<rangle>)")
 apply simp
 apply (rule negDivAlg_induct_lemma)
 apply (simp (no_asm_use))
@@ -620,7 +620,7 @@
 
 (*Typechecking for negDivAlg*)
 lemma negDivAlg_type:
-     "\<lbrakk>a \<in> int; b \<in> int\<rbrakk> \<Longrightarrow> negDivAlg(<a,b>) \<in> int * int"
+     "\<lbrakk>a \<in> int; b \<in> int\<rbrakk> \<Longrightarrow> negDivAlg(\<langle>a,b\<rangle>) \<in> int * int"
 apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
 apply assumption+
 apply (case_tac "#0 $< ba")
@@ -638,7 +638,7 @@
   It doesn't work if a=0 because the 0/b=0 rather than -1*)
 lemma negDivAlg_correct [rule_format]:
      "\<lbrakk>a \<in> int; b \<in> int\<rbrakk>
-      \<Longrightarrow> a $< #0 \<longrightarrow> #0 $< b \<longrightarrow> quorem (<a,b>, negDivAlg(<a,b>))"
+      \<Longrightarrow> a $< #0 \<longrightarrow> #0 $< b \<longrightarrow> quorem (\<langle>a,b\<rangle>, negDivAlg(\<langle>a,b\<rangle>))"
 apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
   apply auto
    apply (simp_all add: quorem_def)
@@ -687,7 +687,7 @@
 apply (simp add: linear_arith_lemma integ_of_type vimage_iff)
 done
 
-lemma negateSnd_eq [simp]: "negateSnd (<q,r>) = <q, $-r>"
+lemma negateSnd_eq [simp]: "negateSnd (\<langle>q,r\<rangle>) = <q, $-r>"
 apply (unfold negateSnd_def)
 apply auto
 done
@@ -699,7 +699,7 @@
 
 lemma quorem_neg:
      "\<lbrakk>quorem (<$-a,$-b>, qr);  a \<in> int;  b \<in> int;  qr \<in> int * int\<rbrakk>
-      \<Longrightarrow> quorem (<a,b>, negateSnd(qr))"
+      \<Longrightarrow> quorem (\<langle>a,b\<rangle>, negateSnd(qr))"
 apply clarify
 apply (auto elim: zless_asym simp add: quorem_def zless_zminus)
 txt\<open>linear arithmetic from here on\<close>
@@ -711,7 +711,7 @@
 done
 
 lemma divAlg_correct:
-     "\<lbrakk>b \<noteq> #0;  a \<in> int;  b \<in> int\<rbrakk> \<Longrightarrow> quorem (<a,b>, divAlg(<a,b>))"
+     "\<lbrakk>b \<noteq> #0;  a \<in> int;  b \<in> int\<rbrakk> \<Longrightarrow> quorem (\<langle>a,b\<rangle>, divAlg(\<langle>a,b\<rangle>))"
 apply (auto simp add: quorem_0 divAlg_def)
 apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct
                     posDivAlg_type negDivAlg_type)
@@ -720,7 +720,7 @@
 apply (auto simp add: zle_def)
 done
 
-lemma divAlg_type: "\<lbrakk>a \<in> int;  b \<in> int\<rbrakk> \<Longrightarrow> divAlg(<a,b>) \<in> int * int"
+lemma divAlg_type: "\<lbrakk>a \<in> int;  b \<in> int\<rbrakk> \<Longrightarrow> divAlg(\<langle>a,b\<rangle>) \<in> int * int"
 apply (auto simp add: divAlg_def)
 apply (auto simp add: posDivAlg_type negDivAlg_type negateSnd_type)
 done
@@ -802,20 +802,20 @@
 
 lemma quorem_div_mod:
      "\<lbrakk>b \<noteq> #0;  a \<in> int;  b \<in> int\<rbrakk>
-      \<Longrightarrow> quorem (<a,b>, <a zdiv b, a zmod b>)"
+      \<Longrightarrow> quorem (\<langle>a,b\<rangle>, <a zdiv b, a zmod b>)"
 apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
 apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound
                       neg_mod_sign neg_mod_bound)
 done
 
-(*Surely quorem(<a,b>,<q,r>) implies @{term"a \<in> int"}, but it doesn't matter*)
+(*Surely quorem(\<langle>a,b\<rangle>,\<langle>q,r\<rangle>) implies @{term"a \<in> int"}, but it doesn't matter*)
 lemma quorem_div:
-     "\<lbrakk>quorem(<a,b>,<q,r>);  b \<noteq> #0;  a \<in> int;  b \<in> int;  q \<in> int\<rbrakk>
+     "\<lbrakk>quorem(\<langle>a,b\<rangle>,\<langle>q,r\<rangle>);  b \<noteq> #0;  a \<in> int;  b \<in> int;  q \<in> int\<rbrakk>
       \<Longrightarrow> a zdiv b = q"
 by (blast intro: quorem_div_mod [THEN unique_quotient])
 
 lemma quorem_mod:
-     "\<lbrakk>quorem(<a,b>,<q,r>); b \<noteq> #0; a \<in> int; b \<in> int; q \<in> int; r \<in> int\<rbrakk>
+     "\<lbrakk>quorem(\<langle>a,b\<rangle>,\<langle>q,r\<rangle>); b \<noteq> #0; a \<in> int; b \<in> int; q \<in> int; r \<in> int\<rbrakk>
       \<Longrightarrow> a zmod b = r"
 by (blast intro: quorem_div_mod [THEN unique_remainder])
 
@@ -953,7 +953,7 @@
 apply (simp add: int_0_less_mult_iff)
 apply (blast dest: zless_trans)
 (*linear arithmetic...*)
-apply (drule_tac t = "%x. x $- r" in subst_context)
+apply (drule_tac t = "\<lambda>x. x $- r" in subst_context)
 apply (drule sym)
 apply (simp add: zcompare_rls)
 done
@@ -963,12 +963,12 @@
  apply (simp add: int_0_le_mult_iff zcompare_rls)
  apply (blast dest: zle_zless_trans)
 apply (simp add: zdiff_zmult_distrib2)
-apply (drule_tac t = "%x. x $- a $* q" in subst_context)
+apply (drule_tac t = "\<lambda>x. x $- a $* q" in subst_context)
 apply (simp add: zcompare_rls)
 done
 
 lemma self_quotient:
-     "\<lbrakk>quorem(<a,a>,<q,r>);  a \<in> int;  q \<in> int;  a \<noteq> #0\<rbrakk> \<Longrightarrow> q = #1"
+     "\<lbrakk>quorem(\<langle>a,a\<rangle>,\<langle>q,r\<rangle>);  a \<in> int;  q \<in> int;  a \<noteq> #0\<rbrakk> \<Longrightarrow> q = #1"
 apply (simp add: split_ifs quorem_def neq_iff_zless)
 apply (rule zle_anti_sym)
 apply safe
@@ -984,7 +984,7 @@
 done
 
 lemma self_remainder:
-     "\<lbrakk>quorem(<a,a>,<q,r>); a \<in> int; q \<in> int; r \<in> int; a \<noteq> #0\<rbrakk> \<Longrightarrow> r = #0"
+     "\<lbrakk>quorem(\<langle>a,a\<rangle>,\<langle>q,r\<rangle>); a \<in> int; q \<in> int; r \<in> int; a \<noteq> #0\<rbrakk> \<Longrightarrow> r = #0"
 apply (frule self_quotient)
 apply (auto simp add: quorem_def)
 done
@@ -1291,7 +1291,7 @@
 (** proving (a*b) zdiv c = a $* (b zdiv c) $+ a * (b zmod c) **)
 
 lemma zmult1_lemma:
-     "\<lbrakk>quorem(<b,c>, <q,r>);  c \<in> int;  c \<noteq> #0\<rbrakk>
+     "\<lbrakk>quorem(\<langle>b,c\<rangle>, \<langle>q,r\<rangle>);  c \<in> int;  c \<noteq> #0\<rbrakk>
       \<Longrightarrow> quorem (<a$*b, c>, <a$*q $+ (a$*r) zdiv c, (a$*r) zmod c>)"
 apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
                       pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
@@ -1354,7 +1354,7 @@
             a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c) **)
 
 lemma zadd1_lemma:
-     "\<lbrakk>quorem(<a,c>, <aq,ar>);  quorem(<b,c>, <bq,br>);
+     "\<lbrakk>quorem(\<langle>a,c\<rangle>, \<langle>aq,ar\<rangle>);  quorem(\<langle>b,c\<rangle>, \<langle>bq,br\<rangle>);
          c \<in> int;  c \<noteq> #0\<rbrakk>
       \<Longrightarrow> quorem (<a$+b, c>, <aq $+ bq $+ (ar$+br) zdiv c, (ar$+br) zmod c>)"
 apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
@@ -1511,7 +1511,7 @@
 done
 
 lemma zdiv_zmult2_lemma:
-     "\<lbrakk>quorem (<a,b>, <q,r>);  a \<in> int;  b \<in> int;  b \<noteq> #0;  #0 $< c\<rbrakk>
+     "\<lbrakk>quorem (\<langle>a,b\<rangle>, \<langle>q,r\<rangle>);  a \<in> int;  b \<in> int;  b \<noteq> #0;  #0 $< c\<rbrakk>
       \<Longrightarrow> quorem (<a,b$*c>, <q zdiv c, b$*(q zmod c) $+ r>)"
 apply (auto simp add: zmult_ac zmod_zdiv_equality [symmetric] quorem_def
                neq_iff_zless int_0_less_mult_iff