# HG changeset patch # User wenzelm # Date 1348767329 -7200 # Node ID 9d34cfe1dbdf793084bf7ec7ef29e238f1fa40e6 # Parent 1a0f25c38629c61d69e587ea85aaf971f376671e# Parent 0009a6ebc83bbcc84eeb2003daf36228629ba968 merged diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/Doc/Nitpick/document/root.tex --- 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. diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/Doc/ProgProve/Logic.thy --- 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 \ 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 \ P}"}, where +@{text v} is a new variable. For example, @{term"{x+y|x. x \ A}"} +is short for \noquotes{@{term[source]"{v. \x. v = x+y \ x \ A}"}}. \end{warn} Here are the ASCII representations of the mathematical symbols: diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/Doc/ProgProve/document/prelude.tex --- 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>}} diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/HOL/BNF/Examples/Misc_Codata.thy --- 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 \ 'd \ ('a + 'c)" -and in_here': 'c = "'d + 'e" +codata ('a, 'b, 'c) some_killing' = + SK' "'a \ 'b \ ('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 \ 'c" -and in_here'': 'c = "'d \ 'b + 'e" +codata ('a, 'b, 'c) some_killing'' = + SK'' "'a \ ('a, 'b, 'c) in_here''" + and ('a, 'b, 'c) in_here'' = + IH1'' 'b 'a | IH2'' 'c codata ('b, 'c) less_killing = LK "'b \ 'c" diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/HOL/BNF/Tools/bnf_def.ML --- 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; diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/HOL/BNF/Tools/bnf_def_tactics.ML --- 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 diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/HOL/BNF/Tools/bnf_fp.ML --- 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 diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/HOL/BNF/Tools/bnf_fp_sugar.ML --- 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 => diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/HOL/BNF/Tools/bnf_gfp.ML --- 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; diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/HOL/BNF/Tools/bnf_tactics.ML --- 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 *) diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/HOL/BNF/Tools/bnf_wrap.ML --- 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; diff -r 0009a6ebc83b -r 9d34cfe1dbdf src/HOL/Tools/Nitpick/nitpick_isar.ML --- 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\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\10"), ("bisim_depth", "9"), ("box", "smart"), ("finitize", "smart"),