# HG changeset patch
# User wenzelm
# Date 972491481 -7200
# Node ID 4362e906b7450c9ba271f4a50d17917ead239309
# Parent  a9898d89a6341696ae780b30c3c344000670f2ca
"List prefixes" library theory (replaces old Lex/Prefix);

diff -r a9898d89a634 -r 4362e906b745 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Oct 25 18:25:41 2000 +0200
+++ b/src/HOL/IsaMakefile	Wed Oct 25 18:31:21 2000 +0200
@@ -162,9 +162,9 @@
 HOL-Library: HOL $(LOG)/HOL-Library.gz
 
 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
-  Library/Library.thy Library/Multiset.thy Library/Quotient.thy \
-  Library/README.html Library/ROOT.ML Library/While_Combinator.thy \
-  Library/While_Combinator_Example.thy
+  Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
+  Library/Quotient.thy Library/README.html Library/ROOT.ML \
+  Library/While_Combinator.thy Library/While_Combinator_Example.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Library
 
 
@@ -254,9 +254,8 @@
   Lex/MaxChop.thy Lex/MaxChop.ML Lex/MaxPrefix.thy Lex/MaxPrefix.ML \
   Lex/NA.thy Lex/NA.ML Lex/NAe.thy Lex/NAe.ML Lex/RegExp2NAe.thy \
   Lex/RegExp2NAe.ML Lex/RegExp2NA.thy Lex/RegExp2NA.ML \
