src/HOL/Library/List_Prefix.thy
changeset 18730 843da46f89ac
parent 18258 836491e9b7d5
child 19086 1b3780be6cc2
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Sat Jan 21 23:02:20 2006 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Sat Jan 21 23:02:21 2006 +0100
     1.3 @@ -21,13 +21,13 @@
     1.4    by intro_classes (auto simp add: prefix_def strict_prefix_def)
     1.5  
     1.6  lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
     1.7 -  by (unfold prefix_def) blast
     1.8 +  unfolding prefix_def by blast
     1.9  
    1.10  lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C"
    1.11 -  by (unfold prefix_def) blast
    1.12 +  unfolding prefix_def by blast
    1.13  
    1.14  lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
    1.15 -  by (unfold strict_prefix_def prefix_def) blast
    1.16 +  unfolding strict_prefix_def prefix_def by blast
    1.17  
    1.18  lemma strict_prefixE' [elim?]:
    1.19    assumes lt: "xs < ys"
    1.20 @@ -35,16 +35,16 @@
    1.21    shows C
    1.22  proof -
    1.23    from lt obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    1.24 -    by (unfold strict_prefix_def prefix_def) blast
    1.25 +    unfolding strict_prefix_def prefix_def by blast
    1.26    with r show ?thesis by (auto simp add: neq_Nil_conv)
    1.27  qed
    1.28  
    1.29  lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
    1.30 -  by (unfold strict_prefix_def) blast
    1.31 +  unfolding strict_prefix_def by blast
    1.32  
    1.33  lemma strict_prefixE [elim?]:
    1.34      "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C"
    1.35 -  by (unfold strict_prefix_def) blast
    1.36 +  unfolding strict_prefix_def by blast
    1.37  
    1.38  
    1.39  subsection {* Basic properties of prefixes *}
    1.40 @@ -160,17 +160,17 @@
    1.41    "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"
    1.42  
    1.43  lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
    1.44 -  by (unfold parallel_def) blast
    1.45 +  unfolding parallel_def by blast
    1.46  
    1.47  lemma parallelE [elim]:
    1.48      "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C"
    1.49 -  by (unfold parallel_def) blast
    1.50 +  unfolding parallel_def by blast
    1.51  
    1.52  theorem prefix_cases:
    1.53    "(xs \<le> ys ==> C) ==>
    1.54      (ys < xs ==> C) ==>
    1.55      (xs \<parallel> ys ==> C) ==> C"
    1.56 -  by (unfold parallel_def strict_prefix_def) blast
    1.57 +  unfolding parallel_def strict_prefix_def by blast
    1.58  
    1.59  theorem parallel_decomp:
    1.60    "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"