src/HOL/MetisExamples/set.thy
 changeset 28486 873726bdfd47 parent 26806 40b411ec05aa child 28592 824f8390aaa2
```     1.1 --- a/src/HOL/MetisExamples/set.thy	Fri Oct 03 19:35:18 2008 +0200
1.2 +++ b/src/HOL/MetisExamples/set.thy	Fri Oct 03 20:10:43 2008 +0200
1.3 @@ -20,9 +20,9 @@
1.4  lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
1.5  by metis
1.6
1.7 -declare [[sledgehammer_full = true]]
1.8  declare [[sledgehammer_modulus = 1]]
1.9
1.10 +
1.11  (*multiple versions of this example*)
1.12  lemma (*equal_union: *)
1.13     "(X = Y \<union> Z) =
1.14 @@ -198,7 +198,7 @@
1.15    by (metis 11 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
1.16  qed
1.17
1.18 -ML {*ResAtp.problem_name := "set__equal_union"*}
1.19 +ML {*AtpThread.problem_name := "set__equal_union"*}
1.20  lemma (*equal_union: *)
1.21     "(X = Y \<union> Z) =
1.22      (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
1.23 @@ -206,12 +206,12 @@
1.24  by (metis Un_least Un_upper1 Un_upper2 set_eq_subset)
1.25
1.26
1.27 -ML {*ResAtp.problem_name := "set__equal_inter"*}
1.28 +ML {*AtpThread.problem_name := "set__equal_inter"*}
1.29  lemma "(X = Y \<inter> Z) =
1.30      (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
1.31  by (metis Int_greatest Int_lower1 Int_lower2 set_eq_subset)
1.32
1.33 -ML {*ResAtp.problem_name := "set__fixedpoint"*}
1.34 +ML {*AtpThread.problem_name := "set__fixedpoint"*}
1.35  lemma fixedpoint:
1.36      "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
1.37  by metis
1.38 @@ -230,7 +230,7 @@
1.39    by (metis 4 0)
1.40  qed
1.41
1.42 -ML {*ResAtp.problem_name := "set__singleton_example"*}
1.43 +ML {*AtpThread.problem_name := "set__singleton_example"*}
1.44  lemma (*singleton_example_2:*)
1.45       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
1.46  by (metis Set.subsetI Union_upper insertCI set_eq_subset)
1.47 @@ -260,7 +260,7 @@
1.48    293-314.
1.49  *}
1.50
1.51 -ML {*ResAtp.problem_name := "set__Bledsoe_Fung"*}
1.52 +ML {*AtpThread.problem_name := "set__Bledsoe_Fung"*}
1.53  (*Notes: 1, the numbering doesn't completely agree with the paper.
1.54  2, we must rename set variables to avoid type clashes.*)
1.55  lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))"
1.56 @@ -282,4 +282,3 @@
1.57  done
1.58
1.59  end
1.60 -
```