# HG changeset patch
# User Thomas Sewell <tsewell@nicta.com.au>
# Date 1253755985 -36000
# Node ID 5fae12e4679ca662fdcbcc01c4b62ee37816f880
# Parent  f65d74a264dd1d92c39e20776fac9c4a21a9cddb# Parent  82956a3f0e0b1b521c65b76bf213d35448eef483
Merge with changes from isabelle dev repository.

diff -r f65d74a264dd -r 5fae12e4679c Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Wed Sep 23 19:17:48 2009 +1000
+++ b/Admin/isatest/isatest-makedist	Thu Sep 24 11:33:05 2009 +1000
@@ -102,9 +102,9 @@
 #sleep 15
 $SSH macbroy21 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
 sleep 15
-$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e"
-sleep 15
-$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly"
+#$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e"
+#sleep 15
+$SSH atbroy99 "$MAKEALL $HOME/settings/at64-poly"
 sleep 15
 $SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8; $MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8"
 sleep 15
diff -r f65d74a264dd -r 5fae12e4679c NEWS
--- a/NEWS	Wed Sep 23 19:17:48 2009 +1000
+++ b/NEWS	Thu Sep 24 11:33:05 2009 +1000
@@ -102,6 +102,10 @@
 
   INCOMPATIBILITY.
 
+* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no
+simp rules by default any longer.  The same applies to
+min_max.inf_absorb1 etc.!  INCOMPATIBILITY.
+
 * Power operations on relations and functions are now one dedicate
 constant "compow" with infix syntax "^^".  Power operations on
 multiplicative monoids retains syntax "^" and is now defined generic
