summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 18 Oct 2000 23:35:08 +0200 | |

changeset 10256 | 320a4084dfac |

parent 10255 | bb66874b4750 |

child 10257 | 21055ac27708 |

moved to HOL/LIbrary;

src/HOL/Isar_examples/MultisetOrder.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Isar_examples/MultisetOrder.thy Wed Oct 18 23:33:04 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,148 +0,0 @@ -(* Title: HOL/Isar_examples/MultisetOrder.thy - ID: $Id$ - Author: Markus Wenzel - -Wellfoundedness proof for the multiset order. -*) - -header {* Wellfoundedness of multiset ordering *} - -theory MultisetOrder = Multiset: - -text_raw {* - \footnote{Original tactic script by Tobias Nipkow (see - \url{http://isabelle.in.tum.de/library/HOL/Induct/Multiset.html}), - based on a pen-and-paper proof due to Wilfried Buchholz.}\isanewline -*} -(*<*)(* FIXME move? *) -declare multiset_induct [induct type: multiset] -declare wf_induct [induct set: wf] -declare acc_induct [induct set: acc](*>*) - -subsection {* A technical lemma *} - -lemma less_add: "(N, M0 + {#a#}) : mult1 r ==> - (EX M. (M, M0) : mult1 r & N = M + {#a#}) | - (EX K. (ALL b. b :# K --> (b, a) : r) & N = M0 + K)" - (concl is "?case1 (mult1 r) | ?case2") -proof (unfold mult1_def) - let ?r = "\<lambda>K a. ALL b. b :# K --> (b, a) : r" - let ?R = "\<lambda>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 blast - with n have ?case1 by simp thus ?thesis .. - qed - qed -qed - - -subsection {* The key property *} - -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 M0: "M0 : ?W" - and wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?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. b :# K --> (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. b :# K --> (b, a) : r" - have "?this --> M0 + K : ?W" (is "?P K") - proof (induct K) - 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. b :# (K + {#x#}) --> (b, a) : r" - hence "(x, a) : r" by simp - with wf_hyp have b: "ALL M:?W. M + {#x#} : ?W" by blast - - 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) - 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 induct - 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 - - -subsection {* Main result *} - -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