src/HOL/Enum.thy
changeset 60352 d46de31a50c4
parent 59867 58043346ca64
child 60429 d3d1e185cd63
     1.1 --- a/src/HOL/Enum.thy	Mon Jun 01 18:59:21 2015 +0200
     1.2 +++ b/src/HOL/Enum.thy	Mon Jun 01 18:59:21 2015 +0200
     1.3 @@ -585,12 +585,11 @@
     1.4  definition [simp]: "Groups.one = a\<^sub>1"
     1.5  definition [simp]: "op + = (\<lambda>_ _. a\<^sub>1)"
     1.6  definition [simp]: "op * = (\<lambda>_ _. a\<^sub>1)"
     1.7 -definition [simp]: "op div = (\<lambda>_ _. a\<^sub>1)" 
     1.8  definition [simp]: "op mod = (\<lambda>_ _. a\<^sub>1)" 
     1.9  definition [simp]: "abs = (\<lambda>_. a\<^sub>1)"
    1.10  definition [simp]: "sgn = (\<lambda>_. a\<^sub>1)"
    1.11  definition [simp]: "inverse = (\<lambda>_. a\<^sub>1)"
    1.12 -definition [simp]: "op / = (\<lambda>_ _. a\<^sub>1)"
    1.13 +definition [simp]: "divide = (\<lambda>_ _. a\<^sub>1)"
    1.14  
    1.15  instance by intro_classes(simp_all add: less_finite_1_def)
    1.16  end
    1.17 @@ -691,15 +690,14 @@
    1.18  definition "op - = (op + :: finite_2 \<Rightarrow> _)"
    1.19  definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    1.20  definition "inverse = (\<lambda>x :: finite_2. x)"
    1.21 -definition "op / = (op * :: finite_2 \<Rightarrow> _)"
    1.22 +definition "divide = (op * :: finite_2 \<Rightarrow> _)"
    1.23  definition "abs = (\<lambda>x :: finite_2. x)"
    1.24 -definition "op div = (op / :: finite_2 \<Rightarrow> _)"
    1.25  definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    1.26  definition "sgn = (\<lambda>x :: finite_2. x)"
    1.27  instance
    1.28  by intro_classes
    1.29    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
    1.30 -       inverse_finite_2_def divide_finite_2_def abs_finite_2_def div_finite_2_def mod_finite_2_def sgn_finite_2_def
    1.31 +       inverse_finite_2_def divide_finite_2_def abs_finite_2_def mod_finite_2_def sgn_finite_2_def
    1.32       split: finite_2.splits)
    1.33  end
    1.34  
    1.35 @@ -819,15 +817,14 @@
    1.36  definition "x - y = x + (- y :: finite_3)"
    1.37  definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
    1.38  definition "inverse = (\<lambda>x :: finite_3. x)" 
    1.39 -definition "x / y = x * inverse (y :: finite_3)"
    1.40 +definition "divide x y = x * inverse (y :: finite_3)"
    1.41  definition "abs = (\<lambda>x :: finite_3. x)"
    1.42 -definition "op div = (op / :: finite_3 \<Rightarrow> _)"
    1.43  definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
    1.44  definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
    1.45  instance
    1.46  by intro_classes
    1.47    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
    1.48 -       inverse_finite_3_def divide_finite_3_def abs_finite_3_def div_finite_3_def mod_finite_3_def sgn_finite_3_def
    1.49 +       inverse_finite_3_def divide_finite_3_def abs_finite_3_def mod_finite_3_def sgn_finite_3_def
    1.50         less_finite_3_def
    1.51       split: finite_3.splits)
    1.52  end