tuned Metis examples

--- a/src/HOL/IsaMakefile	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/IsaMakefile	Mon Jun 06 20:36:35 2011 +0200
@@ -706,11 +706,11 @@
 HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
 
 $(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
-  Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
-  Metis_Examples/BT.thy Metis_Examples/Clausify.thy \
-  Metis_Examples/HO_Reas.thy Metis_Examples/Message.thy \
-  Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \
-  Metis_Examples/Typings.thy Metis_Examples/set.thy
+  Metis_Examples/Abstraction.thy Metis_Examples/Big_O.thy \
+  Metis_Examples/Binary_Tree.thy Metis_Examples/Clausification.thy \
+  Metis_Examples/Message.thy Metis_Examples/Proxies.thy \
+  Metis_Examples/Sets.thy Metis_Examples/Tarski.thy \
+  Metis_Examples/Trans_Closure.thy Metis_Examples/Type_Encodings.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
 
 

--- a/src/HOL/Metis_Examples/Abstraction.thy	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -1,10 +1,12 @@
 (*  Title:      HOL/Metis_Examples/Abstraction.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
-Testing Metis.
+Example featuring Metis's support for lambda-abstractions.
 *)
 
+header {* Example Featuring Metis's Support for Lambda-Abstractions *}
+
 theory Abstraction
 imports Main "~~/src/HOL/Library/FuncSet"
 begin
@@ -93,7 +95,7 @@
 
 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Pi" ]]
 lemma
-    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
+    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
     f \<in> pset cl \<rightarrow> pset cl"
 proof -
   assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
@@ -125,38 +127,38 @@
 by auto
 
 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_subset_Collect_Int" ]]
-lemma "(cl,f) \<in> CLF ==> 
+lemma "(cl,f) \<in> CLF ==>
    CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
    f \<in> pset cl \<inter> cl"
 by auto
 
 
 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]]
-lemma "(cl,f) \<in> CLF ==> 
+lemma "(cl,f) \<in> CLF ==>
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
    f \<in> pset cl \<inter> cl"
 by auto
 
 
 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]]
-lemma 
-   "(cl,f) \<in> CLF ==> 
-    CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> 
+lemma
+   "(cl,f) \<in> CLF ==>
+    CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==>
     f \<in> pset cl \<rightarrow> pset cl"
 by fast
 
 
 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]]
-lemma 
-  "(cl,f) \<in> CLF ==> 
-   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
+lemma
+  "(cl,f) \<in> CLF ==>
+   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
    f \<in> pset cl \<rightarrow> pset cl"
 by auto
 
 
 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]]
-lemma 
-  "(cl,f) \<in> CLF ==> 
+lemma
+  "(cl,f) \<in> CLF ==>
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
    (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
 by auto
@@ -168,7 +170,7 @@
 by auto
 
 declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipB" ]]
-lemma "map (%w. (w -> w, w \<times> w)) xs = 
+lemma "map (%w. (w -> w, w \<times> w)) xs =
        zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
 apply (induct xs)
  apply (metis Nil_is_map_conv zip_Nil)
@@ -179,12 +181,12 @@
 by (metis Collect_def image_subset_iff mem_def)
 
 declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenB" ]]
-lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A 
+lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A
        ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
 by (metis Collect_def imageI image_image image_subset_iff mem_def)
 
 declare [[ sledgehammer_problem_prefix = "Abstraction__image_curry" ]]
-lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" 
+lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)"
 (*sledgehammer*)
 by auto
 
@@ -203,13 +205,13 @@
 (*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*)
 apply (erule ssubst)
 apply (subst split_conv)
-apply (rule SigmaI) 
+apply (rule SigmaI)
 apply (erule imageI) +
 txt{*subgoal 2*}
 apply (clarify );
-apply (simp add: );  
-apply (rule rev_image_eqI)  
-apply (blast intro: elim:); 
+apply (simp add: );
+apply (rule rev_image_eqI)
+apply (blast intro: elim:);
 apply (simp add: );
 done
 
@@ -224,8 +226,8 @@
 
 declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesC" ]]
 lemma image_TimesC:
-    "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = 
-     ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" 
+    "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =
+     ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)"
 (*sledgehammer*)
 by auto
 

--- a/src/HOL/Metis_Examples/BT.thy	Mon Jun 06 20:36:35 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,278 +0,0 @@
-(*  Title:      HOL/Metis_Examples/BT.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Testing Metis.
-*)
-
-header {* Binary trees *}
-
-theory BT
-imports Main
-begin
-
-declare [[metis_new_skolemizer]]
-
-datatype 'a bt =
-    Lf
-  | Br 'a  "'a bt"  "'a bt"
-
-primrec n_nodes :: "'a bt => nat" where
-  "n_nodes Lf = 0"
-| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
-
-primrec n_leaves :: "'a bt => nat" where
-  "n_leaves Lf = Suc 0"
-| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
-
-primrec depth :: "'a bt => nat" where
-  "depth Lf = 0"
-| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
-
-primrec reflect :: "'a bt => 'a bt" where
-  "reflect Lf = Lf"
-| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
-
-primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
-  "bt_map f Lf = Lf"
-| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
-
-primrec preorder :: "'a bt => 'a list" where
-  "preorder Lf = []"
-| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
-
-primrec inorder :: "'a bt => 'a list" where
-  "inorder Lf = []"
-| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
-
-primrec postorder :: "'a bt => 'a list" where
-  "postorder Lf = []"
-| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
-
-primrec append :: "'a bt => 'a bt => 'a bt" where
-  "append Lf t = t"
-| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
-
-text {* \medskip BT simplification *}
-
-declare [[ sledgehammer_problem_prefix = "BT__n_leaves_reflect" ]]
-
-lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
-proof (induct t)
-  case Lf thus ?case
-  proof -
-    let "?p\<^isub>1 x\<^isub>1" = "x\<^isub>1 \<noteq> n_leaves (reflect (Lf::'a bt))"
-    have "\<not> ?p\<^isub>1 (Suc 0)" by (metis reflect.simps(1) n_leaves.simps(1))
-    hence "\<not> ?p\<^isub>1 (n_leaves (Lf::'a bt))" by (metis n_leaves.simps(1))
-    thus "n_leaves (reflect (Lf::'a bt)) = n_leaves (Lf::'a bt)" by metis
-  qed
-next
-  case (Br a t1 t2) thus ?case
-    by (metis n_leaves.simps(2) nat_add_commute reflect.simps(2))
-qed
-
-declare [[ sledgehammer_problem_prefix = "BT__n_nodes_reflect" ]]
-
-lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
-proof (induct t)
-  case Lf thus ?case by (metis reflect.simps(1))
-next
-  case (Br a t1 t2) thus ?case
-    by (metis add_commute n_nodes.simps(2) reflect.simps(2))
-qed
-
-declare [[ sledgehammer_problem_prefix = "BT__depth_reflect" ]]
-
-lemma depth_reflect: "depth (reflect t) = depth t"
-apply (induct t)
- apply (metis depth.simps(1) reflect.simps(1))
-by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2))
-
-text {*
-The famous relationship between the numbers of leaves and nodes.
-*}
-
-declare [[ sledgehammer_problem_prefix = "BT__n_leaves_nodes" ]]
-
-lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
-apply (induct t)
- apply (metis n_leaves.simps(1) n_nodes.simps(1))
-by auto
-
-declare [[ sledgehammer_problem_prefix = "BT__reflect_reflect_ident" ]]
-
-lemma reflect_reflect_ident: "reflect (reflect t) = t"
-apply (induct t)
- apply (metis reflect.simps(1))
-proof -
-  fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt"
-  assume A1: "reflect (reflect t1) = t1"
-  assume A2: "reflect (reflect t2) = t2"
-  have "\<And>V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)"
-    using A1 by (metis reflect.simps(2))
-  hence "\<And>V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))"
-    by (metis reflect.simps(2))
-  hence "\<And>U. reflect (reflect (Br U t1 t2)) = Br U t1 t2"
-    using A2 by metis
-  thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast
-qed
-
-declare [[ sledgehammer_problem_prefix = "BT__bt_map_ident" ]]
-
-lemma bt_map_ident: "bt_map (%x. x) = (%y. y)"
-apply (rule ext) 
-apply (induct_tac y)
- apply (metis bt_map.simps(1))
-by (metis bt_map.simps(2))
-
-declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
-
-lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)"
-apply (induct t)
- apply (metis append.simps(1) bt_map.simps(1))
-by (metis append.simps(2) bt_map.simps(2))
-
-declare [[ sledgehammer_problem_prefix = "BT__bt_map_compose" ]]
-
-lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)"
-apply (induct t)
- apply (metis bt_map.simps(1))
-by (metis bt_map.simps(2) o_eq_dest_lhs)
-
-declare [[ sledgehammer_problem_prefix = "BT__bt_map_reflect" ]]
-
-lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
-apply (induct t)
- apply (metis bt_map.simps(1) reflect.simps(1))
-by (metis bt_map.simps(2) reflect.simps(2))
-
-declare [[ sledgehammer_problem_prefix = "BT__preorder_bt_map" ]]
-
-lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
-apply (induct t)
- apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
-by simp
-
-declare [[ sledgehammer_problem_prefix = "BT__inorder_bt_map" ]]
-
-lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
-proof (induct t)
-  case Lf thus ?case
-  proof -
-    have "map f [] = []" by (metis map.simps(1))
-    hence "map f [] = inorder Lf" by (metis inorder.simps(1))
-    hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1))
-    thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1))
-  qed
-next
-  case (Br a t1 t2) thus ?case by simp
-qed
-
-declare [[ sledgehammer_problem_prefix = "BT__postorder_bt_map" ]]
-
-lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
-apply (induct t)
- apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1))
-by simp
-
-declare [[ sledgehammer_problem_prefix = "BT__depth_bt_map" ]]
-
-lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
-apply (induct t)
- apply (metis bt_map.simps(1) depth.simps(1))
-by simp
-
-declare [[ sledgehammer_problem_prefix = "BT__n_leaves_bt_map" ]]
-
-lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
-apply (induct t)
- apply (metis bt_map.simps(1) n_leaves.simps(1))
-proof -
-  fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt"
-  assume A1: "n_leaves (bt_map f t1) = n_leaves t1"
-  assume A2: "n_leaves (bt_map f t2) = n_leaves t2"
-  have "\<And>V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V"
-    using A1 by (metis n_leaves.simps(2))
-  hence "\<And>V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)"
-    by (metis bt_map.simps(2))
-  hence F1: "\<And>U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2"
-    using A2 by metis
-  have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)"
-    by (metis n_leaves.simps(2))
-  thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)"
-    using F1 by metis
-qed
-
-declare [[ sledgehammer_problem_prefix = "BT__preorder_reflect" ]]
-
-lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
-apply (induct t)
- apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
-              reflect.simps(1))
-apply simp
-done
-
-declare [[ sledgehammer_problem_prefix = "BT__inorder_reflect" ]]
-
-lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
-apply (induct t)
- apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1))
-by simp
-(* Slow:
-by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2)
-          reflect.simps(2) rev.simps(2) rev_append)
-*)
-
-declare [[ sledgehammer_problem_prefix = "BT__postorder_reflect" ]]
-
-lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
-apply (induct t)
- apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
-              reflect.simps(1))
-by (metis preorder_reflect reflect_reflect_ident rev_swap)
-
-text {*
-Analogues of the standard properties of the append function for lists.
-*}
-
-declare [[ sledgehammer_problem_prefix = "BT__append_assoc" ]]
-
-lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)"
-apply (induct t1)
- apply (metis append.simps(1))
-by (metis append.simps(2))
-
-declare [[ sledgehammer_problem_prefix = "BT__append_Lf2" ]]
-
-lemma append_Lf2 [simp]: "append t Lf = t"
-apply (induct t)
- apply (metis append.simps(1))
-by (metis append.simps(2))
-
-declare max_add_distrib_left [simp]
-
-declare [[ sledgehammer_problem_prefix = "BT__depth_append" ]]
-
-lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
-apply (induct t1)
- apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1))
-by simp
-
-declare [[ sledgehammer_problem_prefix = "BT__n_leaves_append" ]]
-
-lemma n_leaves_append [simp]:
-     "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
-apply (induct t1)
- apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
-              semiring_norm(111))
-by (simp add: left_distrib)
-
-declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
-
-lemma (*bt_map_append:*)
-     "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
-apply (induct t1)
- apply (metis append.simps(1) bt_map.simps(1))
-by (metis bt_map_append)
-
-end

