--- a/Admin/isatest/isatest-makedist Wed Sep 23 13:47:08 2009 +0200
+++ b/Admin/isatest/isatest-makedist Wed Sep 23 13:48:16 2009 +0200
@@ -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/src/HOL/Decision_Procs/Approximation.thy Wed Sep 23 13:47:08 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Sep 23 13:48:16 2009 +0200
@@ -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/ex/Approximation_Ex.thy Wed Sep 23 13:47:08 2009 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Wed Sep 23 13:48:16 2009 +0200
@@ -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/Inductive.thy Wed Sep 23 13:47:08 2009 +0200
+++ b/src/HOL/Inductive.thy Wed Sep 23 13:48:16 2009 +0200
@@ -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/Lim.thy Wed Sep 23 13:47:08 2009 +0200
+++ b/src/HOL/Lim.thy Wed Sep 23 13:48:16 2009 +0200
@@ -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"
--- a/src/HOL/Tools/inductive.ML Wed Sep 23 13:47:08 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Sep 23 13:48:16 2009 +0200
@@ -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/Pure/envir.ML Wed Sep 23 13:47:08 2009 +0200
+++ b/src/Pure/envir.ML Wed Sep 23 13:48:16 2009 +0200
@@ -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 13:47:08 2009 +0200
+++ b/src/Pure/type.ML Wed Sep 23 13:48:16 2009 +0200
@@ -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