--- a/Nominal-General/nominal_library.ML	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Mon Jun 07 11:43:01 2010 +0200
@@ -48,7 +48,9 @@
   val pat_completeness_simp: thm list -> Proof.context -> tactic
   val prove_termination: Proof.context -> Function.info * local_theory
 
-  
+  (* transformations of premises in inductions *)
+  val transform_prem1: Proof.context -> string list -> thm -> thm
+  val transform_prem2: Proof.context -> string list -> thm -> thm
 end
 
 
@@ -156,7 +158,9 @@
 end
 
 
-(** function package **)
+
+(** function package tactics **)
+
 fun pat_completeness_auto lthy =
   Pat_Completeness.pat_completeness_tac lthy 1
     THEN auto_tac (clasimpset_of lthy)
@@ -173,6 +177,77 @@
   Function.prove_termination NONE
     (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
 
+
+(** transformations of premises (in inductive proofs) **)
+
+(* 
+ given the theorem F[t]; proves the theorem F[f t] 
+
+  - F needs to be monotone
+  - f returns either SOME for a term it fires on 
+    and NONE elsewhere 
+*)
+fun map_term f t = 
+  (case f t of
+     NONE => map_term' f t 
+   | x => x)
+and map_term' f (t $ u) = 
+    (case (map_term f t, map_term f u) of
+        (NONE, NONE) => NONE
+      | (SOME t'', NONE) => SOME (t'' $ u)
+      | (NONE, SOME u'') => SOME (t $ u'')
+      | (SOME t'', SOME u'') => SOME (t'' $ u''))
+  | map_term' f (Abs (s, T, t)) = 
+      (case map_term f t of
+        NONE => NONE
+      | SOME t'' => SOME (Abs (s, T, t'')))
+  | map_term' _ _  = NONE;
+
+fun map_thm_tac ctxt tac thm =
+let
+  val monos = Inductive.get_monos ctxt
+  val simps = HOL_basic_ss addsimps @{thms split_def}
+in
+  EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, 
+    REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)),
+    REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
+end
+
+fun map_thm ctxt f tac thm =
+let
+  val opt_goal_trm = map_term f (prop_of thm)
+in
+  case opt_goal_trm of
+    NONE => thm
+  | SOME goal =>
+     Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) 
+end
+
+(*
+ inductive premises can be of the form
+ R ... /\ P ...; split_conj_i picks out
+ the part R or P part
+*)
+fun split_conj1 names (Const ("op &", _) $ f1 $ f2) = 
+  (case head_of f1 of
+     Const (name, _) => if member (op =) names name then SOME f1 else NONE
+   | _ => NONE)
+| split_conj1 _ _ = NONE;
+
+fun split_conj2 names (Const ("op &", _) $ f1 $ f2) = 
+  (case head_of f1 of
+     Const (name, _) => if member (op =) names name then SOME f2 else NONE
+   | _ => NONE)
+| split_conj2 _ _ = NONE;
+
+fun transform_prem1 ctxt names thm =
+  map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm
+
+fun transform_prem2 ctxt names thm =
+  map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm
+
+
+
 end (* structure *)
 
 open Nominal_Library;
\ No newline at end of file