author | wenzelm |
Sun, 26 Mar 2000 20:16:34 +0200 | |
changeset 8584 | 016314c2fa0a |
parent 8304 | e132d147374b |
child 8902 | a705822f4e2a |
permissions | -rw-r--r-- |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Isar_examples/MultisetOrder.thy |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
4 |
|
7442 | 5 |
Wellfoundedness proof for the multiset order. |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
6 |
*) |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
7 |
|
7761 | 8 |
header {* Wellfoundedness of multiset ordering *}; |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
9 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
10 |
theory MultisetOrder = Multiset:; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
11 |
|
7968 | 12 |
text_raw {* |
7982 | 13 |
\footnote{Original tactic script by Tobias Nipkow (see |
7968 | 14 |
\url{http://isabelle.in.tum.de/library/HOL/Induct/Multiset.html}), |
8584 | 15 |
based on a pen-and-paper proof due to Wilfried Buchholz.}\isanewline |
7968 | 16 |
*}; |
7527 | 17 |
|
8304 | 18 |
(* FIXME move? *) |
19 |
theorems [induct type: multiset] = multiset_induct; |
|
20 |
theorems [induct set: wf] = wf_induct; |
|
21 |
theorems [induct set: acc] = acc_induct; |
|
22 |
||
23 |
||
7761 | 24 |
subsection {* A technical lemma *}; |
25 |
||
7527 | 26 |
lemma less_add: "(N, M0 + {#a#}) : mult1 r ==> |
27 |
(EX M. (M, M0) : mult1 r & N = M + {#a#}) | |
|
28 |
(EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)" |
|
29 |
(concl is "?case1 (mult1 r) | ?case2"); |
|
30 |
proof (unfold mult1_def); |
|
8281 | 31 |
let ?r = "\\<lambda>K a. ALL b. elem K b --> (b, a) : r"; |
32 |
let ?R = "\\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a"; |
|
7527 | 33 |
let ?case1 = "?case1 {(N, M). ?R N M}"; |
34 |
||
35 |
assume "(N, M0 + {#a#}) : {(N, M). ?R N M}"; |
|
7800 | 36 |
hence "EX a' M0' K. |
37 |
M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp; |
|
7527 | 38 |
thus "?case1 | ?case2"; |
39 |
proof (elim exE conjE); |
|
7874 | 40 |
fix a' M0' K; |
41 |
assume N: "N = M0' + K" and r: "?r K a'"; |
|
7527 | 42 |
assume "M0 + {#a#} = M0' + {#a'#}"; |
7800 | 43 |
hence "M0 = M0' & a = a' | |
44 |
(EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})"; |
|
7527 | 45 |
by (simp only: add_eq_conv_ex); |
46 |
thus ?thesis; |
|
47 |
proof (elim disjE conjE exE); |
|
48 |
assume "M0 = M0'" "a = a'"; |
|
49 |
with N r; have "?r K a & N = M0 + K"; by simp; |
|
50 |
hence ?case2; ..; thus ?thesis; ..; |
|
51 |
next; |
|
52 |
fix K'; |
|
53 |
assume "M0' = K' + {#a#}"; |
|
54 |
with N; have n: "N = K' + K + {#a#}"; by (simp add: union_ac); |
|
55 |
||
56 |
assume "M0 = K' + {#a'#}"; |
|
7565 | 57 |
with r; have "?R (K' + K) M0"; by blast; |
7527 | 58 |
with n; have ?case1; by simp; thus ?thesis; ..; |
59 |
qed; |
|
60 |
qed; |
|
61 |
qed; |
|
62 |
||
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
63 |
|
7761 | 64 |
subsection {* The key property *}; |
65 |
||
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
66 |
lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
67 |
proof; |
7480 | 68 |
let ?R = "mult1 r"; |
69 |
let ?W = "acc ?R"; |
|
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
70 |
{{; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
71 |
fix M M0 a; |
7800 | 72 |
assume M0: "M0 : ?W" |
73 |
and wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)" |
|
7480 | 74 |
and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W"; |
75 |
have "M0 + {#a#} : ?W"; |
|
7442 | 76 |
proof (rule accI [of "M0 + {#a#}"]); |
7874 | 77 |
fix N; |
78 |
assume "(N, M0 + {#a#}) : ?R"; |
|
7480 | 79 |
hence "((EX M. (M, M0) : ?R & N = M + {#a#}) | |
7800 | 80 |
(EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))"; |
7527 | 81 |
by (rule less_add); |
7480 | 82 |
thus "N : ?W"; |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
83 |
proof (elim exE disjE conjE); |
7480 | 84 |
fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}"; |
85 |
from acc_hyp; have "(M, M0) : ?R --> M + {#a#} : ?W"; ..; |
|
86 |
hence "M + {#a#} : ?W"; ..; |
|
87 |
thus "N : ?W"; by (simp only: N); |
|
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
88 |
next; |
7451 | 89 |
fix K; |
90 |
assume N: "N = M0 + K"; |
|
91 |
assume "ALL b. elem K b --> (b, a) : r"; |
|
7480 | 92 |
have "?this --> M0 + K : ?W" (is "?P K"); |
8304 | 93 |
proof (induct K); |
7480 | 94 |
from M0; have "M0 + {#} : ?W"; by simp; |
95 |
thus "?P {#}"; ..; |
|
7442 | 96 |
|
7480 | 97 |
fix K x; assume hyp: "?P K"; |
98 |
show "?P (K + {#x#})"; |
|
7442 | 99 |
proof; |
7451 | 100 |
assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r"; |
7442 | 101 |
hence "(x, a) : r"; by simp; |
7800 | 102 |
with wf_hyp; have b: "ALL M:?W. M + {#x#} : ?W"; by blast; |
7442 | 103 |
|
7480 | 104 |
from a hyp; have "M0 + K : ?W"; by simp; |
105 |
with b; have "(M0 + K) + {#x#} : ?W"; ..; |
|
106 |
thus "M0 + (K + {#x#}) : ?W"; by (simp only: union_assoc); |
|
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
107 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
108 |
qed; |
7480 | 109 |
hence "M0 + K : ?W"; ..; |
110 |
thus "N : ?W"; by (simp only: N); |
|
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
111 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
112 |
qed; |
7442 | 113 |
}}; note tedious_reasoning = this; |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
114 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
115 |
assume wf: "wf r"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
116 |
fix M; |
7480 | 117 |
show "M : ?W"; |
8304 | 118 |
proof (induct M); |
7480 | 119 |
show "{#} : ?W"; |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
120 |
proof (rule accI); |
7480 | 121 |
fix b; assume "(b, {#}) : ?R"; |
122 |
with not_less_empty; show "b : ?W"; by contradiction; |
|
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
123 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
124 |
|
7480 | 125 |
fix M a; assume "M : ?W"; |
126 |
from wf; have "ALL M:?W. M + {#a#} : ?W"; |
|
8304 | 127 |
proof induct; |
7800 | 128 |
fix a; |
129 |
assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"; |
|
7480 | 130 |
show "ALL M:?W. M + {#a#} : ?W"; |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
131 |
proof; |
7480 | 132 |
fix M; assume "M : ?W"; |
7800 | 133 |
thus "M + {#a#} : ?W"; |
134 |
by (rule acc_induct) (rule tedious_reasoning); |
|
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
135 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
136 |
qed; |
7480 | 137 |
thus "M + {#a#} : ?W"; ..; |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
138 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
139 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
140 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
141 |
|
7761 | 142 |
subsection {* Main result *}; |
143 |
||
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
144 |
theorem wf_mult1: "wf r ==> wf (mult1 r)"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
145 |
by (rule acc_wfI, rule all_accessible); |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
146 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
147 |
theorem wf_mult: "wf r ==> wf (mult r)"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
148 |
by (unfold mult_def, rule wf_trancl, rule wf_mult1); |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
149 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
150 |
end; |