author | wenzelm |
Fri, 03 Sep 1999 14:22:12 +0200 | |
changeset 7448 | 3ee96dccdd39 |
parent 7442 | 2d2849258e3f |
child 7451 | d643b3c4996a |
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. |
6 |
||
7 |
Original tactic script by Tobias Nipkow (see also |
|
8 |
HOL/Induct/Multiset). Pen-and-paper proof by Wilfried Buchholz. |
|
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 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
11 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
12 |
theory MultisetOrder = Multiset:; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
13 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
14 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
15 |
lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
16 |
proof; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
17 |
let ??R = "mult1 r"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
18 |
let ??W = "acc ??R"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
19 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
20 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
21 |
{{; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
22 |
fix M M0 a; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
23 |
assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:??W. M + {#b#} : ??W)" |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
24 |
and M0: "M0 : ??W" |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
25 |
and acc_hyp: "ALL M. (M, M0) : ??R --> M + {#a#} : ??W"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
26 |
have "M0 + {#a#} : ??W"; |
7442 | 27 |
proof (rule accI [of "M0 + {#a#}"]); |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
28 |
fix N; assume "(N, M0 + {#a#}) : ??R"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
29 |
hence "((EX M. (M, M0) : ??R & N = M + {#a#}) | |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
30 |
(EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
31 |
by (simp only: less_add_conv); |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
32 |
thus "N : ??W"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
33 |
proof (elim exE disjE conjE); |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
34 |
fix M; assume "(M, M0) : ??R" and N: "N = M + {#a#}"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
35 |
from acc_hyp; have "(M, M0) : ??R --> M + {#a#} : ??W"; ..; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
36 |
hence "M + {#a#} : ??W"; ..; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
37 |
thus "N : ??W"; by (simp only: N); |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
38 |
next; |
7448 | 39 |
fix K; assume "ALL b. elem K b --> (b, a) : r" (is "??A K") |
7442 | 40 |
and N: "N = M0 + K"; |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
41 |
|
7448 | 42 |
have "??A K --> M0 + K : ??W" (is "??P K"); |
7442 | 43 |
proof (rule multiset_induct [of _ K]); |
44 |
from M0; have "M0 + {#} : ??W"; by simp; |
|
45 |
thus "??P {#}"; ..; |
|
46 |
||
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
47 |
fix K x; assume hyp: "??P K"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
48 |
show "??P (K + {#x#})"; |
7442 | 49 |
proof; |
7448 | 50 |
assume a: "??A (K + {#x#})"; |
7442 | 51 |
hence "(x, a) : r"; by simp; |
52 |
with wf_hyp [RS spec]; have b: "ALL M:??W. M + {#x#} : ??W"; ..; |
|
53 |
||
54 |
from a hyp; have "M0 + K : ??W"; by simp; |
|
55 |
with b; have "(M0 + K) + {#x#} : ??W"; ..; |
|
56 |
thus "M0 + (K + {#x#}) : ??W"; by (simp only: union_assoc); |
|
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
57 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
58 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
59 |
hence "M0 + K : ??W"; ..; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
60 |
thus "N : ??W"; by (simp only: N); |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
61 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
62 |
qed; |
7442 | 63 |
}}; note tedious_reasoning = this; |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
64 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
65 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
66 |
assume wf: "wf r"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
67 |
fix M; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
68 |
show "M : ??W"; |
7442 | 69 |
proof (rule multiset_induct [of _ M]); |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
70 |
show "{#} : ??W"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
71 |
proof (rule accI); |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
72 |
fix b; assume "(b, {#}) : ??R"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
73 |
with not_less_empty; show "b : ??W"; by contradiction; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
74 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
75 |
|
7442 | 76 |
fix M a; assume "M : ??W"; |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
77 |
from wf; have "ALL M:??W. M + {#a#} : ??W"; |
7442 | 78 |
proof (rule wf_induct [of r]); |
79 |
fix a; assume "ALL b. (b, a) : r --> (ALL M:??W. M + {#b#} : ??W)"; |
|
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
80 |
show "ALL M:??W. M + {#a#} : ??W"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
81 |
proof; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
82 |
fix M; assume "M : ??W"; |
7442 | 83 |
thus "M + {#a#} : ??W"; by (rule acc_induct) (rule tedious_reasoning); |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
84 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
85 |
qed; |
7442 | 86 |
thus "M + {#a#} : ??W"; ..; |
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
87 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
88 |
qed; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
89 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
90 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
91 |
theorem wf_mult1: "wf r ==> wf (mult1 r)"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
92 |
by (rule acc_wfI, rule all_accessible); |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
93 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
94 |
theorem wf_mult: "wf r ==> wf (mult r)"; |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
95 |
by (unfold mult_def, rule wf_trancl, rule wf_mult1); |
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
96 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
97 |
|
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset
|
98 |
end; |