src/HOL/Lambda/ListOrder.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10264 ef384b242d09
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
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
wenzelm@9771
     9
theory ListOrder = Acc:
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
nipkow@5261
    16
constdefs
wenzelm@9771
    17
  step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
wenzelm@9771
    18
  "step1 r ==
wenzelm@9811
    19
    {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys =
wenzelm@9811
    20
      us @ z' # vs}"
wenzelm@9771
    21
wenzelm@9771
    22
wenzelm@9771
    23
lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1"
wenzelm@9771
    24
  apply (unfold step1_def)
wenzelm@9771
    25
  apply blast
wenzelm@9771
    26
  done
wenzelm@9771
    27
wenzelm@9771
    28
lemma in_step1_converse [iff]: "(p \<in> step1 (r^-1)) = (p \<in> (step1 r)^-1)"
wenzelm@9771
    29
  apply auto
wenzelm@9771
    30
  done
wenzelm@9771
    31
wenzelm@9771
    32
lemma not_Nil_step1 [iff]: "([], xs) \<notin> step1 r"
wenzelm@9771
    33
  apply (unfold step1_def)
wenzelm@9771
    34
  apply blast
wenzelm@9771
    35
  done
wenzelm@9771
    36
wenzelm@9771
    37
lemma not_step1_Nil [iff]: "(xs, []) \<notin> step1 r"
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]:
wenzelm@9811
    43
    "((y # ys, x # xs) \<in> step1 r) =
wenzelm@9811
    44
      ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
wenzelm@9771
    45
  apply (unfold step1_def)
wenzelm@9771
    46
  apply simp
wenzelm@9771
    47
  apply (rule iffI)
wenzelm@9771
    48
   apply (erule exE)
wenzelm@9771
    49
   apply (rename_tac ts)
wenzelm@9771
    50
   apply (case_tac ts)
wenzelm@9771
    51
    apply force
wenzelm@9771
    52
   apply force
wenzelm@9771
    53
  apply (erule disjE)
wenzelm@9771
    54
   apply blast
wenzelm@9771
    55
  apply (blast intro: Cons_eq_appendI)
wenzelm@9771
    56
  done
wenzelm@9771
    57
wenzelm@9771
    58
lemma append_step1I:
wenzelm@9771
    59
  "(ys, xs) \<in> step1 r \<and> vs = us \<or> ys = xs \<and> (vs, us) \<in> step1 r
wenzelm@9771
    60
    ==> (ys @ vs, xs @ us) : step1 r"
wenzelm@9771
    61
  apply (unfold step1_def)
wenzelm@9771
    62
  apply auto
wenzelm@9771
    63
   apply blast
wenzelm@9771
    64
  apply (blast intro: append_eq_appendI)
wenzelm@9771
    65
  done
wenzelm@9771
    66
wenzelm@9941
    67
lemma Cons_step1E [rule_format, elim!]:
wenzelm@9771
    68
  "[| (ys, x # xs) \<in> step1 r;
wenzelm@9811
    69
    \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
wenzelm@9811
    70
    \<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R
wenzelm@9771
    71
   |] ==> R"
wenzelm@9771
    72
  apply (case_tac 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:
wenzelm@9771
    78
  "(ys @ [y], xs @ [x]) \<in> step1 r
wenzelm@9771
    79
    ==> ((ys, xs) \<in> step1 r \<and> y = x \<or> ys = xs \<and> (y, x) \<in> r)"
wenzelm@9771
    80
  apply (unfold step1_def)
wenzelm@9771
    81
  apply simp
wenzelm@9771
    82
  apply (clarify del: disjCI)
wenzelm@9771
    83
  apply (rename_tac vs)
wenzelm@9771
    84
  apply (rule_tac xs = vs in rev_exhaust)
wenzelm@9771
    85
   apply force
wenzelm@9771
    86
  apply simp
wenzelm@9771
    87
  apply blast
wenzelm@9771
    88
  done
wenzelm@9771
    89
wenzelm@9941
    90
lemma Cons_acc_step1I [rule_format, intro!]:
wenzelm@9771
    91
    "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
wenzelm@9771
    92
  apply (erule acc_induct)
wenzelm@9771
    93
  apply (erule thin_rl)
wenzelm@9771
    94
  apply clarify
wenzelm@9771
    95
  apply (erule acc_induct)
wenzelm@9771
    96
  apply (rule accI)
wenzelm@9771
    97
  apply blast
wenzelm@9771
    98
  done
wenzelm@9771
    99
wenzelm@9771
   100
lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)"
wenzelm@9771
   101
  apply (erule lists.induct)
wenzelm@9771
   102
   apply (rule accI)
wenzelm@9771
   103
   apply simp
wenzelm@9771
   104
  apply (rule accI)
wenzelm@9771
   105
  apply (fast dest: acc_downward)
wenzelm@9771
   106
  done
wenzelm@9771
   107
wenzelm@9811
   108
lemma ex_step1I:
wenzelm@9811
   109
  "[| x \<in> set xs; (y, x) \<in> r |]
wenzelm@9771
   110
    ==> \<exists>ys. (ys, xs) \<in> step1 r \<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
wenzelm@9771
   116
lemma lists_accI: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)"
wenzelm@9771
   117
  apply (erule acc_induct)
wenzelm@9771
   118
  apply clarify
wenzelm@9771
   119
  apply (rule accI)
wenzelm@9771
   120
  apply (drule ex_step1I, assumption)
wenzelm@9771
   121
  apply blast
wenzelm@9771
   122
  done
nipkow@5261
   123
wenzelm@9811
   124
end