1.1 --- a/src/HOL/Library/List_Prefix.thy	Thu May 06 12:43:00 2004 +0200
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu May 06 14:14:18 2004 +0200
     1.3 @@ -4,10 +4,7 @@
     1.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.5  *)
     1.6  
     1.7 -header {*
     1.8 -  \title{List prefixes and postfixes}
     1.9 -  \author{Tobias Nipkow and Markus Wenzel}
    1.10 -*}
    1.11 +header {* List prefixes and postfixes *}
    1.12  
    1.13  theory List_Prefix = Main:
    1.14  
    1.15 @@ -222,36 +219,43 @@
    1.16    postfix :: "'a list => 'a list => bool"  ("(_/ >= _)" [51, 50] 50)
    1.17    "xs >= ys == \<exists>zs. xs = zs @ ys"
    1.18  
    1.19 -lemma postfix_refl [simp, intro!]: "xs >= xs" by (auto simp add: postfix_def)
    1.20 -lemma postfix_trans: "\<lbrakk>xs >= ys; ys >= zs\<rbrakk> \<Longrightarrow> xs >= zs" 
    1.21 -         by (auto simp add: postfix_def)
    1.22 -lemma postfix_antisym: "\<lbrakk>xs >= ys; ys >= xs\<rbrakk> \<Longrightarrow> xs = ys" 
    1.23 -         by (auto simp add: postfix_def)
    1.24 +lemma postfix_refl [simp, intro!]: "xs >= xs"
    1.25 +  by (auto simp add: postfix_def)
    1.26 +lemma postfix_trans: "\<lbrakk>xs >= ys; ys >= zs\<rbrakk> \<Longrightarrow> xs >= zs"
    1.27 +  by (auto simp add: postfix_def)
    1.28 +lemma postfix_antisym: "\<lbrakk>xs >= ys; ys >= xs\<rbrakk> \<Longrightarrow> xs = ys"
    1.29 +  by (auto simp add: postfix_def)
    1.30  
    1.31 -lemma Nil_postfix [iff]: "xs >= []" by (simp add: postfix_def)
    1.32 -lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])"by (auto simp add:postfix_def)
    1.33 +lemma Nil_postfix [iff]: "xs >= []"
    1.34 +  by (simp add: postfix_def)
    1.35 +lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])"
    1.36 +  by (auto simp add:postfix_def)
    1.37  
    1.38 -lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys" by (auto simp add: postfix_def)
    1.39 -lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys" by (auto simp add: postfix_def)
    1.40 +lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys"
    1.41 +  by (auto simp add: postfix_def)
    1.42 +lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys"
    1.43 +  by (auto simp add: postfix_def)
    1.44  
    1.45 -lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs@xs >= ys" by(auto simp add: postfix_def)
    1.46 -lemma postfix_appendD: "xs >= zs@ys \<Longrightarrow> xs >= ys" by(auto simp add: postfix_def)
    1.47 +lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs @ xs >= ys"
    1.48 +  by (auto simp add: postfix_def)
    1.49 +lemma postfix_appendD: "xs >= zs @ ys \<Longrightarrow> xs >= ys"
    1.50 +  by(auto simp add: postfix_def)
    1.51  
    1.52  lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
    1.53 -by (induct zs, auto)
    1.54 +  by (induct zs, auto)
    1.55  lemma postfix_is_subset: "xs >= ys \<Longrightarrow> set ys \<subseteq> set xs"
    1.56 -by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
    1.57 +  by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
    1.58  
    1.59  lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >= ys"
    1.60 -by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
    1.61 +  by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
    1.62  lemma postfix_ConsD2: "x#xs >= y#ys \<Longrightarrow> xs >= ys"
    1.63 -by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
    1.64 +  by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
    1.65  
    1.66  lemma postfix2prefix: "(xs >= ys) = (rev ys <= rev xs)"
    1.67 -apply (unfold prefix_def postfix_def, safe)
    1.68 -apply (rule_tac x = "rev zs" in exI, simp)
    1.69 -apply (rule_tac x = "rev zs" in exI)
    1.70 -apply (rule rev_is_rev_conv [THEN iffD1], simp)
    1.71 -done
    1.72 +  apply (unfold prefix_def postfix_def, safe)
    1.73 +  apply (rule_tac x = "rev zs" in exI, simp)
    1.74 +  apply (rule_tac x = "rev zs" in exI)
    1.75 +  apply (rule rev_is_rev_conv [THEN iffD1], simp)
    1.76 +  done
    1.77  
    1.78  end