# HG changeset patch
# User krauss
# Date 1262470738 -3600
# Node ID da4d7d40f2f97ed511559ec5fd0962a23dc8e4d6
# Parent  b0d21ae2528e4ae9e34e2d9e6b3ca5a112c892c4
provide simp and induct rules in Function.info

diff -r b0d21ae2528e -r da4d7d40f2f9 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/function.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -110,8 +110,8 @@
             ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros
 
           val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
-            pinducts=snd pinducts', termination=termination', fs=fs, R=R,
-            defname=defname, is_partial=true }
+            pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
+            fs=fs, R=R, defname=defname, is_partial=true }
 
           val _ =
             if not is_external then ()
@@ -151,19 +151,22 @@
             val tsimps = map remove_domain_condition psimps
             val tinduct = map remove_domain_condition pinducts
 
-            val info' = { is_partial=false, defname=defname, add_simps=add_simps,
-              case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
-              termination=termination }
             fun qualify n = Binding.name n
               |> Binding.qualify true defname
           in
             lthy
-            |> add_simps I "simps" I simp_attribs tsimps |> snd
-            |> Local_Theory.note
+            |> add_simps I "simps" I simp_attribs tsimps
+            ||>> Local_Theory.note
                ((qualify "induct",
                  [Attrib.internal (K (Rule_Cases.case_names case_names))]),
-                tinduct) |> snd
-            |> Local_Theory.declaration false (add_function_data o morph_function_data info')
+                tinduct)
+            |-> (fn (simps, (_, inducts)) =>
+              let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
+                case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
+                simps=SOME simps, inducts=SOME inducts, termination=termination }
+              in
+                Local_Theory.declaration false (add_function_data o morph_function_data info')
+              end)
           end
     in
       lthy
diff -r b0d21ae2528e -r da4d7d40f2f9 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -19,6 +19,8 @@
   R : term,
   psimps: thm list,
   pinducts: thm list,
+  simps : thm list option,
+  inducts : thm list option,
   termination: thm
  }  
 
@@ -38,6 +40,8 @@
   R : term,
   psimps: thm list,
   pinducts: thm list,
+  simps : thm list option,
+  inducts : thm list option,
   termination: thm
  }  
 
@@ -99,14 +103,15 @@
      }
 
 fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
-  termination, defname, is_partial} : info) phi =
+  simps, inducts, termination, defname, is_partial} : info) phi =
     let
       val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
       val name = Binding.name_of o Morphism.binding phi o Binding.name
     in
       { add_simps = add_simps, case_names = case_names,
         fs = map term fs, R = term R, psimps = fact psimps, 
-        pinducts = fact pinducts, termination = thm termination,
+        pinducts = fact pinducts, simps = Option.map fact simps,
+        inducts = Option.map fact inducts, termination = thm termination,
         defname = name defname, is_partial=is_partial }
     end