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