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.70    by (simp add: Ndiv_def)
    1.71  
    1.72  lemma Nlt0_iff[simp]:
    1.73 @@ -463,7 +463,7 @@
    1.74  qed
    1.75  
    1.76  lemma Nadd_commute:
    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.110    by (simp_all add: normNum_def)
   1.111  
   1.112  lemma normNum_Nadd:
   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.118  lemma Nadd_normNum1[simp]:
   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.127  lemma Nadd_normNum2[simp]:
   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.136  lemma Nadd_assoc:
   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"