diff -r 83990a42a068 -r 2bbdb9c427b5 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Tue Aug 17 18:17:53 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Wed Aug 18 00:19:15 2010 +0800
@@ -12,6 +12,9 @@
 
   val size_const: typ -> term 
 
+  val sum_case_const: typ -> typ -> typ -> term
+  val mk_sum_case: term -> term -> term
+ 
   val mk_minus: term -> term
   val mk_plus: term -> term -> term
 
@@ -51,7 +54,7 @@
 
   (* tactics for function package *)
   val pat_completeness_simp: thm list -> Proof.context -> tactic
-  val prove_termination: Proof.context -> Function.info * local_theory
+  val prove_termination: thm list -> Proof.context -> Function.info * local_theory
 
   (* transformations of premises in inductions *)
   val transform_prem1: Proof.context -> string list -> thm -> thm
@@ -76,6 +79,18 @@
 
 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat})
 
+fun sum_case_const ty1 ty2 ty3 = 
+  Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
+fun mk_sum_case trm1 trm2 =
+let
+  val ([ty1], ty3) = strip_type (fastype_of trm1)
+  val ty2 = domain_type (fastype_of trm2)
+in
+  sum_case_const ty1 ty2 ty3 $ trm1 $ trm2
+end 
+
+
+
 fun mk_minus p = @{term "uminus::perm => perm"} $ p
 
 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q
@@ -187,10 +202,29 @@
     THEN ALLGOALS (asm_full_simp_tac simp_set)
 end
 
-fun prove_termination lthy =
-  Function.prove_termination NONE
-    (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
+fun prove_termination_tac size_simps ctxt i st  =
+let
+  fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
+      SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT)
+    | mk_size_measure T = size_const T
 
+  val ((_ $ (_ $ rel)) :: tl) = prems_of st
+  val measure_trm = 
+    fastype_of rel 
+    |> HOLogic.dest_setT
+    |> 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} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals
+in
+  (Function_Relation.relation_tac ctxt measure_trm
+   THEN_ALL_NEW  simp_tac ss) i st
+end
+
+fun prove_termination size_simps ctxt = 
+  Function.prove_termination NONE 
+    (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt
 
 (** transformations of premises (in inductive proofs) **)