author | wenzelm |
Wed, 30 Dec 2015 18:25:39 +0100 | |
changeset 61986 | 2461779da2b8 |
parent 58889 | 5b7a9633cfa8 |
child 67613 | ce654b0e6d69 |
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 |
||
61986 | 6 |
section \<open>Lifting an order to lists of elements\<close> |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
7 |
|
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents:
54295
diff
changeset
|
8 |
theory ListOrder |
58382 | 9 |
imports Main |
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents:
54295
diff
changeset
|
10 |
begin |
5261 | 11 |
|
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
12 |
declare [[syntax_ambiguity_warning = false]] |
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
|
13 |
|
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
|
14 |
|
61986 | 15 |
text \<open> |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
16 |
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
|
17 |
element. |
61986 | 18 |
\<close> |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
19 |
|
19086 | 20 |
definition |
22270 | 21 |
step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where |
19086 | 22 |
"step1 r = |
22270 | 23 |
(\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys = |
24 |
us @ z' # vs)" |
|
9771 | 25 |
|
26 |
||
22270 | 27 |
lemma step1_converse [simp]: "step1 (r^--1) = (step1 r)^--1" |
28 |
apply (unfold step1_def) |
|
29 |
apply (blast intro!: order_antisym) |
|
30 |
done |
|
31 |
||
32 |
lemma in_step1_converse [iff]: "(step1 (r^--1) x y) = ((step1 r)^--1 x y)" |
|
33 |
apply auto |
|
34 |
done |
|
35 |
||
36 |
lemma not_Nil_step1 [iff]: "\<not> step1 r [] xs" |
|
9771 | 37 |
apply (unfold step1_def) |
38 |
apply blast |
|
39 |
done |
|
40 |
||
22270 | 41 |
lemma not_step1_Nil [iff]: "\<not> step1 r xs []" |
9771 | 42 |
apply (unfold step1_def) |
43 |
apply blast |
|
44 |
done |
|
45 |
||
46 |
lemma Cons_step1_Cons [iff]: |
|
22270 | 47 |
"(step1 r (y # ys) (x # xs)) = |
48 |
(r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)" |
|
9771 | 49 |
apply (unfold step1_def) |
50 |
apply (rule iffI) |
|
51 |
apply (erule exE) |
|
52 |
apply (rename_tac ts) |
|
53 |
apply (case_tac ts) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
39157
diff
changeset
|
54 |
apply fastforce |
9771 | 55 |
apply force |
56 |
apply (erule disjE) |
|
57 |
apply blast |
|
58 |
apply (blast intro: Cons_eq_appendI) |
|
59 |
done |
|
60 |
||
61 |
lemma append_step1I: |
|
22270 | 62 |
"step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us |
63 |
==> step1 r (ys @ vs) (xs @ us)" |
|
9771 | 64 |
apply (unfold step1_def) |
65 |
apply auto |
|
66 |
apply blast |
|
67 |
apply (blast intro: append_eq_appendI) |
|
68 |
done |
|
69 |
||
18257 | 70 |
lemma Cons_step1E [elim!]: |
22270 | 71 |
assumes "step1 r ys (x # xs)" |
72 |
and "!!y. ys = y # xs \<Longrightarrow> r y x \<Longrightarrow> R" |
|
73 |
and "!!zs. ys = x # zs \<Longrightarrow> step1 r zs xs \<Longrightarrow> R" |
|
18257 | 74 |
shows R |
23464 | 75 |
using assms |
18257 | 76 |
apply (cases ys) |
9771 | 77 |
apply (simp add: step1_def) |
78 |
apply blast |
|
79 |
done |
|
80 |
||
81 |
lemma Snoc_step1_SnocD: |
|
22270 | 82 |
"step1 r (ys @ [y]) (xs @ [x]) |
83 |
==> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)" |
|
9771 | 84 |
apply (unfold step1_def) |
85 |
apply (clarify del: disjCI) |
|
86 |
apply (rename_tac vs) |
|
87 |
apply (rule_tac xs = vs in rev_exhaust) |
|
88 |
apply force |
|
89 |
apply simp |
|
90 |
apply blast |
|
91 |
done |
|
92 |
||
18241 | 93 |
lemma Cons_acc_step1I [intro!]: |
54295 | 94 |
"Wellfounded.accp r x ==> Wellfounded.accp (step1 r) xs \<Longrightarrow> Wellfounded.accp (step1 r) (x # xs)" |
95 |
apply (induct arbitrary: xs set: Wellfounded.accp) |
|
9771 | 96 |
apply (erule thin_rl) |
23750 | 97 |
apply (erule accp_induct) |
98 |
apply (rule accp.accI) |
|
9771 | 99 |
apply blast |
100 |
done |
|
101 |
||
54295 | 102 |
lemma lists_accD: "listsp (Wellfounded.accp r) xs ==> Wellfounded.accp (step1 r) xs" |
22270 | 103 |
apply (induct set: listsp) |
23750 | 104 |
apply (rule accp.accI) |
9771 | 105 |
apply simp |
23750 | 106 |
apply (rule accp.accI) |
107 |
apply (fast dest: accp_downward) |
|
9771 | 108 |
done |
109 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
110 |
lemma ex_step1I: |
22270 | 111 |
"[| x \<in> set xs; r y x |] |
112 |
==> \<exists>ys. step1 r ys xs \<and> y \<in> set ys" |
|
9771 | 113 |
apply (unfold step1_def) |
114 |
apply (drule in_set_conv_decomp [THEN iffD1]) |
|
115 |
apply force |
|
116 |
done |
|
117 |
||
54295 | 118 |
lemma lists_accI: "Wellfounded.accp (step1 r) xs ==> listsp (Wellfounded.accp r) xs" |
119 |
apply (induct set: Wellfounded.accp) |
|
9771 | 120 |
apply clarify |
23750 | 121 |
apply (rule accp.accI) |
22270 | 122 |
apply (drule_tac r=r in ex_step1I, assumption) |
9771 | 123 |
apply blast |
124 |
done |
|
5261 | 125 |
|
11639 | 126 |
end |