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