src/HOL/Decision_Procs/Rat_Pair.thy
 changeset 68442 477b3f7067c9 parent 67123 3fe40ff1b921 child 69597 ff784d5a5bfb
```     1.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Jun 14 10:51:12 2018 +0200
1.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Jun 14 15:45:53 2018 +0200
1.3 @@ -177,7 +177,7 @@
1.4  lemma isnormNum_unique[simp]:
1.5    assumes na: "isnormNum x"
1.6      and nb: "isnormNum y"
1.7 -  shows "(INum x ::'a::{field_char_0,field}) = INum y \<longleftrightarrow> x = y"
1.8 +  shows "(INum x ::'a::field_char_0) = INum y \<longleftrightarrow> x = y"
1.9    (is "?lhs = ?rhs")
1.10  proof
1.11    obtain a b where x: "x = (a, b)" by (cases x)
1.12 @@ -217,7 +217,7 @@
1.13      using that by simp
1.14  qed
1.15
1.16 -lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> INum x = (0::'a::{field_char_0,field}) \<longleftrightarrow> x = 0\<^sub>N"
1.17 +lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> INum x = (0::'a::field_char_0) \<longleftrightarrow> x = 0\<^sub>N"
1.18    unfolding INum_int(2)[symmetric]
1.19    by (rule isnormNum_unique) simp_all
1.20
1.21 @@ -244,7 +244,7 @@
1.22    shows "(of_int (n div d) ::'a::field_char_0) = of_int n / of_int d"
1.23    using assms of_int_div_aux [of d n, where ?'a = 'a] by simp
1.24
1.25 -lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0,field})"
1.26 +lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::field_char_0)"
1.27  proof -
1.28    obtain a b where x: "x = (a, b)" by (cases x)
1.29    consider "a = 0 \<or> b = 0" | "a \<noteq> 0" "b \<noteq> 0" by blast
1.30 @@ -262,7 +262,7 @@
1.31    qed
1.32  qed
1.33
1.34 -lemma INum_normNum_iff: "(INum x ::'a::{field_char_0,field}) = INum y \<longleftrightarrow> normNum x = normNum y"
1.35 +lemma INum_normNum_iff: "(INum x ::'a::field_char_0) = INum y \<longleftrightarrow> normNum x = normNum y"
1.36    (is "?lhs \<longleftrightarrow> _")
1.37  proof -
1.38    have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
1.39 @@ -271,7 +271,7 @@
1.40    finally show ?thesis by simp
1.41  qed
1.42
1.43 -lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0,field})"
1.44 +lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: field_char_0)"
1.45  proof -
1.46    let ?z = "0::'a"
1.47    obtain a b where x: "x = (a, b)" by (cases x)
1.48 @@ -319,7 +319,7 @@
1.49    qed
1.50  qed
1.51
1.52 -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a::{field_char_0,field})"
1.53 +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a::field_char_0)"
1.54  proof -
1.55    let ?z = "0::'a"
1.56    obtain a b where x: "x = (a, b)" by (cases x)
1.57 @@ -346,13 +346,13 @@
1.58  lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x :: 'a::field)"
1.59    by (simp add: Nneg_def split_def INum_def)
1.60
1.61 -lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a::{field_char_0,field})"
1.62 +lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a::field_char_0)"
1.63    by (simp add: Nsub_def split_def)
1.64
1.65  lemma Ninv[simp]: "INum (Ninv x) = (1 :: 'a::field) / INum x"
1.66    by (simp add: Ninv_def INum_def split_def)
1.67
1.68 -lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y :: 'a::{field_char_0,field})"
1.69 +lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y :: 'a::field_char_0)"
1.71
1.72  lemma Nlt0_iff[simp]:
1.73 @@ -463,7 +463,7 @@
1.74  qed
1.75
1.77 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.78 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.79    shows "x +\<^sub>N y = y +\<^sub>N x"
1.80  proof -
1.81    have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)"
1.82 @@ -475,7 +475,7 @@
1.83  qed
1.84
1.85  lemma [simp]:
1.86 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.87 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.88    shows "(0, b) +\<^sub>N y = normNum y"
1.89      and "(a, 0) +\<^sub>N y = normNum y"
1.90      and "x +\<^sub>N (0, b) = normNum x"
1.91 @@ -489,7 +489,7 @@
1.92    done
1.93
1.94  lemma normNum_nilpotent_aux[simp]:
1.95 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.96 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.97    assumes nx: "isnormNum x"
1.98    shows "normNum x = x"
1.99  proof -
1.100 @@ -500,7 +500,7 @@
1.101  qed
1.102
1.103  lemma normNum_nilpotent[simp]:
1.104 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.105 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.106    shows "normNum (normNum x) = normNum x"
1.107    by simp
1.108
1.109 @@ -508,12 +508,12 @@
1.111
1.113 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.114 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.115    shows "normNum (x +\<^sub>N y) = x +\<^sub>N y"
1.116    by simp
1.117
1.119 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.120 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.121    shows "normNum x +\<^sub>N y = x +\<^sub>N y"
1.122  proof -
1.123    have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)"
1.124 @@ -527,7 +527,7 @@
1.125  qed
1.126
1.128 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.129 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.130    shows "x +\<^sub>N normNum y = x +\<^sub>N y"
1.131  proof -
1.132    have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)"
1.133 @@ -541,7 +541,7 @@
1.134  qed
1.135
1.137 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.138 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.139    shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
1.140  proof -
1.141    have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))"
1.142 @@ -556,7 +556,7 @@
1.143    by (simp add: Nmul_def split_def Let_def gcd.commute mult.commute)
1.144
1.145  lemma Nmul_assoc:
1.146 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.147 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.148    assumes nx: "isnormNum x"
1.149      and ny: "isnormNum y"
1.150      and nz: "isnormNum z"
1.151 @@ -571,7 +571,7 @@
1.152  qed
1.153
1.154  lemma Nsub0:
1.155 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.156 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.157    assumes x: "isnormNum x"
1.158      and y: "isnormNum y"
1.159    shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y"
1.160 @@ -590,7 +590,7 @@
1.161    by (simp_all add: Nmul_def Let_def split_def)
1.162
1.163  lemma Nmul_eq0[simp]:
1.164 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.165 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.166    assumes nx: "isnormNum x"
1.167      and ny: "isnormNum y"
1.168    shows "x*\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N"
```