[isabelle-dev] Shadowing of theorem names in locales

Makarius makarius at sketis.net
Wed Oct 10 16:51:34 CEST 2012

On Tue, 9 Oct 2012, Makarius wrote:

> On Sun, 7 Oct 2012, Florian Haftmann wrote:
>> After some pondering I would argue that this should be forbidden:
>> * (Complete) shadowing is a constant source of confusion.
>> * Global interpretations are impossible then, since they would result in
>> two global theorems with the same name.
> I've started some experiments with this idea and will report the empirical 
> results soon ...

After some detours I am now back on Isabelle/28e37eab4e6f.

In principle, the last big reform of locale + interpretation name space 
prefixes has addressed the situation already, where each locale scope is 
locally strict, but composing several of them in locale expressions etc. 
works by mandatory or non-mandatory prefixes.

Actual strictness checking is part of the underlying name space policy, 
when bindings are applied and react with some naming. The "local" context 
of the locale construction is particularly important here.  It was merely 
a historical left-over that fact bindings were not checked strictly:

   (1) in distant past facts were never strict and totally un-authentic

   (2) the Isar proof "body" mode allows to override 'notes' as it does for

So with the "ch-strict" changeset applied to the critical spot of local 
notes, the namespace policy enforces the concentual locale scopes.

Applying this in practice leads to many surprises about situations found 
in existing theory libraries, though.  Some of the changsets leading up to 
Isabelle/28e37eab4e6f already sort this out.  Some other ad-hoc changes 
are attached as ch-test here.

With Isabelle/28e37eab4e6f + ch-strict + ch-test and AFP/77f79b2076f1
the following sessions fail:

BDD, Dijkstra_Shortest_Path, Free-Groups, Group-Ring-Module, HOL-Algebra, 
HOL-Number_Theory, HOL-ex, JinjaThreads, KBPs, Markov_Models, Ordinal, 
Ordinary_Differential_Equations, Pi_Calculus, Presburger-Automata, 
PseudoHoops, Psi_Calculi, Refine_Monadic, Simpl, Slicing, Topology, 
Transitive-Closure-II, Valuation

So the question if ch-strict can be activated soon is mainly a matter of 
library space.  It is up to emerging volunteers to sort it out further.

(For me it was interesting to see how Isabell/jEdit works on the 
JinjaThreads monster session.  See also AFP/77f79b2076f1 of the result of 
investing 3GB for poly, 4GB for java, and quite a bit of CPU time and 
elapsed time.)

-------------- 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 @@
-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)
-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)
-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)
-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 @@
-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"
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