# HG changeset patch
# User paulson
# Date 1182425013 -7200
# Node ID dd874e6a32824567b37f432c262ea4d3903b0e58
# Parent  020381339d8771663f5668af1bda0bb06d0b185b
integration of Metis prover

diff -r 020381339d87 -r dd874e6a3282 CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Jun 21 12:01:27 2007 +0200
+++ b/CONTRIBUTORS	Thu Jun 21 13:23:33 2007 +0200
@@ -10,6 +10,12 @@
 * June 2007: Amine Chaieb, TUM
   Semiring normalization and Groebner Bases
 
+* June 2007: Joe Hurd, Oxford
+  Metis theorem-prover
+
+* 2006/2007: Kong W. Susanto, Cambridge
+  HOL: Metis prover integration.
+
 * 2006/2007: Florian Haftmann, TUM
   Pure: generic code generator framework.
   Pure: class package.
diff -r 020381339d87 -r dd874e6a3282 NEWS
--- a/NEWS	Thu Jun 21 12:01:27 2007 +0200
+++ b/NEWS	Thu Jun 21 13:23:33 2007 +0200
@@ -541,6 +541,13 @@
 
 *** HOL ***
 
+* Method "metis" proves goals by applying the Metis general-purpose resolution prover.
+  Examples are in the directory MetisExamples.
+  
+* Command "sledgehammer" invokes external automatic theorem provers as background processes.
+  It generates calls to the "metis" method if successful. These can be pasted into the proof.
+  Users do not have to wait for the automatic provers to return.
+
 * IntDef: The constant "int :: nat => int" has been removed; now
   "int" is an abbreviation for "of_nat :: nat => int". Potential
   INCOMPATIBILITY due to differences in default simp rules:
diff -r 020381339d87 -r dd874e6a3282 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jun 21 12:01:27 2007 +0200
+++ b/src/HOL/IsaMakefile	Thu Jun 21 13:23:33 2007 +0200
@@ -27,6 +27,7 @@
   HOL-Isar_examples \
   HOL-Lambda \
   HOL-Lattice \
+  HOL-MetisExamples \
   HOL-MicroJava \
   HOL-Modelcheck \
   HOL-NanoJava \
@@ -390,6 +391,18 @@
 	@$(ISATOOL) usedir -g true $(OUT)/HOL HoareParallel
 
 
+## HOL-MetisExamples
+
+HOL-MetisExamples: HOL $(LOG)/HOL-MetisExamples.gz
+
+$(LOG)/HOL-MetisExamples.gz: $(OUT)/HOL \
+  MetisExamples/ROOT.ML \
+  MetisExamples/Abstraction.thy MetisExamples/BigO.thy MetisExamples/BT.thy \
+  MetisExamples/Message.thy MetisExamples/Tarski.thy MetisExamples/TransClosure.thy \
+  MetisExamples/set.thy
+	@$(ISATOOL) usedir -g true $(OUT)/HOL MetisExamples
+
+
 ## HOL-Algebra
 
 HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
