On Tue, Nov 30, 2010 at 8:35 AM, Florian Haftmann
<[email protected]> wrote:
>>> indeed, both theorems are the same, just with different accesses;
>>> recently, we introduced the concept of mandatory qualifiers to avoid the
>>> strange base accesses (e.g. »induct«, »simps«, »intros«), but this has
>>> never been systematically introduces into existing packages.
>>>
>> Is there any reason why we shouldn't update the datatype package right
>> now, to make the qualifier mandatory on "foo.induct"?
>
> Maybe this is a good opportunity. Maybe this should be done to every
> package which has no specific maintainer.
Attached is a mercurial changeset for adding mandatory qualifiers to
theorems generated by (rep_)datatype. Here are the affected theorem
names (that I know of):
induct
inject
distinct
exhaust
cases
split
split_asm
weak_case_cong
nchotomy
case_cong
I've only tested this with HOL-Main; I'll let someone else test it
more thoroughly and decide whether or not to commit it.
- Brian
# HG changeset patch
# User huffman
# Date 1291143768 28800
# Node ID 987a4e7a7a206d2bc52c05e6d323ffdc3282cccd
# Parent a3af470a55d29db2952d136352af50a9add50c05
theorem names generated by the (rep_)datatype command now have mandatory qualifiers
diff -r a3af470a55d2 -r 987a4e7a7a20 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy Tue Nov 30 18:40:23 2010 +0100
+++ b/src/HOL/Product_Type.thy Tue Nov 30 11:02:48 2010 -0800
@@ -160,7 +160,7 @@
declare prod.simps(2) [nitpick_simp del]
-declare weak_case_cong [cong del]
+declare prod.weak_case_cong [cong del]
subsubsection {* Tuple syntax *}
@@ -440,7 +440,7 @@
lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
-- {* Prevents simplification of @{term c}: much faster *}
- by (fact weak_case_cong)
+ by (fact prod.weak_case_cong)
lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
by (simp add: split_eta)
@@ -578,7 +578,7 @@
\medskip @{term split} used as a logical connective or set former.
\medskip These rules are for use with @{text blast}; could instead
- call @{text simp} using @{thm [source] split} as rewrite. *}
+ call @{text simp} using @{thm [source] prod.split} as rewrite. *}
lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p"
apply (simp only: split_tupled_all)
diff -r a3af470a55d2 -r 987a4e7a7a20 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML Tue Nov 30 18:40:23 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Tue Nov 30 11:02:48 2010 -0800
@@ -628,9 +628,9 @@
val ([dt_induct'], thy7) =
thy6
- |> Sign.add_path big_name
- |> Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
- ||> Sign.parent_path
+ |> Global_Theory.add_thms
+ [((Binding.qualify true big_name (Binding.name "induct"), dt_induct),
+ [case_names_induct])]
||> Theory.checkpoint;
in
diff -r a3af470a55d2 -r 987a4e7a7a20 src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Tue Nov 30 18:40:23 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Tue Nov 30 11:02:48 2010 -0800
@@ -98,18 +98,18 @@
fun store_thmss_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
- Sign.add_path tname
- #> Global_Theory.add_thmss [((Binding.name label, thms), atts)]
- #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+ Global_Theory.add_thmss
+ [((Binding.qualify true tname (Binding.name label), thms), atts)]
+ #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
fun store_thms_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
- Sign.add_path tname
- #> Global_Theory.add_thms [((Binding.name label, thms), atts)]
- #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+ Global_Theory.add_thms
+ [((Binding.qualify true tname (Binding.name label), thms), atts)]
+ #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
diff -r a3af470a55d2 -r 987a4e7a7a20 src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML Tue Nov 30 18:40:23 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Tue Nov 30 11:02:48 2010 -0800
@@ -362,14 +362,14 @@
let
val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+ val prfx = Binding.qualify true (space_implode "_" new_type_names);
val (((inject, distinct), [induct]), thy2) =
thy1
|> store_thmss "inject" new_type_names raw_inject
||>> store_thmss "distinct" new_type_names raw_distinct
- ||> Sign.add_path (space_implode "_" new_type_names)
||>> Global_Theory.add_thms
- [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
- ||> Sign.restore_naming thy1;
+ [((prfx (Binding.name "induct"), raw_induct),
+ [mk_case_names_induct descr])];
in
thy2
|> derive_datatype_props config dt_names alt_names [descr] sorts
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
