also manage induction rule;
authorkrauss
Mon May 23 21:34:37 2011 +0200 (2011-05-23)
changeset 4308073a1d6a7ef1d
parent 43079 4022892a2f28
child 43081 1a39c9898ae6
also manage induction rule;
tuned data slot
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Partial_Function.thy
src/HOL/Tools/Function/partial_function.ML
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon May 30 17:55:34 2011 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon May 23 21:34:37 2011 +0200
     1.3 @@ -426,7 +426,7 @@
     1.4  qed
     1.5  
     1.6  declaration {* Partial_Function.init "heap" @{term heap.fixp_fun}
     1.7 -  @{term heap.mono_body} @{thm heap.fixp_rule_uc} *}
     1.8 +  @{term heap.mono_body} @{thm heap.fixp_rule_uc} NONE *}
     1.9  
    1.10  
    1.11  abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"
     2.1 --- a/src/HOL/Partial_Function.thy	Mon May 30 17:55:34 2011 +0200
     2.2 +++ b/src/HOL/Partial_Function.thy	Mon May 23 21:34:37 2011 +0200
     2.3 @@ -224,10 +224,10 @@
     2.4  by (rule flat_interpretation)
     2.5  
     2.6  declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
     2.7 -  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} *}
     2.8 +  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *}
     2.9  
    2.10  declaration {* Partial_Function.init "option" @{term option.fixp_fun}
    2.11 -  @{term option.mono_body} @{thm option.fixp_rule_uc} *}
    2.12 +  @{term option.mono_body} @{thm option.fixp_rule_uc} NONE *}
    2.13  
    2.14  
    2.15  abbreviation "option_ord \<equiv> flat_ord None"
     3.1 --- a/src/HOL/Tools/Function/partial_function.ML	Mon May 30 17:55:34 2011 +0200
     3.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Mon May 23 21:34:37 2011 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  signature PARTIAL_FUNCTION =
     3.5  sig
     3.6    val setup: theory -> theory
     3.7 -  val init: string -> term -> term -> thm -> declaration
     3.8 +  val init: string -> term -> term -> thm -> thm option -> declaration
     3.9  
    3.10    val add_partial_function: string -> (binding * typ option * mixfix) list ->
    3.11      Attrib.binding * term -> local_theory -> local_theory
    3.12 @@ -22,18 +22,27 @@
    3.13  
    3.14  (*** Context Data ***)
    3.15  
    3.16 +datatype setup_data = Setup_Data of 
    3.17 + {fixp: term,
    3.18 +  mono: term,
    3.19 +  fixp_eq: thm,
    3.20 +  fixp_induct: thm option};
    3.21 +
    3.22  structure Modes = Generic_Data
    3.23  (
    3.24 -  type T = ((term * term) * thm) Symtab.table;
    3.25 +  type T = setup_data Symtab.table;
    3.26    val empty = Symtab.empty;
    3.27    val extend = I;
    3.28    fun merge data = Symtab.merge (K true) data;
    3.29  )
    3.30  
    3.31 -fun init mode fixp mono fixp_eq phi =
    3.32 +fun init mode fixp mono fixp_eq fixp_induct phi =
    3.33    let
    3.34      val term = Morphism.term phi;
    3.35 -    val data' = ((term fixp, term mono), Morphism.thm phi fixp_eq);
    3.36 +    val thm = Morphism.thm phi;
    3.37 +    val data' = Setup_Data 
    3.38 +      {fixp=term fixp, mono=term mono, fixp_eq=thm fixp_eq,
    3.39 +       fixp_induct=Option.map thm fixp_induct};
    3.40    in
    3.41      Modes.map (Symtab.update (mode, data'))
    3.42    end
    3.43 @@ -156,9 +165,10 @@
    3.44  
    3.45  fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy =
    3.46    let
    3.47 -    val ((fixp, mono), fixp_eq) = the (lookup_mode lthy mode)
    3.48 +    val setup_data = the (lookup_mode lthy mode)
    3.49        handle Option.Option => error (cat_lines ["Unknown mode " ^ quote mode ^ ".",
    3.50          "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
    3.51 +    val Setup_Data {fixp, mono, fixp_eq, fixp_induct} = setup_data;
    3.52  
    3.53      val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
    3.54      val ((_, plain_eqn), _) = Variable.focus eqn lthy;