1 (* Title: HOL/Lambda/ListOrder.thy |
|
2 Author: Tobias Nipkow |
|
3 Copyright 1998 TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Lifting an order to lists of elements *} |
|
7 |
|
8 theory ListOrder imports Main begin |
|
9 |
|
10 declare [[syntax_ambiguity_level = 100]] |
|
11 |
|
12 |
|
13 text {* |
|
14 Lifting an order to lists of elements, relating exactly one |
|
15 element. |
|
16 *} |
|
17 |
|
18 definition |
|
19 step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where |
|
20 "step1 r = |
|
21 (\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys = |
|
22 us @ z' # vs)" |
|
23 |
|
24 |
|
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" |
|
35 apply (unfold step1_def) |
|
36 apply blast |
|
37 done |
|
38 |
|
39 lemma not_step1_Nil [iff]: "\<not> step1 r xs []" |
|
40 apply (unfold step1_def) |
|
41 apply blast |
|
42 done |
|
43 |
|
44 lemma Cons_step1_Cons [iff]: |
|
45 "(step1 r (y # ys) (x # xs)) = |
|
46 (r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)" |
|
47 apply (unfold step1_def) |
|
48 apply (rule iffI) |
|
49 apply (erule exE) |
|
50 apply (rename_tac ts) |
|
51 apply (case_tac ts) |
|
52 apply fastsimp |
|
53 apply force |
|
54 apply (erule disjE) |
|
55 apply blast |
|
56 apply (blast intro: Cons_eq_appendI) |
|
57 done |
|
58 |
|
59 lemma append_step1I: |
|
60 "step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us |
|
61 ==> step1 r (ys @ vs) (xs @ us)" |
|
62 apply (unfold step1_def) |
|
63 apply auto |
|
64 apply blast |
|
65 apply (blast intro: append_eq_appendI) |
|
66 done |
|
67 |
|
68 lemma Cons_step1E [elim!]: |
|
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" |
|
72 shows R |
|
73 using assms |
|
74 apply (cases ys) |
|
75 apply (simp add: step1_def) |
|
76 apply blast |
|
77 done |
|
78 |
|
79 lemma Snoc_step1_SnocD: |
|
80 "step1 r (ys @ [y]) (xs @ [x]) |
|
81 ==> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)" |
|
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 |
|
91 lemma Cons_acc_step1I [intro!]: |
|
92 "accp r x ==> accp (step1 r) xs \<Longrightarrow> accp (step1 r) (x # xs)" |
|
93 apply (induct arbitrary: xs set: accp) |
|
94 apply (erule thin_rl) |
|
95 apply (erule accp_induct) |
|
96 apply (rule accp.accI) |
|
97 apply blast |
|
98 done |
|
99 |
|
100 lemma lists_accD: "listsp (accp r) xs ==> accp (step1 r) xs" |
|
101 apply (induct set: listsp) |
|
102 apply (rule accp.accI) |
|
103 apply simp |
|
104 apply (rule accp.accI) |
|
105 apply (fast dest: accp_downward) |
|
106 done |
|
107 |
|
108 lemma ex_step1I: |
|
109 "[| x \<in> set xs; r y x |] |
|
110 ==> \<exists>ys. step1 r ys xs \<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: "accp (step1 r) xs ==> listsp (accp r) xs" |
|
117 apply (induct set: accp) |
|
118 apply clarify |
|
119 apply (rule accp.accI) |
|
120 apply (drule_tac r=r in ex_step1I, assumption) |
|
121 apply blast |
|
122 done |
|
123 |
|
124 end |
|