summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Isar_examples/MultisetOrder.thy

author | wenzelm |

Thu, 09 Sep 1999 12:25:44 +0200 | |

changeset 7530 | 505f6f8e9dcf |

parent 7527 | 9e2dddd8b81f |

child 7565 | bfa85f429629 |

permissions | -rw-r--r-- |

tuned;

(* Title: HOL/Isar_examples/MultisetOrder.thy ID: $Id$ Author: Markus Wenzel Wellfoundedness proof for the multiset order. Original tactic script by Tobias Nipkow (see also HOL/Induct/Multiset). Pen-and-paper proof by Wilfried Buchholz. *) theory MultisetOrder = Multiset:; lemma less_add: "(N, M0 + {#a#}) : mult1 r ==> (EX M. (M, M0) : mult1 r & N = M + {#a#}) | (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)" (concl is "?case1 (mult1 r) | ?case2"); proof (unfold mult1_def); let ?r = "%K a. ALL b. elem K b --> (b, a) : r"; let ?R = "%N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a"; let ?case1 = "?case1 {(N, M). ?R N M}"; assume "(N, M0 + {#a#}) : {(N, M). ?R N M}"; hence "EX a' M0' K. M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp; thus "?case1 | ?case2"; proof (elim exE conjE); fix a' M0' K; assume N: "N = M0' + K" and r: "?r K a'"; assume "M0 + {#a#} = M0' + {#a'#}"; hence "M0 = M0' & a = a' | (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})"; by (simp only: add_eq_conv_ex); thus ?thesis; proof (elim disjE conjE exE); assume "M0 = M0'" "a = a'"; with N r; have "?r K a & N = M0 + K"; by simp; hence ?case2; ..; thus ?thesis; ..; next; fix K'; assume "M0' = K' + {#a#}"; with N; have n: "N = K' + K + {#a#}"; by (simp add: union_ac); assume "M0 = K' + {#a'#}"; with r; have "?R (K' + K) M0"; by simp blast; with n; have ?case1; by simp; thus ?thesis; ..; qed; qed; qed; lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)"; proof; let ?R = "mult1 r"; let ?W = "acc ?R"; {{; fix M M0 a; assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)" and M0: "M0 : ?W" and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W"; have "M0 + {#a#} : ?W"; proof (rule accI [of "M0 + {#a#}"]); fix N; assume "(N, M0 + {#a#}) : ?R"; hence "((EX M. (M, M0) : ?R & N = M + {#a#}) | (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))"; by (rule less_add); thus "N : ?W"; proof (elim exE disjE conjE); fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}"; from acc_hyp; have "(M, M0) : ?R --> M + {#a#} : ?W"; ..; hence "M + {#a#} : ?W"; ..; thus "N : ?W"; by (simp only: N); next; fix K; assume N: "N = M0 + K"; assume "ALL b. elem K b --> (b, a) : r"; have "?this --> M0 + K : ?W" (is "?P K"); proof (induct K rule: multiset_induct); from M0; have "M0 + {#} : ?W"; by simp; thus "?P {#}"; ..; fix K x; assume hyp: "?P K"; show "?P (K + {#x#})"; proof; assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r"; hence "(x, a) : r"; by simp; with wf_hyp [RS spec]; have b: "ALL M:?W. M + {#x#} : ?W"; ..; from a hyp; have "M0 + K : ?W"; by simp; with b; have "(M0 + K) + {#x#} : ?W"; ..; thus "M0 + (K + {#x#}) : ?W"; by (simp only: union_assoc); qed; qed; hence "M0 + K : ?W"; ..; thus "N : ?W"; by (simp only: N); qed; qed; }}; note tedious_reasoning = this; assume wf: "wf r"; fix M; show "M : ?W"; proof (induct M rule: multiset_induct); show "{#} : ?W"; proof (rule accI); fix b; assume "(b, {#}) : ?R"; with not_less_empty; show "b : ?W"; by contradiction; qed; fix M a; assume "M : ?W"; from wf; have "ALL M:?W. M + {#a#} : ?W"; proof (rule wf_induct [of r]); fix a; assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"; show "ALL M:?W. M + {#a#} : ?W"; proof; fix M; assume "M : ?W"; thus "M + {#a#} : ?W"; by (rule acc_induct) (rule tedious_reasoning); qed; qed; thus "M + {#a#} : ?W"; ..; qed; qed; theorem wf_mult1: "wf r ==> wf (mult1 r)"; by (rule acc_wfI, rule all_accessible); theorem wf_mult: "wf r ==> wf (mult r)"; by (unfold mult_def, rule wf_trancl, rule wf_mult1); end;