131 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
132 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
132 where |
133 where |
133 "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> |
134 "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> |
134 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
135 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
135 |
136 |
|
137 lemma test: |
|
138 shows "v1 \<sqsubset>val p v2 \<longleftrightarrow> |
|
139 pflat_len v1 p > pflat_len v2 p \<and> |
|
140 (\<forall>q \<in> Pos v1. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q) \<and> |
|
141 (\<forall>q \<in> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
|
142 unfolding PosOrd_def |
|
143 apply(auto) |
|
144 done |
136 |
145 |
137 |
146 |
138 definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60) |
147 definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60) |
139 where |
148 where |
140 "v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2" |
149 "v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2" |
255 using assms |
262 using assms |
256 apply(rule_tac PosOrd_shorterI) |
263 apply(rule_tac PosOrd_shorterI) |
257 unfolding prefix_list_def sprefix_list_def |
264 unfolding prefix_list_def sprefix_list_def |
258 by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear) |
265 by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear) |
259 |
266 |
|
267 lemma pflat_len_inside: |
|
268 assumes "pflat_len v2 p < pflat_len v1 p" |
|
269 shows "p \<in> Pos v1" |
|
270 using assms |
|
271 unfolding pflat_len_def |
|
272 by (auto split: if_splits) |
260 |
273 |
261 lemma PosOrd_Left_Right: |
274 lemma PosOrd_Left_Right: |
262 assumes "flat v1 = flat v2" |
275 assumes "flat v1 = flat v2" |
263 shows "Left v1 :\<sqsubset>val Right v2" |
276 shows "Left v1 :\<sqsubset>val Right v2" |
264 unfolding PosOrd_ex_def |
277 unfolding PosOrd_ex_def |
265 apply(rule_tac x="[0]" in exI) |
278 apply(rule_tac x="[0]" in exI) |
266 using assms |
279 apply(auto simp add: PosOrd_def pflat_len_simps assms) |
267 apply(auto simp add: PosOrd_def pflat_len_simps) |
280 done |
268 done |
281 |
|
282 lemma PosOrd_LeftE: |
|
283 assumes "Left v1 :\<sqsubset>val Left v2" "flat v1 = flat v2" |
|
284 shows "v1 :\<sqsubset>val v2" |
|
285 using assms |
|
286 unfolding PosOrd_ex_def test |
|
287 apply(auto simp add: pflat_len_simps) |
|
288 apply(frule pflat_len_inside) |
|
289 apply(auto simp add: pflat_len_simps) |
|
290 by (metis lex_simps(3) pflat_len_simps(3)) |
|
291 |
|
292 lemma PosOrd_LeftI: |
|
293 assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2" |
|
294 shows "Left v1 :\<sqsubset>val Left v2" |
|
295 using assms |
|
296 unfolding PosOrd_ex_def test |
|
297 apply(auto simp add: pflat_len_simps) |
|
298 by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3)) |
269 |
299 |
270 lemma PosOrd_Left_eq: |
300 lemma PosOrd_Left_eq: |
271 assumes "flat v = flat v'" |
301 assumes "flat v1 = flat v2" |
272 shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'" |
302 shows "Left v1 :\<sqsubset>val Left v2 \<longleftrightarrow> v1 :\<sqsubset>val v2" |
273 using assms |
303 using assms PosOrd_LeftE PosOrd_LeftI |
274 unfolding PosOrd_ex_def |
304 by blast |
275 apply(auto) |
305 |
276 apply(case_tac p) |
306 |
277 apply(simp add: PosOrd_def pflat_len_simps) |
307 lemma PosOrd_RightE: |
278 apply(case_tac a) |
308 assumes "Right v1 :\<sqsubset>val Right v2" "flat v1 = flat v2" |
279 apply(simp add: PosOrd_def pflat_len_simps) |
309 shows "v1 :\<sqsubset>val v2" |
280 apply(rule_tac x="list" in exI) |
310 using assms |
281 apply(auto simp add: PosOrd_def pflat_len_simps)[1] |
311 unfolding PosOrd_ex_def test |
282 apply (smt Un_def lex_list.intros(2) mem_Collect_eq pflat_len_simps(3)) |
312 apply(auto simp add: pflat_len_simps) |
283 apply (smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(3)) |
313 apply(frule pflat_len_inside) |
284 apply(auto simp add: PosOrd_def pflat_len_outside)[1] |
314 apply(auto simp add: pflat_len_simps) |
285 apply(rule_tac x="0#p" in exI) |
315 by (metis lex_simps(3) pflat_len_simps(5)) |
286 apply(auto simp add: PosOrd_def pflat_len_simps) |
|
287 done |
|
288 |
|
289 |
316 |
290 lemma PosOrd_RightI: |
317 lemma PosOrd_RightI: |
291 assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
318 assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2" |
292 shows "Right v :\<sqsubset>val Right v'" |
319 shows "Right v1 :\<sqsubset>val Right v2" |
293 using assms(1) |
320 using assms |
294 unfolding PosOrd_ex_def |
321 unfolding PosOrd_ex_def test |
295 apply(auto) |
|
296 apply(rule_tac x="Suc 0#p" in exI) |
|
297 using assms(2) |
|
298 apply(auto simp add: PosOrd_def pflat_len_simps) |
|
299 done |
|
300 |
|
301 lemma PosOrd_RightE: |
|
302 assumes "Right v1 :\<sqsubset>val Right v2" |
|
303 shows "v1 :\<sqsubset>val v2" |
|
304 using assms |
|
305 apply(simp add: PosOrd_ex_def) |
|
306 apply(erule exE) |
|
307 apply(case_tac p) |
|
308 apply(simp add: PosOrd_def) |
|
309 apply(auto simp add: pflat_len_simps) |
322 apply(auto simp add: pflat_len_simps) |
310 apply(rule_tac x="[]" in exI) |
323 by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5)) |
311 apply(simp add: Pos_empty pflat_len_simps) |
324 |
312 apply(case_tac a) |
325 |
313 apply(simp add: pflat_len_def PosOrd_def) |
326 lemma PosOrd_Right_eq: |
314 apply(case_tac nat) |
327 assumes "flat v1 = flat v2" |
315 prefer 2 |
328 shows "Right v1 :\<sqsubset>val Right v2 \<longleftrightarrow> v1 :\<sqsubset>val v2" |
316 apply(simp add: pflat_len_def PosOrd_def) |
329 using assms PosOrd_RightE PosOrd_RightI |
317 apply(auto simp add: pflat_len_simps PosOrd_def) |
330 by blast |
318 apply(rule_tac x="list" in exI) |
|
319 apply(auto) |
|
320 apply(drule_tac x="Suc 0#q" in bspec) |
|
321 apply(simp) |
|
322 apply(simp add: pflat_len_simps) |
|
323 apply(drule_tac x="Suc 0#q" in bspec) |
|
324 apply(simp) |
|
325 apply(simp add: pflat_len_simps) |
|
326 done |
|
327 |
331 |
328 |
332 |
329 lemma PosOrd_SeqI1: |
333 lemma PosOrd_SeqI1: |
330 assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
334 assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
331 shows "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" |
335 shows "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" |