--- a/src/HOL/Metis_Examples/BigO.thy	Mon Jun 06 20:36:35 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,966 +0,0 @@
-(*  Title:      HOL/Metis_Examples/BigO.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Testing Metis.
-*)
-
-header {* Big O notation *}
-
-theory BigO
-imports
-  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
-  Main
-  "~~/src/HOL/Library/Function_Algebras"
-  "~~/src/HOL/Library/Set_Algebras"
-begin
-
-declare [[metis_new_skolemizer]]
-
-subsection {* Definitions *}
-
-definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set"    ("(1O'(_'))") where
-  "O(f::('a => 'b)) ==   {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_pos_const" ]]
-lemma bigo_pos_const: "(EX (c::'a::linordered_idom). 
-    ALL x. (abs (h x)) <= (c * (abs (f x))))
-      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
-  apply auto
-  apply (case_tac "c = 0", simp)
-  apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto)
-  apply (metis abs_ge_zero abs_of_nonneg Orderings.xt1(6) abs_mult)
-  done
-
-(*** Now various verions with an increasing shrink factor ***)
-
-sledgehammer_params [isar_proof, isar_shrink_factor = 1]
-
-lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
-    ALL x. (abs (h x)) <= (c * (abs (f x))))
-      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
-  apply auto
-  apply (case_tac "c = 0", simp)
-  apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto)
-proof -
-  fix c :: 'a and x :: 'b
-  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
-  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
-  have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
-  have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
-  have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
-    by (metis abs_mult)
-  have F5: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1"
-    by (metis abs_mult_pos)
-  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = \<bar>1\<bar> * x\<^isub>1" by (metis F2)
-  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F2 abs_one)
-  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>h x\<^isub>3\<bar> \<longrightarrow> \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F3)
-  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F1)
-  hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F5)
-  hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F4)
-  hence "\<forall>x\<^isub>3. c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F1)
-  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1)
-  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
-qed
-
-sledgehammer_params [isar_proof, isar_shrink_factor = 2]
-
-lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
-    ALL x. (abs (h x)) <= (c * (abs (f x))))
-      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
-  apply auto
-  apply (case_tac "c = 0", simp)
-  apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto)
-proof -
-  fix c :: 'a and x :: 'b
-  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
-  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
-  have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
-    by (metis abs_mult)
-  have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
-  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis A1 abs_ge_zero order_trans)
-  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F2 abs_mult_pos)
-  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero)
-  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
-qed
-
-sledgehammer_params [isar_proof, isar_shrink_factor = 3]
-
-lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
-    ALL x. (abs (h x)) <= (c * (abs (f x))))
-      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
-  apply auto
-  apply (case_tac "c = 0", simp)
-  apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto)
-proof -
-  fix c :: 'a and x :: 'b
-  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
-  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
-  have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
-  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
-  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
-  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_mult abs_ge_zero)
-qed
-
-sledgehammer_params [isar_proof, isar_shrink_factor = 4]
-
-lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
-    ALL x. (abs (h x)) <= (c * (abs (f x))))
-      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
-  apply auto
-  apply (case_tac "c = 0", simp)
-  apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto)
-proof -
-  fix c :: 'a and x :: 'b
-  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
-  have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
-  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
-    by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
-  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult)
-  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
-qed
-
-sledgehammer_params [isar_proof, isar_shrink_factor = 1]
-
-lemma bigo_alt_def: "O(f) = 
-    {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
-by (auto simp add: bigo_def bigo_pos_const)
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_elt_subset" ]]
-lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
-  apply (auto simp add: bigo_alt_def)
-  apply (rule_tac x = "ca * c" in exI)
-  apply (rule conjI)
-  apply (rule mult_pos_pos)
-  apply (assumption)+ 
-(*sledgehammer*)
-  apply (rule allI)
-  apply (drule_tac x = "xa" in spec)+
-  apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")
-  apply (erule order_trans)
-  apply (simp add: mult_ac)
-  apply (rule mult_left_mono, assumption)
-  apply (rule order_less_imp_le, assumption)
-done
-
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_refl" ]]
-lemma bigo_refl [intro]: "f : O(f)"
-apply (auto simp add: bigo_def)
-by (metis mult_1 order_refl)
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_zero" ]]
-lemma bigo_zero: "0 : O(g)"
-apply (auto simp add: bigo_def func_zero)
-by (metis mult_zero_left order_refl)
-
-lemma bigo_zero2: "O(%x.0) = {%x.0}"
-  by (auto simp add: bigo_def) 
-
-lemma bigo_plus_self_subset [intro]: 
-  "O(f) \<oplus> O(f) <= O(f)"
-  apply (auto simp add: bigo_alt_def set_plus_def)
-  apply (rule_tac x = "c + ca" in exI)
-  apply auto
-  apply (simp add: ring_distribs func_plus)
-  apply (blast intro:order_trans abs_triangle_ineq add_mono elim:) 
-done
-
-lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)"
-  apply (rule equalityI)
-  apply (rule bigo_plus_self_subset)
-  apply (rule set_zero_plus2) 
-  apply (rule bigo_zero)
-done
-
-lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)"
-  apply (rule subsetI)
-  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
-  apply (subst bigo_pos_const [symmetric])+
-  apply (rule_tac x = 
-    "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
-  apply (rule conjI)
-  apply (rule_tac x = "c + c" in exI)
-  apply (clarsimp)
-  apply (auto)
-  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
-  apply (erule_tac x = xa in allE)
-  apply (erule order_trans)
-  apply (simp)
-  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
-  apply (erule order_trans)
-  apply (simp add: ring_distribs)
-  apply (rule mult_left_mono)
-  apply assumption
-  apply (simp add: order_less_le)
-  apply (rule mult_left_mono)
-  apply (simp add: abs_triangle_ineq)
-  apply (simp add: order_less_le)
-  apply (rule mult_nonneg_nonneg)
-  apply (rule add_nonneg_nonneg)
-  apply auto
-  apply (rule_tac x = "%n. if (abs (f n)) <  abs (g n) then x n else 0" 
-     in exI)
-  apply (rule conjI)
-  apply (rule_tac x = "c + c" in exI)
-  apply auto
-  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
-  apply (erule_tac x = xa in allE)
-  apply (erule order_trans)
-  apply (simp)
-  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
-  apply (erule order_trans)
-  apply (simp add: ring_distribs)
-  apply (rule mult_left_mono)
-  apply (simp add: order_less_le)
-  apply (simp add: order_less_le)
-  apply (rule mult_left_mono)
-  apply (rule abs_triangle_ineq)
-  apply (simp add: order_less_le)
-apply (metis abs_not_less_zero double_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)
-  apply (rule ext)
-  apply (auto simp add: if_splits linorder_not_le)
-done
-
-lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"
-  apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)")
-  apply (erule order_trans)
-  apply simp
-  apply (auto del: subsetI simp del: bigo_plus_idemp)
-done
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq" ]]
-lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
-  O(f + g) = O(f) \<oplus> O(g)"
-  apply (rule equalityI)
-  apply (rule bigo_plus_subset)
-  apply (simp add: bigo_alt_def set_plus_def func_plus)
-  apply clarify 
-(*sledgehammer*) 
-  apply (rule_tac x = "max c ca" in exI)
-  apply (rule conjI)
-   apply (metis Orderings.less_max_iff_disj)
-  apply clarify
-  apply (drule_tac x = "xa" in spec)+
-  apply (subgoal_tac "0 <= f xa + g xa")
-  apply (simp add: ring_distribs)
-  apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
-  apply (subgoal_tac "abs(a xa) + abs(b xa) <= 
-      max c ca * f xa + max c ca * g xa")
-  apply (blast intro: order_trans)
-  defer 1
-  apply (rule abs_triangle_ineq)
-  apply (metis add_nonneg_nonneg)
-  apply (rule add_mono)
-using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]]
-  apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
-  apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
-done
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt" ]]
-lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
-    f : O(g)" 
-  apply (auto simp add: bigo_def)
-(* Version 1: one-line proof *)
-  apply (metis abs_le_D1 linorder_class.not_less  order_less_le  Orderings.xt1(12)  abs_mult)
-  done
-
-lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
-    f : O(g)"
-apply (auto simp add: bigo_def)
-(* Version 2: structured proof *)
-proof -
-  assume "\<forall>x. f x \<le> c * g x"
-  thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
-qed
-
-text{*So here is the easier (and more natural) problem using transitivity*}
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
-lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
-apply (auto simp add: bigo_def)
-(* Version 1: one-line proof *)
-by (metis abs_ge_self abs_mult order_trans)
-
-text{*So here is the easier (and more natural) problem using transitivity*}
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
-lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
-  apply (auto simp add: bigo_def)
-(* Version 2: structured proof *)
-proof -
-  assume "\<forall>x. f x \<le> c * g x"
-  thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
-qed
-
-lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> 
-    f : O(g)" 
-  apply (erule bigo_bounded_alt [of f 1 g])
-  apply simp
-done
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded2" ]]
-lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
-    f : lb +o O(g)"
-apply (rule set_minus_imp_plus)
-apply (rule bigo_bounded)
- apply (auto simp add: diff_minus fun_Compl_def func_plus)
- prefer 2
- apply (drule_tac x = x in spec)+
- apply (metis add_right_mono add_commute diff_add_cancel diff_minus_eq_add le_less order_trans)
-proof -
-  fix x :: 'a
-  assume "\<forall>x. lb x \<le> f x"
-  thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le)
-qed
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs" ]]
-lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
-apply (unfold bigo_def)
-apply auto
-by (metis mult_1 order_refl)
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs2" ]]
-lemma bigo_abs2: "f =o O(%x. abs(f x))"
-apply (unfold bigo_def)
-apply auto
-by (metis mult_1 order_refl)
- 
-lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
-proof -
-  have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset)
-  have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs)
-  have "\<forall>u. u \<in> O(\<lambda>R. \<bar>u R\<bar>)" by (metis bigo_abs2)
-  thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto
-qed 
-
-lemma bigo_abs4: "f =o g +o O(h) ==> 
-    (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
-  apply (drule set_plus_imp_minus)
-  apply (rule set_minus_imp_plus)
-  apply (subst fun_diff_def)
-proof -
-  assume a: "f - g : O(h)"
-  have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
-    by (rule bigo_abs2)
-  also have "... <= O(%x. abs (f x - g x))"
-    apply (rule bigo_elt_subset)
-    apply (rule bigo_bounded)
-    apply force
-    apply (rule allI)
-    apply (rule abs_triangle_ineq3)
-    done
-  also have "... <= O(f - g)"
-    apply (rule bigo_elt_subset)
-    apply (subst fun_diff_def)
-    apply (rule bigo_abs)
-    done
-  also have "... <= O(h)"
-    using a by (rule bigo_elt_subset)
-  finally show "(%x. abs (f x) - abs (g x)) : O(h)".
-qed
-
-lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" 
-by (unfold bigo_def, auto)
-
-lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)"
-proof -
-  assume "f : g +o O(h)"
-  also have "... <= O(g) \<oplus> O(h)"
-    by (auto del: subsetI)
-  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
-    apply (subst bigo_abs3 [symmetric])+
-    apply (rule refl)
-    done
-  also have "... = O((%x. abs(g x)) + (%x. abs(h x)))"
-    by (rule bigo_plus_eq [symmetric], auto)
-  finally have "f : ...".
-  then have "O(f) <= ..."
-    by (elim bigo_elt_subset)
-  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
-    by (rule bigo_plus_eq, auto)
-  finally show ?thesis
-    by (simp add: bigo_abs3 [symmetric])
-qed
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult" ]]
-lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
-  apply (rule subsetI)
-  apply (subst bigo_def)
-  apply (auto simp del: abs_mult mult_ac
-              simp add: bigo_alt_def set_times_def func_times)
-(*sledgehammer*)
-  apply (rule_tac x = "c * ca" in exI)
-  apply(rule allI)
-  apply(erule_tac x = x in allE)+
-  apply(subgoal_tac "c * ca * abs(f x * g x) = 
-      (c * abs(f x)) * (ca * abs(g x))")
-using [[ sledgehammer_problem_prefix = "BigO__bigo_mult_simpler" ]]
-prefer 2 
-apply (metis mult_assoc mult_left_commute
-  abs_of_pos mult_left_commute
-  abs_mult mult_pos_pos)
-  apply (erule ssubst) 
-  apply (subst abs_mult)
-(* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since
-   abs_mult has just been done *)
-by (metis abs_ge_zero mult_mono')
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult2" ]]
-lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
-  apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
-(*sledgehammer*)
-  apply (rule_tac x = c in exI)
-  apply clarify
-  apply (drule_tac x = x in spec)
-using [[ sledgehammer_problem_prefix = "BigO__bigo_mult2_simpler" ]]
-(*sledgehammer [no luck]*)
-  apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
-  apply (simp add: mult_ac)
-  apply (rule mult_left_mono, assumption)
-  apply (rule abs_ge_zero)
-done
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult3" ]]
-lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
-by (metis bigo_mult set_rev_mp set_times_intro)
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult4" ]]
-lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
-by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib)
-
-
-lemma bigo_mult5: "ALL x. f x ~= 0 ==>
-    O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
-proof -
-  assume a: "ALL x. f x ~= 0"
-  show "O(f * g) <= f *o O(g)"
-  proof
-    fix h
-    assume h: "h : O(f * g)"
-    then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
-      by auto
-    also have "... <= O((%x. 1 / f x) * (f * g))"
-      by (rule bigo_mult2)
-    also have "(%x. 1 / f x) * (f * g) = g"
-      apply (simp add: func_times) 
-      apply (rule ext)
-      apply (simp add: a h nonzero_divide_eq_eq mult_ac)
-      done
-    finally have "(%x. (1::'b) / f x) * h : O(g)".
-    then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
-      by auto
-    also have "f * ((%x. (1::'b) / f x) * h) = h"
-      apply (simp add: func_times) 
-      apply (rule ext)
-      apply (simp add: a h nonzero_divide_eq_eq mult_ac)
-      done
-    finally show "h : f *o O(g)".
-  qed
-qed
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult6" ]]
-lemma bigo_mult6: "ALL x. f x ~= 0 ==>
-    O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)"
-by (metis bigo_mult2 bigo_mult5 order_antisym)
-
-(*proof requires relaxing relevance: 2007-01-25*)
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult7" ]]
-  declare bigo_mult6 [simp]
-lemma bigo_mult7: "ALL x. f x ~= 0 ==>
-    O(f * g) <= O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
-(*sledgehammer*)
-  apply (subst bigo_mult6)
-  apply assumption
-  apply (rule set_times_mono3) 
-  apply (rule bigo_refl)
-done
-  declare bigo_mult6 [simp del]
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult8" ]]
-  declare bigo_mult7[intro!]
-lemma bigo_mult8: "ALL x. f x ~= 0 ==>
-    O(f * g) = O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
-by (metis bigo_mult bigo_mult7 order_antisym_conv)
-
-lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
-  by (auto simp add: bigo_def fun_Compl_def)
-
-lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
-  apply (rule set_minus_imp_plus)
-  apply (drule set_plus_imp_minus)
-  apply (drule bigo_minus)
-  apply (simp add: diff_minus)
-done
-
-lemma bigo_minus3: "O(-f) = O(f)"
-  by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
-
-lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
-proof -
-  assume a: "f : O(g)"
-  show "f +o O(g) <= O(g)"
-  proof -
-    have "f : O(f)" by auto
-    then have "f +o O(g) <= O(f) \<oplus> O(g)"
-      by (auto del: subsetI)
-    also have "... <= O(g) \<oplus> O(g)"
-    proof -
-      from a have "O(f) <= O(g)" by (auto del: subsetI)
-      thus ?thesis by (auto del: subsetI)
-    qed
-    also have "... <= O(g)" by (simp add: bigo_plus_idemp)
-    finally show ?thesis .
-  qed
-qed
-
-lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)"
-proof -
-  assume a: "f : O(g)"
-  show "O(g) <= f +o O(g)"
-  proof -
-    from a have "-f : O(g)" by auto
-    then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1)
-    then have "f +o (-f +o O(g)) <= f +o O(g)" by auto
-    also have "f +o (-f +o O(g)) = O(g)"
-      by (simp add: set_plus_rearranges)
-    finally show ?thesis .
-  qed
-qed
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_absorb" ]]
-lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)"
-by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff)
-
-lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"
-  apply (subgoal_tac "f +o A <= f +o O(g)")
-  apply force+
-done
-
-lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"
-  apply (subst set_minus_plus [symmetric])
-  apply (subgoal_tac "g - f = - (f - g)")
-  apply (erule ssubst)
-  apply (rule bigo_minus)
-  apply (subst set_minus_plus)
-  apply assumption
-  apply  (simp add: diff_minus add_ac)
-done
-
-lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
-  apply (rule iffI)
-  apply (erule bigo_add_commute_imp)+
-done
-
-lemma bigo_const1: "(%x. c) : O(%x. 1)"
-by (auto simp add: bigo_def mult_ac)
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_const2" ]]
-lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)"
-by (metis bigo_const1 bigo_elt_subset)
-
-lemma bigo_const2 [intro]: "O(%x. c::'b::linordered_idom) <= O(%x. 1)"
-(* "thus" had to be replaced by "show" with an explicit reference to "F1" *)
-proof -
-  have F1: "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1)
-  show "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis F1 bigo_elt_subset)
-qed
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_const3" ]]
-lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
-apply (simp add: bigo_def)
-by (metis abs_eq_0 left_inverse order_refl)
-
-lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
-by (rule bigo_elt_subset, rule bigo_const3, assumption)
-
-lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==> 
-    O(%x. c) = O(%x. 1)"
-by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult1" ]]
-lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
-  apply (simp add: bigo_def abs_mult)
-by (metis le_less)
-
-lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
-by (rule bigo_elt_subset, rule bigo_const_mult1)
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult3" ]]
-lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)"
-  apply (simp add: bigo_def)
-(*sledgehammer [no luck]*)
-  apply (rule_tac x = "abs(inverse c)" in exI)
-  apply (simp only: abs_mult [symmetric] mult_assoc [symmetric])
-apply (subst left_inverse) 
-apply (auto )
-done
-
-lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==> 
-    O(f) <= O(%x. c * f x)"
-by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
-
-lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==> 
-    O(%x. c * f x) = O(f)"
-by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult5" ]]
-lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==> 
-    (%x. c) *o O(f) = O(f)"
-  apply (auto del: subsetI)
-  apply (rule order_trans)
-  apply (rule bigo_mult2)
-  apply (simp add: func_times)
-  apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times)
-  apply (rule_tac x = "%y. inverse c * x y" in exI)
-  apply (rename_tac g d) 
-  apply safe
-  apply (rule_tac [2] ext) 
-   prefer 2 
-   apply simp
-  apply (simp add: mult_assoc [symmetric] abs_mult)
-  (* couldn't get this proof without the step above *)
-proof -
-  fix g :: "'b \<Rightarrow> 'a" and d :: 'a
-  assume A1: "c \<noteq> (0\<Colon>'a)"
-  assume A2: "\<forall>x\<Colon>'b. \<bar>g x\<bar> \<le> d * \<bar>f x\<bar>"
-  have F1: "inverse \<bar>c\<bar> = \<bar>inverse c\<bar>" using A1 by (metis nonzero_abs_inverse)
-  have F2: "(0\<Colon>'a) < \<bar>c\<bar>" using A1 by (metis zero_less_abs_iff)
-  have "(0\<Colon>'a) < \<bar>c\<bar> \<longrightarrow> (0\<Colon>'a) < \<bar>inverse c\<bar>" using F1 by (metis positive_imp_inverse_positive)
-  hence "(0\<Colon>'a) < \<bar>inverse c\<bar>" using F2 by metis
-  hence F3: "(0\<Colon>'a) \<le> \<bar>inverse c\<bar>" by (metis order_le_less)
-  have "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar>"
-    using A2 by metis
-  hence F4: "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<and> (0\<Colon>'a) \<le> \<bar>inverse c\<bar>"
-    using F3 by metis
-  hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^isub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^isub>7 (u * v))\<bar>)"
-    by (metis comm_mult_left_mono)
-  thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
-    using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono)
-qed
-
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult6" ]]
-lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
-  apply (auto intro!: subsetI
-    simp add: bigo_def elt_set_times_def func_times
-    simp del: abs_mult mult_ac)
-(*sledgehammer*)
-  apply (rule_tac x = "ca * (abs c)" in exI)
-  apply (rule allI)
-  apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
-  apply (erule ssubst)
-  apply (subst abs_mult)
-  apply (rule mult_left_mono)
-  apply (erule spec)
-  apply simp
-  apply(simp add: mult_ac)
-done
-
-lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"
-proof -
-  assume "f =o O(g)"
-  then have "(%x. c) * f =o (%x. c) *o O(g)"
-    by auto
-  also have "(%x. c) * f = (%x. c * f x)"
-    by (simp add: func_times)
-  also have "(%x. c) *o O(g) <= O(g)"
-    by (auto del: subsetI)
-  finally show ?thesis .
-qed
-
-lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))"
-by (unfold bigo_def, auto)
-
-lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o 
-    O(%x. h(k x))"
-  apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
-      func_plus)
-  apply (erule bigo_compose1)
-done
-
-subsection {* Setsum *}
-
-lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==> 
-    EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==>
-      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"  
-  apply (auto simp add: bigo_def)
-  apply (rule_tac x = "abs c" in exI)
-  apply (subst abs_of_nonneg) back back
-  apply (rule setsum_nonneg)
-  apply force
-  apply (subst setsum_right_distrib)
-  apply (rule allI)
-  apply (rule order_trans)
-  apply (rule setsum_abs)
-  apply (rule setsum_mono)
-apply (blast intro: order_trans mult_right_mono abs_ge_self) 
-done
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum1" ]]
-lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> 
-    EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
-      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
-  apply (rule bigo_setsum_main)
-(*sledgehammer*)
-  apply force
-  apply clarsimp
-  apply (rule_tac x = c in exI)
-  apply force
-done
-
-lemma bigo_setsum2: "ALL y. 0 <= h y ==> 
-    EX c. ALL y. abs(f y) <= c * (h y) ==>
-      (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
-by (rule bigo_setsum1, auto)  
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum3" ]]
-lemma bigo_setsum3: "f =o O(h) ==>
-    (%x. SUM y : A x. (l x y) * f(k x y)) =o
-      O(%x. SUM y : A x. abs(l x y * h(k x y)))"
-  apply (rule bigo_setsum1)
-  apply (rule allI)+
-  apply (rule abs_ge_zero)
-  apply (unfold bigo_def)
-  apply (auto simp add: abs_mult)
-(*sledgehammer*)
-  apply (rule_tac x = c in exI)
-  apply (rule allI)+
-  apply (subst mult_left_commute)
-  apply (rule mult_left_mono)
-  apply (erule spec)
-  apply (rule abs_ge_zero)
-done
-
-lemma bigo_setsum4: "f =o g +o O(h) ==>
-    (%x. SUM y : A x. l x y * f(k x y)) =o
-      (%x. SUM y : A x. l x y * g(k x y)) +o
-        O(%x. SUM y : A x. abs(l x y * h(k x y)))"
-  apply (rule set_minus_imp_plus)
-  apply (subst fun_diff_def)
-  apply (subst setsum_subtractf [symmetric])
-  apply (subst right_diff_distrib [symmetric])
-  apply (rule bigo_setsum3)
-  apply (subst fun_diff_def [symmetric])
-  apply (erule set_plus_imp_minus)
-done
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum5" ]]
-lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> 
-    ALL x. 0 <= h x ==>
-      (%x. SUM y : A x. (l x y) * f(k x y)) =o
-        O(%x. SUM y : A x. (l x y) * h(k x y))" 
-  apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) = 
-      (%x. SUM y : A x. abs((l x y) * h(k x y)))")
-  apply (erule ssubst)
-  apply (erule bigo_setsum3)
-  apply (rule ext)
-  apply (rule setsum_cong2)
-  apply (thin_tac "f \<in> O(h)") 
-apply (metis abs_of_nonneg zero_le_mult_iff)
-done
-
-lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>
-    ALL x. 0 <= h x ==>
-      (%x. SUM y : A x. (l x y) * f(k x y)) =o
-        (%x. SUM y : A x. (l x y) * g(k x y)) +o
-          O(%x. SUM y : A x. (l x y) * h(k x y))" 
-  apply (rule set_minus_imp_plus)
-  apply (subst fun_diff_def)
-  apply (subst setsum_subtractf [symmetric])
-  apply (subst right_diff_distrib [symmetric])
-  apply (rule bigo_setsum5)
-  apply (subst fun_diff_def [symmetric])
-  apply (drule set_plus_imp_minus)
-  apply auto
-done
-
-subsection {* Misc useful stuff *}
-
-lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
-  A \<oplus> B <= O(f)"
-  apply (subst bigo_plus_idemp [symmetric])
-  apply (rule set_plus_mono2)
-  apply assumption+
-done
-
-lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"
-  apply (subst bigo_plus_idemp [symmetric])
-  apply (rule set_plus_intro)
-  apply assumption+
-done
-  
-lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==> 
-    (%x. c) * f =o O(h) ==> f =o O(h)"
-  apply (rule subsetD)
-  apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")
-  apply assumption
-  apply (rule bigo_const_mult6)
-  apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")
-  apply (erule ssubst)
-  apply (erule set_times_intro2)
-  apply (simp add: func_times) 
-done
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_fix" ]]
-lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
-    f =o O(h)"
-  apply (simp add: bigo_alt_def)
-(*sledgehammer*)
-  apply clarify
-  apply (rule_tac x = c in exI)
-  apply safe
-  apply (case_tac "x = 0")
-apply (metis abs_ge_zero  abs_zero  order_less_le  split_mult_pos_le) 
-  apply (subgoal_tac "x = Suc (x - 1)")
-  apply metis
-  apply simp
-  done
-
-
-lemma bigo_fix2: 
-    "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> 
-       f 0 = g 0 ==> f =o g +o O(h)"
-  apply (rule set_minus_imp_plus)
-  apply (rule bigo_fix)
-  apply (subst fun_diff_def)
-  apply (subst fun_diff_def [symmetric])
-  apply (rule set_plus_imp_minus)
-  apply simp
-  apply (simp add: fun_diff_def)
-done
-
-subsection {* Less than or equal to *}
-
-definition lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "<o" 70) where
-  "f <o g == (%x. max (f x - g x) 0)"
-
-lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
-    g =o O(h)"
-  apply (unfold bigo_def)
-  apply clarsimp
-apply (blast intro: order_trans) 
-done
-
-lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>
-      g =o O(h)"
-  apply (erule bigo_lesseq1)
-apply (blast intro: abs_ge_self order_trans) 
-done
-
-lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>
-      g =o O(h)"
-  apply (erule bigo_lesseq2)
-  apply (rule allI)
-  apply (subst abs_of_nonneg)
-  apply (erule spec)+
-done
-
-lemma bigo_lesseq4: "f =o O(h) ==>
-    ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>
-      g =o O(h)"
-  apply (erule bigo_lesseq1)
-  apply (rule allI)
-  apply (subst abs_of_nonneg)
-  apply (erule spec)+
-done
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso1" ]]
-lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
-apply (unfold lesso_def)
-apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
-proof -
-  assume "(\<lambda>x. max (f x - g x) 0) = 0"
-  thus "(\<lambda>x. max (f x - g x) 0) \<in> O(h)" by (metis bigo_zero)
-next
-  show "\<forall>x\<Colon>'a. f x \<le> g x \<Longrightarrow> (\<lambda>x\<Colon>'a. max (f x - g x) (0\<Colon>'b)) = (0\<Colon>'a \<Rightarrow> 'b)"
-  apply (unfold func_zero)
-  apply (rule ext)
-  by (simp split: split_max)
-qed
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso2" ]]
-lemma bigo_lesso2: "f =o g +o O(h) ==>
-    ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
-      k <o g =o O(h)"
-  apply (unfold lesso_def)
-  apply (rule bigo_lesseq4)
-  apply (erule set_plus_imp_minus)
-  apply (rule allI)
-  apply (rule le_maxI2)
-  apply (rule allI)
-  apply (subst fun_diff_def)
-apply (erule thin_rl)
-(*sledgehammer*)
-  apply (case_tac "0 <= k x - g x")
-(* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less
-                le_max_iff_disj min_max.le_supE min_max.sup_absorb2
-                min_max.sup_commute) *)
-proof -
-  fix x :: 'a
-  assume "\<forall>x\<Colon>'a. k x \<le> f x"
-  hence F1: "\<forall>x\<^isub>1\<Colon>'a. max (k x\<^isub>1) (f x\<^isub>1) = f x\<^isub>1" by (metis min_max.sup_absorb2)
-  assume "(0\<Colon>'b) \<le> k x - g x"
-  hence F2: "max (0\<Colon>'b) (k x - g x) = k x - g x" by (metis min_max.sup_absorb2)
-  have F3: "\<forall>x\<^isub>1\<Colon>'b. x\<^isub>1 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_le_iff le_less)
-  have "\<forall>(x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>2 \<or> max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>1" by (metis le_less le_max_iff_disj)
-  hence "\<forall>(x\<^isub>3\<Colon>'b) (x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. x\<^isub>1 - x\<^isub>2 \<le> x\<^isub>3 - x\<^isub>2 \<or> x\<^isub>3 \<le> x\<^isub>1" by (metis add_le_imp_le_right diff_minus min_max.le_supE)
-  hence "k x - g x \<le> f x - g x" by (metis F1 le_less min_max.sup_absorb2 min_max.sup_commute)
-  hence "k x - g x \<le> \<bar>f x - g x\<bar>" by (metis F3 le_max_iff_disj min_max.sup_absorb2)
-  thus "max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>" by (metis F2 min_max.sup_commute)
-next
-  show "\<And>x\<Colon>'a.
-       \<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk>
-       \<Longrightarrow> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
-    by (metis abs_ge_zero le_cases min_max.sup_absorb2)
-qed
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3" ]]
-lemma bigo_lesso3: "f =o g +o O(h) ==>
-    ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
-      f <o k =o O(h)"
-  apply (unfold lesso_def)
-  apply (rule bigo_lesseq4)
-  apply (erule set_plus_imp_minus)
-  apply (rule allI)
-  apply (rule le_maxI2)
-  apply (rule allI)
-  apply (subst fun_diff_def)
-apply (erule thin_rl) 
-(*sledgehammer*)
-  apply (case_tac "0 <= f x - k x")
-  apply (simp)
-  apply (subst abs_of_nonneg)
-  apply (drule_tac x = x in spec) back
-using [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3_simpler" ]]
-apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6))
-apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
-apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
-done
-
-lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::linordered_field) ==>
-    g =o h +o O(k) ==> f <o h =o O(k)"
-  apply (unfold lesso_def)
-  apply (drule set_plus_imp_minus)
-  apply (drule bigo_abs5) back
-  apply (simp add: fun_diff_def)
-  apply (drule bigo_useful_add)
-  apply assumption
-  apply (erule bigo_lesseq2) back
-  apply (rule allI)
-  apply (auto simp add: func_plus fun_diff_def algebra_simps
-    split: split_max abs_split)
-done
-
-declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso5" ]]
-lemma bigo_lesso5: "f <o g =o O(h) ==>
-    EX C. ALL x. f x <= g x + C * abs(h x)"
-  apply (simp only: lesso_def bigo_alt_def)
-  apply clarsimp
-  apply (metis abs_if abs_mult add_commute diff_le_eq less_not_permute)  
-done
-
-end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis_Examples/Big_O.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -0,0 +1,966 @@
+(*  Title:      HOL/Metis_Examples/Big_O.thy
+    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Metis example featuring the Big O notation.
+*)
+
+header {* Metis Example Featuring the Big O Notation *}
+
+theory Big_O
+imports
+  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+  Main
+  "~~/src/HOL/Library/Function_Algebras"
+  "~~/src/HOL/Library/Set_Algebras"
+begin
+
+declare [[metis_new_skolemizer]]
+
+subsection {* Definitions *}
+
+definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set"    ("(1O'(_'))") where
+  "O(f::('a => 'b)) ==   {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_pos_const" ]]
+lemma bigo_pos_const: "(EX (c::'a::linordered_idom).
+    ALL x. (abs (h x)) <= (c * (abs (f x))))
+      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
+  apply auto
+  apply (case_tac "c = 0", simp)
+  apply (rule_tac x = "1" in exI, simp)
+  apply (rule_tac x = "abs c" in exI, auto)
+  apply (metis abs_ge_zero abs_of_nonneg Orderings.xt1(6) abs_mult)
+  done
+
+(*** Now various verions with an increasing shrink factor ***)
+
+sledgehammer_params [isar_proof, isar_shrink_factor = 1]
+
+lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
+    ALL x. (abs (h x)) <= (c * (abs (f x))))
+      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
+  apply auto
+  apply (case_tac "c = 0", simp)
+  apply (rule_tac x = "1" in exI, simp)
+  apply (rule_tac x = "abs c" in exI, auto)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
+  have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
+  have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
+  have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
+    by (metis abs_mult)
+  have F5: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1"
+    by (metis abs_mult_pos)
+  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = \<bar>1\<bar> * x\<^isub>1" by (metis F2)
+  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F2 abs_one)
+  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>h x\<^isub>3\<bar> \<longrightarrow> \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F3)
+  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F1)
+  hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F5)
+  hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F4)
+  hence "\<forall>x\<^isub>3. c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F1)
+  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
+qed
+
+sledgehammer_params [isar_proof, isar_shrink_factor = 2]
+
+lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
+    ALL x. (abs (h x)) <= (c * (abs (f x))))
+      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
+  apply auto
+  apply (case_tac "c = 0", simp)
+  apply (rule_tac x = "1" in exI, simp)
+  apply (rule_tac x = "abs c" in exI, auto)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
+  have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
+    by (metis abs_mult)
+  have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
+  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis A1 abs_ge_zero order_trans)
+  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F2 abs_mult_pos)
+  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
+qed
+
+sledgehammer_params [isar_proof, isar_shrink_factor = 3]
+
+lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
+    ALL x. (abs (h x)) <= (c * (abs (f x))))
+      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
+  apply auto
+  apply (case_tac "c = 0", simp)
+  apply (rule_tac x = "1" in exI, simp)
+  apply (rule_tac x = "abs c" in exI, auto)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
+  have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
+  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
+  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_mult abs_ge_zero)
+qed
+
+sledgehammer_params [isar_proof, isar_shrink_factor = 4]
+
+lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
+    ALL x. (abs (h x)) <= (c * (abs (f x))))
+      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
+  apply auto
+  apply (case_tac "c = 0", simp)
+  apply (rule_tac x = "1" in exI, simp)
+  apply (rule_tac x = "abs c" in exI, auto)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
+  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
+    by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
+  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
+qed
+
+sledgehammer_params [isar_proof, isar_shrink_factor = 1]
+
+lemma bigo_alt_def: "O(f) =
+    {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
+by (auto simp add: bigo_def bigo_pos_const)
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_elt_subset" ]]
+lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
+  apply (auto simp add: bigo_alt_def)
+  apply (rule_tac x = "ca * c" in exI)
+  apply (rule conjI)
+  apply (rule mult_pos_pos)
+  apply (assumption)+
+(*sledgehammer*)
+  apply (rule allI)
+  apply (drule_tac x = "xa" in spec)+
+  apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")
+  apply (erule order_trans)
+  apply (simp add: mult_ac)
+  apply (rule mult_left_mono, assumption)
+  apply (rule order_less_imp_le, assumption)
+done
+
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_refl" ]]
+lemma bigo_refl [intro]: "f : O(f)"
+apply (auto simp add: bigo_def)
+by (metis mult_1 order_refl)
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_zero" ]]
+lemma bigo_zero: "0 : O(g)"
+apply (auto simp add: bigo_def func_zero)
+by (metis mult_zero_left order_refl)
+
+lemma bigo_zero2: "O(%x.0) = {%x.0}"
+  by (auto simp add: bigo_def)
+
+lemma bigo_plus_self_subset [intro]:
+  "O(f) \<oplus> O(f) <= O(f)"
+  apply (auto simp add: bigo_alt_def set_plus_def)
+  apply (rule_tac x = "c + ca" in exI)
+  apply auto
+  apply (simp add: ring_distribs func_plus)
+  apply (blast intro:order_trans abs_triangle_ineq add_mono elim:)
+done
+
+lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)"
+  apply (rule equalityI)
+  apply (rule bigo_plus_self_subset)
+  apply (rule set_zero_plus2)
+  apply (rule bigo_zero)
+done
+
+lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)"
+  apply (rule subsetI)
+  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
+  apply (subst bigo_pos_const [symmetric])+
+  apply (rule_tac x =
+    "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
+  apply (rule conjI)
+  apply (rule_tac x = "c + c" in exI)
+  apply (clarsimp)
+  apply (auto)
+  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
+  apply (erule_tac x = xa in allE)
+  apply (erule order_trans)
+  apply (simp)
+  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+  apply (erule order_trans)
+  apply (simp add: ring_distribs)
+  apply (rule mult_left_mono)
+  apply assumption
+  apply (simp add: order_less_le)
+  apply (rule mult_left_mono)
+  apply (simp add: abs_triangle_ineq)
+  apply (simp add: order_less_le)
+  apply (rule mult_nonneg_nonneg)
+  apply (rule add_nonneg_nonneg)
+  apply auto
+  apply (rule_tac x = "%n. if (abs (f n)) <  abs (g n) then x n else 0"
+     in exI)
+  apply (rule conjI)
+  apply (rule_tac x = "c + c" in exI)
+  apply auto
+  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
+  apply (erule_tac x = xa in allE)
+  apply (erule order_trans)
+  apply (simp)
+  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+  apply (erule order_trans)
+  apply (simp add: ring_distribs)
+  apply (rule mult_left_mono)
+  apply (simp add: order_less_le)
+  apply (simp add: order_less_le)
+  apply (rule mult_left_mono)
+  apply (rule abs_triangle_ineq)
+  apply (simp add: order_less_le)
+apply (metis abs_not_less_zero double_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)
+  apply (rule ext)
+  apply (auto simp add: if_splits linorder_not_le)
+done
+
+lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"
+  apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)")
+  apply (erule order_trans)
+  apply simp
+  apply (auto del: subsetI simp del: bigo_plus_idemp)
+done
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq" ]]
+lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==>
+  O(f + g) = O(f) \<oplus> O(g)"
+  apply (rule equalityI)
+  apply (rule bigo_plus_subset)
+  apply (simp add: bigo_alt_def set_plus_def func_plus)
+  apply clarify
+(*sledgehammer*)
+  apply (rule_tac x = "max c ca" in exI)
+  apply (rule conjI)
+   apply (metis Orderings.less_max_iff_disj)
+  apply clarify
+  apply (drule_tac x = "xa" in spec)+
+  apply (subgoal_tac "0 <= f xa + g xa")
+  apply (simp add: ring_distribs)
+  apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
+  apply (subgoal_tac "abs(a xa) + abs(b xa) <=
+      max c ca * f xa + max c ca * g xa")
+  apply (blast intro: order_trans)
+  defer 1
+  apply (rule abs_triangle_ineq)
+  apply (metis add_nonneg_nonneg)
+  apply (rule add_mono)
+using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]]
+  apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
+  apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
+done
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt" ]]
+lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
+    f : O(g)"
+  apply (auto simp add: bigo_def)
+(* Version 1: one-line proof *)
+  apply (metis abs_le_D1 linorder_class.not_less  order_less_le  Orderings.xt1(12)  abs_mult)
+  done
+
+lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
+    f : O(g)"
+apply (auto simp add: bigo_def)
+(* Version 2: structured proof *)
+proof -
+  assume "\<forall>x. f x \<le> c * g x"
+  thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
+qed
+
+text{*So here is the easier (and more natural) problem using transitivity*}
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
+lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)"
+apply (auto simp add: bigo_def)
+(* Version 1: one-line proof *)
+by (metis abs_ge_self abs_mult order_trans)
+
+text{*So here is the easier (and more natural) problem using transitivity*}
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
+lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)"
+  apply (auto simp add: bigo_def)
+(* Version 2: structured proof *)
+proof -
+  assume "\<forall>x. f x \<le> c * g x"
+  thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
+qed
+
+lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==>
+    f : O(g)"
+  apply (erule bigo_bounded_alt [of f 1 g])
+  apply simp
+done
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded2" ]]
+lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
+    f : lb +o O(g)"
+apply (rule set_minus_imp_plus)
+apply (rule bigo_bounded)
+ apply (auto simp add: diff_minus fun_Compl_def func_plus)
+ prefer 2
+ apply (drule_tac x = x in spec)+
+ apply (metis add_right_mono add_commute diff_add_cancel diff_minus_eq_add le_less order_trans)
+proof -
+  fix x :: 'a
+  assume "\<forall>x. lb x \<le> f x"
+  thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le)
+qed
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs" ]]
+lemma bigo_abs: "(%x. abs(f x)) =o O(f)"
+apply (unfold bigo_def)
+apply auto
+by (metis mult_1 order_refl)
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs2" ]]
+lemma bigo_abs2: "f =o O(%x. abs(f x))"
+apply (unfold bigo_def)
+apply auto
+by (metis mult_1 order_refl)
+
+lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
+proof -
+  have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset)
+  have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs)
+  have "\<forall>u. u \<in> O(\<lambda>R. \<bar>u R\<bar>)" by (metis bigo_abs2)
+  thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto
+qed
+
+lemma bigo_abs4: "f =o g +o O(h) ==>
+    (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
+  apply (drule set_plus_imp_minus)
+  apply (rule set_minus_imp_plus)
+  apply (subst fun_diff_def)
+proof -
+  assume a: "f - g : O(h)"
+  have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
+    by (rule bigo_abs2)
+  also have "... <= O(%x. abs (f x - g x))"
+    apply (rule bigo_elt_subset)
+    apply (rule bigo_bounded)
+    apply force
+    apply (rule allI)
+    apply (rule abs_triangle_ineq3)
+    done
+  also have "... <= O(f - g)"
+    apply (rule bigo_elt_subset)
+    apply (subst fun_diff_def)
+    apply (rule bigo_abs)
+    done
+  also have "... <= O(h)"
+    using a by (rule bigo_elt_subset)
+  finally show "(%x. abs (f x) - abs (g x)) : O(h)".
+qed
+
+lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)"
+by (unfold bigo_def, auto)
+
+lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)"
+proof -
+  assume "f : g +o O(h)"
+  also have "... <= O(g) \<oplus> O(h)"
+    by (auto del: subsetI)
+  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
+    apply (subst bigo_abs3 [symmetric])+
+    apply (rule refl)
+    done
+  also have "... = O((%x. abs(g x)) + (%x. abs(h x)))"
+    by (rule bigo_plus_eq [symmetric], auto)
+  finally have "f : ...".
+  then have "O(f) <= ..."
+    by (elim bigo_elt_subset)
+  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
+    by (rule bigo_plus_eq, auto)
+  finally show ?thesis
+    by (simp add: bigo_abs3 [symmetric])
+qed
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult" ]]
+lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
+  apply (rule subsetI)
+  apply (subst bigo_def)
+  apply (auto simp del: abs_mult mult_ac
+              simp add: bigo_alt_def set_times_def func_times)
+(*sledgehammer*)
+  apply (rule_tac x = "c * ca" in exI)
+  apply(rule allI)
+  apply(erule_tac x = x in allE)+
+  apply(subgoal_tac "c * ca * abs(f x * g x) =
+      (c * abs(f x)) * (ca * abs(g x))")
+using [[ sledgehammer_problem_prefix = "BigO__bigo_mult_simpler" ]]
+prefer 2
+apply (metis mult_assoc mult_left_commute
+  abs_of_pos mult_left_commute
+  abs_mult mult_pos_pos)
+  apply (erule ssubst)
+  apply (subst abs_mult)
+(* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since
+   abs_mult has just been done *)
+by (metis abs_ge_zero mult_mono')
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult2" ]]
+lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
+  apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
+(*sledgehammer*)
+  apply (rule_tac x = c in exI)
+  apply clarify
+  apply (drule_tac x = x in spec)
+using [[ sledgehammer_problem_prefix = "BigO__bigo_mult2_simpler" ]]
+(*sledgehammer [no luck]*)
+  apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
+  apply (simp add: mult_ac)
+  apply (rule mult_left_mono, assumption)
+  apply (rule abs_ge_zero)
+done
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult3" ]]
+lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
+by (metis bigo_mult set_rev_mp set_times_intro)
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult4" ]]
+lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
+by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib)
+
+
+lemma bigo_mult5: "ALL x. f x ~= 0 ==>
+    O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
+proof -
+  assume a: "ALL x. f x ~= 0"
+  show "O(f * g) <= f *o O(g)"
+  proof
+    fix h
+    assume h: "h : O(f * g)"
+    then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
+      by auto
+    also have "... <= O((%x. 1 / f x) * (f * g))"
+      by (rule bigo_mult2)
+    also have "(%x. 1 / f x) * (f * g) = g"
+      apply (simp add: func_times)
+      apply (rule ext)
+      apply (simp add: a h nonzero_divide_eq_eq mult_ac)
+      done
+    finally have "(%x. (1::'b) / f x) * h : O(g)".
+    then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
+      by auto
+    also have "f * ((%x. (1::'b) / f x) * h) = h"
+      apply (simp add: func_times)
+      apply (rule ext)
+      apply (simp add: a h nonzero_divide_eq_eq mult_ac)
+      done
+    finally show "h : f *o O(g)".
+  qed
+qed
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult6" ]]
+lemma bigo_mult6: "ALL x. f x ~= 0 ==>
+    O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)"
+by (metis bigo_mult2 bigo_mult5 order_antisym)
+
+(*proof requires relaxing relevance: 2007-01-25*)
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult7" ]]
+  declare bigo_mult6 [simp]
+lemma bigo_mult7: "ALL x. f x ~= 0 ==>
+    O(f * g) <= O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
+(*sledgehammer*)
+  apply (subst bigo_mult6)
+  apply assumption
+  apply (rule set_times_mono3)
+  apply (rule bigo_refl)
+done
+  declare bigo_mult6 [simp del]
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult8" ]]
+  declare bigo_mult7[intro!]
+lemma bigo_mult8: "ALL x. f x ~= 0 ==>
+    O(f * g) = O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
+by (metis bigo_mult bigo_mult7 order_antisym_conv)
+
+lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
+  by (auto simp add: bigo_def fun_Compl_def)
+
+lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
+  apply (rule set_minus_imp_plus)
+  apply (drule set_plus_imp_minus)
+  apply (drule bigo_minus)
+  apply (simp add: diff_minus)
+done
+
+lemma bigo_minus3: "O(-f) = O(f)"
+  by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
+
+lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
+proof -
+  assume a: "f : O(g)"
+  show "f +o O(g) <= O(g)"
+  proof -
+    have "f : O(f)" by auto
+    then have "f +o O(g) <= O(f) \<oplus> O(g)"
+      by (auto del: subsetI)
+    also have "... <= O(g) \<oplus> O(g)"
+    proof -
+      from a have "O(f) <= O(g)" by (auto del: subsetI)
+      thus ?thesis by (auto del: subsetI)
+    qed
+    also have "... <= O(g)" by (simp add: bigo_plus_idemp)
+    finally show ?thesis .
+  qed
+qed
+
+lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)"
+proof -
+  assume a: "f : O(g)"
+  show "O(g) <= f +o O(g)"
+  proof -
+    from a have "-f : O(g)" by auto
+    then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1)
+    then have "f +o (-f +o O(g)) <= f +o O(g)" by auto
+    also have "f +o (-f +o O(g)) = O(g)"
+      by (simp add: set_plus_rearranges)
+    finally show ?thesis .
+  qed
+qed
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_absorb" ]]
+lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)"
+by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff)
+
+lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"
+  apply (subgoal_tac "f +o A <= f +o O(g)")
+  apply force+
+done
+
+lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"
+  apply (subst set_minus_plus [symmetric])
+  apply (subgoal_tac "g - f = - (f - g)")
+  apply (erule ssubst)
+  apply (rule bigo_minus)
+  apply (subst set_minus_plus)
+  apply assumption
+  apply  (simp add: diff_minus add_ac)
+done
+
+lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
+  apply (rule iffI)
+  apply (erule bigo_add_commute_imp)+
+done
+
+lemma bigo_const1: "(%x. c) : O(%x. 1)"
+by (auto simp add: bigo_def mult_ac)
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_const2" ]]
+lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)"
+by (metis bigo_const1 bigo_elt_subset)
+
+lemma bigo_const2 [intro]: "O(%x. c::'b::linordered_idom) <= O(%x. 1)"
+(* "thus" had to be replaced by "show" with an explicit reference to "F1" *)
+proof -
+  have F1: "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1)
+  show "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis F1 bigo_elt_subset)
+qed
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_const3" ]]
+lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
+apply (simp add: bigo_def)
+by (metis abs_eq_0 left_inverse order_refl)
+
+lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
+by (rule bigo_elt_subset, rule bigo_const3, assumption)
+
+lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==>
+    O(%x. c) = O(%x. 1)"
+by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult1" ]]
+lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
+  apply (simp add: bigo_def abs_mult)
+by (metis le_less)
+
+lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
+by (rule bigo_elt_subset, rule bigo_const_mult1)
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult3" ]]
+lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)"
+  apply (simp add: bigo_def)
+(*sledgehammer [no luck]*)
+  apply (rule_tac x = "abs(inverse c)" in exI)
+  apply (simp only: abs_mult [symmetric] mult_assoc [symmetric])
+apply (subst left_inverse)
+apply (auto )
+done
+
+lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==>
+    O(f) <= O(%x. c * f x)"
+by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
+
+lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==>
+    O(%x. c * f x) = O(f)"
+by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult5" ]]
+lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==>
+    (%x. c) *o O(f) = O(f)"
+  apply (auto del: subsetI)
+  apply (rule order_trans)
+  apply (rule bigo_mult2)
+  apply (simp add: func_times)
+  apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times)
+  apply (rule_tac x = "%y. inverse c * x y" in exI)
+  apply (rename_tac g d)
+  apply safe
+  apply (rule_tac [2] ext)
+   prefer 2
+   apply simp
+  apply (simp add: mult_assoc [symmetric] abs_mult)
+  (* couldn't get this proof without the step above *)
+proof -
+  fix g :: "'b \<Rightarrow> 'a" and d :: 'a
+  assume A1: "c \<noteq> (0\<Colon>'a)"
+  assume A2: "\<forall>x\<Colon>'b. \<bar>g x\<bar> \<le> d * \<bar>f x\<bar>"
+  have F1: "inverse \<bar>c\<bar> = \<bar>inverse c\<bar>" using A1 by (metis nonzero_abs_inverse)
+  have F2: "(0\<Colon>'a) < \<bar>c\<bar>" using A1 by (metis zero_less_abs_iff)
+  have "(0\<Colon>'a) < \<bar>c\<bar> \<longrightarrow> (0\<Colon>'a) < \<bar>inverse c\<bar>" using F1 by (metis positive_imp_inverse_positive)
+  hence "(0\<Colon>'a) < \<bar>inverse c\<bar>" using F2 by metis
+  hence F3: "(0\<Colon>'a) \<le> \<bar>inverse c\<bar>" by (metis order_le_less)
+  have "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar>"
+    using A2 by metis
+  hence F4: "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<and> (0\<Colon>'a) \<le> \<bar>inverse c\<bar>"
+    using F3 by metis
+  hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^isub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^isub>7 (u * v))\<bar>)"
+    by (metis comm_mult_left_mono)
+  thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
+    using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono)
+qed
+
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult6" ]]
+lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
+  apply (auto intro!: subsetI
+    simp add: bigo_def elt_set_times_def func_times
+    simp del: abs_mult mult_ac)
+(*sledgehammer*)
+  apply (rule_tac x = "ca * (abs c)" in exI)
+  apply (rule allI)
+  apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
+  apply (erule ssubst)
+  apply (subst abs_mult)
+  apply (rule mult_left_mono)
+  apply (erule spec)
+  apply simp
+  apply(simp add: mult_ac)
+done
+
+lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"
+proof -
+  assume "f =o O(g)"
+  then have "(%x. c) * f =o (%x. c) *o O(g)"
+    by auto
+  also have "(%x. c) * f = (%x. c * f x)"
+    by (simp add: func_times)
+  also have "(%x. c) *o O(g) <= O(g)"
+    by (auto del: subsetI)
+  finally show ?thesis .
+qed
+
+lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))"
+by (unfold bigo_def, auto)
+
+lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o
+    O(%x. h(k x))"
+  apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
+      func_plus)
+  apply (erule bigo_compose1)
+done
+
+subsection {* Setsum *}
+
+lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==>
+    EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==>
+      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
+  apply (auto simp add: bigo_def)
+  apply (rule_tac x = "abs c" in exI)
+  apply (subst abs_of_nonneg) back back
+  apply (rule setsum_nonneg)
+  apply force
+  apply (subst setsum_right_distrib)
+  apply (rule allI)
+  apply (rule order_trans)
+  apply (rule setsum_abs)
+  apply (rule setsum_mono)
+apply (blast intro: order_trans mult_right_mono abs_ge_self)
+done
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum1" ]]
+lemma bigo_setsum1: "ALL x y. 0 <= h x y ==>
+    EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
+      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
+  apply (rule bigo_setsum_main)
+(*sledgehammer*)
+  apply force
+  apply clarsimp
+  apply (rule_tac x = c in exI)
+  apply force
+done
+
+lemma bigo_setsum2: "ALL y. 0 <= h y ==>
+    EX c. ALL y. abs(f y) <= c * (h y) ==>
+      (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
+by (rule bigo_setsum1, auto)
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum3" ]]
+lemma bigo_setsum3: "f =o O(h) ==>
+    (%x. SUM y : A x. (l x y) * f(k x y)) =o
+      O(%x. SUM y : A x. abs(l x y * h(k x y)))"
+  apply (rule bigo_setsum1)
+  apply (rule allI)+
+  apply (rule abs_ge_zero)
+  apply (unfold bigo_def)
+  apply (auto simp add: abs_mult)
+(*sledgehammer*)
+  apply (rule_tac x = c in exI)
+  apply (rule allI)+
+  apply (subst mult_left_commute)
+  apply (rule mult_left_mono)
+  apply (erule spec)
+  apply (rule abs_ge_zero)
+done
+
+lemma bigo_setsum4: "f =o g +o O(h) ==>
+    (%x. SUM y : A x. l x y * f(k x y)) =o
+      (%x. SUM y : A x. l x y * g(k x y)) +o
+        O(%x. SUM y : A x. abs(l x y * h(k x y)))"
+  apply (rule set_minus_imp_plus)
+  apply (subst fun_diff_def)
+  apply (subst setsum_subtractf [symmetric])
+  apply (subst right_diff_distrib [symmetric])
+  apply (rule bigo_setsum3)
+  apply (subst fun_diff_def [symmetric])
+  apply (erule set_plus_imp_minus)
+done
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum5" ]]
+lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==>
+    ALL x. 0 <= h x ==>
+      (%x. SUM y : A x. (l x y) * f(k x y)) =o
+        O(%x. SUM y : A x. (l x y) * h(k x y))"
+  apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) =
+      (%x. SUM y : A x. abs((l x y) * h(k x y)))")
+  apply (erule ssubst)
+  apply (erule bigo_setsum3)
+  apply (rule ext)
+  apply (rule setsum_cong2)
+  apply (thin_tac "f \<in> O(h)")
+apply (metis abs_of_nonneg zero_le_mult_iff)
+done
+
+lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>
+    ALL x. 0 <= h x ==>
+      (%x. SUM y : A x. (l x y) * f(k x y)) =o
+        (%x. SUM y : A x. (l x y) * g(k x y)) +o
+          O(%x. SUM y : A x. (l x y) * h(k x y))"
+  apply (rule set_minus_imp_plus)
+  apply (subst fun_diff_def)
+  apply (subst setsum_subtractf [symmetric])
+  apply (subst right_diff_distrib [symmetric])
+  apply (rule bigo_setsum5)
+  apply (subst fun_diff_def [symmetric])
+  apply (drule set_plus_imp_minus)
+  apply auto
+done
+
+subsection {* Misc useful stuff *}
+
+lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
+  A \<oplus> B <= O(f)"
+  apply (subst bigo_plus_idemp [symmetric])
+  apply (rule set_plus_mono2)
+  apply assumption+
+done
+
+lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"
+  apply (subst bigo_plus_idemp [symmetric])
+  apply (rule set_plus_intro)
+  apply assumption+
+done
+
+lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==>
+    (%x. c) * f =o O(h) ==> f =o O(h)"
+  apply (rule subsetD)
+  apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")
+  apply assumption
+  apply (rule bigo_const_mult6)
+  apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")
+  apply (erule ssubst)
+  apply (erule set_times_intro2)
+  apply (simp add: func_times)
+done
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_fix" ]]
+lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
+    f =o O(h)"
+  apply (simp add: bigo_alt_def)
+(*sledgehammer*)
+  apply clarify
+  apply (rule_tac x = c in exI)
+  apply safe
+  apply (case_tac "x = 0")
+apply (metis abs_ge_zero  abs_zero  order_less_le  split_mult_pos_le)
+  apply (subgoal_tac "x = Suc (x - 1)")
+  apply metis
+  apply simp
+  done
+
+
+lemma bigo_fix2:
+    "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==>
+       f 0 = g 0 ==> f =o g +o O(h)"
+  apply (rule set_minus_imp_plus)
+  apply (rule bigo_fix)
+  apply (subst fun_diff_def)
+  apply (subst fun_diff_def [symmetric])
+  apply (rule set_plus_imp_minus)
+  apply simp
+  apply (simp add: fun_diff_def)
+done
+
+subsection {* Less than or equal to *}
+
+definition lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "<o" 70) where
+  "f <o g == (%x. max (f x - g x) 0)"
+
+lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
+    g =o O(h)"
+  apply (unfold bigo_def)
+  apply clarsimp
+apply (blast intro: order_trans)
+done
+
+lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>
+      g =o O(h)"
+  apply (erule bigo_lesseq1)
+apply (blast intro: abs_ge_self order_trans)
+done
+
+lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>
+      g =o O(h)"
+  apply (erule bigo_lesseq2)
+  apply (rule allI)
+  apply (subst abs_of_nonneg)
+  apply (erule spec)+
+done
+
+lemma bigo_lesseq4: "f =o O(h) ==>
+    ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>
+      g =o O(h)"
+  apply (erule bigo_lesseq1)
+  apply (rule allI)
+  apply (subst abs_of_nonneg)
+  apply (erule spec)+
+done
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso1" ]]
+lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
+apply (unfold lesso_def)
+apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
+proof -
+  assume "(\<lambda>x. max (f x - g x) 0) = 0"
+  thus "(\<lambda>x. max (f x - g x) 0) \<in> O(h)" by (metis bigo_zero)
+next
+  show "\<forall>x\<Colon>'a. f x \<le> g x \<Longrightarrow> (\<lambda>x\<Colon>'a. max (f x - g x) (0\<Colon>'b)) = (0\<Colon>'a \<Rightarrow> 'b)"
+  apply (unfold func_zero)
+  apply (rule ext)
+  by (simp split: split_max)
+qed
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso2" ]]
+lemma bigo_lesso2: "f =o g +o O(h) ==>
+    ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
+      k <o g =o O(h)"
+  apply (unfold lesso_def)
+  apply (rule bigo_lesseq4)
+  apply (erule set_plus_imp_minus)
+  apply (rule allI)
+  apply (rule le_maxI2)
+  apply (rule allI)
+  apply (subst fun_diff_def)
+apply (erule thin_rl)
+(*sledgehammer*)
+  apply (case_tac "0 <= k x - g x")
+(* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less
+                le_max_iff_disj min_max.le_supE min_max.sup_absorb2
+                min_max.sup_commute) *)
+proof -
+  fix x :: 'a
+  assume "\<forall>x\<Colon>'a. k x \<le> f x"
+  hence F1: "\<forall>x\<^isub>1\<Colon>'a. max (k x\<^isub>1) (f x\<^isub>1) = f x\<^isub>1" by (metis min_max.sup_absorb2)
+  assume "(0\<Colon>'b) \<le> k x - g x"
+  hence F2: "max (0\<Colon>'b) (k x - g x) = k x - g x" by (metis min_max.sup_absorb2)
+  have F3: "\<forall>x\<^isub>1\<Colon>'b. x\<^isub>1 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_le_iff le_less)
+  have "\<forall>(x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>2 \<or> max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>1" by (metis le_less le_max_iff_disj)
+  hence "\<forall>(x\<^isub>3\<Colon>'b) (x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. x\<^isub>1 - x\<^isub>2 \<le> x\<^isub>3 - x\<^isub>2 \<or> x\<^isub>3 \<le> x\<^isub>1" by (metis add_le_imp_le_right diff_minus min_max.le_supE)
+  hence "k x - g x \<le> f x - g x" by (metis F1 le_less min_max.sup_absorb2 min_max.sup_commute)
+  hence "k x - g x \<le> \<bar>f x - g x\<bar>" by (metis F3 le_max_iff_disj min_max.sup_absorb2)
+  thus "max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>" by (metis F2 min_max.sup_commute)
+next
+  show "\<And>x\<Colon>'a.
+       \<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk>
+       \<Longrightarrow> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
+    by (metis abs_ge_zero le_cases min_max.sup_absorb2)
+qed
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3" ]]
+lemma bigo_lesso3: "f =o g +o O(h) ==>
+    ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
+      f <o k =o O(h)"
+  apply (unfold lesso_def)
+  apply (rule bigo_lesseq4)
+  apply (erule set_plus_imp_minus)
+  apply (rule allI)
+  apply (rule le_maxI2)
+  apply (rule allI)
+  apply (subst fun_diff_def)
+apply (erule thin_rl)
+(*sledgehammer*)
+  apply (case_tac "0 <= f x - k x")
+  apply (simp)
+  apply (subst abs_of_nonneg)
+  apply (drule_tac x = x in spec) back
+using [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3_simpler" ]]
+apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6))
+apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
+apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
+done
+
+lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::linordered_field) ==>
+    g =o h +o O(k) ==> f <o h =o O(k)"
+  apply (unfold lesso_def)
+  apply (drule set_plus_imp_minus)
+  apply (drule bigo_abs5) back
+  apply (simp add: fun_diff_def)
+  apply (drule bigo_useful_add)
+  apply assumption
+  apply (erule bigo_lesseq2) back
+  apply (rule allI)
+  apply (auto simp add: func_plus fun_diff_def algebra_simps
+    split: split_max abs_split)
+done
+
+declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso5" ]]
+lemma bigo_lesso5: "f <o g =o O(h) ==>
+    EX C. ALL x. f x <= g x + C * abs(h x)"
+  apply (simp only: lesso_def bigo_alt_def)
+  apply clarsimp
+  apply (metis abs_if abs_mult add_commute diff_le_eq less_not_permute)
+done
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -0,0 +1,278 @@
+(*  Title:      HOL/Metis_Examples/Binary_Tree.thy
+    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Metis example featuring binary trees.
+*)
+
+header {* Metis Example Featuring Binary Trees *}
+
+theory Binary_Tree
+imports Main
+begin
+
+declare [[metis_new_skolemizer]]
+
+datatype 'a bt =
+    Lf
+  | Br 'a  "'a bt"  "'a bt"
+
+primrec n_nodes :: "'a bt => nat" where
+  "n_nodes Lf = 0"
+| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
+
+primrec n_leaves :: "'a bt => nat" where
+  "n_leaves Lf = Suc 0"
+| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
+
+primrec depth :: "'a bt => nat" where
+  "depth Lf = 0"
+| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
+
+primrec reflect :: "'a bt => 'a bt" where
+  "reflect Lf = Lf"
+| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
+
+primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
+  "bt_map f Lf = Lf"
+| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
+
+primrec preorder :: "'a bt => 'a list" where
+  "preorder Lf = []"
+| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
+
+primrec inorder :: "'a bt => 'a list" where
+  "inorder Lf = []"
+| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
+
+primrec postorder :: "'a bt => 'a list" where
+  "postorder Lf = []"
+| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
+
+primrec append :: "'a bt => 'a bt => 'a bt" where
+  "append Lf t = t"
+| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
+
+text {* \medskip BT simplification *}
+
+declare [[ sledgehammer_problem_prefix = "BT__n_leaves_reflect" ]]
+
+lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
+proof (induct t)
+  case Lf thus ?case
+  proof -
+    let "?p\<^isub>1 x\<^isub>1" = "x\<^isub>1 \<noteq> n_leaves (reflect (Lf::'a bt))"
+    have "\<not> ?p\<^isub>1 (Suc 0)" by (metis reflect.simps(1) n_leaves.simps(1))
+    hence "\<not> ?p\<^isub>1 (n_leaves (Lf::'a bt))" by (metis n_leaves.simps(1))
+    thus "n_leaves (reflect (Lf::'a bt)) = n_leaves (Lf::'a bt)" by metis
+  qed
+next
+  case (Br a t1 t2) thus ?case
+    by (metis n_leaves.simps(2) nat_add_commute reflect.simps(2))
+qed
+
+declare [[ sledgehammer_problem_prefix = "BT__n_nodes_reflect" ]]
+
+lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
+proof (induct t)
+  case Lf thus ?case by (metis reflect.simps(1))
+next
+  case (Br a t1 t2) thus ?case
+    by (metis add_commute n_nodes.simps(2) reflect.simps(2))
+qed
+
+declare [[ sledgehammer_problem_prefix = "BT__depth_reflect" ]]
+
+lemma depth_reflect: "depth (reflect t) = depth t"
+apply (induct t)
+ apply (metis depth.simps(1) reflect.simps(1))
+by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2))
+
+text {*
+The famous relationship between the numbers of leaves and nodes.
+*}
+
+declare [[ sledgehammer_problem_prefix = "BT__n_leaves_nodes" ]]
+
+lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
+apply (induct t)
+ apply (metis n_leaves.simps(1) n_nodes.simps(1))
+by auto
+
+declare [[ sledgehammer_problem_prefix = "BT__reflect_reflect_ident" ]]
+
+lemma reflect_reflect_ident: "reflect (reflect t) = t"
+apply (induct t)
+ apply (metis reflect.simps(1))
+proof -
+  fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt"
+  assume A1: "reflect (reflect t1) = t1"
+  assume A2: "reflect (reflect t2) = t2"
+  have "\<And>V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)"
+    using A1 by (metis reflect.simps(2))
+  hence "\<And>V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))"
+    by (metis reflect.simps(2))
+  hence "\<And>U. reflect (reflect (Br U t1 t2)) = Br U t1 t2"
+    using A2 by metis
+  thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast
+qed
+
+declare [[ sledgehammer_problem_prefix = "BT__bt_map_ident" ]]
+
+lemma bt_map_ident: "bt_map (%x. x) = (%y. y)"
+apply (rule ext)
+apply (induct_tac y)
+ apply (metis bt_map.simps(1))
+by (metis bt_map.simps(2))
+
+declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
+
+lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)"
+apply (induct t)
+ apply (metis append.simps(1) bt_map.simps(1))
+by (metis append.simps(2) bt_map.simps(2))
+
+declare [[ sledgehammer_problem_prefix = "BT__bt_map_compose" ]]
+
+lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)"
+apply (induct t)
+ apply (metis bt_map.simps(1))
+by (metis bt_map.simps(2) o_eq_dest_lhs)
+
+declare [[ sledgehammer_problem_prefix = "BT__bt_map_reflect" ]]
+
+lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
+apply (induct t)
+ apply (metis bt_map.simps(1) reflect.simps(1))
+by (metis bt_map.simps(2) reflect.simps(2))
+
+declare [[ sledgehammer_problem_prefix = "BT__preorder_bt_map" ]]
+
+lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
+apply (induct t)
+ apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
+by simp
+
+declare [[ sledgehammer_problem_prefix = "BT__inorder_bt_map" ]]
+
+lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
+proof (induct t)
+  case Lf thus ?case
+  proof -
+    have "map f [] = []" by (metis map.simps(1))
+    hence "map f [] = inorder Lf" by (metis inorder.simps(1))
+    hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1))
+    thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1))
+  qed
+next
+  case (Br a t1 t2) thus ?case by simp
+qed
+
+declare [[ sledgehammer_problem_prefix = "BT__postorder_bt_map" ]]
+
+lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
+apply (induct t)
+ apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1))
+by simp
+
+declare [[ sledgehammer_problem_prefix = "BT__depth_bt_map" ]]
+
+lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
+apply (induct t)
+ apply (metis bt_map.simps(1) depth.simps(1))
+by simp
+
+declare [[ sledgehammer_problem_prefix = "BT__n_leaves_bt_map" ]]
+
+lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
+apply (induct t)
+ apply (metis bt_map.simps(1) n_leaves.simps(1))
+proof -
+  fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt"
+  assume A1: "n_leaves (bt_map f t1) = n_leaves t1"
+  assume A2: "n_leaves (bt_map f t2) = n_leaves t2"
+  have "\<And>V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V"
+    using A1 by (metis n_leaves.simps(2))
+  hence "\<And>V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)"
+    by (metis bt_map.simps(2))
+  hence F1: "\<And>U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2"
+    using A2 by metis
+  have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)"
+    by (metis n_leaves.simps(2))
+  thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)"
+    using F1 by metis
+qed
+
+declare [[ sledgehammer_problem_prefix = "BT__preorder_reflect" ]]
+
+lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
+apply (induct t)
+ apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
+              reflect.simps(1))
+apply simp
+done
+
+declare [[ sledgehammer_problem_prefix = "BT__inorder_reflect" ]]
+
+lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
+apply (induct t)
+ apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1))
+by simp
+(* Slow:
+by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2)
+          reflect.simps(2) rev.simps(2) rev_append)
+*)
+
+declare [[ sledgehammer_problem_prefix = "BT__postorder_reflect" ]]
+
+lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
+apply (induct t)
+ apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
+              reflect.simps(1))
+by (metis preorder_reflect reflect_reflect_ident rev_swap)
+
+text {*
+Analogues of the standard properties of the append function for lists.
+*}
+
+declare [[ sledgehammer_problem_prefix = "BT__append_assoc" ]]
+
+lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)"
+apply (induct t1)
+ apply (metis append.simps(1))
+by (metis append.simps(2))
+
+declare [[ sledgehammer_problem_prefix = "BT__append_Lf2" ]]
+
+lemma append_Lf2 [simp]: "append t Lf = t"
+apply (induct t)
+ apply (metis append.simps(1))
+by (metis append.simps(2))
+
+declare max_add_distrib_left [simp]
+
+declare [[ sledgehammer_problem_prefix = "BT__depth_append" ]]
+
+lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
+apply (induct t1)
+ apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1))
+by simp
+
+declare [[ sledgehammer_problem_prefix = "BT__n_leaves_append" ]]
+
+lemma n_leaves_append [simp]:
+     "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
+apply (induct t1)
+ apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
+              semiring_norm(111))
+by (simp add: left_distrib)
+
+declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
+
+lemma (*bt_map_append:*)
+     "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
+apply (induct t1)
+ apply (metis append.simps(1) bt_map.simps(1))
+by (metis bt_map_append)
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis_Examples/Clausification.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -0,0 +1,150 @@
+(*  Title:      HOL/Metis_Examples/Clausification.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Example that exercises Metis's Clausifier.
+*)
+
+header {* Example that Exercises Metis's Clausifier *}
+
+theory Clausification
+imports Complex_Main
+begin
+
+(* FIXME: shouldn't need this *)
+declare [[unify_search_bound = 100]]
+declare [[unify_trace_bound = 100]]
+
+
+text {* Definitional CNF for facts *}
+
+declare [[meson_max_clauses = 10]]
+
+axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
+qax: "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
+
+declare [[metis_new_skolemizer = false]]
+
+lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
+by (metis qax)
+
+lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
+by (metisFT qax)
+
+lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
+by (metis qax)
+
+lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
+by (metisFT qax)
+
+declare [[metis_new_skolemizer]]
+
+lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
+by (metis qax)
+
+lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
+by (metisFT qax)
+
+lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
+by (metis qax)
+
+lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
+by (metisFT qax)
+
+declare [[meson_max_clauses = 60]]
+
+axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
+rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
+      (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
+      (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
+      (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
+
+declare [[metis_new_skolemizer = false]]
+
+lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
+by (metis rax)
+
+lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
+by (metisFT rax)
+
+declare [[metis_new_skolemizer]]
+
+lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
+by (metis rax)
+
+lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
+by (metisFT rax)
+
+lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
+       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
+       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
+       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
+by (metis rax)
+
+lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
+       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
+       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
+       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
+by (metisFT rax)
+
+
+text {* Definitional CNF for goal *}
+
+axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
+pax: "\<exists>b. \<forall>a. (p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b)"
+
+declare [[metis_new_skolemizer = false]]
+
+lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
+                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
+by (metis pax)
+
+lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
+                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
+by (metisFT pax)
+
+declare [[metis_new_skolemizer]]
+
+lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
+                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
+by (metis pax)
+
+lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
+                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
+by (metisFT pax)
+
+
+text {* New Skolemizer *}
+
+declare [[metis_new_skolemizer]]
+
+lemma
+  fixes x :: real
+  assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
+  shows "lim f \<le> x"
+by (metis 1 LIMSEQ_le_const2 fn_le)
+
+definition
+  bounded :: "'a::metric_space set \<Rightarrow> bool" where
+  "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
+
+lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
+by (metis bounded_def subset_eq)
+
+lemma
+  assumes a: "Quotient R Abs Rep"
+  shows "symp R"
+using a unfolding Quotient_def using sympI
+by metisFT
+
+lemma
+  "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
+   (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
+by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
+
+lemma ex_tl: "EX ys. tl ys = xs"
+using tl.simps(2) by fast
+
+lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
+by (metis ex_tl)
+
+end

--- a/src/HOL/Metis_Examples/Clausify.thy	Mon Jun 06 20:36:35 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,148 +0,0 @@
-(*  Title:      HOL/Metis_Examples/Clausify.thy
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Testing Metis's clausifier.
-*)
-
-theory Clausify
-imports Complex_Main
-begin
-
-(* FIXME: shouldn't need this *)
-declare [[unify_search_bound = 100]]
-declare [[unify_trace_bound = 100]]
-
-
-text {* Definitional CNF for facts *}
-
-declare [[meson_max_clauses = 10]]
-
-axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
-qax: "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
-
-declare [[metis_new_skolemizer = false]]
-
-lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
-by (metis qax)
-
-lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
-by (metisFT qax)
-
-lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
-by (metis qax)
-
-lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
-by (metisFT qax)
-
-declare [[metis_new_skolemizer]]
-
-lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
-by (metis qax)
-
-lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
-by (metisFT qax)
-
-lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
-by (metis qax)
-
-lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
-by (metisFT qax)
-
-declare [[meson_max_clauses = 60]]
-
-axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
-rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
-      (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
-      (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
-      (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
-
-declare [[metis_new_skolemizer = false]]
-
-lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
-by (metis rax)
-
-lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
-by (metisFT rax)
-
-declare [[metis_new_skolemizer]]
-
-lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
-by (metis rax)
-
-lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
-by (metisFT rax)
-
-lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
-       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
-       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
-       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
-by (metis rax)
-
-lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
-       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
-       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
-       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
-by (metisFT rax)
-
-
-text {* Definitional CNF for goal *}
-
-axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
-pax: "\<exists>b. \<forall>a. (p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b)"
-
-declare [[metis_new_skolemizer = false]]
-
-lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
-                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
-by (metis pax)
-
-lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
-                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
-by (metisFT pax)
-
-declare [[metis_new_skolemizer]]
-
-lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
-                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
-by (metis pax)
-
-lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
-                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
-by (metisFT pax)
-
-
-text {* New Skolemizer *}
-
-declare [[metis_new_skolemizer]]
-
-lemma
-  fixes x :: real
-  assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
-  shows "lim f \<le> x"
-by (metis 1 LIMSEQ_le_const2 fn_le)
-
-definition
-  bounded :: "'a::metric_space set \<Rightarrow> bool" where
-  "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
-
-lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
-by (metis bounded_def subset_eq)
-
-lemma
-  assumes a: "Quotient R Abs Rep"
-  shows "symp R"
-using a unfolding Quotient_def using sympI
-by metisFT
-
-lemma
-  "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
-   (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
-by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
-
-lemma ex_tl: "EX ys. tl ys = xs"
-using tl.simps(2) by fast
-
-lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
-by (metis ex_tl)
-
-end

--- a/src/HOL/Metis_Examples/HO_Reas.thy	Mon Jun 06 20:36:35 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-(*  Title:      HOL/Metis_Examples/HO_Reas.thy
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Testing Metis's and Sledgehammer's higher-order reasoning capabilities.
-*)
-
-theory HO_Reas
-imports Typings
-begin
-
-declare [[metis_new_skolemizer]]
-
-sledgehammer_params [prover = e, blocking, timeout = 10, preplay_timeout = 0]
-
-text {* Extensionality and set constants *}
-
-lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
-by simp
-
-definition inc :: "nat \<Rightarrow> nat" where
-"inc x = x + 1"
-
-lemma "inc \<noteq> (\<lambda>y. 0)"
-sledgehammer [expect = some] (inc_def plus_1_not_0)
-by (metis_eXhaust inc_def plus_1_not_0)
-
-lemma "inc = (\<lambda>y. y + 1)"
-sledgehammer [expect = some] (inc_def)
-by (metis_eXhaust inc_def)
-
-definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
-"add_swap = (\<lambda>x y. y + x)"
-
-lemma "add_swap m n = n + m"
-sledgehammer [expect = some] (add_swap_def)
-by (metis_eXhaust add_swap_def)
-
-definition "A = {xs\<Colon>'a list. True}"
-
-lemma "xs \<in> A"
-sledgehammer [expect = some]
-by (metis_eXhaust A_def Collect_def mem_def)
-
-definition "B (y::int) \<equiv> y \<le> 0"
-definition "C (y::int) \<equiv> y \<le> 1"
-
-lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1"
-by linarith
-
-lemma "B \<subseteq> C"
-sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
-by (metis_eXhaust B_def C_def int_le_0_imp_le_1 predicate1I)
-
-
-text {* Proxies for logical constants *}
-
-lemma "id (op =) x x"
-sledgehammer [type_sys = erased, expect = none] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = none] (id_apply) (* unfortunate *)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metisX id_apply)
-
-lemma "id True"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "\<not> id False"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "x = id True \<or> x = id False"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "id x = id True \<or> id x = id False"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
-sledgehammer [type_sys = erased, expect = none] ()
-sledgehammer [type_sys = poly_args, expect = none] ()
-sledgehammer [type_sys = poly_tags?, expect = some] ()
-sledgehammer [type_sys = poly_tags, expect = some] ()
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] ()
-sledgehammer [type_sys = mangled_tags?, expect = some] ()
-sledgehammer [type_sys = mangled_tags, expect = some] ()
-sledgehammer [type_sys = mangled_preds?, expect = some] ()
-sledgehammer [type_sys = mangled_preds, expect = some] ()
-by metisX
-
-lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "id (a \<and> b) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "id (a \<and> b) \<Longrightarrow> id b"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "id a \<Longrightarrow> id (a \<or> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "id b \<Longrightarrow> id (a \<or> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
-
-end

--- a/src/HOL/Metis_Examples/Message.thy	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -1,10 +1,12 @@
 (*  Title:      HOL/Metis_Examples/Message.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
-Testing Metis.
+Metis example featuring message authentication.
 *)
 
+header {* Metis Example Featuring Message Authentication *}
+
 theory Message
 imports Main
 begin
@@ -135,7 +137,7 @@
 lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
 by (unfold keysFor_def, auto)
 
-lemma keysFor_insert_Crypt [simp]: 
+lemma keysFor_insert_Crypt [simp]:
     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
 by (unfold keysFor_def, auto)
 
@@ -149,13 +151,13 @@
 subsection{*Inductive relation "parts"*}
 
 lemma MPair_parts:
-     "[| {|X,Y|} \<in> parts H;        
+     "[| {|X,Y|} \<in> parts H;
          [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
-by (blast dest: parts.Fst parts.Snd) 
+by (blast dest: parts.Fst parts.Snd)
 
 declare MPair_parts [elim!] parts.Body [dest!]
 text{*NB These two rules are UNSAFE in the formal sense, as they discard the
-     compound message.  They work well on THIS FILE.  
+     compound message.  They work well on THIS FILE.
   @{text MPair_parts} is left as SAFE because it speeds up proofs.
   The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
 
@@ -218,9 +220,9 @@
   NOTE: the UN versions are no longer used!*}
 
 
-text{*This allows @{text blast} to simplify occurrences of 
+text{*This allows @{text blast} to simplify occurrences of
   @{term "parts(G\<union>H)"} in the assumption.*}
-lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] 
+lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]
 declare in_parts_UnE [elim!]
 
 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
@@ -235,13 +237,13 @@
 by blast
 
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
-apply (rule iffI) 
+apply (rule iffI)
 apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
 apply (metis parts_idem parts_mono)
 done
 
 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
-by (blast dest: parts_mono); 
+by (blast dest: parts_mono);
 
 lemma parts_cut: "[|Y\<in> parts (insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
 by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
@@ -254,36 +256,36 @@
 
 lemma parts_insert_Agent [simp]:
      "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
-apply (rule parts_insert_eq_I) 
-apply (erule parts.induct, auto) 
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Nonce [simp]:
      "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
-apply (rule parts_insert_eq_I) 
-apply (erule parts.induct, auto) 
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Number [simp]:
      "parts (insert (Number N) H) = insert (Number N) (parts H)"
-apply (rule parts_insert_eq_I) 
-apply (erule parts.induct, auto) 
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Key [simp]:
      "parts (insert (Key K) H) = insert (Key K) (parts H)"
-apply (rule parts_insert_eq_I) 
-apply (erule parts.induct, auto) 
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Hash [simp]:
      "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
-apply (rule parts_insert_eq_I) 
-apply (erule parts.induct, auto) 
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Crypt [simp]:
-     "parts (insert (Crypt K X) H) =  
+     "parts (insert (Crypt K X) H) =
           insert (Crypt K X) (parts (insert X H))"
 apply (rule equalityI)
 apply (rule subsetI)
@@ -292,7 +294,7 @@
 done
 
 lemma parts_insert_MPair [simp]:
-     "parts (insert {|X,Y|} H) =  
+     "parts (insert {|X,Y|} H) =
           insert {|X,Y|} (parts (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
@@ -306,7 +308,7 @@
 done
 
 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
-apply (induct_tac "msg") 
+apply (induct_tac "msg")
 apply (simp_all add: parts_insert2)
 apply (metis Suc_n_not_le_n)
 apply (metis le_trans linorder_linear)
@@ -325,21 +327,21 @@
     Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
   | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
   | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
-  | Decrypt [dest]: 
+  | Decrypt [dest]:
              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
 
 
 text{*Monotonicity; Lemma 1 of Lowe's paper*}
 lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
 apply auto
-apply (erule analz.induct) 
-apply (auto dest: analz.Fst analz.Snd) 
+apply (erule analz.induct)
+apply (auto dest: analz.Fst analz.Snd)
 done
 
 text{*Making it safe speeds up proofs*}
 lemma MPair_analz [elim!]:
-     "[| {|X,Y|} \<in> analz H;        
-             [| X \<in> analz H; Y \<in> analz H |] ==> P   
+     "[| {|X,Y|} \<in> analz H;
+             [| X \<in> analz H; Y \<in> analz H |] ==> P
           |] ==> P"
 by (blast dest: analz.Fst analz.Snd)
 
@@ -376,7 +378,7 @@
 apply (erule analz.induct, blast+)
 done
 
-text{*Converse fails: we can analz more from the union than from the 
+text{*Converse fails: we can analz more from the union than from the
   separate parts, as a key in one might decrypt a message in the other*}
 lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
 by (intro Un_least analz_mono Un_upper1 Un_upper2)
@@ -390,39 +392,39 @@
 
 lemma analz_insert_Agent [simp]:
      "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
-apply (rule analz_insert_eq_I) 
-apply (erule analz.induct, auto) 
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Nonce [simp]:
      "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
-apply (rule analz_insert_eq_I) 
-apply (erule analz.induct, auto) 
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Number [simp]:
      "analz (insert (Number N) H) = insert (Number N) (analz H)"
-apply (rule analz_insert_eq_I) 
-apply (erule analz.induct, auto) 
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Hash [simp]:
      "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
-apply (rule analz_insert_eq_I) 
-apply (erule analz.induct, auto) 
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
 done
 
 text{*Can only pull out Keys if they are not needed to decrypt the rest*}
-lemma analz_insert_Key [simp]: 
-    "K \<notin> keysFor (analz H) ==>   
+lemma analz_insert_Key [simp]:
+    "K \<notin> keysFor (analz H) ==>
           analz (insert (Key K) H) = insert (Key K) (analz H)"
 apply (unfold keysFor_def)
-apply (rule analz_insert_eq_I) 
-apply (erule analz.induct, auto) 
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_MPair [simp]:
-     "analz (insert {|X,Y|} H) =  
+     "analz (insert {|X,Y|} H) =
           insert {|X,Y|} (analz (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
@@ -433,22 +435,22 @@
 
 text{*Can pull out enCrypted message if the Key is not known*}
 lemma analz_insert_Crypt:
-     "Key (invKey K) \<notin> analz H 
+     "Key (invKey K) \<notin> analz H
       ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
-apply (rule analz_insert_eq_I) 
-apply (erule analz.induct, auto) 
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
 
 done
 
-lemma lemma1: "Key (invKey K) \<in> analz H ==>   
-               analz (insert (Crypt K X) H) \<subseteq>  
-               insert (Crypt K X) (analz (insert X H))" 
+lemma lemma1: "Key (invKey K) \<in> analz H ==>
+               analz (insert (Crypt K X) H) \<subseteq>
+               insert (Crypt K X) (analz (insert X H))"
 apply (rule subsetI)
 apply (erule_tac x = x in analz.induct, auto)
 done
 
-lemma lemma2: "Key (invKey K) \<in> analz H ==>   
-               insert (Crypt K X) (analz (insert X H)) \<subseteq>  
+lemma lemma2: "Key (invKey K) \<in> analz H ==>
+               insert (Crypt K X) (analz (insert X H)) \<subseteq>
                analz (insert (Crypt K X) H)"
 apply auto
 apply (erule_tac x = x in analz.induct, auto)
@@ -456,26 +458,26 @@
 done
 
 lemma analz_insert_Decrypt:
-     "Key (invKey K) \<in> analz H ==>   
-               analz (insert (Crypt K X) H) =  
+     "Key (invKey K) \<in> analz H ==>
+               analz (insert (Crypt K X) H) =
                insert (Crypt K X) (analz (insert X H))"
 by (intro equalityI lemma1 lemma2)
 
 text{*Case analysis: either the message is secure, or it is not! Effective,
 but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
 @{text "split_tac"} does not cope with patterns such as @{term"analz (insert
-(Crypt K X) H)"} *} 
+(Crypt K X) H)"} *}
 lemma analz_Crypt_if [simp]:
-     "analz (insert (Crypt K X) H) =                 
-          (if (Key (invKey K) \<in> analz H)                 
-           then insert (Crypt K X) (analz (insert X H))  
+     "analz (insert (Crypt K X) H) =
+          (if (Key (invKey K) \<in> analz H)
+           then insert (Crypt K X) (analz (insert X H))
            else insert (Crypt K X) (analz H))"
 by (simp add: analz_insert_Crypt analz_insert_Decrypt)
 
 
 text{*This rule supposes "for the sake of argument" that we have the key.*}
 lemma analz_insert_Crypt_subset:
-     "analz (insert (Crypt K X) H) \<subseteq>   
+     "analz (insert (Crypt K X) H) \<subseteq>
            insert (Crypt K X) (analz (insert X H))"
 apply (rule subsetI)
 apply (erule analz.induct, auto)
@@ -498,8 +500,8 @@
 
 lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
 apply (rule iffI)
-apply (iprover intro: subset_trans analz_increasing)  
-apply (frule analz_mono, simp) 
+apply (iprover intro: subset_trans analz_increasing)
+apply (frule analz_mono, simp)
 done
 
 lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
@@ -525,7 +527,7 @@
 text{*A congruence rule for "analz" *}
 
 lemma analz_subset_cong:
-     "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
+     "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |]
       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
 apply simp
 apply (metis Un_absorb2 Un_commute Un_subset_iff Un_upper1 Un_upper2 analz_mono)
@@ -533,9 +535,9 @@
 
 
 lemma analz_cong:
-     "[| analz G = analz G'; analz H = analz H'  
+     "[| analz G = analz G'; analz H = analz H'
                |] ==> analz (G \<union> H) = analz (G' \<union> H')"
-by (intro equalityI analz_subset_cong, simp_all) 
+by (intro equalityI analz_subset_cong, simp_all)
 
 lemma analz_insert_cong:
      "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
@@ -579,9 +581,9 @@
 
 text{*Monotonicity*}
 lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
-  by (auto, erule synth.induct, auto)  
+  by (auto, erule synth.induct, auto)
 
-text{*NO @{text Agent_synth}, as any Agent name can be synthesized.  
+text{*NO @{text Agent_synth}, as any Agent name can be synthesized.
   The same holds for @{term Number}*}
 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
@@ -595,7 +597,7 @@
 
 subsubsection{*Unions *}
 
-text{*Converse fails: we can synth more from the union than from the 
+text{*Converse fails: we can synth more from the union than from the
   separate parts, building a compound message using elements of each.*}
 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
 by (intro Un_least synth_mono Un_upper1 Un_upper2)
@@ -613,8 +615,8 @@
 
 lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
 apply (rule iffI)
-apply (iprover intro: subset_trans synth_increasing)  
-apply (frule synth_mono, simp add: synth_idem) 
+apply (iprover intro: subset_trans synth_increasing)
+apply (frule synth_mono, simp add: synth_idem)
 done
 
 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
@@ -644,7 +646,7 @@
 by blast
 
 
-lemma keysFor_synth [simp]: 
+lemma keysFor_synth [simp]:
     "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
 by (unfold keysFor_def, blast)
 
@@ -706,7 +708,7 @@
 qed
 
 lemma Fake_parts_insert:
-     "X \<in> synth (analz H) ==>  
+     "X \<in> synth (analz H) ==>
       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
 proof -
   assume A1: "X \<in> synth (analz H)"
@@ -735,11 +737,11 @@
 qed
 
 lemma Fake_parts_insert_in_Un:
-     "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
+     "[|Z \<in> parts (insert X H);  X: synth (analz H)|]
       ==> Z \<in>  synth (analz H) \<union> parts H";
 by (blast dest: Fake_parts_insert [THEN subsetD, dest])
 
-declare analz_mono [intro] synth_mono [intro] 
+declare analz_mono [intro] synth_mono [intro]
 
 lemma Fake_analz_insert:
      "X \<in> synth (analz G) ==>
@@ -748,7 +750,7 @@
           analz_mono analz_synth_Un insert_absorb)
 
 lemma Fake_analz_insert_simpler:
-     "X \<in> synth (analz G) ==>  
+     "X \<in> synth (analz G) ==>
       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
 apply (rule subsetI)
 apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis_Examples/Proxies.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -0,0 +1,264 @@
+(*  Title:      HOL/Metis_Examples/Proxies.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Example that exercises Metis's and Sledgehammer's logical symbol proxies for
+rudimentary higher-order reasoning.
+*)
+
+header {*
+Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for
+Rudimentary Higher-Order Reasoning.
+*}
+
+theory Proxies
+imports Type_Encodings
+begin
+
+text {* Extensionality and set constants *}
+
+lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
+by simp
+
+definition inc :: "nat \<Rightarrow> nat" where
+"inc x = x + 1"
+
+lemma "inc \<noteq> (\<lambda>y. 0)"
+sledgehammer [expect = some] (inc_def plus_1_not_0)
+by (metis_eXhaust inc_def plus_1_not_0)
+
+lemma "inc = (\<lambda>y. y + 1)"
+sledgehammer [expect = some] (inc_def)
+by (metis_eXhaust inc_def)
+
+definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"add_swap = (\<lambda>x y. y + x)"
+
+lemma "add_swap m n = n + m"
+sledgehammer [expect = some] (add_swap_def)
+by (metis_eXhaust add_swap_def)
+
+definition "A = {xs\<Colon>'a list. True}"
+
+lemma "xs \<in> A"
+sledgehammer [expect = some]
+by (metis_eXhaust A_def Collect_def mem_def)
+
+definition "B (y::int) \<equiv> y \<le> 0"
+definition "C (y::int) \<equiv> y \<le> 1"
+
+lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1"
+by linarith
+
+lemma "B \<subseteq> C"
+sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
+by (metis_eXhaust B_def C_def int_le_0_imp_le_1 predicate1I)
+
+
+text {* Proxies for logical constants *}
+
+lemma "id (op =) x x"
+sledgehammer [type_sys = erased, expect = none] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = none] (id_apply) (* unfortunate *)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metisX id_apply)
+
+lemma "id True"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "\<not> id False"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "x = id True \<or> x = id False"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "id x = id True \<or> id x = id False"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
+sledgehammer [type_sys = erased, expect = none] ()
+sledgehammer [type_sys = poly_args, expect = none] ()
+sledgehammer [type_sys = poly_tags?, expect = some] ()
+sledgehammer [type_sys = poly_tags, expect = some] ()
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] ()
+sledgehammer [type_sys = mangled_tags?, expect = some] ()
+sledgehammer [type_sys = mangled_tags, expect = some] ()
+sledgehammer [type_sys = mangled_preds?, expect = some] ()
+sledgehammer [type_sys = mangled_preds, expect = some] ()
+by metisX
+
+lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "id (a \<and> b) \<Longrightarrow> id a"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "id (a \<and> b) \<Longrightarrow> id b"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "id a \<Longrightarrow> id (a \<or> b)"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "id b \<Longrightarrow> id (a \<or> b)"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
+sledgehammer [type_sys = erased, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis_eXhaust id_apply)
+
+end

--- a/src/HOL/Metis_Examples/ROOT.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Metis_Examples/ROOT.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -5,5 +5,5 @@
 Testing Metis and Sledgehammer.
 *)
 
-use_thys ["Abstraction", "BigO", "BT", "Clausify", "HO_Reas", "Message",
-          "Tarski", "TransClosure", "Typings", "set"];
+use_thys ["Abstraction", "Big_O", "Binary_Tree", "Clausification", "Message",
+          "Proxies", "Tarski", "Trans_Closure", "Sets"];

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis_Examples/Sets.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -0,0 +1,204 @@
+(*  Title:      HOL/Metis_Examples/Sets.thy
+    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Metis example featuring typed set theory.
+*)
+
+header {* Metis Example Featuring Typed Set Theory *}
+
+theory Sets
+imports Main
+begin
+
+declare [[metis_new_skolemizer]]
+
+lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
+               (S(x,y) | ~S(y,z) | Q(Z,Z))  &
+               (Q(X,y) | ~Q(y,Z) | S(X,X))"
+by metis
+
+lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
+by metis
+
+sledgehammer_params [isar_proof, isar_shrink_factor = 1]
+
+(*multiple versions of this example*)
+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)
+  { 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) }
+  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) }
+    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) }
+      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) }
+  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 "\<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) }
+    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) }
+      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 }
+  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
+qed
+
+sledgehammer_params [isar_proof, isar_shrink_factor = 2]
+
+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"
+    { 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) }
+      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) }
+    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) }
+  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) }
+  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) }
+  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) }
+    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
+qed
+
+sledgehammer_params [isar_proof, isar_shrink_factor = 3]
+
+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)
+  { 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) }
+  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 "(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)
+qed
+
+sledgehammer_params [isar_proof, isar_shrink_factor = 4]
+
+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 "\<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) }
+  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)
+qed
+
+sledgehammer_params [isar_proof, isar_shrink_factor = 1]
+
+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))"
+by (metis Un_least Un_upper1 Un_upper2 set_eq_subset)
+
+lemma "(X = Y \<inter> Z) = (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
+by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym)
+
+lemma fixedpoint: "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
+by metis
+
+lemma (* fixedpoint: *) "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
+proof -
+  assume "\<exists>!x\<Colon>'a. f (g x) = x"
+  thus "\<exists>!y\<Colon>'b. g (f y) = y" by metis
+qed
+
+lemma (* singleton_example_2: *)
+     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+by (metis Set.subsetI Union_upper insertCI set_eq_subset)
+
+lemma (* singleton_example_2: *)
+     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
+
+lemma singleton_example_2:
+     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+proof -
+  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)
+  thus "\<exists>z. S \<subseteq> {z}" by metis
+qed
+
+text {*
+  From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
+  293-314.
+*}
+
+(* Notes: (1) The numbering doesn't completely agree with the paper.
+   (2) We must rename set variables to avoid type clashes. *)
+lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))"
+      "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
+      "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
+      "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>B. a \<notin> B \<and> b \<in> B \<and> c \<notin> B"
+      "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
+      "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
+      "\<exists>A. a \<notin> A"
+      "(\<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 less_int_def singleton_iff)
+   apply (metis mem_def)
+  apply (metis mem_def)
+ apply (metis all_not_in_conv)
+by (metis pair_in_Id_conv)
+
+end

