equal
deleted
inserted
replaced
8 theory Termination |
8 theory Termination |
9 imports Main "HOL-Library.Multiset" |
9 imports Main "HOL-Library.Multiset" |
10 begin |
10 begin |
11 |
11 |
12 subsection \<open>Manually giving termination relations using \<open>relation\<close> and |
12 subsection \<open>Manually giving termination relations using \<open>relation\<close> and |
13 @{term measure}\<close> |
13 \<^term>\<open>measure\<close>\<close> |
14 |
14 |
15 function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
15 function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
16 where |
16 where |
17 "sum i N = (if i > N then 0 else i + sum (Suc i) N)" |
17 "sum i N = (if i > N then 0 else i + sum (Suc i) N)" |
18 by pat_completeness auto |
18 by pat_completeness auto |