1(*  Title:      HOL/Proofs/Lambda/ListOrder.thy
2    Author:     Tobias Nipkow
3    Copyright   1998 TU Muenchen
4*)
5
6section \<open>Lifting an order to lists of elements\<close>
7
8theory ListOrder
9imports Main
10begin
11
12declare [[syntax_ambiguity_warning = false]]
13
14
15text \<open>
16  Lifting an order to lists of elements, relating exactly one
17  element.
18\<close>
19
20definition
21  step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where
22  "step1 r =
23    (\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys =
24      us @ z' # vs)"
25
26
27lemma step1_converse [simp]: "step1 (r\<inverse>\<inverse>) = (step1 r)\<inverse>\<inverse>"
28  apply (unfold step1_def)
29  apply (blast intro!: order_antisym)
30  done
31
32lemma in_step1_converse [iff]: "(step1 (r\<inverse>\<inverse>) x y) = ((step1 r)\<inverse>\<inverse> x y)"
33  apply auto
34  done
35
36lemma not_Nil_step1 [iff]: "\<not> step1 r [] xs"
37  apply (unfold step1_def)
38  apply blast
39  done
40
41lemma not_step1_Nil [iff]: "\<not> step1 r xs []"
42  apply (unfold step1_def)
43  apply blast
44  done
45
46lemma Cons_step1_Cons [iff]:
47    "(step1 r (y # ys) (x # xs)) =
48      (r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)"
49  apply (unfold step1_def)
50  apply (rule iffI)
51   apply (erule exE)
52   apply (rename_tac ts)
53   apply (case_tac ts)
54    apply fastforce
55   apply force
56  apply (erule disjE)
57   apply blast
58  apply (blast intro: Cons_eq_appendI)
59  done
60
61lemma append_step1I:
62  "step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us
63    ==> step1 r (ys @ vs) (xs @ us)"
64  apply (unfold step1_def)
65  apply auto
66   apply blast
67  apply (blast intro: append_eq_appendI)
68  done
69
70lemma Cons_step1E [elim!]:
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"
74  shows R
75  using assms
76  apply (cases ys)
77   apply (simp add: step1_def)
78  apply blast
79  done
80
81lemma Snoc_step1_SnocD:
82  "step1 r (ys @ [y]) (xs @ [x])
83    ==> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)"
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
93lemma Cons_acc_step1I [intro!]:
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)
96  apply (erule thin_rl)
97  apply (erule accp_induct)
98  apply (rule accp.accI)
99  apply blast
100  done
101
102lemma lists_accD: "listsp (Wellfounded.accp r) xs ==> Wellfounded.accp (step1 r) xs"
103  apply (induct set: listsp)
104   apply (rule accp.accI)
105   apply simp
106  apply (rule accp.accI)
107  apply (fast dest: accp_downward)
108  done
109
110lemma ex_step1I:
111  "[| x \<in> set xs; r y x |]
112    ==> \<exists>ys. step1 r ys xs \<and> y \<in> set ys"
113  apply (unfold step1_def)
114  apply (drule in_set_conv_decomp [THEN iffD1])
115  apply force
116  done
117
118lemma lists_accI: "Wellfounded.accp (step1 r) xs ==> listsp (Wellfounded.accp r) xs"
119  apply (induct set: Wellfounded.accp)
120  apply clarify
121  apply (rule accp.accI)
122  apply (drule_tac r=r in ex_step1I, assumption)
123  apply blast
124  done
125
126end
127