src/HOL/Tools/Function/function.ML

 
   val function_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> Function_Common.function_config ->
     bool -> local_theory -> Proof.state
 
-  val prove_termination: term option -> tactic -> local_theory -> 
+  val prove_termination: term option -> tactic -> local_theory ->
     info * local_theory
   val prove_termination_cmd: string option -> tactic -> local_theory ->
     info * local_theory
 
   val termination : term option -> local_theory -> Proof.state

     val ((goal_state, cont), lthy') =
       Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
 
     fun afterqed [[proof]] lthy =
       let
+        val result = cont (Thm.close_derivation proof)
         val FunctionResult {fs, R, dom, psimps, simple_pinducts,
-          termination, domintros, cases, ...} =
-          cont (Thm.close_derivation proof)
+                termination, domintros, cases, ...} = result
+
+        val pelims = Function_Elims.mk_partial_elim_rules lthy result
 
         val fnames = map (fst o fst) fixes
         fun qualify n = Binding.name n
           |> Binding.qualify true defname
         val conceal_partial = if partials then I else Binding.conceal
 
         val addsmps = add_simps fnames post sort_cont
 
-        val ((((psimps', [pinducts']), [termination']), [cases']), lthy) =
+        (* TODO: case names *)
+        fun addcases lthy =
+          let fun go name thm (thms_acc, lthy) =
+                 case Local_Theory.note ((Binding.name "cases" |> Binding.qualify true name,
+                          [Attrib.internal (K (Rule_Cases.case_names cnames))]), [thm]) lthy
+                 of ((_,thms), lthy') => (thms :: thms_acc, lthy')
+              val (thms, lthy') = fold2 go fnames cases ([], lthy);
+          in
+            (rev thms, lthy')
+          end;
+
+        fun addpelims lthy =
+          let fun go name thm (thms_acc, lthy) =
+                 case Local_Theory.note ((Binding.name "pelims" |> Binding.qualify true name,
+                          [Attrib.internal (K (Rule_Cases.consumes 1)),
+                           Attrib.internal (K (Rule_Cases.constraints 1))]), thm) lthy
+                 of ((_,thms), lthy') => (thms :: thms_acc, lthy')
+              val (thms, lthy') = fold2 go fnames pelims ([], lthy);
+          in
+            (rev thms, lthy')
+          end;
+
+          val (((((psimps', [pinducts']), [termination']), cases'), pelims'), lthy) =
           lthy
           |> addsmps (conceal_partial o Binding.qualify false "partial")
                "psimps" conceal_partial psimp_attribs psimps
           ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []),
                 simple_pinducts |> map (fn th => ([th],
                  [Attrib.internal (K (Rule_Cases.case_names cnames)),
                   Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
                   Attrib.internal (K (Induct.induct_pred ""))])))]
           ||>> (apfst snd o Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]))
-          ||>> (apfst snd o Local_Theory.note ((qualify "cases",
-                 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
-          ||> (case domintros of NONE => I | SOME thms => 
+          ||>> addcases
+          ||>> addpelims
+          ||> (case domintros of NONE => I | SOME thms =>
                    Local_Theory.note ((qualify "domintros", []), thms) #> snd)
 
-        val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
+        val info = { add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
-          fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=cases'}
+          fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
+          pelims=pelims',elims=NONE}
 
         val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
       in
         (info,
          lthy |> Local_Theory.declaration {syntax = false, pervasive = false}

           (case import_last_function lthy of
             SOME info => info
           | NONE => error "Not a function"))
 
     val { termination, fs, R, add_simps, case_names, psimps,
-      pinducts, defname, cases, dom, ...} = info
+      pinducts, defname, fnames, cases, dom, pelims, ...} = info
     val domT = domain_type (fastype_of R)
     val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
     fun afterqed [[totality]] lthy =
       let
         val totality = Thm.close_derivation totality
         val remove_domain_condition =
           full_simplify (put_simpset HOL_basic_ss lthy
             addsimps [totality, @{thm True_implies_equals}])
         val tsimps = map remove_domain_condition psimps
         val tinduct = map remove_domain_condition pinducts
+        val telims = map (map remove_domain_condition) pelims
 
         fun qualify n = Binding.name n
           |> Binding.qualify true defname
+
+        fun addtelims lthy =
+          let fun go name thm (thms_acc, lthy) =
+                 case Local_Theory.note ((Binding.name "elims" |> Binding.qualify true name,
+                          [Attrib.internal (K (Rule_Cases.consumes 1)),
+                           Attrib.internal (K (Rule_Cases.constraints 1)),
+                           Attrib.internal (K (Induct.cases_pred defname))]), thm) lthy
+                 of ((_,thms), lthy') => (thms :: thms_acc, lthy')
+              val (thms, lthy') = fold2 go fnames telims ([], lthy);
+          in
+            (rev thms, lthy')
+          end;
+
       in
         lthy
         |> add_simps I "simps" I simp_attribs tsimps
         ||>> Local_Theory.note
            ((qualify "induct",
              [Attrib.internal (K (Rule_Cases.case_names case_names))]),
             tinduct)
-        |-> (fn (simps, (_, inducts)) => fn lthy =>
-          let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
+        ||>> addtelims
+        |-> (fn ((simps,(_,inducts)), elims) => fn lthy =>
+          let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
             case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
-            simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases }
+            simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases, pelims=pelims, elims=SOME elims}
           in
             (info',
-             lthy 
+             lthy
              |> Local_Theory.declaration {syntax = false, pervasive = false}
                (add_function_data o transform_function_data info')
              |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
           end)
       end