[isabelle-dev] Shadowing of theorem names in locales
Clemens Ballarin
ballarin at in.tum.de
Tue Jun 11 18:57:42 CEST 2013
Quoting Florian Haftmann <florian.haftmann at 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
-------------- next part --------------
# 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)
-------------- next part --------------
# 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"
More information about the isabelle-dev
mailing list