src/HOL/Lambda/ListOrder.thy
 author nipkow Thu Dec 11 08:52:50 2008 +0100 (2008-12-11) changeset 29106 25e28a4070f3 parent 23750 a1db5f819d00 child 36862 952b2b102a0a permissions -rw-r--r--
Testfile for Stefan's code generator
```     1 (*  Title:      HOL/Lambda/ListOrder.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Tobias Nipkow
```
```     4     Copyright   1998 TU Muenchen
```
```     5 *)
```
```     6
```
```     7 header {* Lifting an order to lists of elements *}
```
```     8
```
```     9 theory ListOrder imports Main begin
```
```    10
```
```    11 text {*
```
```    12   Lifting an order to lists of elements, relating exactly one
```
```    13   element.
```
```    14 *}
```
```    15
```
```    16 definition
```
```    17   step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where
```
```    18   "step1 r =
```
```    19     (\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys =
```
```    20       us @ z' # vs)"
```
```    21
```
```    22
```
```    23 lemma step1_converse [simp]: "step1 (r^--1) = (step1 r)^--1"
```
```    24   apply (unfold step1_def)
```
```    25   apply (blast intro!: order_antisym)
```
```    26   done
```
```    27
```
```    28 lemma in_step1_converse [iff]: "(step1 (r^--1) x y) = ((step1 r)^--1 x y)"
```
```    29   apply auto
```
```    30   done
```
```    31
```
```    32 lemma not_Nil_step1 [iff]: "\<not> step1 r [] xs"
```
```    33   apply (unfold step1_def)
```
```    34   apply blast
```
```    35   done
```
```    36
```
```    37 lemma not_step1_Nil [iff]: "\<not> step1 r xs []"
```
```    38   apply (unfold step1_def)
```
```    39   apply blast
```
```    40   done
```
```    41
```
```    42 lemma Cons_step1_Cons [iff]:
```
```    43     "(step1 r (y # ys) (x # xs)) =
```
```    44       (r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)"
```
```    45   apply (unfold step1_def)
```
```    46   apply (rule iffI)
```
```    47    apply (erule exE)
```
```    48    apply (rename_tac ts)
```
```    49    apply (case_tac ts)
```
```    50     apply fastsimp
```
```    51    apply force
```
```    52   apply (erule disjE)
```
```    53    apply blast
```
```    54   apply (blast intro: Cons_eq_appendI)
```
```    55   done
```
```    56
```
```    57 lemma append_step1I:
```
```    58   "step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us
```
```    59     ==> step1 r (ys @ vs) (xs @ us)"
```
```    60   apply (unfold step1_def)
```
```    61   apply auto
```
```    62    apply blast
```
```    63   apply (blast intro: append_eq_appendI)
```
```    64   done
```
```    65
```
```    66 lemma Cons_step1E [elim!]:
```
```    67   assumes "step1 r ys (x # xs)"
```
```    68     and "!!y. ys = y # xs \<Longrightarrow> r y x \<Longrightarrow> R"
```
```    69     and "!!zs. ys = x # zs \<Longrightarrow> step1 r zs xs \<Longrightarrow> R"
```
```    70   shows R
```
```    71   using assms
```
```    72   apply (cases ys)
```
```    73    apply (simp add: step1_def)
```
```    74   apply blast
```
```    75   done
```
```    76
```
```    77 lemma Snoc_step1_SnocD:
```
```    78   "step1 r (ys @ [y]) (xs @ [x])
```
```    79     ==> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)"
```
```    80   apply (unfold step1_def)
```
```    81   apply (clarify del: disjCI)
```
```    82   apply (rename_tac vs)
```
```    83   apply (rule_tac xs = vs in rev_exhaust)
```
```    84    apply force
```
```    85   apply simp
```
```    86   apply blast
```
```    87   done
```
```    88
```
```    89 lemma Cons_acc_step1I [intro!]:
```
```    90     "accp r x ==> accp (step1 r) xs \<Longrightarrow> accp (step1 r) (x # xs)"
```
```    91   apply (induct arbitrary: xs set: accp)
```
```    92   apply (erule thin_rl)
```
```    93   apply (erule accp_induct)
```
```    94   apply (rule accp.accI)
```
```    95   apply blast
```
```    96   done
```
```    97
```
```    98 lemma lists_accD: "listsp (accp r) xs ==> accp (step1 r) xs"
```
```    99   apply (induct set: listsp)
```
```   100    apply (rule accp.accI)
```
```   101    apply simp
```
```   102   apply (rule accp.accI)
```
```   103   apply (fast dest: accp_downward)
```
```   104   done
```
```   105
```
```   106 lemma ex_step1I:
```
```   107   "[| x \<in> set xs; r y x |]
```
```   108     ==> \<exists>ys. step1 r ys xs \<and> y \<in> set ys"
```
```   109   apply (unfold step1_def)
```
```   110   apply (drule in_set_conv_decomp [THEN iffD1])
```
```   111   apply force
```
```   112   done
```
```   113
```
```   114 lemma lists_accI: "accp (step1 r) xs ==> listsp (accp r) xs"
```
```   115   apply (induct set: accp)
```
```   116   apply clarify
```
```   117   apply (rule accp.accI)
```
```   118   apply (drule_tac r=r in ex_step1I, assumption)
```
```   119   apply blast
```
```   120   done
```
```   121
```
```   122 end
```