# HG changeset patch
# User wenzelm
# Date 1125495998 -7200
# Node ID 3bdf1dfcdee43fa40786da4a5f117a0274127cbe
# Parent  3a4d03d1a31bb609bc70ea351cfed745c94d9955
reactivate postfix by change of syntax;
tuned presentation;

diff -r 3a4d03d1a31b -r 3bdf1dfcdee4 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Wed Aug 31 15:46:37 2005 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Wed Aug 31 15:46:38 2005 +0200
@@ -30,11 +30,11 @@
   by (unfold strict_prefix_def prefix_def) blast
 
 lemma strict_prefixE' [elim?]:
-    "xs < ys ==> (!!z zs. ys = xs @ z # zs ==> C) ==> C"
+  assumes lt: "xs < ys"
+    and r: "!!z zs. ys = xs @ z # zs ==> C"
+  shows C
 proof -
-  assume r: "!!z zs. ys = xs @ z # zs ==> C"
-  assume "xs < ys"
-  then obtain us where "ys = xs @ us" and "xs \<noteq> ys"
+  from lt obtain us where "ys = xs @ us" and "xs \<noteq> ys"
     by (unfold strict_prefix_def prefix_def) blast
   with r show ?thesis by (auto simp add: neq_Nil_conv)
 qed
@@ -105,7 +105,7 @@
 qed
 
 lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
-by(simp add:prefix_def) blast
+  by (auto simp add: prefix_def)
 
 theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
   by (cases xs) (auto simp add: prefix_def)
@@ -130,28 +130,27 @@
 theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
   by (auto simp add: prefix_def)
 
-
 lemma prefix_same_cases:
- "\<lbrakk> (xs\<^isub>1::'a list) \<le> ys; xs\<^isub>2 \<le> ys \<rbrakk> \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
-apply(simp add:prefix_def)
-apply(erule exE)+
-apply(simp add: append_eq_append_conv_if split:if_splits)
- apply(rule disjI2)
- apply(rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI)
- apply clarify
- apply(drule sym)
- apply(insert append_take_drop_id[of "length xs\<^isub>2" xs\<^isub>1])
- apply simp
-apply(rule disjI1)
-apply(rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI)
-apply clarify
-apply(insert append_take_drop_id[of "length xs\<^isub>1" xs\<^isub>2])
-apply simp
-done
+    "(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
+  apply (simp add: prefix_def)
+  apply (erule exE)+
+  apply (simp add: append_eq_append_conv_if split: if_splits)
+   apply (rule disjI2)
+   apply (rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI)
+   apply clarify
+   apply (drule sym)
+   apply (insert append_take_drop_id [of "length xs\<^isub>2" xs\<^isub>1])
+   apply simp
+  apply (rule disjI1)
+  apply (rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI)
+  apply clarify
+  apply (insert append_take_drop_id [of "length xs\<^isub>1" xs\<^isub>2])
+  apply simp
+  done
 
 lemma set_mono_prefix:
- "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
-by(fastsimp simp add:prefix_def)
+    "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
+  by (auto simp add: prefix_def)
 
 
 subsection {* Parallel lists *}
@@ -215,48 +214,48 @@
 
 
 subsection {* Postfix order on lists *}
-(*
+
 constdefs
-  postfix :: "'a list => 'a list => bool"  ("(_/ >= _)" [51, 50] 50)
-  "xs >= ys == \<exists>zs. xs = zs @ ys"
+  postfix :: "'a list => 'a list => bool"  ("(_/ >>= _)" [51, 50] 50)
+  "xs >>= ys == \<exists>zs. xs = zs @ ys"
 
-lemma postfix_refl [simp, intro!]: "xs >= xs"
+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"
+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"
+lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys"
   by (auto simp add: postfix_def)
 
-lemma Nil_postfix [iff]: "xs >= []"
+lemma Nil_postfix [iff]: "xs >>= []"
   by (simp add: postfix_def)
-lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])"
+lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])"
   by (auto simp add:postfix_def)
 
-lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys"
+lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys"
   by (auto simp add: postfix_def)
-lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys"
+lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys"
   by (auto simp add: postfix_def)
 
-lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs @ xs >= ys"
+lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys"
   by (auto simp add: postfix_def)
-lemma postfix_appendD: "xs >= zs @ ys \<Longrightarrow> xs >= ys"
+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"
+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"
+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"
+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)"
+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, simp)
   apply (rule_tac x = "rev zs" in exI)
   apply (rule rev_is_rev_conv [THEN iffD1], simp)
   done
-*)
+
 end