[isabelle] Theory Prefix_Order



Dear all,

I've stumbled upon a few issues with the theory
Library/Prefix_Order.thy. This theory instantiates the order type
class for lists like this:

definition "(xs::'a list) <= ys == prefixeq xs ys"
definition "(xs::'a list) < ys == xs <= ys & Not (ys <= xs)"

It then goes on to lift theorems about the constants 'prefixeq' and
'prefix' to the constants 'op <=' and 'op <', adding simp/intro/elim
attributes in the process. However, a few things seem to have gone
wrong here. First off, we have:

lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def]
lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]

The first line hides the fact Sublist.prefixI, so the theorem declared
in the second line is just a duplicate of the one in the first and the
'folded less_list_def' attribute is applied in vain.

However, even when using the fully qualified fact Sublist.prefixI, it
doesn't work the way I assume it was intended to, since 'op <' is not
defined in terms of 'prefix', so the 'folded less_list_def' attribute
still doesn't apply.

Attached are my attempts at fixing these and a few other issues.
Please let me know if I should have posted this on the developer
mailing list.

Cheers,
 Julian
diff -r 92624dd5305f HOL/Library/Prefix_Order.thy
--- a/HOL/Library/Prefix_Order.thy	Fri Aug 29 13:33:55 2014 +0200
+++ b/HOL/Library/Prefix_Order.thy	Mon Oct 20 16:59:20 2014 +0200
@@ -12,29 +12,32 @@
 begin
 
 definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
-definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
+definition "(xs::'a list) < ys \<equiv> prefix xs ys"
 
-instance by (default, unfold less_eq_list_def less_list_def) auto
+instance by (default, unfold prefix_order.less_le_not_le less_eq_list_def less_list_def) auto
 
 end
 
-lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def]
-lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def]
-lemmas strict_prefixI' [intro?] = prefixI' [folded less_list_def]
-lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def]
-lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]
-lemmas strict_prefixE [elim?] = prefixE [folded less_list_def]
-theorems Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def]
-theorems prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def]
-lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def]
-lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def]
-lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def]
-lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def]
-lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def]
-theorems prefix_Cons = prefixeq_Cons [folded less_eq_list_def]
-theorems prefix_length_le = prefixeq_length_le [folded less_eq_list_def]
-lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def]
-lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] =
+lemmas prefixeqI [intro?] = prefixeqI [folded less_eq_list_def]
+lemmas prefixeqE [elim?] = prefixeqE [folded less_eq_list_def]
+lemmas prefixI' [intro?] = prefixI' [folded less_list_def]
+lemmas prefixE' [elim?] = prefixE' [folded less_list_def]
+lemmas prefixI [intro?] = prefixI [folded less_eq_list_def less_list_def]
+lemmas prefixE [elim?] = prefixE [folded less_eq_list_def less_list_def]
+theorems Nil_prefixeq [iff] = Nil_prefixeq [folded less_eq_list_def]
+theorems prefixeq_Nil [simp] = prefixeq_Nil [folded less_eq_list_def]
+lemmas prefixeq_snoc [simp] = prefixeq_snoc [folded less_eq_list_def]
+lemmas Cons_prefixeq_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def]
+lemmas same_prefixeq_prefixeq [simp] = same_prefixeq_prefixeq [folded less_eq_list_def]
+lemmas same_prefixeq_nil [iff] = same_prefixeq_nil [folded less_eq_list_def]
+lemmas prefixeq_prefixeq [simp] = prefixeq_prefixeq [folded less_eq_list_def]
+theorems prefixeq_Cons = prefixeq_Cons [folded less_eq_list_def]
+theorems prefixeq_length_le[dest] = prefixeq_length_le [folded less_eq_list_def]
+lemmas prefix_simps [simp, code] = prefix_simps [folded less_list_def]
+lemmas not_prefixeq_induct [consumes 1, case_names Nil Neq Eq] =
   not_prefixeq_induct [folded less_eq_list_def]
+lemmas take_is_prefixeq [intro] = take_is_prefixeq [folded less_eq_list_def]
+lemmas map_prefixeqI [intro] = map_prefixeqI [folded less_eq_list_def]
+lemmas set_mono_prefixeq [dest] = set_mono_prefixeq [folded less_eq_list_def]
 
 end


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.