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