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