src/HOL/Tools/Function/function.ML

made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded

(*  Title:      HOL/Tools/Function/function.ML
    Author:     Alexander Krauss, TU Muenchen

Main entry points to the function package.
*)

signature FUNCTION =
sig
  include FUNCTION_DATA

  val add_function: (binding * typ option * mixfix) list ->
    (Attrib.binding * term) list -> Function_Common.function_config ->
    (Proof.context -> tactic) -> local_theory -> info * local_theory

  val add_function_cmd: (binding * string option * mixfix) list ->
    (Attrib.binding * string) list -> Function_Common.function_config ->
    (Proof.context -> tactic) -> local_theory -> info * local_theory

  val function: (binding * typ option * mixfix) list ->
    (Attrib.binding * term) list -> Function_Common.function_config ->
    local_theory -> Proof.state

  val function_cmd: (binding * string option * mixfix) list ->
    (Attrib.binding * string) list -> Function_Common.function_config ->
    local_theory -> Proof.state

  val prove_termination: term option -> tactic -> local_theory -> 
    info * local_theory
  val prove_termination_cmd: string option -> tactic -> local_theory ->
    info * local_theory

  val termination : term option -> local_theory -> Proof.state
  val termination_cmd : string option -> local_theory -> Proof.state

  val setup : theory -> theory
  val get_congs : Proof.context -> thm list

  val get_info : Proof.context -> term -> info
end


structure Function : FUNCTION =
struct

open Function_Lib
open Function_Common

val simp_attribs = map (Attrib.internal o K)
  [Simplifier.simp_add,
   Code.add_default_eqn_attribute,
   Nitpick_Simps.add]

val psimp_attribs = map (Attrib.internal o K)
  [Nitpick_Psimps.add]

fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"

