equal
deleted
inserted
replaced
3115 |
3115 |
3116 lemma set_upto[simp]: "set[i..j] = {i..j}" |
3116 lemma set_upto[simp]: "set[i..j] = {i..j}" |
3117 proof(induct i j rule:upto.induct) |
3117 proof(induct i j rule:upto.induct) |
3118 case (1 i j) |
3118 case (1 i j) |
3119 from this show ?case |
3119 from this show ?case |
3120 unfolding upto.simps[of i j] simp_from_to[of i j] by auto |
3120 unfolding upto.simps[of i j] by auto |
3121 qed |
3121 qed |
3122 |
3122 |
3123 text{* Tail recursive version for code generation: *} |
3123 text{* Tail recursive version for code generation: *} |
3124 |
3124 |
3125 definition upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where |
3125 definition upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where |