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