1.1 --- a/src/HOL/FunDef.thy Tue Nov 07 11:47:57 2006 +0100
1.2 +++ b/src/HOL/FunDef.thy Tue Nov 07 11:53:55 2006 +0100
1.3 @@ -189,11 +189,6 @@
1.4 "rproj (Inr x) = x"
1.5 by (auto simp:rproj_def intro: the_equality rpg.intros elim: rpg.cases)
1.6
1.7 -
1.8 -
1.9 -lemma P_imp_P: "P \<Longrightarrow> P" .
1.10 -
1.11 -
1.12 use "Tools/function_package/sum_tools.ML"
1.13 use "Tools/function_package/fundef_common.ML"
1.14 use "Tools/function_package/fundef_lib.ML"
1.15 @@ -205,16 +200,11 @@
1.16 use "Tools/function_package/mutual.ML"
1.17 use "Tools/function_package/pattern_split.ML"
1.18 use "Tools/function_package/fundef_package.ML"
1.19 +use "Tools/function_package/auto_term.ML"
1.20
1.21 setup FundefPackage.setup
1.22 -
1.23 -use "Tools/function_package/fundef_datatype.ML"
1.24 -setup FundefDatatype.setup
1.25 -
1.26 -use "Tools/function_package/auto_term.ML"
1.27 setup FundefAutoTerm.setup
1.28
1.29 -
1.30 lemmas [fundef_cong] =
1.31 let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
1.32
2.1 --- a/src/HOL/List.thy Tue Nov 07 11:47:57 2006 +0100
2.2 +++ b/src/HOL/List.thy Tue Nov 07 11:53:55 2006 +0100
2.3 @@ -2428,8 +2428,12 @@
2.4 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
2.5 by auto
2.6
2.7 +(* install the lexicographic_order method and the "fun" command *)
2.8 use "Tools/function_package/lexicographic_order.ML"
2.9 -setup {* LexicographicOrder.setup *}
2.10 +use "Tools/function_package/fundef_datatype.ML"
2.11 +setup LexicographicOrder.setup
2.12 +setup FundefDatatype.setup
2.13 +
2.14
2.15 subsubsection{*Lifting a Relation on List Elements to the Lists*}
2.16
3.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML Tue Nov 07 11:47:57 2006 +0100
3.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Tue Nov 07 11:53:55 2006 +0100
3.3 @@ -169,6 +169,9 @@
3.4 SOME (Method.Source (Args.src (("simp_all", []), Position.none))))
3.5 (* FIXME avoid dynamic scoping of method name! *)
3.6
3.7 +fun termination_by_lexicographic_order name =
3.8 + FundefPackage.setup_termination_proof (SOME name)
3.9 + #> Proof.global_terminal_proof (Method.Basic (K LexicographicOrder.lexicographic_order), NONE)
3.10
3.11 val setup =
3.12 Method.add_methods [("pat_completeness", Method.no_args pat_completeness, "Completeness prover for datatype patterns")]
3.13 @@ -184,14 +187,19 @@
3.14 val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
3.15 val statements_ow = or_list1 statement_ow
3.16
3.17 +
3.18 +fun fun_cmd fixes statements lthy =
3.19 + lthy
3.20 + |> FundefPackage.add_fundef fixes statements FundefCommon.fun_config
3.21 + ||> by_pat_completeness_simp
3.22 + (*|-> termination_by_lexicographic_order*) |> snd
3.23 +
3.24 +
3.25 val funP =
3.26 OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
3.27 ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
3.28 >> (fn ((target, fixes), statements) =>
3.29 - Toplevel.print o
3.30 - Toplevel.local_theory target
3.31 - (FundefPackage.add_fundef fixes statements FundefCommon.fun_config
3.32 - #> by_pat_completeness_simp)));
3.33 + (Toplevel.local_theory target (fun_cmd fixes statements))));
3.34
3.35 val _ = OuterSyntax.add_parsers [funP];
3.36 end
4.1 --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Nov 07 11:47:57 2006 +0100
4.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Nov 07 11:53:55 2006 +0100
4.3 @@ -13,13 +13,15 @@
4.4 -> ((bstring * Attrib.src list) * string list) list list
4.5 -> FundefCommon.fundef_config
4.6 -> local_theory
4.7 - -> Proof.state
4.8 + -> string * Proof.state
4.9
4.10 val add_fundef_i: (string * typ option * mixfix) list
4.11 -> ((bstring * Attrib.src list) * term list) list list
4.12 -> bool
4.13 -> local_theory
4.14 - -> Proof.state
4.15 + -> string * Proof.state
4.16 +
4.17 + val setup_termination_proof : string option -> local_theory -> Proof.state
4.18
4.19 val cong_add: attribute
4.20 val cong_del: attribute
4.21 @@ -105,9 +107,9 @@
4.22
4.23 val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
4.24 in
4.25 - lthy
4.26 - |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
4.27 - |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd
4.28 + (name, lthy
4.29 + |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
4.30 + |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
4.31 end
4.32
4.33
4.34 @@ -132,7 +134,7 @@
4.35 end
4.36
4.37
4.38 -fun fundef_setup_termination_proof name_opt lthy =
4.39 +fun setup_termination_proof name_opt lthy =
4.40 let
4.41 val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt
4.42 val data = the (get_fundef_data name (Context.Proof lthy))
4.43 @@ -190,8 +192,8 @@
4.44 OuterSyntax.command "function" "define general recursive functions" K.thy_goal
4.45 ((config_parser default_config -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
4.46 >> (fn (((config, target), fixes), statements) =>
4.47 - Toplevel.print o
4.48 - Toplevel.local_theory_to_proof target (add_fundef fixes statements config)));
4.49 + Toplevel.local_theory_to_proof target (add_fundef fixes statements config #> snd)
4.50 + #> Toplevel.print));
4.51
4.52
4.53
4.54 @@ -200,7 +202,7 @@
4.55 (P.opt_locale_target -- Scan.option P.name
4.56 >> (fn (target, name) =>
4.57 Toplevel.print o
4.58 - Toplevel.local_theory_to_proof target (fundef_setup_termination_proof name)));
4.59 + Toplevel.local_theory_to_proof target (setup_termination_proof name)));
4.60
4.61
4.62 val _ = OuterSyntax.add_parsers [functionP];