--- a/src/HOL/Tools/function_package/fundef_common.ML Mon Mar 30 15:16:58 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Mar 30 17:14:44 2009 +0200
@@ -65,7 +65,7 @@
defname : string,
(* contains no logical entities: invariant under morphisms *)
- add_simps : (string -> string) -> string -> Attrib.src list -> thm list
+ add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list
-> local_theory -> thm list * local_theory,
case_names : string list,
@@ -289,8 +289,8 @@
(* Preprocessors *)
type fixes = ((string * typ) * mixfix) list
-type 'a spec = ((bstring * Attrib.src list) * 'a list) list
-type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec
+type 'a spec = (Attrib.binding * 'a list) list
+type preproc = fundef_config -> Proof.context -> fixes -> term spec
-> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
val fname_of = fst o dest_Free o fst o strip_comb o fst
@@ -301,9 +301,9 @@
| mk_case_names _ n 1 = [n]
| mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
-fun empty_preproc check _ _ ctxt fixes spec =
+fun empty_preproc check _ ctxt fixes spec =
let
- val (nas,tss) = split_list spec
+ val (bnds, tss) = split_list spec
val ts = flat tss
val _ = check ctxt fixes ts
val fnames = map (fst o fst) fixes
@@ -314,9 +314,9 @@
|> map (map snd)
(* using theorem names for case name currently disabled *)
- val cnames = map_index (fn (i, (n,_)) => mk_case_names i "" 1) nas |> flat
+ val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
in
- (ts, curry op ~~ nas o Library.unflat tss, sort, cnames)
+ (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
end
structure Preprocessor = GenericDataFun
@@ -344,23 +344,9 @@
fun config_parser default =
(Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
>> (fn opts => fold apply_opt opts default)
-
- val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
-
- fun pipe_error t =
- P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
-
- val statement_ow =
- SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
- --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
-
- val statements_ow = P.enum1 "|" statement_ow
-
- val flags_statements = statements_ow
- >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
in
fun fundef_parser default_cfg =
- config_parser default_cfg -- P.fixes --| P.where_ -- flags_statements
+ config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
end
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Mar 30 15:16:58 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Mon Mar 30 17:14:44 2009 +0200
@@ -15,10 +15,10 @@
val add_fun : FundefCommon.fundef_config ->
(binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
- bool list -> bool -> local_theory -> Proof.context
+ bool -> local_theory -> Proof.context
val add_fun_cmd : FundefCommon.fundef_config ->
(binding * string option * mixfix) list -> (Attrib.binding * string) list ->
- bool list -> bool -> local_theory -> Proof.context
+ bool -> local_theory -> Proof.context
end
structure FundefDatatype : FUNDEF_DATATYPE =
@@ -235,50 +235,40 @@
end
fun add_catchall ctxt fixes spec =
- let
- val catchalls = mk_catchall fixes (mk_arities (map (split_def ctxt) (map snd spec)))
- in
- spec @ map (pair true) catchalls
- end
+ spec @ mk_catchall fixes (mk_arities (map (split_def ctxt) spec))
fun warn_if_redundant ctxt origs tss =
let
fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
val (tss', _) = chop (length origs) tss
- fun check ((_, t), []) = (Output.warning (msg t); [])
- | check ((_, t), s) = s
+ fun check (t, []) = (Output.warning (msg t); [])
+ | check (t, s) = s
in
(map check (origs ~~ tss'); tss)
end
-fun sequential_preproc (config as FundefConfig {sequential, ...}) flags ctxt fixes spec =
- let
- val enabled = sequential orelse exists I flags
- in
- if enabled then
+fun sequential_preproc (config as FundefConfig {sequential, ...}) ctxt fixes spec =
+ if sequential then
let
- val flags' = if sequential then map (K true) flags else flags
-
- val (nas, eqss) = split_list spec
+ val (bnds, eqss) = split_list spec
val eqs = map the_single eqss
val feqs = eqs
|> tap (check_defs ctxt fixes) (* Standard checks *)
|> tap (map (check_pats ctxt)) (* More checks for sequential mode *)
- |> curry op ~~ flags'
val compleqs = add_catchall ctxt fixes feqs (* Completion *)
val spliteqs = warn_if_redundant ctxt feqs
- (FundefSplit.split_some_equations ctxt compleqs)
+ (FundefSplit.split_all_equations ctxt compleqs)
fun restore_spec thms =
- nas ~~ Library.take (length nas, Library.unflat spliteqs thms)
+ bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms)
- val spliteqs' = flat (Library.take (length nas, spliteqs))
+ val spliteqs' = flat (Library.take (length bnds, spliteqs))
val fnames = map (fst o fst) fixes
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
@@ -286,18 +276,17 @@
|> map (map snd)
- val nas' = nas @ replicate (length spliteqs - length nas) ("",[])
+ val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding
(* using theorem names for case name currently disabled *)
- val case_names = map_index (fn (i, ((n, _), es)) => mk_case_names i "" (length es))
- (nas' ~~ spliteqs)
+ val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es))
+ (bnds' ~~ spliteqs)
|> flat
in
(flat spliteqs, restore_spec, sort, case_names)
end
else
- FundefCommon.empty_preproc check_defs config flags ctxt fixes spec
- end
+ FundefCommon.empty_preproc check_defs config ctxt fixes spec
val setup =
Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
@@ -308,11 +297,11 @@
val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*),
domintros=false, tailrec=false }
-fun gen_fun add config fixes statements flags int lthy =
+fun gen_fun add config fixes statements int lthy =
let val group = serial_string () in
lthy
|> LocalTheory.set_group group
- |> add fixes statements config flags
+ |> add fixes statements config
|> by_pat_completeness_auto int
|> LocalTheory.restore
|> LocalTheory.set_group group
@@ -329,7 +318,7 @@
val _ =
OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
(fundef_parser fun_config
- >> (fn ((config, fixes), (flags, statements)) => add_fun_cmd config fixes statements flags));
+ >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements));
end
--- a/src/HOL/Tools/function_package/fundef_package.ML Mon Mar 30 15:16:58 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Mar 30 17:14:44 2009 +0200
@@ -10,13 +10,11 @@
val add_fundef : (binding * typ option * mixfix) list
-> (Attrib.binding * term) list
-> FundefCommon.fundef_config
- -> bool list
-> local_theory
-> Proof.state
val add_fundef_cmd : (binding * string option * mixfix) list
- -> (Attrib.binding * string) list
+ -> (Attrib.binding * string) list
-> FundefCommon.fundef_config
- -> bool list
-> local_theory
-> Proof.state
@@ -36,20 +34,28 @@
open FundefLib
open FundefCommon
+val simp_attribs = map (Attrib.internal o K)
+ [Simplifier.simp_add,
+ Code.add_default_eqn_attribute,
+ Nitpick_Const_Simp_Thms.add]
+
+val psimp_attribs = map (Attrib.internal o K)
+ [Simplifier.simp_add,
+ Nitpick_Const_Psimp_Thms.add]
+
fun note_theorem ((name, atts), ths) =
LocalTheory.note Thm.theoremK ((Binding.qualified_name name, atts), ths)
-fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
+fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
let
- val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
val spec = post simps
- |> map (apfst (apsnd (append atts)))
+ |> map (apfst (apsnd (fn ats => moreatts @ ats)))
|> map (apfst (apfst extra_qualify))
val (saved_spec_simps, lthy) =
- fold_map note_theorem spec lthy
+ fold_map (LocalTheory.note Thm.theoremK) spec lthy
val saved_simps = flat (map snd saved_spec_simps)
val simps_by_f = sort saved_simps
@@ -72,15 +78,15 @@
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
- |> addsmps (Long_Name.qualify "partial") "psimps"
- [Attrib.internal (K Nitpick_Const_Psimp_Thms.add)] psimps
- ||> fold_option (snd oo addsmps I "simps" [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]) trsimps
+ |> addsmps (Binding.qualify false "partial") "psimps"
+ psimp_attribs psimps
+ ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
||>> note_theorem ((qualify "pinduct",
[Attrib.internal (K (RuleCases.case_names cnames)),
Attrib.internal (K (RuleCases.consumes 1)),
Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
||>> note_theorem ((qualify "termination", []), [termination])
- ||> (snd o note_theorem ((qualify "cases",
+ ||> (snd o note_theorem ((qualify "cases",
[Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
@@ -90,18 +96,18 @@
if not do_print then ()
else Specification.print_consts lthy (K false) (map fst fixes)
in
- lthy
+ lthy
|> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata)
end
-fun gen_add_fundef is_external prep default_constraint fixspec eqns config flags lthy =
+fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy =
let
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
val fixes = map (apfst (apfst Binding.name_of)) fixes0;
- val spec = map (fn ((b, atts), prop) => ((Binding.name_of b, atts), [prop])) spec0;
- val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
+ val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
+ val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec
val defname = mk_defname fixes
@@ -131,14 +137,10 @@
val tsimps = map remove_domain_condition psimps
val tinduct = map remove_domain_condition pinducts
- val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
- val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
- [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
-
val qualify = Long_Name.qualify defname;
in
lthy
- |> add_simps I "simps" allatts tsimps |> snd
+ |> add_simps I "simps" simp_attribs tsimps |> snd
|> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd
end
@@ -209,12 +211,10 @@
local structure P = OuterParse and K = OuterKeyword in
-val _ = OuterKeyword.keyword "otherwise";
-
val _ =
OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
(fundef_parser default_config
- >> (fn ((config, fixes), (flags, statements)) => add_fundef_cmd fixes statements config flags));
+ >> (fn ((config, fixes), statements) => add_fundef_cmd fixes statements config));
val _ =
OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
--- a/src/HOL/ex/Numeral.thy Mon Mar 30 15:16:58 2009 +0200
+++ b/src/HOL/ex/Numeral.thy Mon Mar 30 17:14:44 2009 +0200
@@ -507,54 +507,78 @@
context ordered_idom
begin
-lemma minus_of_num_less_of_num_iff [numeral]: "- of_num m < of_num n"
+lemma minus_of_num_less_of_num_iff: "- of_num m < of_num n"
proof -
have "- of_num m < 0" by (simp add: of_num_pos)
also have "0 < of_num n" by (simp add: of_num_pos)
finally show ?thesis .
qed
-lemma minus_of_num_less_one_iff [numeral]: "- of_num n < 1"
-proof -
- have "- of_num n < 0" by (simp add: of_num_pos)
- also have "0 < 1" by simp
- finally show ?thesis .
-qed
+lemma minus_of_num_less_one_iff: "- of_num n < 1"
+using minus_of_num_less_of_num_iff [of n One] by (simp add: of_num_one)
-lemma minus_one_less_of_num_iff [numeral]: "- 1 < of_num n"
-proof -
- have "- 1 < 0" by simp
- also have "0 < of_num n" by (simp add: of_num_pos)
- finally show ?thesis .
-qed
+lemma minus_one_less_of_num_iff: "- 1 < of_num n"
+using minus_of_num_less_of_num_iff [of One n] by (simp add: of_num_one)
-lemma minus_of_num_le_of_num_iff [numeral]: "- of_num m \<le> of_num n"
+lemma minus_one_less_one_iff: "- 1 < 1"
+using minus_of_num_less_of_num_iff [of One One] by (simp add: of_num_one)
+
+lemma minus_of_num_le_of_num_iff: "- of_num m \<le> of_num n"
by (simp add: less_imp_le minus_of_num_less_of_num_iff)
-lemma minus_of_num_le_one_iff [numeral]: "- of_num n \<le> 1"
+lemma minus_of_num_le_one_iff: "- of_num n \<le> 1"
by (simp add: less_imp_le minus_of_num_less_one_iff)
-lemma minus_one_le_of_num_iff [numeral]: "- 1 \<le> of_num n"
+lemma minus_one_le_of_num_iff: "- 1 \<le> of_num n"
by (simp add: less_imp_le minus_one_less_of_num_iff)
-lemma of_num_le_minus_of_num_iff [numeral]: "\<not> of_num m \<le> - of_num n"
+lemma minus_one_le_one_iff: "- 1 \<le> 1"
+ by (simp add: less_imp_le minus_one_less_one_iff)
+
+lemma of_num_le_minus_of_num_iff: "\<not> of_num m \<le> - of_num n"
by (simp add: not_le minus_of_num_less_of_num_iff)
-lemma one_le_minus_of_num_iff [numeral]: "\<not> 1 \<le> - of_num n"
+lemma one_le_minus_of_num_iff: "\<not> 1 \<le> - of_num n"
by (simp add: not_le minus_of_num_less_one_iff)
-lemma of_num_le_minus_one_iff [numeral]: "\<not> of_num n \<le> - 1"
+lemma of_num_le_minus_one_iff: "\<not> of_num n \<le> - 1"
by (simp add: not_le minus_one_less_of_num_iff)
-lemma of_num_less_minus_of_num_iff [numeral]: "\<not> of_num m < - of_num n"
+lemma one_le_minus_one_iff: "\<not> 1 \<le> - 1"
+ by (simp add: not_le minus_one_less_one_iff)
+
+lemma of_num_less_minus_of_num_iff: "\<not> of_num m < - of_num n"
by (simp add: not_less minus_of_num_le_of_num_iff)
-lemma one_less_minus_of_num_iff [numeral]: "\<not> 1 < - of_num n"
+lemma one_less_minus_of_num_iff: "\<not> 1 < - of_num n"
by (simp add: not_less minus_of_num_le_one_iff)
-lemma of_num_less_minus_one_iff [numeral]: "\<not> of_num n < - 1"
+lemma of_num_less_minus_one_iff: "\<not> of_num n < - 1"
by (simp add: not_less minus_one_le_of_num_iff)
+lemma one_less_minus_one_iff: "\<not> 1 < - 1"
+ by (simp add: not_less minus_one_le_one_iff)
+
+lemmas le_signed_numeral_special [numeral] =
+ minus_of_num_le_of_num_iff
+ minus_of_num_le_one_iff
+ minus_one_le_of_num_iff
+ minus_one_le_one_iff
+ of_num_le_minus_of_num_iff
+ one_le_minus_of_num_iff
+ of_num_le_minus_one_iff
+ one_le_minus_one_iff
+
+lemmas less_signed_numeral_special [numeral] =
+ minus_of_num_less_of_num_iff
+ minus_of_num_less_one_iff
+ minus_one_less_of_num_iff
+ minus_one_less_one_iff
+ of_num_less_minus_of_num_iff
+ one_less_minus_of_num_iff
+ of_num_less_minus_one_iff
+ one_less_minus_one_iff
+
end
subsubsection {*