src/HOL/Tools/function_package/termination.ML
author haftmann
Wed Jun 07 16:55:39 2006 +0200 (2006-06-07)
changeset 19818 5c5c1208a3fa
parent 19806 f860b7a98445
child 20270 3abe7dae681e
permissions -rw-r--r--
adding case theorems for code generator
krauss@19564
     1
(*  Title:      HOL/Tools/function_package/termination.ML
krauss@19564
     2
    ID:         $Id$
krauss@19564
     3
    Author:     Alexander Krauss, TU Muenchen
krauss@19564
     4
krauss@19564
     5
A package for general recursive function definitions. 
krauss@19564
     6
Termination goals...
krauss@19564
     7
*)
krauss@19564
     8
krauss@19564
     9
krauss@19564
    10
signature FUNDEF_TERMINATION =
krauss@19564
    11
sig
krauss@19770
    12
    val mk_total_termination_goal : FundefCommon.result_with_names -> term
krauss@19770
    13
    val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
krauss@19564
    14
end
krauss@19564
    15
krauss@19564
    16
structure FundefTermination : FUNDEF_TERMINATION =
krauss@19564
    17
struct
krauss@19564
    18
krauss@19564
    19
krauss@19564
    20
open FundefCommon
krauss@19564
    21
open FundefAbbrev
krauss@19564
    22
krauss@19770
    23
fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _, _) =
krauss@19564
    24
    let
krauss@19564
    25
	val domT = domain_type (fastype_of f)
krauss@19564
    26
	val x = Free ("x", domT)
krauss@19564
    27
    in
krauss@19564
    28
	Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
krauss@19564
    29
    end
krauss@19564
    30
krauss@19770
    31
fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _, _) dom =
krauss@19564
    32
    let
krauss@19564
    33
	val domT = domain_type (fastype_of f)
wenzelm@19806
    34
	val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
krauss@19564
    35
	val DT = type_of D
krauss@19564
    36
	val idomT = HOLogic.dest_setT DT
krauss@19564
    37
krauss@19564
    38
	val x = Free ("x", idomT)
krauss@19564
    39
	val z = Free ("z", idomT)
krauss@19564
    40
	val Rname = fst (dest_Const R)
krauss@19564
    41
	val iRT = mk_relT (idomT, idomT)
krauss@19564
    42
	val iR = Const (Rname, iRT)
krauss@19564
    43
		
krauss@19564
    44
krauss@19564
    45
	val subs = HOLogic.mk_Trueprop 
krauss@19564
    46
			 (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
krauss@19564
    47
				(Const (acc_const_name, iRT --> DT) $ iR))
krauss@19564
    48
			 |> Type.freeze
krauss@19564
    49
krauss@19564
    50
	val dcl = mk_forall x
krauss@19564
    51
			    (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
krauss@19564
    52
							    Logic.mk_implies (mk_relmem (z, x) iR,
krauss@19564
    53
									      Trueprop (mk_mem (z, D))))))
krauss@19564
    54
			    |> Type.freeze
krauss@19564
    55
    in
krauss@19564
    56
	(subs, dcl)
krauss@19564
    57
    end
krauss@19564
    58
krauss@19564
    59
end
krauss@19564
    60
krauss@19564
    61
krauss@19564
    62
krauss@19564
    63