src/HOL/Tools/Function/partial_function.ML
author krauss
Mon May 23 21:34:37 2011 +0200 (2011-05-23)
changeset 43080 73a1d6a7ef1d
parent 42949 618adb3584e5
child 43083 df41a5762c3d
permissions -rw-r--r--
also manage induction rule;
tuned data slot
krauss@40107
     1
(*  Title:      HOL/Tools/Function/partial_function.ML
krauss@40107
     2
    Author:     Alexander Krauss, TU Muenchen
krauss@40107
     3
krauss@40107
     4
Partial function definitions based on least fixed points in ccpos.
krauss@40107
     5
*)
krauss@40107
     6
krauss@40107
     7
signature PARTIAL_FUNCTION =
krauss@40107
     8
sig
krauss@40107
     9
  val setup: theory -> theory
krauss@43080
    10
  val init: string -> term -> term -> thm -> thm option -> declaration
krauss@40107
    11
krauss@40107
    12
  val add_partial_function: string -> (binding * typ option * mixfix) list ->
krauss@40107
    13
    Attrib.binding * term -> local_theory -> local_theory
krauss@40107
    14
krauss@40107
    15
  val add_partial_function_cmd: string -> (binding * string option * mixfix) list ->
krauss@40107
    16
    Attrib.binding * string -> local_theory -> local_theory
krauss@40107
    17
end;
krauss@40107
    18
krauss@40107
    19
krauss@40107
    20
structure Partial_Function: PARTIAL_FUNCTION =
krauss@40107
    21
struct
krauss@40107
    22
krauss@40107
    23
(*** Context Data ***)
krauss@40107
    24
krauss@43080
    25
datatype setup_data = Setup_Data of 
krauss@43080
    26
 {fixp: term,
krauss@43080
    27
  mono: term,
krauss@43080
    28
  fixp_eq: thm,
krauss@43080
    29
  fixp_induct: thm option};
krauss@43080
    30
krauss@40107
    31
structure Modes = Generic_Data
krauss@40107
    32
(
krauss@43080
    33
  type T = setup_data Symtab.table;
krauss@40107
    34
  val empty = Symtab.empty;
krauss@40107
    35
  val extend = I;
wenzelm@41472
    36
  fun merge data = Symtab.merge (K true) data;
krauss@40107
    37
)
krauss@40107
    38
krauss@43080
    39
fun init mode fixp mono fixp_eq fixp_induct phi =
krauss@40107
    40
  let
krauss@40107
    41
    val term = Morphism.term phi;
krauss@43080
    42
    val thm = Morphism.thm phi;
krauss@43080
    43
    val data' = Setup_Data 
krauss@43080
    44
      {fixp=term fixp, mono=term mono, fixp_eq=thm fixp_eq,
krauss@43080
    45
       fixp_induct=Option.map thm fixp_induct};
krauss@40107
    46
  in
