Nominal/nominal_function.ML
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 09 Jul 2015 02:32:46 +0100
changeset 3239 67370521c09c
parent 3235 5ebd327ffb96
child 3243 c4f31f1564b7
permissions -rw-r--r--
updated for Isabelle 2015
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
(*  Nominal Mutual Functions
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
    Author:  Christian Urban
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
    heavily based on the code of Alexander Krauss
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
    (code forked on 14 January 2011)
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
Main entry points to the nominal function package.
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
*)
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
signature NOMINAL_FUNCTION =
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
sig
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2862
diff changeset
    12
  include NOMINAL_FUNCTION_DATA
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
  val add_nominal_function: (binding * typ option * mixfix) list ->
2819
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
    15
    (Attrib.binding * term) list ->  Nominal_Function_Common.nominal_function_config ->
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2862
diff changeset
    16
    (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
  val add_nominal_function_cmd: (binding * string option * mixfix) list ->
2819
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
    19
    (Attrib.binding * string) list ->  Nominal_Function_Common.nominal_function_config ->
2992
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
    20
    (Proof.context -> tactic) -> bool -> local_theory -> nominal_info * local_theory
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
  val nominal_function: (binding * typ option * mixfix) list ->
2819
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
    23
    (Attrib.binding * term) list ->  Nominal_Function_Common.nominal_function_config ->
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
    local_theory -> Proof.state
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
  val nominal_function_cmd: (binding * string option * mixfix) list ->
2819
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
    27
    (Attrib.binding * string) list ->  Nominal_Function_Common.nominal_function_config ->
2992
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
    28
    bool -> local_theory -> Proof.state
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2862
diff changeset
    30
  val get_info : Proof.context -> term -> nominal_info
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
end
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
structure Nominal_Function : NOMINAL_FUNCTION =
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
struct
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
open Function_Lib
2821
c7d4bd9e89e0 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
parents: 2819
diff changeset
    38
open Function_Common
2819
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
    39
open Nominal_Function_Common
2752
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    40
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    41
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    42
(* Check for all sorts of errors in the input - nominal needs a different checking function *)
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    43
fun nominal_check_defs ctxt fixes eqs =
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    44
  let
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    45
    val fnames = map (fst o fst) fixes
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    46
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    47
    fun check geq =
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    48
      let
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    49
        fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    50
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    51
        fun check_head fname =
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    52
          member (op =) fnames fname orelse
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    53
          input_error ("Illegal equation head. Expected " ^ commas_quote fnames)
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    54
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    55
        val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    56
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    57
        val _ = length args > 0 orelse input_error "Function has no arguments:"
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    58
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    59
        fun add_bvs t is = add_loose_bnos (t, 0, is)
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    60
        val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    61
                    |> map (fst o nth (rev qs))
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    62
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    63
        val _ = forall (not o Term.exists_subterm
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    64
          (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args)
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    65
          orelse input_error "Defined function may not occur in premises or arguments"
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    66
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    67
        val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
2860
25a7f421a3ba added a test that every function must be of pt-sort
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
    68
        val funvars = filter (fn q => 
25a7f421a3ba added a test that every function must be of pt-sort
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
    69
          exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
2752
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    70
        val _ = null funvars orelse (warning (cat_lines
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    71
          ["Bound variable" ^ plural " " "s " funvars ^
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    72
          commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    73
          " in function position.", "Misspelled constructor???"]); true)
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    74
      in
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    75
        (fname, length args)
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    76
      end
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    77
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    78
    val grouped_args = AList.group (op =) (map check eqs)
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    79
    val _ = grouped_args
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    80
      |> map (fn (fname, ars) =>
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    81
        length (distinct (op =) ars) = 1
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    82
        orelse error ("Function " ^ quote fname ^
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    83
          " has different numbers of arguments in different equations"))
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    84
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    85
    val not_defined = subtract (op =) (map fst grouped_args) fnames
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    86
    val _ = null not_defined
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    87
      orelse error ("No defining equations for function" ^
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    88
        plural " " "s " not_defined ^ commas_quote not_defined)
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    89
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    90
    fun check_sorts ((fname, fT), _) =
3045
d0ad264f8c4f updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 2999
diff changeset
    91
      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort "pt"})
2752
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    92
      orelse error (cat_lines
2860
25a7f421a3ba added a test that every function must be of pt-sort
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
    93
      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "pt" ^ ":",
2752
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    94
       Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    95
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    96
    val _ = map check_sorts fixes
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    97
  in
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    98
    ()
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
    99
  end
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
   100
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
   101
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents: 2745
diff changeset
   102
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
val simp_attribs = map (Attrib.internal o K)
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
  [Simplifier.simp_add,
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
   Code.add_default_eqn_attribute,
3239
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3235
diff changeset
   106
   Named_Theorems.add @{named_theorems nitpick_simp}]
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
val psimp_attribs = map (Attrib.internal o K)
3239
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3235
diff changeset
   109
  [Named_Theorems.add @{named_theorems nitpick_psimp}]
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   111
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   113
fun add_simps fnames post sort extra_qualify label mod_binding moreatts
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
  simps lthy =
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
  let
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
    val spec = post simps
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
      |> map (apfst (apsnd (fn ats => moreatts @ ats)))
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
      |> map (apfst (apfst extra_qualify))
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
    val (saved_spec_simps, lthy) =
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
      fold_map Local_Theory.note spec lthy
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
    val saved_simps = maps snd saved_spec_simps
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
    val simps_by_f = sort saved_simps
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   126
    fun add_for_f fname simps =
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   127
      Local_Theory.note
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
        ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
      #> snd
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   130
  in
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
    (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
  end
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   133
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
(* nominal *)
2992
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
   135
fun prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy =
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   136
  let
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   137
    val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   138
    val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
    val fixes = map (apfst (apfst Binding.name_of)) fixes0;
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
    val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
2789
32979078bfe9 functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
parents: 2752
diff changeset
   141
    val (eqs, post, sort_cont, cnames) =  
3203
01a13904aaa5 adapted to latest change of Markus on the function package
Christian Urban <urbanc@in.tum.de>
parents: 3190
diff changeset
   142
      empty_preproc nominal_check_defs (Function_Common.default_config) ctxt' fixes spec (* nominal *)
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   143
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
    val defname = mk_defname fixes
2860
25a7f421a3ba added a test that every function must be of pt-sort
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   145
    val NominalFunctionConfig {partials, ...} = config
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   146
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
    val ((goal_state, cont), lthy') =
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   148
      Nominal_Function_Mutual.prepare_nominal_function_mutual config defname fixes eqs lthy
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   149
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
    fun afterqed [[proof]] lthy =
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   151
      let
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2862
diff changeset
   152
        val NominalFunctionResult {fs, R, psimps, simple_pinducts,
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2862
diff changeset
   153
          termination, domintros, cases, eqvts, ...} =
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
          cont (Thm.close_derivation proof)
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2862
diff changeset
   155
  
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   156
        val fnames = map (fst o fst) fixes
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   157
        fun qualify n = Binding.name n
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
          |> Binding.qualify true defname
3239
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3235
diff changeset
   159
        val concealed_partial = if partials then I else Binding.concealed
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   160
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
        val addsmps = add_simps fnames post sort_cont
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   163
        val (((psimps', pinducts'), (_, [termination'])), lthy) =
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   164
          lthy
3239
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3235
diff changeset
   165
          |> addsmps (concealed_partial o Binding.qualify false "partial")
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3235
diff changeset
   166
               "psimps" concealed_partial psimp_attribs psimps
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3235
diff changeset
   167
          ||>> Local_Theory.note ((concealed_partial (qualify "pinduct"),
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   168
                 [Attrib.internal (K (Rule_Cases.case_names cnames)),
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   169
                  Attrib.internal (K (Rule_Cases.consumes 1)),
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   170
                  Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
3239
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3235
diff changeset
   171
          ||>> Local_Theory.note ((Binding.concealed (qualify "termination"), []), [termination])
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   172
          ||> (snd o Local_Theory.note ((qualify "cases",
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   173
                 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
          ||> (case domintros of NONE => I | SOME thms => 
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   175
                   Local_Theory.note ((qualify "domintros", []), thms) #> snd)
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   177
        val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
          pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2862
diff changeset
   179
          fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts}
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2862
diff changeset
   180
3234
08c3ef07cef7 changes from upstream
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3233
diff changeset
   181
        val _ = Proof_Display.print_consts do_print
3233
9ae285ce814e updated changes from upstream (AFP)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3231
diff changeset
   182
          (Position.thread_data ()) lthy (K false) (map fst fixes)
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   183
      in
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   184
        (info, 
3045
d0ad264f8c4f updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 2999
diff changeset
   185
         lthy |> Local_Theory.declaration {syntax = false, pervasive = false} 
d0ad264f8c4f updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 2999
diff changeset
   186
           (add_function_data o morph_function_data info))
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   187
      end
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   188
  in
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   189
    ((goal_state, afterqed), lthy')
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   190
  end
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   191
2992
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
   192
fun gen_add_nominal_function do_print prep default_constraint fixspec eqns config tac lthy =
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   193
  let
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   194
    val ((goal_state, afterqed), lthy') =
2992
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
   195
      prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   196
    val pattern_thm =
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   197
      case SINGLE (tac lthy') goal_state of
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   198
        NONE => error "pattern completeness and compatibility proof failed"
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   199
      | SOME st => Goal.finish lthy' st
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   200
  in
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   201
    lthy'
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   202
    |> afterqed [[pattern_thm]]
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   203
  end
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   204
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
val add_nominal_function =
3231
188826f1ccdb updated to massive changes in Isabelle
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3227
diff changeset
   206
  gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type})
2992
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
   207
fun add_nominal_function_cmd a b c d int = 
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
   208
  gen_add_nominal_function int Specification.read_spec "_::type" a b c d
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
2992
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
   210
fun gen_nominal_function do_print prep default_constraint fixspec eqns config lthy =
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   211
  let
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   212
    val ((goal_state, afterqed), lthy') =
2992
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
   213
      prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   214
  in
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   215
    lthy'
3239
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3235
diff changeset
   216
    |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]]
3227
35bb5b013f0e updated with current AFP version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3203
diff changeset
   217
    |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   218
  end
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   219
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   220
val nominal_function =
3231
188826f1ccdb updated to massive changes in Isabelle
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3227
diff changeset
   221
  gen_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type})
2992
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
   222
fun nominal_function_cmd a b c int = 
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
   223
  gen_nominal_function int Specification.read_spec "_::type" a b c
782a2cd1a8d0 made same changes as in main branch
Christian Urban <urbanc@in.tum.de>
parents: 2988
diff changeset
   224
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   225
fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   226
  |> the_single |> snd
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   227
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   228
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   229
(* outer syntax *)
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   230
2819
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   231
local
2999
68c894c513f6 updated to Isabelle 28 Aug
Christian Urban <urbanc@in.tum.de>
parents: 2992
diff changeset
   232
  val option_parser = Parse.group (fn () => "option")
2819
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   233
    ((Parse.reserved "sequential" >> K Sequential)
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   234
     || ((Parse.reserved "default" |-- Parse.term) >> Default)
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   235
     || (Parse.reserved "domintros" >> K DomIntros)
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   236
     || (Parse.reserved "no_partials" >> K No_Partials)
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   237
     || ((Parse.reserved "invariant" |-- Parse.term) >> Invariant))
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   238
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   239
  fun config_parser default =
3234
08c3ef07cef7 changes from upstream
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3233
diff changeset
   240
    (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) [])
2819
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   241
     >> (fn opts => fold apply_opt opts default)
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   242
in
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   243
  fun nominal_function_parser default_cfg =
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   244
      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   245
end
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   246
4bd584ff4fab added an option for an invariant (at the moment only a stub)
Christian Urban <urbanc@in.tum.de>
parents: 2789
diff changeset
   247
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   248
(* nominal *)
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   249
val _ =
3239
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3235
diff changeset
   250
  Outer_Syntax.local_theory_to_proof' @{command_keyword nominal_function}
3135
92b9b8d2888d updated to new Isabelle (20 March)
Christian Urban <urbanc@in.tum.de>
parents: 3045
diff changeset
   251
    "define general recursive nominal functions"
92b9b8d2888d updated to new Isabelle (20 March)
Christian Urban <urbanc@in.tum.de>
parents: 3045
diff changeset
   252
       (nominal_function_parser nominal_default_config
92b9b8d2888d updated to new Isabelle (20 March)
Christian Urban <urbanc@in.tum.de>
parents: 3045
diff changeset
   253
          >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
2665
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   254
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   255
16b5a67ee279 exported nominal function code to external file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   256
end