src/HOL/Tools/function_package/termination.ML
changeset 21237 b803f9870e97
parent 21104 b6ab939147eb
child 21255 617fdb08abe9
--- 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