src/HOL/Decision_Procs/Commutative_Ring_Complete.thy

 This theory is about of the relative completeness of method comm-ring
 method.  As long as the reified atomic polynomials of type 'a pol are
 in normal form, the cring method is complete.
 *)
 
-section {* Proof of the relative completeness of method comm-ring *}
+section \<open>Proof of the relative completeness of method comm-ring\<close>
 
 theory Commutative_Ring_Complete
 imports Commutative_Ring
 begin
 
-text {* Formalization of normal form *}
+text \<open>Formalization of normal form\<close>
 fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool"
 where
   "isnorm (Pc c) \<longleftrightarrow> True"
 | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
 | "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False"

   case Pinj
   with assms show ?thesis
     by (cases x) auto
 qed
 
-text {* mkPX conserves normalizedness (@{text "_cn"}) *}
+text \<open>mkPX conserves normalizedness (@{text "_cn"})\<close>
 lemma mkPX_cn:
   assumes "x \<noteq> 0"
     and "isnorm P"
     and "isnorm Q"
   shows "isnorm (mkPX P x Q)"

     by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
   from assms PX Y0 show ?thesis
     by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
 qed
 
-text {* add conserves normalizedness *}
+text \<open>add conserves normalizedness\<close>
 lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
 proof (induct P Q rule: add.induct)
   case (2 c i P2)
   then show ?case
     by (cases P2) (simp_all, cases i, simp_all)

     note 6 X0
     moreover
     from 6 have "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     moreover
-    from 6 `x < y` y have "isnorm (Pinj d Q2)"
+    from 6 \<open>x < y\<close> y have "isnorm (Pinj d Q2)"
       by (cases d, simp, cases Q2, auto)
     ultimately have ?case by (simp add: mkPinj_cn)
   }
   moreover {
     assume "x = y"

     note 6 Y0
     moreover
     from 6 have "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     moreover
-    from 6 `x > y` x have "isnorm (Pinj d P2)"
+    from 6 \<open>x > y\<close> x have "isnorm (Pinj d P2)"
       by (cases d) (simp, cases P2, auto)
     ultimately have ?case by (simp add: mkPinj_cn)
   }
   ultimately show ?case by blast
 next

   }
   moreover {
     assume "x = 1"
     from 7 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
-    with 7 `x = 1` have ?case
+    with 7 \<open>x = 1\<close> have "isnorm (R \<oplus> P2)" by simp
+    with 7 \<open>x = 1\<close> have ?case
       by (simp add: norm_PXtrans[of Q2 y _])
   }
   moreover {
     assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith
     then obtain d where X: "x=Suc (Suc d)" ..
     with 7 have NR: "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
     with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
-    with `isnorm (PX Q2 y R)` X have ?case
+    with \<open>isnorm (PX Q2 y R)\<close> X have ?case
       by (simp add: norm_PXtrans[of Q2 y _])
   }
   ultimately show ?case by blast
 next
   case (8 Q2 y R x P2)

   }
   moreover {
     assume "x = 1"
     with 8 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 `x = 1` have "isnorm (R \<oplus> P2)"
+    with 8 \<open>x = 1\<close> have "isnorm (R \<oplus> P2)"
       by simp
-    with 8 `x = 1` have ?case
+    with 8 \<open>x = 1\<close> have ?case
       by (simp add: norm_PXtrans[of Q2 y _])
   }
   moreover {
     assume "x > 1"
     then have "\<exists>d. x = Suc (Suc d)" by arith
     then obtain d where X: "x = Suc (Suc d)" ..
     with 8 have NR: "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with 8 X have "isnorm (Pinj (x - 1) P2)"
       by (cases P2) auto
-    with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
+    with 8 \<open>x > 1\<close> NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
       by simp
-    with `isnorm (PX Q2 y R)` X have ?case
+    with \<open>isnorm (PX Q2 y R)\<close> X have ?case
       by (simp add: norm_PXtrans[of Q2 y _])
   }
   ultimately show ?case by blast
 next
   case (9 P1 x P2 Q1 y Q2)

   }
   moreover {
     assume "x = y"
     with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
       by auto
-    with `x = y` Y0 have ?case
+    with \<open>x = y\<close> Y0 have ?case
       by (simp add: mkPX_cn)
   }
   moreover {
     assume sm1: "x < y"
     then have "\<exists>d. y = d + x" by arith

       by (simp add: mkPX_cn)
   }
   ultimately show ?case by blast
 qed simp
 
-text {* mul concerves normalizedness *}
+text \<open>mul concerves normalizedness\<close>
 lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
 proof (induct P Q rule: mul.induct)
   case (2 c i P2)
   then show ?case
     by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)

       by (cases x) (auto simp add: norm_Pinj_0_False)
     moreover
     from 6 have "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     moreover
-    from 6 `x < y` y have "isnorm (Pinj d Q2)"
+    from 6 \<open>x < y\<close> y have "isnorm (Pinj d Q2)"
       by (cases d) (simp, cases Q2, auto)
     ultimately have ?case by (simp add: mkPinj_cn)
   }
   moreover {
     assume "x = y"

       by (cases y) (auto simp add: norm_Pinj_0_False)
     moreover
     from 6 have "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     moreover
-    from 6 `x > y` x have "isnorm (Pinj d P2)"
+    from 6 \<open>x > y\<close> x have "isnorm (Pinj d P2)"
       by (cases d) (simp, cases P2, auto)
     ultimately have ?case by (simp add: mkPinj_cn)
   }
   ultimately show ?case by blast
 next

   }
   moreover {
     assume "x = 1"
     from 7 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
+    with 7 \<open>x = 1\<close> have "isnorm (R \<otimes> P2)" "isnorm Q2"
       by (auto simp add: norm_PX1[of Q2 y R])
-    with 7 `x = 1` Y0 have ?case
+    with 7 \<open>x = 1\<close> Y0 have ?case
       by (simp add: mkPX_cn)
   }
   moreover {
     assume "x > 1"
     then have "\<exists>d. x = Suc (Suc d)"

   }
   moreover {
     assume "x = 1"
     from 8 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
+    with 8 \<open>x = 1\<close> have "isnorm (R \<otimes> P2)" "isnorm Q2"
       by (auto simp add: norm_PX1[of Q2 y R])
-    with 8 `x = 1` Y0 have ?case
+    with 8 \<open>x = 1\<close> Y0 have ?case
       by (simp add: mkPX_cn)
   }
   moreover {
     assume "x > 1"
     then have "\<exists>d. x = Suc (Suc d)" by arith

     "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"
     by (auto simp add: mkPX_cn)
   then show ?case by (simp add: add_cn)
 qed simp
 
-text {* neg conserves normalizedness *}
+text \<open>neg conserves normalizedness\<close>
 lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
 proof (induct P)
   case (Pinj i P2)
   then have "isnorm P2"
     by (simp add: norm_Pinj[of i P2])

     with PX1 show ?thesis
       by (cases x) auto
   qed (cases x, auto)
 qed simp
 
-text {* sub conserves normalizedness *}
+text \<open>sub conserves normalizedness\<close>
 lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
   by (simp add: sub_def add_cn neg_cn)
 
-text {* sqr conserves normalizizedness *}
+text \<open>sqr conserves normalizizedness\<close>
 lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
 proof (induct P)
   case Pc
   then show ?case by simp
 next

     by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   then show ?case
     by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
 qed
 
-text {* pow conserves normalizedness *}
+text \<open>pow conserves normalizedness\<close>
 lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
 proof (induct n arbitrary: P rule: less_induct)
   case (less k)
   show ?case
   proof (cases "k = 0")