src/HOL/Tools/Function/partial_function.ML
changeset 43080 73a1d6a7ef1d
parent 42949 618adb3584e5
child 43083 df41a5762c3d
     1.1 --- a/src/HOL/Tools/Function/partial_function.ML	Mon May 30 17:55:34 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Mon May 23 21:34:37 2011 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  signature PARTIAL_FUNCTION =
     1.5  sig
     1.6    val setup: theory -> theory
     1.7 -  val init: string -> term -> term -> thm -> declaration
     1.8 +  val init: string -> term -> term -> thm -> thm option -> declaration
     1.9  
    1.10    val add_partial_function: string -> (binding * typ option * mixfix) list ->
    1.11      Attrib.binding * term -> local_theory -> local_theory
    1.12 @@ -22,18 +22,27 @@
    1.13  
    1.14  (*** Context Data ***)
    1.15  
    1.16 +datatype setup_data = Setup_Data of 
    1.17 + {fixp: term,
    1.18 +  mono: term,
    1.19 +  fixp_eq: thm,
    1.20 +  fixp_induct: thm option};
    1.21 +
    1.22  structure Modes = Generic_Data
    1.23  (
    1.24 -  type T = ((term * term) * thm) Symtab.table;
    1.25 +  type T = setup_data Symtab.table;
    1.26    val empty = Symtab.empty;
    1.27    val extend = I;
    1.28    fun merge data = Symtab.merge (K true) data;
    1.29  )
    1.30  
    1.31 -fun init mode fixp mono fixp_eq phi =
    1.32 +fun init mode fixp mono fixp_eq fixp_induct phi =
    1.33    let
    1.34      val term = Morphism.term phi;
    1.35 -    val data' = ((term fixp, term mono), Morphism.thm phi fixp_eq);
    1.36 +    val thm = Morphism.thm phi;
    1.37 +    val data' = Setup_Data 
    1.38 +      {fixp=term fixp, mono=term mono, fixp_eq=thm fixp_eq,
    1.39 +       fixp_induct=Option.map thm fixp_induct};
    1.40    in
    1.41      Modes.map (Symtab.update (mode, data'))
    1.42    end
    1.43 @@ -156,9 +165,10 @@
    1.44  
    1.45  fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy =
    1.46    let
    1.47 -    val ((fixp, mono), fixp_eq) = the (lookup_mode lthy mode)
    1.48 +    val setup_data = the (lookup_mode lthy mode)
    1.49        handle Option.Option => error (cat_lines ["Unknown mode " ^ quote mode ^ ".",
    1.50          "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
    1.51 +    val Setup_Data {fixp, mono, fixp_eq, fixp_induct} = setup_data;
    1.52  
    1.53      val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
    1.54      val ((_, plain_eqn), _) = Variable.focus eqn lthy;