src/HOL/Tools/Function/partial_function.ML
author haftmann
Tue Oct 13 09:21:15 2015 +0200 (2015-10-13)
changeset 61424 c3658c18b7bc
parent 61121 efe8b18306b7
child 61841 4d3527b94f2a
permissions -rw-r--r--
prod_case as canonical name for product type eliminator
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@52728
     9
  val init: string -> term -> term -> thm -> thm -> thm option -> declaration
krauss@52727
    10
  val mono_tac: Proof.context -> int -> tactic
krauss@40107
    11
  val add_partial_function: string -> (binding * typ option * mixfix) list ->
krauss@40107
    12
    Attrib.binding * term -> local_theory -> local_theory
krauss@40107
    13
  val add_partial_function_cmd: string -> (binding * string option * mixfix) list ->
krauss@40107
    14
    Attrib.binding * string -> local_theory -> local_theory
krauss@40107
    15
end;
krauss@40107
    16
krauss@40107
    17
structure Partial_Function: PARTIAL_FUNCTION =
krauss@40107
    18
struct
krauss@40107
    19
krauss@40107
    20
(*** Context Data ***)
krauss@40107
    21
wenzelm@61113
    22
datatype setup_data = Setup_Data of
krauss@43080
    23
 {fixp: term,
krauss@43080
    24
  mono: term,
krauss@43080
    25
  fixp_eq: thm,
krauss@52728
    26
  fixp_induct: thm,
krauss@52728
    27
  fixp_induct_user: thm option};
krauss@43080
    28
wenzelm@61113
    29
fun transform_setup_data phi (Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user}) =
wenzelm@61113
    30
  let
wenzelm@61113
    31
    val term = Morphism.term phi;
wenzelm@61113
    32
    val thm = Morphism.thm phi;
wenzelm@61113
    33
  in
wenzelm@61113
    34
    Setup_Data
wenzelm@61113
    35
     {fixp = term fixp, mono = term mono, fixp_eq = thm fixp_eq,
wenzelm@61113
    36
      fixp_induct = thm fixp_induct, fixp_induct_user = Option.map thm fixp_induct_user}
wenzelm@61113
    37
  end;
wenzelm@61113
    38
krauss@40107
    39
structure Modes = Generic_Data
krauss@40107
    40
(
krauss@43080
    41
  type T = setup_data Symtab.table;
krauss@40107
    42
  val empty = Symtab.empty;
krauss@40107
    43
  val extend = I;
wenzelm@41472
    44
  fun merge data = Symtab.merge (K true) data;
krauss@40107
    45
)
krauss@40107
    46
krauss@52728
    47
fun init mode fixp mono fixp_eq fixp_induct fixp_induct_user phi =
krauss@40107
    48
  let
wenzelm@61113
    49
    val data' =
wenzelm@61113
    50
      Setup_Data
wenzelm@61113
    51
       {fixp = fixp, mono = mono, fixp_eq = fixp_eq,
wenzelm@61113
    52
        fixp_induct = fixp_induct, fixp_induct_user = fixp_induct_user}
wenzelm@61113
    53
      |> transform_setup_data (phi $> Morphism.trim_context_morphism);
