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