Preparations for making "lexicographic_order" part of "fun"
authorkrauss
Tue Nov 07 11:53:55 2006 +0100 (2006-11-07)
changeset 212115370cfbf3070
parent 21210 c17fd2df4e9e
child 21212 547224bf9348
Preparations for making "lexicographic_order" part of "fun"
src/HOL/FunDef.thy
src/HOL/List.thy
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_package.ML
     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];