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