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