# HG changeset patch
# User dixon
# Date 1094129400 -7200
# Node ID e0cd537c43258edb1f6f5675d6bbab6385b657ad
# Parent  e7d4d3314f4c504b73d2f7697b5fd26f49228a59
added code to make use of case splitting to prove the specification equations for recursive definitions.

diff -r e7d4d3314f4c -r e0cd537c4325 TFL/post.ML
--- a/TFL/post.ML	Thu Sep 02 11:29:06 2004 +0200
+++ b/TFL/post.ML	Thu Sep 02 14:50:00 2004 +0200
@@ -203,7 +203,8 @@
 together and say that they must be true to solve the general case,
 but that would hide from the user which sub-case they were related
 to. Probably this is not important, and it would work fine, but, for now, I
-prefer leaving more fine-grain control to the user. *)
+prefer leaving more fine-grain control to the user. 
+-- Lucas Dixon, Aug 2004 *)
 local
   fun get_related_thms i = 
       mapfilter ((fn (r,x) => if x = i then Some r else None));
@@ -212,11 +213,13 @@
       raise ERROR_MESSAGE "derive_init_eqs: missing rules"
     | solve_eq (th, [a], i) = [(a, i)]
     | solve_eq (th, splitths as (_ :: _), i) = 
+      (writeln "Proving unsplit equation...";
       [((standard o ObjectLogic.rulify_no_asm)
-          (CaseSplit.splitto splitths th), i)]
+          (CaseSplit.splitto splitths th), i)])
       (* if there's an error, pretend nothing happened with this definition 
          We should probably print something out so that the user knows...? *)
-      handle ERROR_MESSAGE _ => map (fn x => (x,i)) splitths; 
+      handle ERROR_MESSAGE s => 
+             (writeln ("WARNING:post.ML:solve_eq: " ^ s); map (fn x => (x,i)) splitths); 
 in
 fun derive_init_eqs sgn rules eqs = 
     let 
@@ -237,7 +240,12 @@
 fun define_i strict thy cs ss congs wfs fid R eqs =
   let val {functional,pats} = Prim.mk_functional thy eqs
       val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
-  in (thy, simplify_defn strict thy cs ss congs wfs fid pats def) end;
+      val {induct, rules, tcs} = 
+          simplify_defn strict thy cs ss congs wfs fid pats def
+      val rules' = 
+          if strict then derive_init_eqs (Theory.sign_of thy) rules eqs
+          else rules
+  in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
 
 fun define strict thy cs ss congs wfs fid R seqs =
   define_i strict thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)