equal
deleted
inserted
replaced
165 lemma %quote [code_pred_intro]: |
165 lemma %quote [code_pred_intro]: |
166 "append xs (a # v) ys \<Longrightarrow> lexordp r xs ys" |
166 "append xs (a # v) ys \<Longrightarrow> lexordp r xs ys" |
167 (*<*)unfolding lexordp_def by (auto simp add: append)(*>*) |
167 (*<*)unfolding lexordp_def by (auto simp add: append)(*>*) |
168 |
168 |
169 lemma %quote [code_pred_intro]: |
169 lemma %quote [code_pred_intro]: |
170 "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b \<Longrightarrow> a\<noteq>b |
170 "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b |
171 \<Longrightarrow> lexordp r xs ys" |
171 \<Longrightarrow> lexordp r xs ys" |
172 (*<*)unfolding lexordp_def append apply simp |
172 (*<*)unfolding lexordp_def append apply simp |
173 apply (rule disjI2) by auto(*>*) |
173 apply (rule disjI2) by auto(*>*) |
174 |
174 |
175 code_pred %quote lexordp |
175 code_pred %quote lexordp |
177 fix r xs ys |
177 fix r xs ys |
178 assume lexord: "lexordp r xs ys" |
178 assume lexord: "lexordp r xs ys" |
179 assume 1: "\<And>r' xs' ys' a v. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys' |
179 assume 1: "\<And>r' xs' ys' a v. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys' |
180 \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis" |
180 \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis" |
181 assume 2: "\<And>r' xs' ys' u a v b w. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys' |
181 assume 2: "\<And>r' xs' ys' u a v b w. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys' |
182 \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> a\<noteq>b \<Longrightarrow> thesis" |
182 \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> thesis" |
183 { |
183 { |
184 assume "\<exists>a v. ys = xs @ a # v" |
184 assume "\<exists>a v. ys = xs @ a # v" |
185 from this 1 have thesis |
185 from this 1 have thesis |
186 by (fastforce simp add: append) |
186 by (fastforce simp add: append) |
187 } moreover |
187 } moreover |
188 { |
188 { |
189 assume "\<exists>u a b v w. r a b \<and> a\<noteq>b \<and> xs = u @ a # v \<and> ys = u @ b # w" |
189 assume "\<exists>u a b v w. r a b \<and> xs = u @ a # v \<and> ys = u @ b # w" |
190 from this 2 have thesis by (fastforce simp add: append) |
190 from this 2 have thesis by (fastforce simp add: append) |
191 } moreover |
191 } moreover |
192 note lexord |
192 note lexord |
193 ultimately show thesis |
193 ultimately show thesis |
194 unfolding lexordp_def |
194 unfolding lexordp_def |