2454
+ − 1
theory Nominal2
2435
+ − 2
imports
2943
+ − 3
Nominal2_Base Nominal2_Abs Nominal2_FCB
2598
+ − 4
uses ("nominal_dt_rawfuns.ML")
2435
+ − 5
("nominal_dt_alpha.ML")
+ − 6
("nominal_dt_quot.ML")
2631
e73bd379e839
removed local fix for bug in induction_schema; added setup method for strong inductions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 7
("nominal_induct.ML")
2819
+ − 8
("nominal_inductive.ML")
2822
23befefc6e73
cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 9
("nominal_function_common.ML")
2665
+ − 10
("nominal_function_core.ML")
+ − 11
("nominal_mutual.ML")
+ − 12
("nominal_function.ML")
2973
d1038e67923a
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 13
("nominal_termination.ML")
2885
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 14
("nominal_dt_data.ML")
1941
+ − 15
begin
+ − 16
2885
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 17
use "nominal_dt_data.ML"
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 18
ML {* open Nominal_Dt_Data *}
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 19
2435
+ − 20
use "nominal_dt_rawfuns.ML"
+ − 21
ML {* open Nominal_Dt_RawFuns *}
+ − 22
+ − 23
use "nominal_dt_alpha.ML"
+ − 24
ML {* open Nominal_Dt_Alpha *}
+ − 25
+ − 26
use "nominal_dt_quot.ML"
+ − 27
ML {* open Nominal_Dt_Quot *}
+ − 28
2631
e73bd379e839
removed local fix for bug in induction_schema; added setup method for strong inductions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 29
(*****************************************)
e73bd379e839
removed local fix for bug in induction_schema; added setup method for strong inductions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 30
(* setup for induction principles method *)
e73bd379e839
removed local fix for bug in induction_schema; added setup method for strong inductions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 31
use "nominal_induct.ML"
e73bd379e839
removed local fix for bug in induction_schema; added setup method for strong inductions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 32
method_setup nominal_induct =
e73bd379e839
removed local fix for bug in induction_schema; added setup method for strong inductions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33
{* NominalInduct.nominal_induct_method *}
e73bd379e839
removed local fix for bug in induction_schema; added setup method for strong inductions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 34
{* nominal induction *}
2609
666ffc8a92a9
freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 35
2639
+ − 36
(****************************************************)
+ − 37
(* inductive definition involving nominal datatypes *)
+ − 38
use "nominal_inductive.ML"
+ − 39
+ − 40
2665
+ − 41
(***************************************)
+ − 42
(* forked code of the function package *)
+ − 43
(* for defining nominal functions *)
2822
23befefc6e73
cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
use "nominal_function_common.ML"
2665
+ − 45
use "nominal_function_core.ML"
+ − 46
use "nominal_mutual.ML"
+ − 47
use "nominal_function.ML"
2973
d1038e67923a
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 48
use "nominal_termination.ML"
2665
+ − 49
2603
+ − 50
ML {*
+ − 51
val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+ − 52
val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
+ − 53
val simp_attr = Attrib.internal (K Simplifier.simp_add)
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 54
val induct_attr = Attrib.internal (K Induct.induct_simp_add)
2603
+ − 55
*}
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 56
1941
+ − 57
section{* Interface for nominal_datatype *}
+ − 58
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 59
ML {* print_depth 50 *}
1941
+ − 60
+ − 61
ML {*
+ − 62
fun get_cnstrs dts =
3065
+ − 63
map snd dts
1941
+ − 64
+ − 65
fun get_typed_cnstrs dts =
3065
+ − 66
flat (map (fn ((bn, _, _), constrs) =>
1941
+ − 67
(map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts)
+ − 68
+ − 69
fun get_cnstr_strs dts =
+ − 70
map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts))
+ − 71
+ − 72
fun get_bn_fun_strs bn_funs =
+ − 73
map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
+ − 74
*}
+ − 75
2106
+ − 76
1944
+ − 77
text {* Infrastructure for adding "_raw" to types and terms *}
+ − 78
1941
+ − 79
ML {*
+ − 80
fun add_raw s = s ^ "_raw"
+ − 81
fun add_raws ss = map add_raw ss
+ − 82
fun raw_bind bn = Binding.suffix_name "_raw" bn
+ − 83
+ − 84
fun replace_str ss s =
+ − 85
case (AList.lookup (op=) ss s) of
+ − 86
SOME s' => s'
+ − 87
| NONE => s
+ − 88
+ − 89
fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts)
+ − 90
| replace_typ ty_ss T = T
+ − 91
+ − 92
fun raw_dts ty_ss dts =
+ − 93
let
2640
75d353e8e60e
made sure the raw datatypes and raw functions do not get any mixfix syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 94
fun raw_dts_aux1 (bind, tys, _) =
75d353e8e60e
made sure the raw datatypes and raw functions do not get any mixfix syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 95
(raw_bind bind, map (replace_typ ty_ss) tys, NoSyn)
1941
+ − 96
3065
+ − 97
fun raw_dts_aux2 ((bind, ty_args, _), constrs) =
+ − 98
((raw_bind bind, ty_args, NoSyn), map raw_dts_aux1 constrs)
1941
+ − 99
in
+ − 100
map raw_dts_aux2 dts
+ − 101
end
+ − 102
+ − 103
fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T)
+ − 104
| replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T)
+ − 105
| replace_aterm trm_ss trm = trm
+ − 106
+ − 107
fun replace_term trm_ss ty_ss trm =
+ − 108
trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss)
+ − 109
*}
+ − 110
+ − 111
ML {*
3061
+ − 112
fun rawify_dts dts dts_env = raw_dts dts_env dts
1941
+ − 113
*}
+ − 114
+ − 115
ML {*
+ − 116
fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs =
+ − 117
let
2640
75d353e8e60e
made sure the raw datatypes and raw functions do not get any mixfix syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 118
val bn_funs' = map (fn (bn, ty, _) =>
75d353e8e60e
made sure the raw datatypes and raw functions do not get any mixfix syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 119
(raw_bind bn, SOME (replace_typ dts_env ty), NoSyn)) bn_funs
1941
+ − 120
+ − 121
val bn_eqs' = map (fn (attr, trm) =>
+ − 122
(attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs
+ − 123
in
+ − 124
(bn_funs', bn_eqs')
+ − 125
end
+ − 126
*}
+ − 127
+ − 128
ML {*
+ − 129
fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses =
+ − 130
let
+ − 131
fun rawify_bnds bnds =
+ − 132
map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds
+ − 133
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 134
fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys)
1941
+ − 135
in
2612
+ − 136
(map o map o map) rawify_bclause bclauses
1941
+ − 137
end
+ − 138
*}
+ − 139
+ − 140
+ − 141
ML {*
2885
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 142
(* definition of the raw datatype *)
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 143
2957
+ − 144
fun define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy =
1941
+ − 145
let
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 146
val thy = Local_Theory.exit_global lthy
1941
+ − 147
val thy_name = Context.theory_name thy
+ − 148
3065
+ − 149
val dt_names = map (fn ((s, _, _), _) => Binding.name_of s) dts
1941
+ − 150
val dt_full_names = map (Long_Name.qualify thy_name) dt_names
+ − 151
val dt_full_names' = add_raws dt_full_names
+ − 152
val dts_env = dt_full_names ~~ dt_full_names'
+ − 153
2633
+ − 154
val cnstr_full_names = map (Long_Name.qualify thy_name) cnstr_names
+ − 155
val cnstr_full_names' = map (fn (x, y) => Long_Name.qualify thy_name
+ − 156
(Long_Name.qualify (add_raw x) (add_raw y))) cnstr_tys
+ − 157
val cnstrs_env = cnstr_full_names ~~ cnstr_full_names'
1941
+ − 158
+ − 159
val bn_fun_strs = get_bn_fun_strs bn_funs
+ − 160
val bn_fun_strs' = add_raws bn_fun_strs
+ − 161
val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
+ − 162
val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name))
+ − 163
(bn_fun_strs ~~ bn_fun_strs')
+ − 164
3061
+ − 165
val raw_dts = rawify_dts dts dts_env
1941
+ − 166
val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 167
val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses
1941
+ − 168
2957
+ − 169
val (raw_full_dt_names', thy1) =
3061
+ − 170
Datatype.add_datatype Datatype.default_config raw_dts thy
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 171
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 172
val lthy1 = Named_Target.theory_init thy1
2957
+ − 173
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
+ − 174
val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names'
3062
+ − 175
val {descr, ...} = hd dtinfos
2957
+ − 176
3062
+ − 177
val raw_tys = Datatype_Aux.get_rec_types descr
2957
+ − 178
val raw_ty_args = hd raw_tys
+ − 179
|> snd o dest_Type
+ − 180
|> map dest_TFree
+ − 181
3062
+ − 182
val raw_cns_info = all_dtyp_constrs_types descr
2957
+ − 183
val raw_all_cns = (map o map) (fn (c, _, _, _) => c) raw_cns_info
+ − 184
+ − 185
val raw_inject_thms = flat (map #inject dtinfos)
+ − 186
val raw_distinct_thms = flat (map #distinct dtinfos)
+ − 187
val raw_induct_thm = #induct (hd dtinfos)
+ − 188
val raw_induct_thms = #inducts (hd dtinfos)
+ − 189
val raw_exhaust_thms = map #exhaust dtinfos
+ − 190
val raw_size_trms = map HOLogic.size_const raw_tys
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
+ − 191
val raw_size_thms = Size.size_thms (Proof_Context.theory_of lthy1) (hd raw_full_dt_names')
2957
+ − 192
|> `(fn thms => (length thms) div 2)
+ − 193
|> uncurry drop
+ − 194
+ − 195
val raw_result = RawDtInfo
+ − 196
{raw_dt_names = raw_full_dt_names',
+ − 197
raw_dts = raw_dts,
+ − 198
raw_tys = raw_tys,
+ − 199
raw_ty_args = raw_ty_args,
+ − 200
raw_cns_info = raw_cns_info,
+ − 201
raw_all_cns = raw_all_cns,
+ − 202
raw_inject_thms = raw_inject_thms,
+ − 203
raw_distinct_thms = raw_distinct_thms,
+ − 204
raw_induct_thm = raw_induct_thm,
+ − 205
raw_induct_thms = raw_induct_thms,
+ − 206
raw_exhaust_thms = raw_exhaust_thms,
+ − 207
raw_size_trms = raw_size_trms,
+ − 208
raw_size_thms = raw_size_thms}
2304
+ − 209
in
2957
+ − 210
(raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_result, lthy1)
2304
+ − 211
end
+ − 212
*}
+ − 213
2125
60ee289a8c63
made out of STEPS a configuration value so that it can be set individually in each file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 214
1941
+ − 215
ML {*
2436
+ − 216
fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =
1941
+ − 217
let
2957
+ − 218
val cnstr_names = get_cnstr_strs dts
+ − 219
val cnstr_tys = get_typed_cnstrs dts
1941
+ − 220
2957
+ − 221
val _ = trace_msg (K "Defining raw datatypes...")
+ − 222
val (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_dt_info, lthy0) =
+ − 223
define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 224
2957
+ − 225
val RawDtInfo
+ − 226
{raw_dt_names,
+ − 227
raw_tys,
+ − 228
raw_ty_args,
+ − 229
raw_all_cns,
+ − 230
raw_inject_thms,
+ − 231
raw_distinct_thms,
+ − 232
raw_induct_thm,
+ − 233
raw_induct_thms,
+ − 234
raw_exhaust_thms,
+ − 235
raw_size_trms,
+ − 236
raw_size_thms, ...} = raw_dt_info
2388
+ − 237
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 238
val _ = trace_msg (K "Defining raw permutations...")
2957
+ − 239
val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = define_raw_perms raw_dt_info lthy0
2144
+ − 240
+ − 241
(* noting the raw permutations as eqvt theorems *)
2959
+ − 242
val lthy3 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a)
2011
12ce87b55f97
tried to add some comments in the huge(!) nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 243
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 244
val _ = trace_msg (K "Defining raw fv- and bn-functions...")
2922
+ − 245
val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_inducts, lthy3a) =
2957
+ − 246
define_raw_bns raw_dt_info raw_bn_funs raw_bn_eqs lthy3
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 247
2560
+ − 248
(* defining the permute_bn functions *)
2561
+ − 249
val (raw_perm_bns, raw_perm_bn_simps, lthy3b) =
2957
+ − 250
define_raw_bn_perms raw_dt_info raw_bn_info lthy3a
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 251
2560
+ − 252
val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) =
2957
+ − 253
define_raw_fvs raw_dt_info raw_bn_info raw_bclauses lthy3b
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 254
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 255
val _ = trace_msg (K "Defining alpha relations...")
2928
+ − 256
val (alpha_result, lthy4) =
2957
+ − 257
define_raw_alpha raw_dt_info raw_bn_info raw_bclauses raw_fvs lthy3c
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 258
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 259
val _ = trace_msg (K "Proving distinct theorems...")
2957
+ − 260
val alpha_distincts = raw_prove_alpha_distincts lthy4 alpha_result raw_dt_info
2300
+ − 261
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 262
val _ = trace_msg (K "Proving eq-iff theorems...")
2957
+ − 263
val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_dt_info
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 264
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 265
val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...")
2406
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 266
val raw_bn_eqvt =
2922
+ − 267
raw_prove_eqvt raw_bns raw_bn_inducts (raw_bn_defs @ raw_perm_simps) lthy4
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 268
2406
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 269
(* noting the raw_bn_eqvt lemmas in a temprorary theory *)
2448
+ − 270
val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4)
2305
+ − 271
2406
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 272
val raw_fv_eqvt =
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 273
raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps)
2388
+ − 274
(Local_Theory.restore lthy_tmp)
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 275
2957
+ − 276
val raw_size_eqvt =
+ − 277
let
+ − 278
val RawDtInfo {raw_size_trms, raw_size_thms, raw_induct_thms, ...} = raw_dt_info
+ − 279
in
+ − 280
raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps)
+ − 281
(Local_Theory.restore lthy_tmp)
+ − 282
|> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]})
+ − 283
|> map (fn thm => thm RS @{thm sym})
+ − 284
end
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 285
2448
+ − 286
val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)
2306
+ − 287
2868
+ − 288
val alpha_eqvt =
2928
+ − 289
let
+ − 290
val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, alpha_intros, ...} = alpha_result
+ − 291
in
+ − 292
Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_raw_induct alpha_intros lthy5
+ − 293
end
2868
+ − 294
+ − 295
val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt
2311
+ − 296
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 297
val _ = trace_msg (K "Proving equivalence of alpha...")
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 298
val alpha_refl_thms = raw_prove_refl lthy5 alpha_result raw_induct_thm
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 299
val alpha_sym_thms = raw_prove_sym lthy5 alpha_result alpha_eqvt_norm
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 300
val alpha_trans_thms =
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 301
raw_prove_trans lthy5 alpha_result (raw_distinct_thms @ raw_inject_thms) alpha_eqvt_norm
2311
+ − 302
2404
+ − 303
val (alpha_equivp_thms, alpha_bn_equivp_thms) =
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 304
raw_prove_equivp lthy5 alpha_result alpha_refl_thms alpha_sym_thms alpha_trans_thms
2322
+ − 305
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 306
val _ = trace_msg (K "Proving alpha implies bn...")
2928
+ − 307
val alpha_bn_imp_thms = raw_prove_bn_imp lthy5 alpha_result
2922
+ − 308
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 309
val _ = trace_msg (K "Proving respectfulness...")
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 310
val raw_funs_rsp_aux =
2928
+ − 311
raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs)
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 312
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 313
val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
2388
+ − 314
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 315
val raw_size_rsp =
2928
+ − 316
raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt)
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 317
|> map mk_funs_rsp
2392
+ − 318
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 319
val raw_constrs_rsp =
2957
+ − 320
raw_constrs_rsp lthy5 alpha_result (flat raw_all_cns) (alpha_bn_imp_thms @ raw_funs_rsp_aux)
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 321
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 322
val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
2384
+ − 323
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 324
val alpha_bn_rsp =
2928
+ − 325
raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms
2404
+ − 326
2966
+ − 327
val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps
2561
+ − 328
2398
+ − 329
(* noting the quot_respects lemmas *)
2868
+ − 330
val (_, lthy6) =
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 331
Local_Theory.note ((Binding.empty, [rsp_attr]),
2561
+ − 332
raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @
2868
+ − 333
alpha_bn_rsp @ raw_perm_bn_rsp) lthy5
2398
+ − 334
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 335
val _ = trace_msg (K "Defining the quotient types...")
3065
+ − 336
val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts
2400
+ − 337
2336
+ − 338
val (qty_infos, lthy7) =
2928
+ − 339
let
+ − 340
val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result
+ − 341
in
+ − 342
define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
+ − 343
end
2336
+ − 344
+ − 345
val qtys = map #qtyp qty_infos
2400
+ − 346
val qty_full_names = map (fst o dest_Type) qtys
+ − 347
val qty_names = map Long_Name.base_name qty_full_names
+ − 348
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 349
val _ = trace_msg (K "Defining the quotient constants...")
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 350
val qconstrs_descrs =
2957
+ − 351
(map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_all_cns
2338
+ − 352
2339
+ − 353
val qbns_descr =
2781
+ − 354
map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) bn_funs raw_bns
2339
+ − 355
+ − 356
val qfvs_descr =
2346
+ − 357
map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
2339
+ − 358
2346
+ − 359
val qfv_bns_descr =
2781
+ − 360
map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns
2339
+ − 361
2384
+ − 362
val qalpha_bns_descr =
2928
+ − 363
let
+ − 364
val AlphaResult {alpha_bn_trms, ...} = alpha_result
+ − 365
in
+ − 366
map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs alpha_bn_trms
+ − 367
end
2384
+ − 368
2398
+ − 369
val qperm_descr =
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 370
map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
2398
+ − 371
2400
+ − 372
val qsize_descr =
+ − 373
map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
+ − 374
2562
+ − 375
val qperm_bn_descr =
2781
+ − 376
map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_perm_bns
2562
+ − 377
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 378
val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info),
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 379
lthy8) =
2346
+ − 380
lthy7
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 381
|> fold_map (define_qconsts qtys) qconstrs_descrs
2400
+ − 382
||>> define_qconsts qtys qbns_descr
+ − 383
||>> define_qconsts qtys qfvs_descr
+ − 384
||>> define_qconsts qtys qfv_bns_descr
+ − 385
||>> define_qconsts qtys qalpha_bns_descr
2562
+ − 386
||>> define_qconsts qtys qperm_bn_descr
2338
+ − 387
2400
+ − 388
val lthy9 =
2957
+ − 389
define_qperms qtys qty_full_names raw_ty_args qperm_descr raw_perm_laws lthy8
2400
+ − 390
2401
7645e18e8b19
modified the code for class instantiations (with help from Florian)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 391
val lthy9a =
2957
+ − 392
define_qsizes qtys qty_full_names raw_ty_args qsize_descr lthy9
2398
+ − 393
2612
+ − 394
val qtrms = (map o map) #qconst qconstrs_infos
2346
+ − 395
val qbns = map #qconst qbns_info
+ − 396
val qfvs = map #qconst qfvs_info
+ − 397
val qfv_bns = map #qconst qfv_bns_info
2384
+ − 398
val qalpha_bns = map #qconst qalpha_bns_info
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 399
val qperm_bns = map #qconst qperm_bns_info
2434
+ − 400
2649
a8ebcb368a15
a modified function package where, as a test, True has been injected into the compatibility condictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 401
val _ = trace_msg (K "Lifting of theorems...")
2559
add799cf0817
adapted to changes by Florian on the quotient package and removed local fix for function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 402
val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def
2434
+ − 403
prod.cases}
+ − 404
2959
+ − 405
val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts,
+ − 406
qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps,
2966
+ − 407
qalpha_refl_thms, qalpha_sym_thms, qalpha_trans_thms ], lthyB) =
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 408
lthy9a
2959
+ − 409
|>>> lift_thms qtys [] alpha_distincts
+ − 410
||>>> lift_thms qtys eq_iff_simps alpha_eq_iff
+ − 411
||>>> lift_thms qtys [] raw_fv_defs
+ − 412
||>>> lift_thms qtys [] raw_bn_defs
+ − 413
||>>> lift_thms qtys [] raw_perm_simps
+ − 414
||>>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
+ − 415
||>>> lift_thms qtys [] raw_bn_inducts
+ − 416
||>>> lift_thms qtys [] raw_size_eqvt
+ − 417
||>>> lift_thms qtys [] [raw_induct_thm]
+ − 418
||>>> lift_thms qtys [] raw_exhaust_thms
+ − 419
||>>> lift_thms qtys [] raw_size_thms
+ − 420
||>>> lift_thms qtys [] raw_perm_bn_simps
+ − 421
||>>> lift_thms qtys [] alpha_refl_thms
2966
+ − 422
||>>> lift_thms qtys [] alpha_sym_thms
+ − 423
||>>> lift_thms qtys [] alpha_trans_thms
2434
+ − 424
2922
+ − 425
val qinducts = Project_Rule.projections lthyB qinduct
2474
+ − 426
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 427
val _ = trace_msg (K "Proving supp lemmas and fs-instances...")
2959
+ − 428
val qsupports_thms = prove_supports lthyB qperm_simps (flat qtrms)
2448
+ − 429
2451
+ − 430
(* finite supp lemmas *)
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 431
val qfsupp_thms = prove_fsupp lthyB qtys qinduct qsupports_thms
2450
+ − 432
2451
+ − 433
(* fs instances *)
2957
+ − 434
val lthyC = fs_instance qtys qty_full_names raw_ty_args qfsupp_thms lthyB
2448
+ − 435
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 436
val _ = trace_msg (K "Proving equality between fv and supp...")
2475
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 437
val qfv_supp_thms =
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 438
prove_fv_supp qtys (flat qtrms) qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 439
qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
3063
32abaea424bd
generated the correct thm-list for showing that qfv are equal to support
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 440
|> map Drule.eta_contraction_rule
2475
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 441
2492
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 442
(* postprocessing of eq and fv theorems *)
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 443
val qeq_iffs' = qeq_iffs
2493
+ − 444
|> map (simplify (HOL_basic_ss addsimps qfv_supp_thms))
+ − 445
|> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]}))
2492
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 446
3063
32abaea424bd
generated the correct thm-list for showing that qfv are equal to support
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 447
(* filters the theormes that are of the form "qfv = supp" *)
32abaea424bd
generated the correct thm-list for showing that qfv are equal to support
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 448
fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ _)) = member (op=) qfvs lhs
32abaea424bd
generated the correct thm-list for showing that qfv are equal to support
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 449
| is_qfv_thm _ = false
32abaea424bd
generated the correct thm-list for showing that qfv are equal to support
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 450
2492
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 451
val qsupp_constrs = qfv_defs
3063
32abaea424bd
generated the correct thm-list for showing that qfv are equal to support
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 452
|> map (simplify (HOL_basic_ss addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms)))
2492
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 453
2493
+ − 454
val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp}
+ − 455
val transform_thms =
+ − 456
[ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp},
+ − 457
@{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp},
+ − 458
@{lemma "(lhs = (a \<notin> {})) \<longleftrightarrow> lhs" by simp},
+ − 459
@{thm fresh_def[symmetric]}]
+ − 460
+ − 461
val qfresh_constrs = qsupp_constrs
+ − 462
|> map (fn thm => thm RS transform_thm)
+ − 463
|> map (simplify (HOL_basic_ss addsimps transform_thms))
+ − 464
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 465
(* proving that the qbn result is finite *)
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 466
val qbn_finite_thms = prove_bns_finite qtys qbns qinduct qbn_defs lthyC
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 467
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 468
(* proving that perm_bns preserve alpha *)
2594
+ − 469
val qperm_bn_alpha_thms =
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 470
prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs'
2594
+ − 471
qalpha_refl_thms lthyC
2493
+ − 472
2598
+ − 473
(* proving the relationship of bn and permute_bn *)
+ − 474
val qpermute_bn_thms =
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 475
prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
2598
+ − 476
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 477
val _ = trace_msg (K "Proving strong exhaust lemmas...")
2619
+ − 478
val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs'
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 479
qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 480
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 481
val _ = trace_msg (K "Proving strong induct lemmas...")
2633
+ − 482
val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses
2628
+ − 483
2436
+ − 484
(* noting the theorems *)
+ − 485
+ − 486
(* generating the prefix for the theorem names *)
+ − 487
val thms_name =
+ − 488
the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name
+ − 489
fun thms_suffix s = Binding.qualified true s thms_name
2633
+ − 490
val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names))
2436
+ − 491
2885
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 492
val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 493
2451
+ − 494
val (_, lthy9') = lthyC
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
+ − 495
|> Local_Theory.declaration {syntax = false, pervasive = false} (K (fold register_info infos))
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 496
|> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts)
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 497
||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs')
2436
+ − 498
||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs)
+ − 499
||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs)
2922
+ − 500
||>> Local_Theory.note ((thms_suffix "bn_inducts", []), qbn_inducts)
2448
+ − 501
||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps)
2922
+ − 502
||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", [eqvt_attr]), qfv_qbn_eqvts)
2858
de6b601c8d3d
added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 503
||>> Local_Theory.note ((thms_suffix "size", [simp_attr]), qsize_simps)
2436
+ − 504
||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
2633
+ − 505
||>> Local_Theory.note ((thms_suffix "induct", [case_names_attr]), [qinduct])
+ − 506
||>> Local_Theory.note ((thms_suffix "inducts", [case_names_attr]), qinducts)
+ − 507
||>> Local_Theory.note ((thms_suffix "exhaust", [case_names_attr]), qexhausts)
+ − 508
||>> Local_Theory.note ((thms_suffix "strong_exhaust", [case_names_attr]), qstrong_exhaust_thms)
+ − 509
||>> Local_Theory.note ((thms_suffix "strong_induct", [case_names_attr]), qstrong_induct_thms)
2448
+ − 510
||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
2450
+ − 511
||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
2492
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 512
||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
2493
+ − 513
||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
2563
+ − 514
||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
2571
+ − 515
||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 516
||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)
2598
+ − 517
||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms)
2966
+ − 518
||>> Local_Theory.note ((thms_suffix "alpha_refl", []), qalpha_refl_thms)
+ − 519
||>> Local_Theory.note ((thms_suffix "alpha_sym", []), qalpha_sym_thms)
+ − 520
||>> Local_Theory.note ((thms_suffix "alpha_trans", []), qalpha_trans_thms)
+ − 521
1941
+ − 522
in
2601
+ − 523
lthy9'
2647
5e95387bef45
removed debugging code abd introduced a guarded tracing function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 524
end
1941
+ − 525
*}
+ − 526
2475
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 527
1941
+ − 528
section {* Preparing and parsing of the specification *}
+ − 529
ML {*
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 530
(* generates the parsed datatypes and
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 531
declares the constructors
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 532
*)
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 533
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 534
fun prepare_dts dt_strs thy =
1941
+ − 535
let
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 536
fun prep_spec ((tname, tvs, mx), constrs) =
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 537
((tname, tvs, mx),
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 538
constrs |> map (fn (c, Ts, mx', _) => (c, map snd Ts, mx')))
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 539
3065
+ − 540
fun mk_constr_trms ((tname, tvs, _), constrs) =
+ − 541
let
+ − 542
val full_tname = Sign.full_name thy tname
+ − 543
val ty = Type (full_tname, map TFree tvs)
+ − 544
in
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 545
map (fn (c, tys, mx) => (c, (tys ---> ty), mx)) constrs
3065
+ − 546
end
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 547
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 548
val (dts, spec_ctxt) =
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 549
Datatype.read_specs (map prep_spec dt_strs) thy
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 550
3065
+ − 551
val constr_trms = flat (map mk_constr_trms dts)
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 552
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 553
(* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *)
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 554
val thy' = Sign.add_consts_i constr_trms (Proof_Context.theory_of spec_ctxt)
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 555
1941
+ − 556
in
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 557
(dts, thy')
1941
+ − 558
end
+ − 559
*}
+ − 560
+ − 561
ML {*
+ − 562
(* parsing the binding function specification and *)
+ − 563
(* declaring the functions in the local theory *)
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 564
fun prepare_bn_funs bn_fun_strs bn_eq_strs thy =
1941
+ − 565
let
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 566
val lthy = Named_Target.theory_init thy
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 567
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 568
val ((bn_funs, bn_eqs), lthy') =
1941
+ − 569
Specification.read_spec bn_fun_strs bn_eq_strs lthy
+ − 570
+ − 571
fun prep_bn_fun ((bn, T), mx) = (bn, T, mx)
+ − 572
+ − 573
val bn_funs' = map prep_bn_fun bn_funs
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 574
1941
+ − 575
in
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 576
(Local_Theory.exit_global lthy')
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 577
|> Sign.add_consts_i bn_funs'
1941
+ − 578
|> pair (bn_funs', bn_eqs)
+ − 579
end
+ − 580
*}
+ − 581
+ − 582
text {* associates every SOME with the index in the list; drops NONEs *}
+ − 583
ML {*
+ − 584
fun indexify xs =
+ − 585
let
+ − 586
fun mapp _ [] = []
+ − 587
| mapp i (NONE :: xs) = mapp (i + 1) xs
+ − 588
| mapp i (SOME x :: xs) = (x, i) :: mapp (i + 1) xs
+ − 589
in
+ − 590
mapp 0 xs
+ − 591
end
+ − 592
+ − 593
fun index_lookup xs x =
+ − 594
case AList.lookup (op=) xs x of
+ − 595
SOME x => x
+ − 596
| NONE => error ("Cannot find " ^ x ^ " as argument annotation.");
+ − 597
*}
+ − 598
+ − 599
ML {*
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 600
fun prepare_bclauses dt_strs thy =
1941
+ − 601
let
+ − 602
val annos_bclauses =
+ − 603
get_cnstrs dt_strs
2612
+ − 604
|> (map o map) (fn (_, antys, _, bns) => (map fst antys, bns))
1941
+ − 605
+ − 606
fun prep_binder env bn_str =
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 607
case (Syntax.read_term_global thy bn_str) of
1941
+ − 608
Free (x, _) => (NONE, index_lookup env x)
+ − 609
| Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x)
+ − 610
| _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.")
+ − 611
+ − 612
fun prep_body env bn_str = index_lookup env bn_str
+ − 613
+ − 614
fun prep_bclause env (mode, binders, bodies) =
+ − 615
let
+ − 616
val binders' = map (prep_binder env) binders
+ − 617
val bodies' = map (prep_body env) bodies
+ − 618
in
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 619
BC (mode, binders', bodies')
1941
+ − 620
end
+ − 621
+ − 622
fun prep_bclauses (annos, bclause_strs) =
+ − 623
let
+ − 624
val env = indexify annos (* for every label, associate the index *)
+ − 625
in
+ − 626
map (prep_bclause env) bclause_strs
+ − 627
end
+ − 628
in
2612
+ − 629
((map o map) prep_bclauses annos_bclauses, thy)
1941
+ − 630
end
+ − 631
*}
+ − 632
1943
+ − 633
text {*
+ − 634
adds an empty binding clause for every argument
+ − 635
that is not already part of a binding clause
+ − 636
*}
+ − 637
1941
+ − 638
ML {*
+ − 639
fun included i bcs =
+ − 640
let
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 641
fun incl (BC (_, bns, bds)) =
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 642
member (op =) (map snd bns) i orelse member (op =) bds i
1941
+ − 643
in
+ − 644
exists incl bcs
+ − 645
end
+ − 646
*}
+ − 647
+ − 648
ML {*
+ − 649
fun complete dt_strs bclauses =
+ − 650
let
+ − 651
val args =
+ − 652
get_cnstrs dt_strs
2612
+ − 653
|> (map o map) (fn (_, antys, _, _) => length antys)
1941
+ − 654
+ − 655
fun complt n bcs =
+ − 656
let
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 657
fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])])
1941
+ − 658
in
+ − 659
bcs @ (flat (map_range (add bcs) n))
+ − 660
end
+ − 661
in
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 662
(map2 o map2) complt args bclauses
1941
+ − 663
end
+ − 664
*}
+ − 665
+ − 666
ML {*
2436
+ − 667
fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy =
1941
+ − 668
let
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 669
(* this theory is used just for parsing *)
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
+ − 670
val thy = Proof_Context.theory_of lthy
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 671
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 672
val (((dts, (bn_funs, bn_eqs)), bclauses), thy') =
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 673
thy
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 674
|> prepare_dts dt_strs
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 675
||>> prepare_bn_funs bn_fun_strs bn_eq_strs
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 676
||>> prepare_bclauses dt_strs
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 677
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 678
val bclauses' = complete dt_strs bclauses
1941
+ − 679
in
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 680
nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy
1941
+ − 681
end
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 682
*}
1941
+ − 683
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 684
ML {*
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 685
(* nominal datatype parser *)
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 686
local
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 687
structure P = Parse;
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 688
structure S = Scan
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 689
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 690
fun triple1 ((x, y), z) = (x, y, z)
3065
+ − 691
fun triple2 ((x, y), z) = (y, x, z)
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 692
fun tuple2 (((x, y), z), u) = (x, y, u, z)
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 693
fun tuple3 ((x, y), (z, u)) = (x, y, z, u)
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 694
in
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 695
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 696
val _ = Keyword.keyword "binds"
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 697
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 698
val opt_name = Scan.option (P.binding --| Args.colon)
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 699
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 700
val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 701
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 702
val bind_mode = P.$$$ "binds" |--
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 703
S.optional (Args.parens
2634
3ce1089cdbf3
changed res keyword to set+ for restrictions; comment by a referee
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 704
(Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 705
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 706
val bind_clauses =
3076
2b1b8404fe0d
partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 707
P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1)
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 708
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 709
val cnstr_parser =
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 710
P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tuple2
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 711
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 712
(* datatype parser *)
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 713
val dt_parser =
3065
+ − 714
(P.type_args_constrained -- P.binding -- P.opt_mixfix >> triple2) --
+ − 715
(P.$$$ "=" |-- P.enum1 "|" cnstr_parser)
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 716
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 717
(* binding function parser *)
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 718
val bnfun_parser =
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 719
S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 720
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 721
(* main parser *)
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 722
val main_parser =
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 723
opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 724
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 725
end
1941
+ − 726
+ − 727
(* Command Keyword *)
2168
+ − 728
val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl
1941
+ − 729
(main_parser >> nominal_datatype2_cmd)
+ − 730
*}
+ − 731
2292
+ − 732
1941
+ − 733
end
+ − 734
+ − 735
+ − 736