equal
deleted
inserted
replaced
11 |
11 |
12 theory List_Prefix = Main: |
12 theory List_Prefix = Main: |
13 |
13 |
14 subsection {* Prefix order on lists *} |
14 subsection {* Prefix order on lists *} |
15 |
15 |
16 instance list :: ("term") ord .. |
16 instance list :: (type) ord .. |
17 |
17 |
18 defs (overloaded) |
18 defs (overloaded) |
19 prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs" |
19 prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs" |
20 strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)" |
20 strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)" |
21 |
21 |
22 instance list :: ("term") order |
22 instance list :: (type) order |
23 by intro_classes (auto simp add: prefix_def strict_prefix_def) |
23 by intro_classes (auto simp add: prefix_def strict_prefix_def) |
24 |
24 |
25 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys" |
25 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys" |
26 by (unfold prefix_def) blast |
26 by (unfold prefix_def) blast |
27 |
27 |