583 one, modulo, sgn, inverse}" |
583 one, modulo, sgn, inverse}" |
584 begin |
584 begin |
585 definition [simp]: "Groups.zero = a\<^sub>1" |
585 definition [simp]: "Groups.zero = a\<^sub>1" |
586 definition [simp]: "Groups.one = a\<^sub>1" |
586 definition [simp]: "Groups.one = a\<^sub>1" |
587 definition [simp]: "(+) = (\<lambda>_ _. a\<^sub>1)" |
587 definition [simp]: "(+) = (\<lambda>_ _. a\<^sub>1)" |
588 definition [simp]: "( * ) = (\<lambda>_ _. a\<^sub>1)" |
588 definition [simp]: "(*) = (\<lambda>_ _. a\<^sub>1)" |
589 definition [simp]: "(mod) = (\<lambda>_ _. a\<^sub>1)" |
589 definition [simp]: "(mod) = (\<lambda>_ _. a\<^sub>1)" |
590 definition [simp]: "abs = (\<lambda>_. a\<^sub>1)" |
590 definition [simp]: "abs = (\<lambda>_. a\<^sub>1)" |
591 definition [simp]: "sgn = (\<lambda>_. a\<^sub>1)" |
591 definition [simp]: "sgn = (\<lambda>_. a\<^sub>1)" |
592 definition [simp]: "inverse = (\<lambda>_. a\<^sub>1)" |
592 definition [simp]: "inverse = (\<lambda>_. a\<^sub>1)" |
593 definition [simp]: "divide = (\<lambda>_ _. a\<^sub>1)" |
593 definition [simp]: "divide = (\<lambda>_ _. a\<^sub>1)" |
688 definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)" |
688 definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)" |
689 definition "uminus = (\<lambda>x :: finite_2. x)" |
689 definition "uminus = (\<lambda>x :: finite_2. x)" |
690 definition "(-) = ((+) :: finite_2 \<Rightarrow> _)" |
690 definition "(-) = ((+) :: finite_2 \<Rightarrow> _)" |
691 definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)" |
691 definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)" |
692 definition "inverse = (\<lambda>x :: finite_2. x)" |
692 definition "inverse = (\<lambda>x :: finite_2. x)" |
693 definition "divide = (( * ) :: finite_2 \<Rightarrow> _)" |
693 definition "divide = ((*) :: finite_2 \<Rightarrow> _)" |
694 definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)" |
694 definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)" |
695 definition "abs = (\<lambda>x :: finite_2. x)" |
695 definition "abs = (\<lambda>x :: finite_2. x)" |
696 definition "sgn = (\<lambda>x :: finite_2. x)" |
696 definition "sgn = (\<lambda>x :: finite_2. x)" |
697 instance |
697 instance |
698 by standard |
698 by standard |