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;