src/HOL/Library/Prefix_Order.thy
changeset 63117 acb6d72fc42e
parent 61337 4645502c3c64
child 63465 d7610beb98bc
     1.1 --- a/src/HOL/Library/Prefix_Order.thy	Mon May 23 15:30:13 2016 +0200
     1.2 +++ b/src/HOL/Library/Prefix_Order.thy	Mon May 23 22:43:11 2016 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  instantiation list :: (type) order
     1.5  begin
     1.6  
     1.7 -definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
     1.8 +definition "(xs::'a list) \<le> ys \<equiv> prefix xs ys"
     1.9  definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
    1.10  
    1.11  instance
    1.12 @@ -19,23 +19,26 @@
    1.13  
    1.14  end
    1.15  
    1.16 -lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def]
    1.17 -lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def]
    1.18 -lemmas strict_prefixI' [intro?] = prefixI' [folded less_list_def]
    1.19 -lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def]
    1.20 -lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]
    1.21 -lemmas strict_prefixE [elim?] = prefixE [folded less_list_def]
    1.22 -lemmas Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def]
    1.23 -lemmas prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def]
    1.24 -lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def]
    1.25 -lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def]
    1.26 -lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def]
    1.27 -lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def]
    1.28 -lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def]
    1.29 -lemmas prefix_Cons = prefixeq_Cons [folded less_eq_list_def]
    1.30 -lemmas prefix_length_le = prefixeq_length_le [folded less_eq_list_def]
    1.31 -lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def]
    1.32 +lemma less_list_def': "(xs::'a list) < ys \<longleftrightarrow> strict_prefix xs ys"
    1.33 +by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le)
    1.34 +
    1.35 +lemmas prefixI [intro?] = prefixI [folded less_eq_list_def]
    1.36 +lemmas prefixE [elim?] = prefixE [folded less_eq_list_def]
    1.37 +lemmas strict_prefixI' [intro?] = strict_prefixI' [folded less_list_def']
    1.38 +lemmas strict_prefixE' [elim?] = strict_prefixE' [folded less_list_def']
    1.39 +lemmas strict_prefixI [intro?] = strict_prefixI [folded less_list_def']
    1.40 +lemmas strict_prefixE [elim?] = strict_prefixE [folded less_list_def']
    1.41 +lemmas Nil_prefix [iff] = Nil_prefix [folded less_eq_list_def]
    1.42 +lemmas prefix_Nil [simp] = prefix_Nil [folded less_eq_list_def]
    1.43 +lemmas prefix_snoc [simp] = prefix_snoc [folded less_eq_list_def]
    1.44 +lemmas Cons_prefix_Cons [simp] = Cons_prefix_Cons [folded less_eq_list_def]
    1.45 +lemmas same_prefix_prefix [simp] = same_prefix_prefix [folded less_eq_list_def]
    1.46 +lemmas same_prefix_nil [iff] = same_prefix_nil [folded less_eq_list_def]
    1.47 +lemmas prefix_prefix [simp] = prefix_prefix [folded less_eq_list_def]
    1.48 +lemmas prefix_Cons = prefix_Cons [folded less_eq_list_def]
    1.49 +lemmas prefix_length_le = prefix_length_le [folded less_eq_list_def]
    1.50 +lemmas strict_prefix_simps [simp, code] = strict_prefix_simps [folded less_list_def']
    1.51  lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] =
    1.52 -  not_prefixeq_induct [folded less_eq_list_def]
    1.53 +  not_prefix_induct [folded less_eq_list_def]
    1.54  
    1.55  end