2665
+ − 1
(* Nominal Mutual Functions
+ − 2
Author: Christian Urban
+ − 3
+ − 4
heavily based on the code of Alexander Krauss
+ − 5
(code forked on 14 January 2011)
+ − 6
+ − 7
Main entry points to the nominal function package.
+ − 8
*)
+ − 9
+ − 10
signature NOMINAL_FUNCTION =
+ − 11
sig
2973
d1038e67923a
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 12
include NOMINAL_FUNCTION_DATA
2665
+ − 13
+ − 14
val add_nominal_function: (binding * typ option * mixfix) list ->
2819
+ − 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>
diff
changeset
+ − 16
(Proof.context -> tactic) -> local_theory -> nominal_info * local_theory
2665
+ − 17
+ − 18
val add_nominal_function_cmd: (binding * string option * mixfix) list ->
2819
+ − 19
(Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config ->
2992
+ − 20
(Proof.context -> tactic) -> bool -> local_theory -> nominal_info * local_theory
2665
+ − 21
+ − 22
val nominal_function: (binding * typ option * mixfix) list ->
2819
+ − 23
(Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config ->
2665
+ − 24
local_theory -> Proof.state
+ − 25
+ − 26
val nominal_function_cmd: (binding * string option * mixfix) list ->
2819
+ − 27
(Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config ->
2992
+ − 28
bool -> local_theory -> Proof.state
2665
+ − 29
+ − 30
val setup : theory -> theory
+ − 31
val get_congs : Proof.context -> thm list
+ − 32
2973
d1038e67923a
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33
val get_info : Proof.context -> term -> nominal_info
2665
+ − 34
end
+ − 35
+ − 36
+ − 37
structure Nominal_Function : NOMINAL_FUNCTION =
+ − 38
struct
+ − 39
+ − 40
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>
diff
changeset
+ − 41
open Function_Common
2819
+ − 42
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>
diff
changeset
+ − 43
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 45
(* 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>
diff
changeset
+ − 46
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>
diff
changeset
+ − 47
let
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 48
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>
diff
changeset
+ − 49
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 50
fun check geq =
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 51
let
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 52
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>
diff
changeset
+ − 53
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 54
fun check_head fname =
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
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>
diff
changeset
+ − 56
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>
diff
changeset
+ − 57
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 58
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>
diff
changeset
+ − 59
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 60
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>
diff
changeset
+ − 61
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 62
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>
diff
changeset
+ − 63
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>
diff
changeset
+ − 64
|> 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>
diff
changeset
+ − 65
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 66
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>
diff
changeset
+ − 67
(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>
diff
changeset
+ − 68
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>
diff
changeset
+ − 69
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 70
val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
2860
+ − 71
val funvars = filter (fn q =>
+ − 72
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>
diff
changeset
+ − 73
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>
diff
changeset
+ − 74
["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>
diff
changeset
+ − 75
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>
diff
changeset
+ − 76
" 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>
diff
changeset
+ − 77
in
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 78
(fname, length args)
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 79
end
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 80
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 81
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>
diff
changeset
+ − 82
val _ = grouped_args
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 83
|> map (fn (fname, ars) =>
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 84
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>
diff
changeset
+ − 85
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>
diff
changeset
+ − 86
" 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>
diff
changeset
+ − 87
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 88
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>
diff
changeset
+ − 89
val _ = null not_defined
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 90
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>
diff
changeset
+ − 91
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>
diff
changeset
+ − 92
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 93
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>
diff
changeset
+ − 94
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>
diff
changeset
+ − 95
orelse error (cat_lines
2860
+ − 96
["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>
diff
changeset
+ − 97
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>
diff
changeset
+ − 98
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 99
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>
diff
changeset
+ − 100
in
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 101
()
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 102
end
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 103
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 104
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 105
2665
+ − 106
val simp_attribs = map (Attrib.internal o K)
+ − 107
[Simplifier.simp_add,
+ − 108
Code.add_default_eqn_attribute,
+ − 109
Nitpick_Simps.add]
+ − 110
+ − 111
val psimp_attribs = map (Attrib.internal o K)
+ − 112
[Nitpick_Psimps.add]
+ − 113
+ − 114
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
+ − 115
+ − 116
fun add_simps fnames post sort extra_qualify label mod_binding moreatts
+ − 117
simps lthy =
+ − 118
let
+ − 119
val spec = post simps
+ − 120
|> map (apfst (apsnd (fn ats => moreatts @ ats)))
+ − 121
|> map (apfst (apfst extra_qualify))
+ − 122
+ − 123
val (saved_spec_simps, lthy) =
+ − 124
fold_map Local_Theory.note spec lthy
+ − 125
+ − 126
val saved_simps = maps snd saved_spec_simps
+ − 127
val simps_by_f = sort saved_simps
+ − 128
+ − 129
fun add_for_f fname simps =
+ − 130
Local_Theory.note
+ − 131
((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
+ − 132
#> snd
+ − 133
in
+ − 134
(saved_simps, fold2 add_for_f fnames simps_by_f lthy)
+ − 135
end
+ − 136
+ − 137
(* nominal *)
2992
+ − 138
fun prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy =
2665
+ − 139
let
+ − 140
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
+ − 141
val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
+ − 142
val fixes = map (apfst (apfst Binding.name_of)) fixes0;
+ − 143
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>
diff
changeset
+ − 144
val (eqs, post, sort_cont, cnames) =
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>
diff
changeset
+ − 145
empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *)
2665
+ − 146
+ − 147
val defname = mk_defname fixes
2860
+ − 148
val NominalFunctionConfig {partials, ...} = config
2665
+ − 149
+ − 150
val ((goal_state, cont), lthy') =
+ − 151
Nominal_Function_Mutual.prepare_nominal_function_mutual config defname fixes eqs lthy
+ − 152
+ − 153
fun afterqed [[proof]] lthy =
+ − 154
let
2973
d1038e67923a
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 155
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>
diff
changeset
+ − 156
termination, domintros, cases, eqvts, ...} =
2665
+ − 157
cont (Thm.close_derivation proof)
2973
d1038e67923a
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 158
2665
+ − 159
val fnames = map (fst o fst) fixes
+ − 160
fun qualify n = Binding.name n
+ − 161
|> Binding.qualify true defname
+ − 162
val conceal_partial = if partials then I else Binding.conceal
+ − 163
+ − 164
val addsmps = add_simps fnames post sort_cont
+ − 165
+ − 166
val (((psimps', pinducts'), (_, [termination'])), lthy) =
+ − 167
lthy
+ − 168
|> addsmps (conceal_partial o Binding.qualify false "partial")
+ − 169
"psimps" conceal_partial psimp_attribs psimps
+ − 170
||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
+ − 171
[Attrib.internal (K (Rule_Cases.case_names cnames)),
+ − 172
Attrib.internal (K (Rule_Cases.consumes 1)),
+ − 173
Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
+ − 174
||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
+ − 175
||> (snd o Local_Theory.note ((qualify "cases",
+ − 176
[Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
+ − 177
||> (case domintros of NONE => I | SOME thms =>
+ − 178
Local_Theory.note ((qualify "domintros", []), thms) #> snd)
+ − 179
+ − 180
val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
+ − 181
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>
diff
changeset
+ − 182
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>
diff
changeset
+ − 183
2992
+ − 184
val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
2665
+ − 185
in
+ − 186
(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>
diff
changeset
+ − 187
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>
diff
changeset
+ − 188
(add_function_data o morph_function_data info))
2665
+ − 189
end
+ − 190
in
+ − 191
((goal_state, afterqed), lthy')
+ − 192
end
+ − 193
2992
+ − 194
fun gen_add_nominal_function do_print prep default_constraint fixspec eqns config tac lthy =
2665
+ − 195
let
+ − 196
val ((goal_state, afterqed), lthy') =
2992
+ − 197
prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy
2665
+ − 198
val pattern_thm =
+ − 199
case SINGLE (tac lthy') goal_state of
+ − 200
NONE => error "pattern completeness and compatibility proof failed"
+ − 201
| SOME st => Goal.finish lthy' st
+ − 202
in
+ − 203
lthy'
+ − 204
|> afterqed [[pattern_thm]]
+ − 205
end
+ − 206
+ − 207
val add_nominal_function =
+ − 208
gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
2992
+ − 209
fun add_nominal_function_cmd a b c d int =
+ − 210
gen_add_nominal_function int Specification.read_spec "_::type" a b c d
2665
+ − 211
2992
+ − 212
fun gen_nominal_function do_print prep default_constraint fixspec eqns config lthy =
2665
+ − 213
let
+ − 214
val ((goal_state, afterqed), lthy') =
2992
+ − 215
prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy
2665
+ − 216
in
+ − 217
lthy'
+ − 218
|> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
+ − 219
|> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
+ − 220
end
+ − 221
+ − 222
val nominal_function =
+ − 223
gen_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
2992
+ − 224
fun nominal_function_cmd a b c int =
+ − 225
gen_nominal_function int Specification.read_spec "_::type" a b c
+ − 226
2665
+ − 227
+ − 228
fun add_case_cong n thy =
+ − 229
let
+ − 230
val cong = #case_cong (Datatype.the_info thy n)
+ − 231
|> safe_mk_meta_eq
+ − 232
in
+ − 233
Context.theory_map
+ − 234
(Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
+ − 235
end
+ − 236
+ − 237
val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
+ − 238
+ − 239
2752
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 240
2665
+ − 241
(* setup *)
+ − 242
+ − 243
val setup =
+ − 244
Attrib.setup @{binding fundef_cong}
+ − 245
(Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
+ − 246
"declaration of congruence rule for function definitions"
+ − 247
#> setup_case_cong
+ − 248
#> Function_Relation.setup
+ − 249
#> Function_Common.Termination_Simps.setup
+ − 250
+ − 251
val get_congs = Function_Ctx_Tree.get_function_congs
+ − 252
+ − 253
fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
+ − 254
|> the_single |> snd
+ − 255
+ − 256
+ − 257
(* outer syntax *)
+ − 258
2819
+ − 259
local
2999
+ − 260
val option_parser = Parse.group (fn () => "option")
2819
+ − 261
((Parse.reserved "sequential" >> K Sequential)
+ − 262
|| ((Parse.reserved "default" |-- Parse.term) >> Default)
+ − 263
|| (Parse.reserved "domintros" >> K DomIntros)
+ − 264
|| (Parse.reserved "no_partials" >> K No_Partials)
+ − 265
|| ((Parse.reserved "invariant" |-- Parse.term) >> Invariant))
+ − 266
+ − 267
fun config_parser default =
+ − 268
(Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
+ − 269
>> (fn opts => fold apply_opt opts default)
+ − 270
in
+ − 271
fun nominal_function_parser default_cfg =
+ − 272
config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
+ − 273
end
+ − 274
+ − 275
2665
+ − 276
(* nominal *)
+ − 277
val _ =
3135
+ − 278
Outer_Syntax.local_theory_to_proof' ("nominal_primrec", Keyword.thy_goal)
+ − 279
"define general recursive nominal functions"
+ − 280
(nominal_function_parser nominal_default_config
+ − 281
>> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
2665
+ − 282
+ − 283
+ − 284
end