diff -r f65d74a264dd -r 5fae12e4679c lib/Tools/usedir
--- a/lib/Tools/usedir	Wed Sep 23 19:17:48 2009 +1000
+++ b/lib/Tools/usedir	Thu Sep 24 11:33:05 2009 +1000
@@ -262,7 +262,7 @@
 else
   { echo "$ITEM FAILED";
     echo "(see also $LOG)";
-    echo; tail "$LOG"; echo; } >&2
+    echo; tail -n 20 "$LOG"; echo; } >&2
 fi
 
 exit "$RC"
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Wed Sep 23 19:17:48 2009 +1000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,271 +0,0 @@
-(*  Title:      HOL/Code_Eval.thy
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Term evaluation using the generic code generator *}
-
-theory Code_Eval
-imports Plain Typerep Code_Numeral
-begin
-
-subsection {* Term representation *}
-
-subsubsection {* Terms and class @{text term_of} *}
-
-datatype "term" = dummy_term
-
-definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
-  "Const _ _ = dummy_term"
-
-definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
-  "App _ _ = dummy_term"
-
-code_datatype Const App
-
-class term_of = typerep +
-  fixes term_of :: "'a \<Rightarrow> term"
-
-lemma term_of_anything: "term_of x \<equiv> t"
-  by (rule eq_reflection) (cases "term_of x", cases t, simp)
-
-definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
-  \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
-  "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
-
-lemma valapp_code [code, code_unfold]:
-  "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
-  by (simp only: valapp_def fst_conv snd_conv)
-
-
-subsubsection {* @{text term_of} instances *}
-
-instantiation "fun" :: (typerep, typerep) term_of
-begin
-
-definition
-  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
-     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
-
-instance ..
-
-end
-
-setup {*
-let
-  fun add_term_of tyco raw_vs thy =
-    let
-      val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
-      val ty = Type (tyco, map TFree vs);
-      val lhs = Const (@{const_name term_of}, ty --> @{typ term})
-        $ Free ("x", ty);
-      val rhs = @{term "undefined \<Colon> term"};
-      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
-      fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
-        o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
-    in
-      thy
-      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
-      |> `(fn lthy => Syntax.check_term lthy eq)
-      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
-      |> snd
-      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
-    end;
-  fun ensure_term_of (tyco, (raw_vs, _)) thy =
-    let
-      val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
-        andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
-    in if need_inst then add_term_of tyco raw_vs thy else thy end;
-in
-  Code.type_interpretation ensure_term_of
-end
-*}
-
-setup {*
-let
-  fun mk_term_of_eq thy ty vs tyco (c, tys) =
-    let
-      val t = list_comb (Const (c, tys ---> ty),
-        map Free (Name.names Name.context "a" tys));
-      val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
-        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
-      val cty = Thm.ctyp_of thy ty;
-    in
-      @{thm term_of_anything}
-      |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
-      |> Thm.varifyT
-    end;
-  fun add_term_of_code tyco raw_vs raw_cs thy =
-    let
-      val algebra = Sign.classes_of thy;
-      val vs = map (fn (v, sort) =>
-        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
-      val ty = Type (tyco, map TFree vs);
-      val cs = (map o apsnd o map o map_atyps)
-        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
-      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
-      val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
-   in
-      thy
-      |> Code.del_eqns const
-      |> fold Code.add_eqn eqs
-    end;
-  fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
-    let
-      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
-    in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
-in
-  Code.type_interpretation ensure_term_of_code
-end
-*}
-
-
-subsubsection {* Code generator setup *}
-
-lemmas [code del] = term.recs term.cases term.size
-lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
-
-lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
-lemma [code, code del]:
-  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
-lemma [code, code del]:
-  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
-
-lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
-    (let (n, m) = nibble_pair_of_char c
-  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
-    (Code_Eval.term_of n)) (Code_Eval.term_of m))"
-  by (subst term_of_anything) rule 
-
-code_type "term"
-  (Eval "Term.term")
-
-code_const Const and App
-  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
-
-code_const "term_of \<Colon> String.literal \<Rightarrow> term"
-  (Eval "HOLogic.mk'_message'_string")
-
-code_reserved Eval HOLogic
-
-
-subsubsection {* Syntax *}
-
-definition termify :: "'a \<Rightarrow> term" where
-  [code del]: "termify x = dummy_term"
-
-abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
-  "valtermify x \<equiv> (x, \<lambda>u. termify x)"
-
-setup {*
-let
-  fun map_default f xs =
-    let val ys = map f xs
-    in if exists is_some ys
-      then SOME (map2 the_default xs ys)
-      else NONE
-    end;
-  fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
-        if not (Term.has_abs t)
-        then if fold_aterms (fn Const _ => I | _ => K false) t true
-          then SOME (HOLogic.reflect_term t)
-          else error "Cannot termify expression containing variables"
-        else error "Cannot termify expression containing abstraction"
-    | subst_termify_app (t, ts) = case map_default subst_termify ts
-       of SOME ts' => SOME (list_comb (t, ts'))
-        | NONE => NONE
-  and subst_termify (Abs (v, T, t)) = (case subst_termify t
-       of SOME t' => SOME (Abs (v, T, t'))
-        | NONE => NONE)
-    | subst_termify t = subst_termify_app (strip_comb t) 
-  fun check_termify ts ctxt = map_default subst_termify ts
-    |> Option.map (rpair ctxt)
-in
-  Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
-end;
-*}
-
-locale term_syntax
-begin
-
-notation App (infixl "<\<cdot>>" 70)
-  and valapp (infixl "{\<cdot>}" 70)
-
-end
-
-interpretation term_syntax .
-
-no_notation App (infixl "<\<cdot>>" 70)
-  and valapp (infixl "{\<cdot>}" 70)
-
-
-subsection {* Numeric types *}
-
-definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
-  "term_of_num two = (\<lambda>_. dummy_term)"
-
-lemma (in term_syntax) term_of_num_code [code]:
-  "term_of_num two k = (if k = 0 then termify Int.Pls
-    else (if k mod two = 0
-      then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
-      else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
-  by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
-
-lemma (in term_syntax) term_of_nat_code [code]:
-  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
-  by (simp only: term_of_anything)
-
-lemma (in term_syntax) term_of_int_code [code]:
-  "term_of (k::int) = (if k = 0 then termify (0 :: int)
-    else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
-      else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
-  by (simp only: term_of_anything)
-
-lemma (in term_syntax) term_of_code_numeral_code [code]:
-  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
-  by (simp only: term_of_anything)
-
-subsection {* Obfuscate *}
-
-print_translation {*
-let
-  val term = Const ("<TERM>", dummyT);
-  fun tr1' [_, _] = term;
-  fun tr2' [] = term;
-in
-  [(@{const_syntax Const}, tr1'),
-    (@{const_syntax App}, tr1'),
-    (@{const_syntax dummy_term}, tr2')]
-end
-*}
-
-hide const dummy_term App valapp
-hide (open) const Const termify valtermify term_of term_of_num
-
-
-subsection {* Evaluation setup *}
-
-ML {*
-signature EVAL =
-sig
-  val eval_ref: (unit -> term) option ref
-  val eval_term: theory -> term -> term
-end;
-
-structure Eval : EVAL =
-struct
-
-val eval_ref = ref (NONE : (unit -> term) option);
-
-fun eval_term thy t =
-  Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
-
-end;
-*}
-
-setup {*
-  Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
-*}
-
-end
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Code_Evaluation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Code_Evaluation.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -0,0 +1,271 @@
+(*  Title:      HOL/Code_Evaluation.thy
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Term evaluation using the generic code generator *}
+
+theory Code_Evaluation
+imports Plain Typerep Code_Numeral
+begin
+
+subsection {* Term representation *}
+
+subsubsection {* Terms and class @{text term_of} *}
+
+datatype "term" = dummy_term
+
+definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
+  "Const _ _ = dummy_term"
+
+definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
+  "App _ _ = dummy_term"
+
+code_datatype Const App
+
+class term_of = typerep +
+  fixes term_of :: "'a \<Rightarrow> term"
+
+lemma term_of_anything: "term_of x \<equiv> t"
+  by (rule eq_reflection) (cases "term_of x", cases t, simp)
+
+definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
+  \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
+  "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
+
+lemma valapp_code [code, code_unfold]:
+  "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
+  by (simp only: valapp_def fst_conv snd_conv)
+
+
+subsubsection {* @{text term_of} instances *}
+
+instantiation "fun" :: (typerep, typerep) term_of
+begin
+
+definition
+  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
+     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
+
+instance ..
+
+end
+
+setup {*
+let
+  fun add_term_of tyco raw_vs thy =
+    let
+      val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
+      val ty = Type (tyco, map TFree vs);
+      val lhs = Const (@{const_name term_of}, ty --> @{typ term})
+        $ Free ("x", ty);
+      val rhs = @{term "undefined \<Colon> term"};
+      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+      fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
+        o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
+    in
+      thy
+      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
+      |> `(fn lthy => Syntax.check_term lthy eq)
+      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
+      |> snd
+      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+    end;
+  fun ensure_term_of (tyco, (raw_vs, _)) thy =
+    let
+      val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
+        andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
+    in if need_inst then add_term_of tyco raw_vs thy else thy end;
+in
+  Code.type_interpretation ensure_term_of
+end
+*}
+
+setup {*
+let
+  fun mk_term_of_eq thy ty vs tyco (c, tys) =
+    let
+      val t = list_comb (Const (c, tys ---> ty),
+        map Free (Name.names Name.context "a" tys));
+      val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
+        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
+      val cty = Thm.ctyp_of thy ty;
+    in
+      @{thm term_of_anything}
+      |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
+      |> Thm.varifyT
+    end;
+  fun add_term_of_code tyco raw_vs raw_cs thy =
+    let
+      val algebra = Sign.classes_of thy;
+      val vs = map (fn (v, sort) =>
+        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
+      val ty = Type (tyco, map TFree vs);
+      val cs = (map o apsnd o map o map_atyps)
+        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
+      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+      val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
+   in
+      thy
+      |> Code.del_eqns const
+      |> fold Code.add_eqn eqs
+    end;
+  fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
+    let
+      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
+    in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
+in
+  Code.type_interpretation ensure_term_of_code
+end
+*}
+
+
+subsubsection {* Code generator setup *}
+
+lemmas [code del] = term.recs term.cases term.size
+lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
+
+lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
+lemma [code, code del]:
+  "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
+lemma [code, code del]:
+  "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
+
+lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Evaluation.term_of c =
+    (let (n, m) = nibble_pair_of_char c
+  in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
+    (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
+  by (subst term_of_anything) rule 
+
+code_type "term"
+  (Eval "Term.term")
+
+code_const Const and App
+  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
+
+code_const "term_of \<Colon> String.literal \<Rightarrow> term"
+  (Eval "HOLogic.mk'_message'_string")
+
+code_reserved Eval HOLogic
+
+
+subsubsection {* Syntax *}
+
+definition termify :: "'a \<Rightarrow> term" where
+  [code del]: "termify x = dummy_term"
+
+abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
+  "valtermify x \<equiv> (x, \<lambda>u. termify x)"
+
+setup {*
+let
+  fun map_default f xs =
+    let val ys = map f xs
+    in if exists is_some ys
+      then SOME (map2 the_default xs ys)
+      else NONE
+    end;
+  fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
+        if not (Term.has_abs t)
+        then if fold_aterms (fn Const _ => I | _ => K false) t true
+          then SOME (HOLogic.reflect_term t)
+          else error "Cannot termify expression containing variables"
+        else error "Cannot termify expression containing abstraction"
+    | subst_termify_app (t, ts) = case map_default subst_termify ts
+       of SOME ts' => SOME (list_comb (t, ts'))
+        | NONE => NONE
+  and subst_termify (Abs (v, T, t)) = (case subst_termify t
+       of SOME t' => SOME (Abs (v, T, t'))
+        | NONE => NONE)
+    | subst_termify t = subst_termify_app (strip_comb t) 
+  fun check_termify ts ctxt = map_default subst_termify ts
+    |> Option.map (rpair ctxt)
+in
+  Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
+end;
+*}
+
+locale term_syntax
+begin
+
+notation App (infixl "<\<cdot>>" 70)
+  and valapp (infixl "{\<cdot>}" 70)
+
+end
+
+interpretation term_syntax .
+
+no_notation App (infixl "<\<cdot>>" 70)
+  and valapp (infixl "{\<cdot>}" 70)
+
+
+subsection {* Numeric types *}
+
+definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
+  "term_of_num two = (\<lambda>_. dummy_term)"
+
+lemma (in term_syntax) term_of_num_code [code]:
+  "term_of_num two k = (if k = 0 then termify Int.Pls
+    else (if k mod two = 0
+      then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
+      else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
+  by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
+
+lemma (in term_syntax) term_of_nat_code [code]:
+  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
+  by (simp only: term_of_anything)
+
+lemma (in term_syntax) term_of_int_code [code]:
+  "term_of (k::int) = (if k = 0 then termify (0 :: int)
+    else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
+      else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
+  by (simp only: term_of_anything)
+
+lemma (in term_syntax) term_of_code_numeral_code [code]:
+  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
+  by (simp only: term_of_anything)
+
+subsection {* Obfuscate *}
+
+print_translation {*
+let
+  val term = Const ("<TERM>", dummyT);
+  fun tr1' [_, _] = term;
+  fun tr2' [] = term;
+in
+  [(@{const_syntax Const}, tr1'),
+    (@{const_syntax App}, tr1'),
+    (@{const_syntax dummy_term}, tr2')]
+end
+*}
+
+hide const dummy_term App valapp
+hide (open) const Const termify valtermify term_of term_of_num
+
+
+subsection {* Evaluation setup *}
+
+ML {*
+signature EVAL =
+sig
+  val eval_ref: (unit -> term) option ref
+  val eval_term: theory -> term -> term
+end;
+
+structure Eval : EVAL =
+struct
+
+val eval_ref = ref (NONE : (unit -> term) option);
+
+fun eval_term thy t =
+  Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
+
+end;
+*}
+
+setup {*
+  Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
+*}
+
+end
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Complete_Lattice.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -76,11 +76,11 @@
 
 lemma sup_bot [simp]:
   "x \<squnion> bot = x"
-  using bot_least [of x] by (simp add: sup_commute)
+  using bot_least [of x] by (simp add: sup_commute sup_absorb2)
 
 lemma inf_top [simp]:
   "x \<sqinter> top = x"
-  using top_greatest [of x] by (simp add: inf_commute)
+  using top_greatest [of x] by (simp add: inf_commute inf_absorb2)
 
 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "SUPR A f = \<Squnion> (f ` A)"
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -1904,7 +1904,7 @@
 	show "0 < real x * 2/3" using * by auto
 	show "real ?max + 1 \<le> real x * 2/3" using * up
 	  by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
-	      auto simp add: real_of_float_max)
+	      auto simp add: real_of_float_max min_max.sup_absorb1)
       qed
       finally have "real (?lb_horner (Float 1 -1)) + real (?lb_horner ?max)
 	\<le> ln (real x)"
@@ -3246,12 +3246,13 @@
         = map (` (variable_of_bound o prop_of)) prems
 
       fun add_deps (name, bnds)
-        = Graph.add_deps_acyclic
-            (name, remove (op =) name (Term.add_free_names (prop_of bnds) []))
+        = Graph.add_deps_acyclic (name,
+            remove (op =) name (Term.add_free_names (prop_of bnds) []))
+
       val order = Graph.empty
                   |> fold Graph.new_node variable_bounds
                   |> fold add_deps variable_bounds
-                  |> Graph.topological_order |> rev
+                  |> Graph.strong_conn |> map the_single |> rev
                   |> map_filter (AList.lookup (op =) variable_bounds)
 
       fun prepend_prem th tac
@@ -3338,7 +3339,7 @@
                       etac @{thm meta_eqE},
                       rtac @{thm impI}] i)
       THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
-      THEN TRY (filter_prems_tac (K false) i)
+      THEN DETERM (TRY (filter_prems_tac (K false) i))
       THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
       THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
       THEN gen_eval_tac eval_oracle ctxt i))
@@ -3350,7 +3351,7 @@
 
   fun mk_approx' prec t = (@{const "approx'"}
                          $ HOLogic.mk_number @{typ nat} prec
-                         $ t $ @{term "[] :: (float * float) list"})
+                         $ t $ @{term "[] :: (float * float) option list"})
 
   fun dest_result (Const (@{const_name "Some"}, _) $
                    ((Const (@{const_name "Pair"}, _)) $
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -512,7 +512,7 @@
   assumes g0: "numgcd t = 0"
   shows "Inum bs t = 0"
   using g0[simplified numgcd_def] 
-  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos)
+  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos min_max.sup_absorb2)
 
 lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
   using gp
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Decision_Procs/ex/Approximation_Ex.thy
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -72,7 +72,9 @@
   shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
   using assms by (approximation 80)
 
-lemma "\<phi> \<in> { 0 .. 1 :: real } \<longrightarrow> \<phi> ^ 2 \<le> \<phi>"
-  by (approximation 30 splitting: \<phi>=1 taylor: \<phi> = 3)
+lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x ^ 2 \<le> x"
+  by (approximation 30 splitting: x=1 taylor: x = 3)
+
+value [approximate] "10"
 
 end
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Finite_Set.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -2966,11 +2966,11 @@
 
 lemma dual_max:
   "ord.max (op \<ge>) = min"
-  by (auto simp add: ord.max_def_raw expand_fun_eq)
+  by (auto simp add: ord.max_def_raw min_def expand_fun_eq)
 
 lemma dual_min:
   "ord.min (op \<ge>) = max"
-  by (auto simp add: ord.min_def_raw expand_fun_eq)
+  by (auto simp add: ord.min_def_raw max_def expand_fun_eq)
 
 lemma strict_below_fold1_iff:
   assumes "finite A" and "A \<noteq> {}"
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Hoare_Parallel/Graph.thy
--- a/src/HOL/Hoare_Parallel/Graph.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Hoare_Parallel/Graph.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -187,6 +187,8 @@
 
 subsubsection{* Graph 3 *}
 
+declare min_max.inf_absorb1 [simp] min_max.inf_absorb2 [simp]
+
 lemma Graph3: 
   "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
 apply (unfold Reach_def)
@@ -307,6 +309,8 @@
 apply force
 done
 
+declare min_max.inf_absorb1 [simp del] min_max.inf_absorb2 [simp del]
+
 subsubsection {* Graph 5 *}
 
 lemma Graph5: 
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Induct/LList.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -665,7 +665,7 @@
 apply (subst LList_corec, force)
 done
 
-lemma llist_corec: 
+lemma llist_corec [nitpick_const_simp]: 
     "llist_corec a f =   
      (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))"
 apply (unfold llist_corec_def LNil_def LCons_def)
@@ -774,10 +774,11 @@
 
 subsection{* The functional @{text lmap} *}
 
-lemma lmap_LNil [simp]: "lmap f LNil = LNil"
+lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
 
-lemma lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
+lemma lmap_LCons [simp, nitpick_const_simp]:
+"lmap f (LCons M N) = LCons (f M) (lmap f N)"
 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
 
 
@@ -792,7 +793,7 @@
 
 subsection{* iterates -- @{text llist_fun_equalityI} cannot be used! *}
 
-lemma iterates: "iterates f x = LCons x (iterates f (f x))"
+lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
 by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
 
 lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)"
@@ -847,18 +848,18 @@
 
 subsection{* @{text lappend} -- its two arguments cause some complications! *}
 
-lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
+lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
 done
 
-lemma lappend_LNil_LCons [simp]: 
+lemma lappend_LNil_LCons [simp, nitpick_const_simp]: 
     "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
 done
 
-lemma lappend_LCons [simp]: 
+lemma lappend_LCons [simp, nitpick_const_simp]: 
     "lappend (LCons l l') N = LCons l (lappend l' N)"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Inductive.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -267,26 +267,6 @@
   Ball_def Bex_def
   induct_rulify_fallback
 
-ML {*
-val def_lfp_unfold = @{thm def_lfp_unfold}
-val def_gfp_unfold = @{thm def_gfp_unfold}
-val def_lfp_induct = @{thm def_lfp_induct}
-val def_coinduct = @{thm def_coinduct}
-val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection}
-val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection}
-val sup_bool_eq = @{thm sup_bool_eq} RS @{thm eq_reflection}
-val sup_fun_eq = @{thm sup_fun_eq} RS @{thm eq_reflection}
-val le_boolI = @{thm le_boolI}
-val le_boolI' = @{thm le_boolI'}
-val le_funI = @{thm le_funI}
-val le_boolE = @{thm le_boolE}
-val le_funE = @{thm le_funE}
-val le_boolD = @{thm le_boolD}
-val le_funD = @{thm le_funD}
-val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection}
-val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection}
-*}
-
 use "Tools/inductive.ML"
 setup Inductive.setup
 
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/IsaMakefile	Thu Sep 24 11:33:05 2009 +1000
@@ -210,7 +210,7 @@
 
 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
   ATP_Linkup.thy \
-  Code_Eval.thy \
+  Code_Evaluation.thy \
   Code_Numeral.thy \
   Equiv_Relations.thy \
   Groebner_Basis.thy \
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Lattices.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -127,10 +127,10 @@
 lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   by (rule antisym) (auto intro: le_infI2)
 
-lemma inf_absorb1[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   by (rule antisym) auto
 
-lemma inf_absorb2[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
+lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   by (rule antisym) auto
 
 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
@@ -155,10 +155,10 @@
 lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   by (rule antisym) (auto intro: le_supI2)
 
-lemma sup_absorb1[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
+lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   by (rule antisym) auto
 
-lemma sup_absorb2[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
+lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   by (rule antisym) auto
 
 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
@@ -229,11 +229,11 @@
 
 lemma less_infI1:
   "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
-  by (auto simp add: less_le intro: le_infI1)
+  by (auto simp add: less_le inf_absorb1 intro: le_infI1)
 
 lemma less_infI2:
   "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
-  by (auto simp add: less_le intro: le_infI2)
+  by (auto simp add: less_le inf_absorb2 intro: le_infI2)
 
 end
 
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/Code_Char.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -5,7 +5,7 @@
 header {* Code generation of pretty characters (and strings) *}
 
 theory Code_Char
-imports List Code_Eval Main
+imports List Code_Evaluation Main
 begin
 
 code_type char
@@ -32,7 +32,7 @@
   (OCaml "!((_ : char) = _)")
   (Haskell infixl 4 "==")
 
-code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
+code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
   (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
 
 end
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/Code_Integer.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -100,7 +100,7 @@
 
 text {* Evaluation *}
 
-code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"
+code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term"
   (Eval "HOLogic.mk'_number/ HOLogic.intT")
 
 end
\ No newline at end of file
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/Coinductive_List.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -260,7 +260,7 @@
   qed
 qed
 
-lemma llist_corec [code]:
+lemma llist_corec [code, nitpick_const_simp]:
   "llist_corec a f =
     (case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))"
 proof (cases "f a")
@@ -656,8 +656,9 @@
   qed
 qed
 
-lemma lmap_LNil [simp]: "lmap f LNil = LNil"
-  and lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
+lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
+  and lmap_LCons [simp, nitpick_const_simp]:
+  "lmap f (LCons M N) = LCons (f M) (lmap f N)"
   by (simp_all add: lmap_def llist_corec)
 
 lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
@@ -728,9 +729,9 @@
   qed
 qed
 
-lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
-  and lappend_LNil_LCons [simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
-  and lappend_LCons [simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
+lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
+  and lappend_LNil_LCons [simp, nitpick_const_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
+  and lappend_LCons [simp, nitpick_const_simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
   by (simp_all add: lappend_def llist_corec)
 
 lemma lappend_LNil1 [simp]: "lappend LNil l = l"
@@ -754,7 +755,7 @@
   iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
   "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
 
-lemma iterates: "iterates f x = LCons x (iterates f (f x))"
+lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
   apply (unfold iterates_def)
   apply (subst llist_corec)
   apply simp
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -415,9 +415,9 @@
 text {* Evaluation *}
 
 lemma [code, code del]:
-  "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
+  "(Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term) = Code_Evaluation.term_of" ..
 
-code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
+code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term"
   (SML "HOLogic.mk'_number/ HOLogic.natT")
 
 
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/Executable_Set.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -85,4 +85,6 @@
   card                ("{*Fset.card*}")
   fold                ("{*foldl o flip*}")
 
+hide (open) const subset eq_set Inter Union flip
+
 end
\ No newline at end of file
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/Fin_Fun.thy
--- a/src/HOL/Library/Fin_Fun.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/Fin_Fun.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -311,17 +311,17 @@
 notation scomp (infixl "o\<rightarrow>" 60)
 
 definition (in term_syntax) valtermify_finfun_const ::
-  "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
-  "valtermify_finfun_const y = Code_Eval.valtermify finfun_const {\<cdot>} y"
+  "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+  "valtermify_finfun_const y = Code_Evaluation.valtermify finfun_const {\<cdot>} y"
 
 definition (in term_syntax) valtermify_finfun_update_code ::
-  "'a\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> 'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
-  "valtermify_finfun_update_code x y f = Code_Eval.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
+  "'a\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> 'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+  "valtermify_finfun_update_code x y f = Code_Evaluation.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
 
 instantiation finfun :: (random, random) random
 begin
 
-primrec random_finfun_aux :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
+primrec random_finfun_aux :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
     "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight
        [(1, Quickcheck.random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
   | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/Nested_Environment.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -567,6 +567,6 @@
 qed simp_all
 
 lemma [code, code del]:
-  "(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Eval.term_of" ..
+  "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
 
 end
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/Sum_Of_Squares.thy
--- a/src/HOL/Library/Sum_Of_Squares.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/Sum_Of_Squares.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -10,6 +10,7 @@
 uses
   ("positivstellensatz.ML")  (* duplicate use!? -- cf. Euclidian_Space.thy *)
   ("Sum_Of_Squares/sum_of_squares.ML")
+  ("Sum_Of_Squares/positivstellensatz_tools.ML")
   ("Sum_Of_Squares/sos_wrapper.ML")
 begin
 
@@ -22,112 +23,142 @@
   of a minute for one sos call, because sos calls CSDP repeatedly.  If
   you install CSDP locally, sos calls typically takes only a few
   seconds.
+  sos generates a certificate which can be used to repeat the proof
+  without calling an external prover.
 *}
 
 text {* setup sos tactic *}
 
 use "positivstellensatz.ML"
+use "Sum_Of_Squares/positivstellensatz_tools.ML"
 use "Sum_Of_Squares/sum_of_squares.ML"
 use "Sum_Of_Squares/sos_wrapper.ML"
 
 setup SosWrapper.setup
 
-text {* Tests -- commented since they work only when csdp is installed
-  or take too long with remote csdps *}
+text {* Tests *}
+
+lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0"
+by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))")
+
+lemma "a1 >= 0 & a2 >= 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)"
+by (sos_cert "(((A<0 * R<1) + (([~1/2*a1*b2 + ~1/2*a2*b1] * A=0) + (([~1/2*a1*a2 + 1/2*b1*b2] * A=1) + (((A<0 * R<1) * ((R<1/2 * [b2]^2) + (R<1/2 * [b1]^2))) + ((A<=0 * (A<=1 * R<1)) * ((R<1/2 * [b2]^2) + ((R<1/2 * [b1]^2) + ((R<1/2 * [a2]^2) + (R<1/2 * [a1]^2))))))))))")
 
-(*
-lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" by sos
+lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0"
+by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))")
+
+lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1  --> x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1"
+by (sos_cert "((R<1 + (((A<=3 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=7 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=5 * R<1)) * (R<1 * [1]^2)))))))")
 
-lemma "a1 >= 0 & a2 >= 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and>
-  (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" by sos
+lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 --> x * y + x * z + y * z >= 3 * x * y * z"
+by (sos_cert "(((A<0 * R<1) + (((A<0 * R<1) * (R<1/2 * [1]^2)) + (((A<=2 * R<1) * (R<1/2 * [~1*x + y]^2)) + (((A<=1 * R<1) * (R<1/2 * [~1*x + z]^2)) + (((A<=1 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + (((A<=0 * R<1) * (R<1/2 * [~1*y + z]^2)) + (((A<=0 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + ((A<=0 * (A<=1 * (A<=3 * R<1))) * (R<1/2 * [1]^2))))))))))")
+
+lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3"
+by (sos_cert "(((A<0 * R<1) + (([~3] * A=0) + (R<1 * ((R<2 * [~1/2*x + ~1/2*y + z]^2) + (R<3/2 * [~1*x + y]^2))))))")
 
-lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" by sos
+lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)"
+by (sos_cert "(((A<0 * R<1) + (([~4] * A=0) + (R<1 * ((R<3 * [~1/3*w + ~1/3*x + ~1/3*y + z]^2) + ((R<8/3 * [~1/2*w + ~1/2*x + y]^2) + (R<2 * [~1*w + x]^2)))))))")
 
-lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 -->
-  x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1" by sos
+lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1"
+by (sos_cert "(((A<0 * R<1) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))")
+
+lemma "(x::real) > 1 & y > 1 --> x * y > x + y - 1"
+by (sos_cert "((((A<0 * A<1) * R<1) + ((A<=0 * R<1) * (R<1 * [1]^2))))") 
 
-lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 -->
-  x * y + x * z + y * z >= 3 * x * y * z" by sos
+lemma "abs(x) <= 1 --> abs(64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x) <= (1::real)"
+by (sos_cert "((((A<0 * R<1) + ((A<=1 * R<1) * (R<1 * [~8*x^3 + ~4*x^2 + 4*x + 1]^2)))) & ((((A<0 * A<1) * R<1) + ((A<=1 * (A<0 * R<1)) * (R<1 * [8*x^3 + ~4*x^2 + ~4*x + 1]^2)))))")
+
+(* ------------------------------------------------------------------------- *)
+(* One component of denominator in dodecahedral example.                     *)
+(* ------------------------------------------------------------------------- *)
 
-lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3" by sos
+lemma "2 <= x & x <= 125841 / 50000 & 2 <= y & y <= 125841 / 50000 & 2 <= z & z <= 125841 / 50000 --> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= (0::real)"
+by (sos_cert "(((A<0 * R<1) + ((R<1 * ((R<5749028157/5000000000 * [~25000/222477*x + ~25000/222477*y + ~25000/222477*z + 1]^2) + ((R<864067/1779816 * [419113/864067*x + 419113/864067*y + z]^2) + ((R<320795/864067 * [419113/1283180*x + y]^2) + (R<1702293/5132720 * [x]^2))))) + (((A<=4 * (A<=5 * R<1)) * (R<3/2 * [1]^2)) + (((A<=3 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<3/2 * [1]^2)) + (((A<=1 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=1 * (A<=3 * R<1)) * (R<1/2 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<3/2 * [1]^2)))))))))))))")
 
-lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)" by sos
+(* ------------------------------------------------------------------------- *)
+(* Over a larger but simpler interval.                                       *)
+(* ------------------------------------------------------------------------- *)
 
-lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1" by sos
+lemma "(2::real) <= x & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 0 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)"
+by (sos_cert "((R<1 + ((R<1 * ((R<1 * [~1/6*x + ~1/6*y + ~1/6*z + 1]^2) + ((R<1/18 * [~1/2*x + ~1/2*y + z]^2) + (R<1/24 * [~1*x + y]^2)))) + (((A<0 * R<1) * (R<1/12 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1/6 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1/6 * [1]^2)))))))))))")
 
-lemma "(x::real) > 1 & y > 1 --> x * y > x + y - 1" by sos; 
+(* ------------------------------------------------------------------------- *)
+(* We can do 12. I think 12 is a sharp bound; see PP's certificate.          *)
+(* ------------------------------------------------------------------------- *)
+
+lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)"
+by (sos_cert "(((A<0 * R<1) + (((A<=4 * R<1) * (R<2/3 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1 * [1]^2)) + (((A<=3 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * R<1) * (R<2/3 * [1]^2)) + (((A<=2 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * R<1) * (R<2/3 * [1]^2)) + (((A<=0 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=0 * (A<=3 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<8/3 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))))))))))))))))")
 
-lemma "abs(x) <= 1 --> abs(64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x) <= (1::real)" by sos  
+(* ------------------------------------------------------------------------- *)
+(* Inequality from sci.math (see "Leon-Sotelo, por favor").                  *)
+(* ------------------------------------------------------------------------- *)
 
+lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x + y <= x^2 + y^2"
+by (sos_cert "(((A<0 * R<1) + (([1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") 
 
-text {* One component of denominator in dodecahedral example. *}
+lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x * y * (x + y) <= x^2 + y^2"
+by (sos_cert "(((A<0 * R<1) + (([~1*x + ~1*y + 1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") 
 
-lemma "2 <= x & x <= 125841 / 50000 & 2 <= y & y <= 125841 / 50000 & 2 <= z &
-  z <= 125841 / 50000 --> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= (0::real)" by sos
+lemma "0 <= (x::real) & 0 <= y --> x * y * (x + y)^2 <= (x^2 + y^2)^2"
+by (sos_cert "(((A<0 * R<1) + (R<1 * ((R<1 * [~1/2*x^2 + y^2 + ~1/2*x*y]^2) + (R<3/4 * [~1*x^2 + x*y]^2)))))")
 
+lemma "(0::real) <= a & 0 <= b & 0 <= c & c * (2 * a + b)^3/ 27 <= x \<longrightarrow> c * a^2 * b <= x"
+by (sos_cert "(((A<0 * R<1) + (((A<=3 * R<1) * (R<1 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/27 * [~1*a + b]^2)) + ((A<=0 * (A<=2 * R<1)) * (R<8/27 * [~1*a + b]^2))))))")
+ 
+lemma "(0::real) < x --> 0 < 1 + x + x^2"
+by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))")
 
-text {* Over a larger but simpler interval. *}
+lemma "(0::real) <= x --> 0 < 1 + x + x^2"
+by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))")
 
-lemma "(2::real) <= x & x <= 4 & 2 <= y & y <= 4 & 2 <= z &
-  z <= 4 --> 0 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" by sos
+lemma "(0::real) < 1 + x^2"
+by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))")
+
+lemma "(0::real) <= 1 + 2 * x + x^2"
+by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [x + 1]^2))))")
 
-text {* We can do 12. I think 12 is a sharp bound; see PP's certificate. *}
+lemma "(0::real) < 1 + abs x"
+by (sos_cert "((R<1 + (((A<=1 * R<1) * (R<1/2 * [1]^2)) + ((A<=0 * R<1) * (R<1/2 * [1]^2)))))")
 
-lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 -->
-  12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" by sos
+lemma "(0::real) < 1 + (1 + x)^2 * (abs x)"
+by (sos_cert "(((R<1 + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [x + 1]^2))))) & ((R<1 + (((A<0 * R<1) * (R<1 * [x + 1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))")
 
 
-text {* Inequality from sci.math (see "Leon-Sotelo, por favor"). *}
 
-lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x + y <= x^2 + y^2" by sos 
-
-lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x * y * (x + y) <= x^2 + y^2" by sos 
-
-lemma "0 <= (x::real) & 0 <= y --> x * y * (x + y)^2 <= (x^2 + y^2)^2" by sos
+lemma "abs ((1::real) + x^2) = (1::real) + x^2"
+by (sos_cert "(() & (((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<1 * R<1) * (R<1/2 * [1]^2))))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2)))))))")
+lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<longrightarrow> a < 0"
+by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))")
 
-lemma "(0::real) <= a & 0 <= b & 0 <= c & c * (2 * a + b)^3/ 27 <= x \<longrightarrow> c * a^2 * b <= x" by sos
- 
-lemma "(0::real) < x --> 0 < 1 + x + x^2" by sos
-
-lemma "(0::real) <= x --> 0 < 1 + x + x^2" by sos
-
-lemma "(0::real) < 1 + x^2" by sos
-
-lemma "(0::real) <= 1 + 2 * x + x^2" by sos
-
-lemma "(0::real) < 1 + abs x" by sos
-
-lemma "(0::real) < 1 + (1 + x)^2 * (abs x)" by sos
+lemma "(0::real) < x --> 1 < y --> y * x <= z --> x < z"
+by (sos_cert "((((A<0 * A<1) * R<1) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))")
+lemma "(1::real) < x --> x^2 < y --> 1 < y"
+by (sos_cert "((((A<0 * A<1) * R<1) + ((R<1 * ((R<1/10 * [~2*x + y + 1]^2) + (R<1/10 * [~1*x + y]^2))) + (((A<1 * R<1) * (R<1/2 * [1]^2)) + (((A<0 * R<1) * (R<1 * [x]^2)) + (((A<=0 * R<1) * ((R<1/10 * [x + 1]^2) + (R<1/10 * [x]^2))) + (((A<=0 * (A<1 * R<1)) * (R<1/5 * [1]^2)) + ((A<=0 * (A<0 * R<1)) * (R<1/5 * [1]^2)))))))))")
+lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)"
+by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))")
+lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)"
+by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))")
+lemma "((a::real) * x^2 + b * x + c = 0) --> b^2 >= 4 * a * c"
+by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))")
+lemma "(0::real) <= b & 0 <= c & 0 <= x & 0 <= y & (x^2 = c) & (y^2 = a^2 * c + b) --> a * c <= y * x"
+by (sos_cert "(((A<0 * (A<0 * R<1)) + (((A<=2 * (A<=3 * (A<0 * R<1))) * (R<2 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2)))))")
+lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) --> abs((u * x + v * y) - z) <= (e::real)"
+by (sos_cert "((((A<0 * R<1) + (((A<=3 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=1 * (A<=5 * R<1)) * (R<1 * [1]^2))))) & ((((A<0 * A<1) * R<1) + (((A<=3 * (A<=5 * (A<0 * R<1))) * (R<1 * [1]^2)) + ((A<=1 * (A<=4 * (A<0 * R<1))) * (R<1 * [1]^2))))))")
 
 
-lemma "abs ((1::real) + x^2) = (1::real) + x^2" by sos
-lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<longrightarrow> a < 0" by sos
-
-lemma "(0::real) < x --> 1 < y --> y * x <= z --> x < z" by sos
-lemma "(1::real) < x --> x^2 < y --> 1 < y" by sos
-lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" by sos
-lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" by sos
-lemma "((a::real) * x^2 + b * x + c = 0) --> b^2 >= 4 * a * c" by sos
-lemma "(0::real) <= b & 0 <= c & 0 <= x & 0 <= y & (x^2 = c) & (y^2 = a^2 * c + b) --> a * c <= y * x" by sos
-lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) -->
-  abs((u * x + v * y) - z) <= (e::real)" by sos
-
-(*
-lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 -->
-  y^2 - 7 * y - 12 * x + 17 >= 0" by sos  -- {* Too hard?*}
-*)
+(* lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 --> y^2 - 7 * y - 12 * x + 17 >= 0" by sos *) (* Too hard?*)
 
 lemma "(0::real) <= x --> (1 + x + x^2)/(1 + x^2) <= 1 + x"
-  by sos
+by (sos_cert "(((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2))))))")
 
 lemma "(0::real) <= x --> 1 - x <= 1 / (1 + x + x^2)"
-  by sos
+by (sos_cert "(((R<1 + (([~4/3] * A=0) + ((R<1 * ((R<1/3 * [3/2*x + 1]^2) + (R<7/12 * [x]^2))) + ((A<=0 * R<1) * (R<1/3 * [1]^2)))))) & (((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))))")
 
 lemma "(x::real) <= 1 / 2 --> - x - 2 * x^2 <= - x / (1 - x)"
-  by sos
+by (sos_cert "((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2))))")
 
-lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 -->
-  2*(x::real) = - p + 2*r | 2*x = -p - 2*r" by sos
-*)
+lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 --> 2*(x::real) = - p + 2*r | 2*x = -p - 2*r"
+by (sos_cert "((((((A<0 * A<1) * R<1) + ([~4] * A=0))) & ((((A<0 * A<1) * R<1) + ([4] * A=0)))) & (((((A<0 * A<1) * R<1) + ([4] * A=0))) & ((((A<0 * A<1) * R<1) + ([~4] * A=0)))))")
 
 end
+
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -0,0 +1,158 @@
+(* Title:      positivstellensatz_tools.ML
+   Author:     Philipp Meyer, TU Muenchen
+
+Functions for generating a certificate from a positivstellensatz and vice versa
+*)
+
+signature POSITIVSTELLENSATZ_TOOLS =
+sig
+  val pss_tree_to_cert : RealArith.pss_tree -> string
+
+  val cert_to_pss_tree : Proof.context -> string -> RealArith.pss_tree
+
+end
+
+
+structure PositivstellensatzTools : POSITIVSTELLENSATZ_TOOLS =
+struct
+
+open RealArith FuncUtil
+
+(*** certificate generation ***)
+
+fun string_of_rat r =
+  let
+    val (nom, den) = Rat.quotient_of_rat r
+  in
+    if den = 1 then string_of_int nom
+    else string_of_int nom ^ "/" ^ string_of_int den
+  end
+
+(* map polynomials to strings *)
+
+fun string_of_varpow x k =
+  let
+    val term = term_of x
+    val name = case term of
+      Free (n, _) => n
+    | _ => error "Term in monomial not free variable"
+  in
+    if k = 1 then name else name ^ "^" ^ string_of_int k 
+  end
+
+fun string_of_monomial m = 
+ if Ctermfunc.is_undefined m then "1" 
+ else 
+  let 
+   val m' = dest_monomial m
+   val vps = fold_rev (fn (x,k) => cons (string_of_varpow x k)) m' [] 
+  in foldr1 (fn (s, t) => s ^ "*" ^ t) vps
+  end
+
+fun string_of_cmonomial (m,c) =
+  if Ctermfunc.is_undefined m then string_of_rat c
+  else if c = Rat.one then string_of_monomial m
+  else (string_of_rat c) ^ "*" ^ (string_of_monomial m);
+
+fun string_of_poly p = 
+ if Monomialfunc.is_undefined p then "0" 
+ else
+  let 
+   val cms = map string_of_cmonomial
+     (sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p))
+  in foldr1 (fn (t1, t2) => t1 ^ " + " ^ t2) cms
+  end;
+
+fun pss_to_cert (Axiom_eq i) = "A=" ^ string_of_int i
+  | pss_to_cert (Axiom_le i) = "A<=" ^ string_of_int i
+  | pss_to_cert (Axiom_lt i) = "A<" ^ string_of_int i
+  | pss_to_cert (Rational_eq r) = "R=" ^ string_of_rat r
+  | pss_to_cert (Rational_le r) = "R<=" ^ string_of_rat r
+  | pss_to_cert (Rational_lt r) = "R<" ^ string_of_rat r
+  | pss_to_cert (Square p) = "[" ^ string_of_poly p ^ "]^2"
+  | pss_to_cert (Eqmul (p, pss)) = "([" ^ string_of_poly p ^ "] * " ^ pss_to_cert pss ^ ")"
+  | pss_to_cert (Sum (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " + " ^ pss_to_cert pss2 ^ ")"
+  | pss_to_cert (Product (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " * " ^ pss_to_cert pss2 ^ ")"
+
+fun pss_tree_to_cert Trivial = "()"
+  | pss_tree_to_cert (Cert pss) = "(" ^ pss_to_cert pss ^ ")"
+  | pss_tree_to_cert (Branch (t1, t2)) = "(" ^ pss_tree_to_cert t1 ^ " & " ^ pss_tree_to_cert t2 ^ ")"
+
+(*** certificate parsing ***)
+
+(* basic parser *)
+
+val str = Scan.this_string
+
+val number = Scan.repeat1 (Scan.one Symbol.is_ascii_digit >>
+  (fn s => ord s - ord "0")) >>
+  foldl1 (fn (n, d) => n * 10 + d)
+
+val nat = number
+val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op *;
+val rat = int --| str "/" -- int >> Rat.rat_of_quotient
+val rat_int = rat || int >> Rat.rat_of_int
+
+(* polynomial parser *)
+
+fun repeat_sep s f = f ::: Scan.repeat (str s |-- f)
+
+val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
+
+fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
+  (fn (x, k) => (cterm_of (Context.theory_of_proof ctxt) (Free (x, @{typ real})), k)) 
+
+fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
+  foldl (uncurry Ctermfunc.update) Ctermfunc.undefined
+
+fun parse_cmonomial ctxt =
+  rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
+  (parse_monomial ctxt) >> (fn m => (m, Rat.one)) ||
+  rat_int >> (fn r => (Ctermfunc.undefined, r))
+
+fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
+  foldl (uncurry Monomialfunc.update) Monomialfunc.undefined
+
+(* positivstellensatz parser *)
+
+val parse_axiom =
+  (str "A=" |-- int >> Axiom_eq) ||
+  (str "A<=" |-- int >> Axiom_le) ||
+  (str "A<" |-- int >> Axiom_lt)
+
+val parse_rational =
+  (str "R=" |-- rat_int >> Rational_eq) ||
+  (str "R<=" |-- rat_int >> Rational_le) ||
+  (str "R<" |-- rat_int >> Rational_lt)
+
+fun parse_cert ctxt input =
+  let
+    val pc = parse_cert ctxt
+    val pp = parse_poly ctxt
+  in
+  (parse_axiom ||
+   parse_rational ||
+   str "[" |-- pp --| str "]^2" >> Square ||
+   str "([" |-- pp --| str "]*" -- pc --| str ")" >> Eqmul ||
+   str "(" |-- pc --| str "*" -- pc --| str ")" >> Product ||
+   str "(" |-- pc --| str "+" -- pc --| str ")" >> Sum) input
+  end
+
+fun parse_cert_tree ctxt input =
+  let
+    val pc = parse_cert ctxt
+    val pt = parse_cert_tree ctxt
+  in
+  (str "()" >> K Trivial ||
+   str "(" |-- pc --| str ")" >> Cert ||
+   str "(" |-- pt --| str "&" -- pt --| str ")" >> Branch) input
+  end
+
+(* scanner *)
+
+fun cert_to_pss_tree ctxt input_str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt)
+  (filter_out Symbol.is_blank (Symbol.explode input_str))
+
+end
+
+
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -136,13 +136,32 @@
     run_solver name (Path.explode cmd) find_failure
   end
 
+(* certificate output *)
+
+fun output_line cert = "To repeat this proof with a certifiate use this command:\n" ^
+        (Markup.markup Markup.sendback) ("by (sos_cert \"" ^ cert ^ "\")")
+
+val print_cert = Output.writeln o output_line o PositivstellensatzTools.pss_tree_to_cert
+
 (* setup tactic *)
 
-fun sos_solver name = (SIMPLE_METHOD' o (Sos.sos_tac (call_solver name))) 
+fun parse_cert (input as (ctxt, _)) = 
+  (Scan.lift OuterParse.string >>
+    PositivstellensatzTools.cert_to_pss_tree (Context.proof_of ctxt)) input
+
+fun sos_solver print method = (SIMPLE_METHOD' o (Sos.sos_tac print method)) 
 
-val sos_method = Scan.option (Scan.lift OuterParse.xname) >> sos_solver
+val sos_method =
+   Scan.lift (Scan.option OuterParse.xname) >> (fn n => Sos.Prover (call_solver n)) >>
+   sos_solver print_cert
 
-val setup = Method.setup @{binding sos} sos_method
-  "Prove universal problems over the reals using sums of squares"
+val sos_cert_method =
+  parse_cert >> Sos.Certificate >> sos_solver ignore
+
+val setup =
+     Method.setup @{binding sos} sos_method
+     "Prove universal problems over the reals using sums of squares"
+  #> Method.setup @{binding sos_cert} sos_cert_method
+     "Prove universal problems over the reals using sums of squares with certificates"
 
 end
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -8,7 +8,12 @@
 signature SOS =
 sig
 
-  val sos_tac : (string -> string) -> Proof.context -> int -> Tactical.tactic
+  datatype proof_method =
+    Certificate of RealArith.pss_tree
+  | Prover of (string -> string)
+
+  val sos_tac : (RealArith.pss_tree -> unit) ->
+    proof_method -> Proof.context -> int -> tactic
 
   val debugging : bool ref;
   
@@ -18,6 +23,8 @@
 structure Sos : SOS = 
 struct
 
+open FuncUtil;
+
 val rat_0 = Rat.zero;
 val rat_1 = Rat.one;
 val rat_2 = Rat.two;
@@ -59,6 +66,10 @@
 
 exception Failure of string;
 
+datatype proof_method =
+    Certificate of RealArith.pss_tree
+  | Prover of (string -> string)
+
 (* Turn a rational into a decimal string with d sig digits.                  *)
 
 local
@@ -93,23 +104,11 @@
 
 (* The main types.                                                           *)
 
-fun strict_ord ord (x,y) = case ord (x,y) of LESS => LESS | _ => GREATER
-
-structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
-
 type vector = int* Rat.rat Intfunc.T;
 
 type matrix = (int*int)*(Rat.rat Intpairfunc.T);
 
-type monomial = int Ctermfunc.T;
-
-val cterm_ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t))
- fun monomial_ord (m1,m2) = list_ord (prod_ord cterm_ord int_ord) (Ctermfunc.graph m1, Ctermfunc.graph m2)
-structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
-
-type poly = Rat.rat Monomialfunc.T;
-
- fun iszero (k,r) = r =/ rat_0;
+fun iszero (k,r) = r =/ rat_0;
 
 fun fold_rev2 f l1 l2 b =
   case (l1,l2) of
@@ -346,11 +345,6 @@
   sort humanorder_varpow (Ctermfunc.graph m2))
 end;
 
-fun fold1 f l =  case l of
-   []     => error "fold1"
- | [x]    => x
- | (h::t) => f h (fold1 f t);
-
 (* Conversions to strings.                                                   *)
 
 fun string_of_vector min_size max_size (v:vector) =
@@ -359,7 +353,7 @@
   let 
    val n = max min_size (min n_raw max_size) 
    val xs = map (Rat.string_of_rat o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
-  in "[" ^ fold1 (fn s => fn t => s ^ ", " ^ t) xs ^
+  in "[" ^ foldr1 (fn (s, t) => s ^ ", " ^ t) xs ^
   (if n_raw > max_size then ", ...]" else "]")
   end
  end;
@@ -370,7 +364,7 @@
   val i = min max_size i_raw 
   val j = min max_size j_raw
   val rstr = map (fn k => string_of_vector j j (row k m)) (1 upto i) 
- in "["^ fold1 (fn s => fn t => s^";\n "^t) rstr ^
+ in "["^ foldr1 (fn (s, t) => s^";\n "^t) rstr ^
   (if j > max_size then "\n ...]" else "]")
  end;
 
@@ -396,7 +390,7 @@
  if Ctermfunc.is_undefined m then "1" else
  let val vps = fold_rev (fn (x,k) => fn a => string_of_varpow x k :: a)
   (sort humanorder_varpow (Ctermfunc.graph m)) [] 
- in fold1 (fn s => fn t => s^"*"^t) vps
+ in foldr1 (fn (s, t) => s^"*"^t) vps
  end;
 
 fun string_of_cmonomial (c,m) =
@@ -404,7 +398,7 @@
  else if c =/ rat_1 then string_of_monomial m
  else Rat.string_of_rat c ^ "*" ^ string_of_monomial m;;
 
-fun string_of_poly (p:poly) =
+fun string_of_poly p =
  if Monomialfunc.is_undefined p then "<<0>>" else
  let 
   val cms = sort (fn ((m1,_),(m2,_)) => humanorder_monomial m1  m2) (Monomialfunc.graph p)
@@ -478,10 +472,9 @@
  let 
   val n = dim v
   val strs = map (decimalize 20 o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
- in fold1 (fn x => fn y => x ^ " " ^ y) strs ^ "\n"
+ in foldr1 (fn (x, y) => x ^ " " ^ y) strs ^ "\n"
  end;
 
-fun increasing f ord (x,y) = ord (f x, f y);
 fun triple_int_ord ((a,b,c),(a',b',c')) = 
  prod_ord int_ord (prod_ord int_ord int_ord) 
     ((a,(b,c)),(a',(b',c')));
@@ -989,7 +982,7 @@
  let val alts =
   map (fn k => let val oths = enumerate_monomials (d - k) (tl vars) 
                in map (fn ks => if k = 0 then ks else Ctermfunc.update (hd vars, k) ks) oths end) (0 upto d) 
- in fold1 (curry op @) alts
+ in foldr1 op @ alts
  end;
 
 (* Enumerate products of distinct input polys with degree <= d.              *)
@@ -1040,7 +1033,7 @@
  in
   string_of_int m ^ "\n" ^
   string_of_int nblocks ^ "\n" ^
-  (fold1 (fn s => fn t => s^" "^t) (map string_of_int blocksizes)) ^
+  (foldr1 (fn (s, t) => s^" "^t) (map string_of_int blocksizes)) ^
   "\n" ^
   sdpa_of_vector obj ^
   fold_rev2 (fn k => fn m => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a)
@@ -1080,11 +1073,6 @@
   fun tryfind f = tryfind_with "tryfind" f
 end
 
-(*
-fun tryfind f [] = error "tryfind"
-  | tryfind f (x::xs) = (f x handle ERROR _ => tryfind f xs);
-*)
-
 (* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *)
 
  
@@ -1210,61 +1198,17 @@
 fun deepen f n = 
   (writeln ("Searching with depth limit " ^ string_of_int n) ; (f n handle Failure s => (writeln ("failed with message: " ^ s) ; deepen f (n+1))))
 
-(* The ordering so we can create canonical HOL polynomials.                  *)
 
-fun dest_monomial mon = sort (increasing fst cterm_ord) (Ctermfunc.graph mon);
-
-fun monomial_order (m1,m2) =
- if Ctermfunc.is_undefined m2 then LESS 
- else if Ctermfunc.is_undefined m1 then GREATER 
- else
-  let val mon1 = dest_monomial m1 
-      val mon2 = dest_monomial m2
-      val deg1 = fold (curry op + o snd) mon1 0
-      val deg2 = fold (curry op + o snd) mon2 0 
-  in if deg1 < deg2 then GREATER else if deg1 > deg2 then LESS
-     else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
-  end;
-
-fun dest_poly p =
-  map (fn (m,c) => (c,dest_monomial m))
-      (sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p));
-
-(* Map back polynomials and their composites to HOL.                         *)
+(* Map back polynomials and their composites to a positivstellensatz.        *)
 
 local
  open Thm Numeral RealArith
 in
 
-fun cterm_of_varpow x k = if k = 1 then x else capply (capply @{cterm "op ^ :: real => _"} x) 
-  (mk_cnumber @{ctyp nat} k)
-
-fun cterm_of_monomial m = 
- if Ctermfunc.is_undefined m then @{cterm "1::real"} 
- else 
-  let 
-   val m' = dest_monomial m
-   val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' [] 
-  in fold1 (fn s => fn t => capply (capply @{cterm "op * :: real => _"} s) t) vps
-  end
-
-fun cterm_of_cmonomial (m,c) = if Ctermfunc.is_undefined m then cterm_of_rat c
-    else if c = Rat.one then cterm_of_monomial m
-    else capply (capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
-
-fun cterm_of_poly p = 
- if Monomialfunc.is_undefined p then @{cterm "0::real"} 
- else
-  let 
-   val cms = map cterm_of_cmonomial
-     (sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p))
-  in fold1 (fn t1 => fn t2 => capply(capply @{cterm "op + :: real => _"} t1) t2) cms
-  end;
-
-fun cterm_of_sqterm (c,p) = Product(Rational_lt c,Square(cterm_of_poly p));
+fun cterm_of_sqterm (c,p) = Product(Rational_lt c,Square p);
 
 fun cterm_of_sos (pr,sqs) = if null sqs then pr
-  else Product(pr,fold1 (fn a => fn b => Sum(a,b)) (map cterm_of_sqterm sqs));
+  else Product(pr,foldr1 (fn (a, b) => Sum(a,b)) (map cterm_of_sqterm sqs));
 
 end
 
@@ -1275,14 +1219,14 @@
   fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS
 in
   (* FIXME: Replace tryfind by get_first !! *)
-fun real_nonlinear_prover prover ctxt =
+fun real_nonlinear_prover proof_method ctxt =
  let 
   val {add,mul,neg,pow,sub,main} =  Normalizer.semiring_normalizers_ord_wrapper ctxt
       (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
      simple_cterm_ord
   val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
        real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
-  fun mainf  translator (eqs,les,lts) = 
+  fun mainf cert_choice translator (eqs,les,lts) = 
   let 
    val eq0 = map (poly_of_term o dest_arg1 o concl) eqs
    val le0 = map (poly_of_term o dest_arg o concl) les
@@ -1303,33 +1247,49 @@
                      else raise Failure "trivial_axiom: Not a trivial axiom"
      | _ => error "trivial_axiom: Not a trivial axiom"
    in 
-  ((let val th = tryfind trivial_axiom (keq @ klep @ kltp)
-   in fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th end)
-   handle Failure _ => (
-    let 
-     val pol = fold_rev poly_mul (map fst ltp) (poly_const Rat.one)
-     val leq = lep @ ltp
-     fun tryall d =
-      let val e = multidegree pol
-          val k = if e = 0 then 0 else d div e
-          val eq' = map fst eq 
-      in tryfind (fn i => (d,i,real_positivnullstellensatz_general prover false d eq' leq
-                            (poly_neg(poly_pow pol i))))
-              (0 upto k)
-      end
-    val (d,i,(cert_ideal,cert_cone)) = deepen tryall 0
-    val proofs_ideal =
-      map2 (fn q => fn (p,ax) => Eqmul(cterm_of_poly q,ax)) cert_ideal eq
-    val proofs_cone = map cterm_of_sos cert_cone
-    val proof_ne = if null ltp then Rational_lt Rat.one else
-      let val p = fold1 (fn s => fn t => Product(s,t)) (map snd ltp) 
-      in  funpow i (fn q => Product(p,q)) (Rational_lt Rat.one)
-      end
-    val proof = fold1 (fn s => fn t => Sum(s,t))
-                           (proof_ne :: proofs_ideal @ proofs_cone) 
-    in writeln "Translating proof certificate to HOL";
-       translator (eqs,les,lts) proof
-    end))
+  (let val th = tryfind trivial_axiom (keq @ klep @ kltp)
+   in
+    (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th, Trivial)
+   end)
+   handle Failure _ => 
+     (let val proof =
+       (case proof_method of Certificate certs =>
+         (* choose certificate *)
+         let
+           fun chose_cert [] (Cert c) = c
+             | chose_cert (Left::s) (Branch (l, _)) = chose_cert s l
+             | chose_cert (Right::s) (Branch (_, r)) = chose_cert s r
+             | chose_cert _ _ = error "certificate tree in invalid form"
+         in
+           chose_cert cert_choice certs
+         end
+       | Prover prover =>
+         (* call prover *)
+         let 
+          val pol = fold_rev poly_mul (map fst ltp) (poly_const Rat.one)
+          val leq = lep @ ltp
+          fun tryall d =
+           let val e = multidegree pol
+               val k = if e = 0 then 0 else d div e
+               val eq' = map fst eq 
+           in tryfind (fn i => (d,i,real_positivnullstellensatz_general prover false d eq' leq
+                                 (poly_neg(poly_pow pol i))))
+                   (0 upto k)
+           end
+         val (d,i,(cert_ideal,cert_cone)) = deepen tryall 0
+         val proofs_ideal =
+           map2 (fn q => fn (p,ax) => Eqmul(q,ax)) cert_ideal eq
+         val proofs_cone = map cterm_of_sos cert_cone
+         val proof_ne = if null ltp then Rational_lt Rat.one else
+           let val p = foldr1 (fn (s, t) => Product(s,t)) (map snd ltp) 
+           in  funpow i (fn q => Product(p,q)) (Rational_lt Rat.one)
+           end
+         in 
+           foldr1 (fn (s, t) => Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) 
+         end)
+     in
+        (translator (eqs,les,lts) proof, Cert proof)
+     end)
    end
  in mainf end
 end
@@ -1396,7 +1356,7 @@
          orelse g aconvc @{cterm "op < :: real => _"} 
        then arg_conv cv ct else arg1_conv cv ct
     end
-  fun mainf translator =
+  fun mainf cert_choice translator =
    let 
     fun substfirst(eqs,les,lts) =
       ((let 
@@ -1407,7 +1367,7 @@
                                    aconvc @{cterm "0::real"}) (map modify eqs),
                                    map modify les,map modify lts)
        end)
-       handle Failure  _ => real_nonlinear_prover prover ctxt translator (rev eqs, rev les, rev lts))
+       handle Failure  _ => real_nonlinear_prover prover ctxt cert_choice translator (rev eqs, rev les, rev lts))
     in substfirst
    end
 
@@ -1417,7 +1377,8 @@
 
 (* Overall function. *)
 
-fun real_sos prover ctxt t = gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt) t;
+fun real_sos prover ctxt =
+  gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt)
 end;
 
 (* A tactic *)
@@ -1429,8 +1390,6 @@
    end
 | _ => ([],ct)
 
-fun core_sos_conv prover ctxt t = Drule.arg_cong_rule @{cterm Trueprop} (real_sos prover ctxt (Thm.dest_arg t) RS @{thm Eq_TrueI})
-
 val known_sos_constants = 
   [@{term "op ==>"}, @{term "Trueprop"}, 
    @{term "op -->"}, @{term "op &"}, @{term "op |"}, 
@@ -1458,17 +1417,19 @@
   val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs 
           then error "SOS: not sos. Variables with type not real" else ()
   val vs = Term.add_vars t []
-  val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs 
+  val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) vs 
           then error "SOS: not sos. Variables with type not real" else ()
   val ukcs = subtract (fn (t,p) => Const p aconv t) kcts (Term.add_consts t [])
   val _ = if  null ukcs then () 
               else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs))
 in () end
 
-fun core_sos_tac prover ctxt = CSUBGOAL (fn (ct, i) => 
+fun core_sos_tac print_cert prover ctxt = CSUBGOAL (fn (ct, i) => 
   let val _ = check_sos known_sos_constants ct
       val (avs, p) = strip_all ct
-      val th = standard (fold_rev forall_intr avs (real_sos prover ctxt (Thm.dest_arg p)))
+      val (ths, certificates) = real_sos prover ctxt (Thm.dest_arg p)
+      val th = standard (fold_rev forall_intr avs ths)
+      val _ = print_cert certificates
   in rtac th i end);
 
 fun default_SOME f NONE v = SOME v
@@ -1506,7 +1467,7 @@
 
 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
 
-fun sos_tac prover ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac prover ctxt
+fun sos_tac print_cert prover ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac print_cert prover ctxt
 
 
 end;
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/normarith.ML
--- a/src/HOL/Library/normarith.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/normarith.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -15,7 +15,7 @@
 structure NormArith : NORM_ARITH = 
 struct
 
- open Conv Thm;
+ open Conv Thm FuncUtil;
  val bool_eq = op = : bool *bool -> bool
   fun dest_ratconst t = case term_of t of
    Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
@@ -330,13 +330,13 @@
    val zerodests = filter
         (fn t => null (Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
 
-  in RealArith.real_linear_prover translator
+  in fst (RealArith.real_linear_prover translator
         (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
             zerodests,
         map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
                        arg_conv (arg_conv real_poly_conv))) ges',
         map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
-                       arg_conv (arg_conv real_poly_conv))) gts)
+                       arg_conv (arg_conv real_poly_conv))) gts))
   end
 in val real_vector_combo_prover = real_vector_combo_prover
 end;
@@ -389,9 +389,9 @@
    val (th1,th2) = conj_pair(rawrule th)
   in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc
   end
-in fun real_vector_prover ctxt translator (eqs,ges,gts) =
-     real_vector_ineq_prover ctxt translator
-         (fold_rev (splitequation ctxt) eqs ges,gts)
+in fun real_vector_prover ctxt _ translator (eqs,ges,gts) =
+     (real_vector_ineq_prover ctxt translator
+         (fold_rev (splitequation ctxt) eqs ges,gts), RealArith.Trivial)
 end;
 
   fun init_conv ctxt = 
@@ -400,7 +400,7 @@
    then_conv field_comp_conv 
    then_conv nnf_conv
 
- fun pure ctxt = RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt);
+ fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt);
  fun norm_arith ctxt ct = 
   let 
    val ctxt' = Variable.declare_term (term_of ct) ctxt
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Library/positivstellensatz.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -1,10 +1,11 @@
-(* Title:      Library/positivstellensatz
+(* Title:      Library/Sum_Of_Squares/positivstellensatz
    Author:     Amine Chaieb, University of Cambridge
    Description: A generic arithmetic prover based on Positivstellensatz certificates --- 
     also implements Fourrier-Motzkin elimination as a special case Fourrier-Motzkin elimination.
 *)
 
 (* A functor for finite mappings based on Tables *)
+
 signature FUNC = 
 sig
  type 'a T
@@ -75,27 +76,54 @@
 end
 end;
 
+(* Some standard functors and utility functions for them *)
+
+structure FuncUtil =
+struct
+
+fun increasing f ord (x,y) = ord (f x, f y);
+
 structure Intfunc = FuncFun(type key = int val ord = int_ord);
+structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
+structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
 structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
 structure Termfunc = FuncFun(type key = term val ord = TermOrd.fast_term_ord);
-structure Ctermfunc = FuncFun(type key = cterm val ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t)));
+
+val cterm_ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t))
+
+structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
+
+type monomial = int Ctermfunc.T;
 
-structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
+fun monomial_ord (m1,m2) = list_ord (prod_ord cterm_ord int_ord) (Ctermfunc.graph m1, Ctermfunc.graph m2)
+
+structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
 
+type poly = Rat.rat Monomialfunc.T;
+
+(* The ordering so we can create canonical HOL polynomials.                  *)
 
-    (* Some useful derived rules *)
-fun deduct_antisym_rule tha thb = 
-    equal_intr (implies_intr (cprop_of thb) tha) 
-     (implies_intr (cprop_of tha) thb);
+fun dest_monomial mon = sort (increasing fst cterm_ord) (Ctermfunc.graph mon);
 
-fun prove_hyp tha thb = 
-  if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
-  then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb;
+fun monomial_order (m1,m2) =
+ if Ctermfunc.is_undefined m2 then LESS 
+ else if Ctermfunc.is_undefined m1 then GREATER 
+ else
+  let val mon1 = dest_monomial m1 
+      val mon2 = dest_monomial m2
+      val deg1 = fold (curry op + o snd) mon1 0
+      val deg2 = fold (curry op + o snd) mon2 0 
+  in if deg1 < deg2 then GREATER else if deg1 > deg2 then LESS
+     else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
+  end;
 
+end
 
+(* positivstellensatz datatype and prover generation *)
 
 signature REAL_ARITH = 
 sig
+  
   datatype positivstellensatz =
    Axiom_eq of int
  | Axiom_le of int
@@ -103,34 +131,41 @@
  | Rational_eq of Rat.rat
  | Rational_le of Rat.rat
  | Rational_lt of Rat.rat
- | Square of cterm
- | Eqmul of cterm * positivstellensatz
+ | Square of FuncUtil.poly
+ | Eqmul of FuncUtil.poly * positivstellensatz
  | Sum of positivstellensatz * positivstellensatz
  | Product of positivstellensatz * positivstellensatz;
 
+datatype pss_tree = Trivial | Cert of positivstellensatz | Branch of pss_tree * pss_tree
+
+datatype tree_choice = Left | Right
+
+type prover = tree_choice list -> 
+  (thm list * thm list * thm list -> positivstellensatz -> thm) ->
+  thm list * thm list * thm list -> thm * pss_tree
+type cert_conv = cterm -> thm * pss_tree
+
 val gen_gen_real_arith :
-  Proof.context -> (Rat.rat -> Thm.cterm) * conv * conv * conv * 
-   conv * conv * conv * conv * conv * conv * 
-    ( (thm list * thm list * thm list -> positivstellensatz -> thm) ->
-        thm list * thm list * thm list -> thm) -> conv
-val real_linear_prover : 
-  (thm list * thm list * thm list -> positivstellensatz -> thm) ->
-   thm list * thm list * thm list -> thm
+  Proof.context -> (Rat.rat -> cterm) * conv * conv * conv *
+   conv * conv * conv * conv * conv * conv * prover -> cert_conv
+val real_linear_prover : (thm list * thm list * thm list -> positivstellensatz -> thm) ->
+  thm list * thm list * thm list -> thm * pss_tree
 
 val gen_real_arith : Proof.context ->
-   (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv * conv *
-   ( (thm list * thm list * thm list -> positivstellensatz -> thm) ->
-       thm list * thm list * thm list -> thm) -> conv
-val gen_prover_real_arith : Proof.context ->
-   ((thm list * thm list * thm list -> positivstellensatz -> thm) ->
-     thm list * thm list * thm list -> thm) -> conv
-val real_arith : Proof.context -> conv
+  (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv
+
+val gen_prover_real_arith : Proof.context -> prover -> cert_conv
+
+val is_ratconst : cterm -> bool
+val dest_ratconst : cterm -> Rat.rat
+val cterm_of_rat : Rat.rat -> cterm
+
 end
 
-structure RealArith (* : REAL_ARITH *)=
+structure RealArith : REAL_ARITH =
 struct
 
- open Conv Thm;;
+ open Conv Thm FuncUtil;;
 (* ------------------------------------------------------------------------- *)
 (* Data structure for Positivstellensatz refutations.                        *)
 (* ------------------------------------------------------------------------- *)
@@ -142,12 +177,18 @@
  | Rational_eq of Rat.rat
  | Rational_le of Rat.rat
  | Rational_lt of Rat.rat
- | Square of cterm
- | Eqmul of cterm * positivstellensatz
+ | Square of FuncUtil.poly
+ | Eqmul of FuncUtil.poly * positivstellensatz
  | Sum of positivstellensatz * positivstellensatz
  | Product of positivstellensatz * positivstellensatz;
          (* Theorems used in the procedure *)
 
+datatype pss_tree = Trivial | Cert of positivstellensatz | Branch of pss_tree * pss_tree
+datatype tree_choice = Left | Right
+type prover = tree_choice list -> 
+  (thm list * thm list * thm list -> positivstellensatz -> thm) ->
+  thm list * thm list * thm list -> thm * pss_tree
+type cert_conv = cterm -> thm * pss_tree
 
 val my_eqs = ref ([] : thm list);
 val my_les = ref ([] : thm list);
@@ -164,6 +205,16 @@
 val my_poly_add_conv = ref no_conv;
 val my_poly_mul_conv = ref no_conv;
 
+
+    (* Some useful derived rules *)
+fun deduct_antisym_rule tha thb = 
+    equal_intr (implies_intr (cprop_of thb) tha) 
+     (implies_intr (cprop_of tha) thb);
+
+fun prove_hyp tha thb = 
+  if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
+  then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb;
+
 fun conjunctions th = case try Conjunction.elim th of
    SOME (th1,th2) => (conjunctions th1) @ conjunctions th2
  | NONE => [th];
@@ -292,7 +343,6 @@
  | Abs (_,_,t') => find_cterm p (Thm.dest_abs NONE t |> snd)
  | _ => raise CTERM ("find_cterm",[t]);
 
-
     (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
 fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
 fun is_comb t = case (term_of t) of _$_ => true | _ => false;
@@ -300,6 +350,39 @@
 fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
   handle CTERM _ => false;
 
+
+(* Map back polynomials to HOL.                         *)
+
+local
+ open Thm Numeral
+in
+
+fun cterm_of_varpow x k = if k = 1 then x else capply (capply @{cterm "op ^ :: real => _"} x) 
+  (mk_cnumber @{ctyp nat} k)
+
+fun cterm_of_monomial m = 
+ if Ctermfunc.is_undefined m then @{cterm "1::real"} 
+ else 
+  let 
+   val m' = dest_monomial m
+   val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' [] 
+  in foldr1 (fn (s, t) => capply (capply @{cterm "op * :: real => _"} s) t) vps
+  end
+
+fun cterm_of_cmonomial (m,c) = if Ctermfunc.is_undefined m then cterm_of_rat c
+    else if c = Rat.one then cterm_of_monomial m
+    else capply (capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
+
+fun cterm_of_poly p = 
+ if Monomialfunc.is_undefined p then @{cterm "0::real"} 
+ else
+  let 
+   val cms = map cterm_of_cmonomial
+     (sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p))
+  in foldr1 (fn (t1, t2) => capply(capply @{cterm "op + :: real => _"} t1) t2) cms
+  end;
+
+end;
     (* A general real arithmetic prover *)
 
 fun gen_gen_real_arith ctxt (mk_numeric,
@@ -368,8 +451,8 @@
       | Rational_lt x => eqT_elim(numeric_gt_conv(capply @{cterm Trueprop} 
                       (capply (capply @{cterm "op <::real => _"} @{cterm "0::real"})
                         (mk_numeric x))))
-      | Square t => square_rule t
-      | Eqmul(t,p) => emul_rule t (translate p)
+      | Square pt => square_rule (cterm_of_poly pt)
+      | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
       | Sum(p1,p2) => add_rule (translate p1) (translate p2)
       | Product(p1,p2) => mul_rule (translate p1) (translate p2)
    in fconv_rule (first_conv [numeric_ge_conv, numeric_gt_conv, numeric_eq_conv, all_conv]) 
@@ -394,13 +477,13 @@
        val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
    in implies_elim (implies_elim (implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th) (implies_intr (capply @{cterm Trueprop} p) th1)) (implies_intr (capply @{cterm Trueprop} q) th2)
    end
- fun overall dun ths = case ths of
+ fun overall cert_choice dun ths = case ths of
   [] =>
    let 
     val (eq,ne) = List.partition (is_req o concl) dun
      val (le,nl) = List.partition (is_ge o concl) ne
      val lt = filter (is_gt o concl) nl 
-    in prover hol_of_positivstellensatz (eq,le,lt) end
+    in prover (rev cert_choice) hol_of_positivstellensatz (eq,le,lt) end
  | th::oths =>
    let 
     val ct = concl th 
@@ -408,13 +491,13 @@
     if is_conj ct  then
      let 
       val (th1,th2) = conj_pair th in
-      overall dun (th1::th2::oths) end
+      overall cert_choice dun (th1::th2::oths) end
     else if is_disj ct then
       let 
-       val th1 = overall dun (assume (capply @{cterm Trueprop} (dest_arg1 ct))::oths)
-       val th2 = overall dun (assume (capply @{cterm Trueprop} (dest_arg ct))::oths)
-      in disj_cases th th1 th2 end
-   else overall (th::dun) oths
+       val (th1, cert1) = overall (Left::cert_choice) dun (assume (capply @{cterm Trueprop} (dest_arg1 ct))::oths)
+       val (th2, cert2) = overall (Right::cert_choice) dun (assume (capply @{cterm Trueprop} (dest_arg ct))::oths)
+      in (disj_cases th th1 th2, Branch (cert1, cert2)) end
+   else overall cert_choice (th::dun) oths
   end
   fun dest_binary b ct = if is_binop b ct then dest_binop ct 
                          else raise CTERM ("dest_binary",[b,ct])
@@ -496,16 +579,16 @@
   val nct = capply @{cterm Trueprop} (capply @{cterm "Not"} ct)
   val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
   val tm0 = dest_arg (rhs_of th0)
-  val th = if tm0 aconvc @{cterm False} then equal_implies_1_rule th0 else
+  val (th, certificates) = if tm0 aconvc @{cterm False} then (equal_implies_1_rule th0, Trivial) else
    let 
     val (evs,bod) = strip_exists tm0
     val (avs,ibod) = strip_forall bod
     val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
-    val th2 = overall [] [specl avs (assume (rhs_of th1))]
+    val (th2, certs) = overall [] [] [specl avs (assume (rhs_of th1))]
     val th3 = fold simple_choose evs (prove_hyp (equal_elim th1 (assume (capply @{cterm Trueprop} bod))) th2)
-   in  Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3)
+   in (Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3), certs)
    end
-  in implies_elim (instantiate' [] [SOME ct] pth_final) th
+  in (implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
  end
 in f
 end;
@@ -580,7 +663,7 @@
          val k = (Rat.neg d) */ Rat.abs c // c
          val e' = linear_cmul k e
          val t' = linear_cmul (Rat.abs c) t
-         val p' = Eqmul(cterm_of_rat k,p)
+         val p' = Eqmul(Monomialfunc.onefunc (Ctermfunc.undefined, k),p)
          val q' = Product(Rational_lt(Rat.abs c),q) 
         in (linear_add e' t',Sum(p',q')) 
         end 
@@ -632,7 +715,7 @@
   val le_pols' = le_pols @ map (fn v => Ctermfunc.onefunc (v,Rat.one)) aliens
   val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
   val le' = le @ map (fn a => instantiate' [] [SOME (dest_arg a)] @{thm real_of_nat_ge_zero}) aliens 
- in (translator (eq,le',lt) proof) : thm
+ in ((translator (eq,le',lt) proof), Trivial)
  end
 end;
 
@@ -698,5 +781,4 @@
     main,neg,add,mul, prover)
 end;
 
-fun real_arith ctxt = gen_prover_real_arith ctxt real_linear_prover;
 end
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Lim.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -84,6 +84,8 @@
 lemma LIM_const [simp]: "(%x. k) -- x --> k"
 by (simp add: LIM_def)
 
+lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
+
 lemma LIM_add:
   fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   assumes f: "f -- a --> L" and g: "g -- a --> M"
@@ -544,7 +546,7 @@
     case True thus ?thesis using `0 < s` by auto
   next
     case False hence "s / 2 \<ge> (x - b) / 2" by auto
-    hence "?x = (x + b) / 2" by(simp add:field_simps)
+    hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
     thus ?thesis using `b < x` by auto
   qed
   hence "0 \<le> f ?x" using all_le `?x < x` by auto
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/MicroJava/BV/Effect.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/BV/Effect.thy
-    ID:         $Id$
     Author:     Gerwin Klein
     Copyright   2000 Technische Universitaet Muenchen
 *)
@@ -391,7 +390,7 @@
   with Pair 
   have "?app s \<Longrightarrow> ?P s" by (simp only:)
   moreover
-  have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp)
+  have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min_max.inf_absorb2)
   ultimately
   show ?thesis by (rule iffI) 
 qed 
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/BV/LBVSpec.thy
-    ID:         $Id$
     Author:     Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 *)
@@ -293,7 +292,7 @@
   shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
 proof -
   from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
-  with suc wtl show ?thesis by (simp)
+  with suc wtl show ?thesis by (simp add: min_max.inf_absorb2)
 qed
 
 lemma (in lbv) wtl_all:
@@ -308,7 +307,7 @@
   with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp 
   from pc have "is!pc = drop pc is ! 0" by simp
   with Cons have "is!pc = i" by simp
-  with take pc show ?thesis by (auto)
+  with take pc show ?thesis by (auto simp add: min_max.inf_absorb2)
 qed
 
 section "preserves-type"
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/Comp/CorrCompTp.thy
-    ID:         $Id$
     Author:     Martin Strecker
 *)
 
@@ -1058,7 +1057,7 @@
 lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
   \<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
 apply (intro strip)
 apply (rule conjI)
 apply (rule check_type_mono, assumption, simp)
@@ -1069,7 +1068,7 @@
   bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) 
-  apply (simp add: check_type_simps)
+  apply (simp add: check_type_simps min_max.sup_absorb1)
   apply clarify
   apply (rule_tac x="(length ST)" in exI)
   apply simp+
@@ -1092,7 +1091,7 @@
   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1111,7 +1110,7 @@
   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1127,7 +1126,7 @@
   \<Longrightarrow> bc_mt_corresp [Load i] 
          (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1148,10 +1147,10 @@
 lemma bc_mt_corresp_Store_init: "\<lbrakk> i < length LT \<rbrakk>
   \<Longrightarrow> bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
-  apply (simp add: max_ssize_def  max_of_list_def )
+  apply (simp add: max_ssize_def  max_of_list_def)
   apply (simp add: ssize_sto_def)
   apply (intro strip)
-apply (simp add: check_type_simps)
+apply (simp add: check_type_simps min_max.sup_absorb1)
 apply clarify
 apply (rule conjI)
 apply (rule_tac x="(length ST)" in exI)
@@ -1159,14 +1158,13 @@
 done
 
 
-
 lemma bc_mt_corresp_Store: "\<lbrakk> i < length LT; cG  \<turnstile>  LT[i := OK T] <=l LT \<rbrakk>
   \<Longrightarrow> bc_mt_corresp [Store i] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: sup_state_conv)
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  apply (intro strip)
-apply (simp add: check_type_simps)
+apply (simp add: check_type_simps min_max.sup_absorb1)
 apply clarify
 apply (rule_tac x="(length ST)" in exI)
 apply simp+
@@ -1176,7 +1174,7 @@
 lemma bc_mt_corresp_Dup: "
   bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
-             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1189,7 +1187,7 @@
 lemma bc_mt_corresp_Dup_x1: "
   bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
-              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1206,7 +1204,7 @@
          (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
-  apply (simp add: check_type_simps)
+  apply (simp add: check_type_simps min_max.sup_absorb1)
   apply clarify
   apply (rule_tac x="Suc (length ST)" in exI)
   apply simp+
@@ -1249,7 +1247,7 @@
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
 
   apply (intro strip)
-apply (simp add: check_type_simps)
+apply (simp add: check_type_simps min_max.sup_absorb1)
 apply clarify
 apply (rule_tac x="Suc (length ST)" in exI)
 apply simp+
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/OrderedGroup.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -1075,17 +1075,16 @@
 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
 
 lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
-by (simp add: pprt_def sup_aci)
-
+  by (simp add: pprt_def sup_aci sup_absorb1)
 
 lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
-by (simp add: nprt_def inf_aci)
+  by (simp add: nprt_def inf_aci inf_absorb1)
 
 lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
-by (simp add: pprt_def sup_aci)
+  by (simp add: pprt_def sup_aci sup_absorb2)
 
 lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
-by (simp add: nprt_def inf_aci)
+  by (simp add: nprt_def inf_aci inf_absorb2)
 
 lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
 proof -
@@ -1119,7 +1118,7 @@
   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
 proof
   assume "0 <= a + a"
-  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute)
+  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1)
   have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
     by (simp add: add_sup_inf_distribs inf_aci)
   hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
@@ -1135,7 +1134,7 @@
   assume assm: "a + a = 0"
   then have "a + a + - a = - a" by simp
   then have "a + (a + - a) = - a" by (simp only: add_assoc)
-  then have a: "- a = a" by simp (*FIXME tune proof*)
+  then have a: "- a = a" by simp
   show "a = 0" apply (rule antisym)
   apply (unfold neg_le_iff_le [symmetric, of a])
   unfolding a apply simp
@@ -1275,7 +1274,7 @@
 proof -
   note add_le_cancel_right [of a a "- a", symmetric, simplified]
   moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
-  then show ?thesis by (auto simp: sup_max)
+  then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2)
 qed
 
 lemma abs_if_lattice:
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Quickcheck.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -3,7 +3,7 @@
 header {* A simple counterexample generator *}
 
 theory Quickcheck
-imports Random Code_Eval
+imports Random Code_Evaluation
 uses ("Tools/quickcheck_generators.ML")
 begin
 
@@ -24,7 +24,7 @@
 
 definition
   "random i = Random.range 2 o\<rightarrow>
-    (\<lambda>k. Pair (if k = 0 then Code_Eval.valtermify False else Code_Eval.valtermify True))"
+    (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
 
 instance ..
 
@@ -34,7 +34,7 @@
 begin
 
 definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
-  "random_itself _ = Pair (Code_Eval.valtermify TYPE('a))"
+  "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
 
 instance ..
 
@@ -44,7 +44,7 @@
 begin
 
 definition
-  "random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Eval.term_of c))"
+  "random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
 
 instance ..
 
@@ -54,7 +54,7 @@
 begin
 
 definition 
-  "random _ = Pair (STR '''', \<lambda>u. Code_Eval.term_of (STR ''''))"
+  "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
 
 instance ..
 
@@ -63,10 +63,10 @@
 instantiation nat :: random
 begin
 
-definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
+definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
   "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
      let n = Code_Numeral.nat_of k
-     in (n, \<lambda>_. Code_Eval.term_of n)))"
+     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
 
 instance ..
 
@@ -78,7 +78,7 @@
 definition
   "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
      let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
-     in (j, \<lambda>_. Code_Eval.term_of j)))"
+     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
 
 instance ..
 
@@ -95,7 +95,7 @@
 
 definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
   \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
-  "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed"
+  "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
 
 instantiation "fun" :: ("{eq, term_of}", random) random
 begin
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Rational.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -1002,8 +1002,8 @@
   by simp
 
 definition (in term_syntax)
-  valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
-  [code_unfold]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+  valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+  [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
 
 notation fcomp (infixl "o>" 60)
 notation scomp (infixl "o\<rightarrow>" 60)
@@ -1014,7 +1014,7 @@
 definition
   "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
      let j = Code_Numeral.int_of (denom + 1)
-     in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
+     in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
 
 instance ..
 
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/RealDef.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -1128,8 +1128,8 @@
   by (simp add: of_rat_divide)
 
 definition (in term_syntax)
-  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
-  [code_unfold]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+  [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
 
 notation fcomp (infixl "o>" 60)
 notation scomp (infixl "o\<rightarrow>" 60)
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Statespace/state_space.ML
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Tools/hologic.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -613,17 +613,17 @@
   | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep",
       Term.itselfT T --> typerepT) $ Logic.mk_type T;
 
-val termT = Type ("Code_Eval.term", []);
+val termT = Type ("Code_Evaluation.term", []);
 
-fun term_of_const T = Const ("Code_Eval.term_of_class.term_of", T --> termT);
+fun term_of_const T = Const ("Code_Evaluation.term_of_class.term_of", T --> termT);
 
 fun mk_term_of T t = term_of_const T $ t;
 
 fun reflect_term (Const (c, T)) =
-      Const ("Code_Eval.Const", literalT --> typerepT --> termT)
+      Const ("Code_Evaluation.Const", literalT --> typerepT --> termT)
         $ mk_literal c $ mk_typerep T
   | reflect_term (t1 $ t2) =
-      Const ("Code_Eval.App", termT --> termT --> termT)
+      Const ("Code_Evaluation.App", termT --> termT --> termT)
         $ reflect_term t1 $ reflect_term t2
   | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
   | reflect_term t = t;
@@ -631,7 +631,7 @@
 fun mk_valtermify_app c vs T =
   let
     fun termifyT T = mk_prodT (T, unitT --> termT);
-    fun valapp T T' = Const ("Code_Eval.valapp",
+    fun valapp T T' = Const ("Code_Evaluation.valapp",
       termifyT (T --> T') --> termifyT T --> termifyT T');
     fun mk_fTs [] _ = []
       | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T;
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Tools/inductive.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -103,7 +103,10 @@
       "(P & True) = P" "(True & P) = P"
     by (fact simp_thms)+};
 
-val simp_thms'' = inf_fun_eq :: inf_bool_eq :: simp_thms';
+val simp_thms'' = map mk_meta_eq [@{thm inf_fun_eq}, @{thm inf_bool_eq}] @ simp_thms';
+
+val simp_thms''' = map mk_meta_eq
+  [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_eq}, @{thm sup_bool_eq}];
 
 
 (** context data **)
@@ -171,15 +174,15 @@
       (case concl of
           (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
         | _ => [thm' RS (thm' RS eq_to_mono2)]);
-    fun dest_less_concl thm = dest_less_concl (thm RS le_funD)
-      handle THM _ => thm RS le_boolD
+    fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
+      handle THM _ => thm RS @{thm le_boolD}
   in
     case concl of
       Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
     | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
     | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
       [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
-         (resolve_tac [le_funI, le_boolI'])) thm))]
+         (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))]
     | _ => [thm]
   end handle THM _ =>
     error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
@@ -323,11 +326,11 @@
     (HOLogic.mk_Trueprop
       (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
     (fn _ => EVERY [rtac @{thm monoI} 1,
-      REPEAT (resolve_tac [le_funI, le_boolI'] 1),
+      REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
       REPEAT (FIRST
         [atac 1,
          resolve_tac (List.concat (map mk_mono monos) @ get_monos ctxt) 1,
-         etac le_funE 1, dtac le_boolD 1])]));
+         etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
 
 
 (* prove introduction rules *)
@@ -338,7 +341,7 @@
 
     val unfold = funpow k (fn th => th RS fun_cong)
       (mono RS (fp_def RS
-        (if coind then def_gfp_unfold else def_lfp_unfold)));
+        (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
 
     fun select_disj 1 1 = []
       | select_disj _ 1 = [rtac disjI1]
@@ -553,13 +556,13 @@
     val ind_concl = HOLogic.mk_Trueprop
       (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
 
-    val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
+    val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
 
     val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl
       (fn {prems, ...} => EVERY
         [rewrite_goals_tac [inductive_conj_def],
          DETERM (rtac raw_fp_induct 1),
-         REPEAT (resolve_tac [le_funI, le_boolI] 1),
+         REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
          rewrite_goals_tac simp_thms'',
          (*This disjE separates out the introduction rules*)
          REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
@@ -577,7 +580,7 @@
         [rewrite_goals_tac rec_preds_defs,
          REPEAT (EVERY
            [REPEAT (resolve_tac [conjI, impI] 1),
-            REPEAT (eresolve_tac [le_funE, le_boolE] 1),
+            REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
             atac 1,
             rewrite_goals_tac simp_thms',
             atac 1])])
@@ -763,8 +766,8 @@
            (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
            (rotate_prems ~1 (ObjectLogic.rulify
              (fold_rule rec_preds_defs
-               (rewrite_rule [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq]
-                (mono RS (fp_def RS def_coinduct))))))
+               (rewrite_rule simp_thms'''
+                (mono RS (fp_def RS @{thm def_coinduct}))))))
        else
          prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
            rec_preds_defs ctxt1);
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -76,7 +76,7 @@
     val lhs = HOLogic.mk_random T size;
     val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))]
       (HOLogic.mk_return Tm @{typ Random.seed}
-      (mk_const "Code_Eval.valapp" [T', T]
+      (mk_const "Code_Evaluation.valapp" [T', T]
         $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
       @{typ Random.seed} (SOME Tm, @{typ Random.seed});
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/UNITY/Simple/Common.thy
--- a/src/HOL/UNITY/Simple/Common.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/UNITY/Simple/Common.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -1,5 +1,4 @@
 (*  Title:      HOL/UNITY/Common
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
@@ -10,7 +9,9 @@
 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
 *)
 
-theory Common imports "../UNITY_Main" begin
+theory Common
+imports "../UNITY_Main"
+begin
 
 consts
   ftime :: "nat=>nat"
@@ -65,7 +66,7 @@
 lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
        \<in> {m} co (maxfg m)"
 apply (simp add: mk_total_program_def) 
-apply (simp add: constrains_def maxfg_def gasc)
+apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
 done
 
 (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
@@ -73,7 +74,7 @@
           (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
        \<in> {m} co (maxfg m)"
 apply (simp add: mk_total_program_def) 
-apply (simp add: constrains_def maxfg_def gasc)
+apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
 done
 
 
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Word/BinBoolList.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -919,7 +919,7 @@
   apply (drule spec)
   apply (erule trans)
   apply (drule_tac x = "bin_cat y n a" in spec)
-  apply (simp add : bin_cat_assoc_sym)
+  apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
   done
 
 lemma bin_rcat_bl:
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Word/BinGeneral.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -508,7 +508,7 @@
 lemma sbintrunc_sbintrunc_min [simp]:
   "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
   apply (rule bin_eqI)
-  apply (auto simp: nth_sbintr)
+  apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2)
   done
 
 lemmas bintrunc_Pls = 
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Word/WordDefinition.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -381,14 +381,14 @@
   apply (unfold word_size)
   apply (subst word_ubin.norm_Rep [symmetric]) 
   apply (simp only: bintrunc_bintrunc_min word_size)
-  apply simp
+  apply (simp add: min_max.inf_absorb2)
   done
 
 lemma wi_bintr': 
   "wb = word_of_int bin ==> n >= size wb ==> 
     word_of_int (bintrunc n bin) = wb"
   unfolding word_size
-  by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric])
+  by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
 
 lemmas bintr_uint = bintr_uint' [unfolded word_size]
 lemmas wi_bintr = wi_bintr' [unfolded word_size]
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/Word/WordShift.thy	Thu Sep 24 11:33:05 2009 +1000
@@ -1017,8 +1017,8 @@
   (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
   word_of_int (bin_cat w (size b) (uint b))"
   apply (unfold word_cat_def word_size) 
-  apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
-      word_ubin.eq_norm bintr_cat)
+  apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
+      word_ubin.eq_norm bintr_cat min_max.inf_absorb1)
   done
 
 lemma word_cat_split_alt:
diff -r f65d74a264dd -r 5fae12e4679c src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/HOL/ex/predicate_compile.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -169,7 +169,7 @@
   end;
 
 fun dest_randomT (Type ("fun", [@{typ Random.seed},
-  Type ("*", [Type ("*", [T, @{typ "unit => Code_Eval.term"}]) ,@{typ Random.seed}])])) = T
+  Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
   | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
 
 (* destruction of intro rules *)
@@ -707,7 +707,7 @@
 end;
 
 (* termify_code:
-val termT = Type ("Code_Eval.term", []);
+val termT = Type ("Code_Evaluation.term", []);
 fun termifyT T = HOLogic.mk_prodT (T, HOLogic.unitT --> termT)
 *)
 (*
@@ -1198,7 +1198,7 @@
       val t1' = mk_valtermify_term t1
       val t2' = mk_valtermify_term t2
     in
-      Const ("Code_Eval.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
+      Const ("Code_Evaluation.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
     end
   | mk_valtermify_term _ = error "Not a valid term for mk_valtermify_term"
 *)
diff -r f65d74a264dd -r 5fae12e4679c src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/Pure/Concurrent/future.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -257,7 +257,7 @@
               "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads")));
 
     val m = if ! do_shutdown then 0 else Multithreading.max_threads_value ();
-    val mm = if m = 9999 then 1 else (m * 3) div 2;
+    val mm = if m = 9999 then 1 else m * 2;
     val l = length (! workers);
     val _ = excessive := l - mm;
     val _ =
diff -r f65d74a264dd -r 5fae12e4679c src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/Pure/Isar/code.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -505,9 +505,10 @@
 
 (*those following are permissive wrt. to overloaded constants!*)
 
+val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
 fun const_typ_eqn thy thm =
   let
-    val (c, ty) = (dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
+    val (c, ty) = head_eqn thm;
     val c' = AxClass.unoverload_const thy (c, ty);
   in (c', ty) end;
 
@@ -523,8 +524,8 @@
 
 fun same_typscheme thy thms =
   let
-    fun tvars_of t = rev (Term.add_tvars t []);
-    val vss = map (tvars_of o Thm.prop_of) thms;
+    fun tvars_of T = rev (Term.add_tvarsT T []);
+    val vss = map (tvars_of o snd o head_eqn) thms;
     fun inter_sorts vs =
       fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
     val sorts = map_transpose inter_sorts vss;
@@ -547,7 +548,7 @@
 fun case_certificate thm =
   let
     val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
-      o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.prop_of) thm;
+      o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm;
     val _ = case head of Free _ => true
       | Var _ => true
       | _ => raise TERM ("case_cert", []);
diff -r f65d74a264dd -r 5fae12e4679c src/Pure/envir.ML
--- a/src/Pure/envir.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/Pure/envir.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -282,12 +282,9 @@
   let
     val funerr = "fastype: expected function type";
     fun fast Ts (f $ u) =
-          (case fast Ts f of
+          (case Type.devar tyenv (fast Ts f) of
             Type ("fun", [_, T]) => T
-          | TVar v =>
-              (case Type.lookup tyenv v of
-                SOME (Type ("fun", [_, T])) => T
-              | _ => raise TERM (funerr, [f $ u]))
+          | TVar v => raise TERM (funerr, [f $ u])
           | _ => raise TERM (funerr, [f $ u]))
       | fast Ts (Const (_, T)) = T
       | fast Ts (Free (_, T)) = T
diff -r f65d74a264dd -r 5fae12e4679c src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Sep 23 19:17:48 2009 +1000
+++ b/src/Pure/type.ML	Thu Sep 24 11:33:05 2009 +1000
@@ -55,6 +55,7 @@
   exception TYPE_MATCH
   type tyenv = (sort * typ) Vartab.table
   val lookup: tyenv -> indexname * sort -> typ option
+  val devar: tyenv -> typ -> typ
   val typ_match: tsig -> typ * typ -> tyenv -> tyenv
   val typ_instance: tsig -> typ * typ -> bool
   val raw_match: typ * typ -> tyenv -> tyenv