equal
deleted
inserted
replaced
5 fun |
5 fun |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
7 where |
7 where |
8 "intrel (x, y) (u, v) = (x + v = u + y)" |
8 "intrel (x, y) (u, v) = (x + v = u + y)" |
9 |
9 |
10 quotient my_int = "nat \<times> nat" / intrel |
10 quotient_type my_int = "nat \<times> nat" / intrel |
11 apply(unfold equivp_def) |
11 apply(unfold equivp_def) |
12 apply(auto simp add: mem_def expand_fun_eq) |
12 apply(auto simp add: mem_def expand_fun_eq) |
13 done |
13 done |
14 |
14 |
15 thm quot_equiv |
15 thm quot_equiv |