author  wenzelm 
Thu, 09 Sep 1999 12:25:44 +0200  
changeset 7530  505f6f8e9dcf 
parent 7527  9e2dddd8b81f 
child 7565  bfa85f429629 
permissions  rwrr 
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). Penandpaper 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 

7527  14 

15 
lemma less_add: "(N, M0 + {#a#}) : mult1 r ==> 

16 
(EX M. (M, M0) : mult1 r & N = M + {#a#})  

17 
(EX K. (ALL b. elem K b > (b, a) : r) & N = M0 + K)" 

18 
(concl is "?case1 (mult1 r)  ?case2"); 

19 
proof (unfold mult1_def); 

20 
let ?r = "%K a. ALL b. elem K b > (b, a) : r"; 

21 
let ?R = "%N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a"; 

22 
let ?case1 = "?case1 {(N, M). ?R N M}"; 

23 

24 
assume "(N, M0 + {#a#}) : {(N, M). ?R N M}"; 

25 
hence "EX a' M0' K. M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp; 

26 
thus "?case1  ?case2"; 

27 
proof (elim exE conjE); 

28 
fix a' M0' K; assume N: "N = M0' + K" and r: "?r K a'"; 

29 
assume "M0 + {#a#} = M0' + {#a'#}"; 

30 
hence "M0 = M0' & a = a'  (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})"; 

31 
by (simp only: add_eq_conv_ex); 

32 
thus ?thesis; 

33 
proof (elim disjE conjE exE); 

34 
assume "M0 = M0'" "a = a'"; 

35 
with N r; have "?r K a & N = M0 + K"; by simp; 

36 
hence ?case2; ..; thus ?thesis; ..; 

37 
next; 

38 
fix K'; 

39 
assume "M0' = K' + {#a#}"; 

40 
with N; have n: "N = K' + K + {#a#}"; by (simp add: union_ac); 

41 

42 
assume "M0 = K' + {#a'#}"; 

43 
with r; have "?R (K' + K) M0"; by simp blast; 

44 
with n; have ?case1; by simp; thus ?thesis; ..; 

45 
qed; 

46 
qed; 

47 
qed; 

48 

7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

49 

c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

50 
lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)"; 
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

51 
proof; 
7480  52 
let ?R = "mult1 r"; 
53 
let ?W = "acc ?R"; 

7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

54 

c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

55 

c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

56 
{{; 
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

57 
fix M M0 a; 
7480  58 
assume wf_hyp: "ALL b. (b, a) : r > (ALL M:?W. M + {#b#} : ?W)" 
59 
and M0: "M0 : ?W" 

60 
and acc_hyp: "ALL M. (M, M0) : ?R > M + {#a#} : ?W"; 

61 
have "M0 + {#a#} : ?W"; 

7442  62 
proof (rule accI [of "M0 + {#a#}"]); 
7480  63 
fix N; assume "(N, M0 + {#a#}) : ?R"; 
64 
hence "((EX M. (M, M0) : ?R & N = M + {#a#})  

7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

65 
(EX K. (ALL b. elem K b > (b, a) : r) & N = M0 + K))"; 
7527  66 
by (rule less_add); 
7480  67 
thus "N : ?W"; 
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

68 
proof (elim exE disjE conjE); 
7480  69 
fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}"; 
70 
from acc_hyp; have "(M, M0) : ?R > M + {#a#} : ?W"; ..; 

71 
hence "M + {#a#} : ?W"; ..; 

72 
thus "N : ?W"; by (simp only: N); 

7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

73 
next; 
7451  74 
fix K; 
75 
assume N: "N = M0 + K"; 

76 
assume "ALL b. elem K b > (b, a) : r"; 

7480  77 
have "?this > M0 + K : ?W" (is "?P K"); 
7527  78 
proof (induct K rule: multiset_induct); 
7480  79 
from M0; have "M0 + {#} : ?W"; by simp; 
80 
thus "?P {#}"; ..; 

7442  81 

7480  82 
fix K x; assume hyp: "?P K"; 
83 
show "?P (K + {#x#})"; 

7442  84 
proof; 
7451  85 
assume a: "ALL b. elem (K + {#x#}) b > (b, a) : r"; 
7442  86 
hence "(x, a) : r"; by simp; 
7480  87 
with wf_hyp [RS spec]; have b: "ALL M:?W. M + {#x#} : ?W"; ..; 
7442  88 

7480  89 
from a hyp; have "M0 + K : ?W"; by simp; 
90 
with b; have "(M0 + K) + {#x#} : ?W"; ..; 

91 
thus "M0 + (K + {#x#}) : ?W"; by (simp only: union_assoc); 

7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

92 
qed; 
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

93 
qed; 
7480  94 
hence "M0 + K : ?W"; ..; 
95 
thus "N : ?W"; by (simp only: N); 

7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

96 
qed; 
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

97 
qed; 
7442  98 
}}; note tedious_reasoning = this; 
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

99 

c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

100 

c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

101 
assume wf: "wf r"; 
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

102 
fix M; 
7480  103 
show "M : ?W"; 
7527  104 
proof (induct M rule: multiset_induct); 
7480  105 
show "{#} : ?W"; 
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

106 
proof (rule accI); 
7480  107 
fix b; assume "(b, {#}) : ?R"; 
108 
with not_less_empty; show "b : ?W"; by contradiction; 

7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

109 
qed; 
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

110 

7480  111 
fix M a; assume "M : ?W"; 
112 
from wf; have "ALL M:?W. M + {#a#} : ?W"; 

7442  113 
proof (rule wf_induct [of r]); 
7480  114 
fix a; assume "ALL b. (b, a) : r > (ALL M:?W. M + {#b#} : ?W)"; 
115 
show "ALL M:?W. M + {#a#} : ?W"; 

7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

116 
proof; 
7480  117 
fix M; assume "M : ?W"; 
118 
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

119 
qed; 
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

120 
qed; 
7480  121 
thus "M + {#a#} : ?W"; ..; 
7432
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

122 
qed; 
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 

c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

125 

c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

126 
theorem wf_mult1: "wf r ==> wf (mult1 r)"; 
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

127 
by (rule acc_wfI, rule all_accessible); 
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

128 

c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

129 
theorem wf_mult: "wf r ==> wf (mult r)"; 
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

130 
by (unfold mult_def, rule wf_trancl, rule wf_mult1); 
c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

131 

c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

132 

c32a0fd117a0
Wellfoundedness proof for the multiset order (preliminary version).
wenzelm
parents:
diff
changeset

133 
end; 