--- a/src/HOL/Metis_Examples/Tarski.thy	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -1,11 +1,11 @@
 (*  Title:      HOL/Metis_Examples/Tarski.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
-Testing Metis.
+Metis example featuring the full theorem of Tarski.
 *)
 
-header {* The Full Theorem of Tarski *}
+header {* Metis Example Featuring the Full Theorem of Tarski *}
 
 theory Tarski
 imports Main "~~/src/HOL/Library/FuncSet"
@@ -260,7 +260,7 @@
 by (simp add: dual_def)
 
 lemma (in PO) monotone_dual:
-     "monotone f (pset cl) (order cl) 
+     "monotone f (pset cl) (order cl)
      ==> monotone f (pset (dual cl)) (order(dual cl))"
 by (simp add: monotone_def dualA_iff dualr_iff)
 
@@ -436,7 +436,7 @@
 lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set"
 apply (simp del: dualA_iff)
 apply (simp)
-done 
+done
 
 declare (in CLF) CLF_set_def[simp del] CL_dualCL[simp del] monotone_dual[simp del]
           dualA_iff[simp del]
@@ -459,7 +459,7 @@
 
 (*never proved, 2007-01-22*)
 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_lubH_le_flubH" ]]
-  declare CL.lub_least[intro] CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] PO.transE[intro] PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] 
+  declare CL.lub_least[intro] CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] PO.transE[intro] PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro]
 lemma (in CLF) lubH_le_flubH:
      "H = {x. (x, f x) \<in> r & x \<in> A} ==> (lub H cl, f (lub H cl)) \<in> r"
 apply (rule lub_least, fast)
