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