-  Lex/Prefix.thy Lex/Prefix.ML Lex/ROOT.ML \
-  Lex/RegExp.thy Lex/RegSet.thy Lex/RegSet.ML \
-  Lex/RegSet_of_nat_DA.thy Lex/RegSet_of_nat_DA.ML
+  Lex/ROOT.ML Lex/RegExp.thy Lex/RegSet.thy Lex/RegSet.ML \
+  Lex/RegSet_of_nat_DA.thy Lex/RegSet_of_nat_DA.ML Library/List_Prefix.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Lex
 
 
diff -r a9898d89a634 -r 4362e906b745 src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Wed Oct 25 18:25:41 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-(*  Title:      HOL/Lex/Prefix.thy
-    ID:         $Id$
-    Author:     Richard Mayr & Tobias Nipkow
-    Copyright   1995 TUM
-*)
-
-(** <= is a partial order: **)
-
-Goalw [prefix_def] "xs <= (xs::'a list)";
-by (Simp_tac 1);
-qed "prefix_refl";
-AddIffs[prefix_refl];
-
-Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
-by (Clarify_tac 1);
-by (Simp_tac 1);
-qed "prefix_trans";
-
-Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
-by (Clarify_tac 1);
-by (Asm_full_simp_tac 1);
-qed "prefix_antisym";
-
-Goalw [strict_prefix_def] "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)";
-by Auto_tac;
-qed "prefix_less_le";
-
-
-(** recursion equations **)
-
-Goalw [prefix_def] "[] <= xs";
-by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-qed "Nil_prefix";
-AddIffs[Nil_prefix];
-
-Goalw [prefix_def] "(xs <= []) = (xs = [])";
-by (induct_tac "xs" 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-qed "prefix_Nil";
-Addsimps [prefix_Nil];
-
-Goalw [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
-by (rtac iffI 1);
- by (etac exE 1);
- by (rename_tac "zs" 1);
- by (res_inst_tac [("xs","zs")] rev_exhaust 1);
-  by (Asm_full_simp_tac 1);
- by (hyp_subst_tac 1);
- by (asm_full_simp_tac (simpset() delsimps [append_assoc]
-                                 addsimps [append_assoc RS sym])1);
-by (Force_tac 1);
-qed "prefix_snoc";
-Addsimps [prefix_snoc];
-
-Goalw [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
-by (Simp_tac 1);
-by (Fast_tac 1);
-qed"Cons_prefix_Cons";
-Addsimps [Cons_prefix_Cons];
-
-Goal "(xs@ys <= xs@zs) = (ys <= zs)";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "same_prefix_prefix";
-Addsimps [same_prefix_prefix];
-
-AddIffs   (* (xs@ys <= xs) = (ys <= []) *)
- [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
-
-Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
-by (Clarify_tac 1);
-by (Simp_tac 1);
-qed "prefix_prefix";
-Addsimps [prefix_prefix];
-
-Goalw [prefix_def]
-   "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
-by (case_tac "xs" 1);
-by Auto_tac;
-qed "prefix_Cons";
-
-Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
-by (rev_induct_tac "zs" 1);
- by (Force_tac 1);
-by (asm_full_simp_tac (simpset() delsimps [append_assoc]
-                                 addsimps [append_assoc RS sym])1);
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "prefix_append";
-
-Goalw [prefix_def]
-  "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys";
-by (auto_tac(claset(), simpset() addsimps [nth_append]));
-by (case_tac "ys" 1);
-by Auto_tac;
-qed "append_one_prefix";
-
-Goalw [prefix_def] "xs <= ys ==> length xs <= length ys";
-by Auto_tac;
-qed "prefix_length_le";
-
-Goal "mono length";
-by (blast_tac (claset() addIs [monoI, prefix_length_le]) 1);
-qed "mono_length";
diff -r a9898d89a634 -r 4362e906b745 src/HOL/Lex/Prefix.thy
--- a/src/HOL/Lex/Prefix.thy	Wed Oct 25 18:25:41 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      HOL/Lex/Prefix.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1995 TUM
-*)
-
-Prefix = Main +
-
-instance list :: (term)ord
-
-defs
-        prefix_def        "xs <= zs  ==  ? ys. zs = xs@ys"
-
-        strict_prefix_def "xs < zs  ==  xs <= zs & xs ~= (zs::'a list)"
-  
-end
diff -r a9898d89a634 -r 4362e906b745 src/HOL/Library/List_Prefix.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/List_Prefix.thy	Wed Oct 25 18:31:21 2000 +0200
@@ -0,0 +1,150 @@
+(*  Title:      HOL/Library/List_Prefix.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
+*)
+
+header {*
+  \title{List prefixes}
+  \author{Tobias Nipkow and Markus Wenzel}
+*}
+
+theory List_Prefix = Main:
+
+subsection {* Prefix order on lists *}
+
+instance list :: ("term") ord ..
+
+defs (overloaded)
+  prefix_def: "xs \<le> zs == \<exists>ys. zs = xs @ ys"
+  strict_prefix_def: "xs < zs == xs \<le> zs \<and> xs \<noteq> (zs::'a list)"
+
+instance list :: ("term") order
+proof
+  fix xs ys zs :: "'a list"
+  show "xs \<le> xs" by (simp add: prefix_def)
+  { assume "xs \<le> ys" and "ys \<le> zs" thus "xs \<le> zs" by (auto simp add: prefix_def) }
+  { assume "xs \<le> ys" and "ys \<le> xs" thus "xs = ys" by (auto simp add: prefix_def) }
+  show "(xs < zs) = (xs \<le> zs \<and> xs \<noteq> zs)" by (simp only: strict_prefix_def)
+qed
+
+constdefs
+  parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
+  "xs \<parallel> ys == \<not> (xs \<le> ys) \<and> \<not> (ys \<le> xs)"
+
+lemma parallelI [intro]: "\<not> (xs \<le> ys) ==> \<not> (ys \<le> xs) ==> xs \<parallel> ys"
+  by (unfold parallel_def) blast
+
+lemma parellelE [elim]:
+    "xs \<parallel> ys ==> (\<not> (xs \<le> ys) ==> \<not> (ys \<le> xs) ==> C) ==> C"
+  by (unfold parallel_def) blast
+
+theorem prefix_cases:
+  "(xs \<le> ys ==> C) ==>
+    (ys \<le> xs ==> C) ==>
+    (xs \<parallel> ys ==> C) ==> C"
+  by (unfold parallel_def) blast
+
+
+subsection {* Recursion equations *}
+
+theorem Nil_prefix [iff]: "[] \<le> xs"
+  apply (simp add: prefix_def)
+  done
+
+theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"
+  apply (induct_tac xs)
+   apply simp
+  apply (simp add: prefix_def)
+  done
+
+lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
+  apply (unfold prefix_def)
+  apply (rule iffI)
+   apply (erule exE)
+   apply (rename_tac zs)
+   apply (rule_tac xs = zs in rev_exhaust)
+    apply simp
+   apply hypsubst
+   apply (simp del: append_assoc add: append_assoc [symmetric])
+  apply force
+  done
+
+lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
+  apply (auto simp add: prefix_def)
+  done
+
+lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
+  apply (induct_tac xs)
+   apply simp_all
+  done
+
+lemma [iff]: "(xs @ ys \<le> xs) = (ys = [])"
+  apply (insert same_prefix_prefix [where ?zs = "[]"])
+  apply simp
+  apply blast
+  done
+
+lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
+  apply (unfold prefix_def)
+  apply clarify
+  apply simp
+  done
+
+theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
+  apply (unfold prefix_def)
+  apply (case_tac xs)
+   apply auto
+  done
+
+theorem prefix_append:
+    "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))"
+  apply (induct zs rule: rev_induct)
+   apply force
+  apply (simp del: append_assoc add: append_assoc [symmetric])
+  apply simp
+  apply blast
+  done
+
+lemma append_one_prefix:
+    "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
+  apply (unfold prefix_def)
+  apply (auto simp add: nth_append)
+  apply (case_tac ys)
+   apply auto
+  done
+
+theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
+  apply (auto simp add: prefix_def)
+  done
+
+
+subsection {* Prefix cases *}
+
+lemma prefix_Nil_cases [case_names Nil]:
+  "xs \<le> [] ==>
+    (xs = [] ==> C) ==> C"
+  by simp
+
+lemma prefix_Cons_cases [case_names Nil Cons]:
+  "xs \<le> y # ys ==>
+    (xs = [] ==> C) ==>
+    (!!zs. xs = y # zs ==> zs \<le> ys ==> C) ==> C"
+  by (simp only: prefix_Cons) blast
+
+lemma prefix_snoc_cases [case_names prefix snoc]:
+  "xs \<le> ys @ [y] ==>
+    (xs \<le> ys ==> C) ==>
+    (xs = ys @ [y] ==> C) ==> C"
+  by (simp only: prefix_snoc) blast
+
+lemma prefix_append_cases [case_names prefix append]:
+  "xs \<le> ys @ zs ==>
+    (xs \<le> ys ==> C) ==>
+    (!!us. xs = ys @ us ==> us \<le> zs ==> C) ==> C"
+  by (simp only: prefix_append) blast
+
+lemmas prefix_any_cases [cases set: prefix] =    (*dummy set name*)
+  prefix_Nil_cases prefix_Cons_cases
+  prefix_snoc_cases prefix_append_cases
+
+end