src/HOL/Isar_examples/MultisetOrder.thy
author wenzelm
Sat Sep 04 21:13:01 1999 +0200 (1999-09-04)
changeset 7480 0a0e0dbe1269
parent 7451 d643b3c4996a
child 7527 9e2dddd8b81f
permissions -rw-r--r--
replaced ?? by ?;
wenzelm@7432
     1
(*  Title:      HOL/Isar_examples/MultisetOrder.thy
wenzelm@7432
     2
    ID:         $Id$
wenzelm@7432
     3
    Author:     Markus Wenzel
wenzelm@7432
     4
wenzelm@7442
     5
Wellfoundedness proof for the multiset order.
wenzelm@7442
     6
wenzelm@7442
     7
Original tactic script by Tobias Nipkow (see also
wenzelm@7442
     8
HOL/Induct/Multiset).  Pen-and-paper proof by Wilfried Buchholz.
wenzelm@7432
     9
*)
wenzelm@7432
    10
wenzelm@7432
    11
wenzelm@7432
    12
theory MultisetOrder = Multiset:;
wenzelm@7432
    13
wenzelm@7432
    14
wenzelm@7432
    15
lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)";
wenzelm@7432
    16
proof;
wenzelm@7480
    17
  let ?R = "mult1 r";
wenzelm@7480
    18
  let ?W = "acc ?R";
wenzelm@7432
    19
wenzelm@7432
    20
wenzelm@7432
    21
  {{;
wenzelm@7432
    22
    fix M M0 a;
wenzelm@7480
    23
    assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
wenzelm@7480
    24
      and M0: "M0 : ?W"
wenzelm@7480
    25
      and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W";
wenzelm@7480
    26
    have "M0 + {#a#} : ?W";
wenzelm@7442
    27
    proof (rule accI [of "M0 + {#a#}"]);
wenzelm@7480
    28
      fix N; assume "(N, M0 + {#a#}) : ?R";
wenzelm@7480
    29
      hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
wenzelm@7432
    30
             (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
wenzelm@7432
    31
	by (simp only: less_add_conv);
wenzelm@7480
    32
      thus "N : ?W";
wenzelm@7432
    33
      proof (elim exE disjE conjE);
wenzelm@7480
    34
	fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}";
wenzelm@7480
    35
	from acc_hyp; have "(M, M0) : ?R --> M + {#a#} : ?W"; ..;
wenzelm@7480
    36
	hence "M + {#a#} : ?W"; ..;
wenzelm@7480
    37
	thus "N : ?W"; by (simp only: N);
wenzelm@7432
    38
      next;
wenzelm@7451
    39
	fix K;
wenzelm@7451
    40
	assume N: "N = M0 + K";
wenzelm@7451
    41
	assume "ALL b. elem K b --> (b, a) : r";
wenzelm@7480
    42
	have "?this --> M0 + K : ?W" (is "?P K");
wenzelm@7442
    43
	proof (rule multiset_induct [of _ K]);
wenzelm@7480
    44
	  from M0; have "M0 + {#} : ?W"; by simp;
wenzelm@7480
    45
	  thus "?P {#}"; ..;
wenzelm@7442
    46
wenzelm@7480
    47
	  fix K x; assume hyp: "?P K";
wenzelm@7480
    48
	  show "?P (K + {#x#})";
wenzelm@7442
    49
	  proof;
wenzelm@7451
    50
	    assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r";
wenzelm@7442
    51
	    hence "(x, a) : r"; by simp;
wenzelm@7480
    52
	    with wf_hyp [RS spec]; have b: "ALL M:?W. M + {#x#} : ?W"; ..;
wenzelm@7442
    53
wenzelm@7480
    54
	    from a hyp; have "M0 + K : ?W"; by simp;
wenzelm@7480
    55
	    with b; have "(M0 + K) + {#x#} : ?W"; ..;
wenzelm@7480
    56
	    thus "M0 + (K + {#x#}) : ?W"; by (simp only: union_assoc);
wenzelm@7432
    57
	  qed;
wenzelm@7432
    58
	qed;
wenzelm@7480
    59
	hence "M0 + K : ?W"; ..;
wenzelm@7480
    60
	thus "N : ?W"; by (simp only: N);
wenzelm@7432
    61
      qed;
wenzelm@7432
    62
    qed;
wenzelm@7442
    63
  }}; note tedious_reasoning = this;
wenzelm@7432
    64
wenzelm@7432
    65
wenzelm@7432
    66
  assume wf: "wf r";
wenzelm@7432
    67
  fix M;
wenzelm@7480
    68
  show "M : ?W";
wenzelm@7442
    69
  proof (rule multiset_induct [of _ M]);
wenzelm@7480
    70
    show "{#} : ?W";
wenzelm@7432
    71
    proof (rule accI);
wenzelm@7480
    72
      fix b; assume "(b, {#}) : ?R";
wenzelm@7480
    73
      with not_less_empty; show "b : ?W"; by contradiction;
wenzelm@7432
    74
    qed;
wenzelm@7432
    75
wenzelm@7480
    76
    fix M a; assume "M : ?W";
wenzelm@7480
    77
    from wf; have "ALL M:?W. M + {#a#} : ?W";
wenzelm@7442
    78
    proof (rule wf_induct [of r]);
wenzelm@7480
    79
      fix a; assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)";
wenzelm@7480
    80
      show "ALL M:?W. M + {#a#} : ?W";
wenzelm@7432
    81
      proof;
wenzelm@7480
    82
	fix M; assume "M : ?W";
wenzelm@7480
    83
	thus "M + {#a#} : ?W"; by (rule acc_induct) (rule tedious_reasoning);
wenzelm@7432
    84
      qed;
wenzelm@7432
    85
    qed;
wenzelm@7480
    86
    thus "M + {#a#} : ?W"; ..;
wenzelm@7432
    87
  qed;
wenzelm@7432
    88
qed;
wenzelm@7432
    89
wenzelm@7432
    90
wenzelm@7432
    91
theorem wf_mult1: "wf r ==> wf (mult1 r)";
wenzelm@7432
    92
  by (rule acc_wfI, rule all_accessible);
wenzelm@7432
    93
wenzelm@7432
    94
theorem wf_mult: "wf r ==> wf (mult r)";
wenzelm@7432
    95
  by (unfold mult_def, rule wf_trancl, rule wf_mult1);
wenzelm@7432
    96
wenzelm@7432
    97
wenzelm@7432
    98
end;