src/HOL/Lambda/ListOrder.thy
 author haftmann Mon Aug 14 13:46:06 2006 +0200 (2006-08-14) changeset 20380 14f9f2a1caa6 parent 19564 d3e2f532459a child 20503 503ac4c5ef91 permissions -rw-r--r--
simplified code generator setup
```     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 \<times> 'a) set => ('a list \<times> 'a list) set"
```
```    18   "step1 r =
```
```    19     {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<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
```
```    26   done
```
```    27
```
```    28 lemma in_step1_converse [iff]: "(p \<in> step1 (r^-1)) = (p \<in> (step1 r)^-1)"
```
```    29   apply auto
```
```    30   done
```
```    31
```
```    32 lemma not_Nil_step1 [iff]: "([], xs) \<notin> step1 r"
```
```    33   apply (unfold step1_def)
```
```    34   apply blast
```
```    35   done
```
```    36
```
```    37 lemma not_step1_Nil [iff]: "(xs, []) \<notin> step1 r"
```
```    38   apply (unfold step1_def)
```
```    39   apply blast
```
```    40   done
```
```    41
```
```    42 lemma Cons_step1_Cons [iff]:
```
```    43     "((y # ys, x # xs) \<in> step1 r) =
```
```    44       ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
```
```    45   apply (unfold step1_def)
```
```    46   apply simp
```
```    47   apply (rule iffI)
```
```    48    apply (erule exE)
```
```    49    apply (rename_tac ts)
```
```    50    apply (case_tac ts)
```
```    51     apply fastsimp
```
```    52    apply force
```
```    53   apply (erule disjE)
```
```    54    apply blast
```
```    55   apply (blast intro: Cons_eq_appendI)
```
```    56   done
```
```    57
```
```    58 lemma append_step1I:
```
```    59   "(ys, xs) \<in> step1 r \<and> vs = us \<or> ys = xs \<and> (vs, us) \<in> step1 r
```
```    60     ==> (ys @ vs, xs @ us) : step1 r"
```
```    61   apply (unfold step1_def)
```
```    62   apply auto
```
```    63    apply blast
```
```    64   apply (blast intro: append_eq_appendI)
```
```    65   done
```
```    66
```
```    67 lemma Cons_step1E [elim!]:
```
```    68   assumes "(ys, x # xs) \<in> step1 r"
```
```    69     and "!!y. ys = y # xs \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> R"
```
```    70     and "!!zs. ys = x # zs \<Longrightarrow> (zs, xs) \<in> step1 r \<Longrightarrow> R"
```
```    71   shows R
```
```    72   using prems
```
```    73   apply (cases ys)
```
```    74    apply (simp add: step1_def)
```
```    75   apply blast
```
```    76   done
```
```    77
```
```    78 lemma Snoc_step1_SnocD:
```
```    79   "(ys @ [y], xs @ [x]) \<in> step1 r
```
```    80     ==> ((ys, xs) \<in> step1 r \<and> y = x \<or> ys = xs \<and> (y, x) \<in> r)"
```
```    81   apply (unfold step1_def)
```
```    82   apply simp
```
```    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     "x \<in> acc r ==> xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r)"
```
```    93   apply (induct fixing: xs set: acc)
```
```    94   apply (erule thin_rl)
```
```    95   apply (erule acc_induct)
```
```    96   apply (rule accI)
```
```    97   apply blast
```
```    98   done
```
```    99
```
```   100 lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)"
```
```   101   apply (induct set: lists)
```
```   102    apply (rule accI)
```
```   103    apply simp
```
```   104   apply (rule accI)
```
```   105   apply (fast dest: acc_downward)
```
```   106   done
```
```   107
```
```   108 lemma ex_step1I:
```
```   109   "[| x \<in> set xs; (y, x) \<in> r |]
```
```   110     ==> \<exists>ys. (ys, xs) \<in> step1 r \<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: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)"
```
```   117   apply (induct set: acc)
```
```   118   apply clarify
```
```   119   apply (rule accI)
```
```   120   apply (drule ex_step1I, assumption)
```
```   121   apply blast
```
```   122   done
```
```   123
```
```   124 end
```