merged
authorblanchet
Wed Sep 23 13:48:16 2009 +0200 (2009-09-23)
changeset 326563bd9296b16ac
parent 32655 dd84779cd191
parent 32654 5f9127407430
child 32658 82956a3f0e0b
child 32659 ffe062d9ae95
merged
     1.1 --- a/Admin/isatest/isatest-makedist	Wed Sep 23 13:47:08 2009 +0200
     1.2 +++ b/Admin/isatest/isatest-makedist	Wed Sep 23 13:48:16 2009 +0200
     1.3 @@ -102,9 +102,9 @@
     1.4  #sleep 15
     1.5  $SSH macbroy21 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
     1.6  sleep 15
     1.7 -$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e"
     1.8 -sleep 15
     1.9 -$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly"
    1.10 +#$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e"
    1.11 +#sleep 15
    1.12 +$SSH atbroy99 "$MAKEALL $HOME/settings/at64-poly"
    1.13  sleep 15
    1.14  $SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8; $MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8"
    1.15  sleep 15
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 23 13:47:08 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 23 13:48:16 2009 +0200
     2.3 @@ -3246,12 +3246,13 @@
     2.4          = map (` (variable_of_bound o prop_of)) prems
     2.5  
     2.6        fun add_deps (name, bnds)
     2.7 -        = Graph.add_deps_acyclic
     2.8 -            (name, remove (op =) name (Term.add_free_names (prop_of bnds) []))
     2.9 +        = Graph.add_deps_acyclic (name,
    2.10 +            remove (op =) name (Term.add_free_names (prop_of bnds) []))
    2.11 +
    2.12        val order = Graph.empty
    2.13                    |> fold Graph.new_node variable_bounds
    2.14                    |> fold add_deps variable_bounds
    2.15 -                  |> Graph.topological_order |> rev
    2.16 +                  |> Graph.strong_conn |> map the_single |> rev
    2.17                    |> map_filter (AList.lookup (op =) variable_bounds)
    2.18  
    2.19        fun prepend_prem th tac
    2.20 @@ -3338,7 +3339,7 @@
    2.21                        etac @{thm meta_eqE},
    2.22                        rtac @{thm impI}] i)
    2.23        THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
    2.24 -      THEN TRY (filter_prems_tac (K false) i)
    2.25 +      THEN DETERM (TRY (filter_prems_tac (K false) i))
    2.26        THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
    2.27        THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
    2.28        THEN gen_eval_tac eval_oracle ctxt i))
    2.29 @@ -3350,7 +3351,7 @@
    2.30  
    2.31    fun mk_approx' prec t = (@{const "approx'"}
    2.32                           $ HOLogic.mk_number @{typ nat} prec
    2.33 -                         $ t $ @{term "[] :: (float * float) list"})
    2.34 +                         $ t $ @{term "[] :: (float * float) option list"})
    2.35  
    2.36    fun dest_result (Const (@{const_name "Some"}, _) $
    2.37                     ((Const (@{const_name "Pair"}, _)) $
     3.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Sep 23 13:47:08 2009 +0200
     3.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Sep 23 13:48:16 2009 +0200
     3.3 @@ -72,7 +72,9 @@
     3.4    shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
     3.5    using assms by (approximation 80)
     3.6  
     3.7 -lemma "\<phi> \<in> { 0 .. 1 :: real } \<longrightarrow> \<phi> ^ 2 \<le> \<phi>"
     3.8 -  by (approximation 30 splitting: \<phi>=1 taylor: \<phi> = 3)
     3.9 +lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x ^ 2 \<le> x"
    3.10 +  by (approximation 30 splitting: x=1 taylor: x = 3)
    3.11 +
    3.12 +value [approximate] "10"
    3.13  
    3.14  end
     4.1 --- a/src/HOL/Inductive.thy	Wed Sep 23 13:47:08 2009 +0200
     4.2 +++ b/src/HOL/Inductive.thy	Wed Sep 23 13:48:16 2009 +0200
     4.3 @@ -267,26 +267,6 @@
     4.4    Ball_def Bex_def
     4.5    induct_rulify_fallback
     4.6  
     4.7 -ML {*
     4.8 -val def_lfp_unfold = @{thm def_lfp_unfold}
     4.9 -val def_gfp_unfold = @{thm def_gfp_unfold}
    4.10 -val def_lfp_induct = @{thm def_lfp_induct}
    4.11 -val def_coinduct = @{thm def_coinduct}
    4.12 -val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection}
    4.13 -val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection}
    4.14 -val sup_bool_eq = @{thm sup_bool_eq} RS @{thm eq_reflection}
    4.15 -val sup_fun_eq = @{thm sup_fun_eq} RS @{thm eq_reflection}
    4.16 -val le_boolI = @{thm le_boolI}
    4.17 -val le_boolI' = @{thm le_boolI'}
    4.18 -val le_funI = @{thm le_funI}
    4.19 -val le_boolE = @{thm le_boolE}
    4.20 -val le_funE = @{thm le_funE}
    4.21 -val le_boolD = @{thm le_boolD}
    4.22 -val le_funD = @{thm le_funD}
    4.23 -val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection}
    4.24 -val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection}
    4.25 -*}
    4.26 -
    4.27  use "Tools/inductive.ML"
    4.28  setup Inductive.setup
    4.29  
     5.1 --- a/src/HOL/Lim.thy	Wed Sep 23 13:47:08 2009 +0200
     5.2 +++ b/src/HOL/Lim.thy	Wed Sep 23 13:48:16 2009 +0200
     5.3 @@ -84,6 +84,8 @@
     5.4  lemma LIM_const [simp]: "(%x. k) -- x --> k"
     5.5  by (simp add: LIM_def)
     5.6  
     5.7 +lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
     5.8 +
     5.9  lemma LIM_add:
    5.10    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    5.11    assumes f: "f -- a --> L" and g: "g -- a --> M"
     7.1 --- a/src/HOL/Tools/inductive.ML	Wed Sep 23 13:47:08 2009 +0200
     7.2 +++ b/src/HOL/Tools/inductive.ML	Wed Sep 23 13:48:16 2009 +0200
     7.3 @@ -103,7 +103,10 @@
     7.4        "(P & True) = P" "(True & P) = P"
     7.5      by (fact simp_thms)+};
     7.6  
     7.7 -val simp_thms'' = inf_fun_eq :: inf_bool_eq :: simp_thms';
     7.8 +val simp_thms'' = map mk_meta_eq [@{thm inf_fun_eq}, @{thm inf_bool_eq}] @ simp_thms';
     7.9 +
    7.10 +val simp_thms''' = map mk_meta_eq
    7.11 +  [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_eq}, @{thm sup_bool_eq}];
    7.12  
    7.13  
    7.14  (** context data **)
    7.15 @@ -171,15 +174,15 @@
    7.16        (case concl of
    7.17            (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
    7.18          | _ => [thm' RS (thm' RS eq_to_mono2)]);
    7.19 -    fun dest_less_concl thm = dest_less_concl (thm RS le_funD)
    7.20 -      handle THM _ => thm RS le_boolD
    7.21 +    fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
    7.22 +      handle THM _ => thm RS @{thm le_boolD}
    7.23    in
    7.24      case concl of
    7.25        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    7.26      | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
    7.27      | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
    7.28        [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    7.29 -         (resolve_tac [le_funI, le_boolI'])) thm))]
    7.30 +         (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))]
    7.31      | _ => [thm]
    7.32    end handle THM _ =>
    7.33      error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
    7.34 @@ -323,11 +326,11 @@
    7.35      (HOLogic.mk_Trueprop
    7.36        (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
    7.37      (fn _ => EVERY [rtac @{thm monoI} 1,
    7.38 -      REPEAT (resolve_tac [le_funI, le_boolI'] 1),
    7.39 +      REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
    7.40        REPEAT (FIRST
    7.41          [atac 1,
    7.42           resolve_tac (List.concat (map mk_mono monos) @ get_monos ctxt) 1,
    7.43 -         etac le_funE 1, dtac le_boolD 1])]));
    7.44 +         etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
    7.45  
    7.46  
    7.47  (* prove introduction rules *)
    7.48 @@ -338,7 +341,7 @@
    7.49  
    7.50      val unfold = funpow k (fn th => th RS fun_cong)
    7.51        (mono RS (fp_def RS
    7.52 -        (if coind then def_gfp_unfold else def_lfp_unfold)));
    7.53 +        (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
    7.54  
    7.55      fun select_disj 1 1 = []
    7.56        | select_disj _ 1 = [rtac disjI1]
    7.57 @@ -553,13 +556,13 @@
    7.58      val ind_concl = HOLogic.mk_Trueprop
    7.59        (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
    7.60  
    7.61 -    val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
    7.62 +    val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
    7.63  
    7.64      val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl
    7.65        (fn {prems, ...} => EVERY
    7.66          [rewrite_goals_tac [inductive_conj_def],
    7.67           DETERM (rtac raw_fp_induct 1),
    7.68 -         REPEAT (resolve_tac [le_funI, le_boolI] 1),
    7.69 +         REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
    7.70           rewrite_goals_tac simp_thms'',
    7.71           (*This disjE separates out the introduction rules*)
    7.72           REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
    7.73 @@ -577,7 +580,7 @@
    7.74          [rewrite_goals_tac rec_preds_defs,
    7.75           REPEAT (EVERY
    7.76             [REPEAT (resolve_tac [conjI, impI] 1),
    7.77 -            REPEAT (eresolve_tac [le_funE, le_boolE] 1),
    7.78 +            REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
    7.79              atac 1,
    7.80              rewrite_goals_tac simp_thms',
    7.81              atac 1])])
    7.82 @@ -763,8 +766,8 @@
    7.83             (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
    7.84             (rotate_prems ~1 (ObjectLogic.rulify
    7.85               (fold_rule rec_preds_defs
    7.86 -               (rewrite_rule [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq]
    7.87 -                (mono RS (fp_def RS def_coinduct))))))
    7.88 +               (rewrite_rule simp_thms'''
    7.89 +                (mono RS (fp_def RS @{thm def_coinduct}))))))
    7.90         else
    7.91           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
    7.92             rec_preds_defs ctxt1);
     8.1 --- a/src/Pure/envir.ML	Wed Sep 23 13:47:08 2009 +0200
     8.2 +++ b/src/Pure/envir.ML	Wed Sep 23 13:48:16 2009 +0200
     8.3 @@ -282,12 +282,9 @@
     8.4    let
     8.5      val funerr = "fastype: expected function type";
     8.6      fun fast Ts (f $ u) =
     8.7 -          (case fast Ts f of
     8.8 +          (case Type.devar tyenv (fast Ts f) of
     8.9              Type ("fun", [_, T]) => T
    8.10 -          | TVar v =>
    8.11 -              (case Type.lookup tyenv v of
    8.12 -                SOME (Type ("fun", [_, T])) => T
    8.13 -              | _ => raise TERM (funerr, [f $ u]))
    8.14 +          | TVar v => raise TERM (funerr, [f $ u])
    8.15            | _ => raise TERM (funerr, [f $ u]))
    8.16        | fast Ts (Const (_, T)) = T
    8.17        | fast Ts (Free (_, T)) = T
     9.1 --- a/src/Pure/type.ML	Wed Sep 23 13:47:08 2009 +0200
     9.2 +++ b/src/Pure/type.ML	Wed Sep 23 13:48:16 2009 +0200
     9.3 @@ -55,6 +55,7 @@
     9.4    exception TYPE_MATCH
     9.5    type tyenv = (sort * typ) Vartab.table
     9.6    val lookup: tyenv -> indexname * sort -> typ option
     9.7 +  val devar: tyenv -> typ -> typ
     9.8    val typ_match: tsig -> typ * typ -> tyenv -> tyenv
     9.9    val typ_instance: tsig -> typ * typ -> bool
    9.10    val raw_match: typ * typ -> tyenv -> tyenv