author | paulson |
Wed, 13 Feb 2002 10:44:39 +0100 | |
changeset 12884 | 5d18148e9059 |
parent 11639 | 4213422388c4 |
child 13601 | fd3e3d6b37b2 |
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 |
|
10264 | 9 |
theory ListOrder = Accessible_Part: |
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 |
|
5261 | 16 |
constdefs |
9771 | 17 |
step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" |
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) |
|
51 |
apply force |
|
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 |
||
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
67 |
lemma Cons_step1E [rule_format, elim!]: |
9771 | 68 |
"[| (ys, x # xs) \<in> step1 r; |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
69 |
\<forall>y. ys = y # xs --> (y, x) \<in> r --> R; |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
70 |
\<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R |
9771 | 71 |
|] ==> R" |
72 |
apply (case_tac ys) |
|
73 |
apply (simp add: step1_def) |
|
74 |
apply blast |
|
75 |
done |
|
76 |
||
77 |
lemma Snoc_step1_SnocD: |
|
78 |
"(ys @ [y], xs @ [x]) \<in> step1 r |
|
79 |
==> ((ys, xs) \<in> step1 r \<and> y = x \<or> ys = xs \<and> (y, x) \<in> r)" |
|
80 |
apply (unfold step1_def) |
|
81 |
apply simp |
|
82 |
apply (clarify del: disjCI) |
|
83 |
apply (rename_tac vs) |
|
84 |
apply (rule_tac xs = vs in rev_exhaust) |
|
85 |
apply force |
|
86 |
apply simp |
|
87 |
apply blast |
|
88 |
done |
|
89 |
||
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
90 |
lemma Cons_acc_step1I [rule_format, intro!]: |
9771 | 91 |
"x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)" |
92 |
apply (erule acc_induct) |
|
93 |
apply (erule thin_rl) |
|
94 |
apply clarify |
|
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)" |
|
101 |
apply (erule lists.induct) |
|
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)" |
|
117 |
apply (erule acc_induct) |
|
118 |
apply clarify |
|
119 |
apply (rule accI) |
|
120 |
apply (drule ex_step1I, assumption) |
|
121 |
apply blast |
|
122 |
done |
|
5261 | 123 |
|
11639 | 124 |
end |