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