src/HOL/Proofs/Lambda/ListOrder.thy
 author wenzelm Thu May 24 17:25:53 2012 +0200 (2012-05-24) changeset 47988 e4b69e10b990 parent 46512 4f9f61f9b535 child 54295 45a5523d4a63 permissions -rw-r--r--
tuned proofs;
```     1 (*  Title:      HOL/Proofs/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_warning = false]]
```
```    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 fastforce
```
```    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
```