# HG changeset patch
# User krauss
# Date 1306141101 -7200
# Node ID 618adb3584e513dc850e213f8c7cbf43ebca249a
# Parent  e6990acab6ff4e4cc033fe19c58797466ccdd93c
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform

diff -r e6990acab6ff -r 618adb3584e5 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun May 22 22:22:25 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon May 23 10:58:21 2011 +0200
@@ -425,6 +425,10 @@
     by (simp only: Heap_ord_def Heap_lub_def)
 qed
 
+declaration {* Partial_Function.init "heap" @{term heap.fixp_fun}
+  @{term heap.mono_body} @{thm heap.fixp_rule_uc} *}
+
+
 abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"
 
 lemma Heap_ordI:
diff -r e6990acab6ff -r 618adb3584e5 src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Sun May 22 22:22:25 2011 +0200
+++ b/src/HOL/Partial_Function.thy	Mon May 23 10:58:21 2011 +0200
@@ -16,7 +16,7 @@
 subsection {* Axiomatic setup *}
 
 text {* This techical locale constains the requirements for function
-  definitions with ccpo fixed points.  *}
+  definitions with ccpo fixed points. *}
 
 definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))"
 definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})"
@@ -169,9 +169,6 @@
 lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
 by (rule monotoneI) (rule leq_refl)
 
-declaration {* Partial_Function.init @{term fixp_fun}
-  @{term mono_body} @{thm fixp_rule_uc} *}
-
 end
 
 
@@ -226,6 +223,13 @@
   partial_function_definitions "flat_ord None" "flat_lub None"
 by (rule flat_interpretation)
 
+declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
+  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} *}
+
+declaration {* Partial_Function.init "option" @{term option.fixp_fun}
+  @{term option.mono_body} @{thm option.fixp_rule_uc} *}
+
+
 abbreviation "option_ord \<equiv> flat_ord None"
 abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
 
diff -r e6990acab6ff -r 618adb3584e5 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Sun May 22 22:22:25 2011 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon May 23 10:58:21 2011 +0200
@@ -7,7 +7,7 @@
 signature PARTIAL_FUNCTION =
 sig
   val setup: theory -> theory
-  val init: term -> term -> thm -> declaration
+  val init: string -> term -> term -> thm -> declaration
 
   val add_partial_function: string -> (binding * typ option * mixfix) list ->
     Attrib.binding * term -> local_theory -> local_theory
@@ -30,16 +30,12 @@
   fun merge data = Symtab.merge (K true) data;
 )
 
-fun init fixp mono fixp_eq phi =
+fun init mode fixp mono fixp_eq phi =
   let
     val term = Morphism.term phi;
     val data' = ((term fixp, term mono), Morphism.thm phi fixp_eq);
-    val mode = (* extract mode identifier from morphism prefix! *)
-      Binding.prefix_of (Morphism.binding phi (Binding.empty))
-      |> map fst |> space_implode ".";
   in
-    if mode = "" then I
-    else Modes.map (Symtab.update (mode, data'))
+    Modes.map (Symtab.update (mode, data'))
   end
 
 val known_modes = Symtab.keys o Modes.get o Context.Proof;