--- a/Nominal/nominal_library.ML	Tue Dec 28 00:20:50 2010 +0000
+++ b/Nominal/nominal_library.ML	Tue Dec 28 19:51:25 2010 +0000
@@ -116,8 +116,10 @@
   val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
 
   (* tactics for function package *)
+  val size_simpset: simpset
   val pat_completeness_simp: thm list -> Proof.context -> tactic
-  val prove_termination: thm list -> Proof.context -> Function.info * local_theory
+  val prove_termination_ind: Proof.context -> int -> tactic
+  val prove_termination_fun: thm list -> Proof.context -> Function.info * local_theory
 
   (* transformations of premises in inductions *)
   val transform_prem1: Proof.context -> string list -> thm -> thm
@@ -473,45 +475,69 @@
       THEN ALLGOALS (asm_full_simp_tac simp_set)
   end
 
+(* simpset for size goals *)
+val size_simpset = HOL_ss
+   addsimprocs Nat_Numeral_Simprocs.cancel_numerals
+   addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral 
+     zero_less_Suc prod.size(1) mult_Suc_right}
 
-fun prove_termination_tac size_simps ctxt =
+val natT = @{typ nat}
+    
+fun prod_size_const T1 T2 = 
   let
-    val natT = @{typ nat}
-    fun prod_size_const fT sT = 
-      let
-        val fT_fun = fT --> natT
-        val sT_fun = sT --> natT
-        val prodT = Type (@{type_name prod}, [fT, sT])
-      in
-        Const (@{const_name prod_size}, [fT_fun, sT_fun, prodT] ---> natT)
-      end
+    val T1_fun = T1 --> natT
+    val T2_fun = T2 --> natT
+    val prodT = HOLogic.mk_prodT (T1, T2)
+  in
+    Const (@{const_name prod_size}, [T1_fun, T2_fun, prodT] ---> natT)
+  end
+
+fun snd_const T1 T2 =
+  Const ("Product_Type.snd", HOLogic.mk_prodT (T1, T2) --> T2) 
+
 
+fun mk_measure_trm f ctxt T = 
+  HOLogic.dest_setT T
+  |> fst o HOLogic.dest_prodT
+  |> f
+  |> curry (op $) (Const (@{const_name "measure"}, dummyT))
+  |> Syntax.check_term ctxt
+  
+(* wf-goal arising in induction_schema *)    
+fun prove_termination_ind ctxt =
+  let
     fun mk_size_measure T =
       case T of    
-        (Type (@{type_name Sum_Type.sum}, [fT, sT])) =>
-           SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT)
-      | (Type (@{type_name Product_Type.prod}, [fT, sT])) =>
-           prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT)
+        (Type (@{type_name Sum_Type.sum}, [T1, T2])) =>
+           SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2)
+      | (Type (@{type_name Product_Type.prod}, [T1, T2])) =>
+           HOLogic.mk_comp (mk_size_measure T2, snd_const T1 T2)
       | _ => HOLogic.size_const T
 
-    fun mk_measure_trm T = 
-      HOLogic.dest_setT T
-      |> fst o HOLogic.dest_prodT
-      |> mk_size_measure 
-      |> curry (op $) (Const (@{const_name "measure"}, dummyT))
-      |> Syntax.check_term ctxt
-      
-    val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral 
-      zero_less_Suc prod.size(1) mult_Suc_right} @ size_simps 
-    val ss' = ss addsimprocs Nat_Numeral_Simprocs.cancel_numerals
-  in
-    Function_Relation.relation_tac ctxt mk_measure_trm
-    THEN_ALL_NEW simp_tac ss'
+    val measure_trm = mk_measure_trm (mk_size_measure) ctxt
+  in 
+    Function_Relation.relation_tac ctxt measure_trm
   end
 
-fun prove_termination size_simps ctxt = 
-  Function.prove_termination NONE 
-    (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt
+(* wf-goal arising in function definitions *)
+fun prove_termination_fun size_simps ctxt =
+let
+  fun mk_size_measure T =
+    case T of    
+      (Type (@{type_name Sum_Type.sum}, [T1, T2])) =>
+         SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2)
+    | (Type (@{type_name Product_Type.prod}, [T1, T2])) =>
+         prod_size_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2)
+    | _ => HOLogic.size_const T
+
+  val measure_trm = mk_measure_trm (mk_size_measure) ctxt
+
+  val tac = 
+    Function_Relation.relation_tac ctxt measure_trm
+    THEN_ALL_NEW simp_tac (size_simpset addsimps size_simps)
+  in 
+    Function.prove_termination NONE (HEADGOAL tac) ctxt
+  end
 
 (** transformations of premises (in inductive proofs) **)