--- a/src/HOL/GCD.thy Thu Oct 27 15:59:25 2011 +0200
+++ b/src/HOL/GCD.thy Thu Oct 27 15:59:33 2011 +0200
@@ -357,7 +357,7 @@
apply (induct m n rule: gcd_nat_induct)
apply simp
apply (case_tac "k = 0")
- apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2)
+ apply (simp_all add: gcd_non_0_nat)
done
lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
--- a/src/HOL/Library/BigO.thy Thu Oct 27 15:59:25 2011 +0200
+++ b/src/HOL/Library/BigO.thy Thu Oct 27 15:59:33 2011 +0200
@@ -129,9 +129,6 @@
apply (erule order_trans)
apply (simp add: ring_distribs)
apply (rule mult_left_mono)
- apply assumption
- apply (simp add: order_less_le)
- apply (rule mult_left_mono)
apply (simp add: abs_triangle_ineq)
apply (simp add: order_less_le)
apply (rule mult_nonneg_nonneg)
@@ -150,9 +147,6 @@
apply (erule order_trans)
apply (simp add: ring_distribs)
apply (rule mult_left_mono)
- apply (simp add: order_less_le)
- apply (simp add: order_less_le)
- apply (rule mult_left_mono)
apply (rule abs_triangle_ineq)
apply (simp add: order_less_le)
apply (rule mult_nonneg_nonneg)
--- a/src/HOL/Metis_Examples/Big_O.thy Thu Oct 27 15:59:25 2011 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy Thu Oct 27 15:59:33 2011 +0200
@@ -196,9 +196,6 @@
apply (erule order_trans)
apply (simp add: ring_distribs)
apply (rule mult_left_mono)
- apply assumption
- apply (simp add: order_less_le)
- apply (rule mult_left_mono)
apply (simp add: abs_triangle_ineq)
apply (simp add: order_less_le)
apply (rule mult_nonneg_nonneg)
@@ -217,9 +214,6 @@
apply (erule order_trans)
apply (simp add: ring_distribs)
apply (rule mult_left_mono)
- apply (simp add: order_less_le)
- apply (simp add: order_less_le)
- apply (rule mult_left_mono)
apply (rule abs_triangle_ineq)
apply (simp add: order_less_le)
apply (metis abs_not_less_zero double_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Oct 27 15:59:25 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Oct 27 15:59:33 2011 +0200
@@ -5298,12 +5298,12 @@
then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto
{ fix n assume "n\<ge>N"
- hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding f.diff[THEN sym] by auto
- moreover have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
+ have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
using subspace_sub[OF s, of "x n" "x N"] using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
using normf[THEN bspec[where x="x n - x N"]] by auto
- ultimately have "norm (x n - x N) < d" using `e>0`
- using mult_left_less_imp_less[of e "norm (x n - x N)" d] by auto }
+ also have "norm (f (x n - x N)) < e * d"
+ using `N \<le> n` N unfolding f.diff[THEN sym] by auto
+ finally have "norm (x n - x N) < d" using `e>0` by simp }
hence "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" by auto }
thus ?thesis unfolding cauchy and dist_norm by auto
qed
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Oct 27 15:59:25 2011 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Oct 27 15:59:33 2011 +0200
@@ -134,7 +134,7 @@
apply (induct m n rule: gcd_induct)
apply simp
apply (case_tac "k = 0")
- apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
+ apply (simp_all add: gcd_non_0)
done
lemma gcd_mult [simp, algebra]: "gcd k (k * n) = k"
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Oct 27 15:59:25 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Oct 27 15:59:33 2011 +0200
@@ -642,7 +642,7 @@
|> Option.map snd |> these |> null |> not
| is_codatatype _ _ = false
fun is_real_quot_type thy (Type (s, _)) =
- is_some (Quotient_Info.quotdata_lookup_raw thy s)
+ is_some (Quotient_Info.quotdata_lookup thy s)
| is_real_quot_type _ _ = false
fun is_quot_type ctxt T =
let val thy = Proof_Context.theory_of ctxt in
@@ -738,15 +738,14 @@
| NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
fun rep_type_for_quot_type thy (T as Type (s, _)) =
- let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
+ let val {qtyp, rtyp, ...} = the (Quotient_Info.quotdata_lookup thy s) in
instantiate_type thy qtyp T rtyp
end
| rep_type_for_quot_type _ T =
raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
let
- val {qtyp, equiv_rel, equiv_thm, ...} =
- Quotient_Info.quotdata_lookup thy s
+ val {qtyp, equiv_rel, equiv_thm, ...} = the (Quotient_Info.quotdata_lookup thy s)
val partial =
case prop_of equiv_thm of
@{const Trueprop} $ (Const (@{const_name equivp}, _) $ _) => false
--- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Oct 27 15:59:25 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Thu Oct 27 15:59:33 2011 +0200
@@ -8,20 +8,17 @@
signature QUOTIENT_INFO =
sig
- exception NotFound (* FIXME complicates signatures unnecessarily *)
type maps_info = {mapfun: string, relmap: string}
val maps_defined: theory -> string -> bool
- (* FIXME functions called "lookup" must return option, not raise exception! *)
- val maps_lookup: theory -> string -> maps_info (* raises NotFound *)
+ val maps_lookup: theory -> string -> maps_info option
val maps_update_thy: string -> maps_info -> theory -> theory
val maps_update: string -> maps_info -> Proof.context -> Proof.context
val print_mapsinfo: Proof.context -> unit
type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
val transform_quotdata: morphism -> quotdata_info -> quotdata_info
- val quotdata_lookup_raw: theory -> string -> quotdata_info option
- val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *)
+ val quotdata_lookup: theory -> string -> quotdata_info option
val quotdata_update_thy: string -> quotdata_info -> theory -> theory
val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
val quotdata_dest: Proof.context -> quotdata_info list
@@ -29,7 +26,7 @@
type qconsts_info = {qconst: term, rconst: term, def: thm}
val transform_qconsts: morphism -> qconsts_info -> qconsts_info
- val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *)
+ val qconsts_lookup: theory -> term -> qconsts_info option
val qconsts_update_thy: string -> qconsts_info -> theory -> theory
val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
val qconsts_dest: Proof.context -> qconsts_info list
@@ -50,9 +47,6 @@
structure Quotient_Info: QUOTIENT_INFO =
struct
-exception NotFound (* FIXME odd OCaml-ism!? *)
-
-
(** data containers **)
(* FIXME just one data slot (record) per program unit *)
@@ -68,13 +62,9 @@
fun merge data = Symtab.merge (K true) data
)
-fun maps_defined thy s =
- Symtab.defined (MapsData.get thy) s
+fun maps_defined thy s = Symtab.defined (MapsData.get thy) s
-fun maps_lookup thy s =
- (case Symtab.lookup (MapsData.get thy) s of
- SOME map_fun => map_fun
- | NONE => raise NotFound)
+fun maps_lookup thy s = Symtab.lookup (MapsData.get thy) s
fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
fun maps_update k minfo = Proof_Context.background_theory (maps_update_thy k minfo) (* FIXME *)
@@ -136,12 +126,7 @@
equiv_rel = Morphism.term phi equiv_rel,
equiv_thm = Morphism.thm phi equiv_thm}
-fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str
-
-fun quotdata_lookup thy str =
- case Symtab.lookup (QuotData.get thy) str of
- SOME qinfo => qinfo
- | NONE => raise NotFound
+fun quotdata_lookup thy str = Symtab.lookup (QuotData.get thy) str
fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
@@ -208,11 +193,8 @@
end
in
(case Symtab.lookup (QConstsData.get thy) name of
- NONE => raise NotFound
- | SOME l =>
- (case find_first matches l of
- SOME x => x
- | NONE => raise NotFound))
+ NONE => NONE
+ | SOME l => find_first matches l)
end
fun print_qconstinfo ctxt =
--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Oct 27 15:59:25 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Oct 27 15:59:33 2011 +0200
@@ -63,13 +63,9 @@
| RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
fun get_mapfun ctxt s =
- let
- val thy = Proof_Context.theory_of ctxt
- val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
- raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
- in
- Const (mapfun, dummyT)
- end
+ case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
+ SOME map_data => Const (#mapfun map_data, dummyT)
+ | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
(* makes a Free out of a TVar *)
fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
@@ -100,13 +96,9 @@
a quotient definition
*)
fun get_rty_qty ctxt s =
- let
- val thy = Proof_Context.theory_of ctxt
- val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound =>
- raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
- in
- (#rtyp qdata, #qtyp qdata)
- end
+ case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
+ SOME qdata => (#rtyp qdata, #qtyp qdata)
+ | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.");
(* takes two type-environments and looks
up in both of them the variable v, which
@@ -279,13 +271,9 @@
Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
fun get_relmap ctxt s =
- let
- val thy = Proof_Context.theory_of ctxt
- val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
- raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
- in
- Const (relmap, dummyT)
- end
+ case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
+ SOME map_data => Const (#relmap map_data, dummyT)
+ | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
fun mk_relmap ctxt vs rty =
let
@@ -302,12 +290,9 @@
end
fun get_equiv_rel ctxt s =
- let
- val thy = Proof_Context.theory_of ctxt
- in
- #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound =>
- raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
- end
+ case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
+ SOME qdata => #equiv_rel qdata
+ | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
fun equiv_match_err ctxt ty_pat ty =
let
@@ -442,7 +427,7 @@
if length rtys <> length qtys then false
else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
else
- (case Quotient_Info.quotdata_lookup_raw thy qs of
+ (case Quotient_Info.quotdata_lookup thy qs of
SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
| NONE => false)
| _ => false)
@@ -568,9 +553,9 @@
if same_const rtrm qtrm then rtrm
else
let
- val rtrm' = #rconst (Quotient_Info.qconsts_lookup thy qtrm)
- handle Quotient_Info.NotFound =>
- term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
+ val rtrm' = case Quotient_Info.qconsts_lookup thy qtrm of
+ SOME qconst_info => #rconst qconst_info
+ | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
in
if Pattern.matches thy (rtrm', rtrm)
then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Thu Oct 27 15:59:25 2011 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Thu Oct 27 15:59:33 2011 +0200
@@ -366,6 +366,7 @@
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
val prove_conv = Arith_Data.prove_conv
+ fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
end;
structure EqCancelFactor = ExtractCommonTermFun
--- a/src/HOL/Tools/numeral_simprocs.ML Thu Oct 27 15:59:25 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Thu Oct 27 15:59:33 2011 +0200
@@ -512,6 +512,7 @@
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
val prove_conv = Arith_Data.prove_conv
+ fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
end;
(*mult_cancel_left requires a ring with no zero divisors.*)
--- a/src/HOL/ex/Simproc_Tests.thy Thu Oct 27 15:59:25 2011 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy Thu Oct 27 15:59:33 2011 +0200
@@ -374,9 +374,8 @@
lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z"
by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
-lemma "(0::rat) < z \<Longrightarrow> z*x < z*y"
-apply (tactic {* test [linordered_ring_less_cancel_factor] *})?
-oops -- "FIXME: test fails"
+lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < z*y"
+by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
subsection {* @{text linordered_ring_le_cancel_factor} *}
@@ -385,8 +384,7 @@
by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y"
-apply (tactic {* test [linordered_ring_le_cancel_factor] *})?
-oops -- "FIXME: test fails"
+by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
subsection {* @{text field_combine_numerals} *}
--- a/src/Provers/Arith/extract_common_term.ML Thu Oct 27 15:59:25 2011 +0200
+++ b/src/Provers/Arith/extract_common_term.ML Thu Oct 27 15:59:33 2011 +0200
@@ -22,6 +22,7 @@
val dest_bal: term -> term * term
val find_first: term -> term list -> term list
(*proof tools*)
+ val mk_eq: term * term -> term
val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
val norm_tac: simpset -> tactic (*proves the result*)
val simplify_meta_eq: simpset -> thm -> thm -> thm (*simplifies the result*)
@@ -65,11 +66,12 @@
and terms2' = Data.find_first u terms2
and T = Term.fastype_of u
+ val t'' = Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2'))
val reshape =
- Data.prove_conv [Data.norm_tac ss] ctxt prems
- (t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2')))
+ Goal.prove ctxt [] [] (Data.mk_eq (t', t'')) (K (Data.norm_tac ss))
+
in
- Option.map (export o Data.simplify_meta_eq ss simp_th) reshape
+ SOME (export (Data.simplify_meta_eq ss simp_th reshape))
end
(* FIXME avoid handling of generic exceptions *)
handle TERM _ => NONE
--- a/src/Pure/Isar/proof_display.ML Thu Oct 27 15:59:25 2011 +0200
+++ b/src/Pure/Isar/proof_display.ML Thu Oct 27 15:59:33 2011 +0200
@@ -31,9 +31,14 @@
Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
else Pretty.str "<context>");
-fun default_context thy =
- Context.cases Syntax.init_pretty_global I
- (the_default (Context.Theory thy) (try ML_Context.the_generic_context ()));
+fun default_context thy0 =
+ (case Context.thread_data () of
+ SOME (Context.Proof ctxt) => ctxt
+ | SOME (Context.Theory thy) =>
+ (case try Syntax.init_pretty_global thy of
+ SOME ctxt => ctxt
+ | NONE => Syntax.init_pretty_global thy0)
+ | NONE => Syntax.init_pretty_global thy0);
fun pp_thm th =
let
--- a/src/Tools/Code/code_runtime.ML Thu Oct 27 15:59:25 2011 +0200
+++ b/src/Tools/Code/code_runtime.ML Thu Oct 27 15:59:33 2011 +0200
@@ -422,7 +422,7 @@
val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
val _ = Secure.use_text notifying_context
(0, Path.implode filepath) false (File.read filepath);
- val thy'' = (Context.the_theory o the) (Context.thread_data ());
+ val thy'' = Context.the_theory (Context.the_thread_data ());
val names = Loaded_Values.get thy'';
in (names, thy'') end;