[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