wenzelm@61113
    54
  in Modes.map (Symtab.update (mode, data')) end;
krauss@40107
    55
krauss@40107
    56
val known_modes = Symtab.keys o Modes.get o Context.Proof;
wenzelm@61113
    57
wenzelm@61113
    58
fun lookup_mode ctxt =
wenzelm@61113
    59
  Symtab.lookup (Modes.get (Context.Proof ctxt))
wenzelm@61113
    60
  #> Option.map (transform_setup_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
krauss@40107
    61
krauss@40107
    62
krauss@40107
    63
(*** Automated monotonicity proofs ***)
krauss@40107
    64
krauss@40107
    65
fun strip_cases ctac = ctac #> Seq.map snd;
krauss@40107
    66
krauss@40107
    67
(*rewrite conclusion with k-th assumtion*)
krauss@40107
    68
fun rewrite_with_asm_tac ctxt k =
wenzelm@45403
    69
  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
krauss@40107
    70
    Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;
krauss@40107
    71
blanchet@54405
    72
fun dest_case ctxt t =
krauss@40107
    73
  case strip_comb t of
krauss@40107
    74
    (Const (case_comb, _), args) =>
blanchet@54405
    75
      (case Ctr_Sugar.ctr_sugar_of_case ctxt case_comb of
krauss@40107
    76
         NONE => NONE
blanchet@54405
    77
       | SOME {case_thms, ...} =>
krauss@40107
    78
           let
wenzelm@59582
    79
             val lhs = Thm.prop_of (hd case_thms)
krauss@40107
    80
               |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst;
krauss@40107
    81
             val arity = length (snd (strip_comb lhs));
krauss@40107
    82
             val conv = funpow (length args - arity) Conv.fun_conv
blanchet@54405
    83
               (Conv.rewrs_conv (map mk_meta_eq case_thms));
krauss@40107
    84
           in
krauss@40107
    85
             SOME (nth args (arity - 1), conv)
krauss@40107
    86
           end)
krauss@40107
    87
  | _ => NONE;
krauss@40107
    88
krauss@40107
    89
(*split on case expressions*)
wenzelm@59498
    90
val split_cases_tac = Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} =>
krauss@40107
    91
  SUBGOAL (fn (t, i) => case t of
krauss@40107
    92
    _ $ (_ $ Abs (_, _, body)) =>
blanchet@54405
    93
      (case dest_case ctxt body of
krauss@40107
    94
         NONE => no_tac
krauss@40107
    95
       | SOME (arg, conv) =>
krauss@40107
    96
           let open Conv in
wenzelm@42083
    97
              if Term.is_open arg then no_tac
krauss@40107
    98
              else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
krauss@40107
    99
                THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
wenzelm@59498
   100
                THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl}
krauss@40107
   101
                THEN_ALL_NEW (CONVERSION
krauss@40107
   102
                  (params_conv ~1 (fn ctxt' =>
krauss@40107
   103
                    arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i
krauss@40107
   104
           end)
krauss@40107
   105
  | _ => no_tac) 1);
krauss@40107
   106
krauss@40107
   107
(*monotonicity proof: apply rules + split case expressions*)
krauss@40107
   108
fun mono_tac ctxt =
krauss@40107
   109
  K (Local_Defs.unfold_tac ctxt [@{thm curry_def}])
krauss@40107
   110
  THEN' (TRY o REPEAT_ALL_NEW
wenzelm@59498
   111
   (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems partial_function_mono}))
krauss@40107
   112
     ORELSE' split_cases_tac ctxt));
krauss@40107
   113
krauss@40107
   114
krauss@40107
   115
(*** Auxiliary functions ***)
krauss@40107
   116
krauss@40107
   117
(*Returns t $ u, but instantiates the type of t to make the
krauss@40107
   118
application type correct*)
krauss@40107
   119
fun apply_inst ctxt t u =
krauss@40107
   120
  let
wenzelm@42361
   121
    val thy = Proof_Context.theory_of ctxt;
krauss@40107
   122
    val T = domain_type (fastype_of t);
krauss@40107
   123
    val T' = fastype_of u;
wenzelm@42388
   124
    val subst = Sign.typ_match thy (T, T') Vartab.empty
krauss@40107
   125
      handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u])
krauss@40107
   126
  in
krauss@40107
   127
    map_types (Envir.norm_type subst) t $ u
krauss@40107
   128
  end;
krauss@40107
   129
krauss@40107
   130
fun head_conv cv ct =
krauss@40107
   131
  if can Thm.dest_comb ct then Conv.fun_conv (head_conv cv) ct else cv ct;
krauss@40107
   132
krauss@40107
   133
krauss@40107
   134
(*** currying transformation ***)
krauss@40107
   135
krauss@40107
   136