@@ -480,15 +480,15 @@
 apply (rule lub_upper, fast)
 apply assumption
 done
-  declare CL.lub_least[rule del] CLF.f_in_funcset[rule del] 
-          funcset_mem[rule del] CL.lub_in_lattice[rule del] 
-          PO.transE[rule del] PO.monotoneE[rule del] 
-          CLF.monotone_f[rule del] CL.lub_upper[rule del] 
+  declare CL.lub_least[rule del] CLF.f_in_funcset[rule del]
+          funcset_mem[rule del] CL.lub_in_lattice[rule del]
+          PO.transE[rule del] PO.monotoneE[rule del]
+          CLF.monotone_f[rule del] CL.lub_upper[rule del]
 
 (*never proved, 2007-01-22*)
 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_flubH_le_lubH" ]]
   declare CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro]
-       PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] 
+       PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro]
        CLF.lubH_le_flubH[simp]
 lemma (in CLF) flubH_le_lubH:
      "[|  H = {x. (x, f x) \<in> r & x \<in> A} |] ==> (f (lub H cl), lub H cl) \<in> r"
@@ -498,14 +498,14 @@
 apply (rule conjI)
 using [[ sledgehammer_problem_prefix = "Tarski__CLF_flubH_le_lubH_simpler" ]]
 (*??no longer terminates, with combinators
-apply (metis CO_refl_on lubH_le_flubH monotone_def monotone_f reflD1 reflD2) 
+apply (metis CO_refl_on lubH_le_flubH monotone_def monotone_f reflD1 reflD2)
 *)
 apply (metis CO_refl_on lubH_le_flubH monotoneE [OF monotone_f] refl_onD1 refl_onD2)
 apply (metis CO_refl_on lubH_le_flubH refl_onD2)
 done
