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