# HG changeset patch # User blanchet # Date 1253706496 -7200 # Node ID 3bd9296b16acd57103b694d1c8736aa7e167493b # Parent dd84779cd191438e8de7ad40bc25ef0d201105cb# Parent 5f91274074304e24cfa6c89223078084875b6080 merged diff -r dd84779cd191 -r 3bd9296b16ac Admin/isatest/isatest-makedist --- 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 diff -r dd84779cd191 -r 3bd9296b16ac src/HOL/Decision_Procs/Approximation.thy --- 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"}, _)) $ diff -r dd84779cd191 -r 3bd9296b16ac src/HOL/Decision_Procs/ex/Approximation_Ex.thy --- 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) \ { 3 * d .. 3.1 * d }" using assms by (approximation 80) -lemma "\ \ { 0 .. 1 :: real } \ \ ^ 2 \ \" - by (approximation 30 splitting: \=1 taylor: \ = 3) +lemma "x \ { 0 .. 1 :: real } \ x ^ 2 \ x" + by (approximation 30 splitting: x=1 taylor: x = 3) + +value [approximate] "10" end diff -r dd84779cd191 -r 3bd9296b16ac src/HOL/Inductive.thy --- 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 diff -r dd84779cd191 -r 3bd9296b16ac src/HOL/Lim.thy --- 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: "\ f -- x --> L ; K = L \ \ f -- x --> K" by simp + lemma LIM_add: fixes f g :: "'a::metric_space \ 'b::real_normed_vector" assumes f: "f -- a --> L" and g: "g -- a --> M" diff -r dd84779cd191 -r 3bd9296b16ac src/HOL/Statespace/state_space.ML diff -r dd84779cd191 -r 3bd9296b16ac src/HOL/Tools/inductive.ML --- 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); diff -r dd84779cd191 -r 3bd9296b16ac src/Pure/envir.ML --- 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 diff -r dd84779cd191 -r 3bd9296b16ac src/Pure/type.ML --- 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