1 (* Title: HOL/Library/SCT_Misc.thy |
|
2 ID: $Id$ |
|
3 Author: Alexander Krauss, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Miscellaneous Tools for Size-Change Termination *} |
|
7 |
|
8 theory Misc_Tools |
|
9 imports Main |
|
10 begin |
|
11 |
|
12 subsection {* Searching in lists *} |
|
13 |
|
14 fun index_of :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" |
|
15 where |
|
16 "index_of [] c = 0" |
|
17 | "index_of (x#xs) c = (if x = c then 0 else Suc (index_of xs c))" |
|
18 |
|
19 lemma index_of_member: |
|
20 "(x \<in> set l) \<Longrightarrow> (l ! index_of l x = x)" |
|
21 by (induct l) auto |
|
22 |
|
23 lemma index_of_length: |
|
24 "(x \<in> set l) = (index_of l x < length l)" |
|
25 by (induct l) auto |
|
26 |
|
27 subsection {* Some reasoning tools *} |
|
28 |
|
29 lemma three_cases: |
|
30 assumes "a1 \<Longrightarrow> thesis" |
|
31 assumes "a2 \<Longrightarrow> thesis" |
|
32 assumes "a3 \<Longrightarrow> thesis" |
|
33 assumes "\<And>R. \<lbrakk>a1 \<Longrightarrow> R; a2 \<Longrightarrow> R; a3 \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
|
34 shows "thesis" |
|
35 using assms |
|
36 by auto |
|
37 |
|
38 |
|
39 subsection {* Sequences *} |
|
40 |
|
41 types |
|
42 'a sequence = "nat \<Rightarrow> 'a" |
|
43 |
|
44 |
|
45 subsubsection {* Increasing sequences *} |
|
46 |
|
47 definition |
|
48 increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where |
|
49 "increasing s = (\<forall>i j. i < j \<longrightarrow> s i < s j)" |
|
50 |
|
51 lemma increasing_strict: |
|
52 assumes "increasing s" |
|
53 assumes "i < j" |
|
54 shows "s i < s j" |
|
55 using assms |
|
56 unfolding increasing_def by simp |
|
57 |
|
58 lemma increasing_weak: |
|
59 assumes "increasing s" |
|
60 assumes "i \<le> j" |
|
61 shows "s i \<le> s j" |
|
62 using assms increasing_strict[of s i j] |
|
63 by (cases "i < j") auto |
|
64 |
|
65 lemma increasing_inc: |
|
66 assumes "increasing s" |
|
67 shows "n \<le> s n" |
|
68 proof (induct n) |
|
69 case 0 then show ?case by simp |
|
70 next |
|
71 case (Suc n) |
|
72 with increasing_strict [OF `increasing s`, of n "Suc n"] |
|
73 show ?case by auto |
|
74 qed |
|
75 |
|
76 lemma increasing_bij: |
|
77 assumes [simp]: "increasing s" |
|
78 shows "(s i < s j) = (i < j)" |
|
79 proof |
|
80 assume "s i < s j" |
|
81 show "i < j" |
|
82 proof (rule classical) |
|
83 assume "\<not> ?thesis" |
|
84 hence "j \<le> i" by arith |
|
85 with increasing_weak have "s j \<le> s i" by simp |
|
86 with `s i < s j` show ?thesis by simp |
|
87 qed |
|
88 qed (simp add:increasing_strict) |
|
89 |
|
90 |
|
91 subsubsection {* Sections induced by an increasing sequence *} |
|
92 |
|
93 abbreviation |
|
94 "section s i == {s i ..< s (Suc i)}" |
|
95 |
|
96 definition |
|
97 "section_of s n = (LEAST i. n < s (Suc i))" |
|
98 |
|
99 lemma section_help: |
|
100 assumes "increasing s" |
|
101 shows "\<exists>i. n < s (Suc i)" |
|
102 proof - |
|
103 have "n \<le> s n" |
|
104 using `increasing s` by (rule increasing_inc) |
|
105 also have "\<dots> < s (Suc n)" |
|
106 using `increasing s` increasing_strict by simp |
|
107 finally show ?thesis .. |
|
108 qed |
|
109 |
|
110 lemma section_of2: |
|
111 assumes "increasing s" |
|
112 shows "n < s (Suc (section_of s n))" |
|
113 unfolding section_of_def |
|
114 by (rule LeastI_ex) (rule section_help [OF `increasing s`]) |
|
115 |
|
116 lemma section_of1: |
|
117 assumes [simp, intro]: "increasing s" |
|
118 assumes "s i \<le> n" |
|
119 shows "s (section_of s n) \<le> n" |
|
120 proof (rule classical) |
|
121 let ?m = "section_of s n" |
|
122 |
|
123 assume "\<not> ?thesis" |
|
124 hence a: "n < s ?m" by simp |
|
125 |
|
126 have nonzero: "?m \<noteq> 0" |
|
127 proof |
|
128 assume "?m = 0" |
|
129 from increasing_weak have "s 0 \<le> s i" by simp |
|
130 also note `\<dots> \<le> n` |
|
131 finally show False using `?m = 0` `n < s ?m` by simp |
|
132 qed |
|
133 with a have "n < s (Suc (?m - 1))" by simp |
|
134 with Least_le have "?m \<le> ?m - 1" |
|
135 unfolding section_of_def . |
|
136 with nonzero show ?thesis by simp |
|
137 qed |
|
138 |
|
139 lemma section_of_known: |
|
140 assumes [simp]: "increasing s" |
|
141 assumes in_sect: "k \<in> section s i" |
|
142 shows "section_of s k = i" (is "?s = i") |
|
143 proof (rule classical) |
|
144 assume "\<not> ?thesis" |
|
145 |
|
146 hence "?s < i \<or> ?s > i" by arith |
|
147 thus ?thesis |
|
148 proof |
|
149 assume "?s < i" |
|
150 hence "Suc ?s \<le> i" by simp |
|
151 with increasing_weak have "s (Suc ?s) \<le> s i" by simp |
|
152 moreover have "k < s (Suc ?s)" using section_of2 by simp |
|
153 moreover from in_sect have "s i \<le> k" by simp |
|
154 ultimately show ?thesis by simp |
|
155 next |
|
156 assume "i < ?s" hence "Suc i \<le> ?s" by simp |
|
157 with increasing_weak have "s (Suc i) \<le> s ?s" by simp |
|
158 moreover |
|
159 from in_sect have "s i \<le> k" by simp |
|
160 with section_of1 have "s ?s \<le> k" by simp |
|
161 moreover from in_sect have "k < s (Suc i)" by simp |
|
162 ultimately show ?thesis by simp |
|
163 qed |
|
164 qed |
|
165 |
|
166 lemma in_section_of: |
|
167 assumes "increasing s" |
|
168 assumes "s i \<le> k" |
|
169 shows "k \<in> section s (section_of s k)" |
|
170 using assms |
|
171 by (auto intro:section_of1 section_of2) |
|
172 |
|
173 end |
|