krauss@42949
    47
    Modes.map (Symtab.update (mode, data'))
krauss@40107
    48
  end
krauss@40107
    49
krauss@40107
    50
val known_modes = Symtab.keys o Modes.get o Context.Proof;
krauss@40107
    51
val lookup_mode = Symtab.lookup o Modes.get o Context.Proof;
krauss@40107
    52
krauss@40107
    53
krauss@40107
    54
structure Mono_Rules = Named_Thms
krauss@40107
    55
(
krauss@40107
    56
  val name = "partial_function_mono";
krauss@40107
    57
  val description = "monotonicity rules for partial function definitions";
krauss@40107
    58
);
krauss@40107
    59
krauss@40107
    60
krauss@40107
    61
(*** Automated monotonicity proofs ***)
krauss@40107
    62
krauss@40107
    63
fun strip_cases ctac = ctac #> Seq.map snd;
krauss@40107
    64
krauss@40107
    65
(*rewrite conclusion with k-th assumtion*)
krauss@40107
    66
fun rewrite_with_asm_tac ctxt k =
krauss@40107
    67
  Subgoal.FOCUS (fn {context=ctxt', prems, ...} =>
krauss@40107
    68
    Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;
krauss@40107
    69
krauss@40107
    70
fun dest_case thy t =
krauss@40107
    71
  case strip_comb t of
krauss@40107
    72
    (Const (case_comb, _), args) =>
krauss@40107
    73
      (case Datatype.info_of_case thy case_comb of
krauss@40107
    74
         NONE => NONE
krauss@40107
    75
       | SOME {case_rewrites, ...} =>
krauss@40107
    76
           let
krauss@40107
    77
             val lhs = prop_of (hd case_rewrites)
krauss@40107
    78
               |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst;
krauss@40107
    79
             val arity = length (snd (strip_comb lhs));
krauss@40107
    80
             val conv = funpow (length args - arity) Conv.fun_conv
krauss@40107
    81
               (Conv.rewrs_conv (map mk_meta_eq case_rewrites));
krauss@40107
    82
           in
krauss@40107
    83
             SOME (nth args (arity - 1), conv)
krauss@40107
    84
           end)
krauss@40107
    85
  | _ => NONE;
krauss@40107
    86
krauss@40107
    87
(*split on case expressions*)
krauss@40107
    88
val split_cases_tac = Subgoal.FOCUS_PARAMS (fn {context=ctxt, ...} =>
krauss@40107
    89
  SUBGOAL (fn (t, i) => case t of
krauss@40107
    90
    _ $ (_ $ Abs (_, _, body)) =>
wenzelm@42361
    91
      (case dest_case (Proof_Context.theory_of ctxt) body of
krauss@40107
    92
         NONE => no_tac
krauss@40107
    93
       | SOME (arg, conv) =>
krauss@40107
    94
           let open Conv in
wenzelm@42083
    95
              if Term.is_open arg then no_tac
krauss@40107
    96
              else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
krauss@40107
    97
                THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
krauss@40107
    98
                THEN_ALL_NEW etac @{thm thin_rl}
krauss@40107
    99
                THEN_ALL_NEW (CONVERSION
krauss@40107
   100
                  (params_conv ~1 (fn ctxt' =>
krauss@40107
   101
                    arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i
krauss@40107
   102
           end)
krauss@40107
   103
  | _ => no_tac) 1);
krauss@40107
   104
krauss@40107
   105
(*monotonicity proof: apply rules + split case expressions*)
krauss@40107
   106
fun mono_tac ctxt =
krauss@40107
   107
  K (Local_Defs.unfold_tac ctxt [@{thm curry_def}])
krauss@40107
   108
  THEN' (TRY o REPEAT_ALL_NEW
krauss@40107
   109
   (resolve_tac (Mono_Rules.get ctxt)
krauss@40107
   110
     ORELSE' split_cases_tac ctxt));
krauss@40107
   111
krauss@40107
   112
krauss@40107
   113
(*** Auxiliary functions ***)
krauss@40107
   114
krauss@40107
   115
(*positional instantiation with computed type substitution.
krauss@40107
   116
  internal version of  attribute "[of s t u]".*)
krauss@40107
   117
fun cterm_instantiate' cts thm =
krauss@40107
   118
  let
krauss@40107
   119
    val thy = Thm.theory_of_thm thm;
krauss@40107
   120
    val vs = rev (Term.add_vars (prop_of thm) [])
krauss@40107
   121
      |> map (Thm.cterm_of thy o Var);
krauss@40107
   122
  in
krauss@40107
   123
    cterm_instantiate (zip_options vs cts) thm
krauss@40107
   124
  end;
krauss@40107
   125
krauss@40107
   126
(*Returns t $ u, but instantiates the type of t to make the
krauss@40107
   127
application type correct*)
krauss@40107
   128
fun apply_inst ctxt t u =
krauss@40107
   129
  let
wenzelm@42361
   130
    val thy = Proof_Context.theory_of ctxt;
krauss@40107
   131
    val T = domain_type (fastype_of t);
krauss@40107
   132
    val T' = fastype_of u;
wenzelm@42388
   133
    val subst = Sign.typ_match thy (T, T') Vartab.empty
krauss@40107
   134
      handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u])
krauss@40107
   135
  in
krauss@40107
   136
    map_types (Envir.norm_type subst) t $ u
krauss@40107
   137
  end;
krauss@40107
   138
krauss@40107
   139
fun head_conv cv ct =
krauss@40107
   140
  if can Thm.dest_comb ct then Conv.fun_conv (head_conv cv) ct else cv ct;
krauss@40107
   141
krauss@40107
   142
krauss@40107
   143
(*** currying transformation ***)
krauss@40107
   144
krauss@40107
   145
fun curry_const (A, B, C) =
krauss@40107
   146
  Const (@{const_name Product_Type.curry},
krauss@40107
   147
    [HOLogic.mk_prodT (A, B) --> C, A, B] ---> C);
krauss@40107
   148
krauss@40107
   149
fun mk_curry f =
krauss@40107
   150
  case fastype_of f of
krauss@40107
   151
    Type ("fun", [Type (_, [S, T]), U]) =>
krauss@40107
   152
      curry_const (S, T, U) $ f
krauss@40107
   153
  | T => raise TYPE ("mk_curry", [T], [f]);
krauss@40107
   154
krauss@40107
   155
(* iterated versions. Nonstandard left-nested tuples arise naturally
krauss@40107
   156
from "split o split o split"*)
krauss@40107
   157
fun curry_n arity = funpow (arity - 1) mk_curry;
krauss@40107
   158
fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_split;
krauss@40107
   159
krauss@40107
   160
val curry_uncurry_ss = HOL_basic_ss addsimps
krauss@40107
   161
  [@{thm Product_Type.curry_split}, @{thm Product_Type.split_curry}]
krauss@40107
   162
krauss@40107
   163
krauss@40107
   164
(*** partial_function definition ***)
krauss@40107
   165
krauss@40107
   166
fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy =
krauss@40107
   167
  let
krauss@43080
   168
    val setup_data = the (lookup_mode lthy mode)
krauss@40107
   169
      handle Option.Option => error (cat_lines ["Unknown mode " ^ quote mode ^ ".",
krauss@40107
   170
        "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
krauss@43080
   171
    val Setup_Data {fixp, mono, fixp_eq, fixp_induct} = setup_data;
krauss@40107
   172
krauss@40107
   173
    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
wenzelm@42495
   174
    val ((_, plain_eqn), _) = Variable.focus eqn lthy;
krauss@40107
   175
krauss@40107
   176
    val ((f_binding, fT), mixfix) = the_single fixes;
krauss@40107
   177
    val fname = Binding.name_of f_binding;
krauss@40107
   178
wenzelm@42361
   179
    val cert = cterm_of (Proof_Context.theory_of lthy);
krauss@40107
   180
    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn);
krauss@40107
   181
    val (head, args) = strip_comb lhs;
krauss@40107
   182
    val F = fold_rev lambda (head :: args) rhs;
krauss@40107
   183
krauss@40107
   184
    val arity = length args;
krauss@40107
   185
    val (aTs, bTs) = chop arity (binder_types fT);
krauss@40107
   186
krauss@40107
   187
    val tupleT = foldl1 HOLogic.mk_prodT aTs;
krauss@40107
   188
    val fT_uc = tupleT :: bTs ---> body_type fT;
krauss@40107
   189
    val f_uc = Var ((fname, 0), fT_uc);
krauss@40107
   190
    val x_uc = Var (("x", 0), tupleT);
krauss@40107
   191
    val uncurry = lambda head (uncurry_n arity head);
krauss@40107
   192
    val curry = lambda f_uc (curry_n arity f_uc);
krauss@40107
   193
krauss@40107
   194
    val F_uc =
krauss@40107
   195
      lambda f_uc (uncurry_n arity (F $ curry_n arity f_uc));
krauss@40107
   196
krauss@40107
   197
    val mono_goal = apply_inst lthy mono (lambda f_uc (F_uc $ f_uc $ x_uc))
krauss@40107
   198
      |> HOLogic.mk_Trueprop
krauss@40107
   199
      |> Logic.all x_uc;
krauss@40107
   200
krauss@40107
   201
    val mono_thm = Goal.prove_internal [] (cert mono_goal)
krauss@40107
   202
        (K (mono_tac lthy 1))
krauss@40107
   203
      |> Thm.forall_elim (cert x_uc);
krauss@40107
   204
krauss@40107
   205
    val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
krauss@40107
   206
    val f_def_binding = Binding.conceal (Binding.name (Thm.def_name fname));
krauss@40107
   207
    val ((f, (_, f_def)), lthy') = Local_Theory.define
krauss@40107
   208
      ((f_binding, mixfix), ((f_def_binding, []), f_def_rhs)) lthy;
krauss@40107
   209
krauss@40107
   210
    val eqn = HOLogic.mk_eq (list_comb (f, args),
krauss@40107
   211
        Term.betapplys (F, f :: args))
krauss@40107
   212
      |> HOLogic.mk_Trueprop;
krauss@40107
   213
krauss@40107
   214
    val unfold =
krauss@40107
   215
      (cterm_instantiate' (map (SOME o cert) [uncurry, F, curry]) fixp_eq
krauss@40107
   216
        OF [mono_thm, f_def])
krauss@40107
   217
      |> Tactic.rule_by_tactic lthy (Simplifier.simp_tac curry_uncurry_ss 1);
krauss@40107
   218
krauss@40107
   219
    val rec_rule = let open Conv in
krauss@40107
   220
      Goal.prove lthy' (map (fst o dest_Free) args) [] eqn (fn _ =>
krauss@40107
   221
        CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1
krauss@40107
   222
        THEN rtac @{thm refl} 1) end;
krauss@40107
   223
  in
krauss@40107
   224
    lthy'
krauss@40107
   225
    |> Local_Theory.note (eq_abinding, [rec_rule])
krauss@40107
   226
    |-> (fn (_, rec') =>
krauss@40180
   227
      Spec_Rules.add Spec_Rules.Equational ([f], rec')
krauss@40180
   228
      #> Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec') #> snd)
krauss@40107
   229
  end;
krauss@40107
   230
krauss@40107
   231
val add_partial_function = gen_add_partial_function Specification.check_spec;
krauss@40107
   232
val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
krauss@40107
   233
krauss@40107
   234
val mode = Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")";
krauss@40107
   235
krauss@40107
   236
val _ = Outer_Syntax.local_theory
haftmann@40186
   237
  "partial_function" "define partial function" Keyword.thy_decl
krauss@40107
   238
  ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
krauss@40107
   239
     >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
krauss@40107
   240
krauss@40107
   241
krauss@40107
   242
val setup = Mono_Rules.setup;
krauss@40107
   243
krauss@40107
   244
end