src/HOL/Metis_Examples/Message.thy
 changeset 36911 0e2818493775 parent 36580 d23a3a4d1849 child 39260 f94c53d9b8fb
```--- a/src/HOL/Metis_Examples/Message.thy	Fri May 14 11:24:14 2010 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Fri May 14 11:24:49 2010 +0200
@@ -9,7 +9,7 @@
begin

lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
-by (metis Un_ac(2) Un_ac(3))
+by (metis Un_commute Un_left_absorb)

types
key = nat
@@ -681,14 +681,10 @@

lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
proof -
-  have "\<forall>x\<^isub>2 x\<^isub>1. synth x\<^isub>1 \<union> analz (x\<^isub>1 \<union> x\<^isub>2) = analz (synth x\<^isub>1 \<union> x\<^isub>2)"
-    by (metis Un_commute analz_synth_Un)
-  hence "\<forall>x\<^isub>3 x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1 \<union> UNION {} x\<^isub>3)"
-    by (metis UN_extend_simps(3))
-  hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1)"
-    by (metis UN_extend_simps(3))
-  hence "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth x\<^isub>1 = analz (synth x\<^isub>1)"
-    by (metis Un_commute)
+  have "\<forall>x\<^isub>2 x\<^isub>1. synth x\<^isub>1 \<union> analz (x\<^isub>1 \<union> x\<^isub>2) = analz (synth x\<^isub>1 \<union> x\<^isub>2)" by (metis Un_commute analz_synth_Un)
+  hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1 \<union> {})" by (metis Un_empty_right)
+  hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1)" by (metis Un_empty_right)
+  hence "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth x\<^isub>1 = analz (synth x\<^isub>1)" by (metis Un_commute)
thus "analz (synth H) = analz H \<union> synth H" by metis
qed

@@ -698,20 +694,18 @@
lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
proof -
assume "X \<in> G"
-  hence "\<forall>u. X \<in> G \<union> u" by (metis Un_iff)
-  hence "X \<in> G \<union> H \<and> H \<subseteq> G \<union> H"
-    by (metis Un_upper2)
-  hence "insert X H \<subseteq> G \<union> H" by (metis insert_subset)
-  hence "parts (insert X H) \<subseteq> parts (G \<union> H)"
-    by (metis parts_mono)
-  thus "parts (insert X H) \<subseteq> parts G \<union> parts H"
-    by (metis parts_Un)
+  hence "G X" by (metis mem_def)
+  hence "\<forall>x\<^isub>1. G \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 X" by (metis predicate1D)
+  hence "\<forall>x\<^isub>1. (G \<union> x\<^isub>1) X" by (metis Un_upper1)
+  hence "\<forall>x\<^isub>1. X \<in> G \<union> x\<^isub>1" by (metis mem_def)
+  hence "insert X H \<subseteq> G \<union> H" by (metis Un_upper2 insert_subset)
+  hence "parts (insert X H) \<subseteq> parts (G \<union> H)" by (metis parts_mono)
+  thus "parts (insert X H) \<subseteq> parts G \<union> parts H" by (metis parts_Un)
qed

lemma Fake_parts_insert:
"X \<in> synth (analz H) ==>
parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
-(*sledgehammer*)
proof -
assume A1: "X \<in> synth (analz H)"
have F1: "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth (analz x\<^isub>1) = analz (synth (analz x\<^isub>1))"```