# HG changeset patch # User wenzelm # Date 1238426084 -7200 # Node ID 787b39d499cf694b60b99d49fee5b68b322f43da # Parent b558464df7c909416e5cf2547365ee4b40a26e5c# Parent 461f7b5f16a2fd6a3d8e0d7ef52e6644a53857ee merged diff -r 461f7b5f16a2 -r 787b39d499cf src/HOL/Tools/function_package/fundef_common.ML --- 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 diff -r 461f7b5f16a2 -r 787b39d499cf src/HOL/Tools/function_package/fundef_datatype.ML --- 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 diff -r 461f7b5f16a2 -r 787b39d499cf src/HOL/Tools/function_package/fundef_package.ML --- 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 diff -r 461f7b5f16a2 -r 787b39d499cf src/HOL/ex/Numeral.thy --- 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 \ 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 \ 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 \ 1" +lemma minus_of_num_le_one_iff: "- of_num n \ 1" by (simp add: less_imp_le minus_of_num_less_one_iff) -lemma minus_one_le_of_num_iff [numeral]: "- 1 \ of_num n" +lemma minus_one_le_of_num_iff: "- 1 \ of_num n" by (simp add: less_imp_le minus_one_less_of_num_iff) -lemma of_num_le_minus_of_num_iff [numeral]: "\ of_num m \ - of_num n" +lemma minus_one_le_one_iff: "- 1 \ 1" + by (simp add: less_imp_le minus_one_less_one_iff) + +lemma of_num_le_minus_of_num_iff: "\ of_num m \ - of_num n" by (simp add: not_le minus_of_num_less_of_num_iff) -lemma one_le_minus_of_num_iff [numeral]: "\ 1 \ - of_num n" +lemma one_le_minus_of_num_iff: "\ 1 \ - of_num n" by (simp add: not_le minus_of_num_less_one_iff) -lemma of_num_le_minus_one_iff [numeral]: "\ of_num n \ - 1" +lemma of_num_le_minus_one_iff: "\ of_num n \ - 1" by (simp add: not_le minus_one_less_of_num_iff) -lemma of_num_less_minus_of_num_iff [numeral]: "\ of_num m < - of_num n" +lemma one_le_minus_one_iff: "\ 1 \ - 1" + by (simp add: not_le minus_one_less_one_iff) + +lemma of_num_less_minus_of_num_iff: "\ 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]: "\ 1 < - of_num n" +lemma one_less_minus_of_num_iff: "\ 1 < - of_num n" by (simp add: not_less minus_of_num_le_one_iff) -lemma of_num_less_minus_one_iff [numeral]: "\ of_num n < - 1" +lemma of_num_less_minus_one_iff: "\ of_num n < - 1" by (simp add: not_less minus_one_le_of_num_iff) +lemma one_less_minus_one_iff: "\ 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 {*