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