# HG changeset patch
# User paulson
# Date 927276604 -7200
# Node ID 63e53327f5e5e57c8d945bc69d4951daa88ed0f5
# Parent  32892a8ecb1524ae0867e99626ae9c59917f3995
changes to show that Lists are partially ordered by the prefix relation

diff -r 32892a8ecb15 -r 63e53327f5e5 src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Fri May 21 10:47:07 1999 +0200
+++ b/src/HOL/Lex/Prefix.ML	Fri May 21 10:50:04 1999 +0200
@@ -21,6 +21,11 @@
 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";
@@ -98,3 +103,7 @@
 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 32892a8ecb15 -r 63e53327f5e5 src/HOL/Lex/Prefix.thy
--- a/src/HOL/Lex/Prefix.thy	Fri May 21 10:47:07 1999 +0200
+++ b/src/HOL/Lex/Prefix.thy	Fri May 21 10:50:04 1999 +0200
@@ -9,5 +9,8 @@
 arities list :: (term)ord
 
 defs
-        prefix_def     "xs <= zs  ==  ? ys. zs = xs@ys"
+        prefix_def        "xs <= zs  ==  ? ys. zs = xs@ys"
+
+        strict_prefix_def "xs < zs  ==  xs <= zs & xs ~= (zs::'a list)"
+  
 end