--- a/src/HOL/Metis_Examples/Sets.thy Mon Jan 02 15:08:40 2012 +0100
+++ b/src/HOL/Metis_Examples/Sets.thy Mon Jan 02 15:15:46 2012 +0100
@@ -24,50 +24,50 @@
sledgehammer_params [isar_proof, isar_shrink_factor = 1]
(*multiple versions of this example*)
-(* lemma (*equal_union: *)
+lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
proof -
- have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>1 \<union> x\<^isub>2" by (metis Un_commute Un_upper2)
- have F2a: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq)
- have F2: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis F2a subset_Un_eq)
+ have F1: "\<forall>(x\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>1 \<union> x\<^isub>2" by (metis Un_commute Un_upper2)
+ have F2a: "\<forall>(x\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq)
+ have F2: "\<forall>(x\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis F2a subset_Un_eq)
{ assume "\<not> Z \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
moreover
{ assume AA1: "Y \<union> Z \<noteq> X"
{ assume "\<not> Y \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
moreover
{ assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
{ assume "\<not> Z \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
moreover
{ assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff)
hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2)
- hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1)
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
- ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) }
- ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1) }
+ hence "\<exists>x\<^isub>1\<Colon>'a set. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1)
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1) }
moreover
- { assume "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
+ { assume "\<exists>x\<^isub>1\<Colon>'a set. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
{ assume "\<not> Y \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
moreover
{ assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
{ assume "\<not> Z \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
moreover
{ assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff)
hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2)
- hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1)
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
- ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) }
- ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by blast }
+ hence "\<exists>x\<^isub>1\<Colon>'a set. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1)
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by blast }
moreover
{ assume "\<not> Y \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
- ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
+ ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
qed
sledgehammer_params [isar_proof, isar_shrink_factor = 2]
@@ -75,36 +75,36 @@
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
proof -
- have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq)
- { assume AA1: "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
+ have F1: "\<forall>(x\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq)
+ { assume AA1: "\<exists>x\<^isub>1\<Colon>'a set. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
{ assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
{ assume "\<not> Z \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
moreover
{ assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z"
- hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1 Un_commute Un_upper2)
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
- ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1 Un_subset_iff) }
+ hence "\<exists>x\<^isub>1\<Colon>'a set. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1 Un_commute Un_upper2)
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1 Un_subset_iff) }
moreover
{ assume "\<not> Y \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
- ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) }
moreover
{ assume "\<not> Z \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
moreover
{ assume "\<not> Y \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
moreover
{ assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
{ assume "\<not> Z \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
moreover
{ assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z"
- hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1 Un_commute Un_upper2)
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
- ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) }
- ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
+ hence "\<exists>x\<^isub>1\<Colon>'a set. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1 Un_commute Un_upper2)
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) }
+ ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
qed
sledgehammer_params [isar_proof, isar_shrink_factor = 3]
@@ -112,16 +112,16 @@
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
proof -
- have F1a: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq)
- have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis F1a subset_Un_eq)
+ have F1a: "\<forall>(x\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq)
+ have F1: "\<forall>(x\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis F1a subset_Un_eq)
{ assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) }
moreover
- { assume AA1: "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
+ { assume AA1: "\<exists>x\<^isub>1\<Colon>'a set. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
{ assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) }
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) }
- ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) }
+ ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
qed
sledgehammer_params [isar_proof, isar_shrink_factor = 4]
@@ -129,15 +129,15 @@
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
proof -
- have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq)
+ have F1: "\<forall>(x\<^isub>2\<Colon>'b set) x\<^isub>1\<Colon>'b set. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq)
{ assume "\<not> Y \<subseteq> X"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
moreover
{ assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
- { assume "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z"
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
- hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) }
- ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
+ { assume "\<exists>x\<^isub>1\<Colon>'a set. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z"
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+ hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) }
+ ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
qed
sledgehammer_params [isar_proof, isar_shrink_factor = 1]
@@ -172,8 +172,8 @@
assume "\<forall>x \<in> S. \<Union>S \<subseteq> x"
hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> \<Union>S \<and> x\<^isub>1 \<in> S \<longrightarrow> x\<^isub>1 = \<Union>S" by (metis set_eq_subset)
hence "\<forall>x\<^isub>1. x\<^isub>1 \<in> S \<longrightarrow> x\<^isub>1 = \<Union>S" by (metis Union_upper)
- hence "\<forall>x\<^isub>1\<Colon>('a \<Rightarrow> bool) \<Rightarrow> bool. \<Union>S \<in> x\<^isub>1 \<longrightarrow> S \<subseteq> x\<^isub>1" by (metis subsetI)
- hence "\<forall>x\<^isub>1\<Colon>('a \<Rightarrow> bool) \<Rightarrow> bool. S \<subseteq> insert (\<Union>S) x\<^isub>1" by (metis insert_iff)
+ hence "\<forall>x\<^isub>1\<Colon>('a set) set. \<Union>S \<in> x\<^isub>1 \<longrightarrow> S \<subseteq> x\<^isub>1" by (metis subsetI)
+ hence "\<forall>x\<^isub>1\<Colon>('a set) set. S \<subseteq> insert (\<Union>S) x\<^isub>1" by (metis insert_iff)
thus "\<exists>z. S \<subseteq> {z}" by metis
qed
@@ -194,12 +194,11 @@
"(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m"
apply (metis all_not_in_conv)
apply (metis all_not_in_conv)
- apply (metis mem_def)
+ apply (metis mem_Collect_eq)
apply (metis less_int_def singleton_iff)
- apply (metis mem_def)
- apply (metis mem_def)
+ apply (metis mem_Collect_eq)
+ apply (metis mem_Collect_eq)
apply (metis all_not_in_conv)
by (metis pair_in_Id_conv)
-*)
end