Quoting Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de>:
If you point we to particular occurences, I am willing to polish them accordingly.
There are several versions of bounded_iff in the locales of that theory (and lattice locales from imported theories). To find all problematic theorems, you probably want to apply Makarius' ch-strict patch. I attach this and the other one from his original message. The second patch no longer applies, though.
Clemens
# HG changeset patch # User wenzelm # Date 1349877701 -7200 # Node ID f1455859ff039bb15cb2ff451cc2eb91cb14116b # Parent 28e37eab4e6fa7065d872ae8fcc5978a93ea0845 strict namespace policy for local facts, in correspondance with local terms (cf. Variable.is_body); diff -r 28e37eab4e6f -r f1455859ff03 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Oct 10 15:39:01 2012 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Oct 10 16:01:41 2012 +0200 @@ -952,7 +952,8 @@ val (res, ctxt') = fold_map app facts ctxt; val thms = Global_Theory.name_thms false false name (flat res); val Mode {stmt, ...} = get_mode ctxt; - in ((name, thms), ctxt' |> update_thms {strict = false, index = stmt} (b, SOME thms)) end); + val strict = not (Variable.is_body ctxt); + in ((name, thms), ctxt' |> update_thms {strict = strict, index = stmt} (b, SOME thms)) end); fun put_thms index thms ctxt = ctxt |> map_naming (K Name_Space.local_naming)
# HG changeset patch # User wenzelm # Date 1349877725 -7200 # Node ID 9e0ea0b5bab5f5c7de77f135a21d76f763d22c47 # Parent f1455859ff039bb15cb2ff451cc2eb91cb14116b some attempts to accomodate strict facts; diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Wed Oct 10 16:01:41 2012 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Wed Oct 10 16:02:05 2012 +0200 @@ -74,7 +74,7 @@ "iter' m n f x = (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))" -lemma iter'_pfp_above: +lemma WN_iter'_pfp_above: shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0" and "x0 \<sqsubseteq> iter' m n f x0" using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"] @@ -198,7 +198,7 @@ and bfilter_ivl' is bfilter and AI_ivl' is AI and aval_ivl' is aval' -proof qed (auto simp: iter'_pfp_above) +proof qed (auto simp: WN_iter'_pfp_above) value [code] "list_up(AI_ivl' test3_ivl Top)" value [code] "list_up(AI_ivl' test4_ivl Top)" diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Wed Oct 10 16:01:41 2012 +0200 +++ b/src/HOL/Library/Code_Integer.thy Wed Oct 10 16:02:05 2012 +0200 @@ -31,7 +31,7 @@ done qed -lemma (in ring_1) of_int_code: +lemma (in ring_1) of_int_code': "of_int k = (if k = 0 then 0 else if k < 0 then - of_int (- k) else let @@ -45,7 +45,7 @@ of_int_add [symmetric]) (simp add: * mult_commute) qed -declare of_int_code [code] +declare of_int_code' [code] text {* HOL numeral expressions are mapped to integer literals diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/Library/Target_Numeral.thy --- a/src/HOL/Library/Target_Numeral.thy Wed Oct 10 16:01:41 2012 +0200 +++ b/src/HOL/Library/Target_Numeral.thy Wed Oct 10 16:02:05 2012 +0200 @@ -605,7 +605,7 @@ "k < l \<longleftrightarrow> (of_int k :: Target_Numeral.int) < of_int l" by (simp add: less_int_def) -lemma (in ring_1) of_int_code: +lemma (in ring_1) of_int_code': "of_int k = (if k = 0 then 0 else if k < 0 then - of_int (- k) else let @@ -619,7 +619,7 @@ of_int_add [symmetric]) (simp add: * mult_commute) qed -declare of_int_code [code] +declare of_int_code' [code] subsection {* Implementation for @{typ nat} *} @@ -707,7 +707,7 @@ "num_of_nat = Target_Numeral.num_of_int \<circ> of_nat" by (simp add: fun_eq_iff num_of_int_def of_nat_def) -lemma (in semiring_1) of_nat_code: +lemma (in semiring_1) of_nat_code': "of_nat n = (if n = 0 then 0 else let (m, q) = divmod_nat n 2; @@ -721,7 +721,7 @@ (simp add: * mult_commute of_nat_mult add_commute) qed -declare of_nat_code [code] +declare of_nat_code' [code] text {* Conversions between @{typ nat} and @{typ int} *} diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/Probability/Finite_Product_Measure.thy --- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 10 16:01:41 2012 +0200 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 10 16:02:05 2012 +0200 @@ -696,7 +696,7 @@ qed qed -sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure "Pi\<^isub>M I M" +sublocale finite_product_sigma_finite \<subseteq> Pi: sigma_finite_measure "Pi\<^isub>M I M" using sigma_finite[OF finite_index] . lemma (in finite_product_sigma_finite) measure_times: diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Wed Oct 10 16:01:41 2012 +0200 +++ b/src/HOL/Probability/Probability_Measure.thy Wed Oct 10 16:02:05 2012 +0200 @@ -417,7 +417,8 @@ sublocale product_prob_space \<subseteq> M: prob_space "M i" for i by (rule prob_space) -locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I +locale finite_product_prob_space = + finite_product_sigma_finite M I + product_prob_space: product_prob_space M I for M I sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^isub>M i\<in>I. M i" proof diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Oct 10 16:01:41 2012 +0200 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Oct 10 16:02:05 2012 +0200 @@ -127,7 +127,7 @@ sublocale finite_information \<subseteq> prob_space "point_measure \<Omega> p" by default (simp add: one_ereal_def emeasure_point_measure_finite) -sublocale finite_information \<subseteq> information_space "point_measure \<Omega> p" b +sublocale finite_information \<subseteq> point_measure: information_space "point_measure \<Omega> p" b by default simp lemma (in finite_information) \<mu>'_eq: "A \<subseteq> \<Omega> \<Longrightarrow> prob A = setsum p A"
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev