author | wenzelm |
Fri, 17 Nov 2006 02:20:03 +0100 | |
changeset 21404 | eb85850d3eb7 |
parent 20503 | 503ac4c5ef91 |
child 22270 | 4ccb7e6be929 |
permissions | -rw-r--r-- |
5261 | 1 |
(* Title: HOL/Lambda/ListOrder.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1998 TU Muenchen |
|
5 |
*) |
|
6 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
7 |
header {* Lifting an order to lists of elements *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
8 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
19086
diff
changeset
|
9 |
theory ListOrder imports Main begin |
5261 | 10 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
11 |
text {* |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
12 |
Lifting an order to lists of elements, relating exactly one |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
13 |
element. |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
14 |
*} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
15 |
|
19086 | 16 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20503
diff
changeset
|
17 |
step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where |
19086 | 18 |
"step1 r = |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
19 |
{(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys = |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
20 |
us @ z' # vs}" |
9771 | 21 |
|
22 |
||
23 |
lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1" |
|
24 |
apply (unfold step1_def) |
|
25 |
apply blast |
|
26 |
done |
|
27 |
||
28 |
lemma in_step1_converse [iff]: "(p \<in> step1 (r^-1)) = (p \<in> (step1 r)^-1)" |
|
29 |
apply auto |
|
30 |
done |
|
31 |
||
32 |
lemma not_Nil_step1 [iff]: "([], xs) \<notin> step1 r" |
|
33 |
apply (unfold step1_def) |
|
34 |
apply blast |
|
35 |
done |
|
36 |
||
37 |
lemma not_step1_Nil [iff]: "(xs, []) \<notin> step1 r" |
|
38 |
apply (unfold step1_def) |
|
39 |
apply blast |
|
40 |
done |
|
41 |
||
42 |
lemma Cons_step1_Cons [iff]: |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
43 |
"((y # ys, x # xs) \<in> step1 r) = |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
44 |
((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)" |
9771 | 45 |
apply (unfold step1_def) |
46 |
apply simp |
|
47 |
apply (rule iffI) |
|
48 |
apply (erule exE) |
|
49 |
apply (rename_tac ts) |
|
50 |
apply (case_tac ts) |
|
13601 | 51 |
apply fastsimp |
9771 | 52 |
apply force |
53 |
apply (erule disjE) |
|
54 |
apply blast |
|
55 |
apply (blast intro: Cons_eq_appendI) |
|
56 |
done |
|
57 |
||
58 |
lemma append_step1I: |
|
59 |
"(ys, xs) \<in> step1 r \<and> vs = us \<or> ys = xs \<and> (vs, us) \<in> step1 r |
|
60 |
==> (ys @ vs, xs @ us) : step1 r" |
|
61 |
apply (unfold step1_def) |
|
62 |
apply auto |
|
63 |
apply blast |
|
64 |
apply (blast intro: append_eq_appendI) |
|
65 |
done |
|
66 |
||
18257 | 67 |
lemma Cons_step1E [elim!]: |
68 |
assumes "(ys, x # xs) \<in> step1 r" |
|
69 |
and "!!y. ys = y # xs \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> R" |
|
70 |
and "!!zs. ys = x # zs \<Longrightarrow> (zs, xs) \<in> step1 r \<Longrightarrow> R" |
|
71 |
shows R |
|
72 |
using prems |
|
73 |
apply (cases ys) |
|
9771 | 74 |
apply (simp add: step1_def) |
75 |
apply blast |
|
76 |
done |
|
77 |
||
78 |
lemma Snoc_step1_SnocD: |
|
79 |
"(ys @ [y], xs @ [x]) \<in> step1 r |
|
80 |
==> ((ys, xs) \<in> step1 r \<and> y = x \<or> ys = xs \<and> (y, x) \<in> r)" |
|
81 |
apply (unfold step1_def) |
|
82 |
apply simp |
|
83 |
apply (clarify del: disjCI) |
|
84 |
apply (rename_tac vs) |
|
85 |
apply (rule_tac xs = vs in rev_exhaust) |
|
86 |
apply force |
|
87 |
apply simp |
|
88 |
apply blast |
|
89 |
done |
|
90 |
||
18241 | 91 |
lemma Cons_acc_step1I [intro!]: |
18257 | 92 |
"x \<in> acc r ==> xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r)" |
20503 | 93 |
apply (induct arbitrary: xs set: acc) |
9771 | 94 |
apply (erule thin_rl) |
95 |
apply (erule acc_induct) |
|
96 |
apply (rule accI) |
|
97 |
apply blast |
|
98 |
done |
|
99 |
||
100 |
lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)" |
|
18241 | 101 |
apply (induct set: lists) |
9771 | 102 |
apply (rule accI) |
103 |
apply simp |
|
104 |
apply (rule accI) |
|
105 |
apply (fast dest: acc_downward) |
|
106 |
done |
|
107 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
108 |
lemma ex_step1I: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
109 |
"[| x \<in> set xs; (y, x) \<in> r |] |
9771 | 110 |
==> \<exists>ys. (ys, xs) \<in> step1 r \<and> y \<in> set ys" |
111 |
apply (unfold step1_def) |
|
112 |
apply (drule in_set_conv_decomp [THEN iffD1]) |
|
113 |
apply force |
|
114 |
done |
|
115 |
||
116 |
lemma lists_accI: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)" |
|
18241 | 117 |
apply (induct set: acc) |
9771 | 118 |
apply clarify |
119 |
apply (rule accI) |
|
120 |
apply (drule ex_step1I, assumption) |
|
121 |
apply blast |
|
122 |
done |
|
5261 | 123 |
|
11639 | 124 |
end |