first version of partial_function package
authorkrauss
Sat Oct 23 23:41:19 2010 +0200 (2010-10-23)
changeset 40107374f3ef9f940
parent 40106 c58951943cba
child 40108 dbab949c2717
first version of partial_function package
src/HOL/Partial_Function.thy
src/HOL/Tools/Function/partial_function.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Partial_Function.thy	Sat Oct 23 23:41:19 2010 +0200
     1.3 @@ -0,0 +1,247 @@
     1.4 +(* Title:    HOL/Partial_Function.thy
     1.5 +   Author:   Alexander Krauss, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Partial Function Definitions *}
     1.9 +
    1.10 +theory Partial_Function
    1.11 +imports Complete_Partial_Order Option
    1.12 +uses 
    1.13 +  "Tools/Function/function_lib.ML" 
    1.14 +  "Tools/Function/partial_function.ML" 
    1.15 +begin
    1.16 +
    1.17 +setup Partial_Function.setup
    1.18 +
    1.19 +subsection {* Axiomatic setup *}
    1.20 +
    1.21 +text {* This techical locale constains the requirements for function
    1.22 +  definitions with ccpo fixed points.  *}
    1.23 +
    1.24 +definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))"
    1.25 +definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})"
    1.26 +definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))"
    1.27 +definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))"
    1.28 +
    1.29 +lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)"
    1.30 +by (rule monotoneI) (auto simp: fun_ord_def)
    1.31 +
    1.32 +lemma if_mono[partial_function_mono]: "monotone orda ordb F 
    1.33 +\<Longrightarrow> monotone orda ordb G
    1.34 +\<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)"
    1.35 +unfolding monotone_def by simp
    1.36 +
    1.37 +definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)"
    1.38 +
    1.39 +locale partial_function_definitions = 
    1.40 +  fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.41 +  fixes lub :: "'a set \<Rightarrow> 'a"
    1.42 +  assumes leq_refl: "leq x x"
    1.43 +  assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z"
    1.44 +  assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y"
    1.45 +  assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)"
    1.46 +  assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> leq (lub A) z"
    1.47 +
    1.48 +lemma partial_function_lift:
    1.49 +  assumes "partial_function_definitions ord lb"
    1.50 +  shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf")
    1.51 +proof -
    1.52 +  interpret partial_function_definitions ord lb by fact
    1.53 +
    1.54 +  { fix A a assume A: "chain ?ordf A"
    1.55 +    have "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
    1.56 +    proof (rule chainI)
    1.57 +      fix x y assume "x \<in> ?C" "y \<in> ?C"
    1.58 +      then obtain f g where fg: "f \<in> A" "g \<in> A" 
    1.59 +        and [simp]: "x = f a" "y = g a" by blast
    1.60 +      from chainD[OF A fg]
    1.61 +      show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
    1.62 +    qed }
    1.63 +  note chain_fun = this
    1.64 +
    1.65 +  show ?thesis
    1.66 +  proof
    1.67 +    fix x show "?ordf x x"
    1.68 +      unfolding fun_ord_def by (auto simp: leq_refl)
    1.69 +  next
    1.70 +    fix x y z assume "?ordf x y" "?ordf y z"
    1.71 +    thus "?ordf x z" unfolding fun_ord_def 
    1.72 +      by (force dest: leq_trans)
    1.73 +  next
    1.74 +    fix x y assume "?ordf x y" "?ordf y x"
    1.75 +    thus "x = y" unfolding fun_ord_def
    1.76 +      by (force intro!: ext dest: leq_antisym)
    1.77 +  next
    1.78 +    fix A f assume f: "f \<in> A" and A: "chain ?ordf A"
    1.79 +    thus "?ordf f (?lubf A)"
    1.80 +      unfolding fun_lub_def fun_ord_def
    1.81 +      by (blast intro: lub_upper chain_fun[OF A] f)
    1.82 +  next
    1.83 +    fix A :: "('b \<Rightarrow> 'a) set" and g :: "'b \<Rightarrow> 'a"
    1.84 +    assume A: "chain ?ordf A" and g: "\<And>f. f \<in> A \<Longrightarrow> ?ordf f g"
    1.85 +    show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def
    1.86 +      by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def])
    1.87 +   qed
    1.88 +qed
    1.89 +
    1.90 +lemma ccpo: assumes "partial_function_definitions ord lb"
    1.91 +  shows "class.ccpo ord (mk_less ord) lb"
    1.92 +using assms unfolding partial_function_definitions_def mk_less_def
    1.93 +by unfold_locales blast+
    1.94 +
    1.95 +lemma partial_function_image:
    1.96 +  assumes "partial_function_definitions ord Lub"
    1.97 +  assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
    1.98 +  assumes inv: "\<And>x. f (g x) = x"
    1.99 +  shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)"
   1.100 +proof -
   1.101 +  let ?iord = "img_ord f ord"
   1.102 +  let ?ilub = "img_lub f g Lub"
   1.103 +
   1.104 +  interpret partial_function_definitions ord Lub by fact
   1.105 +  show ?thesis
   1.106 +  proof
   1.107 +    fix A x assume "chain ?iord A" "x \<in> A"
   1.108 +    then have "chain ord (f ` A)" "f x \<in> f ` A"
   1.109 +      by (auto simp: img_ord_def intro: chainI dest: chainD)
   1.110 +    thus "?iord x (?ilub A)"
   1.111 +      unfolding inv img_lub_def img_ord_def by (rule lub_upper)
   1.112 +  next
   1.113 +    fix A x assume "chain ?iord A"
   1.114 +      and 1: "\<And>z. z \<in> A \<Longrightarrow> ?iord z x"
   1.115 +    then have "chain ord (f ` A)"
   1.116 +      by (auto simp: img_ord_def intro: chainI dest: chainD)
   1.117 +    thus "?iord (?ilub A) x"
   1.118 +      unfolding inv img_lub_def img_ord_def
   1.119 +      by (rule lub_least) (auto dest: 1[unfolded img_ord_def])
   1.120 +  qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj)
   1.121 +qed
   1.122 +
   1.123 +context partial_function_definitions
   1.124 +begin
   1.125 +
   1.126 +abbreviation "le_fun \<equiv> fun_ord leq"
   1.127 +abbreviation "lub_fun \<equiv> fun_lub lub"
   1.128 +abbreviation "fixp_fun == ccpo.fixp le_fun lub_fun"
   1.129 +abbreviation "mono_body \<equiv> monotone le_fun leq"
   1.130 +
   1.131 +text {* Interpret manually, to avoid flooding everything with facts about
   1.132 +  orders *}
   1.133 +
   1.134 +lemma ccpo: "class.ccpo le_fun (mk_less le_fun) lub_fun"
   1.135 +apply (rule ccpo)
   1.136 +apply (rule partial_function_lift)
   1.137 +apply (rule partial_function_definitions_axioms)
   1.138 +done
   1.139 +
   1.140 +text {* The crucial fixed-point theorem *}
   1.141 +
   1.142 +lemma mono_body_fixp: 
   1.143 +  "(\<And>x. mono_body (\<lambda>f. F f x)) \<Longrightarrow> fixp_fun F = F (fixp_fun F)"
   1.144 +by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def)
   1.145 +
   1.146 +text {* Version with curry/uncurry combinators, to be used by package *}
   1.147 +
   1.148 +lemma fixp_rule_uc:
   1.149 +  fixes F :: "'c \<Rightarrow> 'c" and
   1.150 +    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
   1.151 +    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
   1.152 +  assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
   1.153 +  assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
   1.154 +  assumes inverse: "\<And>f. C (U f) = f"
   1.155 +  shows "f = F f"
   1.156 +proof -
   1.157 +  have "f = C (fixp_fun (\<lambda>f. U (F (C f))))" by (simp add: eq)
   1.158 +  also have "... = C (U (F (C (fixp_fun (\<lambda>f. U (F (C f)))))))"
   1.159 +    by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl)
   1.160 +  also have "... = F (C (fixp_fun (\<lambda>f. U (F (C f)))))" by (rule inverse)
   1.161 +  also have "... = F f" by (simp add: eq)
   1.162 +  finally show "f = F f" .
   1.163 +qed
   1.164 +
   1.165 +text {* Rules for @{term mono_body}: *}
   1.166 +
   1.167 +lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
   1.168 +by (rule monotoneI) (rule leq_refl)
   1.169 +
   1.170 +declaration {* Partial_Function.init @{term fixp_fun}
   1.171 +  @{term mono_body} @{thm fixp_rule_uc} *}
   1.172 +
   1.173 +end
   1.174 +
   1.175 +
   1.176 +subsection {* Flat interpretation: tailrec and option *}
   1.177 +
   1.178 +definition 
   1.179 +  "flat_ord b x y \<longleftrightarrow> x = b \<or> x = y"
   1.180 +
   1.181 +definition 
   1.182 +  "flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> A - {b}))"
   1.183 +
   1.184 +lemma flat_interpretation:
   1.185 +  "partial_function_definitions (flat_ord b) (flat_lub b)"
   1.186 +proof
   1.187 +  fix A x assume 1: "chain (flat_ord b) A" "x \<in> A"
   1.188 +  show "flat_ord b x (flat_lub b A)"
   1.189 +  proof cases
   1.190 +    assume "x = b"
   1.191 +    thus ?thesis by (simp add: flat_ord_def)
   1.192 +  next
   1.193 +    assume "x \<noteq> b"
   1.194 +    with 1 have "A - {b} = {x}"
   1.195 +      by (auto elim: chainE simp: flat_ord_def)
   1.196 +    then have "flat_lub b A = x"
   1.197 +      by (auto simp: flat_lub_def)
   1.198 +    thus ?thesis by (auto simp: flat_ord_def)
   1.199 +  qed
   1.200 +next
   1.201 +  fix A z assume A: "chain (flat_ord b) A"
   1.202 +    and z: "\<And>x. x \<in> A \<Longrightarrow> flat_ord b x z"
   1.203 +  show "flat_ord b (flat_lub b A) z"
   1.204 +  proof cases
   1.205 +    assume "A \<subseteq> {b}"
   1.206 +    thus ?thesis
   1.207 +      by (auto simp: flat_lub_def flat_ord_def)
   1.208 +  next
   1.209 +    assume nb: "\<not> A \<subseteq> {b}"
   1.210 +    then obtain y where y: "y \<in> A" "y \<noteq> b" by auto
   1.211 +    with A have "A - {b} = {y}"
   1.212 +      by (auto elim: chainE simp: flat_ord_def)
   1.213 +    with nb have "flat_lub b A = y"
   1.214 +      by (auto simp: flat_lub_def)
   1.215 +    with z y show ?thesis by auto    
   1.216 +  qed
   1.217 +qed (auto simp: flat_ord_def)
   1.218 +
   1.219 +interpretation tailrec!:
   1.220 +  partial_function_definitions "flat_ord undefined" "flat_lub undefined"
   1.221 +by (rule flat_interpretation)
   1.222 +
   1.223 +interpretation option!:
   1.224 +  partial_function_definitions "flat_ord None" "flat_lub None"
   1.225 +by (rule flat_interpretation)
   1.226 +
   1.227 +abbreviation "option_ord \<equiv> flat_ord None"
   1.228 +abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
   1.229 +
   1.230 +lemma bind_mono[partial_function_mono]:
   1.231 +assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)"
   1.232 +shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))"
   1.233 +proof (rule monotoneI)
   1.234 +  fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g"
   1.235 +  with mf
   1.236 +  have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
   1.237 +  then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))"
   1.238 +    unfolding flat_ord_def by auto    
   1.239 +  also from mg
   1.240 +  have "\<And>y'. option_ord (C y' f) (C y' g)"
   1.241 +    by (rule monotoneD) (rule fg)
   1.242 +  then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))"
   1.243 +    unfolding flat_ord_def by (cases "B g") auto
   1.244 +  finally (option.leq_trans)
   1.245 +  show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
   1.246 +qed
   1.247 +
   1.248 +
   1.249 +end
   1.250 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Sat Oct 23 23:41:19 2010 +0200
     2.3 @@ -0,0 +1,238 @@
     2.4 +(*  Title:      HOL/Tools/Function/partial_function.ML
     2.5 +    Author:     Alexander Krauss, TU Muenchen
     2.6 +
     2.7 +Partial function definitions based on least fixed points in ccpos.
     2.8 +*)
     2.9 +
    2.10 +signature PARTIAL_FUNCTION =
    2.11 +sig
    2.12 +  val setup: theory -> theory
    2.13 +  val init: term -> term -> thm -> declaration
    2.14 +
    2.15 +  val add_partial_function: string -> (binding * typ option * mixfix) list ->
    2.16 +    Attrib.binding * term -> local_theory -> local_theory
    2.17 +
    2.18 +  val add_partial_function_cmd: string -> (binding * string option * mixfix) list ->
    2.19 +    Attrib.binding * string -> local_theory -> local_theory
    2.20 +end;
    2.21 +
    2.22 +
    2.23 +structure Partial_Function: PARTIAL_FUNCTION =
    2.24 +struct
    2.25 +
    2.26 +(*** Context Data ***)
    2.27 +
    2.28 +structure Modes = Generic_Data
    2.29 +(
    2.30 +  type T = ((term * term) * thm) Symtab.table;
    2.31 +  val empty = Symtab.empty;
    2.32 +  val extend = I;
    2.33 +  fun merge (a, b) = Symtab.merge (K true) (a, b);
    2.34 +)
    2.35 +
    2.36 +fun init fixp mono fixp_eq phi =
    2.37 +  let
    2.38 +    val term = Morphism.term phi;
    2.39 +    val data' = ((term fixp, term mono), Morphism.thm phi fixp_eq);
    2.40 +    val mode = (* extract mode identifier from morphism prefix! *)
    2.41 +      Binding.prefix_of (Morphism.binding phi (Binding.empty))
    2.42 +      |> map fst |> space_implode ".";
    2.43 +  in
    2.44 +    if mode = "" then I
    2.45 +    else Modes.map (Symtab.update (mode, data'))
    2.46 +  end
    2.47 +
    2.48 +val known_modes = Symtab.keys o Modes.get o Context.Proof;
    2.49 +val lookup_mode = Symtab.lookup o Modes.get o Context.Proof;
    2.50 +
    2.51 +
    2.52 +structure Mono_Rules = Named_Thms
    2.53 +(
    2.54 +  val name = "partial_function_mono";
    2.55 +  val description = "monotonicity rules for partial function definitions";
    2.56 +);
    2.57 +
    2.58 +
    2.59 +(*** Automated monotonicity proofs ***)
    2.60 +
    2.61 +fun strip_cases ctac = ctac #> Seq.map snd;
    2.62 +
    2.63 +(*rewrite conclusion with k-th assumtion*)
    2.64 +fun rewrite_with_asm_tac ctxt k =
    2.65 +  Subgoal.FOCUS (fn {context=ctxt', prems, ...} =>
    2.66 +    Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;
    2.67 +
    2.68 +fun dest_case thy t =
    2.69 +  case strip_comb t of
    2.70 +    (Const (case_comb, _), args) =>
    2.71 +      (case Datatype.info_of_case thy case_comb of
    2.72 +         NONE => NONE
    2.73 +       | SOME {case_rewrites, ...} =>
    2.74 +           let
    2.75 +             val lhs = prop_of (hd case_rewrites)
    2.76 +               |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst;
    2.77 +             val arity = length (snd (strip_comb lhs));
    2.78 +             val conv = funpow (length args - arity) Conv.fun_conv
    2.79 +               (Conv.rewrs_conv (map mk_meta_eq case_rewrites));
    2.80 +           in
    2.81 +             SOME (nth args (arity - 1), conv)
    2.82 +           end)
    2.83 +  | _ => NONE;
    2.84 +
    2.85 +(*split on case expressions*)
    2.86 +val split_cases_tac = Subgoal.FOCUS_PARAMS (fn {context=ctxt, ...} =>
    2.87 +  SUBGOAL (fn (t, i) => case t of
    2.88 +    _ $ (_ $ Abs (_, _, body)) =>
    2.89 +      (case dest_case (ProofContext.theory_of ctxt) body of
    2.90 +         NONE => no_tac
    2.91 +       | SOME (arg, conv) =>
    2.92 +           let open Conv in
    2.93 +              if not (null (loose_bnos arg)) then no_tac
    2.94 +              else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
    2.95 +                THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
    2.96 +                THEN_ALL_NEW etac @{thm thin_rl}
    2.97 +                THEN_ALL_NEW (CONVERSION
    2.98 +                  (params_conv ~1 (fn ctxt' =>
    2.99 +                    arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i
   2.100 +           end)
   2.101 +  | _ => no_tac) 1);
   2.102 +
   2.103 +(*monotonicity proof: apply rules + split case expressions*)
   2.104 +fun mono_tac ctxt =
   2.105 +  K (Local_Defs.unfold_tac ctxt [@{thm curry_def}])
   2.106 +  THEN' (TRY o REPEAT_ALL_NEW
   2.107 +   (resolve_tac (Mono_Rules.get ctxt)
   2.108 +     ORELSE' split_cases_tac ctxt));
   2.109 +
   2.110 +
   2.111 +(*** Auxiliary functions ***)
   2.112 +
   2.113 +(*positional instantiation with computed type substitution.
   2.114 +  internal version of  attribute "[of s t u]".*)
   2.115 +fun cterm_instantiate' cts thm =
   2.116 +  let
   2.117 +    val thy = Thm.theory_of_thm thm;
   2.118 +    val vs = rev (Term.add_vars (prop_of thm) [])
   2.119 +      |> map (Thm.cterm_of thy o Var);
   2.120 +  in
   2.121 +    cterm_instantiate (zip_options vs cts) thm
   2.122 +  end;
   2.123 +
   2.124 +(*Returns t $ u, but instantiates the type of t to make the
   2.125 +application type correct*)
   2.126 +fun apply_inst ctxt t u =
   2.127 +  let
   2.128 +    val thy = ProofContext.theory_of ctxt;
   2.129 +    val T = domain_type (fastype_of t);
   2.130 +    val T' = fastype_of u;
   2.131 +    val subst = Type.typ_match (Sign.tsig_of thy) (T, T') Vartab.empty
   2.132 +      handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u])
   2.133 +  in
   2.134 +    map_types (Envir.norm_type subst) t $ u
   2.135 +  end;
   2.136 +
   2.137 +fun head_conv cv ct =
   2.138 +  if can Thm.dest_comb ct then Conv.fun_conv (head_conv cv) ct else cv ct;
   2.139 +
   2.140 +
   2.141 +(*** currying transformation ***)
   2.142 +
   2.143 +fun curry_const (A, B, C) =
   2.144 +  Const (@{const_name Product_Type.curry},
   2.145 +    [HOLogic.mk_prodT (A, B) --> C, A, B] ---> C);
   2.146 +
   2.147 +fun mk_curry f =
   2.148 +  case fastype_of f of
   2.149 +    Type ("fun", [Type (_, [S, T]), U]) =>
   2.150 +      curry_const (S, T, U) $ f
   2.151 +  | T => raise TYPE ("mk_curry", [T], [f]);
   2.152 +
   2.153 +(* iterated versions. Nonstandard left-nested tuples arise naturally
   2.154 +from "split o split o split"*)
   2.155 +fun curry_n arity = funpow (arity - 1) mk_curry;
   2.156 +fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_split;
   2.157 +
   2.158 +val curry_uncurry_ss = HOL_basic_ss addsimps
   2.159 +  [@{thm Product_Type.curry_split}, @{thm Product_Type.split_curry}]
   2.160 +
   2.161 +
   2.162 +(*** partial_function definition ***)
   2.163 +
   2.164 +fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy =
   2.165 +  let
   2.166 +    val ((fixp, mono), fixp_eq) = the (lookup_mode lthy mode)
   2.167 +      handle Option.Option => error (cat_lines ["Unknown mode " ^ quote mode ^ ".",
   2.168 +        "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
   2.169 +
   2.170 +    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
   2.171 +    val (_, _, plain_eqn) = Function_Lib.dest_all_all_ctx lthy eqn;
   2.172 +
   2.173 +    val ((f_binding, fT), mixfix) = the_single fixes;
   2.174 +    val fname = Binding.name_of f_binding;
   2.175 +
   2.176 +    val cert = cterm_of (ProofContext.theory_of lthy);
   2.177 +    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn);
   2.178 +    val (head, args) = strip_comb lhs;
   2.179 +    val F = fold_rev lambda (head :: args) rhs;
   2.180 +
   2.181 +    val arity = length args;
   2.182 +    val (aTs, bTs) = chop arity (binder_types fT);
   2.183 +
   2.184 +    val tupleT = foldl1 HOLogic.mk_prodT aTs;
   2.185 +    val fT_uc = tupleT :: bTs ---> body_type fT;
   2.186 +    val f_uc = Var ((fname, 0), fT_uc);
   2.187 +    val x_uc = Var (("x", 0), tupleT);
   2.188 +    val uncurry = lambda head (uncurry_n arity head);
   2.189 +    val curry = lambda f_uc (curry_n arity f_uc);
   2.190 +
   2.191 +    val F_uc =
   2.192 +      lambda f_uc (uncurry_n arity (F $ curry_n arity f_uc));
   2.193 +
   2.194 +    val mono_goal = apply_inst lthy mono (lambda f_uc (F_uc $ f_uc $ x_uc))
   2.195 +      |> HOLogic.mk_Trueprop
   2.196 +      |> Logic.all x_uc;
   2.197 +
   2.198 +    val mono_thm = Goal.prove_internal [] (cert mono_goal)
   2.199 +        (K (mono_tac lthy 1))
   2.200 +      |> Thm.forall_elim (cert x_uc);
   2.201 +
   2.202 +    val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
   2.203 +    val f_def_binding = Binding.conceal (Binding.name (Thm.def_name fname));
   2.204 +    val ((f, (_, f_def)), lthy') = Local_Theory.define
   2.205 +      ((f_binding, mixfix), ((f_def_binding, []), f_def_rhs)) lthy;
   2.206 +
   2.207 +    val eqn = HOLogic.mk_eq (list_comb (f, args),
   2.208 +        Term.betapplys (F, f :: args))
   2.209 +      |> HOLogic.mk_Trueprop;
   2.210 +
   2.211 +    val unfold =
   2.212 +      (cterm_instantiate' (map (SOME o cert) [uncurry, F, curry]) fixp_eq
   2.213 +        OF [mono_thm, f_def])
   2.214 +      |> Tactic.rule_by_tactic lthy (Simplifier.simp_tac curry_uncurry_ss 1);
   2.215 +
   2.216 +    val rec_rule = let open Conv in
   2.217 +      Goal.prove lthy' (map (fst o dest_Free) args) [] eqn (fn _ =>
   2.218 +        CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1
   2.219 +        THEN rtac @{thm refl} 1) end;
   2.220 +  in
   2.221 +    lthy'
   2.222 +    |> Local_Theory.note (eq_abinding, [rec_rule])
   2.223 +    |-> (fn (_, rec') =>
   2.224 +      Local_Theory.note ((Binding.qualify true fname (Binding.name "rec"), []), rec'))
   2.225 +    |> snd
   2.226 +  end;
   2.227 +
   2.228 +val add_partial_function = gen_add_partial_function Specification.check_spec;
   2.229 +val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
   2.230 +
   2.231 +val mode = Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")";
   2.232 +
   2.233 +val _ = Outer_Syntax.local_theory
   2.234 +  "partial_function" "define partial function" Keyword.thy_goal
   2.235 +  ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
   2.236 +     >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
   2.237 +
   2.238 +
   2.239 +val setup = Mono_Rules.setup;
   2.240 +
   2.241 +end