fun curry_const (A, B, C) =
krauss@40107
   137
  Const (@{const_name Product_Type.curry},
krauss@40107
   138
    [HOLogic.mk_prodT (A, B) --> C, A, B] ---> C);
krauss@40107
   139
krauss@40107
   140
fun mk_curry f =
krauss@40107
   141
  case fastype_of f of
krauss@40107
   142
    Type ("fun", [Type (_, [S, T]), U]) =>
krauss@40107
   143
      curry_const (S, T, U) $ f
krauss@40107
   144
  | T => raise TYPE ("mk_curry", [T], [f]);
krauss@40107
   145
krauss@40107
   146
(* iterated versions. Nonstandard left-nested tuples arise naturally
krauss@40107
   147
from "split o split o split"*)
krauss@40107
   148
fun curry_n arity = funpow (arity - 1) mk_curry;
haftmann@61424
   149
fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_case_prod;
krauss@40107
   150
wenzelm@51717
   151
val curry_uncurry_ss =
wenzelm@51717
   152
  simpset_of (put_simpset HOL_basic_ss @{context}
haftmann@61424
   153
    addsimps [@{thm Product_Type.curry_case_prod}, @{thm Product_Type.case_prod_curry}])
krauss@40107
   154
wenzelm@51717
   155
val split_conv_ss =
wenzelm@51717
   156
  simpset_of (put_simpset HOL_basic_ss @{context}
wenzelm@51717
   157
    addsimps [@{thm Product_Type.split_conv}]);
krauss@43083
   158
Andreas@54630
   159
val curry_K_ss =
Andreas@54630
   160
  simpset_of (put_simpset HOL_basic_ss @{context}
Andreas@54630
   161
    addsimps [@{thm Product_Type.curry_K}]);
krauss@52728
   162
krauss@52728
   163
(* instantiate generic fixpoint induction and eliminate the canonical assumptions;
krauss@52728
   164
  curry induction predicate *)
krauss@52728
   165
fun specialize_fixp_induct ctxt args fT fT_uc F curry uncurry mono_thm f_def rule =
krauss@52728
   166
  let
krauss@52728
   167
    val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
krauss@52728
   168
    val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
wenzelm@61113
   169
  in
