23 let ?r = "%K a. ALL b. elem K b --> (b, a) : r"; |
23 let ?r = "%K a. ALL b. elem K b --> (b, a) : r"; |
24 let ?R = "%N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a"; |
24 let ?R = "%N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a"; |
25 let ?case1 = "?case1 {(N, M). ?R N M}"; |
25 let ?case1 = "?case1 {(N, M). ?R N M}"; |
26 |
26 |
27 assume "(N, M0 + {#a#}) : {(N, M). ?R N M}"; |
27 assume "(N, M0 + {#a#}) : {(N, M). ?R N M}"; |
28 hence "EX a' M0' K. M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp; |
28 hence "EX a' M0' K. |
|
29 M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp; |
29 thus "?case1 | ?case2"; |
30 thus "?case1 | ?case2"; |
30 proof (elim exE conjE); |
31 proof (elim exE conjE); |
31 fix a' M0' K; assume N: "N = M0' + K" and r: "?r K a'"; |
32 fix a' M0' K; assume N: "N = M0' + K" and r: "?r K a'"; |
32 assume "M0 + {#a#} = M0' + {#a'#}"; |
33 assume "M0 + {#a#} = M0' + {#a'#}"; |
33 hence "M0 = M0' & a = a' | (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})"; |
34 hence "M0 = M0' & a = a' | |
|
35 (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})"; |
34 by (simp only: add_eq_conv_ex); |
36 by (simp only: add_eq_conv_ex); |
35 thus ?thesis; |
37 thus ?thesis; |
36 proof (elim disjE conjE exE); |
38 proof (elim disjE conjE exE); |
37 assume "M0 = M0'" "a = a'"; |
39 assume "M0 = M0'" "a = a'"; |
38 with N r; have "?r K a & N = M0 + K"; by simp; |
40 with N r; have "?r K a & N = M0 + K"; by simp; |
57 let ?R = "mult1 r"; |
59 let ?R = "mult1 r"; |
58 let ?W = "acc ?R"; |
60 let ?W = "acc ?R"; |
59 |
61 |
60 {{; |
62 {{; |
61 fix M M0 a; |
63 fix M M0 a; |
62 assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)" |
64 assume M0: "M0 : ?W" |
63 and M0: "M0 : ?W" |
65 and wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)" |
64 and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W"; |
66 and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W"; |
65 have "M0 + {#a#} : ?W"; |
67 have "M0 + {#a#} : ?W"; |
66 proof (rule accI [of "M0 + {#a#}"]); |
68 proof (rule accI [of "M0 + {#a#}"]); |
67 fix N; assume "(N, M0 + {#a#}) : ?R"; |
69 fix N; assume "(N, M0 + {#a#}) : ?R"; |
68 hence "((EX M. (M, M0) : ?R & N = M + {#a#}) | |
70 hence "((EX M. (M, M0) : ?R & N = M + {#a#}) | |
69 (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))"; |
71 (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))"; |
70 by (rule less_add); |
72 by (rule less_add); |
71 thus "N : ?W"; |
73 thus "N : ?W"; |
72 proof (elim exE disjE conjE); |
74 proof (elim exE disjE conjE); |
73 fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}"; |
75 fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}"; |
74 from acc_hyp; have "(M, M0) : ?R --> M + {#a#} : ?W"; ..; |
76 from acc_hyp; have "(M, M0) : ?R --> M + {#a#} : ?W"; ..; |
86 fix K x; assume hyp: "?P K"; |
88 fix K x; assume hyp: "?P K"; |
87 show "?P (K + {#x#})"; |
89 show "?P (K + {#x#})"; |
88 proof; |
90 proof; |
89 assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r"; |
91 assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r"; |
90 hence "(x, a) : r"; by simp; |
92 hence "(x, a) : r"; by simp; |
91 with wf_hyp [RS spec]; have b: "ALL M:?W. M + {#x#} : ?W"; ..; |
93 with wf_hyp; have b: "ALL M:?W. M + {#x#} : ?W"; by blast; |
92 |
94 |
93 from a hyp; have "M0 + K : ?W"; by simp; |
95 from a hyp; have "M0 + K : ?W"; by simp; |
94 with b; have "(M0 + K) + {#x#} : ?W"; ..; |
96 with b; have "(M0 + K) + {#x#} : ?W"; ..; |
95 thus "M0 + (K + {#x#}) : ?W"; by (simp only: union_assoc); |
97 thus "M0 + (K + {#x#}) : ?W"; by (simp only: union_assoc); |
96 qed; |
98 qed; |
112 qed; |
114 qed; |
113 |
115 |
114 fix M a; assume "M : ?W"; |
116 fix M a; assume "M : ?W"; |
115 from wf; have "ALL M:?W. M + {#a#} : ?W"; |
117 from wf; have "ALL M:?W. M + {#a#} : ?W"; |
116 proof (rule wf_induct [of r]); |
118 proof (rule wf_induct [of r]); |
117 fix a; assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"; |
119 fix a; |
|
120 assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"; |
118 show "ALL M:?W. M + {#a#} : ?W"; |
121 show "ALL M:?W. M + {#a#} : ?W"; |
119 proof; |
122 proof; |
120 fix M; assume "M : ?W"; |
123 fix M; assume "M : ?W"; |
121 thus "M + {#a#} : ?W"; by (rule acc_induct) (rule tedious_reasoning); |
124 thus "M + {#a#} : ?W"; |
|
125 by (rule acc_induct) (rule tedious_reasoning); |
122 qed; |
126 qed; |
123 qed; |
127 qed; |
124 thus "M + {#a#} : ?W"; ..; |
128 thus "M + {#a#} : ?W"; ..; |
125 qed; |
129 qed; |
126 qed; |
130 qed; |