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 -