[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
'fixes'.
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.)
Makarius
-------------- 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