-  declare CLF.f_in_funcset[rule del] funcset_mem[rule del] 
-          CL.lub_in_lattice[rule del] PO.monotoneE[rule del] 
-          CLF.monotone_f[rule del] CL.lub_upper[rule del] 
+  declare CLF.f_in_funcset[rule del] funcset_mem[rule del]
+          CL.lub_in_lattice[rule del] PO.monotoneE[rule del]
+          CLF.monotone_f[rule del] CL.lub_upper[rule del]
           CLF.lubH_le_flubH[simp del]
 
 
@@ -577,7 +577,7 @@
 
 subsection {* Tarski fixpoint theorem 1, first part *}
 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_T_thm_1_lub" ]]
-  declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro] 
+  declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro]
           CLF.fixf_le_lubH[simp] CLF.lubH_least_fixf[simp]
 lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \<in> r & x \<in> A} cl"
 (*sledgehammer;*)
@@ -585,7 +585,7 @@
 apply (simp add: P_def)
 apply (rule lubI)
 using [[ sledgehammer_problem_prefix = "Tarski__CLF_T_thm_1_lub_simpler" ]]
-apply (metis P_def fix_subset) 
+apply (metis P_def fix_subset)
 apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def)
 (*??no longer terminates, with combinators
 apply (metis P_def fix_def fixf_le_lubH)
@@ -594,13 +594,13 @@
 apply (simp add: fixf_le_lubH)
 apply (simp add: lubH_least_fixf)
 done
-  declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del] 
+  declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del]
           CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del]
 
 
 (*never proved, 2007-01-22*)
 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_glbH_is_fixp" ]]
