--- a/src/Doc/Nitpick/document/root.tex Thu Sep 27 19:34:31 2012 +0200
+++ b/src/Doc/Nitpick/document/root.tex Thu Sep 27 19:35:29 2012 +0200
@@ -2032,7 +2032,7 @@
{\small See also \textit{bits} (\S\ref{scope-of-search}) and
\textit{show\_datatypes} (\S\ref{output-format}).}
-\opdefault{bits}{int\_seq}{\upshape 1,2,3,4,6,8,10,12,14,16}
+\opdefault{bits}{int\_seq}{\upshape 1--10}
Specifies the number of bits to use to represent natural numbers and integers in
binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
--- a/src/Doc/ProgProve/Logic.thy Thu Sep 27 19:34:31 2012 +0200
+++ b/src/Doc/ProgProve/Logic.thy Thu Sep 27 19:35:29 2012 +0200
@@ -87,10 +87,12 @@
\begin{warn}
In @{term"{x. P}"} the @{text x} must be a variable. Set comprehension
involving a proper term @{text t} must be written
-@{term[source]"{t | x y z. P}"},
-where @{text "x y z"} are the free variables in @{text t}.
-This is just a shorthand for @{term"{v. EX x y z. v = t \<and> P}"}, where
-@{text v} is a new variable.
+\noquotes{@{term[source] "{t | x y. P}"}},
+where @{text "x y"} are those free variables in @{text t}
+that occur in @{text P}.
+This is just a shorthand for @{term"{v. EX x y. v = t \<and> P}"}, where
+@{text v} is a new variable. For example, @{term"{x+y|x. x \<in> A}"}
+is short for \noquotes{@{term[source]"{v. \<exists>x. v = x+y \<and> x \<in> A}"}}.
\end{warn}
Here are the ASCII representations of the mathematical symbols:
--- a/src/Doc/ProgProve/document/prelude.tex Thu Sep 27 19:34:31 2012 +0200
+++ b/src/Doc/ProgProve/document/prelude.tex Thu Sep 27 19:35:29 2012 +0200
@@ -68,7 +68,7 @@
\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
\renewenvironment{isamarkuptxt}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
-\newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}#1}}
+\newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}\renewcommand{\isachardoublequoteopen}{}\renewcommand{\isachardoublequoteclose}{}#1}}
\newcommand{\concept}[1]{\textbf{#1}}
\newcommand{\xsymbol}[1]{\texttt{\char`\\\char`<#1>}}
--- a/src/HOL/BNF/Examples/Misc_Codata.thy Thu Sep 27 19:34:31 2012 +0200
+++ b/src/HOL/BNF/Examples/Misc_Codata.thy Thu Sep 27 19:35:29 2012 +0200
@@ -58,11 +58,15 @@
and ('a, 'b, 'c) in_here =
IH1 'b 'a | IH2 'c
-codata_raw some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
-and in_here': 'c = "'d + 'e"
+codata ('a, 'b, 'c) some_killing' =
+ SK' "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing' + ('a, 'b, 'c) in_here'"
+ and ('a, 'b, 'c) in_here' =
+ IH1' 'b | IH2' 'c
-codata_raw some_killing'': 'a = "'b \<Rightarrow> 'c"
-and in_here'': 'c = "'d \<times> 'b + 'e"
+codata ('a, 'b, 'c) some_killing'' =
+ SK'' "'a \<Rightarrow> ('a, 'b, 'c) in_here''"
+ and ('a, 'b, 'c) in_here'' =
+ IH1'' 'b 'a | IH2'' 'c
codata ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c"
--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Sep 27 19:34:31 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Sep 27 19:35:29 2012 +0200
@@ -923,8 +923,7 @@
(*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
in
- Skip_Proof.prove lthy [] [] goal
- (fn {context = ctxt, ...} => mk_collect_set_natural_tac ctxt (#set_natural axioms))
+ Skip_Proof.prove lthy [] [] goal (K (mk_collect_set_natural_tac (#set_natural axioms)))
|> Thm.close_derivation
end;
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Sep 27 19:34:31 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Sep 27 19:35:29 2012 +0200
@@ -8,7 +8,7 @@
signature BNF_DEF_TACTICS =
sig
- val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic
+ val mk_collect_set_natural_tac: thm list -> tactic
val mk_id': thm -> thm
val mk_comp': thm -> thm
val mk_in_mono_tac: int -> tactic
@@ -44,8 +44,12 @@
((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
(etac subset_trans THEN' atac) 1;
-fun mk_collect_set_natural_tac ctxt set_naturals =
- substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1;
+fun mk_collect_set_natural_tac set_naturals =
+ (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
+ EVERY' (map (fn set_natural =>
+ rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
+ rtac set_natural) set_naturals) THEN'
+ rtac @{thm image_empty}) 1;
fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals =
if null set_naturals then
@@ -106,11 +110,10 @@
fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} =
unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN
- subst_tac ctxt NONE [map_id] 1 THEN
- (if n = 0 then rtac refl 1
- else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
- rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
- CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1);
+ (if n = 0 then rtac refl 1
+ else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
+ rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
+ CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id] 1);
fun mk_srel_mono_tac srel_O_Grs in_mono {context = ctxt, prems = _} =
unfold_thms_tac ctxt srel_O_Grs THEN
--- a/src/HOL/BNF/Tools/bnf_fp.ML Thu Sep 27 19:34:31 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML Thu Sep 27 19:35:29 2012 +0200
@@ -257,7 +257,6 @@
val rel_distinctN = relN ^ "_" ^ distinctN
val injectN = "inject"
val rel_injectN = relN ^ "_" ^ injectN
-val relsN = relN ^ "s"
val selN = "sel"
val sel_unfoldN = selN ^ "_" ^ unfoldN
val sel_corecN = selN ^ "_" ^ corecN
--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML Thu Sep 27 19:34:31 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML Thu Sep 27 19:35:29 2012 +0200
@@ -28,6 +28,19 @@
open BNF_FP
open BNF_FP_Sugar_Tactics
+(* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A") *)
+fun quasi_unambiguous_case_names names =
+ let
+ val ps = map (`Long_Name.base_name) names;
+ val dups = Library.duplicates (op =) (map fst ps);
+ fun underscore s =
+ let val ss = space_explode Long_Name.separator s in
+ space_implode "_" (drop (length ss - 2) ss)
+ end;
+ in
+ map (fn (base, full) => if member (op =) dups base then underscore full else base) ps
+ end;
+
val mp_conj = @{thm mp_conj};
val simp_attrs = @{attributes [simp]};
@@ -747,8 +760,7 @@
`(conj_dests nn) thm
end;
- (* TODO: Generate nicer names in case of clashes *)
- val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss);
+ val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss);
val (fold_thmss, rec_thmss) =
let
@@ -813,8 +825,8 @@
val notes =
[(inductN, map single induct_thms,
fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
- (foldN, fold_thmss, K (code_simp_attrs)),
- (recN, rec_thmss, K (code_simp_attrs)),
+ (foldN, fold_thmss, K code_simp_attrs),
+ (recN, rec_thmss, K code_simp_attrs),
(simpsN, simp_thmss, K [])]
|> maps (fn (thmN, thmss, attrs) =>
map3 (fn b => fn Type (T_name, _) => fn thms =>
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Sep 27 19:34:31 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Sep 27 19:35:29 2012 +0200
@@ -104,6 +104,7 @@
fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
+ val (dead_params, dead_params') = `(map Term.dest_TFree) (subtract (op =) passiveAs params');
val FTsAs = mk_FTs allAs;
val FTsBs = mk_FTs allBs;
val FTsCs = mk_FTs allCs;
@@ -1022,10 +1023,10 @@
val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b;
val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
- typedef false NONE (sbdT_bind, params, NoSyn)
+ typedef false NONE (sbdT_bind, dead_params, NoSyn)
(HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
- val sbdT = Type (sbdT_name, params');
+ val sbdT = Type (sbdT_name, dead_params');
val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
val sbd_bind = Binding.suffix_name ("_" ^ sum_bdN) b;
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Sep 27 19:34:31 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Sep 27 19:35:29 2012 +0200
@@ -14,7 +14,6 @@
val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
val fo_rtac: thm -> Proof.context -> int -> tactic
val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic
- val substs_tac: Proof.context -> thm list -> int -> tactic
val unfold_thms_tac: Proof.context -> thm list -> tactic
val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
@@ -62,7 +61,6 @@
(*unlike "unfold_thms_tac", these succeed when the RHS contains schematic variables not in the LHS*)
fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
-fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt NONE;
(* Theorems for open typedefs with UNIV as representing set *)
--- a/src/HOL/BNF/Tools/bnf_wrap.ML Thu Sep 27 19:34:31 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML Thu Sep 27 19:35:29 2012 +0200
@@ -13,7 +13,7 @@
val mk_ctr: typ list -> term -> term
val mk_disc_or_sel: typ list -> term -> term
- val base_name_of_ctr: term -> string
+ val name_of_ctr: term -> string
val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
((bool * term list) * term) *
@@ -93,11 +93,13 @@
Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t
end;
-fun base_name_of_ctr c =
- Long_Name.base_name (case head_of c of
- Const (s, _) => s
- | Free (s, _) => s
- | _ => error "Cannot extract name of constructor");
+fun name_of_ctr c =
+ (case head_of c of
+ Const (s, _) => s
+ | Free (s, _) => s
+ | _ => error "Cannot extract name of constructor");
+
+val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Sep 27 19:34:31 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Sep 27 19:35:29 2012 +0200
@@ -44,7 +44,7 @@
val default_default_params =
[("card", "1\<emdash>10"),
("iter", "0,1,2,4,8,12,16,20,24,28"),
- ("bits", "1,2,3,4,6,8,10,12,14,16"),
+ ("bits", "1\<emdash>10"),
("bisim_depth", "9"),
("box", "smart"),
("finitize", "smart"),