# HG changeset patch
# User krauss
# Date 1306179277 -7200
# Node ID 73a1d6a7ef1de05f8b6fd55acf160cff40cf62f6
# Parent  4022892a2f283eb14fc3c7aa2fa453f724cb223c
also manage induction rule;
tuned data slot

diff -r 4022892a2f28 -r 73a1d6a7ef1d src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon May 30 17:55:34 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon May 23 21:34:37 2011 +0200
@@ -426,7 +426,7 @@
 qed
 
 declaration {* Partial_Function.init "heap" @{term heap.fixp_fun}
-  @{term heap.mono_body} @{thm heap.fixp_rule_uc} *}
+  @{term heap.mono_body} @{thm heap.fixp_rule_uc} NONE *}
 
 
 abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"
diff -r 4022892a2f28 -r 73a1d6a7ef1d src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Mon May 30 17:55:34 2011 +0200
+++ b/src/HOL/Partial_Function.thy	Mon May 23 21:34:37 2011 +0200
@@ -224,10 +224,10 @@
 by (rule flat_interpretation)
 
 declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
-  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} *}
+  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *}
 
 declaration {* Partial_Function.init "option" @{term option.fixp_fun}
-  @{term option.mono_body} @{thm option.fixp_rule_uc} *}
+  @{term option.mono_body} @{thm option.fixp_rule_uc} NONE *}
 
 
 abbreviation "option_ord \<equiv> flat_ord None"
diff -r 4022892a2f28 -r 73a1d6a7ef1d src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Mon May 30 17:55:34 2011 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon May 23 21:34:37 2011 +0200
@@ -7,7 +7,7 @@
 signature PARTIAL_FUNCTION =
 sig
   val setup: theory -> theory
-  val init: string -> term -> term -> thm -> declaration
+  val init: string -> term -> term -> thm -> thm option -> declaration
 
   val add_partial_function: string -> (binding * typ option * mixfix) list ->
     Attrib.binding * term -> local_theory -> local_theory
@@ -22,18 +22,27 @@
 
 (*** Context Data ***)
 
+datatype setup_data = Setup_Data of 
+ {fixp: term,
+  mono: term,
+  fixp_eq: thm,
+  fixp_induct: thm option};
+
 structure Modes = Generic_Data
 (
-  type T = ((term * term) * thm) Symtab.table;
+  type T = setup_data Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data = Symtab.merge (K true) data;
 )
 
-fun init mode fixp mono fixp_eq phi =
+fun init mode fixp mono fixp_eq fixp_induct phi =
   let
     val term = Morphism.term phi;
-    val data' = ((term fixp, term mono), Morphism.thm phi fixp_eq);
+    val thm = Morphism.thm phi;
+    val data' = Setup_Data 
+      {fixp=term fixp, mono=term mono, fixp_eq=thm fixp_eq,
+       fixp_induct=Option.map thm fixp_induct};
   in
     Modes.map (Symtab.update (mode, data'))
   end
@@ -156,9 +165,10 @@
 
 fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy =
   let
-    val ((fixp, mono), fixp_eq) = the (lookup_mode lthy mode)
+    val setup_data = the (lookup_mode lthy mode)
       handle Option.Option => error (cat_lines ["Unknown mode " ^ quote mode ^ ".",
         "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
+    val Setup_Data {fixp, mono, fixp_eq, fixp_induct} = setup_data;
 
     val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
     val ((_, plain_eqn), _) = Variable.focus eqn lthy;