1 (*  Nominal Termination

     2     Author: Christian Urban

     3 

     4     heavily based on the code of Alexander Krauss

     5     (code forked on 18 July 2011)

     6 

     7 Redefinition of the termination command

     8 *)

     9 

    10 signature NOMINAL_FUNCTION_TERMINATION =

    11 sig

    12   include NOMINAL_FUNCTION_DATA

    13 

    14   val termination : term option -> local_theory -> Proof.state

    15   val termination_cmd : string option -> local_theory -> Proof.state

    16 

    17 end

    18 

    19 structure Nominal_Function_Termination : NOMINAL_FUNCTION_TERMINATION =

    20 struct

    21 

    22 open Function_Lib

    23 open Function_Common

    24 open Nominal_Function_Common

    25 

    26 val simp_attribs = map (Attrib.internal o K)

    27   [Simplifier.simp_add,

    28    Code.add_default_eqn_attribute,

    29    Nitpick_Simps.add]

    30 

    31 val eqvt_attrib =  Attrib.internal (K Nominal_ThmDecls.eqvt_add)

    32 

    33 fun prepare_termination_proof prep_term raw_term_opt lthy =

    34   let

    35     val term_opt = Option.map (prep_term lthy) raw_term_opt

    36     val info = the (case term_opt of

    37                       SOME t => (import_function_data t lthy

    38                         handle Option.Option =>

    39                           error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))

    40                     | NONE => (import_last_function lthy handle Option.Option => error "Not a function"))

    41 

    42       val { termination, fs, R, add_simps, case_names, psimps,

    43         pinducts, defname, eqvts, ...} = info

    44       val domT = domain_type (fastype_of R)

    45       val goal = HOLogic.mk_Trueprop

    46                    (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))

    47       fun afterqed [[totality]] lthy =

    48         let

    49           val totality = Thm.close_derivation totality

    50           val remove_domain_condition =

    51             full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])

    52           val tsimps = map remove_domain_condition psimps

    53           val tinduct = map remove_domain_condition pinducts

    54           val teqvts = map remove_domain_condition eqvts

    55   

    56           fun qualify n = Binding.name n

    57             |> Binding.qualify true defname

    58         in

    59           lthy

    60           |> add_simps I "simps" I simp_attribs tsimps

    61           ||>> Local_Theory.note ((qualify "eqvt", [eqvt_attrib]), teqvts)

    62           ||>> Local_Theory.note

    63              ((qualify "induct",

    64                [Attrib.internal (K (Rule_Cases.case_names case_names))]),

    65               tinduct)

    66           |-> (fn ((simps, (_, eqvts)), (_, inducts)) => fn lthy =>

    67             let val info' = { is_partial=false, defname=defname, add_simps=add_simps,

    68               case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,

    69               simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=eqvts }

    70             in

    71               (info',

    72                lthy 

    73                |> Local_Theory.declaration false (add_function_data o morph_function_data info')

    74                |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))

    75             end)

    76         end

    77   in

    78     (goal, afterqed, termination)

    79   end

    80 

    81 fun gen_termination prep_term raw_term_opt lthy =

    82   let

    83     val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy

    84   in

    85     lthy

    86     |> Proof_Context.note_thmss ""

    87        [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd

    88     |> Proof_Context.note_thmss ""

    89        [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd

    90     |> Proof_Context.note_thmss ""

    91        [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),

    92          [([Goal.norm_result termination], [])])] |> snd

    93     |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]

    94   end

    95 

    96 val termination = gen_termination Syntax.check_term

    97 val termination_cmd = gen_termination Syntax.read_term

    98 

    99 (* outer syntax *)

   100 

   101 val option_parser =

   102   (Scan.optional (Parse.$$$ "(" |-- Parse.!!! 

   103     (Parse.reserved "eqvt" >> K true) --| Parse.$$$ ")") false)

   104 

   105 val _ =

   106   Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"

   107   Keyword.thy_goal

   108   (option_parser -- Scan.option Parse.term >> 

   109      (fn (is_eqvt, trm) => 

   110         if is_eqvt then termination_cmd trm else Function.termination_cmd trm))

   111 

   112 end