changed termination goal to use object quantifier
authorkrauss
Thu Feb 15 17:35:19 2007 +0100 (2007-02-15)
changeset 22325be61bd159a99
parent 22324 c95319d14332
child 22326 a3acee47a883
changed termination goal to use object quantifier
src/HOL/FunDef.thy
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/function_package/termination.ML
     1.1 --- a/src/HOL/FunDef.thy	Thu Feb 15 12:14:34 2007 +0100
     1.2 +++ b/src/HOL/FunDef.thy	Thu Feb 15 17:35:19 2007 +0100
     1.3 @@ -14,7 +14,6 @@
     1.4  ("Tools/function_package/inductive_wrap.ML")
     1.5  ("Tools/function_package/context_tree.ML")
     1.6  ("Tools/function_package/fundef_core.ML")
     1.7 -("Tools/function_package/termination.ML")
     1.8  ("Tools/function_package/mutual.ML")
     1.9  ("Tools/function_package/pattern_split.ML")
    1.10  ("Tools/function_package/fundef_package.ML")
    1.11 @@ -109,7 +108,6 @@
    1.12  use "Tools/function_package/inductive_wrap.ML"
    1.13  use "Tools/function_package/context_tree.ML"
    1.14  use "Tools/function_package/fundef_core.ML"
    1.15 -use "Tools/function_package/termination.ML"
    1.16  use "Tools/function_package/mutual.ML"
    1.17  use "Tools/function_package/pattern_split.ML"
    1.18  use "Tools/function_package/auto_term.ML"
     2.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Thu Feb 15 12:14:34 2007 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Thu Feb 15 17:35:19 2007 +0100
     2.3 @@ -758,8 +758,8 @@
     2.4      in
     2.5        FundefCtxTree.traverse_tree step tree
     2.6      end
     2.7 -    
     2.8 -    
     2.9 +
    2.10 +
    2.11  fun mk_nest_term_rule thy globals R R_cases clauses =
    2.12      let
    2.13        val Globals { domT, x, z, ... } = globals
    2.14 @@ -797,6 +797,8 @@
    2.15          |> forall_intr (cterm_of thy x)
    2.16          |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
    2.17          |> curry op RS (assume wfR')
    2.18 +        |> forall_intr_vars
    2.19 +        |> (fn it => it COMP allI)
    2.20          |> fold implies_intr hyps
    2.21          |> implies_intr wfR'
    2.22          |> forall_intr (cterm_of thy R')
     3.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Feb 15 12:14:34 2007 +0100
     3.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Feb 15 17:35:19 2007 +0100
     3.3 @@ -166,11 +166,14 @@
     3.4                     handle Option.Option => raise ERROR ("No such function definition: " ^ defname)
     3.5  
     3.6          val FundefCtxData {termination, R, ...} = data
     3.7 -        val goal = FundefTermination.mk_total_termination_goal R
     3.8 +        val domT = domain_type (fastype_of R)
     3.9 +        val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
    3.10      in
    3.11        lthy
    3.12 +        |> ProofContext.note_thmss_i "" [(("", [ContextRules.rule_del]), [([allI], [])])] |> snd
    3.13 +        |> ProofContext.note_thmss_i "" [(("", [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
    3.14          |> ProofContext.note_thmss_i ""
    3.15 -          [(("termination", [ContextRules.intro_query NONE]),
    3.16 +          [(("termination", [ContextRules.intro_bang (SOME 0)]),
    3.17              [([Goal.norm_result termination], [])])] |> snd
    3.18          |> set_termination_rule termination
    3.19          |> Proof.theorem_i NONE (total_termination_afterqed defname data) [[(goal, [])]]
     4.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Feb 15 12:14:34 2007 +0100
     4.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Feb 15 17:35:19 2007 +0100
     4.3 @@ -270,11 +270,11 @@
     4.4      in
     4.5        case premlist of 
     4.6              [] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal" 
     4.7 -          | (wf::tl) => let
     4.8 -    val (var, prop) = FundefLib.dest_all wf
     4.9 -    val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
    4.10 +          | (wfR::tl) => let
    4.11 +    val trueprop $ (wf $ rel) = wfR
    4.12      val crel = cterm_of thy rel
    4.13 -    val measure_funs = mk_all_measure_funs (fastype_of var)
    4.14 +    val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
    4.15 +    val measure_funs = mk_all_measure_funs domT
    4.16      val _ = writeln "Creating table"
    4.17      val table = map (mk_row thy measure_funs) tl
    4.18      val _ = writeln "Searching for lexicographic order"
    4.19 @@ -286,8 +286,8 @@
    4.20        | SOME order  => let
    4.21        val clean_table = map (fn x => map (nth x) order) table
    4.22        val funs = map (nth measure_funs) order
    4.23 -      val list = HOLogic.mk_list (fastype_of var --> HOLogic.natT) funs
    4.24 -      val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list)
    4.25 +      val list = HOLogic.mk_list (domT --> HOLogic.natT) funs
    4.26 +      val relterm = Const(measures, (fastype_of list) --> (fastype_of rel)) $ list
    4.27        val crelterm = cterm_of thy relterm
    4.28        val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
    4.29        val _ = writeln "Proving subgoals"
     5.1 --- a/src/HOL/Tools/function_package/termination.ML	Thu Feb 15 12:14:34 2007 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,64 +0,0 @@
     5.4 -(*  Title:      HOL/Tools/function_package/termination.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Alexander Krauss, TU Muenchen
     5.7 -
     5.8 -A package for general recursive function definitions. 
     5.9 -Termination goals...
    5.10 -*)
    5.11 -
    5.12 -
    5.13 -signature FUNDEF_TERMINATION =
    5.14 -sig
    5.15 -  val mk_total_termination_goal : term -> term
    5.16 -(*  val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*)
    5.17 -end
    5.18 -
    5.19 -structure FundefTermination : FUNDEF_TERMINATION =
    5.20 -struct
    5.21 -
    5.22 -
    5.23 -open FundefLib
    5.24 -open FundefCommon
    5.25 -open FundefAbbrev
    5.26 -     
    5.27 -fun mk_total_termination_goal R =
    5.28 -    let
    5.29 -      val domT = domain_type (fastype_of R)
    5.30 -      val x = Free ("x", domT)
    5.31 -    in
    5.32 -      mk_forall x (Trueprop (mk_acc domT R $ x))
    5.33 -    end
    5.34 -    
    5.35 -(*
    5.36 -fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
    5.37 -    let
    5.38 -      val domT = domain_type (fastype_of f)
    5.39 -      val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
    5.40 -      val DT = type_of D
    5.41 -      val idomT = HOLogic.dest_setT DT
    5.42 -                  
    5.43 -      val x = Free ("x", idomT)
    5.44 -      val z = Free ("z", idomT)
    5.45 -      val Rname = fst (dest_Const R)
    5.46 -      val iRT = mk_relT (idomT, idomT)
    5.47 -      val iR = Const (Rname, iRT)
    5.48 -               
    5.49 -      val subs = HOLogic.mk_Trueprop 
    5.50 -                   (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
    5.51 -                          (Const (acc_const_name, iRT --> DT) $ iR))
    5.52 -                   |> Type.freeze
    5.53 -
    5.54 -      val dcl = mk_forall x
    5.55 -                (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
    5.56 -                                                Logic.mk_implies (mk_relmem (z, x) iR,
    5.57 -                                                                  Trueprop (mk_mem (z, D))))))
    5.58 -                |> Type.freeze
    5.59 -    in
    5.60 -      (subs, dcl)
    5.61 -    end
    5.62 -*)
    5.63 -end
    5.64 -
    5.65 -
    5.66 -
    5.67 -