fun add_simps fnames post sort extra_qualify label mod_binding moreatts
  simps lthy =
  let
    val spec = post simps
      |> map (apfst (apsnd (fn ats => moreatts @ ats)))
      |> map (apfst (apfst extra_qualify))

    val (saved_spec_simps, lthy) =
      fold_map Local_Theory.note spec lthy

    val saved_simps = maps snd saved_spec_simps
    val simps_by_f = sort saved_simps

    fun add_for_f fname simps =
      Local_Theory.note
        ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
      #> snd
  in
    (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
  end

fun prepare_function is_external prep default_constraint fixspec eqns config lthy =
  let
    val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
    val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
    val fixes = map (apfst (apfst Binding.name_of)) fixes0;
    val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
    val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec

    val defname = mk_defname fixes
    val FunctionConfig {partials, default, ...} = config
    val _ =
      if is_some default then Output.legacy_feature
        "'function (default)'. Use 'partial_function'."
      else ()

    val ((goal_state, cont), lthy') =
      Function_Mutual.prepare_function_mutual config defname fixes eqs lthy

    fun afterqed [[proof]] lthy =
      let
        val FunctionResult {fs, R, psimps, simple_pinducts,
          termination, domintros, cases, ...} =
          cont (Thm.close_derivation proof)

        val fnames = map (fst o fst) fixes
        fun qualify n = Binding.name n
          |> Binding.qualify true defname
        val conceal_partial = if partials then I else Binding.conceal

        val addsmps = add_simps fnames post sort_cont

        val (((psimps', pinducts'), (_, [termination'])), lthy) =
          lthy
          |> addsmps (conceal_partial o Binding.qualify false "partial")
               "psimps" conceal_partial psimp_attribs psimps
          ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
                 [Attrib.internal (K (Rule_Cases.case_names cnames)),
                  Attrib.internal (K (Rule_Cases.consumes 1)),
                  Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
          ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
          ||> (snd o Local_Theory.note ((qualify "cases",
                 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
          ||> (case domintros of NONE => I | SOME thms => 
                   Local_Theory.note ((qualify "domintros", []), thms) #> snd)

        val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
          pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
          fs=fs, R=R, defname=defname, is_partial=true }

        val _ =
          if not is_external then ()
          else Specification.print_consts lthy (K false) (map fst fixes)
      in
        (info, 
         lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
      end
  in
    ((goal_state, afterqed), lthy')
  end

fun gen_add_function is_external prep default_constraint fixspec eqns config tac lthy =
  let
    val ((goal_state, afterqed), lthy') =
      prepare_function is_external prep default_constraint fixspec eqns config lthy
    val pattern_thm =
      case SINGLE (tac lthy') goal_state of
        NONE => error "pattern completeness and compatibility proof failed"
      | SOME st => Goal.finish lthy' st
  in
    lthy'
    |> afterqed [[pattern_thm]]
  end

val add_function =
  gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
val add_function_cmd = gen_add_function true Specification.read_spec "_::type"

fun gen_function is_external prep default_constraint fixspec eqns config lthy =
  let
    val ((goal_state, afterqed), lthy') =
      prepare_function is_external prep default_constraint fixspec eqns config lthy
  in
    lthy'
    |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
    |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
  end

val function =
  gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
val function_cmd = gen_function true Specification.read_spec "_::type"

fun prepare_termination_proof prep_term raw_term_opt lthy =
  let
    val term_opt = Option.map (prep_term lthy) raw_term_opt
    val info = the (case term_opt of
                      SOME t => (import_function_data t lthy
                        handle Option.Option =>
                          error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
                    | NONE => (import_last_function lthy handle Option.Option => error "Not a function"))

      val { termination, fs, R, add_simps, case_names, psimps,
        pinducts, defname, ...} = info
      val domT = domain_type (fastype_of R)
      val goal = HOLogic.mk_Trueprop
                   (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
      fun afterqed [[totality]] lthy =
        let
          val totality = Thm.close_derivation totality
          val remove_domain_condition =
            full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])
          val tsimps = map remove_domain_condition psimps
          val tinduct = map remove_domain_condition pinducts

          fun qualify n = Binding.name n
            |> Binding.qualify true defname
        in
          lthy
          |> add_simps I "simps" I simp_attribs tsimps
          ||>> Local_Theory.note
             ((qualify "induct",
               [Attrib.internal (K (Rule_Cases.case_names case_names))]),
              tinduct)
          |-> (fn (simps, (_, inducts)) => fn lthy =>
            let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
              case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
              simps=SOME simps, inducts=SOME inducts, termination=termination }
            in
              (info',
               lthy 
               |> Local_Theory.declaration false (add_function_data o morph_function_data info')
               |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
            end)
        end
  in
    (goal, afterqed, termination)
  end

fun gen_prove_termination prep_term raw_term_opt tac lthy =
  let
    val (goal, afterqed, termination) =
      prepare_termination_proof prep_term raw_term_opt lthy

    val totality = Goal.prove lthy [] [] goal (K tac)
  in
    afterqed [[totality]] lthy
end

val prove_termination = gen_prove_termination Syntax.check_term
val prove_termination_cmd = gen_prove_termination Syntax.read_term

fun gen_termination prep_term raw_term_opt lthy =
  let
    val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
  in
    lthy
    |> Proof_Context.note_thmss ""
       [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
    |> Proof_Context.note_thmss ""
       [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
    |> Proof_Context.note_thmss ""
       [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
         [([Goal.norm_result termination], [])])] |> snd
    |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
  end

val termination = gen_termination Syntax.check_term
val termination_cmd = gen_termination Syntax.read_term


(* Datatype hook to declare datatype congs as "function_congs" *)


fun add_case_cong n thy =
  let
    val cong = #case_cong (Datatype.the_info thy n)
      |> safe_mk_meta_eq
  in
    Context.theory_map
      (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
  end

val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))


(* setup *)

val setup =
  Attrib.setup @{binding fundef_cong}
    (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
    "declaration of congruence rule for function definitions"
  #> setup_case_cong
  #> Function_Relation.setup
  #> Function_Common.Termination_Simps.setup

val get_congs = Function_Ctx_Tree.get_function_congs

fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
  |> the_single |> snd


(* outer syntax *)

val _ =
  Outer_Syntax.local_theory_to_proof "function" "define general recursive functions"
  Keyword.thy_goal
  (function_parser default_config
     >> (fn ((config, fixes), statements) => function_cmd fixes statements config))

val _ =
  Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
  Keyword.thy_goal
  (Scan.option Parse.term >> termination_cmd)


end