wenzelm@54742
   170
    (* FIXME ctxt vs. ctxt' (!?) *)
krauss@52728
   171
    rule
wenzelm@60784
   172
    |> infer_instantiate' ctxt
wenzelm@60784
   173
      ((map o Option.map) (Thm.cterm_of ctxt) [SOME uncurry, NONE, SOME curry, NONE, SOME P_inst])
krauss@52728
   174
    |> Tactic.rule_by_tactic ctxt
krauss@52728
   175
      (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 (* discharge U (C f) = f *)
Andreas@54630
   176
       THEN Simplifier.simp_tac (put_simpset curry_K_ss ctxt) 4 (* simplify bot case *)
Andreas@54630
   177
       THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
krauss@52728
   178
    |> (fn thm => thm OF [mono_thm, f_def])
krauss@52728
   179
    |> Conv.fconv_rule (Conv.concl_conv ~1    (* simplify conclusion *)
haftmann@61424
   180
         (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
krauss@52728
   181
    |> singleton (Variable.export ctxt' ctxt)
krauss@52728
   182
  end
krauss@52728
   183
krauss@52727
   184
fun mk_curried_induct args ctxt inst_rule =
krauss@43083
   185
  let
wenzelm@59621
   186
    val cert = Thm.cterm_of ctxt
krauss@43083
   187
    val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
krauss@43083
   188
krauss@43083
   189
    val split_paired_all_conv =
krauss@43083
   190
      Conv.every_conv (replicate (length args - 1) (Conv.rewr_conv @{thm split_paired_all}))
krauss@43083
   191
wenzelm@61113
   192
    val split_params_conv =
krauss@43083
   193
      Conv.params_conv ~1 (fn ctxt' =>
krauss@43083
   194
        Conv.implies_conv split_paired_all_conv Conv.all_conv)
krauss@43083
   195
krauss@52521
   196
    val (P_var, x_var) =
krauss@51484
   197
       Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop
krauss@52521
   198
      |> strip_comb |> apsnd hd
wenzelm@60642
   199
      |> apply2 dest_Var
wenzelm@60642
   200
    val P_rangeT = range_type (snd P_var)
krauss@51484
   201
    val PT = map (snd o dest_Free) args ---> P_rangeT
krauss@43083
   202
    val x_inst = cert (foldl1 HOLogic.mk_prod args)
krauss@43083
   203
    val P_inst = cert (uncurry_n (length args) (Free (P, PT)))
krauss@43083
   204
krauss@43083
   205
    val inst_rule' = inst_rule
krauss@43083
   206
      |> Tactic.rule_by_tactic ctxt
wenzelm@51717
   207
        (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 4
wenzelm@51717
   208
         THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3
krauss@43083
   209
         THEN CONVERSION (split_params_conv ctxt
krauss@43083
   210
           then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3)
wenzelm@60642
   211
      |> Thm.instantiate ([], [(P_var, P_inst), (x_var, x_inst)])
wenzelm@51717
   212
      |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt)
krauss@43083
   213
      |> singleton (Variable.export ctxt' ctxt)
krauss@43083
   214
  in
krauss@43083
   215
    inst_rule'
krauss@43083
   216
  end;
wenzelm@61113
   217
krauss@40107
   218
krauss@40107
   219
(*** partial_function definition ***)
krauss@40107
   220
krauss@40107
   221
fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy =
krauss@40107
   222
  let
krauss@43080
   223
    val setup_data = the (lookup_mode lthy mode)
krauss@40107
   224
      handle Option.Option => error (cat_lines ["Unknown mode " ^ quote mode ^ ".",
krauss@40107
   225
        "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
krauss@52728
   226
    val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data;
krauss@40107
   227
krauss@40107
   228
    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
wenzelm@60695
   229
    val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy;
krauss@40107
   230
krauss@40107
   231
    val ((f_binding, fT), mixfix) = the_single fixes;
krauss@40107
   232
    val fname = Binding.name_of f_binding;
krauss@40107
   233
krauss@40107
   234
    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn);
krauss@40107
   235
    val (head, args) = strip_comb lhs;
krauss@43083
   236
    val argnames = map (fst o dest_Free) args;
krauss@40107
   237
    val F = fold_rev lambda (head :: args) rhs;
krauss@40107
   238
krauss@40107
   239
    val arity = length args;
krauss@40107
   240
    val (aTs, bTs) = chop arity (binder_types fT);
krauss@40107
   241
krauss@40107
   242
    val tupleT = foldl1 HOLogic.mk_prodT aTs;
krauss@40107
   243
    val fT_uc = tupleT :: bTs ---> body_type fT;
krauss@40107
   244
    val f_uc = Var ((fname, 0), fT_uc);
krauss@40107
   245
    val x_uc = Var (("x", 0), tupleT);
krauss@40107
   246
    val uncurry = lambda head (uncurry_n arity head);
krauss@40107
   247
    val curry = lambda f_uc (curry_n arity f_uc);
krauss@40107
   248
krauss@40107
   249
    val F_uc =
krauss@40107
   250
      lambda f_uc (uncurry_n arity (F $ curry_n arity f_uc));
krauss@40107
   251
krauss@40107
   252
    val mono_goal = apply_inst lthy mono (lambda f_uc (F_uc $ f_uc $ x_uc))
krauss@40107
   253
      |> HOLogic.mk_Trueprop
krauss@40107
   254
      |> Logic.all x_uc;
krauss@40107
   255
wenzelm@60784
   256
    val mono_thm = Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal)
krauss@40107
   257
        (K (mono_tac lthy 1))
wenzelm@60784
   258
    val inst_mono_thm = Thm.forall_elim (Thm.cterm_of lthy x_uc) mono_thm
krauss@40107
   259
krauss@40107
   260
    val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
wenzelm@61121
   261
    val f_def_binding =
wenzelm@61121
   262
      if Config.get lthy Function_Lib.function_defs then (Binding.name (Thm.def_name fname), [])
wenzelm@61121
   263
      else Attrib.empty_binding;
krauss@40107
   264
    val ((f, (_, f_def)), lthy') = Local_Theory.define
wenzelm@61121
   265
      ((f_binding, mixfix), (f_def_binding, f_def_rhs)) lthy;
krauss@40107
   266
krauss@40107
   267
    val eqn = HOLogic.mk_eq (list_comb (f, args),
krauss@40107
   268
        Term.betapplys (F, f :: args))
krauss@40107
   269
      |> HOLogic.mk_Trueprop;
krauss@40107
   270
krauss@40107
   271
    val unfold =
wenzelm@60784
   272
      (infer_instantiate' lthy' (map (SOME o Thm.cterm_of lthy') [uncurry, F, curry]) fixp_eq
krauss@52727
   273
        OF [inst_mono_thm, f_def])
wenzelm@52087
   274
      |> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1);
krauss@40107
   275
wenzelm@61113
   276
    val specialized_fixp_induct =
krauss@52728
   277
      specialize_fixp_induct lthy' args fT fT_uc F curry uncurry inst_mono_thm f_def fixp_induct
krauss@52728
   278
      |> Drule.rename_bvars' (map SOME (fname :: fname :: argnames));
krauss@52728
   279
krauss@43083
   280
    val mk_raw_induct =
wenzelm@60784
   281
      infer_instantiate' args_ctxt
wenzelm@60784
   282
        ((map o Option.map) (Thm.cterm_of args_ctxt) [SOME uncurry, NONE, SOME curry])
krauss@52727
   283
      #> mk_curried_induct args args_ctxt
wenzelm@52087
   284
      #> singleton (Variable.export args_ctxt lthy')
wenzelm@60784
   285
      #> (fn thm => infer_instantiate' lthy'
wenzelm@60784
   286
          [SOME (Thm.cterm_of lthy' F)] thm OF [inst_mono_thm, f_def])
krauss@43083
   287
      #> Drule.rename_bvars' (map SOME (fname :: argnames @ argnames))
krauss@43083
   288
krauss@52728
   289
    val raw_induct = Option.map mk_raw_induct fixp_induct_user
krauss@40107
   290
    val rec_rule = let open Conv in
krauss@40107
   291
      Goal.prove lthy' (map (fst o dest_Free) args) [] eqn (fn _ =>
krauss@40107
   292
        CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1
wenzelm@59498
   293
        THEN resolve_tac lthy' @{thms refl} 1) end;
krauss@40107
   294
  in
krauss@40107
   295
    lthy'
krauss@40107
   296
    |> Local_Theory.note (eq_abinding, [rec_rule])
krauss@40107
   297
    |-> (fn (_, rec') =>
krauss@40180
   298
      Spec_Rules.add Spec_Rules.Equational ([f], rec')
krauss@40180
   299
      #> Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec') #> snd)
wenzelm@61113
   300
    |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "mono"), []), [mono_thm]) #> snd)
krauss@43083
   301
    |> (case raw_induct of NONE => I | SOME thm =>
krauss@43083
   302
         Local_Theory.note ((Binding.qualify true fname (Binding.name "raw_induct"), []), [thm]) #> snd)
wenzelm@61113
   303
    |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "fixp_induct"), []), [specialized_fixp_induct]) #> snd)
krauss@40107
   304
  end;
krauss@40107
   305
krauss@40107
   306
val add_partial_function = gen_add_partial_function Specification.check_spec;
krauss@40107
   307
val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
krauss@40107
   308
wenzelm@46949
   309
val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
krauss@40107
   310
wenzelm@46961
   311
val _ =
wenzelm@59936
   312
  Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
wenzelm@46961
   313
    ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
wenzelm@46961
   314
      >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
krauss@40107
   315
wenzelm@61113
   316
end;