|
1 theory Max |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 section {* Some generic facts about Max *} |
|
6 |
|
7 |
|
8 lemma Max_insert: |
|
9 assumes "finite B" |
|
10 and "B \<noteq> {}" |
|
11 shows "Max ({x} \<union> B) = max x (Max B)" |
|
12 using assms by (simp add: Lattices_Big.Max.insert) |
|
13 |
|
14 lemma Max_Union: |
|
15 assumes fc: "finite C" |
|
16 and ne: "C \<noteq> {}" |
|
17 and fa: "\<And> A. A \<in> C \<Longrightarrow> finite A \<and> A \<noteq> {}" |
|
18 shows "Max (\<Union>C) = Max (Max ` C)" |
|
19 using assms |
|
20 proof(induct rule: finite_induct) |
|
21 case (insert x F) |
|
22 assume ih: "\<lbrakk>F \<noteq> {}; \<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}\<rbrakk> \<Longrightarrow> Max (\<Union>F) = Max (Max ` F)" |
|
23 and h: "\<And> A. A \<in> insert x F \<Longrightarrow> finite A \<and> A \<noteq> {}" |
|
24 show ?case (is "?L = ?R") |
|
25 proof(cases "F = {}") |
|
26 case False |
|
27 from Union_insert have "?L = Max (x \<union> (\<Union> F))" by simp |
|
28 also have "\<dots> = max (Max x) (Max(\<Union> F))" |
|
29 proof(rule Max_Un) |
|
30 from h[of x] show "finite x" by auto |
|
31 next |
|
32 from h[of x] show "x \<noteq> {}" by auto |
|
33 next |
|
34 show "finite (\<Union>F)" |
|
35 by (metis (full_types) finite_Union h insert.hyps(1) insertCI) |
|
36 next |
|
37 from False and h show "\<Union>F \<noteq> {}" by auto |
|
38 qed |
|
39 also have "\<dots> = ?R" |
|
40 proof - |
|
41 have "?R = Max (Max ` ({x} \<union> F))" by simp |
|
42 also have "\<dots> = Max ({Max x} \<union> (Max ` F))" by simp |
|
43 also have "\<dots> = max (Max x) (Max (\<Union>F))" |
|
44 proof - |
|
45 have "Max ({Max x} \<union> Max ` F) = max (Max {Max x}) (Max (Max ` F))" |
|
46 proof(rule Max_Un) |
|
47 show "finite {Max x}" by simp |
|
48 next |
|
49 show "{Max x} \<noteq> {}" by simp |
|
50 next |
|
51 from insert show "finite (Max ` F)" by auto |
|
52 next |
|
53 from False show "Max ` F \<noteq> {}" by auto |
|
54 qed |
|
55 moreover have "Max {Max x} = Max x" by simp |
|
56 moreover have "Max (\<Union>F) = Max (Max ` F)" |
|
57 proof(rule ih) |
|
58 show "F \<noteq> {}" by fact |
|
59 next |
|
60 from h show "\<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}" |
|
61 by auto |
|
62 qed |
|
63 ultimately show ?thesis by auto |
|
64 qed |
|
65 finally show ?thesis by simp |
|
66 qed |
|
67 finally show ?thesis by simp |
|
68 next |
|
69 case True |
|
70 thus ?thesis by auto |
|
71 qed |
|
72 next |
|
73 case empty |
|
74 assume "{} \<noteq> {}" show ?case by auto |
|
75 qed |
|
76 |
|
77 |
|
78 end |