diff -r 020381339d87 -r dd874e6a3282 src/HOL/MetisExamples/Abstraction.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MetisExamples/Abstraction.thy	Thu Jun 21 13:23:33 2007 +0200
@@ -0,0 +1,248 @@
+(*  Title:      HOL/MetisExamples/Abstraction.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Testing the metis method
+*)
+
+theory Abstraction imports FuncSet
+begin
+
+(*For Christoph Benzmueller*)
+lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))";
+  by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2)
+
+(*this is a theorem, but we can't prove it unless ext is applied explicitly
+lemma "(op=) = (%x y. y=x)"
+*)
+
+consts
+  monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
+  pset  :: "'a set => 'a set"
+  order :: "'a set => ('a * 'a) set"
+
+ML{*ResAtp.problem_name := "Abstraction__Collect_triv"*}
+lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
+proof (neg_clausify)
+assume 0: "(a\<Colon>'a\<Colon>type) \<in> Collect (P\<Colon>'a\<Colon>type \<Rightarrow> bool)"
+assume 1: "\<not> (P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
+have 2: "(P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
+  by (metis CollectD 0)
+show "False"
+  by (metis 2 1)
+qed
+
+lemma Collect_triv: "a \<in> {x. P x} ==> P a"
+by (metis member_Collect_eq member_def)
+
+
+ML{*ResAtp.problem_name := "Abstraction__Collect_mp"*}
+lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
+  by (metis CollectI Collect_imp_eq ComplD UnE memberI member_Collect_eq);
+  --{*34 secs*}
+
+ML{*ResAtp.problem_name := "Abstraction__Sigma_triv"*}
+lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
+proof (neg_clausify)
+assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type) \<in> Sigma (A\<Colon>'a\<Colon>type set) (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set)"
+assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> (b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) a"
+have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
+  by (metis SigmaD1 0)
+have 3: "(b\<Colon>'b\<Colon>type) \<in> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
+  by (metis SigmaD2 0)
+have 4: "(b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
+  by (metis 1 2)
+show "False"
+  by (metis 3 4)
+qed
+
+lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
+by (metis SigmaD1 SigmaD2)
+
+ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect"*}
+lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
+(*???metis cannot prove this
+by (metis CollectD SigmaD1 SigmaD2 UN_eq)
+Also, UN_eq is unnecessary*)
+by (meson CollectD SigmaD1 SigmaD2)
+
+
+
+(*single-step*)
+lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
+proof (neg_clausify)
+assume 0: "(a, b) \<in> Sigma A (llabs_subgoal_1 f)"
+assume 1: "\<And>f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)"
+assume 2: "a \<notin> A \<or> a \<noteq> f b"
+have 3: "a \<in> A"
+  by (metis SigmaD1 0)
+have 4: "b \<in> llabs_subgoal_1 f a"
+  by (metis SigmaD2 0)
+have 5: "\<And>X1 X2. X2 -` {X1} = llabs_subgoal_1 X2 X1"
+  by (metis 1 vimage_Collect_eq singleton_conv2)
+have 6: "\<And>X1 X2 X3. X1 X2 = X3 \<or> X2 \<notin> llabs_subgoal_1 X1 X3"
+  by (metis vimage_singleton_eq 5)
+have 7: "f b \<noteq> a"
+  by (metis 2 3)
+have 8: "f b = a"
+  by (metis 6 4)
+show "False"
+  by (metis 8 7)
+qed finish_clausify
+
+
+ML{*ResAtp.problem_name := "Abstraction__CLF_eq_in_pp"*}
+lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
+apply (metis Collect_mem_eq SigmaD2);
+done
+
+lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"proof (neg_clausify)
+assume 0: "(cl, f) \<in> CLF"
+assume 1: "CLF = Sigma CL llabs_subgoal_1"
+assume 2: "\<And>cl. llabs_subgoal_1 cl =
+     Collect (llabs_Predicate_XRangeP_def_2_ op \<in> (pset cl))"
+assume 3: "f \<notin> pset cl"
+show "False"
+  by (metis 0 1 SigmaD2 3 2 Collect_mem_eq)
+qed finish_clausify (*ugly hack: combinators??*)
+
+ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*}
+lemma
+    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
+    f \<in> pset cl \<rightarrow> pset cl"
+apply (metis Collect_mem_eq SigmaD2);
+done
+
+lemma
+    "(cl,f) \<in> (SIGMA cl::'a set : CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
+    f \<in> pset cl \<rightarrow> pset cl" 
+proof (neg_clausify)
+assume 0: "(cl, f) \<in> Sigma CL llabs_subgoal_1"
+assume 1: "\<And>cl. llabs_subgoal_1 cl =
+     Collect
+      (llabs_Predicate_XRangeP_def_2_ op \<in> (Pi (pset cl) (COMBK (pset cl))))"
+assume 2: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
+show "False"
+  by (metis Collect_mem_eq 1 2 SigmaD2 0 member2_def)
+qed finish_clausify
+    (*Hack to prevent the "Additional hypotheses" error*)
+
+ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*}
+lemma
+    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
+   f \<in> pset cl \<inter> cl"
+by (metis Collect_mem_eq SigmaD2)
+
+ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*}
+lemma
+    "(cl,f) \<in> (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
+
+ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Int"*}
+lemma "(cl,f) \<in> CLF ==> 
+   CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
+   f \<in> pset cl \<inter> cl"
+by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)
+  --{*@{text Int_def} is redundant}
+
+ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*}
+lemma "(cl,f) \<in> CLF ==> 
+   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
+   f \<in> pset cl \<inter> cl"
+by (metis Collect_mem_eq Int_commute SigmaD2)
+
+ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*}
+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 (metis Collect_mem_eq SigmaD2 subsetD)
+
+ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*}
+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 (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)
+
+ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*}
+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
+
+ML{*ResAtp.problem_name := "Abstraction__map_eq_zipA"*}
+lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
+apply (induct xs)
+(*sledgehammer*)  
+apply auto
+done
+
+ML{*ResAtp.problem_name := "Abstraction__map_eq_zipB"*}
+lemma "map (%w. (w -> w, w \<times> w)) xs = 
+       zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
+apply (induct xs)
+(*sledgehammer*)  
+apply auto
+done
+
+ML{*ResAtp.problem_name := "Abstraction__image_evenA"*}
+lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)";
+(*sledgehammer*)  
+by auto
+
+ML{*ResAtp.problem_name := "Abstraction__image_evenB"*}
+lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A 
+       ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
+(*sledgehammer*)  
+by auto
+
+ML{*ResAtp.problem_name := "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)" 
+(*sledgehammer*)  
+by auto
+
+ML{*ResAtp.problem_name := "Abstraction__image_TimesA"*}
+lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
+(*sledgehammer*) 
+apply (rule equalityI)
+(***Even the two inclusions are far too difficult
+ML{*ResAtp.problem_name := "Abstraction__image_TimesA_simpler"*}
+***)
+apply (rule subsetI)
+apply (erule imageE)
+(*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*)
+apply (erule ssubst)
+apply (erule SigmaE)
+(*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*)
+apply (erule ssubst)
+apply (subst split_conv)
+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: );
+done
+
+(*Given the difficulty of the previous problem, these two are probably
+impossible*)
+
+ML{*ResAtp.problem_name := "Abstraction__image_TimesB"*}
+lemma image_TimesB:
+    "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)" 
+(*sledgehammer*) 
+by force
+
+ML{*ResAtp.problem_name := "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)" 
+(*sledgehammer*) 
+by auto
+
+end
diff -r 020381339d87 -r dd874e6a3282 src/HOL/MetisExamples/BT.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MetisExamples/BT.thy	Thu Jun 21 13:23:33 2007 +0200
@@ -0,0 +1,242 @@
+(*  Title:      HOL/MetisTest/BT.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Testing the metis method
+*)
+
+header {* Binary trees *}
+
+theory BT imports Main begin
+
+
+datatype 'a bt =
+    Lf
+  | Br 'a  "'a bt"  "'a bt"
+
+consts
+  n_nodes   :: "'a bt => nat"
+  n_leaves  :: "'a bt => nat"
+  depth     :: "'a bt => nat"
+  reflect   :: "'a bt => 'a bt"
+  bt_map    :: "('a => 'b) => ('a bt => 'b bt)"
+  preorder  :: "'a bt => 'a list"
+  inorder   :: "'a bt => 'a list"
+  postorder :: "'a bt => 'a list"
+  appnd    :: "'a bt => 'a bt => 'a bt"
+
+primrec
+  "n_nodes Lf = 0"
+  "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
+
+primrec
+  "n_leaves Lf = Suc 0"
+  "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
+
+primrec
+  "depth Lf = 0"
+  "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
+
+primrec
+  "reflect Lf = Lf"
+  "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
+
+primrec
+  "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 Lf = []"
+  "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
+
+primrec
+  "inorder Lf = []"
+  "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
+
+primrec
+  "postorder Lf = []"
+  "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
+
+primrec
+  "appnd Lf t = t"
+  "appnd (Br a t1 t2) t = Br a (appnd t1 t) (appnd t2 t)"
+
+
+text {* \medskip BT simplification *}
+
+ML {*ResAtp.problem_name := "BT__n_leaves_reflect"*}
+lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
+  apply (induct t)
+  apply (metis add_right_cancel n_leaves.simps(1) reflect.simps(1))
+  apply (metis add_commute n_leaves.simps(2) reflect.simps(2))
+  done
+
+ML {*ResAtp.problem_name := "BT__n_nodes_reflect"*}
+lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
+  apply (induct t)
+  apply (metis reflect.simps(1))
+  apply (metis n_nodes.simps(2) nat_add_commute reflect.simps(2))
+  done
+
+ML {*ResAtp.problem_name := "BT__depth_reflect"*}
+lemma depth_reflect: "depth (reflect t) = depth t"
+  apply (induct t)
+  apply (metis depth.simps(1) reflect.simps(1))
+  apply (metis depth.simps(2) min_max.less_eq_less_sup.sup_commute reflect.simps(2))
+  done
+
+text {*
+  The famous relationship between the numbers of leaves and nodes.
+*}
+
+ML {*ResAtp.problem_name := "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))
+  apply auto
+  done
+
+ML {*ResAtp.problem_name := "BT__reflect_reflect_ident"*}
+lemma reflect_reflect_ident: "reflect (reflect t) = t"
+  apply (induct t)
+  apply (metis add_right_cancel reflect.simps(1));
+  apply (metis Suc_Suc_eq reflect.simps(2))
+  done
+
+ML {*ResAtp.problem_name := "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))
+txt{*BUG involving flex-flex pairs*}
+(*  apply (metis bt_map.simps(2)) *)
+apply auto
+done
+
+
+ML {*ResAtp.problem_name := "BT__bt_map_appnd"*}
+lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)"
+apply (induct t)
+  apply (metis appnd.simps(1) bt_map.simps(1))
+  apply (metis appnd.simps(2) bt_map.simps(2))  (*slow!!*)
+done
+
+
+ML {*ResAtp.problem_name := "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))
+txt{*Metis runs forever*}
+(*  apply (metis bt_map.simps(2) o_apply)*)
+apply auto
+done
+
+
+ML {*ResAtp.problem_name := "BT__bt_map_reflect"*}
+lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
+  apply (induct t)
+  apply (metis add_right_cancel bt_map.simps(1) reflect.simps(1))
+  apply (metis add_right_cancel bt_map.simps(2) reflect.simps(2))
+  done
+
+ML {*ResAtp.problem_name := "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))
+   apply simp
+  done
+
+ML {*ResAtp.problem_name := "BT__inorder_bt_map"*}
+lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
+  apply (induct t)
+  apply (metis bt_map.simps(1) inorder.simps(1) map.simps(1))
+  apply simp
+  done
+
+ML {*ResAtp.problem_name := "BT__postorder_bt_map"*}
+lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
+  apply (induct t)
+  apply (metis bt_map.simps(1) map.simps(1) postorder.simps(1))
+   apply simp
+  done
+
+ML {*ResAtp.problem_name := "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))
+   apply simp
+  done
+
+ML {*ResAtp.problem_name := "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 One_nat_def Suc_eq_add_numeral_1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
+  apply (metis add_commute bt_map.simps(2) n_leaves.simps(2))
+  done
+
+
+ML {*ResAtp.problem_name := "BT__preorder_reflect"*}
+lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
+  apply (induct t)
+  apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv)
+  apply (metis append_eq_append_conv2 inorder.simps(1) postorder.simps(2) preorder.simps(2) reflect.simps(2) rev_append rev_is_rev_conv rev_singleton_conv rev_swap rotate_simps)
+  done
+
+ML {*ResAtp.problem_name := "BT__inorder_reflect"*}
+lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
+  apply (induct t)
+  apply (metis inorder.simps(1) reflect.simps(1) rev.simps(1))
+  apply simp
+  done
+
+ML {*ResAtp.problem_name := "BT__postorder_reflect"*}
+lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
+  apply (induct t)
+  apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1))
+  apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rotate1_def self_append_conv2)
+  done
+
+text {*
+ Analogues of the standard properties of the append function for lists.
+*}
+
+ML {*ResAtp.problem_name := "BT__appnd_assoc"*}
+lemma appnd_assoc [simp]:
+     "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
+  apply (induct t1)
+  apply (metis appnd.simps(1))
+  apply (metis appnd.simps(2))
+  done
+
+ML {*ResAtp.problem_name := "BT__appnd_Lf2"*}
+lemma appnd_Lf2 [simp]: "appnd t Lf = t"
+  apply (induct t)
+  apply (metis appnd.simps(1))
+  apply (metis appnd.simps(2))
+  done
+
+ML {*ResAtp.problem_name := "BT__depth_appnd"*}
+  declare max_add_distrib_left [simp]
+lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2"
+  apply (induct t1)
+  apply (metis add_0 appnd.simps(1) depth.simps(1))
+apply (simp add: ); 
+  done
+
+ML {*ResAtp.problem_name := "BT__n_leaves_appnd"*}
+lemma n_leaves_appnd [simp]:
+     "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2"
+  apply (induct t1)
+  apply (metis One_nat_def appnd.simps(1) less_irrefl less_linear n_leaves.simps(1) nat_mult_1) 
+  apply (simp add: left_distrib)
+  done
+
+ML {*ResAtp.problem_name := "BT__bt_map_appnd"*}
+lemma bt_map_appnd:
+     "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
+  apply (induct t1)
+  apply (metis appnd.simps(1) bt_map_appnd)
+  apply (metis bt_map_appnd)
+  done
+
+end
diff -r 020381339d87 -r dd874e6a3282 src/HOL/MetisExamples/BigO.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MetisExamples/BigO.thy	Thu Jun 21 13:23:33 2007 +0200
@@ -0,0 +1,1553 @@
+(*  Title:      HOL/MetisExamples/BigO.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Testing the metis method
+*)
+
+header {* Big O notation *}
+
+theory BigO
+imports SetsAndFunctions 
+begin
+
+subsection {* Definitions *}
+
+constdefs 
+
+  bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))")
+  "O(f::('a => 'b)) ==   {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
+
+ML{*ResAtp.problem_name := "BigO__bigo_pos_const"*}
+lemma bigo_pos_const: "(EX (c::'a::ordered_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);
+txt{*Version 1: one-shot proof. MUCH SLOWER with types: 24 versus 6.7 seconds*}
+  apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_le_mult)
+  done
+
+(*** Now various verions with an increasing modulus ***)
+
+ML{*ResReconstruct.modulus := 1*}
+
+lemma bigo_pos_const: "(EX (c::'a::ordered_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)
+(*hand-modified to give 'a sort ordered_idom and X3 type 'a*)
+proof (neg_clausify)
+fix c x
+assume 0: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
+assume 1: "c \<noteq> (0\<Colon>'a::ordered_idom)"
+assume 2: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
+have 3: "\<And>X1 X3. \<bar>h X3\<bar> < X1 \<or> \<not> c * \<bar>f X3\<bar> < X1"
+  by (metis order_le_less_trans 0)
+have 4: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3 \<or> \<not> (1\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis mult_le_cancel_right2 order_refl)
+have 5: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3"
+  by (metis 4 order_refl)
+have 6: "\<And>X3. \<bar>0\<Colon>'a\<bar> = \<bar>X3\<bar> * (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (0\<Colon>'a)"
+  by (metis abs_mult_pos mult_cancel_right1)
+have 7: "\<bar>0\<Colon>'a\<bar> = (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (0\<Colon>'a)"
+  by (metis 6 mult_cancel_right1)
+have 8: "\<bar>0\<Colon>'a\<bar> = (0\<Colon>'a)"
+  by (metis 7 order_refl)
+have 9: "\<not> (0\<Colon>'a) < (0\<Colon>'a)"
+  by (metis abs_not_less_zero 8)
+have 10: "\<bar>(1\<Colon>'a) * (0\<Colon>'a)\<bar> = - ((1\<Colon>'a) * (0\<Colon>'a))"
+  by (metis abs_of_nonpos 5)
+have 11: "(0\<Colon>'a) = - ((1\<Colon>'a) * (0\<Colon>'a))"
+  by (metis 10 mult_cancel_right1 8)
+have 12: "(0\<Colon>'a) = - (0\<Colon>'a)"
+  by (metis 11 mult_cancel_right1)
+have 13: "\<And>X3. \<bar>X3\<bar> = X3 \<or> X3 \<le> (0\<Colon>'a)"
+  by (metis abs_of_nonneg linorder_linear)
+have 14: "c \<le> (0\<Colon>'a) \<or> \<not> \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  by (metis 2 13)
+have 15: "c \<le> (0\<Colon>'a)"
+  by (metis 14 0)
+have 16: "c = (0\<Colon>'a) \<or> c < (0\<Colon>'a)"
+  by (metis linorder_antisym_conv2 15)
+have 17: "\<bar>c\<bar> = - c"
+  by (metis abs_of_nonpos 15)
+have 18: "c < (0\<Colon>'a)"
+  by (metis 16 1)
+have 19: "\<not> \<bar>h x\<bar> \<le> - c * \<bar>f x\<bar>"
+  by (metis 2 17)
+have 20: "\<And>X3. X3 * (1\<Colon>'a) = X3"
+  by (metis mult_cancel_right1 AC_mult.f.commute)
+have 21: "\<And>X3. (0\<Colon>'a) \<le> X3 * X3"
+  by (metis zero_le_square AC_mult.f.commute)
+have 22: "(0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis 21 mult_cancel_left1)
+have 23: "\<And>X3. (0\<Colon>'a) = X3 \<or> (0\<Colon>'a) \<noteq> - X3"
+  by (metis neg_equal_iff_equal 12)
+have 24: "\<And>X3. (0\<Colon>'a) = - X3 \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis 23 minus_equation_iff)
+have 25: "\<And>X3. \<bar>0\<Colon>'a\<bar> = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis abs_minus_cancel 24)
+have 26: "\<And>X3. (0\<Colon>'a) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis 25 8)
+have 27: "\<And>X1 X3. (0\<Colon>'a) * \<bar>X1\<bar> = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis abs_mult 26)
+have 28: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis 27 mult_cancel_left1)
+have 29: "\<And>X1 X3. (0\<Colon>'a) = X3 * X1 \<or> (0\<Colon>'a) < (0\<Colon>'a) \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis zero_less_abs_iff 28)
+have 30: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis 29 9)
+have 31: "\<And>X1 X3. (0\<Colon>'a) = X1 * X3 \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis AC_mult.f.commute 30)
+have 32: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
+  by (metis abs_mult 31)
+have 33: "\<And>X3::'a. \<bar>X3 * X3\<bar> = X3 * X3"
+  by (metis abs_mult_self abs_mult AC_mult.f.commute)
+have 34: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis abs_ge_zero abs_mult_pos 20)
+have 35: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar>"
+  by (metis 34 22)
+have 36: "\<And>X3. X3 * (1\<Colon>'a) = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis abs_eq_0 abs_mult_pos 20)
+have 37: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis 36 20)
+have 38: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a)"
+  by (metis 37 22)
+have 39: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
+  by (metis 38 32)
+have 40: "\<And>X3::'a. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis abs_idempotent abs_mult_pos 20)
+have 41: "\<And>X3::'a. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar>"
+  by (metis 40 22)
+have 42: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis abs_not_less_zero abs_mult_pos 20)
+have 43: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a)"
+  by (metis 42 22)
+have 44: "\<And>X3. X3 * (1\<Colon>'a) = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis abs_le_zero_iff abs_mult_pos 20)
+have 45: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis 44 20)
+have 46: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
+  by (metis 45 22)
+have 47: "\<And>X3. X3 * X3 = (0\<Colon>'a) \<or> \<not> X3 * X3 \<le> (0\<Colon>'a)"
+  by (metis 46 33)
+have 48: "\<And>X3. X3 * X3 = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
+  by (metis 47 mult_le_0_iff)
+have 49: "\<And>X3. \<bar>X3\<bar> = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
+  by (metis mult_eq_0_iff abs_mult_self 48)
+have 50: "\<And>X1 X3.
+   (0\<Colon>'a) * \<bar>X1\<bar> = \<bar>\<bar>X3 * X1\<bar>\<bar> \<or>
+   \<not> (0\<Colon>'a) \<le> \<bar>X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
+  by (metis abs_mult_pos abs_mult 49)
+have 51: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> X1 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X1"
+  by (metis 39 49)
+have 52: "\<And>X1 X3.
+   (0\<Colon>'a) = \<bar>\<bar>X3 * X1\<bar>\<bar> \<or>
+   \<not> (0\<Colon>'a) \<le> \<bar>X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
+  by (metis 50 mult_cancel_left1)
+have 53: "\<And>X1 X3.
+   (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> (0\<Colon>'a) \<le> \<bar>X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
+  by (metis 52 41)
+have 54: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
+  by (metis 53 35)
+have 55: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
+  by (metis 54 35)
+have 56: "\<And>X1 X3. \<bar>X1 * X3\<bar> = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
+  by (metis 55 AC_mult.f.commute)
+have 57: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a)"
+  by (metis 38 56)
+have 58: "\<And>X3. \<bar>h X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> \<bar>f X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>f X3\<bar>"
+  by (metis 0 51)
+have 59: "\<And>X3. \<bar>h X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> \<bar>f X3\<bar> \<le> (0\<Colon>'a)"
+  by (metis 58 35)
+have 60: "\<And>X3. \<bar>h X3\<bar> \<le> (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>f X3\<bar>"
+  by (metis 59 linorder_not_le)
+have 61: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>X1\<bar>"
+  by (metis 57 linorder_not_le)
+have 62: "(0\<Colon>'a) < \<bar>\<bar>f x\<bar>\<bar> \<or> \<not> \<bar>h x\<bar> \<le> (0\<Colon>'a)"
+  by (metis 19 61)
+have 63: "(0\<Colon>'a) < \<bar>f x\<bar> \<or> \<not> \<bar>h x\<bar> \<le> (0\<Colon>'a)"
+  by (metis 62 41)
+have 64: "(0\<Colon>'a) < \<bar>f x\<bar>"
+  by (metis 63 60)
+have 65: "\<And>X3. \<bar>h X3\<bar> < (0\<Colon>'a) \<or> \<not> c < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
+  by (metis 3 mult_less_0_iff)
+have 66: "\<And>X3. \<bar>h X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
+  by (metis 65 18)
+have 67: "\<And>X3. \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
+  by (metis 66 43)
+show "False"
+  by (metis 67 64)
+qed
+
+lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_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);
+ML{*ResReconstruct.modulus:=2*}
+proof (neg_clausify)
+fix c x
+assume 0: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
+assume 1: "c \<noteq> (0\<Colon>'a::ordered_idom)"
+assume 2: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
+have 3: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3"
+  by (metis mult_le_cancel_right2 order_refl order_refl)
+have 4: "\<bar>0\<Colon>'a\<bar> = (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (0\<Colon>'a)"
+  by (metis abs_mult_pos mult_cancel_right1 mult_cancel_right1)
+have 5: "\<not> (0\<Colon>'a) < (0\<Colon>'a)"
+  by (metis abs_not_less_zero 4 order_refl)
+have 6: "(0\<Colon>'a) = - ((1\<Colon>'a) * (0\<Colon>'a))"
+  by (metis abs_of_nonpos 3 mult_cancel_right1 4 order_refl)
+have 7: "\<And>X3. \<bar>X3\<bar> = X3 \<or> X3 \<le> (0\<Colon>'a)"
+  by (metis abs_of_nonneg linorder_linear)
+have 8: "c \<le> (0\<Colon>'a)"
+  by (metis 2 7 0)
+have 9: "\<bar>c\<bar> = - c"
+  by (metis abs_of_nonpos 8)
+have 10: "\<not> \<bar>h x\<bar> \<le> - c * \<bar>f x\<bar>"
+  by (metis 2 9)
+have 11: "\<And>X3. X3 * (1\<Colon>'a) = X3"
+  by (metis mult_cancel_right1 AC_mult.f.commute)
+have 12: "(0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis zero_le_square AC_mult.f.commute mult_cancel_left1)
+have 13: "\<And>X3. (0\<Colon>'a) = - X3 \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis neg_equal_iff_equal 6 mult_cancel_right1 minus_equation_iff)
+have 14: "\<And>X3. (0\<Colon>'a) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis abs_minus_cancel 13 4 order_refl)
+have 15: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis abs_mult 14 mult_cancel_left1)
+have 16: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis zero_less_abs_iff 15 5)
+have 17: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
+  by (metis abs_mult AC_mult.f.commute 16)
+have 18: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar>"
+  by (metis abs_ge_zero abs_mult_pos 11 12)
+have 19: "\<And>X3. X3 * (1\<Colon>'a) = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis abs_eq_0 abs_mult_pos 11)
+have 20: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a)"
+  by (metis 19 11 12)
+have 21: "\<And>X3::'a. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis abs_idempotent abs_mult_pos 11)
+have 22: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis abs_not_less_zero abs_mult_pos 11)
+have 23: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis abs_le_zero_iff abs_mult_pos 11 11)
+have 24: "\<And>X3. X3 * X3 = (0\<Colon>'a) \<or> \<not> X3 * X3 \<le> (0\<Colon>'a)"
+  by (metis 23 12 abs_mult_self abs_mult AC_mult.f.commute)
+have 25: "\<And>X3. \<bar>X3\<bar> = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
+  by (metis mult_eq_0_iff abs_mult_self 24 mult_le_0_iff)
+have 26: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> X1 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X1"
+  by (metis 20 17 25)
+have 27: "\<And>X1 X3.
+   (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> (0\<Colon>'a) \<le> \<bar>X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
+  by (metis abs_mult_pos abs_mult 25 mult_cancel_left1 21 12)
+have 28: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
+  by (metis 27 18 18)
+have 29: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a)"
+  by (metis 20 28 AC_mult.f.commute)
+have 30: "\<And>X3. \<bar>h X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> \<bar>f X3\<bar> \<le> (0\<Colon>'a)"
+  by (metis 0 26 18)
+have 31: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>X1\<bar>"
+  by (metis 29 linorder_not_le)
+have 32: "(0\<Colon>'a) < \<bar>f x\<bar> \<or> \<not> \<bar>h x\<bar> \<le> (0\<Colon>'a)"
+  by (metis 10 31 21 12)
+have 33: "\<And>X3. \<bar>h X3\<bar> < (0\<Colon>'a) \<or> \<not> c < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
+  by (metis order_le_less_trans 0 mult_less_0_iff)
+have 34: "\<And>X3. \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
+  by (metis 33 linorder_antisym_conv2 8 1 22 12)
+show "False"
+  by (metis 34 32 30 linorder_not_le)
+qed
+
+lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_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);
+ML{*ResReconstruct.modulus:=3*}
+proof (neg_clausify)
+fix c x
+assume 0: "\<And>A\<Colon>'b\<Colon>type.
+   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) A\<bar>
+   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) A\<bar>"
+assume 1: "(c\<Colon>'a\<Colon>ordered_idom) \<noteq> (0\<Colon>'a\<Colon>ordered_idom)"
+assume 2: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
+  \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
+have 3: "\<And>X3\<Colon>'a\<Colon>ordered_idom. (1\<Colon>'a\<Colon>ordered_idom) * X3 \<le> X3"
+  by (metis mult_le_cancel_right2 order_refl order_refl)
+have 4: "\<bar>0\<Colon>'a\<Colon>ordered_idom\<bar> = (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis abs_mult_pos mult_cancel_right1 mult_cancel_right1 order_refl)
+have 5: "(0\<Colon>'a\<Colon>ordered_idom) = - ((1\<Colon>'a\<Colon>ordered_idom) * (0\<Colon>'a\<Colon>ordered_idom))"
+  by (metis abs_of_nonpos 3 mult_cancel_right1 4)
+have 6: "(c\<Colon>'a\<Colon>ordered_idom) \<le> (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis 2 abs_of_nonneg linorder_linear 0)
+have 7: "(c\<Colon>'a\<Colon>ordered_idom) < (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis linorder_antisym_conv2 6 1)
+have 8: "\<And>X3\<Colon>'a\<Colon>ordered_idom. X3 * (1\<Colon>'a\<Colon>ordered_idom) = X3"
+  by (metis mult_cancel_right1 AC_mult.f.commute)
+have 9: "\<And>X3\<Colon>'a\<Colon>ordered_idom. (0\<Colon>'a\<Colon>ordered_idom) = X3 \<or> (0\<Colon>'a\<Colon>ordered_idom) \<noteq> - X3"
+  by (metis neg_equal_iff_equal 5 mult_cancel_right1)
+have 10: "\<And>X3\<Colon>'a\<Colon>ordered_idom. (0\<Colon>'a\<Colon>ordered_idom) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis abs_minus_cancel 9 minus_equation_iff 4)
+have 11: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
+   (0\<Colon>'a\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis abs_mult 10)
+have 12: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
+   X3 * X1 = (0\<Colon>'a\<Colon>ordered_idom) \<or> X3 \<noteq> (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis zero_less_abs_iff 11 mult_cancel_left1 abs_not_less_zero 4)
+have 13: "\<And>X3\<Colon>'a\<Colon>ordered_idom. \<bar>X3 * X3\<bar> = X3 * X3"
+  by (metis abs_mult_self abs_mult AC_mult.f.commute)
+have 14: "\<And>X3\<Colon>'a\<Colon>ordered_idom. (0\<Colon>'a\<Colon>ordered_idom) \<le> \<bar>X3\<bar>"
+  by (metis abs_ge_zero abs_mult_pos 8 zero_le_square AC_mult.f.commute mult_cancel_left1)
+have 15: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
+   X3 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
+   \<bar>X3\<bar> \<noteq> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> (1\<Colon>'a\<Colon>ordered_idom)"
+  by (metis abs_eq_0 abs_mult_pos 8 8)
+have 16: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
+   \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> (1\<Colon>'a\<Colon>ordered_idom)"
+  by (metis abs_idempotent abs_mult_pos 8)
+have 17: "\<And>X3\<Colon>'a\<Colon>ordered_idom. \<not> \<bar>X3\<bar> < (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis abs_not_less_zero abs_mult_pos 8 zero_le_square AC_mult.f.commute mult_cancel_left1)
+have 18: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
+   X3 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
+   \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or>
+   \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> (1\<Colon>'a\<Colon>ordered_idom)"
+  by (metis abs_le_zero_iff abs_mult_pos 8 8)
+have 19: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
+   X3 * X3 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
+   \<not> X3 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> X3"
+  by (metis 18 zero_le_square AC_mult.f.commute mult_cancel_left1 13 mult_le_0_iff)
+have 20: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
+   X3 * X1 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
+   \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> X1"
+  by (metis 15 zero_le_square AC_mult.f.commute mult_cancel_left1 abs_mult AC_mult.f.commute 12 mult_eq_0_iff abs_mult_self 19)
+have 21: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
+   (0\<Colon>'a\<Colon>ordered_idom) = \<bar>X3 * X1\<bar> \<or>
+   \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> \<bar>X3\<bar>"
+  by (metis abs_mult_pos abs_mult mult_eq_0_iff abs_mult_self 19 mult_cancel_left1 16 zero_le_square AC_mult.f.commute mult_cancel_left1 14)
+have 22: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
+   X3 * X1 = (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis 15 zero_le_square AC_mult.f.commute mult_cancel_left1 21 14 AC_mult.f.commute)
+have 23: "\<And>X3\<Colon>'b\<Colon>type.
+   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or>
+   (0\<Colon>'a\<Colon>ordered_idom) < \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar>"
+  by (metis 0 20 14 linorder_not_le)
+have 24: "(0\<Colon>'a\<Colon>ordered_idom) < \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar> \<or>
+\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis 2 abs_of_nonpos 6 22 linorder_not_le 16 zero_le_square AC_mult.f.commute mult_cancel_left1)
+have 25: "\<And>X3\<Colon>'b\<Colon>type.
+   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar> < (0\<Colon>'a\<Colon>ordered_idom) \<or>
+   \<not> (0\<Colon>'a\<Colon>ordered_idom) < \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar>"
+  by (metis order_le_less_trans 0 mult_less_0_iff 7)
+show "False"
+  by (metis 25 17 24 23)
+qed
+
+lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_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);
+ML{*ResReconstruct.modulus:=4*}
+ML{*ResReconstruct.recon_sorts:=false*}
+proof (neg_clausify)
+fix c x
+assume 0: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
+assume 1: "c \<noteq> (0\<Colon>'a)"
+assume 2: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
+have 3: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3"
+  by (metis mult_le_cancel_right2 order_refl order_refl)
+have 4: "\<not> (0\<Colon>'a) < (0\<Colon>'a)"
+  by (metis abs_not_less_zero abs_mult_pos mult_cancel_right1 mult_cancel_right1 order_refl)
+have 5: "c \<le> (0\<Colon>'a)"
+  by (metis 2 abs_of_nonneg linorder_linear 0)
+have 6: "\<not> \<bar>h x\<bar> \<le> - c * \<bar>f x\<bar>"
+  by (metis 2 abs_of_nonpos 5)
+have 7: "(0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis zero_le_square AC_mult.f.commute mult_cancel_left1)
+have 8: "\<And>X3. (0\<Colon>'a) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis abs_minus_cancel neg_equal_iff_equal abs_of_nonpos 3 mult_cancel_right1 abs_mult_pos mult_cancel_right1 mult_cancel_right1 order_refl mult_cancel_right1 minus_equation_iff abs_mult_pos mult_cancel_right1 mult_cancel_right1 order_refl)
+have 9: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
+  by (metis abs_mult 8 mult_cancel_left1)
+have 10: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
+  by (metis abs_mult AC_mult.f.commute zero_less_abs_iff 9 4)
+have 11: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar>"
+  by (metis abs_ge_zero abs_mult_pos mult_cancel_right1 AC_mult.f.commute 7)
+have 12: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a)"
+  by (metis abs_eq_0 abs_mult_pos mult_cancel_right1 AC_mult.f.commute mult_cancel_right1 AC_mult.f.commute 7)
+have 13: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis abs_not_less_zero abs_mult_pos mult_cancel_right1 AC_mult.f.commute)
+have 14: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
+  by (metis abs_le_zero_iff abs_mult_pos mult_cancel_right1 AC_mult.f.commute mult_cancel_right1 AC_mult.f.commute)
+have 15: "\<And>X3. \<bar>X3\<bar> = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
+  by (metis mult_eq_0_iff abs_mult_self 14 7 abs_mult_self abs_mult AC_mult.f.commute mult_le_0_iff)
+have 16: "\<And>X1 X3.
+   (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> (0\<Colon>'a) \<le> \<bar>X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
+  by (metis abs_mult_pos abs_mult 15 mult_cancel_left1 abs_idempotent abs_mult_pos mult_cancel_right1 AC_mult.f.commute 7)
+have 17: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a)"
+  by (metis 12 16 11 11 AC_mult.f.commute)
+have 18: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>X1\<bar>"
+  by (metis 17 linorder_not_le)
+have 19: "\<And>X3. \<bar>h X3\<bar> < (0\<Colon>'a) \<or> \<not> c < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
+  by (metis order_le_less_trans 0 mult_less_0_iff)
+show "False"
+  by (metis 19 linorder_antisym_conv2 5 1 13 7 6 18 abs_idempotent abs_mult_pos mult_cancel_right1 AC_mult.f.commute 7 0 12 10 15 11 linorder_not_le)
+qed
+
+
+ML{*ResReconstruct.modulus:=1*}
+ML{*ResReconstruct.recon_sorts:=true*}
+
+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)
+
+ML{*ResAtp.problem_name := "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
+
+
+ML{*ResAtp.problem_name := "BigO__bigo_refl"*}
+lemma bigo_refl [intro]: "f : O(f)"
+  apply(auto simp add: bigo_def)
+proof (neg_clausify)
+fix x
+assume 0: "\<And>mes_pSG\<Colon>'b\<Colon>ordered_idom.
+   \<not> \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_pSG)\<bar>
+     \<le> mes_pSG * \<bar>f (x mes_pSG)\<bar>"
+have 1: "\<And>X3\<Colon>'b. X3 \<le> (1\<Colon>'b) * X3 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
+  by (metis Ring_and_Field.mult_le_cancel_right1 order_refl)
+have 2: "\<And>X3\<Colon>'b. X3 \<le> (1\<Colon>'b) * X3"
+  by (metis 1 order_refl)
+show 3: "False"
+  by (metis 0 2)
+qed
+
+ML{*ResAtp.problem_name := "BigO__bigo_zero"*}
+lemma bigo_zero: "0 : O(g)"
+  apply (auto simp add: bigo_def func_zero)
+proof (neg_clausify)
+fix x
+assume 0: "\<And>mes_mVM\<Colon>'b\<Colon>ordered_idom.
+   \<not> (0\<Colon>'b\<Colon>ordered_idom)
+     \<le> mes_mVM *
+       \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom)
+         ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_mVM)\<bar>"
+have 1: "(0\<Colon>'b\<Colon>ordered_idom) < (0\<Colon>'b\<Colon>ordered_idom)"
+  by (metis 0 Ring_and_Field.mult_le_cancel_left1)
+show 2: "False"
+  by (metis Orderings.linorder_class.neq_iff 1)
+qed
+
+lemma bigo_zero2: "O(%x.0) = {%x.0}"
+  apply (auto simp add: bigo_def) 
+  apply (rule ext)
+  apply auto
+done
+
+lemma bigo_plus_self_subset [intro]: 
+  "O(f) + O(f) <= O(f)"
+  apply (auto simp add: bigo_alt_def set_plus)
+  apply (rule_tac x = "c + ca" in exI)
+  apply auto
+  apply (simp add: ring_distrib func_plus)
+  apply (blast intro:order_trans abs_triangle_ineq add_mono elim:) 
+done
+
+lemma bigo_plus_idemp [simp]: "O(f) + 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) + O(g)"
+  apply (rule subsetI)
+  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus)
+  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_distrib)
+  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_distrib)
+  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 (rule mult_nonneg_nonneg)
+  apply (rule add_nonneg_nonneg)
+  apply (erule order_less_imp_le)+
+  apply simp
+  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 + B <= O(f)"
+  apply (subgoal_tac "A + B <= O(f) + O(f)")
+  apply (erule order_trans)
+  apply simp
+  apply (auto del: subsetI simp del: bigo_plus_idemp)
+done
+
+ML{*ResAtp.problem_name := "BigO__bigo_plus_eq"*}
+lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
+  O(f + g) = O(f) + O(g)"
+  apply (rule equalityI)
+  apply (rule bigo_plus_subset)
+  apply (simp add: bigo_alt_def set_plus func_plus)
+  apply clarify 
+(*sledgehammer*); 
+  apply (rule_tac x = "max c ca" in exI)
+  apply (rule conjI)
+  apply (subgoal_tac "c <= max c ca")
+  apply (erule order_less_le_trans)
+  apply assumption
+  apply (rule le_maxI1)
+  apply clarify
+  apply (drule_tac x = "xa" in spec)+
+  apply (subgoal_tac "0 <= f xa + g xa")
+  apply (simp add: ring_distrib)
+  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 (rule add_nonneg_nonneg)
+  apply assumption+
+  apply (rule add_mono)
+ML{*ResAtp.problem_name := "BigO__bigo_plus_eq_simpler"*} 
+(*sledgehammer...fails*); 
+  apply (subgoal_tac "c * f xa <= max c ca * f xa")
+  apply (blast intro: order_trans)
+  apply (rule mult_right_mono)
+  apply (rule le_maxI1)
+  apply assumption
+  apply (subgoal_tac "ca * g xa <= max c ca * g xa")
+  apply (blast intro: order_trans)
+  apply (rule mult_right_mono)
+  apply (rule le_maxI2)
+  apply assumption
+done
+
+ML{*ResAtp.problem_name := "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-shot proof*)
+  apply (metis OrderedGroup.abs_ge_self  OrderedGroup.abs_le_D1  OrderedGroup.abs_of_nonneg  Orderings.linorder_class.not_less  order_less_le  Orderings.xt1(12)  Ring_and_Field.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: single-step proof*)
+proof (neg_clausify)
+fix x
+assume 0: "\<And>mes_mbt\<Colon>'a.
+   (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mbt
+   \<le> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mbt"
+assume 1: "\<And>mes_mbs\<Colon>'b\<Colon>ordered_idom.
+   \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_mbs)
+     \<le> mes_mbs * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x mes_mbs)\<bar>"
+have 2: "\<And>X3\<Colon>'a.
+   (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 =
+   (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 \<or>
+   \<not> c * g X3 \<le> f X3"
+  by (metis Lattices.min_max.less_eq_less_inf.antisym_intro 0)
+have 3: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
+   \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
+     \<le> \<bar>X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)\<bar>"
+  by (metis 1 Ring_and_Field.abs_mult)
+have 4: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (1\<Colon>'b\<Colon>ordered_idom) * X3 = X3"
+  by (metis Ring_and_Field.mult_cancel_left2 Finite_Set.AC_mult.f.commute)
+have 5: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * (1\<Colon>'b\<Colon>ordered_idom) = X3"
+  by (metis Ring_and_Field.mult_cancel_right2 Finite_Set.AC_mult.f.commute)
+have 6: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
+  by (metis Ring_and_Field.abs_mult_self Finite_Set.AC_mult.f.commute)
+have 7: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> X3 * X3"
+  by (metis Ring_and_Field.zero_le_square Finite_Set.AC_mult.f.commute)
+have 8: "(0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis 7 Ring_and_Field.mult_cancel_left2)
+have 9: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * X3 = \<bar>X3 * X3\<bar>"
+  by (metis Ring_and_Field.abs_mult 6)
+have 10: "\<bar>1\<Colon>'b\<Colon>ordered_idom\<bar> = (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis 9 4)
+have 11: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>1\<Colon>'b\<Colon>ordered_idom\<bar>"
+  by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 5)
+have 12: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar>"
+  by (metis 11 10 5)
+have 13: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
+   X3 * (1\<Colon>'b\<Colon>ordered_idom) \<le> X1 \<or>
+   \<not> \<bar>X3\<bar> \<le> X1 \<or> \<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis OrderedGroup.abs_le_D1 Ring_and_Field.abs_mult_pos 5)
+have 14: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
+   X3 \<le> X1 \<or> \<not> \<bar>X3\<bar> \<le> X1 \<or> \<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis 13 5)
+have 15: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> \<not> \<bar>X3\<bar> \<le> X1"
+  by (metis 14 8)
+have 16: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
+  by (metis 15 Orderings.linorder_class.less_eq_less.linear)
+have 17: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
+   X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
+   \<le> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)"
+  by (metis 3 16)
+have 18: "(c\<Colon>'b\<Colon>ordered_idom) *
+(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<bar>) =
+(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)"
+  by (metis 2 17)
+have 19: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3 * X1\<bar> \<le> \<bar>\<bar>X3\<bar>\<bar> * \<bar>\<bar>X1\<bar>\<bar>"
+  by (metis 15 Ring_and_Field.abs_le_mult Ring_and_Field.abs_mult)
+have 20: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3 * X1\<bar> \<le> \<bar>X3\<bar> * \<bar>X1\<bar>"
+  by (metis 19 12 12)
+have 21: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 * X1 \<le> \<bar>X3\<bar> * \<bar>X1\<bar>"
+  by (metis 15 20)
+have 22: "(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom)
+ ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar>)
+\<le> \<bar>c\<bar> * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)\<bar>"
+  by (metis 21 18)
+show 23: "False"
+  by (metis 22 1)
+qed
+
+
+text{*So here is the easier (and more natural) problem using transitivity*}
+ML{*ResAtp.problem_name := "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-shot proof*) 
+apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less xt1(12));
+  done
+
+text{*So here is the easier (and more natural) problem using transitivity*}
+ML{*ResAtp.problem_name := "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: single-step proof*)
+proof (neg_clausify)
+fix x
+assume 0: "\<And>mes_mb9\<Colon>'a.
+   (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mb9
+   \<le> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mb9"
+assume 1: "\<And>mes_mb8\<Colon>'b\<Colon>ordered_idom.
+   \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_mb8)
+     \<le> mes_mb8 * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x mes_mb8)\<bar>"
+have 2: "\<And>X3\<Colon>'a.
+   (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 =
+   (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 \<or>
+   \<not> c * g X3 \<le> f X3"
+  by (metis Lattices.min_max.less_eq_less_inf.antisym_intro 0)
+have 3: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
+   \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
+     \<le> \<bar>X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)\<bar>"
+  by (metis 1 Ring_and_Field.abs_mult)
+have 4: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (1\<Colon>'b\<Colon>ordered_idom) * X3 = X3"
+  by (metis Ring_and_Field.mult_cancel_left2 Finite_Set.AC_mult.f.commute)
+have 5: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * (1\<Colon>'b\<Colon>ordered_idom) = X3"
+  by (metis Ring_and_Field.mult_cancel_right2 Finite_Set.AC_mult.f.commute)
+have 6: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
+  by (metis Ring_and_Field.abs_mult_self Finite_Set.AC_mult.f.commute)
+have 7: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> X3 * X3"
+  by (metis Ring_and_Field.zero_le_square Finite_Set.AC_mult.f.commute)
+have 8: "(0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis 7 Ring_and_Field.mult_cancel_left2)
+have 9: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * X3 = \<bar>X3 * X3\<bar>"
+  by (metis Ring_and_Field.abs_mult 6)
+have 10: "\<bar>1\<Colon>'b\<Colon>ordered_idom\<bar> = (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis 9 4)
+have 11: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>1\<Colon>'b\<Colon>ordered_idom\<bar>"
+  by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 5)
+have 12: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar>"
+  by (metis 11 10 5)
+have 13: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
+   X3 * (1\<Colon>'b\<Colon>ordered_idom) \<le> X1 \<or>
+   \<not> \<bar>X3\<bar> \<le> X1 \<or> \<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis OrderedGroup.abs_le_D1 Ring_and_Field.abs_mult_pos 5)
+have 14: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
+   X3 \<le> X1 \<or> \<not> \<bar>X3\<bar> \<le> X1 \<or> \<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis 13 5)
+have 15: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> \<not> \<bar>X3\<bar> \<le> X1"
+  by (metis 14 8)
+have 16: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
+  by (metis 15 Orderings.linorder_class.less_eq_less.linear)
+have 17: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
+   X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
+   \<le> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)"
+  by (metis 3 16)
+have 18: "(c\<Colon>'b\<Colon>ordered_idom) *
+(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<bar>) =
+(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)"
+  by (metis 2 17)
+have 19: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3 * X1\<bar> \<le> \<bar>\<bar>X3\<bar>\<bar> * \<bar>\<bar>X1\<bar>\<bar>"
+  by (metis 15 Ring_and_Field.abs_le_mult Ring_and_Field.abs_mult)
+have 20: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3 * X1\<bar> \<le> \<bar>X3\<bar> * \<bar>X1\<bar>"
+  by (metis 19 12 12)
+have 21: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 * X1 \<le> \<bar>X3\<bar> * \<bar>X1\<bar>"
+  by (metis 15 20)
+have 22: "(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom)
+ ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar>)
+\<le> \<bar>c\<bar> * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)\<bar>"
+  by (metis 21 18)
+show 23: "False"
+  by (metis 22 1)
+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
+
+ML{*ResAtp.problem_name := "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 func_minus func_plus)
+  prefer 2
+  apply (drule_tac x = x in spec)+ 
+  apply arith (*not clear that it's provable otherwise*) 
+proof (neg_clausify)
+fix x
+assume 0: "\<And>y. lb y \<le> f y"
+assume 1: "\<not> (0\<Colon>'b) \<le> f x + - lb x"
+have 2: "\<And>X3. (0\<Colon>'b) + X3 = X3"
+  by (metis diff_eq_eq right_minus_eq)
+have 3: "\<not> (0\<Colon>'b) \<le> f x - lb x"
+  by (metis 1 compare_rls(1))
+have 4: "\<not> (0\<Colon>'b) + lb x \<le> f x"
+  by (metis 3 le_diff_eq)
+show "False"
+  by (metis 4 2 0)
+qed
+
+ML{*ResAtp.problem_name := "BigO__bigo_abs"*}
+lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
+  apply (unfold bigo_def)
+  apply auto
+proof (neg_clausify)
+fix x
+assume 0: "!!mes_o43::'b::ordered_idom.
+   ~ abs ((f::'a::type => 'b::ordered_idom)
+           ((x::'b::ordered_idom => 'a::type) mes_o43))
+     <= mes_o43 * abs (f (x mes_o43))"
+have 1: "!!X3::'b::ordered_idom.
+   X3 <= (1::'b::ordered_idom) * X3 |
+   ~ (1::'b::ordered_idom) <= (1::'b::ordered_idom)"
+  by (metis mult_le_cancel_right1 order_refl)
+have 2: "!!X3::'b::ordered_idom. X3 <= (1::'b::ordered_idom) * X3"
+  by (metis 1 order_refl)
+show "False"
+  by (metis 0 2)
+qed
+
+ML{*ResAtp.problem_name := "BigO__bigo_abs2"*}
+lemma bigo_abs2: "f =o O(%x. abs(f x))"
+  apply (unfold bigo_def)
+  apply auto
+proof (neg_clausify)
+fix x
+assume 0: "\<And>mes_o4C\<Colon>'b\<Colon>ordered_idom.
+   \<not> \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_o4C)\<bar>
+     \<le> mes_o4C * \<bar>f (x mes_o4C)\<bar>"
+have 1: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
+   X3 \<le> (1\<Colon>'b\<Colon>ordered_idom) * X3 \<or>
+   \<not> (1\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis mult_le_cancel_right1 order_refl)
+have 2: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> (1\<Colon>'b\<Colon>ordered_idom) * X3"
+  by (metis 1 order_refl)
+show "False"
+  by (metis 0 2)
+qed
+ 
+lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
+  apply (rule equalityI)
+  apply (rule bigo_elt_subset)
+  apply (rule bigo_abs2)
+  apply (rule bigo_elt_subset)
+  apply (rule bigo_abs)
+done
+
+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 func_diff)
+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 func_diff)
+    apply (rule bigo_abs)
+    done
+  also have "... <= O(h)"
+    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) + O(h)"
+proof -
+  assume "f : g +o O(h)"
+  also have "... <= O(g) + O(h)"
+    by (auto del: subsetI)
+  also have "... = O(%x. abs(g x)) + 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)) + O(%x. abs(h x))"
+    by (rule bigo_plus_eq, auto)
+  finally show ?thesis
+    by (simp add: bigo_abs3 [symmetric])
+qed
+
+ML{*ResAtp.problem_name := "BigO__bigo_mult"*}
+lemma bigo_mult [intro]: "O(f)*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 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))")
+ML{*ResAtp.problem_name := "BigO__bigo_mult_simpler"*}
+prefer 2 
+apply (metis  Finite_Set.AC_mult.f.assoc  Finite_Set.AC_mult.f.left_commute  OrderedGroup.abs_of_pos  OrderedGroup.mult_left_commute  Ring_and_Field.abs_mult  Ring_and_Field.mult_pos_pos)
+  apply(erule ssubst) 
+  apply (subst abs_mult)
+(*not qute BigO__bigo_mult_simpler_1 (a hard problem!) as abs_mult has
+  just been done*)
+proof (neg_clausify)
+fix a c b ca x
+assume 0: "(0\<Colon>'b\<Colon>ordered_idom) < (c\<Colon>'b\<Colon>ordered_idom)"
+assume 1: "\<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
+\<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
+assume 2: "\<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
+\<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
+assume 3: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar> *
+  \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>
+  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> *
+    ((ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>)"
+have 4: "\<bar>c\<Colon>'b\<Colon>ordered_idom\<bar> = c"
+  by (metis OrderedGroup.abs_of_pos 0)
+have 5: "\<And>X1\<Colon>'b\<Colon>ordered_idom. (c\<Colon>'b\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>c * X1\<bar>"
+  by (metis Ring_and_Field.abs_mult 4)
+have 6: "(0\<Colon>'b\<Colon>ordered_idom) = (1\<Colon>'b\<Colon>ordered_idom) \<or>
+(0\<Colon>'b\<Colon>ordered_idom) < (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis OrderedGroup.abs_not_less_zero Ring_and_Field.abs_one Ring_and_Field.linorder_neqE_ordered_idom)
+have 7: "(0\<Colon>'b\<Colon>ordered_idom) < (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis 6 Ring_and_Field.one_neq_zero)
+have 8: "\<bar>1\<Colon>'b\<Colon>ordered_idom\<bar> = (1\<Colon>'b\<Colon>ordered_idom)"
+  by (metis OrderedGroup.abs_of_pos 7)
+have 9: "\<And>X1\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>X1\<bar>"
+  by (metis OrderedGroup.abs_ge_zero 5)
+have 10: "\<And>X1\<Colon>'b\<Colon>ordered_idom. X1 * (1\<Colon>'b\<Colon>ordered_idom) = X1"
+  by (metis Ring_and_Field.mult_cancel_right2 Finite_Set.AC_mult.f.commute)
+have 11: "\<And>X1\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar> * \<bar>1\<Colon>'b\<Colon>ordered_idom\<bar>"
+  by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 10)
+have 12: "\<And>X1\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
+  by (metis 11 8 10)
+have 13: "\<And>X1\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> \<bar>X1\<bar>"
+  by (metis OrderedGroup.abs_ge_zero 12)
+have 14: "\<not> (0\<Colon>'b\<Colon>ordered_idom)
+  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar> \<or>
+\<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
+\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
+\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<le> c * \<bar>f x\<bar>"
+  by (metis 3 Ring_and_Field.mult_mono)
+have 15: "\<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar> \<or>
+\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
+\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>
+  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
+  by (metis 14 9)
+have 16: "\<not> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
+  \<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
+\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>
+  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
+  by (metis 15 13)
+have 17: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
+  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
+  by (metis 16 2)
+show 18: "False"
+  by (metis 17 1)
+qed
+
+
+ML{*ResAtp.problem_name := "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)
+ML{*ResAtp.problem_name := "BigO__bigo_mult2_simpler"*}
+(*sledgehammer*); 
+  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
+
+ML{*ResAtp.problem_name:="BigO__bigo_mult3"*}
+lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
+by (metis bigo_mult set_times_intro subset_iff)
+
+ML{*ResAtp.problem_name:="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::ordered_field)) *o O(g)"
+proof -
+  assume "ALL x. f x ~= 0"
+  show "O(f * g) <= f *o O(g)"
+  proof
+    fix h
+    assume "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: prems 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: prems nonzero_divide_eq_eq mult_ac)
+      done
+    finally show "h : f *o O(g)".
+  qed
+qed
+
+ML{*ResAtp.problem_name := "BigO__bigo_mult6"*}
+lemma bigo_mult6: "ALL x. f x ~= 0 ==>
+    O(f * g) = (f::'a => ('b::ordered_field)) *o O(g)"
+by (metis bigo_mult2 bigo_mult5 order_antisym)
+
+(*proof requires relaxing relevance: 2007-01-25*)
+ML{*ResAtp.problem_name := "BigO__bigo_mult7"*}
+  declare bigo_mult6 [simp]
+lemma bigo_mult7: "ALL x. f x ~= 0 ==>
+    O(f * g) <= O(f::'a => ('b::ordered_field)) * O(g)"
+(*sledgehammer*)
+  apply (subst bigo_mult6)
+  apply assumption
+  apply (rule set_times_mono3) 
+  apply (rule bigo_refl)
+done
+  declare bigo_mult6 [simp del]
+
+ML{*ResAtp.problem_name := "BigO__bigo_mult8"*}
+  declare bigo_mult7[intro!]
+lemma bigo_mult8: "ALL x. f x ~= 0 ==>
+    O(f * g) = O(f::'a => ('b::ordered_field)) * 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 func_minus)
+
+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 func_minus 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) + O(g)"
+      by (auto del: subsetI)
+    also have "... <= O(g) + 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
+
+ML{*ResAtp.problem_name:="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 bigo_const1 [skolem]
+
+ML{*ResAtp.problem_name:="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) <= O(%x. 1)"; 
+(*??FAILS because the two occurrences of COMBK have different polymorphic types
+proof (neg_clausify)
+assume 0: "\<not> O(COMBK (c\<Colon>'b\<Colon>ordered_idom)) \<subseteq> O(COMBK (1\<Colon>'b\<Colon>ordered_idom))"
+have 1: "COMBK (c\<Colon>'b\<Colon>ordered_idom) \<notin> O(COMBK (1\<Colon>'b\<Colon>ordered_idom))"
+apply (rule notI) 
+apply (rule 0 [THEN notE]) 
+apply (rule bigo_elt_subset) 
+apply assumption; 
+sorry
+  by (metis 0 bigo_elt_subset)  loops??
+show "False"
+  by (metis 1 bigo_const1)
+qed
+*)
+  apply (rule bigo_elt_subset)
+  apply (rule bigo_const1)
+done
+
+declare bigo_const2 [skolem]
+
+ML{*ResAtp.problem_name := "BigO__bigo_const3"*}
+lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
+apply (simp add: bigo_def)
+proof (neg_clausify)
+assume 0: "(c\<Colon>'a\<Colon>ordered_field) \<noteq> (0\<Colon>'a\<Colon>ordered_field)"
+assume 1: "\<And>mes_md\<Colon>'a\<Colon>ordered_field. \<not> (1\<Colon>'a\<Colon>ordered_field) \<le> mes_md * \<bar>c\<Colon>'a\<Colon>ordered_field\<bar>"
+have 2: "(0\<Colon>'a\<Colon>ordered_field) = \<bar>c\<Colon>'a\<Colon>ordered_field\<bar> \<or>
+\<not> (1\<Colon>'a\<Colon>ordered_field) \<le> (1\<Colon>'a\<Colon>ordered_field)"
+  by (metis 1 field_inverse)
+have 3: "\<bar>c\<Colon>'a\<Colon>ordered_field\<bar> = (0\<Colon>'a\<Colon>ordered_field)"
+  by (metis 2 order_refl)
+have 4: "(0\<Colon>'a\<Colon>ordered_field) = (c\<Colon>'a\<Colon>ordered_field)"
+  by (metis OrderedGroup.abs_eq_0 3)
+show 5: "False"
+  by (metis 4 0)
+qed
+
+lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
+by (rule bigo_elt_subset, rule bigo_const3, assumption)
+
+lemma bigo_const [simp]: "(c::'a::ordered_field) ~= 0 ==> 
+    O(%x. c) = O(%x. 1)"
+by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
+
+ML{*ResAtp.problem_name := "BigO__bigo_const_mult1"*}
+lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
+  apply (simp add: bigo_def abs_mult) 
+proof (neg_clausify)
+fix x
+assume 0: "\<And>mes_vAL\<Colon>'b.
+   \<not> \<bar>c\<Colon>'b\<bar> *
+     \<bar>(f\<Colon>'a \<Rightarrow> 'b) ((x\<Colon>'b \<Rightarrow> 'a) mes_vAL)\<bar>
+     \<le> mes_vAL * \<bar>f (x mes_vAL)\<bar>"
+have 1: "\<And>Y\<Colon>'b. Y \<le> Y"
+  by (metis order_refl)
+show 2: "False"
+  by (metis 0 1)
+qed
+
+lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
+by (rule bigo_elt_subset, rule bigo_const_mult1)
+
+ML{*ResAtp.problem_name := "BigO__bigo_const_mult3"*}
+lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)"
+  apply (simp add: bigo_def)
+(*sledgehammer*); 
+  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::ordered_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::ordered_field) ~= 0 ==> 
+    O(%x. c * f x) = O(f)"
+by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
+
+ML{*ResAtp.problem_name := "BigO__bigo_const_mult5"*}
+lemma bigo_const_mult5 [simp]: "(c::'a::ordered_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) 
+(*sledgehammer*); 
+  apply (simp_all del: mult_assoc add: mult_assoc [symmetric] abs_mult)
+  apply (rule_tac x = "abs (inverse c) * d" in exI)
+  apply (rule allI)
+  apply (subst mult_assoc)
+  apply (rule mult_left_mono)
+  apply (erule spec)
+apply (simp add: ); 
+done
+
+
+ML{*ResAtp.problem_name := "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 func_minus
+      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
+
+ML{*ResAtp.problem_name := "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)  
+
+ML{*ResAtp.problem_name := "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 func_diff)
+  apply (subst setsum_subtractf [symmetric])
+  apply (subst right_diff_distrib [symmetric])
+  apply (rule bigo_setsum3)
+  apply (subst func_diff [symmetric])
+  apply (erule set_plus_imp_minus)
+done
+
+ML{*ResAtp.problem_name := "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)") 
+(*sledgehammer*); 
+  apply (subst abs_of_nonneg)
+  apply (rule mult_nonneg_nonneg)
+  apply auto
+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 func_diff)
+  apply (subst setsum_subtractf [symmetric])
+  apply (subst right_diff_distrib [symmetric])
+  apply (rule bigo_setsum5)
+  apply (subst func_diff [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 + 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::ordered_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
+
+ML{*ResAtp.problem_name := "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")
+prefer 2
+  apply (subgoal_tac "x = Suc (x - 1)")
+  apply (erule ssubst) back
+  apply (erule spec)
+  apply (rule Suc_pred') 
+  apply simp
+apply (metis OrderedGroup.abs_ge_zero  OrderedGroup.abs_zero  order_less_le  Ring_and_Field.split_mult_pos_le) 
+  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 func_diff)
+  apply (subst func_diff [symmetric])
+  apply (rule set_plus_imp_minus)
+  apply simp
+  apply (simp add: func_diff)
+done
+
+subsection {* Less than or equal to *}
+
+constdefs 
+  lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
+      (infixl "<o" 70)
+  "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
+
+ML{*ResAtp.problem_name:="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")
+(*
+?? abstractions don't work: abstraction function gets the wrong type?
+proof (neg_clausify)
+assume 0: "llabs_subgoal_1 f g = 0"
+assume 1: "llabs_subgoal_1 f g \<notin> O(h)"
+show "False"
+  by (metis 1 0 bigo_zero)
+*)
+  apply (erule ssubst)
+  apply (rule bigo_zero)
+  apply (unfold func_zero)
+  apply (rule ext)
+  apply (simp split: split_max)
+done
+
+
+ML{*ResAtp.problem_name := "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 func_diff)
+apply (erule thin_rl)
+(*sledgehammer*);  
+  apply (case_tac "0 <= k x - g x")
+  apply (simp del: compare_rls diff_minus);
+  apply (subst abs_of_nonneg)
+  apply (drule_tac x = x in spec) back
+ML{*ResAtp.problem_name := "BigO__bigo_lesso2_simpler"*}
+(*sledgehammer*);  
+  apply (simp add: compare_rls del: diff_minus)
+  apply (subst diff_minus)+
+  apply (rule add_right_mono)
+  apply (erule spec)
+  apply (rule order_trans) 
+  prefer 2
+  apply (rule abs_ge_zero)
+(*
+  apply (simp only: compare_rls min_max.below_sup.above_sup_conv 
+             linorder_not_le order_less_imp_le)
+*)
+  apply (simp add: compare_rls del: diff_minus)
+done
+
+
+
+ML{*ResAtp.problem_name := "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 func_diff)
+apply (erule thin_rl) 
+(*sledgehammer*); 
+  apply (case_tac "0 <= f x - k x")
+  apply (simp del: compare_rls diff_minus);
+  apply (subst abs_of_nonneg)
+  apply (drule_tac x = x in spec) back
+ML{*ResAtp.problem_name := "BigO__bigo_lesso3_simpler"*}
+(*sledgehammer*);  
+  apply (simp del: diff_minus)
+  apply (subst diff_minus)+
+  apply (rule add_left_mono)
+  apply (rule le_imp_neg_le)
+  apply (erule spec)
+  apply (rule order_trans) 
+  prefer 2
+  apply (rule abs_ge_zero)
+  apply (simp del: diff_minus)
+done
+
+lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_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: func_diff)
+  apply (drule bigo_useful_add)
+  apply assumption
+  apply (erule bigo_lesseq2) back
+  apply (rule allI)
+  apply (auto simp add: func_plus func_diff compare_rls 
+    split: split_max abs_split)
+done
+
+ML{*ResAtp.problem_name := "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
+(*sledgehammer*);  
+apply (auto simp add: compare_rls add_ac) 
+done
+
+end
diff -r 020381339d87 -r dd874e6a3282 src/HOL/MetisExamples/Message.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MetisExamples/Message.thy	Thu Jun 21 13:23:33 2007 +0200
@@ -0,0 +1,810 @@
+(*  Title:      HOL/MetisTest/Message.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Testing the metis method
+*)
+
+theory Message imports Main begin
+
+(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
+lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
+by blast
+
+types 
+  key = nat
+
+consts
+  all_symmetric :: bool        --{*true if all keys are symmetric*}
+  invKey        :: "key=>key"  --{*inverse of a symmetric key*}
+
+specification (invKey)
+  invKey [simp]: "invKey (invKey K) = K"
+  invKey_symmetric: "all_symmetric --> invKey = id"
+    by (rule exI [of _ id], auto)
+
+
+text{*The inverse of a symmetric key is itself; that of a public key
+      is the private key and vice versa*}
+
+constdefs
+  symKeys :: "key set"
+  "symKeys == {K. invKey K = K}"
+
+datatype  --{*We allow any number of friendly agents*}
+  agent = Server | Friend nat | Spy
+
+datatype
+     msg = Agent  agent	    --{*Agent names*}
+         | Number nat       --{*Ordinary integers, timestamps, ...*}
+         | Nonce  nat       --{*Unguessable nonces*}
+         | Key    key       --{*Crypto keys*}
+	 | Hash   msg       --{*Hashing*}
+	 | MPair  msg msg   --{*Compound messages*}
+	 | Crypt  key msg   --{*Encryption, public- or shared-key*}
+
+
+text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
+syntax
+  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
+
+syntax (xsymbols)
+  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
+
+translations
+  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
+  "{|x, y|}"      == "MPair x y"
+
+
+constdefs
+  HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
+    --{*Message Y paired with a MAC computed with the help of X*}
+    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
+
+  keysFor :: "msg set => key set"
+    --{*Keys useful to decrypt elements of a message set*}
+  "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
+
+
+subsubsection{*Inductive Definition of All Parts" of a Message*}
+
+consts  parts   :: "msg set => msg set"
+inductive "parts H"
+  intros 
+    Inj [intro]:               "X \<in> H ==> X \<in> parts H"
+    Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
+    Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
+    Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
+
+
+ML{*ResAtp.problem_name := "Message__parts_mono"*}
+lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
+apply auto
+apply (erule parts.induct) 
+apply (metis Inj set_mp)
+apply (metis Fst)
+apply (metis Snd)
+apply (metis Body)
+done
+
+
+text{*Equations hold because constructors are injective.*}
+lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
+by auto
+
+lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
+by auto
+
+lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
+by auto
+
+
+subsubsection{*Inverse of keys *}
+
+ML{*ResAtp.problem_name := "Message__invKey_eq"*}
+lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
+by (metis invKey)
+
+
+subsection{*keysFor operator*}
+
+lemma keysFor_empty [simp]: "keysFor {} = {}"
+by (unfold keysFor_def, blast)
+
+lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
+by (unfold keysFor_def, blast)
+
+lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
+by (unfold keysFor_def, blast)
+
+text{*Monotonicity*}
+lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> keysFor(H)"
+by (unfold keysFor_def, blast)
+
+lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Crypt [simp]: 
+    "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
+by (unfold keysFor_def, auto)
+
+lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
+by (unfold keysFor_def, blast)
+
+
+subsection{*Inductive relation "parts"*}
+
+lemma MPair_parts:
+     "[| {|X,Y|} \<in> parts H;        
+         [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
+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.  
+  @{text MPair_parts} is left as SAFE because it speeds up proofs.
+  The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
+
+lemma parts_increasing: "H \<subseteq> parts(H)"
+by blast
+
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+
+lemma parts_empty [simp]: "parts{} = {}"
+apply safe
+apply (erule parts.induct)
+apply blast+
+done
+
+lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
+by simp
+
+text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
+lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
+apply (erule parts.induct)
+apply blast+
+done
+
+
+subsubsection{*Unions *}
+
+lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
+by (intro Un_least parts_mono Un_upper1 Un_upper2)
+
+lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
+apply (rule subsetI)
+apply (erule parts.induct, blast+)
+done
+
+lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
+by (intro equalityI parts_Un_subset1 parts_Un_subset2)
+
+lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
+apply (subst insert_is_Un [of _ H])
+apply (simp only: parts_Un)
+done
+
+ML{*ResAtp.problem_name := "Message__parts_insert_two"*}
+lemma parts_insert2:
+     "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
+by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right insert_commute parts_Un)
+
+
+lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
+by (intro UN_least parts_mono UN_upper)
+
+lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
+apply (rule subsetI)
+apply (erule parts.induct, blast+)
+done
+
+lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
+by (intro equalityI parts_UN_subset1 parts_UN_subset2)
+
+text{*Added to simplify arguments to parts, analz and synth.
+  NOTE: the UN versions are no longer used!*}
+
+
+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] 
+declare in_parts_UnE [elim!]
+
+lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
+by (blast intro: parts_mono [THEN [2] rev_subsetD])
+
+subsubsection{*Idempotence and transitivity *}
+
+lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
+by (erule parts.induct, blast+)
+
+lemma parts_idem [simp]: "parts (parts H) = parts H"
+by blast
+
+ML{*ResAtp.problem_name := "Message__parts_subset_iff"*}
+lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
+apply (rule iffI) 
+apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
+apply (metis parts_Un parts_idem parts_increasing parts_mono)
+done
+
+lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
+by (blast dest: parts_mono); 
+
+
+ML{*ResAtp.problem_name := "Message__parts_cut"*}
+lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
+by (metis Un_subset_iff Un_upper1 Un_upper2 insert_subset parts_Un parts_increasing parts_trans) 
+
+
+
+subsubsection{*Rewrite rules for pulling out atomic messages *}
+
+lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
+
+
+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) 
+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) 
+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) 
+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) 
+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) 
+done
+
+lemma parts_insert_Crypt [simp]:
+     "parts (insert (Crypt K X) H) =  
+          insert (Crypt K X) (parts (insert X H))"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule parts.induct, auto)
+apply (blast intro: parts.Body)
+done
+
+lemma parts_insert_MPair [simp]:
+     "parts (insert {|X,Y|} H) =  
+          insert {|X,Y|} (parts (insert X (insert Y H)))"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule parts.induct, auto)
+apply (blast intro: parts.Fst parts.Snd)+
+done
+
+lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
+apply auto
+apply (erule parts.induct, auto)
+done
+
+
+ML{*ResAtp.problem_name := "Message__msg_Nonce_supply"*}
+lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
+apply (induct_tac "msg") 
+apply (simp_all add: parts_insert2)
+apply (metis Suc_n_not_le_n)
+apply (metis le_trans linorder_linear)
+done
+
+subsection{*Inductive relation "analz"*}
+
+text{*Inductive definition of "analz" -- what can be broken down from a set of
+    messages, including keys.  A form of downward closure.  Pairs can
+    be taken apart; messages decrypted with known keys.  *}
+
+consts  analz   :: "msg set => msg set"
+inductive "analz H"
+  intros 
+    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]: 
+             "[|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) 
+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   
+          |] ==> P"
+by (blast dest: analz.Fst analz.Snd)
+
+lemma analz_increasing: "H \<subseteq> analz(H)"
+by blast
+
+lemma analz_subset_parts: "analz H \<subseteq> parts H"
+apply (rule subsetI)
+apply (erule analz.induct, blast+)
+done
+
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+
+
+ML{*ResAtp.problem_name := "Message__parts_analz"*}
+lemma parts_analz [simp]: "parts (analz H) = parts H"
+apply (rule equalityI)
+apply (metis analz_subset_parts parts_subset_iff)
+apply (metis analz_increasing parts_mono)
+done
+
+
+lemma analz_parts [simp]: "analz (parts H) = parts H"
+apply auto
+apply (erule analz.induct, auto)
+done
+
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+
+subsubsection{*General equational properties *}
+
+lemma analz_empty [simp]: "analz{} = {}"
+apply safe
+apply (erule analz.induct, blast+)
+done
+
+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)
+
+lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+subsubsection{*Rewrite rules for pulling out atomic messages *}
+
+lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
+
+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) 
+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) 
+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) 
+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) 
+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) ==>   
+          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) 
+done
+
+lemma analz_insert_MPair [simp]:
+     "analz (insert {|X,Y|} H) =  
+          insert {|X,Y|} (analz (insert X (insert Y H)))"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule analz.induct, auto)
+apply (erule analz.induct)
+apply (blast intro: analz.Fst analz.Snd)+
+done
+
+text{*Can pull out enCrypted message if the Key is not known*}
+lemma analz_insert_Crypt:
+     "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) 
+
+done
+
+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 xa = x in analz.induct, auto)
+done
+
+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 xa = x in analz.induct, auto)
+apply (blast intro: analz_insertI analz.Decrypt)
+done
+
+lemma analz_insert_Decrypt:
+     "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)"} *} 
+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))  
+           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>   
+           insert (Crypt K X) (analz (insert X H))"
+apply (rule subsetI)
+apply (erule analz.induct, auto)
+done
+
+
+lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
+apply auto
+apply (erule analz.induct, auto)
+done
+
+
+subsubsection{*Idempotence and transitivity *}
+
+lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
+by (erule analz.induct, blast+)
+
+lemma analz_idem [simp]: "analz (analz H) = analz H"
+by blast
+
+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) 
+done
+
+lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
+by (drule analz_mono, blast)
+
+
+ML{*ResAtp.problem_name := "Message__analz_cut"*}
+    declare analz_trans[intro]
+lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
+(*TOO SLOW
+by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) --{*317s*}
+??*)
+by (erule analz_trans, blast)
+
+
+text{*This rewrite rule helps in the simplification of messages that involve
+  the forwarding of unknown components (X).  Without it, removing occurrences
+  of X can be very complicated. *}
+lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
+by (blast intro: analz_cut analz_insertI)
+
+
+text{*A congruence rule for "analz" *}
+
+ML{*ResAtp.problem_name := "Message__analz_subset_cong"*}
+lemma analz_subset_cong:
+     "[| 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)
+done
+
+
+lemma analz_cong:
+     "[| analz G = analz G'; analz H = analz H'  
+               |] ==> analz (G \<union> H) = analz (G' \<union> H')"
+by (intro equalityI analz_subset_cong, simp_all) 
+
+lemma analz_insert_cong:
+     "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
+by (force simp only: insert_def intro!: analz_cong)
+
+text{*If there are no pairs or encryptions then analz does nothing*}
+lemma analz_trivial:
+     "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
+apply safe
+apply (erule analz.induct, blast+)
+done
+
+text{*These two are obsolete (with a single Spy) but cost little to prove...*}
+lemma analz_UN_analz_lemma:
+     "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
+apply (erule analz.induct)
+apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
+done
+
+lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
+by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
+
+
+subsection{*Inductive relation "synth"*}
+
+text{*Inductive definition of "synth" -- what can be built up from a set of
+    messages.  A form of upward closure.  Pairs can be built, messages
+    encrypted with known keys.  Agent names are public domain.
+    Numbers can be guessed, but Nonces cannot be.  *}
+
+consts  synth   :: "msg set => msg set"
+inductive "synth H"
+  intros 
+    Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
+    Agent  [intro]:   "Agent agt \<in> synth H"
+    Number [intro]:   "Number n  \<in> synth H"
+    Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
+    MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
+    Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
+
+text{*Monotonicity*}
+lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
+  by (auto, erule synth.induct, auto)  
+
+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"
+inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
+inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
+inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
+
+
+lemma synth_increasing: "H \<subseteq> synth(H)"
+by blast
+
+subsubsection{*Unions *}
+
+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)
+
+
+ML{*ResAtp.problem_name := "Message__synth_insert"*}
+ 
+lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
+by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)
+
+subsubsection{*Idempotence and transitivity *}
+
+lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
+by (erule synth.induct, blast+)
+
+lemma synth_idem: "synth (synth H) = synth H"
+by blast
+
+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) 
+done
+
+lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
+by (drule synth_mono, blast)
+
+ML{*ResAtp.problem_name := "Message__synth_cut"*}
+lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
+(*TOO SLOW
+by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)
+*)
+by (erule synth_trans, blast)
+
+
+lemma Agent_synth [simp]: "Agent A \<in> synth H"
+by blast
+
+lemma Number_synth [simp]: "Number n \<in> synth H"
+by blast
+
+lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
+by blast
+
+lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
+by blast
+
+lemma Crypt_synth_eq [simp]:
+     "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
+by blast
+
+
+lemma keysFor_synth [simp]: 
+    "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
+by (unfold keysFor_def, blast)
+
+
+subsubsection{*Combinations of parts, analz and synth *}
+
+ML{*ResAtp.problem_name := "Message__parts_synth"*}
+lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule parts.induct)
+apply (metis UnCI)
+apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Fst parts_increasing)
+apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Snd parts_increasing)
+apply (metis Body Crypt_synth UnCI UnE insert_absorb insert_subset parts_increasing)
+apply (metis Un_subset_iff parts_increasing parts_mono synth_increasing)
+done
+
+
+
+
+ML{*ResAtp.problem_name := "Message__analz_analz_Un"*}
+lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
+apply (rule equalityI);
+apply (metis analz_idem analz_subset_cong order_eq_refl)
+apply (metis analz_increasing analz_subset_cong order_eq_refl)
+done
+
+ML{*ResAtp.problem_name := "Message__analz_synth_Un"*}
+    declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
+lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule analz.induct)
+apply (metis UnCI UnE Un_commute analz.Inj)
+apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Fst analz_increasing analz_mono insert_absorb insert_subset)
+apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Snd analz_increasing analz_mono insert_absorb insert_subset)
+apply (blast intro: analz.Decrypt)
+apply (metis Diff_Int Diff_empty Diff_subset_conv Int_empty_right Un_commute Un_subset_iff Un_upper1 analz_increasing analz_mono synth_increasing)
+done
+
+
+ML{*ResAtp.problem_name := "Message__analz_synth"*}
+lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
+proof (neg_clausify)
+assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
+have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
+  by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)
+have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
+  by (metis 0 sup_set_eq)
+have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
+  by (metis 1 Un_commute sup_set_eq sup_set_eq)
+have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
+  by (metis 3 Un_empty_right sup_set_eq)
+have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
+  by (metis 4 Un_empty_right sup_set_eq)
+have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
+  by (metis 5 Un_commute sup_set_eq sup_set_eq)
+show "False"
+  by (metis 2 6)
+qed
+
+
+subsubsection{*For reasoning about the Fake rule in traces *}
+
+ML{*ResAtp.problem_name := "Message__parts_insert_subset_Un"*}
+lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
+proof (neg_clausify)
+assume 0: "X \<in> G"
+assume 1: "\<not> parts (insert X H) \<subseteq> parts G \<union> parts H"
+have 2: "\<not> parts (insert X H) \<subseteq> parts (G \<union> H)"
+  by (metis 1 parts_Un)
+have 3: "\<not> insert X H \<subseteq> G \<union> H"
+  by (metis 2 parts_mono)
+have 4: "X \<notin> G \<union> H \<or> \<not> H \<subseteq> G \<union> H"
+  by (metis 3 insert_subset)
+have 5: "X \<notin> G \<union> H"
+  by (metis 4 Un_upper2)
+have 6: "X \<notin> G"
+  by (metis 5 UnCI)
+show "False"
+  by (metis 6 0)
+qed
+
+ML{*ResAtp.problem_name := "Message__Fake_parts_insert"*}
+lemma Fake_parts_insert:
+     "X \<in> synth (analz H) ==>  
+      parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
+proof (neg_clausify)
+assume 0: "X \<in> synth (analz H)"
+assume 1: "\<not> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
+have 2: "\<And>X3. parts X3 \<union> synth (analz X3) = parts (synth (analz X3))"
+  by (metis parts_synth parts_analz)
+have 3: "\<And>X3. analz X3 \<union> synth (analz X3) = analz (synth (analz X3))"
+  by (metis analz_synth analz_idem)
+have 4: "\<And>X3. analz X3 \<subseteq> analz (synth X3)"
+  by (metis Un_upper1 analz_synth)
+have 5: "\<not> parts (insert X H) \<subseteq> parts H \<union> synth (analz H)"
+  by (metis 1 Un_commute)
+have 6: "\<not> parts (insert X H) \<subseteq> parts (synth (analz H))"
+  by (metis 5 2)
+have 7: "\<not> insert X H \<subseteq> synth (analz H)"
+  by (metis 6 parts_mono)
+have 8: "X \<notin> synth (analz H) \<or> \<not> H \<subseteq> synth (analz H)"
+  by (metis 7 insert_subset)
+have 9: "\<not> H \<subseteq> synth (analz H)"
+  by (metis 8 0)
+have 10: "\<And>X3. X3 \<subseteq> analz (synth X3)"
+  by (metis analz_subset_iff 4)
+have 11: "\<And>X3. X3 \<subseteq> analz (synth (analz X3))"
+  by (metis analz_subset_iff 10)
+have 12: "\<And>X3. analz (synth (analz X3)) = synth (analz X3) \<or>
+     \<not> analz X3 \<subseteq> synth (analz X3)"
+  by (metis Un_absorb1 3)
+have 13: "\<And>X3. analz (synth (analz X3)) = synth (analz X3)"
+  by (metis 12 synth_increasing)
+have 14: "\<And>X3. X3 \<subseteq> synth (analz X3)"
+  by (metis 11 13)
+show "False"
+  by (metis 9 14)
+qed
+
+lemma Fake_parts_insert_in_Un:
+     "[|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])
+
+ML{*ResAtp.problem_name := "Message__Fake_analz_insert"*}
+    declare analz_mono [intro] synth_mono [intro] 
+lemma Fake_analz_insert:
+     "X\<in> synth (analz G) ==>  
+      analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
+by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un analz_mono analz_synth_Un equalityE insert_absorb order_le_less xt1(12))
+
+ML{*ResAtp.problem_name := "Message__Fake_analz_insert_simpler"*}
+(*simpler problems?  BUT METIS CAN'T PROVE
+lemma Fake_analz_insert_simpler:
+     "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) ")
+apply (metis Un_commute analz_analz_Un analz_synth_Un)
+apply (metis Un_commute Un_upper1 Un_upper2 analz_cut analz_increasing analz_mono insert_absorb insert_mono insert_subset)
+done
+*)
+
+end
diff -r 020381339d87 -r dd874e6a3282 src/HOL/MetisExamples/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MetisExamples/ROOT.ML	Thu Jun 21 13:23:33 2007 +0200
@@ -0,0 +1,14 @@
+(*  Title:      HOL/MetisExamples/ROOT.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Testing the metis method
+*)
+
+time_use_thy "set";
+time_use_thy "BigO";
+time_use_thy "Abstraction";
+time_use_thy "BT";
+time_use_thy "Message";
+time_use_thy "Tarski";
+time_use_thy "TransClosure";
diff -r 020381339d87 -r dd874e6a3282 src/HOL/MetisExamples/Tarski.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MetisExamples/Tarski.thy	Thu Jun 21 13:23:33 2007 +0200
@@ -0,0 +1,1103 @@
+(*  Title:      HOL/MetisTest/Tarski.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Testing the metis method
+*)
+
+header {* The Full Theorem of Tarski *}
+
+theory Tarski imports FuncSet begin
+
+(*Many of these higher-order problems appear to be impossible using the
+current linkup. They often seem to need either higher-order unification
+or explicit reasoning about connectives such as conjunction. The numerous
+set comprehensions are to blame.*)
+
+
+record 'a potype =
+  pset  :: "'a set"
+  order :: "('a * 'a) set"
+
+constdefs
+  monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
+  "monotone f A r == \<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r"
+
+  least :: "['a => bool, 'a potype] => 'a"
+  "least P po == @ x. x: pset po & P x &
+                       (\<forall>y \<in> pset po. P y --> (x,y): order po)"
+
+  greatest :: "['a => bool, 'a potype] => 'a"
+  "greatest P po == @ x. x: pset po & P x &
+                          (\<forall>y \<in> pset po. P y --> (y,x): order po)"
+
+  lub  :: "['a set, 'a potype] => 'a"
+  "lub S po == least (%x. \<forall>y\<in>S. (y,x): order po) po"
+
+  glb  :: "['a set, 'a potype] => 'a"
+  "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
+
+  isLub :: "['a set, 'a potype, 'a] => bool"
+  "isLub S po == %L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
+                   (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po))"
+
+  isGlb :: "['a set, 'a potype, 'a] => bool"
+  "isGlb S po == %G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
+                 (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po))"
+
+  "fix"    :: "[('a => 'a), 'a set] => 'a set"
+  "fix f A  == {x. x: A & f x = x}"
+
+  interval :: "[('a*'a) set,'a, 'a ] => 'a set"
+  "interval r a b == {x. (a,x): r & (x,b): r}"
+
+declare monotone_def [skolem]
+        lub_def [skolem]
+        glb_def [skolem]
+        isLub_def [skolem]
+        isGlb_def [skolem]
+        fix_def [skolem]
+        interval_def [skolem]
+
+constdefs
+  Bot :: "'a potype => 'a"
+  "Bot po == least (%x. True) po"
+
+  Top :: "'a potype => 'a"
+  "Top po == greatest (%x. True) po"
+
+  PartialOrder :: "('a potype) set"
+  "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) &
+                       trans (order P)}"
+
+  CompleteLattice :: "('a potype) set"
+  "CompleteLattice == {cl. cl: PartialOrder &
+                        (\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) &
+                        (\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}"
+
+  CLF :: "('a potype * ('a => 'a)) set"
+  "CLF == SIGMA cl: CompleteLattice.
+            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)}"
+
+  induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
+  "induced A r == {(a,b). a : A & b: A & (a,b): r}"
+
+declare Bot_def [skolem]
+        Top_def [skolem]
+        PartialOrder_def [skolem]
+        CompleteLattice_def [skolem]
+        CLF_def [skolem]
+
+constdefs
+  sublattice :: "('a potype * 'a set)set"
+  "sublattice ==
+      SIGMA cl: CompleteLattice.
+          {S. S \<subseteq> pset cl &
+           (| pset = S, order = induced S (order cl) |): CompleteLattice }"
+
+syntax
+  "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
+
+translations
+  "S <<= cl" == "S : sublattice `` {cl}"
+
+constdefs
+  dual :: "'a potype => 'a potype"
+  "dual po == (| pset = pset po, order = converse (order po) |)"
+
+locale (open) PO =
+  fixes cl :: "'a potype"
+    and A  :: "'a set"
+    and r  :: "('a * 'a) set"
+  assumes cl_po:  "cl : PartialOrder"
+  defines A_def: "A == pset cl"
+     and  r_def: "r == order cl"
+
+locale (open) CL = PO +
+  assumes cl_co:  "cl : CompleteLattice"
+
+locale (open) CLF = CL +
+  fixes f :: "'a => 'a"
+    and P :: "'a set"
+  assumes f_cl:  "(cl,f) : CLF" (*was the equivalent "f : CLF``{cl}"*)
+  defines P_def: "P == fix f A"
+
+
+locale (open) Tarski = CLF +
+  fixes Y     :: "'a set"
+    and intY1 :: "'a set"
+    and v     :: "'a"
+  assumes
+    Y_ss: "Y \<subseteq> P"
+  defines
+    intY1_def: "intY1 == interval r (lub Y cl) (Top cl)"
+    and v_def: "v == glb {x. ((%x: intY1. f x) x, x): induced intY1 r &
+                             x: intY1}
+                      (| pset=intY1, order=induced intY1 r|)"
+
+
+subsection {* Partial Order *}
+
+lemma (in PO) PO_imp_refl: "refl A r"
+apply (insert cl_po)
+apply (simp add: PartialOrder_def A_def r_def)
+done
+
+lemma (in PO) PO_imp_sym: "antisym r"
+apply (insert cl_po)
+apply (simp add: PartialOrder_def r_def)
+done
+
+lemma (in PO) PO_imp_trans: "trans r"
+apply (insert cl_po)
+apply (simp add: PartialOrder_def r_def)
+done
+
+lemma (in PO) reflE: "x \<in> A ==> (x, x) \<in> r"
+apply (insert cl_po)
+apply (simp add: PartialOrder_def refl_def A_def r_def)
+done
+
+lemma (in PO) antisymE: "[| (a, b) \<in> r; (b, a) \<in> r |] ==> a = b"
+apply (insert cl_po)
+apply (simp add: PartialOrder_def antisym_def r_def)
+done
+
+lemma (in PO) transE: "[| (a, b) \<in> r; (b, c) \<in> r|] ==> (a,c) \<in> r"
+apply (insert cl_po)
+apply (simp add: PartialOrder_def r_def)
+apply (unfold trans_def, fast)
+done
+
+lemma (in PO) monotoneE:
+     "[| monotone f A r;  x \<in> A; y \<in> A; (x, y) \<in> r |] ==> (f x, f y) \<in> r"
+by (simp add: monotone_def)
+
+lemma (in PO) po_subset_po:
+     "S \<subseteq> A ==> (| pset = S, order = induced S r |) \<in> PartialOrder"
+apply (simp (no_asm) add: PartialOrder_def)
+apply auto
+-- {* refl *}
+apply (simp add: refl_def induced_def)
+apply (blast intro: reflE)
+-- {* antisym *}
+apply (simp add: antisym_def induced_def)
+apply (blast intro: antisymE)
+-- {* trans *}
+apply (simp add: trans_def induced_def)
+apply (blast intro: transE)
+done
+
+lemma (in PO) indE: "[| (x, y) \<in> induced S r; S \<subseteq> A |] ==> (x, y) \<in> r"
+by (simp add: add: induced_def)
+
+lemma (in PO) indI: "[| (x, y) \<in> r; x \<in> S; y \<in> S |] ==> (x, y) \<in> induced S r"
+by (simp add: add: induced_def)
+
+lemma (in CL) CL_imp_ex_isLub: "S \<subseteq> A ==> \<exists>L. isLub S cl L"
+apply (insert cl_co)
+apply (simp add: CompleteLattice_def A_def)
+done
+
+declare (in CL) cl_co [simp]
+
+lemma isLub_lub: "(\<exists>L. isLub S cl L) = isLub S cl (lub S cl)"
+by (simp add: lub_def least_def isLub_def some_eq_ex [symmetric])
+
+declare isLub_lub [skolem]
+
+lemma isGlb_glb: "(\<exists>G. isGlb S cl G) = isGlb S cl (glb S cl)"
+by (simp add: glb_def greatest_def isGlb_def some_eq_ex [symmetric])
+
+declare isGlb_glb [skolem]
+
+lemma isGlb_dual_isLub: "isGlb S cl = isLub S (dual cl)"
+by (simp add: isLub_def isGlb_def dual_def converse_def)
+
+lemma isLub_dual_isGlb: "isLub S cl = isGlb S (dual cl)"
+by (simp add: isLub_def isGlb_def dual_def converse_def)
+
+lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
+apply (insert cl_po)
+apply (simp add: PartialOrder_def dual_def refl_converse
+                 trans_converse antisym_converse)
+done
+
+lemma Rdual:
+     "\<forall>S. (S \<subseteq> A -->( \<exists>L. isLub S (| pset = A, order = r|) L))
+      ==> \<forall>S. (S \<subseteq> A --> (\<exists>G. isGlb S (| pset = A, order = r|) G))"
+apply safe
+apply (rule_tac x = "lub {y. y \<in> A & (\<forall>k \<in> S. (y, k) \<in> r)}
+                      (|pset = A, order = r|) " in exI)
+apply (drule_tac x = "{y. y \<in> A & (\<forall>k \<in> S. (y,k) \<in> r) }" in spec)
+apply (drule mp, fast)
+apply (simp add: isLub_lub isGlb_def)
+apply (simp add: isLub_def, blast)
+done
+
+declare Rdual [skolem]
+
+lemma lub_dual_glb: "lub S cl = glb S (dual cl)"
+by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def)
+
+lemma glb_dual_lub: "glb S cl = lub S (dual cl)"
+by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def)
+
+lemma CL_subset_PO: "CompleteLattice \<subseteq> PartialOrder"
+by (simp add: PartialOrder_def CompleteLattice_def, fast)
+
+lemmas CL_imp_PO = CL_subset_PO [THEN subsetD]
+
+declare CL_imp_PO [THEN PO.PO_imp_refl, simp]
+declare CL_imp_PO [THEN PO.PO_imp_sym, simp]
+declare CL_imp_PO [THEN PO.PO_imp_trans, simp]
+
+lemma (in CL) CO_refl: "refl A r"
+by (rule PO_imp_refl)
+
+lemma (in CL) CO_antisym: "antisym r"
+by (rule PO_imp_sym)
+
+lemma (in CL) CO_trans: "trans r"
+by (rule PO_imp_trans)
+
+lemma CompleteLatticeI:
+     "[| po \<in> PartialOrder; (\<forall>S. S \<subseteq> pset po --> (\<exists>L. isLub S po L));
+         (\<forall>S. S \<subseteq> pset po --> (\<exists>G. isGlb S po G))|]
+      ==> po \<in> CompleteLattice"
+apply (unfold CompleteLattice_def, blast)
+done
+
+declare CompleteLatticeI [skolem]
+
+lemma (in CL) CL_dualCL: "dual cl \<in> CompleteLattice"
+apply (insert cl_co)
+apply (simp add: CompleteLattice_def dual_def)
+apply (fold dual_def)
+apply (simp add: isLub_dual_isGlb [symmetric] isGlb_dual_isLub [symmetric]
+                 dualPO)
+done
+
+lemma (in PO) dualA_iff: "pset (dual cl) = pset cl"
+by (simp add: dual_def)
+
+lemma (in PO) dualr_iff: "((x, y) \<in> (order(dual cl))) = ((y, x) \<in> order cl)"
+by (simp add: dual_def)
+
+lemma (in PO) monotone_dual:
+     "monotone f (pset cl) (order cl) 
+     ==> monotone f (pset (dual cl)) (order(dual cl))"
+by (simp add: monotone_def dualA_iff dualr_iff)
+
+lemma (in PO) interval_dual:
+     "[| x \<in> A; y \<in> A|] ==> interval r x y = interval (order(dual cl)) y x"
+apply (simp add: interval_def dualr_iff)
+apply (fold r_def, fast)
+done
+
+lemma (in PO) interval_not_empty:
+     "[| trans r; interval r a b \<noteq> {} |] ==> (a, b) \<in> r"
+apply (simp add: interval_def)
+apply (unfold trans_def, blast)
+done
+
+lemma (in PO) interval_imp_mem: "x \<in> interval r a b ==> (a, x) \<in> r"
+by (simp add: interval_def)
+
+lemma (in PO) left_in_interval:
+     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] ==> a \<in> interval r a b"
+apply (simp (no_asm_simp) add: interval_def)
+apply (simp add: PO_imp_trans interval_not_empty)
+apply (simp add: reflE)
+done
+
+lemma (in PO) right_in_interval:
+     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] ==> b \<in> interval r a b"
+apply (simp (no_asm_simp) add: interval_def)
+apply (simp add: PO_imp_trans interval_not_empty)
+apply (simp add: reflE)
+done
+
+
+subsection {* sublattice *}
+
+lemma (in PO) sublattice_imp_CL:
+     "S <<= cl  ==> (| pset = S, order = induced S r |) \<in> CompleteLattice"
+by (simp add: sublattice_def CompleteLattice_def A_def r_def)
+
+lemma (in CL) sublatticeI:
+     "[| S \<subseteq> A; (| pset = S, order = induced S r |) \<in> CompleteLattice |]
+      ==> S <<= cl"
+by (simp add: sublattice_def A_def r_def)
+
+
+subsection {* lub *}
+
+lemma (in CL) lub_unique: "[| S \<subseteq> A; isLub S cl x; isLub S cl L|] ==> x = L"
+apply (rule antisymE)
+apply (auto simp add: isLub_def r_def)
+done
+
+lemma (in CL) lub_upper: "[|S \<subseteq> A; x \<in> S|] ==> (x, lub S cl) \<in> r"
+apply (rule CL_imp_ex_isLub [THEN exE], assumption)
+apply (unfold lub_def least_def)
+apply (rule some_equality [THEN ssubst])
+  apply (simp add: isLub_def)
+ apply (simp add: lub_unique A_def isLub_def)
+apply (simp add: isLub_def r_def)
+done
+
+lemma (in CL) lub_least:
+     "[| S \<subseteq> A; L \<in> A; \<forall>x \<in> S. (x,L) \<in> r |] ==> (lub S cl, L) \<in> r"
+apply (rule CL_imp_ex_isLub [THEN exE], assumption)
+apply (unfold lub_def least_def)
+apply (rule_tac s=x in some_equality [THEN ssubst])
+  apply (simp add: isLub_def)
+ apply (simp add: lub_unique A_def isLub_def)
+apply (simp add: isLub_def r_def A_def)
+done
+
+lemma (in CL) lub_in_lattice: "S \<subseteq> A ==> lub S cl \<in> A"
+apply (rule CL_imp_ex_isLub [THEN exE], assumption)
+apply (unfold lub_def least_def)
+apply (subst some_equality)
+apply (simp add: isLub_def)
+prefer 2 apply (simp add: isLub_def A_def)
+apply (simp add: lub_unique A_def isLub_def)
+done
+
+lemma (in CL) lubI:
+     "[| S \<subseteq> A; L \<in> A; \<forall>x \<in> S. (x,L) \<in> r;
+         \<forall>z \<in> A. (\<forall>y \<in> S. (y,z) \<in> r) --> (L,z) \<in> r |] ==> L = lub S cl"
+apply (rule lub_unique, assumption)
+apply (simp add: isLub_def A_def r_def)
+apply (unfold isLub_def)
+apply (rule conjI)
+apply (fold A_def r_def)
+apply (rule lub_in_lattice, assumption)
+apply (simp add: lub_upper lub_least)
+done
+
+declare (in CL) lubI [skolem]
+
+lemma (in CL) lubIa: "[| S \<subseteq> A; isLub S cl L |] ==> L = lub S cl"
+by (simp add: lubI isLub_def A_def r_def)
+
+lemma (in CL) isLub_in_lattice: "isLub S cl L ==> L \<in> A"
+by (simp add: isLub_def  A_def)
+
+lemma (in CL) isLub_upper: "[|isLub S cl L; y \<in> S|] ==> (y, L) \<in> r"
+by (simp add: isLub_def r_def)
+
+lemma (in CL) isLub_least:
+     "[| isLub S cl L; z \<in> A; \<forall>y \<in> S. (y, z) \<in> r|] ==> (L, z) \<in> r"
+by (simp add: isLub_def A_def r_def)
+
+lemma (in CL) isLubI:
+     "[| L \<in> A; \<forall>y \<in> S. (y, L) \<in> r;
+         (\<forall>z \<in> A. (\<forall>y \<in> S. (y, z):r) --> (L, z) \<in> r)|] ==> isLub S cl L"
+by (simp add: isLub_def A_def r_def)
+
+declare (in CL) isLub_least [skolem]
+declare (in CL) isLubI [skolem]
+
+
+subsection {* glb *}
+
+lemma (in CL) glb_in_lattice: "S \<subseteq> A ==> glb S cl \<in> A"
+apply (subst glb_dual_lub)
+apply (simp add: A_def)
+apply (rule dualA_iff [THEN subst])
+apply (rule CL.lub_in_lattice)
+apply (rule dualPO)
+apply (rule CL_dualCL)
+apply (simp add: dualA_iff)
+done
+
+lemma (in CL) glb_lower: "[|S \<subseteq> A; x \<in> S|] ==> (glb S cl, x) \<in> r"
+apply (subst glb_dual_lub)
+apply (simp add: r_def)
+apply (rule dualr_iff [THEN subst])
+apply (rule CL.lub_upper)
+apply (rule dualPO)
+apply (rule CL_dualCL)
+apply (simp add: dualA_iff A_def, assumption)
+done
+
+text {*
+  Reduce the sublattice property by using substructural properties;
+  abandoned see @{text "Tarski_4.ML"}.
+*}
+
+declare (in CLF) f_cl [simp]
+
+(*never proved, 2007-01-22: Tarski__CLF_unnamed_lemma
+  NOT PROVABLE because of the conjunction used in the definition: we don't
+  allow reasoning with rules like conjE, which is essential here.*)
+ML{*ResAtp.problem_name:="Tarski__CLF_unnamed_lemma"*}
+lemma (in CLF) [simp]:
+    "f: pset cl -> pset cl & monotone f (pset cl) (order cl)" 
+apply (insert f_cl)
+apply (unfold CLF_def)
+apply (erule SigmaE2) 
+apply (erule CollectE) 
+apply assumption; 
+done
+
+lemma (in CLF) f_in_funcset: "f \<in> A -> A"
+by (simp add: A_def)
+
+lemma (in CLF) monotone_f: "monotone f A r"
+by (simp add: A_def r_def)
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__CLF_CLF_dual"*}
+  declare (in CLF) CLF_def[simp] CL_dualCL[simp] monotone_dual[simp] dualA_iff[simp]
+lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF" 
+apply (simp del: dualA_iff)
+apply (simp)
+done
+  declare  (in CLF) CLF_def[simp del] CL_dualCL[simp del] monotone_dual[simp del]
+          dualA_iff[simp del]
+
+
+subsection {* fixed points *}
+
+lemma fix_subset: "fix f A \<subseteq> A"
+by (simp add: fix_def, fast)
+
+lemma fix_imp_eq: "x \<in> fix f A ==> f x = x"
+by (simp add: fix_def)
+
+lemma fixf_subset:
+     "[| A \<subseteq> B; x \<in> fix (%y: A. f y) A |] ==> x \<in> fix f B"
+by (simp add: fix_def, auto)
+
+
+subsection {* lemmas for Tarski, lub *}
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="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] 
+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)
+apply (rule f_in_funcset [THEN funcset_mem])
+apply (rule lub_in_lattice, fast)
+-- {* @{text "\<forall>x:H. (x, f (lub H r)) \<in> r"} *}
+apply (rule ballI)
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__CLF_lubH_le_flubH_simpler"*}
+apply (rule transE)
+-- {* instantiates @{text "(x, ?z) \<in> order cl to (x, f x)"}, *}
+-- {* because of the def of @{text H} *}
+apply fast
+-- {* so it remains to show @{text "(f x, f (lub H cl)) \<in> r"} *}
+apply (rule_tac f = "f" in monotoneE)
+apply (rule monotone_f, fast)
+apply (rule lub_in_lattice, fast)
+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] 
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="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] 
+       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"
+apply (rule lub_upper, fast)
+apply (rule_tac t = "H" in ssubst, assumption)
+apply (rule CollectI)
+apply (rule conjI)
+ML{*ResAtp.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*} 
+apply (metis CO_refl lubH_le_flubH lub_dual_glb monotoneE monotone_f reflD1 reflD2)
+apply (metis CO_refl lubH_le_flubH reflD2)
+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] 
+          CLF.lubH_le_flubH[simp del]
+
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__CLF_lubH_is_fixp"*}
+(*Single-step version fails. The conjecture clauses refer to local abstraction
+functions (Frees), which prevents expand_defs_tac from removing those 
+"definitions" at the end of the proof. 
+lemma (in CLF) lubH_is_fixp:
+     "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
+apply (simp add: fix_def)
+apply (rule conjI)
+ proof (neg_clausify)
+assume 0: "H = Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)"
+assume 1: "lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl \<notin> A"
+have 2: "glb H (dual cl) \<notin> A"
+  by (metis 0 1 lub_dual_glb)
+have 3: "(glb H (dual cl), f (glb H (dual cl))) \<in> r"
+  by (metis 0 lubH_le_flubH lub_dual_glb)
+have 4: "(f (glb H (dual cl)), glb H (dual cl)) \<in> r"
+  by (metis 0 flubH_le_lubH lub_dual_glb)
+have 5: "glb H (dual cl) = f (glb H (dual cl)) \<or>
+(glb H (dual cl), f (glb H (dual cl))) \<notin> r"
+  by (metis 4 antisymE)
+have 6: "glb H (dual cl) = f (glb H (dual cl))"
+  by (metis 3 5)
+have 7: "(glb H (dual cl), glb H (dual cl)) \<in> r"
+  by (metis 4 6)
+have 8: "\<And>X1. glb H (dual cl) \<in> X1 \<or> \<not> refl X1 r"
+  by (metis reflD2 7)
+have 9: "\<not> refl A r"
+  by (metis 2 8)
+show "False"
+  by (metis 9 CO_refl)
+proof (neg_clausify)
+assume 0: "H = Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)"
+assume 1: "f (lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl) \<noteq>
+lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl"
+have 2: "(glb H (dual cl), f (glb H (dual cl))) \<in> r"
+  by (metis 0 lubH_le_flubH lub_dual_glb lub_dual_glb)
+have 3: "f (glb H (dual cl)) \<noteq> glb H (dual cl)"
+  by (metis 0 1 lub_dual_glb)
+have 4: "(f (glb H (dual cl)), glb H (dual cl)) \<in> r"
+  by (metis lub_dual_glb flubH_le_lubH 0)
+have 5: "f (glb H (dual cl)) = glb H (dual cl) \<or>
+(f (glb H (dual cl)), glb H (dual cl)) \<notin> r"
+  by (metis antisymE 2)
+have 6: "f (glb H (dual cl)) = glb H (dual cl)"
+  by (metis 5 4)
+show "False"
+  by (metis 3 6)
+*)
+
+lemma (in CLF) lubH_is_fixp:
+     "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
+apply (simp add: fix_def)
+apply (rule conjI)
+ML{*ResAtp.problem_name:="Tarski__CLF_lubH_is_fixp_simpler"*} 
+apply (metis CO_refl Domain_iff lubH_le_flubH reflD1)
+apply (metis antisymE flubH_le_lubH lubH_le_flubH)
+done
+
+lemma (in CLF) fix_in_H:
+     "[| H = {x. (x, f x) \<in> r & x \<in> A};  x \<in> P |] ==> x \<in> H"
+by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl
+                    fix_subset [of f A, THEN subsetD])
+
+
+lemma (in CLF) fixf_le_lubH:
+     "H = {x. (x, f x) \<in> r & x \<in> A} ==> \<forall>x \<in> fix f A. (x, lub H cl) \<in> r"
+apply (rule ballI)
+apply (rule lub_upper, fast)
+apply (rule fix_in_H)
+apply (simp_all add: P_def)
+done
+
+ML{*ResAtp.problem_name:="Tarski__CLF_lubH_least_fixf"*}
+lemma (in CLF) lubH_least_fixf:
+     "H = {x. (x, f x) \<in> r & x \<in> A}
+      ==> \<forall>L. (\<forall>y \<in> fix f A. (y,L) \<in> r) --> (lub H cl, L) \<in> r"
+apply (metis P_def lubH_is_fixp)
+done
+
+subsection {* Tarski fixpoint theorem 1, first part *}
+ML{*ResAtp.problem_name:="Tarski__CLF_T_thm_1_lub"*}
+  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;*)
+apply (rule sym)
+apply (simp add: P_def)
+apply (rule lubI)
+ML{*ResAtp.problem_name:="Tarski__CLF_T_thm_1_lub_simpler"*}
+apply (metis P_def equalityE fix_subset subset_trans) 
+apply (metis P_def fix_subset lubH_is_fixp set_mp subset_refl subset_trans)
+apply (metis P_def fixf_le_lubH)
+apply (metis P_def lubH_is_fixp)
+done
+  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*)
+ML{*ResAtp.problem_name:="Tarski__CLF_glbH_is_fixp"*}
+  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 *}
+(*sledgehammer;*)
+apply (simp add: glb_dual_lub P_def A_def r_def)
+apply (rule dualA_iff [THEN subst])
+apply (rule CLF.lubH_is_fixp)
+apply (rule dualPO)
+apply (rule CL_dualCL)
+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] 
+          PO.dualPO[rule del] CL.CL_dualCL[rule del] PO.dualr_iff[simp del]
+
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__T_thm_1_glb"*}  (*ALL THEOREMS*)
+lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \<in> r & x \<in> A} cl"
+(*sledgehammer;*)
+apply (simp add: glb_dual_lub P_def A_def r_def)
+apply (rule dualA_iff [THEN subst])
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__T_thm_1_glb_simpler"*}  (*ALL THEOREMS*)
+(*sledgehammer;*)
+apply (simp add: CLF.T_thm_1_lub [of _ f, OF dualPO CL_dualCL]
+                 dualPO CL_dualCL CLF_dual dualr_iff)
+done
+
+subsection {* interval *}
+
+
+ML{*ResAtp.problem_name:="Tarski__rel_imp_elem"*}
+  declare (in CLF) CO_refl[simp] refl_def [simp]
+lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
+apply (metis CO_refl reflD1)
+done
+  declare (in CLF) CO_refl[simp del]  refl_def [simp del]
+
+ML{*ResAtp.problem_name:="Tarski__interval_subset"*}
+  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"
+apply (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def)
+done
+  declare (in CLF) rel_imp_elem[rule del] 
+  declare interval_def [simp del]
+
+
+
+lemma (in CLF) intervalI:
+     "[| (a, x) \<in> r; (x, b) \<in> r |] ==> x \<in> interval r a b"
+by (simp add: interval_def)
+
+lemma (in CLF) interval_lemma1:
+     "[| S \<subseteq> interval r a b; x \<in> S |] ==> (a, x) \<in> r"
+by (unfold interval_def, fast)
+
+lemma (in CLF) interval_lemma2:
+     "[| S \<subseteq> interval r a b; x \<in> S |] ==> (x, b) \<in> r"
+by (unfold interval_def, fast)
+
+lemma (in CLF) a_less_lub:
+     "[| S \<subseteq> A; S \<noteq> {};
+         \<forall>x \<in> S. (a,x) \<in> r; \<forall>y \<in> S. (y, L) \<in> r |] ==> (a,L) \<in> r"
+by (blast intro: transE)
+
+declare (in CLF) a_less_lub [skolem]
+
+lemma (in CLF) glb_less_b:
+     "[| S \<subseteq> A; S \<noteq> {};
+         \<forall>x \<in> S. (x,b) \<in> r; \<forall>y \<in> S. (G, y) \<in> r |] ==> (G,b) \<in> r"
+by (blast intro: transE)
+
+declare (in CLF) glb_less_b [skolem]
+
+lemma (in CLF) S_intv_cl:
+     "[| a \<in> A; b \<in> A; S \<subseteq> interval r a b |]==> S \<subseteq> A"
+by (simp add: subset_trans [OF _ interval_subset])
+
+ML{*ResAtp.problem_name:="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" 
+(*WON'T TERMINATE
+apply (metis CO_trans intervalI interval_lemma1 interval_lemma2 isLub_least isLub_upper subset_empty subset_iff trans_def)
+*)
+apply (rule intervalI)
+apply (rule a_less_lub)
+prefer 2 apply assumption
+apply (simp add: S_intv_cl)
+apply (rule ballI)
+apply (simp add: interval_lemma1)
+apply (simp add: isLub_upper)
+-- {* @{text "(L, b) \<in> r"} *}
+apply (simp add: isLub_least interval_lemma2)
+done
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__G_in_interval"*}  (*ALL THEOREMS*)
+lemma (in CLF) G_in_interval:
+     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G;
+         S \<noteq> {} |] ==> G \<in> interval r a b"
+apply (simp add: interval_dual)
+apply (simp add: CLF.L_in_interval [of _ f]
+                 dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub)
+done
+
+ML{*ResAtp.problem_name:="Tarski__intervalPO"*}  (*ALL THEOREMS*)
+lemma (in CLF) intervalPO:
+     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |]
+      ==> (| pset = interval r a b, order = induced (interval r a b) r |)
+          \<in> PartialOrder"
+proof (neg_clausify)
+assume 0: "a \<in> A"
+assume 1: "b \<in> A"
+assume 2: "\<lparr>pset = interval r a b, order = induced (interval r a b) r\<rparr> \<notin> PartialOrder"
+have 3: "\<not> interval r a b \<subseteq> A"
+  by (metis 2 po_subset_po)
+have 4: "b \<notin> A \<or> a \<notin> A"
+  by (metis 3 interval_subset)
+have 5: "a \<notin> A"
+  by (metis 4 1)
+show "False"
+  by (metis 5 0)
+qed
+
+lemma (in CLF) intv_CL_lub:
+ "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |]
+  ==> \<forall>S. S \<subseteq> interval r a b -->
+          (\<exists>L. isLub S (| pset = interval r a b,
+                          order = induced (interval r a b) r |)  L)"
+apply (intro strip)
+apply (frule S_intv_cl [THEN CL_imp_ex_isLub])
+prefer 2 apply assumption
+apply assumption
+apply (erule exE)
+-- {* define the lub for the interval as *}
+apply (rule_tac x = "if S = {} then a else L" in exI)
+apply (simp (no_asm_simp) add: isLub_def split del: split_if)
+apply (intro impI conjI)
+-- {* @{text "(if S = {} then a else L) \<in> interval r a b"} *}
+apply (simp add: CL_imp_PO L_in_interval)
+apply (simp add: left_in_interval)
+-- {* lub prop 1 *}
+apply (case_tac "S = {}")
+-- {* @{text "S = {}, y \<in> S = False => everything"} *}
+apply fast
+-- {* @{text "S \<noteq> {}"} *}
+apply simp
+-- {* @{text "\<forall>y:S. (y, L) \<in> induced (interval r a b) r"} *}
+apply (rule ballI)
+apply (simp add: induced_def  L_in_interval)
+apply (rule conjI)
+apply (rule subsetD)
+apply (simp add: S_intv_cl, assumption)
+apply (simp add: isLub_upper)
+-- {* @{text "\<forall>z:interval r a b. (\<forall>y:S. (y, z) \<in> induced (interval r a b) r \<longrightarrow> (if S = {} then a else L, z) \<in> induced (interval r a b) r"} *}
+apply (rule ballI)
+apply (rule impI)
+apply (case_tac "S = {}")
+-- {* @{text "S = {}"} *}
+apply simp
+apply (simp add: induced_def  interval_def)
+apply (rule conjI)
+apply (rule reflE, assumption)
+apply (rule interval_not_empty)
+apply (rule CO_trans)
+apply (simp add: interval_def)
+-- {* @{text "S \<noteq> {}"} *}
+apply simp
+apply (simp add: induced_def  L_in_interval)
+apply (rule isLub_least, assumption)
+apply (rule subsetD)
+prefer 2 apply assumption
+apply (simp add: S_intv_cl, fast)
+done
+
+lemmas (in CLF) intv_CL_glb = intv_CL_lub [THEN Rdual]
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__interval_is_sublattice"*}  (*ALL THEOREMS*)
+lemma (in CLF) interval_is_sublattice:
+     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |]
+        ==> interval r a b <<= cl"
+(*sledgehammer *)
+apply (rule sublatticeI)
+apply (simp add: interval_subset)
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__interval_is_sublattice_simpler"*}  
+(*sledgehammer *)
+apply (rule CompleteLatticeI)
+apply (simp add: intervalPO)
+ apply (simp add: intv_CL_lub)
+apply (simp add: intv_CL_glb)
+done
+
+lemmas (in CLF) interv_is_compl_latt =
+    interval_is_sublattice [THEN sublattice_imp_CL]
+
+
+subsection {* Top and Bottom *}
+lemma (in CLF) Top_dual_Bot: "Top cl = Bot (dual cl)"
+by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff)
+
+lemma (in CLF) Bot_dual_Top: "Bot cl = Top (dual cl)"
+by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff)
+
+ML{*ResAtp.problem_name:="Tarski__Bot_in_lattice"*}  (*ALL THEOREMS*)
+lemma (in CLF) Bot_in_lattice: "Bot cl \<in> A"
+(*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 
+                     r_def [symmetric] A_def [symmetric])
+done
+
+(*first proved 2007-01-25 after relaxing relevance*)
+ML{*ResAtp.problem_name:="Tarski__Top_in_lattice"*}  (*ALL THEOREMS*)
+lemma (in CLF) Top_in_lattice: "Top cl \<in> A"
+(*sledgehammer;*)
+apply (simp add: Top_dual_Bot A_def)
+(*first proved 2007-01-25 after relaxing relevance*)
+ML{*ResAtp.problem_name:="Tarski__Top_in_lattice_simpler"*}  (*ALL THEOREMS*)
+(*sledgehammer*)
+apply (rule dualA_iff [THEN subst])
+apply (blast intro!: CLF.Bot_in_lattice dualPO CL_dualCL CLF_dual)
+done
+
+lemma (in CLF) Top_prop: "x \<in> A ==> (x, Top cl) \<in> r"
+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 
+                     r_def [symmetric] A_def [symmetric])
+done
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__Bot_prop"*}  (*ALL THEOREMS*) 
+lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r"
+(*sledgehammer*) 
+apply (simp add: Bot_dual_Top r_def)
+apply (rule dualr_iff [THEN subst])
+apply (simp add: CLF.Top_prop [of _ f]
+                 dualA_iff A_def dualPO CL_dualCL CLF_dual)
+done
+
+ML{*ResAtp.problem_name:="Tarski__Bot_in_lattice"*}  (*ALL THEOREMS*)
+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
+
+ML{*ResAtp.problem_name:="Tarski__Bot_intv_not_empty"*}  (*ALL THEOREMS*)
+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
+
+
+subsection {* fixed points form a partial order *}
+
+lemma (in CLF) fixf_po: "(| pset = P, order = induced P r|) \<in> PartialOrder"
+by (simp add: P_def fix_subset po_subset_po)
+
+(*first proved 2007-01-25 after relaxing relevance*)
+ML{*ResAtp.problem_name:="Tarski__Y_subset_A"*}
+  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*) 
+apply (rule subset_trans [OF _ fix_subset])
+apply (rule Y_ss [simplified P_def])
+done
+  declare (in Tarski) P_def[simp del] Y_ss [simp del]
+  declare fix_subset [rule del] subset_trans [rule del]
+
+
+lemma (in Tarski) lubY_in_A: "lub Y cl \<in> A"
+  by (rule Y_subset_A [THEN lub_in_lattice])
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__lubY_le_flubY"*}  (*ALL THEOREMS*)
+lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \<in> r"
+(*sledgehammer*) 
+apply (rule lub_least)
+apply (rule Y_subset_A)
+apply (rule f_in_funcset [THEN funcset_mem])
+apply (rule lubY_in_A)
+-- {* @{text "Y \<subseteq> P ==> f x = x"} *}
+apply (rule ballI)
+ML{*ResAtp.problem_name:="Tarski__lubY_le_flubY_simpler"*}  (*ALL THEOREMS*)
+(*sledgehammer *)
+apply (rule_tac t = "x" in fix_imp_eq [THEN subst])
+apply (erule Y_ss [simplified P_def, THEN subsetD])
+-- {* @{text "reduce (f x, f (lub Y cl)) \<in> r to (x, lub Y cl) \<in> r"} by monotonicity *}
+ML{*ResAtp.problem_name:="Tarski__lubY_le_flubY_simplest"*}  (*ALL THEOREMS*)
+(*sledgehammer*)
+apply (rule_tac f = "f" in monotoneE)
+apply (rule monotone_f)
+apply (simp add: Y_subset_A [THEN subsetD])
+apply (rule lubY_in_A)
+apply (simp add: lub_upper Y_subset_A)
+done
+
+(*first proved 2007-01-25 after relaxing relevance*)
+ML{*ResAtp.problem_name:="Tarski__intY1_subset"*}  (*ALL THEOREMS*)
+lemma (in Tarski) intY1_subset: "intY1 \<subseteq> A"
+(*sledgehammer*) 
+apply (unfold intY1_def)
+apply (rule interval_subset)
+apply (rule lubY_in_A)
+apply (rule Top_in_lattice)
+done
+
+lemmas (in Tarski) intY1_elem = intY1_subset [THEN subsetD]
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__intY1_f_closed"*}  (*ALL THEOREMS*)
+lemma (in Tarski) intY1_f_closed: "x \<in> intY1 \<Longrightarrow> f x \<in> intY1"
+(*sledgehammer*) 
+apply (simp add: intY1_def  interval_def)
+apply (rule conjI)
+apply (rule transE)
+apply (rule lubY_le_flubY)
+-- {* @{text "(f (lub Y cl), f x) \<in> r"} *}
+ML{*ResAtp.problem_name:="Tarski__intY1_f_closed_simpler"*}  (*ALL THEOREMS*)
+(*sledgehammer [has been proved before now...]*)
+apply (rule_tac f=f in monotoneE)
+apply (rule monotone_f)
+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"} *} 
+apply (rule Top_prop)
+apply (rule f_in_funcset [THEN funcset_mem])
+apply (simp add: intY1_def interval_def  intY1_elem)
+done
+
+ML{*ResAtp.problem_name:="Tarski__intY1_func"*}  (*ALL THEOREMS*)
+lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1" 
+apply (metis intY1_f_closed restrict_in_funcset)
+done
+
+ML{*ResAtp.problem_name:="Tarski__intY1_mono"*}  (*ALL THEOREMS*)
+lemma (in Tarski) intY1_mono [skolem]:
+     "monotone (%x: intY1. f x) intY1 (induced intY1 r)"
+(*sledgehammer *)
+apply (auto simp add: monotone_def induced_def intY1_f_closed)
+apply (blast intro: intY1_elem monotone_f [THEN monotoneE])
+done
+
+(*proof requires relaxing relevance: 2007-01-25*)
+ML{*ResAtp.problem_name:="Tarski__intY1_is_cl"*}  (*ALL THEOREMS*)
+lemma (in Tarski) intY1_is_cl:
+    "(| pset = intY1, order = induced intY1 r |) \<in> CompleteLattice"
+(*sledgehammer*) 
+apply (unfold intY1_def)
+apply (rule interv_is_compl_latt)
+apply (rule lubY_in_A)
+apply (rule Top_in_lattice)
+apply (rule Top_intv_not_empty)
+apply (rule lubY_in_A)
+done
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__v_in_P"*}  (*ALL THEOREMS*)
+lemma (in Tarski) v_in_P: "v \<in> P"
+(*sledgehammer*) 
+apply (unfold P_def)
+apply (rule_tac A = "intY1" in fixf_subset)
+apply (rule intY1_subset)
+apply (simp add: CLF.glbH_is_fixp [OF _ intY1_is_cl, simplified]
+                 v_def CL_imp_PO intY1_is_cl CLF_def intY1_func intY1_mono)
+done
+
+ML{*ResAtp.problem_name:="Tarski__z_in_interval"*}  (*ALL THEOREMS*)
+lemma (in Tarski) z_in_interval:
+     "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] ==> z \<in> intY1"
+(*sledgehammer *)
+apply (unfold intY1_def P_def)
+apply (rule intervalI)
+prefer 2
+ apply (erule fix_subset [THEN subsetD, THEN Top_prop])
+apply (rule lub_least)
+apply (rule Y_subset_A)
+apply (fast elim!: fix_subset [THEN subsetD])
+apply (simp add: induced_def)
+done
+
+ML{*ResAtp.problem_name:="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" 
+(*
+  apply (metis P_def UnE Un_absorb contra_subsetD equalityE fix_imp_eq indI intY1_elem intY1_f_closed monotoneE monotone_f reflE rel_imp_elem restrict_apply z_in_interval)
+??unsound??*)
+apply (simp add: induced_def  intY1_f_closed z_in_interval P_def)
+apply (simp add: fix_imp_eq [of _ f A] fix_subset [of f A, THEN subsetD]
+                 reflE)
+done
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__tarski_full_lemma"*}  (*ALL THEOREMS*)
+lemma (in Tarski) tarski_full_lemma:
+     "\<exists>L. isLub Y (| pset = P, order = induced P r |) L"
+apply (rule_tac x = "v" in exI)
+apply (simp add: isLub_def)
+-- {* @{text "v \<in> P"} *}
+apply (simp add: v_in_P)
+apply (rule conjI)
+(*sledgehammer*) 
+-- {* @{text v} is lub *}
+-- {* @{text "1. \<forall>y:Y. (y, v) \<in> induced P r"} *}
+apply (rule ballI)
+apply (simp add: induced_def subsetD v_in_P)
+apply (rule conjI)
+apply (erule Y_ss [THEN subsetD])
+apply (rule_tac b = "lub Y cl" in transE)
+apply (rule lub_upper)
+apply (rule Y_subset_A, assumption)
+apply (rule_tac b = "Top cl" in interval_imp_mem)
+apply (simp add: v_def)
+apply (fold intY1_def)
+apply (rule CL.glb_in_lattice [OF _ intY1_is_cl, simplified])
+ apply (simp add: CL_imp_PO intY1_is_cl, force)
+-- {* @{text v} is LEAST ub *}
+apply clarify
+apply (rule indI)
+  prefer 3 apply assumption
+ prefer 2 apply (simp add: v_in_P)
+apply (unfold v_def)
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__tarski_full_lemma_simpler"*} 
+(*sledgehammer*) 
+apply (rule indE)
+apply (rule_tac [2] intY1_subset)
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__tarski_full_lemma_simplest"*} 
+(*sledgehammer*) 
+apply (rule CL.glb_lower [OF _ intY1_is_cl, simplified])
+  apply (simp add: CL_imp_PO intY1_is_cl)
+ apply force
+apply (simp add: induced_def intY1_f_closed z_in_interval)
+apply (simp add: P_def fix_imp_eq [of _ f A] reflE
+                 fix_subset [of f A, THEN subsetD])
+done
+
+lemma CompleteLatticeI_simp:
+     "[| (| pset = A, order = r |) \<in> PartialOrder;
+         \<forall>S. S \<subseteq> A --> (\<exists>L. isLub S (| pset = A, order = r |)  L) |]
+    ==> (| pset = A, order = r |) \<in> CompleteLattice"
+by (simp add: CompleteLatticeI Rdual)
+
+
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__Tarski_full"*}
+  declare (in CLF) fixf_po[intro] P_def [simp] A_def [simp] r_def [simp]
+               Tarski.tarski_full_lemma [intro] cl_po [intro] cl_co [intro]
+               CompleteLatticeI_simp [intro]
+theorem (in CLF) Tarski_full:
+     "(| pset = P, order = induced P r|) \<in> CompleteLattice"
+(*sledgehammer*) 
+apply (rule CompleteLatticeI_simp)
+apply (rule fixf_po, clarify)
+(*never proved, 2007-01-22*)
+ML{*ResAtp.problem_name:="Tarski__Tarski_full_simpler"*}
+(*sledgehammer*) 
+apply (simp add: P_def A_def r_def)
+apply (blast intro!: Tarski.tarski_full_lemma cl_po cl_co f_cl)
+done
+  declare (in CLF) fixf_po[rule del] P_def [simp del] A_def [simp del] r_def [simp del]
+         Tarski.tarski_full_lemma [rule del] cl_po [rule del] cl_co [rule del]
+         CompleteLatticeI_simp [rule del]
+
+
+end
diff -r 020381339d87 -r dd874e6a3282 src/HOL/MetisExamples/TransClosure.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MetisExamples/TransClosure.thy	Thu Jun 21 13:23:33 2007 +0200
@@ -0,0 +1,62 @@
+(*  Title:      HOL/MetisTest/TransClosure.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Testing the metis method
+*)
+
+theory TransClosure
+imports Main
+begin
+
+types 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"
+
+ML {*ResAtp.problem_name := "TransClosure__test"*}
+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>*"  
+by (metis Transitive_Closure.rtrancl_into_rtrancl converse_rtranclE trancl_reflcl)
+
+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>*"
+proof (neg_clausify)
+assume 0: "f c = Intg x"
+assume 1: "(a, b) \<in> R\<^sup>*"
+assume 2: "(b, c) \<in> R\<^sup>*"
+assume 3: "f b \<noteq> Intg x"
+assume 4: "\<And>A. (b, A) \<notin> R \<or> (a, A) \<notin> R\<^sup>*"
+have 5: "b = c \<or> b \<in> Domain R"
+  by (metis Not_Domain_rtrancl 2)
+have 6: "\<And>X1. (a, X1) \<in> R\<^sup>* \<or> (b, X1) \<notin> R"
+  by (metis Transitive_Closure.rtrancl_into_rtrancl 1)
+have 7: "\<And>X1. (b, X1) \<notin> R"
+  by (metis 6 4)
+have 8: "b \<notin> Domain R"
+  by (metis 7 DomainE)
+have 9: "c = b"
+  by (metis 5 8)
+have 10: "f b = Intg x"
+  by (metis 0 9)
+show "False"
+  by (metis 10 3)
+qed
+
+ML {*ResAtp.problem_name := "TransClosure__test_simpler"*}
+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 rel_pow_0_E rel_pow_0_I)
+apply (metis DomainE Domain_iff Transitive_Closure.rtrancl_into_rtrancl)
+done
+
+end
diff -r 020381339d87 -r dd874e6a3282 src/HOL/MetisExamples/set.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MetisExamples/set.thy	Thu Jun 21 13:23:33 2007 +0200
@@ -0,0 +1,285 @@
+(*  Title:      HOL/MetisExamples/set.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Testing the metis method
+*)
+
+theory set imports Main
+
+begin
+
+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;
+
+(*??Single-step reconstruction fails due to "assume?"*)
+
+lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
+by metis
+
+ML{*ResReconstruct.modulus := 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 (neg_clausify)
+fix x
+assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
+assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
+assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
+have 6: "sup Y Z = X \<or> Y \<subseteq> X"
+  by (metis 0 sup_set_eq)
+have 7: "sup Y Z = X \<or> Z \<subseteq> X"
+  by (metis 1 sup_set_eq)
+have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
+  by (metis 5 sup_set_eq)
+have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
+  by (metis 2 sup_set_eq)
+have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
+  by (metis 3 sup_set_eq)
+have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
+  by (metis 4 sup_set_eq)
+have 12: "Z \<subseteq> X"
+  by (metis Un_upper2 sup_set_eq 7)
+have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
+  by (metis 8 Un_upper2 sup_set_eq)
+have 14: "Y \<subseteq> X"
+  by (metis Un_upper1 sup_set_eq 6)
+have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
+  by (metis 10 12)
+have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
+  by (metis 9 12)
+have 17: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
+  by (metis 11 12)
+have 18: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x"
+  by (metis 17 14)
+have 19: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
+  by (metis 15 14)
+have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
+  by (metis 16 14)
+have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
+  by (metis 13 Un_upper1 sup_set_eq)
+have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
+  by (metis equalityI 21)
+have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
+  by (metis 22 Un_least sup_set_eq)
+have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
+  by (metis 23 12)
+have 25: "sup Y Z = X"
+  by (metis 24 14)
+have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
+  by (metis Un_least sup_set_eq 25)
+have 27: "Y \<subseteq> x"
+  by (metis 20 25)
+have 28: "Z \<subseteq> x"
+  by (metis 19 25)
+have 29: "\<not> X \<subseteq> x"
+  by (metis 18 25)
+have 30: "X \<subseteq> x \<or> \<not> Y \<subseteq> x"
+  by (metis 26 28)
+have 31: "X \<subseteq> x"
+  by (metis 30 27)
+show "False"
+  by (metis 31 29)
+qed
+
+
+ML{*ResReconstruct.modulus := 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 (neg_clausify)
+fix x
+assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
+assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
+assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
+have 6: "sup Y Z = X \<or> Y \<subseteq> X"
+  by (metis 0 sup_set_eq)
+have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
+  by (metis 2 sup_set_eq)
+have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
+  by (metis 4 sup_set_eq)
+have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
+  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
+have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
+  by (metis 3 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq)
+have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
+  by (metis 8 Un_upper2 sup_set_eq 1 sup_set_eq)
+have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
+  by (metis 10 Un_upper1 sup_set_eq 6)
+have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
+  by (metis 9 Un_upper1 sup_set_eq)
+have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
+  by (metis equalityI 13 Un_least sup_set_eq)
+have 15: "sup Y Z = X"
+  by (metis 14 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 6)
+have 16: "Y \<subseteq> x"
+  by (metis 7 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 6 15)
+have 17: "\<not> X \<subseteq> x"
+  by (metis 11 Un_upper1 sup_set_eq 6 15)
+have 18: "X \<subseteq> x"
+  by (metis Un_least sup_set_eq 15 12 15 16)
+show "False"
+  by (metis 18 17)
+qed
+
+ML{*ResReconstruct.modulus := 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 (neg_clausify)
+fix x
+assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
+assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
+assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
+have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
+  by (metis 3 sup_set_eq)
+have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
+  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
+have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
+  by (metis 2 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq)
+have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
+  by (metis 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
+  by (metis equalityI 7 Un_upper1 sup_set_eq)
+have 11: "sup Y Z = X"
+  by (metis 10 Un_least sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+have 12: "Z \<subseteq> x"
+  by (metis 9 11)
+have 13: "X \<subseteq> x"
+  by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq 0 sup_set_eq 11)
+show "False"
+  by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 11)
+qed
+
+(*Example included in TPHOLs paper*)
+
+ML{*ResReconstruct.modulus := 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 (neg_clausify)
+fix x
+assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
+assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
+assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
+assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
+have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
+  by (metis 4 sup_set_eq)
+have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
+  by (metis 3 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq)
+have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
+  by (metis 7 Un_upper1 sup_set_eq 0 sup_set_eq)
+have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
+  by (metis equalityI 5 sup_set_eq Un_upper2 sup_set_eq Un_upper1 sup_set_eq Un_least sup_set_eq)
+have 10: "Y \<subseteq> x"
+  by (metis 2 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+have 11: "X \<subseteq> x"
+  by (metis Un_least sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 8 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 10)
+show "False"
+  by (metis 11 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+qed 
+
+ML {*ResAtp.problem_name := "set__equal_union"*}
+lemma (*equal_union: *)
+   "(X = Y \<union> Z) =
+    (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" 
+(*One shot proof: hand-reduced. Metis can't do the full proof any more.*)
+by (metis Un_least Un_upper1 Un_upper2 set_eq_subset)
+
+
+ML {*ResAtp.problem_name := "set__equal_inter"*}
+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 set_eq_subset)
+
+ML {*ResAtp.problem_name := "set__fixedpoint"*}
+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 (neg_clausify)
+fix x xa
+assume 0: "f (g x) = x"
+assume 1: "\<And>mes_oip. mes_oip = x \<or> f (g mes_oip) \<noteq> mes_oip"
+assume 2: "\<And>mes_oio. g (f (xa mes_oio)) = xa mes_oio \<or> g (f mes_oio) \<noteq> mes_oio"
+assume 3: "\<And>mes_oio. g (f mes_oio) \<noteq> mes_oio \<or> xa mes_oio \<noteq> mes_oio"
+have 4: "\<And>X1. g (f X1) \<noteq> X1 \<or> g x \<noteq> X1"
+  by (metis 3 2 1 2)
+show "False"
+  by (metis 4 0)
+qed
+
+ML {*ResAtp.problem_name := "set__singleton_example"*}
+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)
+  --{*found by SPASS*}
+
+lemma (*singleton_example_2:*)
+     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+by (metis UnE Un_absorb Un_absorb2 Un_eq_Union Union_insert insertI1 insert_Diff insert_Diff_single subset_def)
+  --{*found by Vampire*}
+
+lemma singleton_example_2:
+     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+proof (neg_clausify)
+assume 0: "\<And>mes_ojD. \<not> S \<subseteq> {mes_ojD}"
+assume 1: "\<And>mes_ojE. mes_ojE \<notin> S \<or> \<Union>S \<subseteq> mes_ojE"
+have 2: "\<And>X3. X3 = \<Union>S \<or> \<not> X3 \<subseteq> \<Union>S \<or> X3 \<notin> S"
+  by (metis equalityI 1)
+have 3: "\<And>X3. S \<subseteq> insert (\<Union>S) X3"
+  by (metis Set.subsetI 2 Union_upper Set.subsetI insertCI)
+show "False"
+  by (metis 0 3)
+qed
+
+
+
+text {*
+  From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
+  293-314.
+*}
+
+ML {*ResAtp.problem_name := "set__Bledsoe_Fung"*}
+(*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 atMost_iff);
+apply (metis emptyE)
+apply (metis insert_iff singletonE)
+apply (metis insertCI singletonE zless_le)
+apply (metis insert_iff singletonE)
+apply (metis insert_iff singletonE)
+apply (metis DiffE)
+apply (metis Suc_eq_add_numeral_1 nat_add_commute pair_in_Id_conv) 
+done
+
+end
+