Merge with changes from isabelle dev repository.
authorThomas Sewell <tsewell@nicta.com.au>
Thu Sep 24 11:33:05 2009 +1000 (2009-09-24)
changeset 327535fae12e4679c
parent 32752 f65d74a264dd
parent 32658 82956a3f0e0b
child 32754 4e0256f7d219
Merge with changes from isabelle dev repository.
src/HOL/Code_Eval.thy
     1.1 --- a/Admin/isatest/isatest-makedist	Wed Sep 23 19:17:48 2009 +1000
     1.2 +++ b/Admin/isatest/isatest-makedist	Thu Sep 24 11:33:05 2009 +1000
     1.3 @@ -102,9 +102,9 @@
     1.4  #sleep 15
     1.5  $SSH macbroy21 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
     1.6  sleep 15
     1.7 -$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e"
     1.8 -sleep 15
     1.9 -$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly"
    1.10 +#$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e"
    1.11 +#sleep 15
    1.12 +$SSH atbroy99 "$MAKEALL $HOME/settings/at64-poly"
    1.13  sleep 15
    1.14  $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"
    1.15  sleep 15
     2.1 --- a/NEWS	Wed Sep 23 19:17:48 2009 +1000
     2.2 +++ b/NEWS	Thu Sep 24 11:33:05 2009 +1000
     2.3 @@ -102,6 +102,10 @@
     2.4  
     2.5    INCOMPATIBILITY.
     2.6  
     2.7 +* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no
     2.8 +simp rules by default any longer.  The same applies to
     2.9 +min_max.inf_absorb1 etc.!  INCOMPATIBILITY.
    2.10 +
    2.11  * Power operations on relations and functions are now one dedicate
    2.12  constant "compow" with infix syntax "^^".  Power operations on
    2.13  multiplicative monoids retains syntax "^" and is now defined generic
     3.1 --- a/lib/Tools/usedir	Wed Sep 23 19:17:48 2009 +1000
     3.2 +++ b/lib/Tools/usedir	Thu Sep 24 11:33:05 2009 +1000
     3.3 @@ -262,7 +262,7 @@
     3.4  else
     3.5    { echo "$ITEM FAILED";
     3.6      echo "(see also $LOG)";
     3.7 -    echo; tail "$LOG"; echo; } >&2
     3.8 +    echo; tail -n 20 "$LOG"; echo; } >&2
     3.9  fi
    3.10  
    3.11  exit "$RC"
     4.1 --- a/src/HOL/Code_Eval.thy	Wed Sep 23 19:17:48 2009 +1000
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,271 +0,0 @@
     4.4 -(*  Title:      HOL/Code_Eval.thy
     4.5 -    Author:     Florian Haftmann, TU Muenchen
     4.6 -*)
     4.7 -
     4.8 -header {* Term evaluation using the generic code generator *}
     4.9 -
    4.10 -theory Code_Eval
    4.11 -imports Plain Typerep Code_Numeral
    4.12 -begin
    4.13 -
    4.14 -subsection {* Term representation *}
    4.15 -
    4.16 -subsubsection {* Terms and class @{text term_of} *}
    4.17 -
    4.18 -datatype "term" = dummy_term
    4.19 -
    4.20 -definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
    4.21 -  "Const _ _ = dummy_term"
    4.22 -
    4.23 -definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
    4.24 -  "App _ _ = dummy_term"
    4.25 -
    4.26 -code_datatype Const App
    4.27 -
    4.28 -class term_of = typerep +
    4.29 -  fixes term_of :: "'a \<Rightarrow> term"
    4.30 -
    4.31 -lemma term_of_anything: "term_of x \<equiv> t"
    4.32 -  by (rule eq_reflection) (cases "term_of x", cases t, simp)
    4.33 -
    4.34 -definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
    4.35 -  \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
    4.36 -  "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
    4.37 -
    4.38 -lemma valapp_code [code, code_unfold]:
    4.39 -  "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
    4.40 -  by (simp only: valapp_def fst_conv snd_conv)
    4.41 -
    4.42 -
    4.43 -subsubsection {* @{text term_of} instances *}
    4.44 -
    4.45 -instantiation "fun" :: (typerep, typerep) term_of
    4.46 -begin
    4.47 -
    4.48 -definition
    4.49 -  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
    4.50 -     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
    4.51 -
    4.52 -instance ..
    4.53 -
    4.54 -end
    4.55 -
    4.56 -setup {*
    4.57 -let
    4.58 -  fun add_term_of tyco raw_vs thy =
    4.59 -    let
    4.60 -      val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    4.61 -      val ty = Type (tyco, map TFree vs);
    4.62 -      val lhs = Const (@{const_name term_of}, ty --> @{typ term})
    4.63 -        $ Free ("x", ty);
    4.64 -      val rhs = @{term "undefined \<Colon> term"};
    4.65 -      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    4.66 -      fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    4.67 -        o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    4.68 -    in
    4.69 -      thy
    4.70 -      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
    4.71 -      |> `(fn lthy => Syntax.check_term lthy eq)
    4.72 -      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    4.73 -      |> snd
    4.74 -      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    4.75 -    end;
    4.76 -  fun ensure_term_of (tyco, (raw_vs, _)) thy =
    4.77 -    let
    4.78 -      val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
    4.79 -        andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    4.80 -    in if need_inst then add_term_of tyco raw_vs thy else thy end;
    4.81 -in
    4.82 -  Code.type_interpretation ensure_term_of
    4.83 -end
    4.84 -*}
    4.85 -
    4.86 -setup {*
    4.87 -let
    4.88 -  fun mk_term_of_eq thy ty vs tyco (c, tys) =
    4.89 -    let
    4.90 -      val t = list_comb (Const (c, tys ---> ty),
    4.91 -        map Free (Name.names Name.context "a" tys));
    4.92 -      val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
    4.93 -        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    4.94 -      val cty = Thm.ctyp_of thy ty;
    4.95 -    in
    4.96 -      @{thm term_of_anything}
    4.97 -      |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    4.98 -      |> Thm.varifyT
    4.99 -    end;
   4.100 -  fun add_term_of_code tyco raw_vs raw_cs thy =
   4.101 -    let
   4.102 -      val algebra = Sign.classes_of thy;
   4.103 -      val vs = map (fn (v, sort) =>
   4.104 -        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
   4.105 -      val ty = Type (tyco, map TFree vs);
   4.106 -      val cs = (map o apsnd o map o map_atyps)
   4.107 -        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
   4.108 -      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   4.109 -      val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
   4.110 -   in
   4.111 -      thy
   4.112 -      |> Code.del_eqns const
   4.113 -      |> fold Code.add_eqn eqs
   4.114 -    end;
   4.115 -  fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
   4.116 -    let
   4.117 -      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
   4.118 -    in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
   4.119 -in
   4.120 -  Code.type_interpretation ensure_term_of_code
   4.121 -end
   4.122 -*}
   4.123 -
   4.124 -
   4.125 -subsubsection {* Code generator setup *}
   4.126 -
   4.127 -lemmas [code del] = term.recs term.cases term.size
   4.128 -lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
   4.129 -
   4.130 -lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
   4.131 -lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
   4.132 -lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
   4.133 -lemma [code, code del]:
   4.134 -  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
   4.135 -lemma [code, code del]:
   4.136 -  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
   4.137 -
   4.138 -lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
   4.139 -    (let (n, m) = nibble_pair_of_char c
   4.140 -  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   4.141 -    (Code_Eval.term_of n)) (Code_Eval.term_of m))"
   4.142 -  by (subst term_of_anything) rule 
   4.143 -
   4.144 -code_type "term"
   4.145 -  (Eval "Term.term")
   4.146 -
   4.147 -code_const Const and App
   4.148 -  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
   4.149 -
   4.150 -code_const "term_of \<Colon> String.literal \<Rightarrow> term"
   4.151 -  (Eval "HOLogic.mk'_message'_string")
   4.152 -
   4.153 -code_reserved Eval HOLogic
   4.154 -
   4.155 -
   4.156 -subsubsection {* Syntax *}
   4.157 -
   4.158 -definition termify :: "'a \<Rightarrow> term" where
   4.159 -  [code del]: "termify x = dummy_term"
   4.160 -
   4.161 -abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
   4.162 -  "valtermify x \<equiv> (x, \<lambda>u. termify x)"
   4.163 -
   4.164 -setup {*
   4.165 -let
   4.166 -  fun map_default f xs =
   4.167 -    let val ys = map f xs
   4.168 -    in if exists is_some ys
   4.169 -      then SOME (map2 the_default xs ys)
   4.170 -      else NONE
   4.171 -    end;
   4.172 -  fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
   4.173 -        if not (Term.has_abs t)
   4.174 -        then if fold_aterms (fn Const _ => I | _ => K false) t true
   4.175 -          then SOME (HOLogic.reflect_term t)
   4.176 -          else error "Cannot termify expression containing variables"
   4.177 -        else error "Cannot termify expression containing abstraction"
   4.178 -    | subst_termify_app (t, ts) = case map_default subst_termify ts
   4.179 -       of SOME ts' => SOME (list_comb (t, ts'))
   4.180 -        | NONE => NONE
   4.181 -  and subst_termify (Abs (v, T, t)) = (case subst_termify t
   4.182 -       of SOME t' => SOME (Abs (v, T, t'))
   4.183 -        | NONE => NONE)
   4.184 -    | subst_termify t = subst_termify_app (strip_comb t) 
   4.185 -  fun check_termify ts ctxt = map_default subst_termify ts
   4.186 -    |> Option.map (rpair ctxt)
   4.187 -in
   4.188 -  Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
   4.189 -end;
   4.190 -*}
   4.191 -
   4.192 -locale term_syntax
   4.193 -begin
   4.194 -
   4.195 -notation App (infixl "<\<cdot>>" 70)
   4.196 -  and valapp (infixl "{\<cdot>}" 70)
   4.197 -
   4.198 -end
   4.199 -
   4.200 -interpretation term_syntax .
   4.201 -
   4.202 -no_notation App (infixl "<\<cdot>>" 70)
   4.203 -  and valapp (infixl "{\<cdot>}" 70)
   4.204 -
   4.205 -
   4.206 -subsection {* Numeric types *}
   4.207 -
   4.208 -definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
   4.209 -  "term_of_num two = (\<lambda>_. dummy_term)"
   4.210 -
   4.211 -lemma (in term_syntax) term_of_num_code [code]:
   4.212 -  "term_of_num two k = (if k = 0 then termify Int.Pls
   4.213 -    else (if k mod two = 0
   4.214 -      then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
   4.215 -      else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
   4.216 -  by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
   4.217 -
   4.218 -lemma (in term_syntax) term_of_nat_code [code]:
   4.219 -  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
   4.220 -  by (simp only: term_of_anything)
   4.221 -
   4.222 -lemma (in term_syntax) term_of_int_code [code]:
   4.223 -  "term_of (k::int) = (if k = 0 then termify (0 :: int)
   4.224 -    else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
   4.225 -      else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
   4.226 -  by (simp only: term_of_anything)
   4.227 -
   4.228 -lemma (in term_syntax) term_of_code_numeral_code [code]:
   4.229 -  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
   4.230 -  by (simp only: term_of_anything)
   4.231 -
   4.232 -subsection {* Obfuscate *}
   4.233 -
   4.234 -print_translation {*
   4.235 -let
   4.236 -  val term = Const ("<TERM>", dummyT);
   4.237 -  fun tr1' [_, _] = term;
   4.238 -  fun tr2' [] = term;
   4.239 -in
   4.240 -  [(@{const_syntax Const}, tr1'),
   4.241 -    (@{const_syntax App}, tr1'),
   4.242 -    (@{const_syntax dummy_term}, tr2')]
   4.243 -end
   4.244 -*}
   4.245 -
   4.246 -hide const dummy_term App valapp
   4.247 -hide (open) const Const termify valtermify term_of term_of_num
   4.248 -
   4.249 -
   4.250 -subsection {* Evaluation setup *}
   4.251 -
   4.252 -ML {*
   4.253 -signature EVAL =
   4.254 -sig
   4.255 -  val eval_ref: (unit -> term) option ref
   4.256 -  val eval_term: theory -> term -> term
   4.257 -end;
   4.258 -
   4.259 -structure Eval : EVAL =
   4.260 -struct
   4.261 -
   4.262 -val eval_ref = ref (NONE : (unit -> term) option);
   4.263 -
   4.264 -fun eval_term thy t =
   4.265 -  Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
   4.266 -
   4.267 -end;
   4.268 -*}
   4.269 -
   4.270 -setup {*
   4.271 -  Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
   4.272 -*}
   4.273 -
   4.274 -end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Code_Evaluation.thy	Thu Sep 24 11:33:05 2009 +1000
     5.3 @@ -0,0 +1,271 @@
     5.4 +(*  Title:      HOL/Code_Evaluation.thy
     5.5 +    Author:     Florian Haftmann, TU Muenchen
     5.6 +*)
     5.7 +
     5.8 +header {* Term evaluation using the generic code generator *}
     5.9 +
    5.10 +theory Code_Evaluation
    5.11 +imports Plain Typerep Code_Numeral
    5.12 +begin
    5.13 +
    5.14 +subsection {* Term representation *}
    5.15 +
    5.16 +subsubsection {* Terms and class @{text term_of} *}
    5.17 +
    5.18 +datatype "term" = dummy_term
    5.19 +
    5.20 +definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
    5.21 +  "Const _ _ = dummy_term"
    5.22 +
    5.23 +definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
    5.24 +  "App _ _ = dummy_term"
    5.25 +
    5.26 +code_datatype Const App
    5.27 +
    5.28 +class term_of = typerep +
    5.29 +  fixes term_of :: "'a \<Rightarrow> term"
    5.30 +
    5.31 +lemma term_of_anything: "term_of x \<equiv> t"
    5.32 +  by (rule eq_reflection) (cases "term_of x", cases t, simp)
    5.33 +
    5.34 +definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
    5.35 +  \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
    5.36 +  "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
    5.37 +
    5.38 +lemma valapp_code [code, code_unfold]:
    5.39 +  "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
    5.40 +  by (simp only: valapp_def fst_conv snd_conv)
    5.41 +
    5.42 +
    5.43 +subsubsection {* @{text term_of} instances *}
    5.44 +
    5.45 +instantiation "fun" :: (typerep, typerep) term_of
    5.46 +begin
    5.47 +
    5.48 +definition
    5.49 +  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
    5.50 +     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
    5.51 +
    5.52 +instance ..
    5.53 +
    5.54 +end
    5.55 +
    5.56 +setup {*
    5.57 +let
    5.58 +  fun add_term_of tyco raw_vs thy =
    5.59 +    let
    5.60 +      val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    5.61 +      val ty = Type (tyco, map TFree vs);
    5.62 +      val lhs = Const (@{const_name term_of}, ty --> @{typ term})
    5.63 +        $ Free ("x", ty);
    5.64 +      val rhs = @{term "undefined \<Colon> term"};
    5.65 +      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    5.66 +      fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    5.67 +        o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    5.68 +    in
    5.69 +      thy
    5.70 +      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
    5.71 +      |> `(fn lthy => Syntax.check_term lthy eq)
    5.72 +      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    5.73 +      |> snd
    5.74 +      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    5.75 +    end;
    5.76 +  fun ensure_term_of (tyco, (raw_vs, _)) thy =
    5.77 +    let
    5.78 +      val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
    5.79 +        andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    5.80 +    in if need_inst then add_term_of tyco raw_vs thy else thy end;
    5.81 +in
    5.82 +  Code.type_interpretation ensure_term_of
    5.83 +end
    5.84 +*}
    5.85 +
    5.86 +setup {*
    5.87 +let
    5.88 +  fun mk_term_of_eq thy ty vs tyco (c, tys) =
    5.89 +    let
    5.90 +      val t = list_comb (Const (c, tys ---> ty),
    5.91 +        map Free (Name.names Name.context "a" tys));
    5.92 +      val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
    5.93 +        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    5.94 +      val cty = Thm.ctyp_of thy ty;
    5.95 +    in
    5.96 +      @{thm term_of_anything}
    5.97 +      |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    5.98 +      |> Thm.varifyT
    5.99 +    end;
   5.100 +  fun add_term_of_code tyco raw_vs raw_cs thy =
   5.101 +    let
   5.102 +      val algebra = Sign.classes_of thy;
   5.103 +      val vs = map (fn (v, sort) =>
   5.104 +        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
   5.105 +      val ty = Type (tyco, map TFree vs);
   5.106 +      val cs = (map o apsnd o map o map_atyps)
   5.107 +        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
   5.108 +      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   5.109 +      val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
   5.110 +   in
   5.111 +      thy
   5.112 +      |> Code.del_eqns const
   5.113 +      |> fold Code.add_eqn eqs
   5.114 +    end;
   5.115 +  fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
   5.116 +    let
   5.117 +      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
   5.118 +    in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
   5.119 +in
   5.120 +  Code.type_interpretation ensure_term_of_code
   5.121 +end
   5.122 +*}
   5.123 +
   5.124 +
   5.125 +subsubsection {* Code generator setup *}
   5.126 +
   5.127 +lemmas [code del] = term.recs term.cases term.size
   5.128 +lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
   5.129 +
   5.130 +lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
   5.131 +lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
   5.132 +lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
   5.133 +lemma [code, code del]:
   5.134 +  "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
   5.135 +lemma [code, code del]:
   5.136 +  "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
   5.137 +
   5.138 +lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Evaluation.term_of c =
   5.139 +    (let (n, m) = nibble_pair_of_char c
   5.140 +  in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   5.141 +    (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
   5.142 +  by (subst term_of_anything) rule 
   5.143 +
   5.144 +code_type "term"
   5.145 +  (Eval "Term.term")
   5.146 +
   5.147 +code_const Const and App
   5.148 +  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
   5.149 +
   5.150 +code_const "term_of \<Colon> String.literal \<Rightarrow> term"
   5.151 +  (Eval "HOLogic.mk'_message'_string")
   5.152 +
   5.153 +code_reserved Eval HOLogic
   5.154 +
   5.155 +
   5.156 +subsubsection {* Syntax *}
   5.157 +
   5.158 +definition termify :: "'a \<Rightarrow> term" where
   5.159 +  [code del]: "termify x = dummy_term"
   5.160 +
   5.161 +abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
   5.162 +  "valtermify x \<equiv> (x, \<lambda>u. termify x)"
   5.163 +
   5.164 +setup {*
   5.165 +let
   5.166 +  fun map_default f xs =
   5.167 +    let val ys = map f xs
   5.168 +    in if exists is_some ys
   5.169 +      then SOME (map2 the_default xs ys)
   5.170 +      else NONE
   5.171 +    end;
   5.172 +  fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
   5.173 +        if not (Term.has_abs t)
   5.174 +        then if fold_aterms (fn Const _ => I | _ => K false) t true
   5.175 +          then SOME (HOLogic.reflect_term t)
   5.176 +          else error "Cannot termify expression containing variables"
   5.177 +        else error "Cannot termify expression containing abstraction"
   5.178 +    | subst_termify_app (t, ts) = case map_default subst_termify ts
   5.179 +       of SOME ts' => SOME (list_comb (t, ts'))
   5.180 +        | NONE => NONE
   5.181 +  and subst_termify (Abs (v, T, t)) = (case subst_termify t
   5.182 +       of SOME t' => SOME (Abs (v, T, t'))
   5.183 +        | NONE => NONE)
   5.184 +    | subst_termify t = subst_termify_app (strip_comb t) 
   5.185 +  fun check_termify ts ctxt = map_default subst_termify ts
   5.186 +    |> Option.map (rpair ctxt)
   5.187 +in
   5.188 +  Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
   5.189 +end;
   5.190 +*}
   5.191 +
   5.192 +locale term_syntax
   5.193 +begin
   5.194 +
   5.195 +notation App (infixl "<\<cdot>>" 70)
   5.196 +  and valapp (infixl "{\<cdot>}" 70)
   5.197 +
   5.198 +end
   5.199 +
   5.200 +interpretation term_syntax .
   5.201 +
   5.202 +no_notation App (infixl "<\<cdot>>" 70)
   5.203 +  and valapp (infixl "{\<cdot>}" 70)
   5.204 +
   5.205 +
   5.206 +subsection {* Numeric types *}
   5.207 +
   5.208 +definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
   5.209 +  "term_of_num two = (\<lambda>_. dummy_term)"
   5.210 +
   5.211 +lemma (in term_syntax) term_of_num_code [code]:
   5.212 +  "term_of_num two k = (if k = 0 then termify Int.Pls
   5.213 +    else (if k mod two = 0
   5.214 +      then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
   5.215 +      else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
   5.216 +  by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
   5.217 +
   5.218 +lemma (in term_syntax) term_of_nat_code [code]:
   5.219 +  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
   5.220 +  by (simp only: term_of_anything)
   5.221 +
   5.222 +lemma (in term_syntax) term_of_int_code [code]:
   5.223 +  "term_of (k::int) = (if k = 0 then termify (0 :: int)
   5.224 +    else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
   5.225 +      else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
   5.226 +  by (simp only: term_of_anything)
   5.227 +
   5.228 +lemma (in term_syntax) term_of_code_numeral_code [code]:
   5.229 +  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
   5.230 +  by (simp only: term_of_anything)
   5.231 +
   5.232 +subsection {* Obfuscate *}
   5.233 +
   5.234 +print_translation {*
   5.235 +let
   5.236 +  val term = Const ("<TERM>", dummyT);
   5.237 +  fun tr1' [_, _] = term;
   5.238 +  fun tr2' [] = term;
   5.239 +in
   5.240 +  [(@{const_syntax Const}, tr1'),
   5.241 +    (@{const_syntax App}, tr1'),
   5.242 +    (@{const_syntax dummy_term}, tr2')]
   5.243 +end
   5.244 +*}
   5.245 +
   5.246 +hide const dummy_term App valapp
   5.247 +hide (open) const Const termify valtermify term_of term_of_num
   5.248 +
   5.249 +
   5.250 +subsection {* Evaluation setup *}
   5.251 +
   5.252 +ML {*
   5.253 +signature EVAL =
   5.254 +sig
   5.255 +  val eval_ref: (unit -> term) option ref
   5.256 +  val eval_term: theory -> term -> term
   5.257 +end;
   5.258 +
   5.259 +structure Eval : EVAL =
   5.260 +struct
   5.261 +
   5.262 +val eval_ref = ref (NONE : (unit -> term) option);
   5.263 +
   5.264 +fun eval_term thy t =
   5.265 +  Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
   5.266 +
   5.267 +end;
   5.268 +*}
   5.269 +
   5.270 +setup {*
   5.271 +  Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
   5.272 +*}
   5.273 +
   5.274 +end
     6.1 --- a/src/HOL/Complete_Lattice.thy	Wed Sep 23 19:17:48 2009 +1000
     6.2 +++ b/src/HOL/Complete_Lattice.thy	Thu Sep 24 11:33:05 2009 +1000
     6.3 @@ -76,11 +76,11 @@
     6.4  
     6.5  lemma sup_bot [simp]:
     6.6    "x \<squnion> bot = x"
     6.7 -  using bot_least [of x] by (simp add: sup_commute)
     6.8 +  using bot_least [of x] by (simp add: sup_commute sup_absorb2)
     6.9  
    6.10  lemma inf_top [simp]:
    6.11    "x \<sqinter> top = x"
    6.12 -  using top_greatest [of x] by (simp add: inf_commute)
    6.13 +  using top_greatest [of x] by (simp add: inf_commute inf_absorb2)
    6.14  
    6.15  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    6.16    "SUPR A f = \<Squnion> (f ` A)"
     7.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 23 19:17:48 2009 +1000
     7.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Sep 24 11:33:05 2009 +1000
     7.3 @@ -1904,7 +1904,7 @@
     7.4  	show "0 < real x * 2/3" using * by auto
     7.5  	show "real ?max + 1 \<le> real x * 2/3" using * up
     7.6  	  by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
     7.7 -	      auto simp add: real_of_float_max)
     7.8 +	      auto simp add: real_of_float_max min_max.sup_absorb1)
     7.9        qed
    7.10        finally have "real (?lb_horner (Float 1 -1)) + real (?lb_horner ?max)
    7.11  	\<le> ln (real x)"
    7.12 @@ -3246,12 +3246,13 @@
    7.13          = map (` (variable_of_bound o prop_of)) prems
    7.14  
    7.15        fun add_deps (name, bnds)
    7.16 -        = Graph.add_deps_acyclic
    7.17 -            (name, remove (op =) name (Term.add_free_names (prop_of bnds) []))
    7.18 +        = Graph.add_deps_acyclic (name,
    7.19 +            remove (op =) name (Term.add_free_names (prop_of bnds) []))
    7.20 +
    7.21        val order = Graph.empty
    7.22                    |> fold Graph.new_node variable_bounds
    7.23                    |> fold add_deps variable_bounds
    7.24 -                  |> Graph.topological_order |> rev
    7.25 +                  |> Graph.strong_conn |> map the_single |> rev
    7.26                    |> map_filter (AList.lookup (op =) variable_bounds)
    7.27  
    7.28        fun prepend_prem th tac
    7.29 @@ -3338,7 +3339,7 @@
    7.30                        etac @{thm meta_eqE},
    7.31                        rtac @{thm impI}] i)
    7.32        THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
    7.33 -      THEN TRY (filter_prems_tac (K false) i)
    7.34 +      THEN DETERM (TRY (filter_prems_tac (K false) i))
    7.35        THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
    7.36        THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
    7.37        THEN gen_eval_tac eval_oracle ctxt i))
    7.38 @@ -3350,7 +3351,7 @@
    7.39  
    7.40    fun mk_approx' prec t = (@{const "approx'"}
    7.41                           $ HOLogic.mk_number @{typ nat} prec
    7.42 -                         $ t $ @{term "[] :: (float * float) list"})
    7.43 +                         $ t $ @{term "[] :: (float * float) option list"})
    7.44  
    7.45    fun dest_result (Const (@{const_name "Some"}, _) $
    7.46                     ((Const (@{const_name "Pair"}, _)) $
     8.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Sep 23 19:17:48 2009 +1000
     8.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Sep 24 11:33:05 2009 +1000
     8.3 @@ -512,7 +512,7 @@
     8.4    assumes g0: "numgcd t = 0"
     8.5    shows "Inum bs t = 0"
     8.6    using g0[simplified numgcd_def] 
     8.7 -  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos)
     8.8 +  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos min_max.sup_absorb2)
     8.9  
    8.10  lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
    8.11    using gp
     9.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Sep 23 19:17:48 2009 +1000
     9.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Thu Sep 24 11:33:05 2009 +1000
     9.3 @@ -72,7 +72,9 @@
     9.4    shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
     9.5    using assms by (approximation 80)
     9.6  
     9.7 -lemma "\<phi> \<in> { 0 .. 1 :: real } \<longrightarrow> \<phi> ^ 2 \<le> \<phi>"
     9.8 -  by (approximation 30 splitting: \<phi>=1 taylor: \<phi> = 3)
     9.9 +lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x ^ 2 \<le> x"
    9.10 +  by (approximation 30 splitting: x=1 taylor: x = 3)
    9.11 +
    9.12 +value [approximate] "10"
    9.13  
    9.14  end
    10.1 --- a/src/HOL/Finite_Set.thy	Wed Sep 23 19:17:48 2009 +1000
    10.2 +++ b/src/HOL/Finite_Set.thy	Thu Sep 24 11:33:05 2009 +1000
    10.3 @@ -2966,11 +2966,11 @@
    10.4  
    10.5  lemma dual_max:
    10.6    "ord.max (op \<ge>) = min"
    10.7 -  by (auto simp add: ord.max_def_raw expand_fun_eq)
    10.8 +  by (auto simp add: ord.max_def_raw min_def expand_fun_eq)
    10.9  
   10.10  lemma dual_min:
   10.11    "ord.min (op \<ge>) = max"
   10.12 -  by (auto simp add: ord.min_def_raw expand_fun_eq)
   10.13 +  by (auto simp add: ord.min_def_raw max_def expand_fun_eq)
   10.14  
   10.15  lemma strict_below_fold1_iff:
   10.16    assumes "finite A" and "A \<noteq> {}"
    11.1 --- a/src/HOL/Hoare_Parallel/Graph.thy	Wed Sep 23 19:17:48 2009 +1000
    11.2 +++ b/src/HOL/Hoare_Parallel/Graph.thy	Thu Sep 24 11:33:05 2009 +1000
    11.3 @@ -187,6 +187,8 @@
    11.4  
    11.5  subsubsection{* Graph 3 *}
    11.6  
    11.7 +declare min_max.inf_absorb1 [simp] min_max.inf_absorb2 [simp]
    11.8 +
    11.9  lemma Graph3: 
   11.10    "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
   11.11  apply (unfold Reach_def)
   11.12 @@ -307,6 +309,8 @@
   11.13  apply force
   11.14  done
   11.15  
   11.16 +declare min_max.inf_absorb1 [simp del] min_max.inf_absorb2 [simp del]
   11.17 +
   11.18  subsubsection {* Graph 5 *}
   11.19  
   11.20  lemma Graph5: 
    12.1 --- a/src/HOL/Induct/LList.thy	Wed Sep 23 19:17:48 2009 +1000
    12.2 +++ b/src/HOL/Induct/LList.thy	Thu Sep 24 11:33:05 2009 +1000
    12.3 @@ -665,7 +665,7 @@
    12.4  apply (subst LList_corec, force)
    12.5  done
    12.6  
    12.7 -lemma llist_corec: 
    12.8 +lemma llist_corec [nitpick_const_simp]: 
    12.9      "llist_corec a f =   
   12.10       (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))"
   12.11  apply (unfold llist_corec_def LNil_def LCons_def)
   12.12 @@ -774,10 +774,11 @@
   12.13  
   12.14  subsection{* The functional @{text lmap} *}
   12.15  
   12.16 -lemma lmap_LNil [simp]: "lmap f LNil = LNil"
   12.17 +lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
   12.18  by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
   12.19  
   12.20 -lemma lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
   12.21 +lemma lmap_LCons [simp, nitpick_const_simp]:
   12.22 +"lmap f (LCons M N) = LCons (f M) (lmap f N)"
   12.23  by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
   12.24  
   12.25  
   12.26 @@ -792,7 +793,7 @@
   12.27  
   12.28  subsection{* iterates -- @{text llist_fun_equalityI} cannot be used! *}
   12.29  
   12.30 -lemma iterates: "iterates f x = LCons x (iterates f (f x))"
   12.31 +lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
   12.32  by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
   12.33  
   12.34  lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)"
   12.35 @@ -847,18 +848,18 @@
   12.36  
   12.37  subsection{* @{text lappend} -- its two arguments cause some complications! *}
   12.38  
   12.39 -lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
   12.40 +lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
   12.41  apply (simp add: lappend_def)
   12.42  apply (rule llist_corec [THEN trans], simp)
   12.43  done
   12.44  
   12.45 -lemma lappend_LNil_LCons [simp]: 
   12.46 +lemma lappend_LNil_LCons [simp, nitpick_const_simp]: 
   12.47      "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
   12.48  apply (simp add: lappend_def)
   12.49  apply (rule llist_corec [THEN trans], simp)
   12.50  done
   12.51  
   12.52 -lemma lappend_LCons [simp]: 
   12.53 +lemma lappend_LCons [simp, nitpick_const_simp]: 
   12.54      "lappend (LCons l l') N = LCons l (lappend l' N)"
   12.55  apply (simp add: lappend_def)
   12.56  apply (rule llist_corec [THEN trans], simp)
    13.1 --- a/src/HOL/Inductive.thy	Wed Sep 23 19:17:48 2009 +1000
    13.2 +++ b/src/HOL/Inductive.thy	Thu Sep 24 11:33:05 2009 +1000
    13.3 @@ -267,26 +267,6 @@
    13.4    Ball_def Bex_def
    13.5    induct_rulify_fallback
    13.6  
    13.7 -ML {*
    13.8 -val def_lfp_unfold = @{thm def_lfp_unfold}
    13.9 -val def_gfp_unfold = @{thm def_gfp_unfold}
   13.10 -val def_lfp_induct = @{thm def_lfp_induct}
   13.11 -val def_coinduct = @{thm def_coinduct}
   13.12 -val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection}
   13.13 -val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection}
   13.14 -val sup_bool_eq = @{thm sup_bool_eq} RS @{thm eq_reflection}
   13.15 -val sup_fun_eq = @{thm sup_fun_eq} RS @{thm eq_reflection}
   13.16 -val le_boolI = @{thm le_boolI}
   13.17 -val le_boolI' = @{thm le_boolI'}
   13.18 -val le_funI = @{thm le_funI}
   13.19 -val le_boolE = @{thm le_boolE}
   13.20 -val le_funE = @{thm le_funE}
   13.21 -val le_boolD = @{thm le_boolD}
   13.22 -val le_funD = @{thm le_funD}
   13.23 -val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection}
   13.24 -val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection}
   13.25 -*}
   13.26 -
   13.27  use "Tools/inductive.ML"
   13.28  setup Inductive.setup
   13.29  
    14.1 --- a/src/HOL/IsaMakefile	Wed Sep 23 19:17:48 2009 +1000
    14.2 +++ b/src/HOL/IsaMakefile	Thu Sep 24 11:33:05 2009 +1000
    14.3 @@ -210,7 +210,7 @@
    14.4  
    14.5  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
    14.6    ATP_Linkup.thy \
    14.7 -  Code_Eval.thy \
    14.8 +  Code_Evaluation.thy \
    14.9    Code_Numeral.thy \
   14.10    Equiv_Relations.thy \
   14.11    Groebner_Basis.thy \
    15.1 --- a/src/HOL/Lattices.thy	Wed Sep 23 19:17:48 2009 +1000
    15.2 +++ b/src/HOL/Lattices.thy	Thu Sep 24 11:33:05 2009 +1000
    15.3 @@ -127,10 +127,10 @@
    15.4  lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    15.5    by (rule antisym) (auto intro: le_infI2)
    15.6  
    15.7 -lemma inf_absorb1[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
    15.8 +lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
    15.9    by (rule antisym) auto
   15.10  
   15.11 -lemma inf_absorb2[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   15.12 +lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   15.13    by (rule antisym) auto
   15.14  
   15.15  lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   15.16 @@ -155,10 +155,10 @@
   15.17  lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   15.18    by (rule antisym) (auto intro: le_supI2)
   15.19  
   15.20 -lemma sup_absorb1[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   15.21 +lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   15.22    by (rule antisym) auto
   15.23  
   15.24 -lemma sup_absorb2[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   15.25 +lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   15.26    by (rule antisym) auto
   15.27  
   15.28  lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   15.29 @@ -229,11 +229,11 @@
   15.30  
   15.31  lemma less_infI1:
   15.32    "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   15.33 -  by (auto simp add: less_le intro: le_infI1)
   15.34 +  by (auto simp add: less_le inf_absorb1 intro: le_infI1)
   15.35  
   15.36  lemma less_infI2:
   15.37    "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   15.38 -  by (auto simp add: less_le intro: le_infI2)
   15.39 +  by (auto simp add: less_le inf_absorb2 intro: le_infI2)
   15.40  
   15.41  end
   15.42  
    16.1 --- a/src/HOL/Library/Code_Char.thy	Wed Sep 23 19:17:48 2009 +1000
    16.2 +++ b/src/HOL/Library/Code_Char.thy	Thu Sep 24 11:33:05 2009 +1000
    16.3 @@ -5,7 +5,7 @@
    16.4  header {* Code generation of pretty characters (and strings) *}
    16.5  
    16.6  theory Code_Char
    16.7 -imports List Code_Eval Main
    16.8 +imports List Code_Evaluation Main
    16.9  begin
   16.10  
   16.11  code_type char
   16.12 @@ -32,7 +32,7 @@
   16.13    (OCaml "!((_ : char) = _)")
   16.14    (Haskell infixl 4 "==")
   16.15  
   16.16 -code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
   16.17 +code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
   16.18    (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
   16.19  
   16.20  end
    17.1 --- a/src/HOL/Library/Code_Integer.thy	Wed Sep 23 19:17:48 2009 +1000
    17.2 +++ b/src/HOL/Library/Code_Integer.thy	Thu Sep 24 11:33:05 2009 +1000
    17.3 @@ -100,7 +100,7 @@
    17.4  
    17.5  text {* Evaluation *}
    17.6  
    17.7 -code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"
    17.8 +code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term"
    17.9    (Eval "HOLogic.mk'_number/ HOLogic.intT")
   17.10  
   17.11  end
   17.12 \ No newline at end of file
    18.1 --- a/src/HOL/Library/Coinductive_List.thy	Wed Sep 23 19:17:48 2009 +1000
    18.2 +++ b/src/HOL/Library/Coinductive_List.thy	Thu Sep 24 11:33:05 2009 +1000
    18.3 @@ -260,7 +260,7 @@
    18.4    qed
    18.5  qed
    18.6  
    18.7 -lemma llist_corec [code]:
    18.8 +lemma llist_corec [code, nitpick_const_simp]:
    18.9    "llist_corec a f =
   18.10      (case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))"
   18.11  proof (cases "f a")
   18.12 @@ -656,8 +656,9 @@
   18.13    qed
   18.14  qed
   18.15  
   18.16 -lemma lmap_LNil [simp]: "lmap f LNil = LNil"
   18.17 -  and lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
   18.18 +lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
   18.19 +  and lmap_LCons [simp, nitpick_const_simp]:
   18.20 +  "lmap f (LCons M N) = LCons (f M) (lmap f N)"
   18.21    by (simp_all add: lmap_def llist_corec)
   18.22  
   18.23  lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
   18.24 @@ -728,9 +729,9 @@
   18.25    qed
   18.26  qed
   18.27  
   18.28 -lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
   18.29 -  and lappend_LNil_LCons [simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
   18.30 -  and lappend_LCons [simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
   18.31 +lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
   18.32 +  and lappend_LNil_LCons [simp, nitpick_const_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
   18.33 +  and lappend_LCons [simp, nitpick_const_simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
   18.34    by (simp_all add: lappend_def llist_corec)
   18.35  
   18.36  lemma lappend_LNil1 [simp]: "lappend LNil l = l"
   18.37 @@ -754,7 +755,7 @@
   18.38    iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
   18.39    "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
   18.40  
   18.41 -lemma iterates: "iterates f x = LCons x (iterates f (f x))"
   18.42 +lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
   18.43    apply (unfold iterates_def)
   18.44    apply (subst llist_corec)
   18.45    apply simp
    19.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Sep 23 19:17:48 2009 +1000
    19.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Sep 24 11:33:05 2009 +1000
    19.3 @@ -415,9 +415,9 @@
    19.4  text {* Evaluation *}
    19.5  
    19.6  lemma [code, code del]:
    19.7 -  "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
    19.8 +  "(Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term) = Code_Evaluation.term_of" ..
    19.9  
   19.10 -code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
   19.11 +code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term"
   19.12    (SML "HOLogic.mk'_number/ HOLogic.natT")
   19.13  
   19.14  
    20.1 --- a/src/HOL/Library/Executable_Set.thy	Wed Sep 23 19:17:48 2009 +1000
    20.2 +++ b/src/HOL/Library/Executable_Set.thy	Thu Sep 24 11:33:05 2009 +1000
    20.3 @@ -85,4 +85,6 @@
    20.4    card                ("{*Fset.card*}")
    20.5    fold                ("{*foldl o flip*}")
    20.6  
    20.7 +hide (open) const subset eq_set Inter Union flip
    20.8 +
    20.9  end
   20.10 \ No newline at end of file
    21.1 --- a/src/HOL/Library/Fin_Fun.thy	Wed Sep 23 19:17:48 2009 +1000
    21.2 +++ b/src/HOL/Library/Fin_Fun.thy	Thu Sep 24 11:33:05 2009 +1000
    21.3 @@ -311,17 +311,17 @@
    21.4  notation scomp (infixl "o\<rightarrow>" 60)
    21.5  
    21.6  definition (in term_syntax) valtermify_finfun_const ::
    21.7 -  "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
    21.8 -  "valtermify_finfun_const y = Code_Eval.valtermify finfun_const {\<cdot>} y"
    21.9 +  "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   21.10 +  "valtermify_finfun_const y = Code_Evaluation.valtermify finfun_const {\<cdot>} y"
   21.11  
   21.12  definition (in term_syntax) valtermify_finfun_update_code ::
   21.13 -  "'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
   21.14 -  "valtermify_finfun_update_code x y f = Code_Eval.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
   21.15 +  "'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
   21.16 +  "valtermify_finfun_update_code x y f = Code_Evaluation.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
   21.17  
   21.18  instantiation finfun :: (random, random) random
   21.19  begin
   21.20  
   21.21 -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
   21.22 +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
   21.23      "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight
   21.24         [(1, Quickcheck.random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
   21.25    | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight
    22.1 --- a/src/HOL/Library/Nested_Environment.thy	Wed Sep 23 19:17:48 2009 +1000
    22.2 +++ b/src/HOL/Library/Nested_Environment.thy	Thu Sep 24 11:33:05 2009 +1000
    22.3 @@ -567,6 +567,6 @@
    22.4  qed simp_all
    22.5  
    22.6  lemma [code, code del]:
    22.7 -  "(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Eval.term_of" ..
    22.8 +  "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
    22.9  
   22.10  end
    23.1 --- a/src/HOL/Library/Sum_Of_Squares.thy	Wed Sep 23 19:17:48 2009 +1000
    23.2 +++ b/src/HOL/Library/Sum_Of_Squares.thy	Thu Sep 24 11:33:05 2009 +1000
    23.3 @@ -10,6 +10,7 @@
    23.4  uses
    23.5    ("positivstellensatz.ML")  (* duplicate use!? -- cf. Euclidian_Space.thy *)
    23.6    ("Sum_Of_Squares/sum_of_squares.ML")
    23.7 +  ("Sum_Of_Squares/positivstellensatz_tools.ML")
    23.8    ("Sum_Of_Squares/sos_wrapper.ML")
    23.9  begin
   23.10  
   23.11 @@ -22,112 +23,142 @@
   23.12    of a minute for one sos call, because sos calls CSDP repeatedly.  If
   23.13    you install CSDP locally, sos calls typically takes only a few
   23.14    seconds.
   23.15 +  sos generates a certificate which can be used to repeat the proof
   23.16 +  without calling an external prover.
   23.17  *}
   23.18  
   23.19  text {* setup sos tactic *}
   23.20  
   23.21  use "positivstellensatz.ML"
   23.22 +use "Sum_Of_Squares/positivstellensatz_tools.ML"
   23.23  use "Sum_Of_Squares/sum_of_squares.ML"
   23.24  use "Sum_Of_Squares/sos_wrapper.ML"
   23.25  
   23.26  setup SosWrapper.setup
   23.27  
   23.28 -text {* Tests -- commented since they work only when csdp is installed
   23.29 -  or take too long with remote csdps *}
   23.30 +text {* Tests *}
   23.31 +
   23.32 +lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0"
   23.33 +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))))))")
   23.34 +
   23.35 +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)"
   23.36 +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))))))))))")
   23.37  
   23.38 -(*
   23.39 -lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" by sos
   23.40 +lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0"
   23.41 +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))))))")
   23.42 +
   23.43 +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"
   23.44 +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)))))))")
   23.45  
   23.46 -lemma "a1 >= 0 & a2 >= 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and>
   23.47 -  (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" by sos
   23.48 +lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 --> x * y + x * z + y * z >= 3 * x * y * z"
   23.49 +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))))))))))")
   23.50 +
   23.51 +lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3"
   23.52 +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))))))")
   23.53  
   23.54 -lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" by sos
   23.55 +lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)"
   23.56 +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)))))))")
   23.57  
   23.58 -lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 -->
   23.59 -  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
   23.60 +lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1"
   23.61 +by (sos_cert "(((A<0 * R<1) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))")
   23.62 +
   23.63 +lemma "(x::real) > 1 & y > 1 --> x * y > x + y - 1"
   23.64 +by (sos_cert "((((A<0 * A<1) * R<1) + ((A<=0 * R<1) * (R<1 * [1]^2))))") 
   23.65  
   23.66 -lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 -->
   23.67 -  x * y + x * z + y * z >= 3 * x * y * z" by sos
   23.68 +lemma "abs(x) <= 1 --> abs(64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x) <= (1::real)"
   23.69 +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)))))")
   23.70 +
   23.71 +(* ------------------------------------------------------------------------- *)
   23.72 +(* One component of denominator in dodecahedral example.                     *)
   23.73 +(* ------------------------------------------------------------------------- *)
   23.74  
   23.75 -lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3" by sos
   23.76 +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)"
   23.77 +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)))))))))))))")
   23.78  
   23.79 -lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)" by sos
   23.80 +(* ------------------------------------------------------------------------- *)
   23.81 +(* Over a larger but simpler interval.                                       *)
   23.82 +(* ------------------------------------------------------------------------- *)
   23.83  
   23.84 -lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1" by sos
   23.85 +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)"
   23.86 +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)))))))))))")
   23.87  
   23.88 -lemma "(x::real) > 1 & y > 1 --> x * y > x + y - 1" by sos; 
   23.89 +(* ------------------------------------------------------------------------- *)
   23.90 +(* We can do 12. I think 12 is a sharp bound; see PP's certificate.          *)
   23.91 +(* ------------------------------------------------------------------------- *)
   23.92 +
   23.93 +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)"
   23.94 +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))))))))))))))))))")
   23.95  
   23.96 -lemma "abs(x) <= 1 --> abs(64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x) <= (1::real)" by sos  
   23.97 +(* ------------------------------------------------------------------------- *)
   23.98 +(* Inequality from sci.math (see "Leon-Sotelo, por favor").                  *)
   23.99 +(* ------------------------------------------------------------------------- *)
  23.100  
  23.101 +lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x + y <= x^2 + y^2"
  23.102 +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))))))") 
  23.103  
  23.104 -text {* One component of denominator in dodecahedral example. *}
  23.105 +lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x * y * (x + y) <= x^2 + y^2"
  23.106 +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))))))") 
  23.107  
  23.108 -lemma "2 <= x & x <= 125841 / 50000 & 2 <= y & y <= 125841 / 50000 & 2 <= z &
  23.109 -  z <= 125841 / 50000 --> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= (0::real)" by sos
  23.110 +lemma "0 <= (x::real) & 0 <= y --> x * y * (x + y)^2 <= (x^2 + y^2)^2"
  23.111 +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)))))")
  23.112  
  23.113 +lemma "(0::real) <= a & 0 <= b & 0 <= c & c * (2 * a + b)^3/ 27 <= x \<longrightarrow> c * a^2 * b <= x"
  23.114 +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))))))")
  23.115 + 
  23.116 +lemma "(0::real) < x --> 0 < 1 + x + x^2"
  23.117 +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))))))")
  23.118  
  23.119 -text {* Over a larger but simpler interval. *}
  23.120 +lemma "(0::real) <= x --> 0 < 1 + x + x^2"
  23.121 +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))))))")
  23.122  
  23.123 -lemma "(2::real) <= x & x <= 4 & 2 <= y & y <= 4 & 2 <= z &
  23.124 -  z <= 4 --> 0 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" by sos
  23.125 +lemma "(0::real) < 1 + x^2"
  23.126 +by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))")
  23.127 +
  23.128 +lemma "(0::real) <= 1 + 2 * x + x^2"
  23.129 +by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [x + 1]^2))))")
  23.130  
  23.131 -text {* We can do 12. I think 12 is a sharp bound; see PP's certificate. *}
  23.132 +lemma "(0::real) < 1 + abs x"
  23.133 +by (sos_cert "((R<1 + (((A<=1 * R<1) * (R<1/2 * [1]^2)) + ((A<=0 * R<1) * (R<1/2 * [1]^2)))))")
  23.134  
  23.135 -lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 -->
  23.136 -  12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" by sos
  23.137 +lemma "(0::real) < 1 + (1 + x)^2 * (abs x)"
  23.138 +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))))))")
  23.139  
  23.140  
  23.141 -text {* Inequality from sci.math (see "Leon-Sotelo, por favor"). *}
  23.142  
  23.143 -lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x + y <= x^2 + y^2" by sos 
  23.144 -
  23.145 -lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x * y * (x + y) <= x^2 + y^2" by sos 
  23.146 -
  23.147 -lemma "0 <= (x::real) & 0 <= y --> x * y * (x + y)^2 <= (x^2 + y^2)^2" by sos
  23.148 +lemma "abs ((1::real) + x^2) = (1::real) + x^2"
  23.149 +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)))))))")
  23.150 +lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<longrightarrow> a < 0"
  23.151 +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))))))")
  23.152  
  23.153 -lemma "(0::real) <= a & 0 <= b & 0 <= c & c * (2 * a + b)^3/ 27 <= x \<longrightarrow> c * a^2 * b <= x" by sos
  23.154 - 
  23.155 -lemma "(0::real) < x --> 0 < 1 + x + x^2" by sos
  23.156 -
  23.157 -lemma "(0::real) <= x --> 0 < 1 + x + x^2" by sos
  23.158 -
  23.159 -lemma "(0::real) < 1 + x^2" by sos
  23.160 -
  23.161 -lemma "(0::real) <= 1 + 2 * x + x^2" by sos
  23.162 -
  23.163 -lemma "(0::real) < 1 + abs x" by sos
  23.164 -
  23.165 -lemma "(0::real) < 1 + (1 + x)^2 * (abs x)" by sos
  23.166 +lemma "(0::real) < x --> 1 < y --> y * x <= z --> x < z"
  23.167 +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)))))")
  23.168 +lemma "(1::real) < x --> x^2 < y --> 1 < y"
  23.169 +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)))))))))")
  23.170 +lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)"
  23.171 +by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))")
  23.172 +lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)"
  23.173 +by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))")
  23.174 +lemma "((a::real) * x^2 + b * x + c = 0) --> b^2 >= 4 * a * c"
  23.175 +by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))")
  23.176 +lemma "(0::real) <= b & 0 <= c & 0 <= x & 0 <= y & (x^2 = c) & (y^2 = a^2 * c + b) --> a * c <= y * x"
  23.177 +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)))))")
  23.178 +lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) --> abs((u * x + v * y) - z) <= (e::real)"
  23.179 +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))))))")
  23.180  
  23.181  
  23.182 -lemma "abs ((1::real) + x^2) = (1::real) + x^2" by sos
  23.183 -lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<longrightarrow> a < 0" by sos
  23.184 -
  23.185 -lemma "(0::real) < x --> 1 < y --> y * x <= z --> x < z" by sos
  23.186 -lemma "(1::real) < x --> x^2 < y --> 1 < y" by sos
  23.187 -lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" by sos
  23.188 -lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" by sos
  23.189 -lemma "((a::real) * x^2 + b * x + c = 0) --> b^2 >= 4 * a * c" by sos
  23.190 -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
  23.191 -lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) -->
  23.192 -  abs((u * x + v * y) - z) <= (e::real)" by sos
  23.193 -
  23.194 -(*
  23.195 -lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 -->
  23.196 -  y^2 - 7 * y - 12 * x + 17 >= 0" by sos  -- {* Too hard?*}
  23.197 -*)
  23.198 +(* 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?*)
  23.199  
  23.200  lemma "(0::real) <= x --> (1 + x + x^2)/(1 + x^2) <= 1 + x"
  23.201 -  by sos
  23.202 +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))))))")
  23.203  
  23.204  lemma "(0::real) <= x --> 1 - x <= 1 / (1 + x + x^2)"
  23.205 -  by sos
  23.206 +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))))))))")
  23.207  
  23.208  lemma "(x::real) <= 1 / 2 --> - x - 2 * x^2 <= - x / (1 - x)"
  23.209 -  by sos
  23.210 +by (sos_cert "((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2))))")
  23.211  
  23.212 -lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 -->
  23.213 -  2*(x::real) = - p + 2*r | 2*x = -p - 2*r" by sos
  23.214 -*)
  23.215 +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"
  23.216 +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)))))")
  23.217  
  23.218  end
  23.219 +
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Thu Sep 24 11:33:05 2009 +1000
    24.3 @@ -0,0 +1,158 @@
    24.4 +(* Title:      positivstellensatz_tools.ML
    24.5 +   Author:     Philipp Meyer, TU Muenchen
    24.6 +
    24.7 +Functions for generating a certificate from a positivstellensatz and vice versa
    24.8 +*)
    24.9 +
   24.10 +signature POSITIVSTELLENSATZ_TOOLS =
   24.11 +sig
   24.12 +  val pss_tree_to_cert : RealArith.pss_tree -> string
   24.13 +
   24.14 +  val cert_to_pss_tree : Proof.context -> string -> RealArith.pss_tree
   24.15 +
   24.16 +end
   24.17 +
   24.18 +
   24.19 +structure PositivstellensatzTools : POSITIVSTELLENSATZ_TOOLS =
   24.20 +struct
   24.21 +
   24.22 +open RealArith FuncUtil
   24.23 +
   24.24 +(*** certificate generation ***)
   24.25 +
   24.26 +fun string_of_rat r =
   24.27 +  let
   24.28 +    val (nom, den) = Rat.quotient_of_rat r
   24.29 +  in
   24.30 +    if den = 1 then string_of_int nom
   24.31 +    else string_of_int nom ^ "/" ^ string_of_int den
   24.32 +  end
   24.33 +
   24.34 +(* map polynomials to strings *)
   24.35 +
   24.36 +fun string_of_varpow x k =
   24.37 +  let
   24.38 +    val term = term_of x
   24.39 +    val name = case term of
   24.40 +      Free (n, _) => n
   24.41 +    | _ => error "Term in monomial not free variable"
   24.42 +  in
   24.43 +    if k = 1 then name else name ^ "^" ^ string_of_int k 
   24.44 +  end
   24.45 +
   24.46 +fun string_of_monomial m = 
   24.47 + if Ctermfunc.is_undefined m then "1" 
   24.48 + else 
   24.49 +  let 
   24.50 +   val m' = dest_monomial m
   24.51 +   val vps = fold_rev (fn (x,k) => cons (string_of_varpow x k)) m' [] 
   24.52 +  in foldr1 (fn (s, t) => s ^ "*" ^ t) vps
   24.53 +  end
   24.54 +
   24.55 +fun string_of_cmonomial (m,c) =
   24.56 +  if Ctermfunc.is_undefined m then string_of_rat c
   24.57 +  else if c = Rat.one then string_of_monomial m
   24.58 +  else (string_of_rat c) ^ "*" ^ (string_of_monomial m);
   24.59 +
   24.60 +fun string_of_poly p = 
   24.61 + if Monomialfunc.is_undefined p then "0" 
   24.62 + else
   24.63 +  let 
   24.64 +   val cms = map string_of_cmonomial
   24.65 +     (sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p))
   24.66 +  in foldr1 (fn (t1, t2) => t1 ^ " + " ^ t2) cms
   24.67 +  end;
   24.68 +
   24.69 +fun pss_to_cert (Axiom_eq i) = "A=" ^ string_of_int i
   24.70 +  | pss_to_cert (Axiom_le i) = "A<=" ^ string_of_int i
   24.71 +  | pss_to_cert (Axiom_lt i) = "A<" ^ string_of_int i
   24.72 +  | pss_to_cert (Rational_eq r) = "R=" ^ string_of_rat r
   24.73 +  | pss_to_cert (Rational_le r) = "R<=" ^ string_of_rat r
   24.74 +  | pss_to_cert (Rational_lt r) = "R<" ^ string_of_rat r
   24.75 +  | pss_to_cert (Square p) = "[" ^ string_of_poly p ^ "]^2"
   24.76 +  | pss_to_cert (Eqmul (p, pss)) = "([" ^ string_of_poly p ^ "] * " ^ pss_to_cert pss ^ ")"
   24.77 +  | pss_to_cert (Sum (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " + " ^ pss_to_cert pss2 ^ ")"
   24.78 +  | pss_to_cert (Product (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " * " ^ pss_to_cert pss2 ^ ")"
   24.79 +
   24.80 +fun pss_tree_to_cert Trivial = "()"
   24.81 +  | pss_tree_to_cert (Cert pss) = "(" ^ pss_to_cert pss ^ ")"
   24.82 +  | pss_tree_to_cert (Branch (t1, t2)) = "(" ^ pss_tree_to_cert t1 ^ " & " ^ pss_tree_to_cert t2 ^ ")"
   24.83 +
   24.84 +(*** certificate parsing ***)
   24.85 +
   24.86 +(* basic parser *)
   24.87 +
   24.88 +val str = Scan.this_string
   24.89 +
   24.90 +val number = Scan.repeat1 (Scan.one Symbol.is_ascii_digit >>
   24.91 +  (fn s => ord s - ord "0")) >>
   24.92 +  foldl1 (fn (n, d) => n * 10 + d)
   24.93 +
   24.94 +val nat = number
   24.95 +val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op *;
   24.96 +val rat = int --| str "/" -- int >> Rat.rat_of_quotient
   24.97 +val rat_int = rat || int >> Rat.rat_of_int
   24.98 +
   24.99 +(* polynomial parser *)
  24.100 +
  24.101 +fun repeat_sep s f = f ::: Scan.repeat (str s |-- f)
  24.102 +
  24.103 +val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
  24.104 +
  24.105 +fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
  24.106 +  (fn (x, k) => (cterm_of (Context.theory_of_proof ctxt) (Free (x, @{typ real})), k)) 
  24.107 +
  24.108 +fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
  24.109 +  foldl (uncurry Ctermfunc.update) Ctermfunc.undefined
  24.110 +
  24.111 +fun parse_cmonomial ctxt =
  24.112 +  rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
  24.113 +  (parse_monomial ctxt) >> (fn m => (m, Rat.one)) ||
  24.114 +  rat_int >> (fn r => (Ctermfunc.undefined, r))
  24.115 +
  24.116 +fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
  24.117 +  foldl (uncurry Monomialfunc.update) Monomialfunc.undefined
  24.118 +
  24.119 +(* positivstellensatz parser *)
  24.120 +
  24.121 +val parse_axiom =
  24.122 +  (str "A=" |-- int >> Axiom_eq) ||
  24.123 +  (str "A<=" |-- int >> Axiom_le) ||
  24.124 +  (str "A<" |-- int >> Axiom_lt)
  24.125 +
  24.126 +val parse_rational =
  24.127 +  (str "R=" |-- rat_int >> Rational_eq) ||
  24.128 +  (str "R<=" |-- rat_int >> Rational_le) ||
  24.129 +  (str "R<" |-- rat_int >> Rational_lt)
  24.130 +
  24.131 +fun parse_cert ctxt input =
  24.132 +  let
  24.133 +    val pc = parse_cert ctxt
  24.134 +    val pp = parse_poly ctxt
  24.135 +  in
  24.136 +  (parse_axiom ||
  24.137 +   parse_rational ||
  24.138 +   str "[" |-- pp --| str "]^2" >> Square ||
  24.139 +   str "([" |-- pp --| str "]*" -- pc --| str ")" >> Eqmul ||
  24.140 +   str "(" |-- pc --| str "*" -- pc --| str ")" >> Product ||
  24.141 +   str "(" |-- pc --| str "+" -- pc --| str ")" >> Sum) input
  24.142 +  end
  24.143 +
  24.144 +fun parse_cert_tree ctxt input =
  24.145 +  let
  24.146 +    val pc = parse_cert ctxt
  24.147 +    val pt = parse_cert_tree ctxt
  24.148 +  in
  24.149 +  (str "()" >> K Trivial ||
  24.150 +   str "(" |-- pc --| str ")" >> Cert ||
  24.151 +   str "(" |-- pt --| str "&" -- pt --| str ")" >> Branch) input
  24.152 +  end
  24.153 +
  24.154 +(* scanner *)
  24.155 +
  24.156 +fun cert_to_pss_tree ctxt input_str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt)
  24.157 +  (filter_out Symbol.is_blank (Symbol.explode input_str))
  24.158 +
  24.159 +end
  24.160 +
  24.161 +
    25.1 --- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Wed Sep 23 19:17:48 2009 +1000
    25.2 +++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Thu Sep 24 11:33:05 2009 +1000
    25.3 @@ -136,13 +136,32 @@
    25.4      run_solver name (Path.explode cmd) find_failure
    25.5    end
    25.6  
    25.7 +(* certificate output *)
    25.8 +
    25.9 +fun output_line cert = "To repeat this proof with a certifiate use this command:\n" ^
   25.10 +        (Markup.markup Markup.sendback) ("by (sos_cert \"" ^ cert ^ "\")")
   25.11 +
   25.12 +val print_cert = Output.writeln o output_line o PositivstellensatzTools.pss_tree_to_cert
   25.13 +
   25.14  (* setup tactic *)
   25.15  
   25.16 -fun sos_solver name = (SIMPLE_METHOD' o (Sos.sos_tac (call_solver name))) 
   25.17 +fun parse_cert (input as (ctxt, _)) = 
   25.18 +  (Scan.lift OuterParse.string >>
   25.19 +    PositivstellensatzTools.cert_to_pss_tree (Context.proof_of ctxt)) input
   25.20 +
   25.21 +fun sos_solver print method = (SIMPLE_METHOD' o (Sos.sos_tac print method)) 
   25.22  
   25.23 -val sos_method = Scan.option (Scan.lift OuterParse.xname) >> sos_solver
   25.24 +val sos_method =
   25.25 +   Scan.lift (Scan.option OuterParse.xname) >> (fn n => Sos.Prover (call_solver n)) >>
   25.26 +   sos_solver print_cert
   25.27  
   25.28 -val setup = Method.setup @{binding sos} sos_method
   25.29 -  "Prove universal problems over the reals using sums of squares"
   25.30 +val sos_cert_method =
   25.31 +  parse_cert >> Sos.Certificate >> sos_solver ignore
   25.32 +
   25.33 +val setup =
   25.34 +     Method.setup @{binding sos} sos_method
   25.35 +     "Prove universal problems over the reals using sums of squares"
   25.36 +  #> Method.setup @{binding sos_cert} sos_cert_method
   25.37 +     "Prove universal problems over the reals using sums of squares with certificates"
   25.38  
   25.39  end
    26.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Sep 23 19:17:48 2009 +1000
    26.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Sep 24 11:33:05 2009 +1000
    26.3 @@ -8,7 +8,12 @@
    26.4  signature SOS =
    26.5  sig
    26.6  
    26.7 -  val sos_tac : (string -> string) -> Proof.context -> int -> Tactical.tactic
    26.8 +  datatype proof_method =
    26.9 +    Certificate of RealArith.pss_tree
   26.10 +  | Prover of (string -> string)
   26.11 +
   26.12 +  val sos_tac : (RealArith.pss_tree -> unit) ->
   26.13 +    proof_method -> Proof.context -> int -> tactic
   26.14  
   26.15    val debugging : bool ref;
   26.16    
   26.17 @@ -18,6 +23,8 @@
   26.18  structure Sos : SOS = 
   26.19  struct
   26.20  
   26.21 +open FuncUtil;
   26.22 +
   26.23  val rat_0 = Rat.zero;
   26.24  val rat_1 = Rat.one;
   26.25  val rat_2 = Rat.two;
   26.26 @@ -59,6 +66,10 @@
   26.27  
   26.28  exception Failure of string;
   26.29  
   26.30 +datatype proof_method =
   26.31 +    Certificate of RealArith.pss_tree
   26.32 +  | Prover of (string -> string)
   26.33 +
   26.34  (* Turn a rational into a decimal string with d sig digits.                  *)
   26.35  
   26.36  local
   26.37 @@ -93,23 +104,11 @@
   26.38  
   26.39  (* The main types.                                                           *)
   26.40  
   26.41 -fun strict_ord ord (x,y) = case ord (x,y) of LESS => LESS | _ => GREATER
   26.42 -
   26.43 -structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
   26.44 -
   26.45  type vector = int* Rat.rat Intfunc.T;
   26.46  
   26.47  type matrix = (int*int)*(Rat.rat Intpairfunc.T);
   26.48  
   26.49 -type monomial = int Ctermfunc.T;
   26.50 -
   26.51 -val cterm_ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t))
   26.52 - fun monomial_ord (m1,m2) = list_ord (prod_ord cterm_ord int_ord) (Ctermfunc.graph m1, Ctermfunc.graph m2)
   26.53 -structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
   26.54 -
   26.55 -type poly = Rat.rat Monomialfunc.T;
   26.56 -
   26.57 - fun iszero (k,r) = r =/ rat_0;
   26.58 +fun iszero (k,r) = r =/ rat_0;
   26.59  
   26.60  fun fold_rev2 f l1 l2 b =
   26.61    case (l1,l2) of
   26.62 @@ -346,11 +345,6 @@
   26.63    sort humanorder_varpow (Ctermfunc.graph m2))
   26.64  end;
   26.65  
   26.66 -fun fold1 f l =  case l of
   26.67 -   []     => error "fold1"
   26.68 - | [x]    => x
   26.69 - | (h::t) => f h (fold1 f t);
   26.70 -
   26.71  (* Conversions to strings.                                                   *)
   26.72  
   26.73  fun string_of_vector min_size max_size (v:vector) =
   26.74 @@ -359,7 +353,7 @@
   26.75    let 
   26.76     val n = max min_size (min n_raw max_size) 
   26.77     val xs = map (Rat.string_of_rat o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
   26.78 -  in "[" ^ fold1 (fn s => fn t => s ^ ", " ^ t) xs ^
   26.79 +  in "[" ^ foldr1 (fn (s, t) => s ^ ", " ^ t) xs ^
   26.80    (if n_raw > max_size then ", ...]" else "]")
   26.81    end
   26.82   end;
   26.83 @@ -370,7 +364,7 @@
   26.84    val i = min max_size i_raw 
   26.85    val j = min max_size j_raw
   26.86    val rstr = map (fn k => string_of_vector j j (row k m)) (1 upto i) 
   26.87 - in "["^ fold1 (fn s => fn t => s^";\n "^t) rstr ^
   26.88 + in "["^ foldr1 (fn (s, t) => s^";\n "^t) rstr ^
   26.89    (if j > max_size then "\n ...]" else "]")
   26.90   end;
   26.91  
   26.92 @@ -396,7 +390,7 @@
   26.93   if Ctermfunc.is_undefined m then "1" else
   26.94   let val vps = fold_rev (fn (x,k) => fn a => string_of_varpow x k :: a)
   26.95    (sort humanorder_varpow (Ctermfunc.graph m)) [] 
   26.96 - in fold1 (fn s => fn t => s^"*"^t) vps
   26.97 + in foldr1 (fn (s, t) => s^"*"^t) vps
   26.98   end;
   26.99  
  26.100  fun string_of_cmonomial (c,m) =
  26.101 @@ -404,7 +398,7 @@
  26.102   else if c =/ rat_1 then string_of_monomial m
  26.103   else Rat.string_of_rat c ^ "*" ^ string_of_monomial m;;
  26.104  
  26.105 -fun string_of_poly (p:poly) =
  26.106 +fun string_of_poly p =
  26.107   if Monomialfunc.is_undefined p then "<<0>>" else
  26.108   let 
  26.109    val cms = sort (fn ((m1,_),(m2,_)) => humanorder_monomial m1  m2) (Monomialfunc.graph p)
  26.110 @@ -478,10 +472,9 @@
  26.111   let 
  26.112    val n = dim v
  26.113    val strs = map (decimalize 20 o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
  26.114 - in fold1 (fn x => fn y => x ^ " " ^ y) strs ^ "\n"
  26.115 + in foldr1 (fn (x, y) => x ^ " " ^ y) strs ^ "\n"
  26.116   end;
  26.117  
  26.118 -fun increasing f ord (x,y) = ord (f x, f y);
  26.119  fun triple_int_ord ((a,b,c),(a',b',c')) = 
  26.120   prod_ord int_ord (prod_ord int_ord int_ord) 
  26.121      ((a,(b,c)),(a',(b',c')));
  26.122 @@ -989,7 +982,7 @@
  26.123   let val alts =
  26.124    map (fn k => let val oths = enumerate_monomials (d - k) (tl vars) 
  26.125                 in map (fn ks => if k = 0 then ks else Ctermfunc.update (hd vars, k) ks) oths end) (0 upto d) 
  26.126 - in fold1 (curry op @) alts
  26.127 + in foldr1 op @ alts
  26.128   end;
  26.129  
  26.130  (* Enumerate products of distinct input polys with degree <= d.              *)
  26.131 @@ -1040,7 +1033,7 @@
  26.132   in
  26.133    string_of_int m ^ "\n" ^
  26.134    string_of_int nblocks ^ "\n" ^
  26.135 -  (fold1 (fn s => fn t => s^" "^t) (map string_of_int blocksizes)) ^
  26.136 +  (foldr1 (fn (s, t) => s^" "^t) (map string_of_int blocksizes)) ^
  26.137    "\n" ^
  26.138    sdpa_of_vector obj ^
  26.139    fold_rev2 (fn k => fn m => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a)
  26.140 @@ -1080,11 +1073,6 @@
  26.141    fun tryfind f = tryfind_with "tryfind" f
  26.142  end
  26.143  
  26.144 -(*
  26.145 -fun tryfind f [] = error "tryfind"
  26.146 -  | tryfind f (x::xs) = (f x handle ERROR _ => tryfind f xs);
  26.147 -*)
  26.148 -
  26.149  (* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *)
  26.150  
  26.151   
  26.152 @@ -1210,61 +1198,17 @@
  26.153  fun deepen f n = 
  26.154    (writeln ("Searching with depth limit " ^ string_of_int n) ; (f n handle Failure s => (writeln ("failed with message: " ^ s) ; deepen f (n+1))))
  26.155  
  26.156 -(* The ordering so we can create canonical HOL polynomials.                  *)
  26.157  
  26.158 -fun dest_monomial mon = sort (increasing fst cterm_ord) (Ctermfunc.graph mon);
  26.159 -
  26.160 -fun monomial_order (m1,m2) =
  26.161 - if Ctermfunc.is_undefined m2 then LESS 
  26.162 - else if Ctermfunc.is_undefined m1 then GREATER 
  26.163 - else
  26.164 -  let val mon1 = dest_monomial m1 
  26.165 -      val mon2 = dest_monomial m2
  26.166 -      val deg1 = fold (curry op + o snd) mon1 0
  26.167 -      val deg2 = fold (curry op + o snd) mon2 0 
  26.168 -  in if deg1 < deg2 then GREATER else if deg1 > deg2 then LESS
  26.169 -     else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
  26.170 -  end;
  26.171 -
  26.172 -fun dest_poly p =
  26.173 -  map (fn (m,c) => (c,dest_monomial m))
  26.174 -      (sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p));
  26.175 -
  26.176 -(* Map back polynomials and their composites to HOL.                         *)
  26.177 +(* Map back polynomials and their composites to a positivstellensatz.        *)
  26.178  
  26.179  local
  26.180   open Thm Numeral RealArith
  26.181  in
  26.182  
  26.183 -fun cterm_of_varpow x k = if k = 1 then x else capply (capply @{cterm "op ^ :: real => _"} x) 
  26.184 -  (mk_cnumber @{ctyp nat} k)
  26.185 -
  26.186 -fun cterm_of_monomial m = 
  26.187 - if Ctermfunc.is_undefined m then @{cterm "1::real"} 
  26.188 - else 
  26.189 -  let 
  26.190 -   val m' = dest_monomial m
  26.191 -   val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' [] 
  26.192 -  in fold1 (fn s => fn t => capply (capply @{cterm "op * :: real => _"} s) t) vps
  26.193 -  end
  26.194 -
  26.195 -fun cterm_of_cmonomial (m,c) = if Ctermfunc.is_undefined m then cterm_of_rat c
  26.196 -    else if c = Rat.one then cterm_of_monomial m
  26.197 -    else capply (capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
  26.198 -
  26.199 -fun cterm_of_poly p = 
  26.200 - if Monomialfunc.is_undefined p then @{cterm "0::real"} 
  26.201 - else
  26.202 -  let 
  26.203 -   val cms = map cterm_of_cmonomial
  26.204 -     (sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p))
  26.205 -  in fold1 (fn t1 => fn t2 => capply(capply @{cterm "op + :: real => _"} t1) t2) cms
  26.206 -  end;
  26.207 -
  26.208 -fun cterm_of_sqterm (c,p) = Product(Rational_lt c,Square(cterm_of_poly p));
  26.209 +fun cterm_of_sqterm (c,p) = Product(Rational_lt c,Square p);
  26.210  
  26.211  fun cterm_of_sos (pr,sqs) = if null sqs then pr
  26.212 -  else Product(pr,fold1 (fn a => fn b => Sum(a,b)) (map cterm_of_sqterm sqs));
  26.213 +  else Product(pr,foldr1 (fn (a, b) => Sum(a,b)) (map cterm_of_sqterm sqs));
  26.214  
  26.215  end
  26.216  
  26.217 @@ -1275,14 +1219,14 @@
  26.218    fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS
  26.219  in
  26.220    (* FIXME: Replace tryfind by get_first !! *)
  26.221 -fun real_nonlinear_prover prover ctxt =
  26.222 +fun real_nonlinear_prover proof_method ctxt =
  26.223   let 
  26.224    val {add,mul,neg,pow,sub,main} =  Normalizer.semiring_normalizers_ord_wrapper ctxt
  26.225        (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
  26.226       simple_cterm_ord
  26.227    val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
  26.228         real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
  26.229 -  fun mainf  translator (eqs,les,lts) = 
  26.230 +  fun mainf cert_choice translator (eqs,les,lts) = 
  26.231    let 
  26.232     val eq0 = map (poly_of_term o dest_arg1 o concl) eqs
  26.233     val le0 = map (poly_of_term o dest_arg o concl) les
  26.234 @@ -1303,33 +1247,49 @@
  26.235                       else raise Failure "trivial_axiom: Not a trivial axiom"
  26.236       | _ => error "trivial_axiom: Not a trivial axiom"
  26.237     in 
  26.238 -  ((let val th = tryfind trivial_axiom (keq @ klep @ kltp)
  26.239 -   in fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th end)
  26.240 -   handle Failure _ => (
  26.241 -    let 
  26.242 -     val pol = fold_rev poly_mul (map fst ltp) (poly_const Rat.one)
  26.243 -     val leq = lep @ ltp
  26.244 -     fun tryall d =
  26.245 -      let val e = multidegree pol
  26.246 -          val k = if e = 0 then 0 else d div e
  26.247 -          val eq' = map fst eq 
  26.248 -      in tryfind (fn i => (d,i,real_positivnullstellensatz_general prover false d eq' leq
  26.249 -                            (poly_neg(poly_pow pol i))))
  26.250 -              (0 upto k)
  26.251 -      end
  26.252 -    val (d,i,(cert_ideal,cert_cone)) = deepen tryall 0
  26.253 -    val proofs_ideal =
  26.254 -      map2 (fn q => fn (p,ax) => Eqmul(cterm_of_poly q,ax)) cert_ideal eq
  26.255 -    val proofs_cone = map cterm_of_sos cert_cone
  26.256 -    val proof_ne = if null ltp then Rational_lt Rat.one else
  26.257 -      let val p = fold1 (fn s => fn t => Product(s,t)) (map snd ltp) 
  26.258 -      in  funpow i (fn q => Product(p,q)) (Rational_lt Rat.one)
  26.259 -      end
  26.260 -    val proof = fold1 (fn s => fn t => Sum(s,t))
  26.261 -                           (proof_ne :: proofs_ideal @ proofs_cone) 
  26.262 -    in writeln "Translating proof certificate to HOL";
  26.263 -       translator (eqs,les,lts) proof
  26.264 -    end))
  26.265 +  (let val th = tryfind trivial_axiom (keq @ klep @ kltp)
  26.266 +   in
  26.267 +    (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th, Trivial)
  26.268 +   end)
  26.269 +   handle Failure _ => 
  26.270 +     (let val proof =
  26.271 +       (case proof_method of Certificate certs =>
  26.272 +         (* choose certificate *)
  26.273 +         let
  26.274 +           fun chose_cert [] (Cert c) = c
  26.275 +             | chose_cert (Left::s) (Branch (l, _)) = chose_cert s l
  26.276 +             | chose_cert (Right::s) (Branch (_, r)) = chose_cert s r
  26.277 +             | chose_cert _ _ = error "certificate tree in invalid form"
  26.278 +         in
  26.279 +           chose_cert cert_choice certs
  26.280 +         end
  26.281 +       | Prover prover =>
  26.282 +         (* call prover *)
  26.283 +         let 
  26.284 +          val pol = fold_rev poly_mul (map fst ltp) (poly_const Rat.one)
  26.285 +          val leq = lep @ ltp
  26.286 +          fun tryall d =
  26.287 +           let val e = multidegree pol
  26.288 +               val k = if e = 0 then 0 else d div e
  26.289 +               val eq' = map fst eq 
  26.290 +           in tryfind (fn i => (d,i,real_positivnullstellensatz_general prover false d eq' leq
  26.291 +                                 (poly_neg(poly_pow pol i))))
  26.292 +                   (0 upto k)
  26.293 +           end
  26.294 +         val (d,i,(cert_ideal,cert_cone)) = deepen tryall 0
  26.295 +         val proofs_ideal =
  26.296 +           map2 (fn q => fn (p,ax) => Eqmul(q,ax)) cert_ideal eq
  26.297 +         val proofs_cone = map cterm_of_sos cert_cone
  26.298 +         val proof_ne = if null ltp then Rational_lt Rat.one else
  26.299 +           let val p = foldr1 (fn (s, t) => Product(s,t)) (map snd ltp) 
  26.300 +           in  funpow i (fn q => Product(p,q)) (Rational_lt Rat.one)
  26.301 +           end
  26.302 +         in 
  26.303 +           foldr1 (fn (s, t) => Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) 
  26.304 +         end)
  26.305 +     in
  26.306 +        (translator (eqs,les,lts) proof, Cert proof)
  26.307 +     end)
  26.308     end
  26.309   in mainf end
  26.310  end
  26.311 @@ -1396,7 +1356,7 @@
  26.312           orelse g aconvc @{cterm "op < :: real => _"} 
  26.313         then arg_conv cv ct else arg1_conv cv ct
  26.314      end
  26.315 -  fun mainf translator =
  26.316 +  fun mainf cert_choice translator =
  26.317     let 
  26.318      fun substfirst(eqs,les,lts) =
  26.319        ((let 
  26.320 @@ -1407,7 +1367,7 @@
  26.321                                     aconvc @{cterm "0::real"}) (map modify eqs),
  26.322                                     map modify les,map modify lts)
  26.323         end)
  26.324 -       handle Failure  _ => real_nonlinear_prover prover ctxt translator (rev eqs, rev les, rev lts))
  26.325 +       handle Failure  _ => real_nonlinear_prover prover ctxt cert_choice translator (rev eqs, rev les, rev lts))
  26.326      in substfirst
  26.327     end
  26.328  
  26.329 @@ -1417,7 +1377,8 @@
  26.330  
  26.331  (* Overall function. *)
  26.332  
  26.333 -fun real_sos prover ctxt t = gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt) t;
  26.334 +fun real_sos prover ctxt =
  26.335 +  gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt)
  26.336  end;
  26.337  
  26.338  (* A tactic *)
  26.339 @@ -1429,8 +1390,6 @@
  26.340     end
  26.341  | _ => ([],ct)
  26.342  
  26.343 -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})
  26.344 -
  26.345  val known_sos_constants = 
  26.346    [@{term "op ==>"}, @{term "Trueprop"}, 
  26.347     @{term "op -->"}, @{term "op &"}, @{term "op |"}, 
  26.348 @@ -1458,17 +1417,19 @@
  26.349    val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs 
  26.350            then error "SOS: not sos. Variables with type not real" else ()
  26.351    val vs = Term.add_vars t []
  26.352 -  val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs 
  26.353 +  val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) vs 
  26.354            then error "SOS: not sos. Variables with type not real" else ()
  26.355    val ukcs = subtract (fn (t,p) => Const p aconv t) kcts (Term.add_consts t [])
  26.356    val _ = if  null ukcs then () 
  26.357                else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs))
  26.358  in () end
  26.359  
  26.360 -fun core_sos_tac prover ctxt = CSUBGOAL (fn (ct, i) => 
  26.361 +fun core_sos_tac print_cert prover ctxt = CSUBGOAL (fn (ct, i) => 
  26.362    let val _ = check_sos known_sos_constants ct
  26.363        val (avs, p) = strip_all ct
  26.364 -      val th = standard (fold_rev forall_intr avs (real_sos prover ctxt (Thm.dest_arg p)))
  26.365 +      val (ths, certificates) = real_sos prover ctxt (Thm.dest_arg p)
  26.366 +      val th = standard (fold_rev forall_intr avs ths)
  26.367 +      val _ = print_cert certificates
  26.368    in rtac th i end);
  26.369  
  26.370  fun default_SOME f NONE v = SOME v
  26.371 @@ -1506,7 +1467,7 @@
  26.372  
  26.373  fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
  26.374  
  26.375 -fun sos_tac prover ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac prover ctxt
  26.376 +fun sos_tac print_cert prover ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac print_cert prover ctxt
  26.377  
  26.378  
  26.379  end;
    27.1 --- a/src/HOL/Library/normarith.ML	Wed Sep 23 19:17:48 2009 +1000
    27.2 +++ b/src/HOL/Library/normarith.ML	Thu Sep 24 11:33:05 2009 +1000
    27.3 @@ -15,7 +15,7 @@
    27.4  structure NormArith : NORM_ARITH = 
    27.5  struct
    27.6  
    27.7 - open Conv Thm;
    27.8 + open Conv Thm FuncUtil;
    27.9   val bool_eq = op = : bool *bool -> bool
   27.10    fun dest_ratconst t = case term_of t of
   27.11     Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
   27.12 @@ -330,13 +330,13 @@
   27.13     val zerodests = filter
   27.14          (fn t => null (Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
   27.15  
   27.16 -  in RealArith.real_linear_prover translator
   27.17 +  in fst (RealArith.real_linear_prover translator
   27.18          (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
   27.19              zerodests,
   27.20          map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
   27.21                         arg_conv (arg_conv real_poly_conv))) ges',
   27.22          map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
   27.23 -                       arg_conv (arg_conv real_poly_conv))) gts)
   27.24 +                       arg_conv (arg_conv real_poly_conv))) gts))
   27.25    end
   27.26  in val real_vector_combo_prover = real_vector_combo_prover
   27.27  end;
   27.28 @@ -389,9 +389,9 @@
   27.29     val (th1,th2) = conj_pair(rawrule th)
   27.30    in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc
   27.31    end
   27.32 -in fun real_vector_prover ctxt translator (eqs,ges,gts) =
   27.33 -     real_vector_ineq_prover ctxt translator
   27.34 -         (fold_rev (splitequation ctxt) eqs ges,gts)
   27.35 +in fun real_vector_prover ctxt _ translator (eqs,ges,gts) =
   27.36 +     (real_vector_ineq_prover ctxt translator
   27.37 +         (fold_rev (splitequation ctxt) eqs ges,gts), RealArith.Trivial)
   27.38  end;
   27.39  
   27.40    fun init_conv ctxt = 
   27.41 @@ -400,7 +400,7 @@
   27.42     then_conv field_comp_conv 
   27.43     then_conv nnf_conv
   27.44  
   27.45 - fun pure ctxt = RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt);
   27.46 + fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt);
   27.47   fun norm_arith ctxt ct = 
   27.48    let 
   27.49     val ctxt' = Variable.declare_term (term_of ct) ctxt
    28.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Sep 23 19:17:48 2009 +1000
    28.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Sep 24 11:33:05 2009 +1000
    28.3 @@ -1,10 +1,11 @@
    28.4 -(* Title:      Library/positivstellensatz
    28.5 +(* Title:      Library/Sum_Of_Squares/positivstellensatz
    28.6     Author:     Amine Chaieb, University of Cambridge
    28.7     Description: A generic arithmetic prover based on Positivstellensatz certificates --- 
    28.8      also implements Fourrier-Motzkin elimination as a special case Fourrier-Motzkin elimination.
    28.9  *)
   28.10  
   28.11  (* A functor for finite mappings based on Tables *)
   28.12 +
   28.13  signature FUNC = 
   28.14  sig
   28.15   type 'a T
   28.16 @@ -75,27 +76,54 @@
   28.17  end
   28.18  end;
   28.19  
   28.20 +(* Some standard functors and utility functions for them *)
   28.21 +
   28.22 +structure FuncUtil =
   28.23 +struct
   28.24 +
   28.25 +fun increasing f ord (x,y) = ord (f x, f y);
   28.26 +
   28.27  structure Intfunc = FuncFun(type key = int val ord = int_ord);
   28.28 +structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
   28.29 +structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
   28.30  structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
   28.31  structure Termfunc = FuncFun(type key = term val ord = TermOrd.fast_term_ord);
   28.32 -structure Ctermfunc = FuncFun(type key = cterm val ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t)));
   28.33 +
   28.34 +val cterm_ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t))
   28.35 +
   28.36 +structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
   28.37 +
   28.38 +type monomial = int Ctermfunc.T;
   28.39  
   28.40 -structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
   28.41 +fun monomial_ord (m1,m2) = list_ord (prod_ord cterm_ord int_ord) (Ctermfunc.graph m1, Ctermfunc.graph m2)
   28.42 +
   28.43 +structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
   28.44  
   28.45 +type poly = Rat.rat Monomialfunc.T;
   28.46 +
   28.47 +(* The ordering so we can create canonical HOL polynomials.                  *)
   28.48  
   28.49 -    (* Some useful derived rules *)
   28.50 -fun deduct_antisym_rule tha thb = 
   28.51 -    equal_intr (implies_intr (cprop_of thb) tha) 
   28.52 -     (implies_intr (cprop_of tha) thb);
   28.53 +fun dest_monomial mon = sort (increasing fst cterm_ord) (Ctermfunc.graph mon);
   28.54  
   28.55 -fun prove_hyp tha thb = 
   28.56 -  if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
   28.57 -  then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb;
   28.58 +fun monomial_order (m1,m2) =
   28.59 + if Ctermfunc.is_undefined m2 then LESS 
   28.60 + else if Ctermfunc.is_undefined m1 then GREATER 
   28.61 + else
   28.62 +  let val mon1 = dest_monomial m1 
   28.63 +      val mon2 = dest_monomial m2
   28.64 +      val deg1 = fold (curry op + o snd) mon1 0
   28.65 +      val deg2 = fold (curry op + o snd) mon2 0 
   28.66 +  in if deg1 < deg2 then GREATER else if deg1 > deg2 then LESS
   28.67 +     else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
   28.68 +  end;
   28.69  
   28.70 +end
   28.71  
   28.72 +(* positivstellensatz datatype and prover generation *)
   28.73  
   28.74  signature REAL_ARITH = 
   28.75  sig
   28.76 +  
   28.77    datatype positivstellensatz =
   28.78     Axiom_eq of int
   28.79   | Axiom_le of int
   28.80 @@ -103,34 +131,41 @@
   28.81   | Rational_eq of Rat.rat
   28.82   | Rational_le of Rat.rat
   28.83   | Rational_lt of Rat.rat
   28.84 - | Square of cterm
   28.85 - | Eqmul of cterm * positivstellensatz
   28.86 + | Square of FuncUtil.poly
   28.87 + | Eqmul of FuncUtil.poly * positivstellensatz
   28.88   | Sum of positivstellensatz * positivstellensatz
   28.89   | Product of positivstellensatz * positivstellensatz;
   28.90  
   28.91 +datatype pss_tree = Trivial | Cert of positivstellensatz | Branch of pss_tree * pss_tree
   28.92 +
   28.93 +datatype tree_choice = Left | Right
   28.94 +
   28.95 +type prover = tree_choice list -> 
   28.96 +  (thm list * thm list * thm list -> positivstellensatz -> thm) ->
   28.97 +  thm list * thm list * thm list -> thm * pss_tree
   28.98 +type cert_conv = cterm -> thm * pss_tree
   28.99 +
  28.100  val gen_gen_real_arith :
  28.101 -  Proof.context -> (Rat.rat -> Thm.cterm) * conv * conv * conv * 
  28.102 -   conv * conv * conv * conv * conv * conv * 
  28.103 -    ( (thm list * thm list * thm list -> positivstellensatz -> thm) ->
  28.104 -        thm list * thm list * thm list -> thm) -> conv
  28.105 -val real_linear_prover : 
  28.106 -  (thm list * thm list * thm list -> positivstellensatz -> thm) ->
  28.107 -   thm list * thm list * thm list -> thm
  28.108 +  Proof.context -> (Rat.rat -> cterm) * conv * conv * conv *
  28.109 +   conv * conv * conv * conv * conv * conv * prover -> cert_conv
  28.110 +val real_linear_prover : (thm list * thm list * thm list -> positivstellensatz -> thm) ->
  28.111 +  thm list * thm list * thm list -> thm * pss_tree
  28.112  
  28.113  val gen_real_arith : Proof.context ->
  28.114 -   (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv * conv *
  28.115 -   ( (thm list * thm list * thm list -> positivstellensatz -> thm) ->
  28.116 -       thm list * thm list * thm list -> thm) -> conv
  28.117 -val gen_prover_real_arith : Proof.context ->
  28.118 -   ((thm list * thm list * thm list -> positivstellensatz -> thm) ->
  28.119 -     thm list * thm list * thm list -> thm) -> conv
  28.120 -val real_arith : Proof.context -> conv
  28.121 +  (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv
  28.122 +
  28.123 +val gen_prover_real_arith : Proof.context -> prover -> cert_conv
  28.124 +
  28.125 +val is_ratconst : cterm -> bool
  28.126 +val dest_ratconst : cterm -> Rat.rat
  28.127 +val cterm_of_rat : Rat.rat -> cterm
  28.128 +
  28.129  end
  28.130  
  28.131 -structure RealArith (* : REAL_ARITH *)=
  28.132 +structure RealArith : REAL_ARITH =
  28.133  struct
  28.134  
  28.135 - open Conv Thm;;
  28.136 + open Conv Thm FuncUtil;;
  28.137  (* ------------------------------------------------------------------------- *)
  28.138  (* Data structure for Positivstellensatz refutations.                        *)
  28.139  (* ------------------------------------------------------------------------- *)
  28.140 @@ -142,12 +177,18 @@
  28.141   | Rational_eq of Rat.rat
  28.142   | Rational_le of Rat.rat
  28.143   | Rational_lt of Rat.rat
  28.144 - | Square of cterm
  28.145 - | Eqmul of cterm * positivstellensatz
  28.146 + | Square of FuncUtil.poly
  28.147 + | Eqmul of FuncUtil.poly * positivstellensatz
  28.148   | Sum of positivstellensatz * positivstellensatz
  28.149   | Product of positivstellensatz * positivstellensatz;
  28.150           (* Theorems used in the procedure *)
  28.151  
  28.152 +datatype pss_tree = Trivial | Cert of positivstellensatz | Branch of pss_tree * pss_tree
  28.153 +datatype tree_choice = Left | Right
  28.154 +type prover = tree_choice list -> 
  28.155 +  (thm list * thm list * thm list -> positivstellensatz -> thm) ->
  28.156 +  thm list * thm list * thm list -> thm * pss_tree
  28.157 +type cert_conv = cterm -> thm * pss_tree
  28.158  
  28.159  val my_eqs = ref ([] : thm list);
  28.160  val my_les = ref ([] : thm list);
  28.161 @@ -164,6 +205,16 @@
  28.162  val my_poly_add_conv = ref no_conv;
  28.163  val my_poly_mul_conv = ref no_conv;
  28.164  
  28.165 +
  28.166 +    (* Some useful derived rules *)
  28.167 +fun deduct_antisym_rule tha thb = 
  28.168 +    equal_intr (implies_intr (cprop_of thb) tha) 
  28.169 +     (implies_intr (cprop_of tha) thb);
  28.170 +
  28.171 +fun prove_hyp tha thb = 
  28.172 +  if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
  28.173 +  then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb;
  28.174 +
  28.175  fun conjunctions th = case try Conjunction.elim th of
  28.176     SOME (th1,th2) => (conjunctions th1) @ conjunctions th2
  28.177   | NONE => [th];
  28.178 @@ -292,7 +343,6 @@
  28.179   | Abs (_,_,t') => find_cterm p (Thm.dest_abs NONE t |> snd)
  28.180   | _ => raise CTERM ("find_cterm",[t]);
  28.181  
  28.182 -
  28.183      (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
  28.184  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
  28.185  fun is_comb t = case (term_of t) of _$_ => true | _ => false;
  28.186 @@ -300,6 +350,39 @@
  28.187  fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
  28.188    handle CTERM _ => false;
  28.189  
  28.190 +
  28.191 +(* Map back polynomials to HOL.                         *)
  28.192 +
  28.193 +local
  28.194 + open Thm Numeral
  28.195 +in
  28.196 +
  28.197 +fun cterm_of_varpow x k = if k = 1 then x else capply (capply @{cterm "op ^ :: real => _"} x) 
  28.198 +  (mk_cnumber @{ctyp nat} k)
  28.199 +
  28.200 +fun cterm_of_monomial m = 
  28.201 + if Ctermfunc.is_undefined m then @{cterm "1::real"} 
  28.202 + else 
  28.203 +  let 
  28.204 +   val m' = dest_monomial m
  28.205 +   val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' [] 
  28.206 +  in foldr1 (fn (s, t) => capply (capply @{cterm "op * :: real => _"} s) t) vps
  28.207 +  end
  28.208 +
  28.209 +fun cterm_of_cmonomial (m,c) = if Ctermfunc.is_undefined m then cterm_of_rat c
  28.210 +    else if c = Rat.one then cterm_of_monomial m
  28.211 +    else capply (capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
  28.212 +
  28.213 +fun cterm_of_poly p = 
  28.214 + if Monomialfunc.is_undefined p then @{cterm "0::real"} 
  28.215 + else
  28.216 +  let 
  28.217 +   val cms = map cterm_of_cmonomial
  28.218 +     (sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p))
  28.219 +  in foldr1 (fn (t1, t2) => capply(capply @{cterm "op + :: real => _"} t1) t2) cms
  28.220 +  end;
  28.221 +
  28.222 +end;
  28.223      (* A general real arithmetic prover *)
  28.224  
  28.225  fun gen_gen_real_arith ctxt (mk_numeric,
  28.226 @@ -368,8 +451,8 @@
  28.227        | Rational_lt x => eqT_elim(numeric_gt_conv(capply @{cterm Trueprop} 
  28.228                        (capply (capply @{cterm "op <::real => _"} @{cterm "0::real"})
  28.229                          (mk_numeric x))))
  28.230 -      | Square t => square_rule t
  28.231 -      | Eqmul(t,p) => emul_rule t (translate p)
  28.232 +      | Square pt => square_rule (cterm_of_poly pt)
  28.233 +      | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
  28.234        | Sum(p1,p2) => add_rule (translate p1) (translate p2)
  28.235        | Product(p1,p2) => mul_rule (translate p1) (translate p2)
  28.236     in fconv_rule (first_conv [numeric_ge_conv, numeric_gt_conv, numeric_eq_conv, all_conv]) 
  28.237 @@ -394,13 +477,13 @@
  28.238         val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
  28.239     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)
  28.240     end
  28.241 - fun overall dun ths = case ths of
  28.242 + fun overall cert_choice dun ths = case ths of
  28.243    [] =>
  28.244     let 
  28.245      val (eq,ne) = List.partition (is_req o concl) dun
  28.246       val (le,nl) = List.partition (is_ge o concl) ne
  28.247       val lt = filter (is_gt o concl) nl 
  28.248 -    in prover hol_of_positivstellensatz (eq,le,lt) end
  28.249 +    in prover (rev cert_choice) hol_of_positivstellensatz (eq,le,lt) end
  28.250   | th::oths =>
  28.251     let 
  28.252      val ct = concl th 
  28.253 @@ -408,13 +491,13 @@
  28.254      if is_conj ct  then
  28.255       let 
  28.256        val (th1,th2) = conj_pair th in
  28.257 -      overall dun (th1::th2::oths) end
  28.258 +      overall cert_choice dun (th1::th2::oths) end
  28.259      else if is_disj ct then
  28.260        let 
  28.261 -       val th1 = overall dun (assume (capply @{cterm Trueprop} (dest_arg1 ct))::oths)
  28.262 -       val th2 = overall dun (assume (capply @{cterm Trueprop} (dest_arg ct))::oths)
  28.263 -      in disj_cases th th1 th2 end
  28.264 -   else overall (th::dun) oths
  28.265 +       val (th1, cert1) = overall (Left::cert_choice) dun (assume (capply @{cterm Trueprop} (dest_arg1 ct))::oths)
  28.266 +       val (th2, cert2) = overall (Right::cert_choice) dun (assume (capply @{cterm Trueprop} (dest_arg ct))::oths)
  28.267 +      in (disj_cases th th1 th2, Branch (cert1, cert2)) end
  28.268 +   else overall cert_choice (th::dun) oths
  28.269    end
  28.270    fun dest_binary b ct = if is_binop b ct then dest_binop ct 
  28.271                           else raise CTERM ("dest_binary",[b,ct])
  28.272 @@ -496,16 +579,16 @@
  28.273    val nct = capply @{cterm Trueprop} (capply @{cterm "Not"} ct)
  28.274    val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
  28.275    val tm0 = dest_arg (rhs_of th0)
  28.276 -  val th = if tm0 aconvc @{cterm False} then equal_implies_1_rule th0 else
  28.277 +  val (th, certificates) = if tm0 aconvc @{cterm False} then (equal_implies_1_rule th0, Trivial) else
  28.278     let 
  28.279      val (evs,bod) = strip_exists tm0
  28.280      val (avs,ibod) = strip_forall bod
  28.281      val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
  28.282 -    val th2 = overall [] [specl avs (assume (rhs_of th1))]
  28.283 +    val (th2, certs) = overall [] [] [specl avs (assume (rhs_of th1))]
  28.284      val th3 = fold simple_choose evs (prove_hyp (equal_elim th1 (assume (capply @{cterm Trueprop} bod))) th2)
  28.285 -   in  Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3)
  28.286 +   in (Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3), certs)
  28.287     end
  28.288 -  in implies_elim (instantiate' [] [SOME ct] pth_final) th
  28.289 +  in (implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
  28.290   end
  28.291  in f
  28.292  end;
  28.293 @@ -580,7 +663,7 @@
  28.294           val k = (Rat.neg d) */ Rat.abs c // c
  28.295           val e' = linear_cmul k e
  28.296           val t' = linear_cmul (Rat.abs c) t
  28.297 -         val p' = Eqmul(cterm_of_rat k,p)
  28.298 +         val p' = Eqmul(Monomialfunc.onefunc (Ctermfunc.undefined, k),p)
  28.299           val q' = Product(Rational_lt(Rat.abs c),q) 
  28.300          in (linear_add e' t',Sum(p',q')) 
  28.301          end 
  28.302 @@ -632,7 +715,7 @@
  28.303    val le_pols' = le_pols @ map (fn v => Ctermfunc.onefunc (v,Rat.one)) aliens
  28.304    val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
  28.305    val le' = le @ map (fn a => instantiate' [] [SOME (dest_arg a)] @{thm real_of_nat_ge_zero}) aliens 
  28.306 - in (translator (eq,le',lt) proof) : thm
  28.307 + in ((translator (eq,le',lt) proof), Trivial)
  28.308   end
  28.309  end;
  28.310  
  28.311 @@ -698,5 +781,4 @@
  28.312      main,neg,add,mul, prover)
  28.313  end;
  28.314  
  28.315 -fun real_arith ctxt = gen_prover_real_arith ctxt real_linear_prover;
  28.316  end
    29.1 --- a/src/HOL/Lim.thy	Wed Sep 23 19:17:48 2009 +1000
    29.2 +++ b/src/HOL/Lim.thy	Thu Sep 24 11:33:05 2009 +1000
    29.3 @@ -84,6 +84,8 @@
    29.4  lemma LIM_const [simp]: "(%x. k) -- x --> k"
    29.5  by (simp add: LIM_def)
    29.6  
    29.7 +lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
    29.8 +
    29.9  lemma LIM_add:
   29.10    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   29.11    assumes f: "f -- a --> L" and g: "g -- a --> M"
   29.12 @@ -544,7 +546,7 @@
   29.13      case True thus ?thesis using `0 < s` by auto
   29.14    next
   29.15      case False hence "s / 2 \<ge> (x - b) / 2" by auto
   29.16 -    hence "?x = (x + b) / 2" by(simp add:field_simps)
   29.17 +    hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
   29.18      thus ?thesis using `b < x` by auto
   29.19    qed
   29.20    hence "0 \<le> f ?x" using all_le `?x < x` by auto
    30.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Wed Sep 23 19:17:48 2009 +1000
    30.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Thu Sep 24 11:33:05 2009 +1000
    30.3 @@ -1,5 +1,4 @@
    30.4  (*  Title:      HOL/MicroJava/BV/Effect.thy
    30.5 -    ID:         $Id$
    30.6      Author:     Gerwin Klein
    30.7      Copyright   2000 Technische Universitaet Muenchen
    30.8  *)
    30.9 @@ -391,7 +390,7 @@
   30.10    with Pair 
   30.11    have "?app s \<Longrightarrow> ?P s" by (simp only:)
   30.12    moreover
   30.13 -  have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp)
   30.14 +  have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min_max.inf_absorb2)
   30.15    ultimately
   30.16    show ?thesis by (rule iffI) 
   30.17  qed 
    31.1 --- a/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Sep 23 19:17:48 2009 +1000
    31.2 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Sep 24 11:33:05 2009 +1000
    31.3 @@ -1,5 +1,4 @@
    31.4  (*  Title:      HOL/MicroJava/BV/LBVSpec.thy
    31.5 -    ID:         $Id$
    31.6      Author:     Gerwin Klein
    31.7      Copyright   1999 Technische Universitaet Muenchen
    31.8  *)
    31.9 @@ -293,7 +292,7 @@
   31.10    shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
   31.11  proof -
   31.12    from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
   31.13 -  with suc wtl show ?thesis by (simp)
   31.14 +  with suc wtl show ?thesis by (simp add: min_max.inf_absorb2)
   31.15  qed
   31.16  
   31.17  lemma (in lbv) wtl_all:
   31.18 @@ -308,7 +307,7 @@
   31.19    with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp 
   31.20    from pc have "is!pc = drop pc is ! 0" by simp
   31.21    with Cons have "is!pc = i" by simp
   31.22 -  with take pc show ?thesis by (auto)
   31.23 +  with take pc show ?thesis by (auto simp add: min_max.inf_absorb2)
   31.24  qed
   31.25  
   31.26  section "preserves-type"
    32.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Sep 23 19:17:48 2009 +1000
    32.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Sep 24 11:33:05 2009 +1000
    32.3 @@ -1,5 +1,4 @@
    32.4  (*  Title:      HOL/MicroJava/Comp/CorrCompTp.thy
    32.5 -    ID:         $Id$
    32.6      Author:     Martin Strecker
    32.7  *)
    32.8  
    32.9 @@ -1058,7 +1057,7 @@
   32.10  lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
   32.11    \<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
   32.12  apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   32.13 -    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   32.14 +    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   32.15  apply (intro strip)
   32.16  apply (rule conjI)
   32.17  apply (rule check_type_mono, assumption, simp)
   32.18 @@ -1069,7 +1068,7 @@
   32.19    bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   32.20    apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   32.21    apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) 
   32.22 -  apply (simp add: check_type_simps)
   32.23 +  apply (simp add: check_type_simps min_max.sup_absorb1)
   32.24    apply clarify
   32.25    apply (rule_tac x="(length ST)" in exI)
   32.26    apply simp+
   32.27 @@ -1092,7 +1091,7 @@
   32.28    \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
   32.29  apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   32.30    apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   32.31 -              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   32.32 +              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   32.33    apply (intro strip)
   32.34    apply (rule conjI)
   32.35    apply (rule check_type_mono, assumption, simp)
   32.36 @@ -1111,7 +1110,7 @@
   32.37    \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
   32.38  apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   32.39    apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   32.40 -              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   32.41 +              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   32.42    apply (intro strip)
   32.43    apply (rule conjI)
   32.44    apply (rule check_type_mono, assumption, simp)
   32.45 @@ -1127,7 +1126,7 @@
   32.46    \<Longrightarrow> bc_mt_corresp [Load i] 
   32.47           (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
   32.48  apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   32.49 -            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   32.50 +            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   32.51    apply (intro strip)
   32.52    apply (rule conjI)
   32.53    apply (rule check_type_mono, assumption, simp)
   32.54 @@ -1148,10 +1147,10 @@
   32.55  lemma bc_mt_corresp_Store_init: "\<lbrakk> i < length LT \<rbrakk>
   32.56    \<Longrightarrow> bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
   32.57   apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
   32.58 -  apply (simp add: max_ssize_def  max_of_list_def )
   32.59 +  apply (simp add: max_ssize_def  max_of_list_def)
   32.60    apply (simp add: ssize_sto_def)
   32.61    apply (intro strip)
   32.62 -apply (simp add: check_type_simps)
   32.63 +apply (simp add: check_type_simps min_max.sup_absorb1)
   32.64  apply clarify
   32.65  apply (rule conjI)
   32.66  apply (rule_tac x="(length ST)" in exI)
   32.67 @@ -1159,14 +1158,13 @@
   32.68  done
   32.69  
   32.70  
   32.71 -
   32.72  lemma bc_mt_corresp_Store: "\<lbrakk> i < length LT; cG  \<turnstile>  LT[i := OK T] <=l LT \<rbrakk>
   32.73    \<Longrightarrow> bc_mt_corresp [Store i] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   32.74    apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   32.75    apply (simp add: sup_state_conv)
   32.76    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
   32.77   apply (intro strip)
   32.78 -apply (simp add: check_type_simps)
   32.79 +apply (simp add: check_type_simps min_max.sup_absorb1)
   32.80  apply clarify
   32.81  apply (rule_tac x="(length ST)" in exI)
   32.82  apply simp+
   32.83 @@ -1176,7 +1174,7 @@
   32.84  lemma bc_mt_corresp_Dup: "
   32.85    bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
   32.86   apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
   32.87 -             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   32.88 +             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   32.89    apply (intro strip)
   32.90    apply (rule conjI)
   32.91    apply (rule check_type_mono, assumption, simp)
   32.92 @@ -1189,7 +1187,7 @@
   32.93  lemma bc_mt_corresp_Dup_x1: "
   32.94    bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
   32.95    apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
   32.96 -              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   32.97 +              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   32.98    apply (intro strip)
   32.99    apply (rule conjI)
  32.100    apply (rule check_type_mono, assumption, simp)
  32.101 @@ -1206,7 +1204,7 @@
  32.102           (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
  32.103    apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
  32.104    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  32.105 -  apply (simp add: check_type_simps)
  32.106 +  apply (simp add: check_type_simps min_max.sup_absorb1)
  32.107    apply clarify
  32.108    apply (rule_tac x="Suc (length ST)" in exI)
  32.109    apply simp+
  32.110 @@ -1249,7 +1247,7 @@
  32.111    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  32.112  
  32.113    apply (intro strip)
  32.114 -apply (simp add: check_type_simps)
  32.115 +apply (simp add: check_type_simps min_max.sup_absorb1)
  32.116  apply clarify
  32.117  apply (rule_tac x="Suc (length ST)" in exI)
  32.118  apply simp+
    33.1 --- a/src/HOL/OrderedGroup.thy	Wed Sep 23 19:17:48 2009 +1000
    33.2 +++ b/src/HOL/OrderedGroup.thy	Thu Sep 24 11:33:05 2009 +1000
    33.3 @@ -1075,17 +1075,16 @@
    33.4  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
    33.5  
    33.6  lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
    33.7 -by (simp add: pprt_def sup_aci)
    33.8 -
    33.9 +  by (simp add: pprt_def sup_aci sup_absorb1)
   33.10  
   33.11  lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
   33.12 -by (simp add: nprt_def inf_aci)
   33.13 +  by (simp add: nprt_def inf_aci inf_absorb1)
   33.14  
   33.15  lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
   33.16 -by (simp add: pprt_def sup_aci)
   33.17 +  by (simp add: pprt_def sup_aci sup_absorb2)
   33.18  
   33.19  lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
   33.20 -by (simp add: nprt_def inf_aci)
   33.21 +  by (simp add: nprt_def inf_aci inf_absorb2)
   33.22  
   33.23  lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
   33.24  proof -
   33.25 @@ -1119,7 +1118,7 @@
   33.26    "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   33.27  proof
   33.28    assume "0 <= a + a"
   33.29 -  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute)
   33.30 +  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1)
   33.31    have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
   33.32      by (simp add: add_sup_inf_distribs inf_aci)
   33.33    hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
   33.34 @@ -1135,7 +1134,7 @@
   33.35    assume assm: "a + a = 0"
   33.36    then have "a + a + - a = - a" by simp
   33.37    then have "a + (a + - a) = - a" by (simp only: add_assoc)
   33.38 -  then have a: "- a = a" by simp (*FIXME tune proof*)
   33.39 +  then have a: "- a = a" by simp
   33.40    show "a = 0" apply (rule antisym)
   33.41    apply (unfold neg_le_iff_le [symmetric, of a])
   33.42    unfolding a apply simp
   33.43 @@ -1275,7 +1274,7 @@
   33.44  proof -
   33.45    note add_le_cancel_right [of a a "- a", symmetric, simplified]
   33.46    moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
   33.47 -  then show ?thesis by (auto simp: sup_max)
   33.48 +  then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2)
   33.49  qed
   33.50  
   33.51  lemma abs_if_lattice:
    34.1 --- a/src/HOL/Quickcheck.thy	Wed Sep 23 19:17:48 2009 +1000
    34.2 +++ b/src/HOL/Quickcheck.thy	Thu Sep 24 11:33:05 2009 +1000
    34.3 @@ -3,7 +3,7 @@
    34.4  header {* A simple counterexample generator *}
    34.5  
    34.6  theory Quickcheck
    34.7 -imports Random Code_Eval
    34.8 +imports Random Code_Evaluation
    34.9  uses ("Tools/quickcheck_generators.ML")
   34.10  begin
   34.11  
   34.12 @@ -24,7 +24,7 @@
   34.13  
   34.14  definition
   34.15    "random i = Random.range 2 o\<rightarrow>
   34.16 -    (\<lambda>k. Pair (if k = 0 then Code_Eval.valtermify False else Code_Eval.valtermify True))"
   34.17 +    (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
   34.18  
   34.19  instance ..
   34.20  
   34.21 @@ -34,7 +34,7 @@
   34.22  begin
   34.23  
   34.24  definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   34.25 -  "random_itself _ = Pair (Code_Eval.valtermify TYPE('a))"
   34.26 +  "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
   34.27  
   34.28  instance ..
   34.29  
   34.30 @@ -44,7 +44,7 @@
   34.31  begin
   34.32  
   34.33  definition
   34.34 -  "random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Eval.term_of c))"
   34.35 +  "random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
   34.36  
   34.37  instance ..
   34.38  
   34.39 @@ -54,7 +54,7 @@
   34.40  begin
   34.41  
   34.42  definition 
   34.43 -  "random _ = Pair (STR '''', \<lambda>u. Code_Eval.term_of (STR ''''))"
   34.44 +  "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
   34.45  
   34.46  instance ..
   34.47  
   34.48 @@ -63,10 +63,10 @@
   34.49  instantiation nat :: random
   34.50  begin
   34.51  
   34.52 -definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
   34.53 +definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
   34.54    "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
   34.55       let n = Code_Numeral.nat_of k
   34.56 -     in (n, \<lambda>_. Code_Eval.term_of n)))"
   34.57 +     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
   34.58  
   34.59  instance ..
   34.60  
   34.61 @@ -78,7 +78,7 @@
   34.62  definition
   34.63    "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
   34.64       let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
   34.65 -     in (j, \<lambda>_. Code_Eval.term_of j)))"
   34.66 +     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
   34.67  
   34.68  instance ..
   34.69  
   34.70 @@ -95,7 +95,7 @@
   34.71  
   34.72  definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
   34.73    \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   34.74 -  "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed"
   34.75 +  "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
   34.76  
   34.77  instantiation "fun" :: ("{eq, term_of}", random) random
   34.78  begin
    35.1 --- a/src/HOL/Rational.thy	Wed Sep 23 19:17:48 2009 +1000
    35.2 +++ b/src/HOL/Rational.thy	Thu Sep 24 11:33:05 2009 +1000
    35.3 @@ -1002,8 +1002,8 @@
    35.4    by simp
    35.5  
    35.6  definition (in term_syntax)
    35.7 -  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
    35.8 -  [code_unfold]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
    35.9 +  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
   35.10 +  [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
   35.11  
   35.12  notation fcomp (infixl "o>" 60)
   35.13  notation scomp (infixl "o\<rightarrow>" 60)
   35.14 @@ -1014,7 +1014,7 @@
   35.15  definition
   35.16    "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
   35.17       let j = Code_Numeral.int_of (denom + 1)
   35.18 -     in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
   35.19 +     in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
   35.20  
   35.21  instance ..
   35.22  
    36.1 --- a/src/HOL/RealDef.thy	Wed Sep 23 19:17:48 2009 +1000
    36.2 +++ b/src/HOL/RealDef.thy	Thu Sep 24 11:33:05 2009 +1000
    36.3 @@ -1128,8 +1128,8 @@
    36.4    by (simp add: of_rat_divide)
    36.5  
    36.6  definition (in term_syntax)
    36.7 -  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
    36.8 -  [code_unfold]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
    36.9 +  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   36.10 +  [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
   36.11  
   36.12  notation fcomp (infixl "o>" 60)
   36.13  notation scomp (infixl "o\<rightarrow>" 60)
    38.1 --- a/src/HOL/Tools/hologic.ML	Wed Sep 23 19:17:48 2009 +1000
    38.2 +++ b/src/HOL/Tools/hologic.ML	Thu Sep 24 11:33:05 2009 +1000
    38.3 @@ -613,17 +613,17 @@
    38.4    | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep",
    38.5        Term.itselfT T --> typerepT) $ Logic.mk_type T;
    38.6  
    38.7 -val termT = Type ("Code_Eval.term", []);
    38.8 +val termT = Type ("Code_Evaluation.term", []);
    38.9  
   38.10 -fun term_of_const T = Const ("Code_Eval.term_of_class.term_of", T --> termT);
   38.11 +fun term_of_const T = Const ("Code_Evaluation.term_of_class.term_of", T --> termT);
   38.12  
   38.13  fun mk_term_of T t = term_of_const T $ t;
   38.14  
   38.15  fun reflect_term (Const (c, T)) =
   38.16 -      Const ("Code_Eval.Const", literalT --> typerepT --> termT)
   38.17 +      Const ("Code_Evaluation.Const", literalT --> typerepT --> termT)
   38.18          $ mk_literal c $ mk_typerep T
   38.19    | reflect_term (t1 $ t2) =
   38.20 -      Const ("Code_Eval.App", termT --> termT --> termT)
   38.21 +      Const ("Code_Evaluation.App", termT --> termT --> termT)
   38.22          $ reflect_term t1 $ reflect_term t2
   38.23    | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
   38.24    | reflect_term t = t;
   38.25 @@ -631,7 +631,7 @@
   38.26  fun mk_valtermify_app c vs T =
   38.27    let
   38.28      fun termifyT T = mk_prodT (T, unitT --> termT);
   38.29 -    fun valapp T T' = Const ("Code_Eval.valapp",
   38.30 +    fun valapp T T' = Const ("Code_Evaluation.valapp",
   38.31        termifyT (T --> T') --> termifyT T --> termifyT T');
   38.32      fun mk_fTs [] _ = []
   38.33        | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T;
    39.1 --- a/src/HOL/Tools/inductive.ML	Wed Sep 23 19:17:48 2009 +1000
    39.2 +++ b/src/HOL/Tools/inductive.ML	Thu Sep 24 11:33:05 2009 +1000
    39.3 @@ -103,7 +103,10 @@
    39.4        "(P & True) = P" "(True & P) = P"
    39.5      by (fact simp_thms)+};
    39.6  
    39.7 -val simp_thms'' = inf_fun_eq :: inf_bool_eq :: simp_thms';
    39.8 +val simp_thms'' = map mk_meta_eq [@{thm inf_fun_eq}, @{thm inf_bool_eq}] @ simp_thms';
    39.9 +
   39.10 +val simp_thms''' = map mk_meta_eq
   39.11 +  [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_eq}, @{thm sup_bool_eq}];
   39.12  
   39.13  
   39.14  (** context data **)
   39.15 @@ -171,15 +174,15 @@
   39.16        (case concl of
   39.17            (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
   39.18          | _ => [thm' RS (thm' RS eq_to_mono2)]);
   39.19 -    fun dest_less_concl thm = dest_less_concl (thm RS le_funD)
   39.20 -      handle THM _ => thm RS le_boolD
   39.21 +    fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
   39.22 +      handle THM _ => thm RS @{thm le_boolD}
   39.23    in
   39.24      case concl of
   39.25        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
   39.26      | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
   39.27      | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
   39.28        [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   39.29 -         (resolve_tac [le_funI, le_boolI'])) thm))]
   39.30 +         (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))]
   39.31      | _ => [thm]
   39.32    end handle THM _ =>
   39.33      error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
   39.34 @@ -323,11 +326,11 @@
   39.35      (HOLogic.mk_Trueprop
   39.36        (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
   39.37      (fn _ => EVERY [rtac @{thm monoI} 1,
   39.38 -      REPEAT (resolve_tac [le_funI, le_boolI'] 1),
   39.39 +      REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
   39.40        REPEAT (FIRST
   39.41          [atac 1,
   39.42           resolve_tac (List.concat (map mk_mono monos) @ get_monos ctxt) 1,
   39.43 -         etac le_funE 1, dtac le_boolD 1])]));
   39.44 +         etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
   39.45  
   39.46  
   39.47  (* prove introduction rules *)
   39.48 @@ -338,7 +341,7 @@
   39.49  
   39.50      val unfold = funpow k (fn th => th RS fun_cong)
   39.51        (mono RS (fp_def RS
   39.52 -        (if coind then def_gfp_unfold else def_lfp_unfold)));
   39.53 +        (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
   39.54  
   39.55      fun select_disj 1 1 = []
   39.56        | select_disj _ 1 = [rtac disjI1]
   39.57 @@ -553,13 +556,13 @@
   39.58      val ind_concl = HOLogic.mk_Trueprop
   39.59        (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
   39.60  
   39.61 -    val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
   39.62 +    val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
   39.63  
   39.64      val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl
   39.65        (fn {prems, ...} => EVERY
   39.66          [rewrite_goals_tac [inductive_conj_def],
   39.67           DETERM (rtac raw_fp_induct 1),
   39.68 -         REPEAT (resolve_tac [le_funI, le_boolI] 1),
   39.69 +         REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
   39.70           rewrite_goals_tac simp_thms'',
   39.71           (*This disjE separates out the introduction rules*)
   39.72           REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
   39.73 @@ -577,7 +580,7 @@
   39.74          [rewrite_goals_tac rec_preds_defs,
   39.75           REPEAT (EVERY
   39.76             [REPEAT (resolve_tac [conjI, impI] 1),
   39.77 -            REPEAT (eresolve_tac [le_funE, le_boolE] 1),
   39.78 +            REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
   39.79              atac 1,
   39.80              rewrite_goals_tac simp_thms',
   39.81              atac 1])])
   39.82 @@ -763,8 +766,8 @@
   39.83             (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
   39.84             (rotate_prems ~1 (ObjectLogic.rulify
   39.85               (fold_rule rec_preds_defs
   39.86 -               (rewrite_rule [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq]
   39.87 -                (mono RS (fp_def RS def_coinduct))))))
   39.88 +               (rewrite_rule simp_thms'''
   39.89 +                (mono RS (fp_def RS @{thm def_coinduct}))))))
   39.90         else
   39.91           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
   39.92             rec_preds_defs ctxt1);
    40.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Wed Sep 23 19:17:48 2009 +1000
    40.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 24 11:33:05 2009 +1000
    40.3 @@ -76,7 +76,7 @@
    40.4      val lhs = HOLogic.mk_random T size;
    40.5      val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))]
    40.6        (HOLogic.mk_return Tm @{typ Random.seed}
    40.7 -      (mk_const "Code_Eval.valapp" [T', T]
    40.8 +      (mk_const "Code_Evaluation.valapp" [T', T]
    40.9          $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
   40.10        @{typ Random.seed} (SOME Tm, @{typ Random.seed});
   40.11      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    41.1 --- a/src/HOL/UNITY/Simple/Common.thy	Wed Sep 23 19:17:48 2009 +1000
    41.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Thu Sep 24 11:33:05 2009 +1000
    41.3 @@ -1,5 +1,4 @@
    41.4  (*  Title:      HOL/UNITY/Common
    41.5 -    ID:         $Id$
    41.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    41.7      Copyright   1998  University of Cambridge
    41.8  
    41.9 @@ -10,7 +9,9 @@
   41.10  From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
   41.11  *)
   41.12  
   41.13 -theory Common imports "../UNITY_Main" begin
   41.14 +theory Common
   41.15 +imports "../UNITY_Main"
   41.16 +begin
   41.17  
   41.18  consts
   41.19    ftime :: "nat=>nat"
   41.20 @@ -65,7 +66,7 @@
   41.21  lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
   41.22         \<in> {m} co (maxfg m)"
   41.23  apply (simp add: mk_total_program_def) 
   41.24 -apply (simp add: constrains_def maxfg_def gasc)
   41.25 +apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
   41.26  done
   41.27  
   41.28  (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
   41.29 @@ -73,7 +74,7 @@
   41.30            (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
   41.31         \<in> {m} co (maxfg m)"
   41.32  apply (simp add: mk_total_program_def) 
   41.33 -apply (simp add: constrains_def maxfg_def gasc)
   41.34 +apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
   41.35  done
   41.36  
   41.37  
    42.1 --- a/src/HOL/Word/BinBoolList.thy	Wed Sep 23 19:17:48 2009 +1000
    42.2 +++ b/src/HOL/Word/BinBoolList.thy	Thu Sep 24 11:33:05 2009 +1000
    42.3 @@ -919,7 +919,7 @@
    42.4    apply (drule spec)
    42.5    apply (erule trans)
    42.6    apply (drule_tac x = "bin_cat y n a" in spec)
    42.7 -  apply (simp add : bin_cat_assoc_sym)
    42.8 +  apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
    42.9    done
   42.10  
   42.11  lemma bin_rcat_bl:
    43.1 --- a/src/HOL/Word/BinGeneral.thy	Wed Sep 23 19:17:48 2009 +1000
    43.2 +++ b/src/HOL/Word/BinGeneral.thy	Thu Sep 24 11:33:05 2009 +1000
    43.3 @@ -508,7 +508,7 @@
    43.4  lemma sbintrunc_sbintrunc_min [simp]:
    43.5    "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
    43.6    apply (rule bin_eqI)
    43.7 -  apply (auto simp: nth_sbintr)
    43.8 +  apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2)
    43.9    done
   43.10  
   43.11  lemmas bintrunc_Pls = 
    44.1 --- a/src/HOL/Word/WordDefinition.thy	Wed Sep 23 19:17:48 2009 +1000
    44.2 +++ b/src/HOL/Word/WordDefinition.thy	Thu Sep 24 11:33:05 2009 +1000
    44.3 @@ -381,14 +381,14 @@
    44.4    apply (unfold word_size)
    44.5    apply (subst word_ubin.norm_Rep [symmetric]) 
    44.6    apply (simp only: bintrunc_bintrunc_min word_size)
    44.7 -  apply simp
    44.8 +  apply (simp add: min_max.inf_absorb2)
    44.9    done
   44.10  
   44.11  lemma wi_bintr': 
   44.12    "wb = word_of_int bin ==> n >= size wb ==> 
   44.13      word_of_int (bintrunc n bin) = wb"
   44.14    unfolding word_size
   44.15 -  by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric])
   44.16 +  by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
   44.17  
   44.18  lemmas bintr_uint = bintr_uint' [unfolded word_size]
   44.19  lemmas wi_bintr = wi_bintr' [unfolded word_size]
    45.1 --- a/src/HOL/Word/WordShift.thy	Wed Sep 23 19:17:48 2009 +1000
    45.2 +++ b/src/HOL/Word/WordShift.thy	Thu Sep 24 11:33:05 2009 +1000
    45.3 @@ -1017,8 +1017,8 @@
    45.4    (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
    45.5    word_of_int (bin_cat w (size b) (uint b))"
    45.6    apply (unfold word_cat_def word_size) 
    45.7 -  apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
    45.8 -      word_ubin.eq_norm bintr_cat)
    45.9 +  apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
   45.10 +      word_ubin.eq_norm bintr_cat min_max.inf_absorb1)
   45.11    done
   45.12  
   45.13  lemma word_cat_split_alt:
    46.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Sep 23 19:17:48 2009 +1000
    46.2 +++ b/src/HOL/ex/predicate_compile.ML	Thu Sep 24 11:33:05 2009 +1000
    46.3 @@ -169,7 +169,7 @@
    46.4    end;
    46.5  
    46.6  fun dest_randomT (Type ("fun", [@{typ Random.seed},
    46.7 -  Type ("*", [Type ("*", [T, @{typ "unit => Code_Eval.term"}]) ,@{typ Random.seed}])])) = T
    46.8 +  Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
    46.9    | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
   46.10  
   46.11  (* destruction of intro rules *)
   46.12 @@ -707,7 +707,7 @@
   46.13  end;
   46.14  
   46.15  (* termify_code:
   46.16 -val termT = Type ("Code_Eval.term", []);
   46.17 +val termT = Type ("Code_Evaluation.term", []);
   46.18  fun termifyT T = HOLogic.mk_prodT (T, HOLogic.unitT --> termT)
   46.19  *)
   46.20  (*
   46.21 @@ -1198,7 +1198,7 @@
   46.22        val t1' = mk_valtermify_term t1
   46.23        val t2' = mk_valtermify_term t2
   46.24      in
   46.25 -      Const ("Code_Eval.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
   46.26 +      Const ("Code_Evaluation.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
   46.27      end
   46.28    | mk_valtermify_term _ = error "Not a valid term for mk_valtermify_term"
   46.29  *)
    47.1 --- a/src/Pure/Concurrent/future.ML	Wed Sep 23 19:17:48 2009 +1000
    47.2 +++ b/src/Pure/Concurrent/future.ML	Thu Sep 24 11:33:05 2009 +1000
    47.3 @@ -257,7 +257,7 @@
    47.4                "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads")));
    47.5  
    47.6      val m = if ! do_shutdown then 0 else Multithreading.max_threads_value ();
    47.7 -    val mm = if m = 9999 then 1 else (m * 3) div 2;
    47.8 +    val mm = if m = 9999 then 1 else m * 2;
    47.9      val l = length (! workers);
   47.10      val _ = excessive := l - mm;
   47.11      val _ =
    48.1 --- a/src/Pure/Isar/code.ML	Wed Sep 23 19:17:48 2009 +1000
    48.2 +++ b/src/Pure/Isar/code.ML	Thu Sep 24 11:33:05 2009 +1000
    48.3 @@ -505,9 +505,10 @@
    48.4  
    48.5  (*those following are permissive wrt. to overloaded constants!*)
    48.6  
    48.7 +val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
    48.8  fun const_typ_eqn thy thm =
    48.9    let
   48.10 -    val (c, ty) = (dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   48.11 +    val (c, ty) = head_eqn thm;
   48.12      val c' = AxClass.unoverload_const thy (c, ty);
   48.13    in (c', ty) end;
   48.14  
   48.15 @@ -523,8 +524,8 @@
   48.16  
   48.17  fun same_typscheme thy thms =
   48.18    let
   48.19 -    fun tvars_of t = rev (Term.add_tvars t []);
   48.20 -    val vss = map (tvars_of o Thm.prop_of) thms;
   48.21 +    fun tvars_of T = rev (Term.add_tvarsT T []);
   48.22 +    val vss = map (tvars_of o snd o head_eqn) thms;
   48.23      fun inter_sorts vs =
   48.24        fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
   48.25      val sorts = map_transpose inter_sorts vss;
   48.26 @@ -547,7 +548,7 @@
   48.27  fun case_certificate thm =
   48.28    let
   48.29      val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
   48.30 -      o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.prop_of) thm;
   48.31 +      o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm;
   48.32      val _ = case head of Free _ => true
   48.33        | Var _ => true
   48.34        | _ => raise TERM ("case_cert", []);
    49.1 --- a/src/Pure/envir.ML	Wed Sep 23 19:17:48 2009 +1000
    49.2 +++ b/src/Pure/envir.ML	Thu Sep 24 11:33:05 2009 +1000
    49.3 @@ -282,12 +282,9 @@
    49.4    let
    49.5      val funerr = "fastype: expected function type";
    49.6      fun fast Ts (f $ u) =
    49.7 -          (case fast Ts f of
    49.8 +          (case Type.devar tyenv (fast Ts f) of
    49.9              Type ("fun", [_, T]) => T
   49.10 -          | TVar v =>
   49.11 -              (case Type.lookup tyenv v of
   49.12 -                SOME (Type ("fun", [_, T])) => T
   49.13 -              | _ => raise TERM (funerr, [f $ u]))
   49.14 +          | TVar v => raise TERM (funerr, [f $ u])
   49.15            | _ => raise TERM (funerr, [f $ u]))
   49.16        | fast Ts (Const (_, T)) = T
   49.17        | fast Ts (Free (_, T)) = T
    50.1 --- a/src/Pure/type.ML	Wed Sep 23 19:17:48 2009 +1000
    50.2 +++ b/src/Pure/type.ML	Thu Sep 24 11:33:05 2009 +1000
    50.3 @@ -55,6 +55,7 @@
    50.4    exception TYPE_MATCH
    50.5    type tyenv = (sort * typ) Vartab.table
    50.6    val lookup: tyenv -> indexname * sort -> typ option
    50.7 +  val devar: tyenv -> typ -> typ
    50.8    val typ_match: tsig -> typ * typ -> tyenv -> tyenv
    50.9    val typ_instance: tsig -> typ * typ -> bool
   50.10    val raw_match: typ * typ -> tyenv -> tyenv