--- a/src/HOL/Tools/function_package/termination.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/termination.ML Tue Nov 07 22:06:32 2006 +0100
@@ -9,8 +9,8 @@
signature FUNDEF_TERMINATION =
sig
- val mk_total_termination_goal : FundefCommon.result_with_names -> term
- val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
+ val mk_total_termination_goal : FundefCommon.result_with_names -> term
+ val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
end
structure FundefTermination : FUNDEF_TERMINATION =
@@ -20,41 +20,40 @@
open FundefLib
open FundefCommon
open FundefAbbrev
-
+
fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _) =
let
- val domT = domain_type (fastype_of f)
- val x = Free ("x", domT)
+ val domT = domain_type (fastype_of f)
+ val x = Free ("x", domT)
in
mk_forall x (Trueprop (mk_acc domT R $ x))
end
-
+
fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
let
- val domT = domain_type (fastype_of f)
- val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
- val DT = type_of D
- val idomT = HOLogic.dest_setT DT
-
- val x = Free ("x", idomT)
- val z = Free ("z", idomT)
- val Rname = fst (dest_Const R)
- val iRT = mk_relT (idomT, idomT)
- val iR = Const (Rname, iRT)
-
+ val domT = domain_type (fastype_of f)
+ val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
+ val DT = type_of D
+ val idomT = HOLogic.dest_setT DT
+
+ val x = Free ("x", idomT)
+ val z = Free ("z", idomT)
+ val Rname = fst (dest_Const R)
+ val iRT = mk_relT (idomT, idomT)
+ val iR = Const (Rname, iRT)
+
+ val subs = HOLogic.mk_Trueprop
+ (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
+ (Const (acc_const_name, iRT --> DT) $ iR))
+ |> Type.freeze
- val subs = HOLogic.mk_Trueprop
- (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
- (Const (acc_const_name, iRT --> DT) $ iR))
- |> Type.freeze
-
- val dcl = mk_forall x
- (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
- Logic.mk_implies (mk_relmem (z, x) iR,
- Trueprop (mk_mem (z, D))))))
- |> Type.freeze
+ val dcl = mk_forall x
+ (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
+ Logic.mk_implies (mk_relmem (z, x) iR,
+ Trueprop (mk_mem (z, D))))))
+ |> Type.freeze
in
- (subs, dcl)
+ (subs, dcl)
end
end