12 theory MultisetOrder = Multiset:; |
12 theory MultisetOrder = Multiset:; |
13 |
13 |
14 |
14 |
15 lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)"; |
15 lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)"; |
16 proof; |
16 proof; |
17 let ??R = "mult1 r"; |
17 let ?R = "mult1 r"; |
18 let ??W = "acc ??R"; |
18 let ?W = "acc ?R"; |
19 |
19 |
20 |
20 |
21 {{; |
21 {{; |
22 fix M M0 a; |
22 fix M M0 a; |
23 assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:??W. M + {#b#} : ??W)" |
23 assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)" |
24 and M0: "M0 : ??W" |
24 and M0: "M0 : ?W" |
25 and acc_hyp: "ALL M. (M, M0) : ??R --> M + {#a#} : ??W"; |
25 and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W"; |
26 have "M0 + {#a#} : ??W"; |
26 have "M0 + {#a#} : ?W"; |
27 proof (rule accI [of "M0 + {#a#}"]); |
27 proof (rule accI [of "M0 + {#a#}"]); |
28 fix N; assume "(N, M0 + {#a#}) : ??R"; |
28 fix N; assume "(N, M0 + {#a#}) : ?R"; |
29 hence "((EX M. (M, M0) : ??R & N = M + {#a#}) | |
29 hence "((EX M. (M, M0) : ?R & N = M + {#a#}) | |
30 (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))"; |
30 (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))"; |
31 by (simp only: less_add_conv); |
31 by (simp only: less_add_conv); |
32 thus "N : ??W"; |
32 thus "N : ?W"; |
33 proof (elim exE disjE conjE); |
33 proof (elim exE disjE conjE); |
34 fix M; assume "(M, M0) : ??R" and N: "N = M + {#a#}"; |
34 fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}"; |
35 from acc_hyp; have "(M, M0) : ??R --> M + {#a#} : ??W"; ..; |
35 from acc_hyp; have "(M, M0) : ?R --> M + {#a#} : ?W"; ..; |
36 hence "M + {#a#} : ??W"; ..; |
36 hence "M + {#a#} : ?W"; ..; |
37 thus "N : ??W"; by (simp only: N); |
37 thus "N : ?W"; by (simp only: N); |
38 next; |
38 next; |
39 fix K; |
39 fix K; |
40 assume N: "N = M0 + K"; |
40 assume N: "N = M0 + K"; |
41 assume "ALL b. elem K b --> (b, a) : r"; |
41 assume "ALL b. elem K b --> (b, a) : r"; |
42 have "??this --> M0 + K : ??W" (is "??P K"); |
42 have "?this --> M0 + K : ?W" (is "?P K"); |
43 proof (rule multiset_induct [of _ K]); |
43 proof (rule multiset_induct [of _ K]); |
44 from M0; have "M0 + {#} : ??W"; by simp; |
44 from M0; have "M0 + {#} : ?W"; by simp; |
45 thus "??P {#}"; ..; |
45 thus "?P {#}"; ..; |
46 |
46 |
47 fix K x; assume hyp: "??P K"; |
47 fix K x; assume hyp: "?P K"; |
48 show "??P (K + {#x#})"; |
48 show "?P (K + {#x#})"; |
49 proof; |
49 proof; |
50 assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r"; |
50 assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r"; |
51 hence "(x, a) : r"; by simp; |
51 hence "(x, a) : r"; by simp; |
52 with wf_hyp [RS spec]; have b: "ALL M:??W. M + {#x#} : ??W"; ..; |
52 with wf_hyp [RS spec]; have b: "ALL M:?W. M + {#x#} : ?W"; ..; |
53 |
53 |
54 from a hyp; have "M0 + K : ??W"; by simp; |
54 from a hyp; have "M0 + K : ?W"; by simp; |
55 with b; have "(M0 + K) + {#x#} : ??W"; ..; |
55 with b; have "(M0 + K) + {#x#} : ?W"; ..; |
56 thus "M0 + (K + {#x#}) : ??W"; by (simp only: union_assoc); |
56 thus "M0 + (K + {#x#}) : ?W"; by (simp only: union_assoc); |
57 qed; |
57 qed; |
58 qed; |
58 qed; |
59 hence "M0 + K : ??W"; ..; |
59 hence "M0 + K : ?W"; ..; |
60 thus "N : ??W"; by (simp only: N); |
60 thus "N : ?W"; by (simp only: N); |
61 qed; |
61 qed; |
62 qed; |
62 qed; |
63 }}; note tedious_reasoning = this; |
63 }}; note tedious_reasoning = this; |
64 |
64 |
65 |
65 |
66 assume wf: "wf r"; |
66 assume wf: "wf r"; |
67 fix M; |
67 fix M; |
68 show "M : ??W"; |
68 show "M : ?W"; |
69 proof (rule multiset_induct [of _ M]); |
69 proof (rule multiset_induct [of _ M]); |
70 show "{#} : ??W"; |
70 show "{#} : ?W"; |
71 proof (rule accI); |
71 proof (rule accI); |
72 fix b; assume "(b, {#}) : ??R"; |
72 fix b; assume "(b, {#}) : ?R"; |
73 with not_less_empty; show "b : ??W"; by contradiction; |
73 with not_less_empty; show "b : ?W"; by contradiction; |
74 qed; |
74 qed; |
75 |
75 |
76 fix M a; assume "M : ??W"; |
76 fix M a; assume "M : ?W"; |
77 from wf; have "ALL M:??W. M + {#a#} : ??W"; |
77 from wf; have "ALL M:?W. M + {#a#} : ?W"; |
78 proof (rule wf_induct [of r]); |
78 proof (rule wf_induct [of r]); |
79 fix a; assume "ALL b. (b, a) : r --> (ALL M:??W. M + {#b#} : ??W)"; |
79 fix a; assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"; |
80 show "ALL M:??W. M + {#a#} : ??W"; |
80 show "ALL M:?W. M + {#a#} : ?W"; |
81 proof; |
81 proof; |
82 fix M; assume "M : ??W"; |
82 fix M; assume "M : ?W"; |
83 thus "M + {#a#} : ??W"; by (rule acc_induct) (rule tedious_reasoning); |
83 thus "M + {#a#} : ?W"; by (rule acc_induct) (rule tedious_reasoning); |
84 qed; |
84 qed; |
85 qed; |
85 qed; |
86 thus "M + {#a#} : ??W"; ..; |
86 thus "M + {#a#} : ?W"; ..; |
87 qed; |
87 qed; |
88 qed; |
88 qed; |
89 |
89 |
90 |
90 |
91 theorem wf_mult1: "wf r ==> wf (mult1 r)"; |
91 theorem wf_mult1: "wf r ==> wf (mult1 r)"; |