author wenzelm Wed, 08 Sep 1999 23:49:39 +0200 changeset 7527 9e2dddd8b81f parent 7526 1ea137d3b5bf child 7528 ee5f37e4f186
```--- a/src/HOL/Isar_examples/MultisetOrder.thy	Wed Sep 08 18:10:39 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy	Wed Sep 08 23:49:39 1999 +0200
@@ -11,6 +11,44 @@

theory MultisetOrder = Multiset:;

+(* FIXME *)
+theorems [intro!!] = disjI1 disjI2;
+
+
+lemma less_add: "(N, M0 + {#a#}) : mult1 r ==>
+    (EX M. (M, M0) : mult1 r & N = M + {#a#}) |
+    (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"
+  (concl is "?case1 (mult1 r) | ?case2");
+proof (unfold mult1_def);
+  let ?r = "%K a. ALL b. elem K b --> (b, a) : r";
+  let ?R = "%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#})";
+    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 simp blast;
+      with n; have ?case1; by simp; thus ?thesis; ..;
+    qed;
+  qed;
+qed;
+

lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)";
proof;
@@ -28,7 +66,7 @@
fix N; assume "(N, M0 + {#a#}) : ?R";
hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
(EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
thus "N : ?W";
proof (elim exE disjE conjE);
fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}";
@@ -40,7 +78,7 @@
assume N: "N = M0 + K";
assume "ALL b. elem K b --> (b, a) : r";
have "?this --> M0 + K : ?W" (is "?P K");
-	proof (rule multiset_induct [of _ K]);
+	proof (induct K rule: multiset_induct);
from M0; have "M0 + {#} : ?W"; by simp;
thus "?P {#}"; ..;

@@ -66,7 +104,7 @@
assume wf: "wf r";
fix M;
show "M : ?W";
-  proof (rule multiset_induct [of _ M]);
+  proof (induct M rule: multiset_induct);
show "{#} : ?W";
proof (rule accI);
fix b; assume "(b, {#}) : ?R";```