equal
deleted
inserted
replaced
34 by auto |
34 by auto |
35 termination by (relation "measure (\<lambda>(a, b). nat (- a - b))") auto |
35 termination by (relation "measure (\<lambda>(a, b). nat (- a - b))") auto |
36 |
36 |
37 text{*algorithm for the general case @{term "b\<noteq>0"}*} |
37 text{*algorithm for the general case @{term "b\<noteq>0"}*} |
38 definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where |
38 definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where |
39 [code_inline]: "negateSnd = apsnd uminus" |
39 [code_unfold]: "negateSnd = apsnd uminus" |
40 |
40 |
41 definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where |
41 definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where |
42 --{*The full division algorithm considers all possible signs for a, b |
42 --{*The full division algorithm considers all possible signs for a, b |
43 including the special case @{text "a=0, b<0"} because |
43 including the special case @{text "a=0, b<0"} because |
44 @{term negDivAlg} requires @{term "a<0"}.*} |
44 @{term negDivAlg} requires @{term "a<0"}.*} |