-  declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro] 
+  declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro]
           PO.dualPO[intro] CL.CL_dualCL[intro] PO.dualr_iff[simp]
 lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \<in> r & x \<in> A} ==> glb H cl \<in> P"
   -- {* Tarski for glb *}
@@ -618,7 +618,7 @@
 apply (rule CLF_dual)
 apply (simp add: dualr_iff dualA_iff)
 done
-  declare glb_dual_lub[simp del] PO.dualA_iff[rule del] CLF.lubH_is_fixp[rule del] 
+  declare glb_dual_lub[simp del] PO.dualA_iff[rule del] CLF.lubH_is_fixp[rule del]
           PO.dualPO[rule del] CL.CL_dualCL[rule del] PO.dualr_iff[simp del]
 
 
@@ -645,11 +645,11 @@
   declare (in CLF) CO_refl_on[simp del]  refl_on_def [simp del]
 
 declare [[ sledgehammer_problem_prefix = "Tarski__interval_subset" ]]
-  declare (in CLF) rel_imp_elem[intro] 
+  declare (in CLF) rel_imp_elem[intro]
   declare interval_def [simp]
 lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
 by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq)
-  declare (in CLF) rel_imp_elem[rule del] 
+  declare (in CLF) rel_imp_elem[rule del]
   declare interval_def [simp del]
 
 
