360 |
360 |
361 lemma Longest_common_prefix_Nil: "[] \<in> L \<Longrightarrow> Longest_common_prefix L = []" |
361 lemma Longest_common_prefix_Nil: "[] \<in> L \<Longrightarrow> Longest_common_prefix L = []" |
362 using Longest_common_prefix_prefix prefix_Nil by blast |
362 using Longest_common_prefix_prefix prefix_Nil by blast |
363 |
363 |
364 lemma Longest_common_prefix_image_Cons: "L \<noteq> {} \<Longrightarrow> |
364 lemma Longest_common_prefix_image_Cons: "L \<noteq> {} \<Longrightarrow> |
365 Longest_common_prefix (op # x ` L) = x # Longest_common_prefix L" |
365 Longest_common_prefix ((#) x ` L) = x # Longest_common_prefix L" |
366 apply(rule Longest_common_prefix_eq) |
366 apply(rule Longest_common_prefix_eq) |
367 apply(simp) |
367 apply(simp) |
368 apply (simp add: Longest_common_prefix_prefix) |
368 apply (simp add: Longest_common_prefix_prefix) |
369 apply simp |
369 apply simp |
370 by(metis Longest_common_prefix_longest[of L] Cons_prefix_Cons Nitpick.size_list_simp(2) |
370 by(metis Longest_common_prefix_longest[of L] Cons_prefix_Cons Nitpick.size_list_simp(2) |
371 Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc) |
371 Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc) |
372 |
372 |
373 lemma Longest_common_prefix_eq_Cons: assumes "L \<noteq> {}" "[] \<notin> L" "\<forall>xs\<in>L. hd xs = x" |
373 lemma Longest_common_prefix_eq_Cons: assumes "L \<noteq> {}" "[] \<notin> L" "\<forall>xs\<in>L. hd xs = x" |
374 shows "Longest_common_prefix L = x # Longest_common_prefix {ys. x#ys \<in> L}" |
374 shows "Longest_common_prefix L = x # Longest_common_prefix {ys. x#ys \<in> L}" |
375 proof - |
375 proof - |
376 have "L = op # x ` {ys. x#ys \<in> L}" using assms(2,3) |
376 have "L = (#) x ` {ys. x#ys \<in> L}" using assms(2,3) |
377 by (auto simp: image_def)(metis hd_Cons_tl) |
377 by (auto simp: image_def)(metis hd_Cons_tl) |
378 thus ?thesis |
378 thus ?thesis |
379 by (metis Longest_common_prefix_image_Cons image_is_empty assms(1)) |
379 by (metis Longest_common_prefix_image_Cons image_is_empty assms(1)) |
380 qed |
380 qed |
381 |
381 |
1209 sublist xs ys \<or> sublist xs zs \<or> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> suffix xs1 ys \<and> prefix xs2 zs)" |
1209 sublist xs ys \<or> sublist xs zs \<or> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> suffix xs1 ys \<and> prefix xs2 zs)" |
1210 by (auto simp: sublist_altdef prefix_append suffix_append) |
1210 by (auto simp: sublist_altdef prefix_append suffix_append) |
1211 |
1211 |
1212 primrec sublists :: "'a list \<Rightarrow> 'a list list" where |
1212 primrec sublists :: "'a list \<Rightarrow> 'a list list" where |
1213 "sublists [] = [[]]" |
1213 "sublists [] = [[]]" |
1214 | "sublists (x # xs) = sublists xs @ map (op # x) (prefixes xs)" |
1214 | "sublists (x # xs) = sublists xs @ map ((#) x) (prefixes xs)" |
1215 |
1215 |
1216 lemma in_set_sublists [simp]: "xs \<in> set (sublists ys) \<longleftrightarrow> sublist xs ys" |
1216 lemma in_set_sublists [simp]: "xs \<in> set (sublists ys) \<longleftrightarrow> sublist xs ys" |
1217 by (induction ys arbitrary: xs) (auto simp: sublist_Cons_right prefix_Cons) |
1217 by (induction ys arbitrary: xs) (auto simp: sublist_Cons_right prefix_Cons) |
1218 |
1218 |
1219 lemma set_sublists_eq: "set (sublists xs) = {ys. sublist ys xs}" |
1219 lemma set_sublists_eq: "set (sublists xs) = {ys. sublist ys xs}" |
1311 (auto simp: list_emb_code List.null_def split: list.splits) |
1311 (auto simp: list_emb_code List.null_def split: list.splits) |
1312 qed |
1312 qed |
1313 |
1313 |
1314 lemma prefix_transfer [transfer_rule]: |
1314 lemma prefix_transfer [transfer_rule]: |
1315 assumes [transfer_rule]: "bi_unique A" |
1315 assumes [transfer_rule]: "bi_unique A" |
1316 shows "(list_all2 A ===> list_all2 A ===> op =) prefix prefix" |
1316 shows "(list_all2 A ===> list_all2 A ===> (=)) prefix prefix" |
1317 unfolding prefix_primrec by transfer_prover |
1317 unfolding prefix_primrec by transfer_prover |
1318 |
1318 |
1319 lemma suffix_transfer [transfer_rule]: |
1319 lemma suffix_transfer [transfer_rule]: |
1320 assumes [transfer_rule]: "bi_unique A" |
1320 assumes [transfer_rule]: "bi_unique A" |
1321 shows "(list_all2 A ===> list_all2 A ===> op =) suffix suffix" |
1321 shows "(list_all2 A ===> list_all2 A ===> (=)) suffix suffix" |
1322 unfolding suffix_to_prefix [abs_def] by transfer_prover |
1322 unfolding suffix_to_prefix [abs_def] by transfer_prover |
1323 |
1323 |
1324 lemma sublist_transfer [transfer_rule]: |
1324 lemma sublist_transfer [transfer_rule]: |
1325 assumes [transfer_rule]: "bi_unique A" |
1325 assumes [transfer_rule]: "bi_unique A" |
1326 shows "(list_all2 A ===> list_all2 A ===> op =) sublist sublist" |
1326 shows "(list_all2 A ===> list_all2 A ===> (=)) sublist sublist" |
1327 unfolding sublist_primrec by transfer_prover |
1327 unfolding sublist_primrec by transfer_prover |
1328 |
1328 |
1329 lemma parallel_transfer [transfer_rule]: |
1329 lemma parallel_transfer [transfer_rule]: |
1330 assumes [transfer_rule]: "bi_unique A" |
1330 assumes [transfer_rule]: "bi_unique A" |
1331 shows "(list_all2 A ===> list_all2 A ===> op =) parallel parallel" |
1331 shows "(list_all2 A ===> list_all2 A ===> (=)) parallel parallel" |
1332 unfolding parallel_def by transfer_prover |
1332 unfolding parallel_def by transfer_prover |
1333 |
1333 |
1334 |
1334 |
1335 |
1335 |
1336 lemma list_emb_transfer [transfer_rule]: |
1336 lemma list_emb_transfer [transfer_rule]: |
1337 "((A ===> A ===> op =) ===> list_all2 A ===> list_all2 A ===> op =) list_emb list_emb" |
1337 "((A ===> A ===> (=)) ===> list_all2 A ===> list_all2 A ===> (=)) list_emb list_emb" |
1338 unfolding list_emb_primrec by transfer_prover |
1338 unfolding list_emb_primrec by transfer_prover |
1339 |
1339 |
1340 lemma strict_prefix_transfer [transfer_rule]: |
1340 lemma strict_prefix_transfer [transfer_rule]: |
1341 assumes [transfer_rule]: "bi_unique A" |
1341 assumes [transfer_rule]: "bi_unique A" |
1342 shows "(list_all2 A ===> list_all2 A ===> op =) strict_prefix strict_prefix" |
1342 shows "(list_all2 A ===> list_all2 A ===> (=)) strict_prefix strict_prefix" |
1343 unfolding strict_prefix_def by transfer_prover |
1343 unfolding strict_prefix_def by transfer_prover |
1344 |
1344 |
1345 lemma strict_suffix_transfer [transfer_rule]: |
1345 lemma strict_suffix_transfer [transfer_rule]: |
1346 assumes [transfer_rule]: "bi_unique A" |
1346 assumes [transfer_rule]: "bi_unique A" |
1347 shows "(list_all2 A ===> list_all2 A ===> op =) strict_suffix strict_suffix" |
1347 shows "(list_all2 A ===> list_all2 A ===> (=)) strict_suffix strict_suffix" |
1348 unfolding strict_suffix_def by transfer_prover |
1348 unfolding strict_suffix_def by transfer_prover |
1349 |
1349 |
1350 lemma strict_subseq_transfer [transfer_rule]: |
1350 lemma strict_subseq_transfer [transfer_rule]: |
1351 assumes [transfer_rule]: "bi_unique A" |
1351 assumes [transfer_rule]: "bi_unique A" |
1352 shows "(list_all2 A ===> list_all2 A ===> op =) strict_subseq strict_subseq" |
1352 shows "(list_all2 A ===> list_all2 A ===> (=)) strict_subseq strict_subseq" |
1353 unfolding strict_subseq_def by transfer_prover |
1353 unfolding strict_subseq_def by transfer_prover |
1354 |
1354 |
1355 lemma strict_sublist_transfer [transfer_rule]: |
1355 lemma strict_sublist_transfer [transfer_rule]: |
1356 assumes [transfer_rule]: "bi_unique A" |
1356 assumes [transfer_rule]: "bi_unique A" |
1357 shows "(list_all2 A ===> list_all2 A ===> op =) strict_sublist strict_sublist" |
1357 shows "(list_all2 A ===> list_all2 A ===> (=)) strict_sublist strict_sublist" |
1358 unfolding strict_sublist_def by transfer_prover |
1358 unfolding strict_sublist_def by transfer_prover |
1359 |
1359 |
1360 lemma prefixes_transfer [transfer_rule]: |
1360 lemma prefixes_transfer [transfer_rule]: |
1361 assumes [transfer_rule]: "bi_unique A" |
1361 assumes [transfer_rule]: "bi_unique A" |
1362 shows "(list_all2 A ===> list_all2 (list_all2 A)) prefixes prefixes" |
1362 shows "(list_all2 A ===> list_all2 (list_all2 A)) prefixes prefixes" |