removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy

--- a/src/HOL/Library/List_Prefix.thy	Mon Apr 12 19:54:09 2004 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Mon Apr 12 19:54:32 2004 +0200
@@ -5,7 +5,7 @@
 *)
 
 header {*
-  \title{List prefixes}
+  \title{List prefixes and postfixes}
   \author{Tobias Nipkow and Markus Wenzel}
 *}
 
@@ -215,4 +215,43 @@
   qed
 qed
 
+
+subsection {* Postfix order on lists *}
+
+constdefs
+  postfix :: "'a list => 'a list => bool"  ("(_/ >= _)" [51, 50] 50)
+  "xs >= ys == \<exists>zs. xs = zs @ ys"
+
+lemma postfix_refl [simp, intro!]: "xs >= xs" by (auto simp add: postfix_def)
+lemma postfix_trans: "\<lbrakk>xs >= ys; ys >= zs\<rbrakk> \<Longrightarrow> xs >= zs" 
+         by (auto simp add: postfix_def)
+lemma postfix_antisym: "\<lbrakk>xs >= ys; ys >= xs\<rbrakk> \<Longrightarrow> xs = ys" 
+         by (auto simp add: postfix_def)
+
+lemma Nil_postfix [iff]: "xs >= []" by (simp add: postfix_def)
+lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])"by (auto simp add:postfix_def)
+
+lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys" by (auto simp add: postfix_def)
+lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys" by (auto simp add: postfix_def)
+
+lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs@xs >= ys" by(auto simp add: postfix_def)
+lemma postfix_appendD: "xs >= zs@ys \<Longrightarrow> xs >= ys" by(auto simp add: postfix_def)
+
+lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
+by (induct zs, auto)
+lemma postfix_is_subset: "xs >= ys \<Longrightarrow> set ys \<subseteq> set xs"
+by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
+
+lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >= ys"
+by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
+lemma postfix_ConsD2: "x#xs >= y#ys \<Longrightarrow> xs >= ys"
+by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
+
+lemma postfix2prefix: "(xs >= ys) = (rev ys <= rev xs)"
+apply (unfold prefix_def postfix_def, safe)
+apply (rule_tac x = "rev zs" in exI, simp)
+apply (rule_tac x = "rev zs" in exI)
+apply (rule rev_is_rev_conv [THEN iffD1], simp)
+done
+
 end

--- a/src/HOL/List.thy	Mon Apr 12 19:54:09 2004 +0200
+++ b/src/HOL/List.thy	Mon Apr 12 19:54:32 2004 +0200
@@ -18,13 +18,11 @@
   concat:: "'a list list => 'a list"
   foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
   foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
-  fold_rel :: "('a * 'c * 'a) set => ('a * 'c list * 'a) set"
   hd:: "'a list => 'a"
   tl:: "'a list => 'a list"
   last:: "'a list => 'a"
   butlast :: "'a list => 'a list"
   set :: "'a list => 'a set"
-  o2l :: "'a option => 'a list"
   list_all:: "('a => bool) => ('a list => bool)"
   list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool"
   map :: "('a=>'b) => ('a list => 'b list)"
@@ -42,10 +40,6 @@
   null:: "'a list => bool"
   "distinct":: "'a list => bool"
   replicate :: "nat => 'a => 'a list"
-  postfix :: "'a list => 'a list => bool"
-
-syntax (xsymbols)
-  postfix :: "'a list => 'a list => bool"             ("(_/ \<sqsupseteq> _)" [51, 51] 50)
 
 nonterminals lupdbinds lupdbind
 
@@ -114,9 +108,6 @@
 "set [] = {}"
 "set (x#xs) = insert x (set xs)"
 primrec
- "o2l  None    = []"
- "o2l (Some x) = [x]"
-primrec
 list_all_Nil:"list_all P [] = True"
 list_all_Cons: "list_all P (x#xs) = (P(x) \<and> list_all P xs)"
 primrec
@@ -183,8 +174,6 @@
 replicate_0: "replicate 0 x = []"
 replicate_Suc: "replicate (Suc n) x = x # replicate n x"
 defs
- postfix_def: "postfix xs ys == \<exists>zs. xs = zs @ ys"
-defs
  list_all2_def:
  "list_all2 P xs ys == length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)"
 
@@ -1241,21 +1230,6 @@
 by (induct ns) auto
 
 
-subsection {* folding a relation over a list *}
-
-(*"fold_rel R cs \<equiv> foldl (%r c. r O {(x,y). (c,x,y):R}) Id cs"*)
-inductive "fold_rel R" intros
-  Nil:  "(a, [],a) : fold_rel R"
-  Cons: "[|(a,x,b) : R; (b,xs,c) : fold_rel R|] ==> (a,x#xs,c) : fold_rel R"
-inductive_cases fold_rel_elim_case [elim!]:
-   "(a, [] , b) : fold_rel R"
-   "(a, x#xs, b) : fold_rel R"
-
-lemma fold_rel_Nil [intro!]: "a = b ==> (a, [], b) : fold_rel R" 
-by (simp add: fold_rel.Nil)
-declare fold_rel.Cons [intro!]
-
-
 subsection {* @{text upto} *}
 
 lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])"
@@ -1444,31 +1418,6 @@
 by (simp add: set_replicate_conv_if split: split_if_asm)
 
 
-subsection {* @{text postfix} *}
-
-lemma postfix_refl [simp, intro!]: "xs \<sqsupseteq> xs" by (auto simp add: postfix_def)
-lemma postfix_trans: "\<lbrakk>xs \<sqsupseteq> ys; ys \<sqsupseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsupseteq> zs" 
-         by (auto simp add: postfix_def)
-lemma postfix_antisym: "\<lbrakk>xs \<sqsupseteq> ys; ys \<sqsupseteq> xs\<rbrakk> \<Longrightarrow> xs = ys" 
-         by (auto simp add: postfix_def)
-
-lemma postfix_emptyI [simp, intro!]: "xs \<sqsupseteq> []" by (auto simp add: postfix_def)
-lemma postfix_emptyD [dest!]: "[] \<sqsupseteq> xs \<Longrightarrow> xs = []"by(auto simp add:postfix_def)
-lemma postfix_ConsI: "xs \<sqsupseteq> ys \<Longrightarrow> x#xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
-lemma postfix_ConsD: "xs \<sqsupseteq> y#ys \<Longrightarrow> xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
-lemma postfix_appendI: "xs \<sqsupseteq> ys \<Longrightarrow> zs@xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
-lemma postfix_appendD: "xs \<sqsupseteq> zs@ys \<Longrightarrow> xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
-
-lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
-by (induct zs, auto)
-lemma postfix_is_subset: "xs \<sqsupseteq> ys \<Longrightarrow> set ys \<subseteq> set xs"
-by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
-
-lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs \<sqsupseteq> ys"
-by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
-lemma postfix_ConsD2: "x#xs \<sqsupseteq> y#ys \<Longrightarrow> xs \<sqsupseteq> ys"
-by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
-
 subsection {* Lexicographic orderings on lists *}
 
 lemma wf_lexn: "wf r ==> wf (lexn r n)"