@@ -682,7 +682,7 @@
 declare [[ sledgehammer_problem_prefix = "Tarski__L_in_interval" ]]  (*ALL THEOREMS*)
 lemma (in CLF) L_in_interval:
      "[| a \<in> A; b \<in> A; S \<subseteq> interval r a b;
-         S \<noteq> {}; isLub S cl L; interval r a b \<noteq> {} |] ==> L \<in> interval r a b" 
+         S \<noteq> {}; isLub S cl L; interval r a b \<noteq> {} |] ==> L \<in> interval r a b"
 (*WON'T TERMINATE
 apply (metis CO_trans intervalI interval_lemma1 interval_lemma2 isLub_least isLub_upper subset_empty subset_iff trans_def)
 *)
@@ -807,7 +807,7 @@
 (*sledgehammer; *)
 apply (simp add: Bot_def least_def)
 apply (rule_tac a="glb A cl" in someI2)
-apply (simp_all add: glb_in_lattice glb_lower 
+apply (simp_all add: glb_in_lattice glb_lower
                      r_def [symmetric] A_def [symmetric])
 done
 
@@ -827,14 +827,14 @@
 apply (simp add: Top_def greatest_def)
 apply (rule_tac a="lub A cl" in someI2)
 apply (rule someI2)
-apply (simp_all add: lub_in_lattice lub_upper 
+apply (simp_all add: lub_in_lattice lub_upper
                      r_def [symmetric] A_def [symmetric])
 done
 
 (*never proved, 2007-01-22*)
-declare [[ sledgehammer_problem_prefix = "Tarski__Bot_prop" ]]  (*ALL THEOREMS*) 
+declare [[ sledgehammer_problem_prefix = "Tarski__Bot_prop" ]]  (*ALL THEOREMS*)
 lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r"
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (simp add: Bot_dual_Top r_def)
 apply (rule dualr_iff [THEN subst])
 apply (simp add: CLF.Top_prop [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro]
@@ -842,12 +842,12 @@
 done
 
 declare [[ sledgehammer_problem_prefix = "Tarski__Bot_in_lattice" ]]  (*ALL THEOREMS*)
-lemma (in CLF) Top_intv_not_empty: "x \<in> A  ==> interval r x (Top cl) \<noteq> {}" 
+lemma (in CLF) Top_intv_not_empty: "x \<in> A  ==> interval r x (Top cl) \<noteq> {}"
 apply (metis Top_in_lattice Top_prop empty_iff intervalI reflE)
 done
 
 declare [[ sledgehammer_problem_prefix = "Tarski__Bot_intv_not_empty" ]]  (*ALL THEOREMS*)
-lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}" 
+lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}"
 apply (metis Bot_prop ex_in_conv intervalI reflE rel_imp_elem)
 done
 
@@ -862,7 +862,7 @@
   declare (in Tarski) P_def[simp] Y_ss [simp]
   declare fix_subset [intro] subset_trans [intro]
 lemma (in Tarski) Y_subset_A: "Y \<subseteq> A"
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (rule subset_trans [OF _ fix_subset])
 apply (rule Y_ss [simplified P_def])
 done
@@ -876,7 +876,7 @@
 (*never proved, 2007-01-22*)
 declare [[ sledgehammer_problem_prefix = "Tarski__lubY_le_flubY" ]]  (*ALL THEOREMS*)
 lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \<in> r"
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (rule lub_least)
 apply (rule Y_subset_A)
 apply (rule f_in_funcset [THEN funcset_mem])
@@ -900,7 +900,7 @@
 (*first proved 2007-01-25 after relaxing relevance*)
 declare [[ sledgehammer_problem_prefix = "Tarski__intY1_subset" ]]  (*ALL THEOREMS*)
 lemma (in Tarski) intY1_subset: "intY1 \<subseteq> A"
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (unfold intY1_def)
 apply (rule interval_subset)
 apply (rule lubY_in_A)
@@ -912,7 +912,7 @@
 (*never proved, 2007-01-22*)
 declare [[ sledgehammer_problem_prefix = "Tarski__intY1_f_closed" ]]  (*ALL THEOREMS*)
 lemma (in Tarski) intY1_f_closed: "x \<in> intY1 \<Longrightarrow> f x \<in> intY1"
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (simp add: intY1_def  interval_def)
 apply (rule conjI)
 apply (rule transE)
@@ -925,7 +925,7 @@
 apply (rule lubY_in_A)
 apply (simp add: intY1_def interval_def  intY1_elem)
 apply (simp add: intY1_def  interval_def)
--- {* @{text "(f x, Top cl) \<in> r"} *} 
+-- {* @{text "(f x, Top cl) \<in> r"} *}
 apply (rule Top_prop)
 apply (rule f_in_funcset [THEN funcset_mem])
 apply (simp add: intY1_def interval_def  intY1_elem)
@@ -949,7 +949,7 @@
 declare [[ sledgehammer_problem_prefix = "Tarski__intY1_is_cl" ]]  (*ALL THEOREMS*)
 lemma (in Tarski) intY1_is_cl:
     "(| pset = intY1, order = induced intY1 r |) \<in> CompleteLattice"
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (unfold intY1_def)
 apply (rule interv_is_compl_latt)
 apply (rule lubY_in_A)
@@ -961,7 +961,7 @@
 (*never proved, 2007-01-22*)
 declare [[ sledgehammer_problem_prefix = "Tarski__v_in_P" ]]  (*ALL THEOREMS*)
 lemma (in Tarski) v_in_P: "v \<in> P"
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (unfold P_def)
 apply (rule_tac A = "intY1" in fixf_subset)
 apply (rule intY1_subset)
@@ -985,7 +985,7 @@
 
 declare [[ sledgehammer_problem_prefix = "Tarski__fz_in_int_rel" ]]  (*ALL THEOREMS*)
 lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |]
