author | wenzelm |
Mon, 06 Sep 2010 14:18:16 +0200 | |
changeset 39157 | b98909faaea8 |
parent 39126 | src/HOL/Lambda/ListOrder.thy@ee117c5b3b75 |
child 44890 | 22f665a2e91c |
permissions | -rw-r--r-- |
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39126
diff
changeset
|
1 |
(* Title: HOL/Proofs/Lambda/ListOrder.thy |
5261 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 1998 TU Muenchen |
|
4 |
*) |
|
5 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
6 |
header {* Lifting an order to lists of elements *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
7 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
19086
diff
changeset
|
8 |
theory ListOrder imports Main begin |
5261 | 9 |
|
39126
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
36862
diff
changeset
|
10 |
declare [[syntax_ambiguity_level = 100]] |
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
36862
diff
changeset
|
11 |
|
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
36862
diff
changeset
|
12 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
13 |
text {* |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
14 |
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
|
15 |
element. |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
16 |
*} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
17 |
|
19086 | 18 |
definition |
22270 | 19 |
step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where |
19086 | 20 |
"step1 r = |
22270 | 21 |
(\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys = |
22 |
us @ z' # vs)" |
|
9771 | 23 |
|
24 |
||
22270 | 25 |
lemma step1_converse [simp]: "step1 (r^--1) = (step1 r)^--1" |
26 |
apply (unfold step1_def) |
|
27 |
apply (blast intro!: order_antisym) |
|
28 |
done |
|
29 |
||
30 |
lemma in_step1_converse [iff]: "(step1 (r^--1) x y) = ((step1 r)^--1 x y)" |
|
31 |
apply auto |
|
32 |
done |
|
33 |
||
34 |
lemma not_Nil_step1 [iff]: "\<not> step1 r [] xs" |
|
9771 | 35 |
apply (unfold step1_def) |
36 |
apply blast |
|
37 |
done |
|
38 |
||
22270 | 39 |
lemma not_step1_Nil [iff]: "\<not> step1 r xs []" |
9771 | 40 |
apply (unfold step1_def) |
41 |
apply blast |
|
42 |
done |
|
43 |
||
44 |
lemma Cons_step1_Cons [iff]: |
|
22270 | 45 |
"(step1 r (y # ys) (x # xs)) = |
46 |
(r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)" |
|
9771 | 47 |
apply (unfold step1_def) |
48 |
apply (rule iffI) |
|
49 |
apply (erule exE) |
|
50 |
apply (rename_tac ts) |
|
51 |
apply (case_tac ts) |
|
13601 | 52 |
apply fastsimp |
9771 | 53 |
apply force |
54 |
apply (erule disjE) |
|
55 |
apply blast |
|
56 |
apply (blast intro: Cons_eq_appendI) |
|
57 |
done |
|
58 |
||
59 |
lemma append_step1I: |
|
22270 | 60 |
"step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us |
61 |
==> step1 r (ys @ vs) (xs @ us)" |
|
9771 | 62 |
apply (unfold step1_def) |
63 |
apply auto |
|
64 |
apply blast |
|
65 |
apply (blast intro: append_eq_appendI) |
|
66 |
done |
|
67 |
||
18257 | 68 |
lemma Cons_step1E [elim!]: |
22270 | 69 |
assumes "step1 r ys (x # xs)" |
70 |
and "!!y. ys = y # xs \<Longrightarrow> r y x \<Longrightarrow> R" |
|
71 |
and "!!zs. ys = x # zs \<Longrightarrow> step1 r zs xs \<Longrightarrow> R" |
|
18257 | 72 |
shows R |
23464 | 73 |
using assms |
18257 | 74 |
apply (cases ys) |
9771 | 75 |
apply (simp add: step1_def) |
76 |
apply blast |
|
77 |
done |
|
78 |
||
79 |
lemma Snoc_step1_SnocD: |
|
22270 | 80 |
"step1 r (ys @ [y]) (xs @ [x]) |
81 |
==> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)" |
|
9771 | 82 |
apply (unfold step1_def) |
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!]: |
23750 | 92 |
"accp r x ==> accp (step1 r) xs \<Longrightarrow> accp (step1 r) (x # xs)" |
93 |
apply (induct arbitrary: xs set: accp) |
|
9771 | 94 |
apply (erule thin_rl) |
23750 | 95 |
apply (erule accp_induct) |
96 |
apply (rule accp.accI) |
|
9771 | 97 |
apply blast |
98 |
done |
|
99 |
||
23750 | 100 |
lemma lists_accD: "listsp (accp r) xs ==> accp (step1 r) xs" |
22270 | 101 |
apply (induct set: listsp) |
23750 | 102 |
apply (rule accp.accI) |
9771 | 103 |
apply simp |
23750 | 104 |
apply (rule accp.accI) |
105 |
apply (fast dest: accp_downward) |
|
9771 | 106 |
done |
107 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
108 |
lemma ex_step1I: |
22270 | 109 |
"[| x \<in> set xs; r y x |] |
110 |
==> \<exists>ys. step1 r ys xs \<and> y \<in> set ys" |
|
9771 | 111 |
apply (unfold step1_def) |
112 |
apply (drule in_set_conv_decomp [THEN iffD1]) |
|
113 |
apply force |
|
114 |
done |
|
115 |
||
23750 | 116 |
lemma lists_accI: "accp (step1 r) xs ==> listsp (accp r) xs" |
117 |
apply (induct set: accp) |
|
9771 | 118 |
apply clarify |
23750 | 119 |
apply (rule accp.accI) |
22270 | 120 |
apply (drule_tac r=r in ex_step1I, assumption) |
9771 | 121 |
apply blast |
122 |
done |
|
5261 | 123 |
|
11639 | 124 |
end |