--- 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