-      ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r" 
+      ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r"
 apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval)
 done
 
@@ -998,7 +998,7 @@
 -- {* @{text "v \<in> P"} *}
 apply (simp add: v_in_P)
 apply (rule conjI)
-(*sledgehammer*) 
+(*sledgehammer*)
 -- {* @{text v} is lub *}
 -- {* @{text "1. \<forall>y:Y. (y, v) \<in> induced P r"} *}
 apply (rule ballI)
@@ -1021,12 +1021,12 @@
 apply (unfold v_def)
 (*never proved, 2007-01-22*)
 using [[ sledgehammer_problem_prefix = "Tarski__tarski_full_lemma_simpler" ]]
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (rule indE)
 apply (rule_tac [2] intY1_subset)
 (*never proved, 2007-01-22*)
 using [[ sledgehammer_problem_prefix = "Tarski__tarski_full_lemma_simplest" ]]
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified])
   apply (simp add: CL_imp_PO intY1_is_cl)
  apply force
@@ -1049,12 +1049,12 @@
                CompleteLatticeI_simp [intro]
 theorem (in CLF) Tarski_full:
      "(| pset = P, order = induced P r|) \<in> CompleteLattice"
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (rule CompleteLatticeI_simp)
 apply (rule fixf_po, clarify)
 (*never proved, 2007-01-22*)
 using [[ sledgehammer_problem_prefix = "Tarski__Tarski_full_simpler" ]]
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (simp add: P_def A_def r_def)
 apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro,
   OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl)

--- a/src/HOL/Metis_Examples/TransClosure.thy	Mon Jun 06 20:36:35 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(*  Title:      HOL/Metis_Examples/TransClosure.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Testing Metis.
-*)
-
-theory TransClosure
-imports Main
-begin
-
-declare [[metis_new_skolemizer]]
-
-type_synonym addr = nat
-
-datatype val
-  = Unit        -- "dummy result value of void expressions"
-  | Null        -- "null reference"
-  | Bool bool   -- "Boolean value"
-  | Intg int    -- "integer value"
-  | Addr addr   -- "addresses of objects in the heap"
-
-consts R :: "(addr \<times> addr) set"
-
-consts f :: "addr \<Rightarrow> val"
-
-lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk>
-       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-(* sledgehammer *)
-proof -
-  assume A1: "f c = Intg x"
-  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
-  assume A3: "(a, b) \<in> R\<^sup>*"
-  assume A4: "(b, c) \<in> R\<^sup>*"
-  have F1: "f c \<noteq> f b" using A2 A1 by metis
-  have F2: "\<forall>u. (b, u) \<in> R \<longrightarrow> (a, u) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
-  have F3: "\<exists>x. (b, x b c R) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
-  have "c \<noteq> b" using F1 by metis
-  hence "\<exists>u. (b, u) \<in> R" using F3 by metis
-  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis
-qed
-
-lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
-       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-(* sledgehammer [isar_proof, isar_shrink_factor = 2] *)
-proof -
-  assume A1: "f c = Intg x"
-  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
-  assume A3: "(a, b) \<in> R\<^sup>*"
-  assume A4: "(b, c) \<in> R\<^sup>*"
-  have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def)
-  hence F1: "(a, b) \<in> R\<^sup>*" by (metis mem_def)
-  have "b \<noteq> c" using A1 A2 by metis
-  hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
-  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6))
-qed
-
-lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk>
-       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-apply (erule_tac x = b in converse_rtranclE)
- apply metis
-by (metis transitive_closure_trans(6))
-
-end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -0,0 +1,66 @@
+(*  Title:      HOL/Metis_Examples/Trans_Closure.thy
+    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Metis example featuring the transitive closure.
+*)
+
+header {* Metis Example Featuring the Transitive Closure *}
+
+theory Trans_Closure
+imports Main
+begin
+
+declare [[metis_new_skolemizer]]
+
+type_synonym addr = nat
+
+datatype val
+  = Unit        -- "dummy result value of void expressions"
+  | Null        -- "null reference"
+  | Bool bool   -- "Boolean value"
+  | Intg int    -- "integer value"
+  | Addr addr   -- "addresses of objects in the heap"
+
+consts R :: "(addr \<times> addr) set"
+
+consts f :: "addr \<Rightarrow> val"
+
+lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk>
+       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
+(* sledgehammer *)
+proof -
+  assume A1: "f c = Intg x"
+  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
+  assume A3: "(a, b) \<in> R\<^sup>*"
+  assume A4: "(b, c) \<in> R\<^sup>*"
+  have F1: "f c \<noteq> f b" using A2 A1 by metis
+  have F2: "\<forall>u. (b, u) \<in> R \<longrightarrow> (a, u) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
+  have F3: "\<exists>x. (b, x b c R) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
+  have "c \<noteq> b" using F1 by metis
+  hence "\<exists>u. (b, u) \<in> R" using F3 by metis
+  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis
+qed
+
+lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
+       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
+(* sledgehammer [isar_proof, isar_shrink_factor = 2] *)
+proof -
+  assume A1: "f c = Intg x"
+  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
+  assume A3: "(a, b) \<in> R\<^sup>*"
+  assume A4: "(b, c) \<in> R\<^sup>*"
+  have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def)
+  hence F1: "(a, b) \<in> R\<^sup>*" by (metis mem_def)
+  have "b \<noteq> c" using A1 A2 by metis
+  hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
+  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6))
+qed
+
+lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk>
+       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
+apply (erule_tac x = b in converse_rtranclE)
+ apply metis
+by (metis transitive_closure_trans(6))
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -0,0 +1,86 @@
+(*  Title:      HOL/Metis_Examples/Type_Encodings.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Example that exercises Metis's (and hence Sledgehammer's) type encodings.
+*)
+
+header {*
+Example that Exercises Metis's (and Hence Sledgehammer's) Type Encodings
+*}
+
+theory Type_Encodings
+imports Main
+begin
+
+declare [[metis_new_skolemizer]]
+
+sledgehammer_params [prover = e, blocking, timeout = 10, preplay_timeout = 0]
+
+
+text {* Setup for testing Metis exhaustively *}
+
+lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
+
+ML {*
+open ATP_Translate
+
+val polymorphisms = [Polymorphic, Monomorphic, Mangled_Monomorphic]
+val levels =
+  [All_Types, Nonmonotonic_Types, Finite_Types, Const_Arg_Types, No_Types]
+val heaviness = [Heavyweight, Lightweight]
+val type_syss =
+  (levels |> map Simple_Types) @
+  (map_product pair levels heaviness
+   (* The following two families of type systems are too incomplete for our
+      tests. *)
+   |> remove (op =) (Nonmonotonic_Types, Heavyweight)
+   |> remove (op =) (Finite_Types, Heavyweight)
+   |> map_product pair polymorphisms
+   |> map_product (fn constr => fn (poly, (level, heaviness)) =>
+                      constr (poly, level, heaviness))
+                  [Preds, Tags])
+
+fun metis_eXhaust_tac ctxt ths =
+  let
+    fun tac [] st = all_tac st
+      | tac (type_sys :: type_syss) st =
+        st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *)
+           |> ((if null type_syss then all_tac else rtac @{thm fork} 1)
+               THEN Metis_Tactics.metisX_tac ctxt (SOME type_sys) ths 1
+               THEN COND (has_fewer_prems 2) all_tac no_tac
+               THEN tac type_syss)
+  in tac end
+*}
+
+method_setup metis_eXhaust = {*
+  Attrib.thms >>
+    (fn ths => fn ctxt => SIMPLE_METHOD (metis_eXhaust_tac ctxt ths type_syss))
+*} "exhaustively run the new Metis with all type encodings"
+
+
+text {* Miscellaneous tests *}
+
+lemma "x = y \<Longrightarrow> y = x"
+by metis_eXhaust
+
+lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
+by (metis_eXhaust last.simps)
+
+lemma "map Suc [0] = [Suc 0]"
+by (metis_eXhaust map.simps)
+
+lemma "map Suc [1 + 1] = [Suc 2]"
+by (metis_eXhaust map.simps nat_1_add_1)
+
+lemma "map Suc [2] = [Suc (1 + 1)]"
+by (metis_eXhaust map.simps nat_1_add_1)
+
+definition "null xs = (xs = [])"
+
+lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
+by (metis_eXhaust null_def)
+
+lemma "(0::nat) + 0 = 0"
+by (metis_eXhaust arithmetic_simps(38))
+
+end

--- a/src/HOL/Metis_Examples/Typings.thy	Mon Jun 06 20:36:35 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,77 +0,0 @@
-(*  Title:      HOL/Metis_Examples/Typings.thy
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Testing the new Metis's (and hence Sledgehammer's) type translations.
-*)
-
-theory Typings
-imports Main
-begin
-
-text {* Setup for testing Metis exhaustively *}
-
-lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
-
-ML {*
-open ATP_Translate
-
-val polymorphisms = [Polymorphic, Monomorphic, Mangled_Monomorphic]
-val levels =
-  [All_Types, Nonmonotonic_Types, Finite_Types, Const_Arg_Types, No_Types]
-val heaviness = [Heavyweight, Lightweight]
-val type_syss =
-  (levels |> map Simple_Types) @
-  (map_product pair levels heaviness
-   (* The following two families of type systems are too incomplete for our
-      tests. *)
-   |> remove (op =) (Nonmonotonic_Types, Heavyweight)
-   |> remove (op =) (Finite_Types, Heavyweight)
-   |> map_product pair polymorphisms
-   |> map_product (fn constr => fn (poly, (level, heaviness)) =>
-                      constr (poly, level, heaviness))
-                  [Preds, Tags])
-
-fun metis_eXhaust_tac ctxt ths =
-  let
-    fun tac [] st = all_tac st
-      | tac (type_sys :: type_syss) st =
-        st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *)
-           |> ((if null type_syss then all_tac else rtac @{thm fork} 1)
-               THEN Metis_Tactics.metisX_tac ctxt (SOME type_sys) ths 1
-               THEN COND (has_fewer_prems 2) all_tac no_tac
-               THEN tac type_syss)
-  in tac end
-*}
-
-method_setup metis_eXhaust = {*
-  Attrib.thms >>
-    (fn ths => fn ctxt => SIMPLE_METHOD (metis_eXhaust_tac ctxt ths type_syss))
-*} "exhaustively run the new Metis with all type encodings"
-
-
-text {* Metis tests *}
-
-lemma "x = y \<Longrightarrow> y = x"
-by metis_eXhaust
-
-lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
-by (metis_eXhaust last.simps)
-
-lemma "map Suc [0] = [Suc 0]"
-by (metis_eXhaust map.simps)
-
-lemma "map Suc [1 + 1] = [Suc 2]"
-by (metis_eXhaust map.simps nat_1_add_1)
-
-lemma "map Suc [2] = [Suc (1 + 1)]"
-by (metis_eXhaust map.simps nat_1_add_1)
-
-definition "null xs = (xs = [])"
-
-lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
-by (metis_eXhaust null_def)
-
-lemma "(0::nat) + 0 = 0"
-by (metis_eXhaust arithmetic_simps(38))
-
-end

--- a/src/HOL/Metis_Examples/set.thy	Mon Jun 06 20:36:35 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,202 +0,0 @@
-(*  Title:      HOL/Metis_Examples/set.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Testing Metis.
-*)
-
-theory set
-imports Main
-begin
-
-declare [[metis_new_skolemizer]]
-
-lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
-               (S(x,y) | ~S(y,z) | Q(Z,Z))  &
-               (Q(X,y) | ~Q(y,Z) | S(X,X))" 
-by metis
-
-lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
-by metis
-
-sledgehammer_params [isar_proof, isar_shrink_factor = 1]
-
-(*multiple versions of this example*)
-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)
-  { 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) }
-  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) }
-    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) }
-      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) }
-  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 "\<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) }
-    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) }
-      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 }
-  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
-qed
-
-sledgehammer_params [isar_proof, isar_shrink_factor = 2]
-
-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"
-    { 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) }
-      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) }
-    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) }
-  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) }
-  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) }
-  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) }
-    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
-qed
-
-sledgehammer_params [isar_proof, isar_shrink_factor = 3]
-
-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)
-  { 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) }
-  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 "(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)
-qed
-
-sledgehammer_params [isar_proof, isar_shrink_factor = 4]
-
-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 "\<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) }
-  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)
-qed
-
-sledgehammer_params [isar_proof, isar_shrink_factor = 1]
-
-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))"
-by (metis Un_least Un_upper1 Un_upper2 set_eq_subset)
-
-lemma "(X = Y \<inter> Z) = (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
-by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym)
-
-lemma fixedpoint: "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
-by metis
-
-lemma (* fixedpoint: *) "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
-proof -
-  assume "\<exists>!x\<Colon>'a. f (g x) = x"
-  thus "\<exists>!y\<Colon>'b. g (f y) = y" by metis
-qed
-
-lemma (* singleton_example_2: *)
-     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-by (metis Set.subsetI Union_upper insertCI set_eq_subset)
-
-lemma (* singleton_example_2: *)
-     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
-
-lemma singleton_example_2:
-     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-proof -
-  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)
-  thus "\<exists>z. S \<subseteq> {z}" by metis
-qed
-
-text {*
-  From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
-  293-314.
-*}
-
-(* Notes: (1) The numbering doesn't completely agree with the paper.
-   (2) We must rename set variables to avoid type clashes. *)
-lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))"
-      "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
-      "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
-      "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>B. a \<notin> B \<and> b \<in> B \<and> c \<notin> B"
-      "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
-      "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
-      "\<exists>A. a \<notin> A"
-      "(\<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 less_int_def singleton_iff)
-   apply (metis mem_def)
-  apply (metis mem_def)
- apply (metis all_not_in_conv)
-by (metis pair_in_Id_conv)
-
-end