1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7section "Word Lemmas that use List Prefix-Order"
8
9(* The AFP does not includes this theory to avoid polluting the class name
10   space with the List prefix order. New lemmas should be proved with
11   explicit prefix/strict_prefix in Word_Lemmas and then lifted here *)
12
13theory Word_Lemmas_Prefix
14imports
15  Word_Lemmas
16  Word_Lemmas_Internal
17  "HOL-Library.Prefix_Order"
18begin
19
20lemmas bl_pad_to_prefix = bl_pad_to_prefix[folded less_eq_list_def]
21lemmas sublist_equal_part = sublist_equal_part[folded less_eq_list_def]
22lemmas not_prefix_longer = not_prefix_longer[folded less_eq_list_def]
23lemmas map_prefixI = map_prefixI[folded less_eq_list_def]
24lemmas take_prefix = take_prefix[folded less_eq_list_def]
25lemmas take_is_prefix = take_is_prefix[folded less_eq_list_def]
26
27lemmas prefix_length_less = prefix_length_less[folded less_list_def']
28lemmas take_less = take_strict_prefix[folded less_list_def']
29
30end
31