src/HOL/Isar_examples/MultisetOrder.thy
author wenzelm
Sat Oct 30 20:20:48 1999 +0200 (1999-10-30)
changeset 7982 d534b897ce39
parent 7968 964b65b4e433
child 8281 188e2924433e
permissions -rw-r--r--
improved presentation;
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@7432
     6
*)
wenzelm@7432
     7
wenzelm@7761
     8
header {* Wellfoundedness of multiset ordering *};
wenzelm@7432
     9
wenzelm@7432
    10
theory MultisetOrder = Multiset:;
wenzelm@7432
    11
wenzelm@7968
    12
text_raw {*
wenzelm@7982
    13
 \footnote{Original tactic script by Tobias Nipkow (see
wenzelm@7968
    14
 \url{http://isabelle.in.tum.de/library/HOL/Induct/Multiset.html}),
wenzelm@7968
    15
 based on a pen-and-paper proof due to Wilfried Buchholz.}
wenzelm@7968
    16
*};
wenzelm@7527
    17
wenzelm@7761
    18
subsection {* A technical lemma *};
wenzelm@7761
    19
wenzelm@7527
    20
lemma less_add: "(N, M0 + {#a#}) : mult1 r ==>
wenzelm@7527
    21
    (EX M. (M, M0) : mult1 r & N = M + {#a#}) |
wenzelm@7527
    22
    (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"
wenzelm@7527
    23
  (concl is "?case1 (mult1 r) | ?case2");
wenzelm@7527
    24
proof (unfold mult1_def);
wenzelm@7982
    25
  let ?r = "\<lambda>K a. ALL b. elem K b --> (b, a) : r";
wenzelm@7982
    26
  let ?R = "\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
wenzelm@7527
    27
  let ?case1 = "?case1 {(N, M). ?R N M}";
wenzelm@7527
    28
wenzelm@7527
    29
  assume "(N, M0 + {#a#}) : {(N, M). ?R N M}";
wenzelm@7800
    30
  hence "EX a' M0' K.
wenzelm@7800
    31
      M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp;
wenzelm@7527
    32
  thus "?case1 | ?case2";
wenzelm@7527
    33
  proof (elim exE conjE);
wenzelm@7874
    34
    fix a' M0' K;
wenzelm@7874
    35
    assume N: "N = M0' + K" and r: "?r K a'";
wenzelm@7527
    36
    assume "M0 + {#a#} = M0' + {#a'#}";
wenzelm@7800
    37
    hence "M0 = M0' & a = a' |
wenzelm@7800
    38
        (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})";
wenzelm@7527
    39
      by (simp only: add_eq_conv_ex);
wenzelm@7527
    40
    thus ?thesis;
wenzelm@7527
    41
    proof (elim disjE conjE exE);
wenzelm@7527
    42
      assume "M0 = M0'" "a = a'";
wenzelm@7527
    43
      with N r; have "?r K a & N = M0 + K"; by simp;
wenzelm@7527
    44
      hence ?case2; ..; thus ?thesis; ..;
wenzelm@7527
    45
    next;
wenzelm@7527
    46
      fix K';
wenzelm@7527
    47
      assume "M0' = K' + {#a#}";
wenzelm@7527
    48
      with N; have n: "N = K' + K + {#a#}"; by (simp add: union_ac);
wenzelm@7527
    49
wenzelm@7527
    50
      assume "M0 = K' + {#a'#}";
wenzelm@7565
    51
      with r; have "?R (K' + K) M0"; by blast;
wenzelm@7527
    52
      with n; have ?case1; by simp; thus ?thesis; ..;
wenzelm@7527
    53
    qed;
wenzelm@7527
    54
  qed;
wenzelm@7527
    55
qed;
wenzelm@7527
    56
wenzelm@7432
    57
wenzelm@7761
    58
subsection {* The key property *};
wenzelm@7761
    59
wenzelm@7432
    60
lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)";
wenzelm@7432
    61
proof;
wenzelm@7480
    62
  let ?R = "mult1 r";
wenzelm@7480
    63
  let ?W = "acc ?R";
wenzelm@7432
    64
  {{;
wenzelm@7432
    65
    fix M M0 a;
wenzelm@7800
    66
    assume M0: "M0 : ?W"
wenzelm@7800
    67
      and wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
wenzelm@7480
    68
      and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W";
wenzelm@7480
    69
    have "M0 + {#a#} : ?W";
wenzelm@7442
    70
    proof (rule accI [of "M0 + {#a#}"]);
wenzelm@7874
    71
      fix N;
wenzelm@7874
    72
      assume "(N, M0 + {#a#}) : ?R";
wenzelm@7480
    73
      hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
wenzelm@7800
    74
          (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
wenzelm@7527
    75
	by (rule less_add);
wenzelm@7480
    76
      thus "N : ?W";
wenzelm@7432
    77
      proof (elim exE disjE conjE);
wenzelm@7480
    78
	fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}";
wenzelm@7480
    79
	from acc_hyp; have "(M, M0) : ?R --> M + {#a#} : ?W"; ..;
wenzelm@7480
    80
	hence "M + {#a#} : ?W"; ..;
wenzelm@7480
    81
	thus "N : ?W"; by (simp only: N);
wenzelm@7432
    82
      next;
wenzelm@7451
    83
	fix K;
wenzelm@7451
    84
	assume N: "N = M0 + K";
wenzelm@7451
    85
	assume "ALL b. elem K b --> (b, a) : r";
wenzelm@7480
    86
	have "?this --> M0 + K : ?W" (is "?P K");
wenzelm@7527
    87
	proof (induct K rule: multiset_induct);
wenzelm@7480
    88
	  from M0; have "M0 + {#} : ?W"; by simp;
wenzelm@7480
    89
	  thus "?P {#}"; ..;
wenzelm@7442
    90
wenzelm@7480
    91
	  fix K x; assume hyp: "?P K";
wenzelm@7480
    92
	  show "?P (K + {#x#})";
wenzelm@7442
    93
	  proof;
wenzelm@7451
    94
	    assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r";
wenzelm@7442
    95
	    hence "(x, a) : r"; by simp;
wenzelm@7800
    96
	    with wf_hyp; have b: "ALL M:?W. M + {#x#} : ?W"; by blast;
wenzelm@7442
    97
wenzelm@7480
    98
	    from a hyp; have "M0 + K : ?W"; by simp;
wenzelm@7480
    99
	    with b; have "(M0 + K) + {#x#} : ?W"; ..;
wenzelm@7480
   100
	    thus "M0 + (K + {#x#}) : ?W"; by (simp only: union_assoc);
wenzelm@7432
   101
	  qed;
wenzelm@7432
   102
	qed;
wenzelm@7480
   103
	hence "M0 + K : ?W"; ..;
wenzelm@7480
   104
	thus "N : ?W"; by (simp only: N);
wenzelm@7432
   105
      qed;
wenzelm@7432
   106
    qed;
wenzelm@7442
   107
  }}; note tedious_reasoning = this;
wenzelm@7432
   108
wenzelm@7432
   109
  assume wf: "wf r";
wenzelm@7432
   110
  fix M;
wenzelm@7480
   111
  show "M : ?W";
wenzelm@7527
   112
  proof (induct M rule: multiset_induct);
wenzelm@7480
   113
    show "{#} : ?W";
wenzelm@7432
   114
    proof (rule accI);
wenzelm@7480
   115
      fix b; assume "(b, {#}) : ?R";
wenzelm@7480
   116
      with not_less_empty; show "b : ?W"; by contradiction;
wenzelm@7432
   117
    qed;
wenzelm@7432
   118
wenzelm@7480
   119
    fix M a; assume "M : ?W";
wenzelm@7480
   120
    from wf; have "ALL M:?W. M + {#a#} : ?W";
wenzelm@7442
   121
    proof (rule wf_induct [of r]);
wenzelm@7800
   122
      fix a;
wenzelm@7800
   123
      assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)";
wenzelm@7480
   124
      show "ALL M:?W. M + {#a#} : ?W";
wenzelm@7432
   125
      proof;
wenzelm@7480
   126
	fix M; assume "M : ?W";
wenzelm@7800
   127
	thus "M + {#a#} : ?W";
wenzelm@7800
   128
          by (rule acc_induct) (rule tedious_reasoning);
wenzelm@7432
   129
      qed;
wenzelm@7432
   130
    qed;
wenzelm@7480
   131
    thus "M + {#a#} : ?W"; ..;
wenzelm@7432
   132
  qed;
wenzelm@7432
   133
qed;
wenzelm@7432
   134
wenzelm@7432
   135
wenzelm@7761
   136
subsection {* Main result *};
wenzelm@7761
   137
wenzelm@7432
   138
theorem wf_mult1: "wf r ==> wf (mult1 r)";
wenzelm@7432
   139
  by (rule acc_wfI, rule all_accessible);
wenzelm@7432
   140
wenzelm@7432
   141
theorem wf_mult: "wf r ==> wf (mult r)";
wenzelm@7432
   142
  by (unfold mult_def, rule wf_trancl, rule wf_mult1);
wenzelm@7432
   143
wenzelm@7432
   144
end;