2454
+ − 1
theory Nominal2
2435
+ − 2
imports
2568
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 3
Nominal2_Base Nominal2_Eqvt Nominal2_Abs
2598
+ − 4
uses ("nominal_dt_rawfuns.ML")
2435
+ − 5
("nominal_dt_alpha.ML")
+ − 6
("nominal_dt_quot.ML")
1941
+ − 7
begin
+ − 8
2611
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 9
2435
+ − 10
use "nominal_dt_rawfuns.ML"
+ − 11
ML {* open Nominal_Dt_RawFuns *}
+ − 12
+ − 13
use "nominal_dt_alpha.ML"
+ − 14
ML {* open Nominal_Dt_Alpha *}
+ − 15
+ − 16
use "nominal_dt_quot.ML"
+ − 17
ML {* open Nominal_Dt_Quot *}
+ − 18
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
+ − 19
2603
+ − 20
ML {*
+ − 21
val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+ − 22
val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
+ − 23
val simp_attr = Attrib.internal (K Simplifier.simp_add)
+ − 24
*}
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
+ − 25
1941
+ − 26
section{* Interface for nominal_datatype *}
+ − 27
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
+ − 28
ML {* print_depth 50 *}
1941
+ − 29
+ − 30
ML {*
+ − 31
fun get_cnstrs dts =
+ − 32
map (fn (_, _, _, constrs) => constrs) dts
+ − 33
+ − 34
fun get_typed_cnstrs dts =
+ − 35
flat (map (fn (_, bn, _, constrs) =>
+ − 36
(map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts)
+ − 37
+ − 38
fun get_cnstr_strs dts =
+ − 39
map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts))
+ − 40
+ − 41
fun get_bn_fun_strs bn_funs =
+ − 42
map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
+ − 43
*}
+ − 44
2106
+ − 45
1944
+ − 46
text {* Infrastructure for adding "_raw" to types and terms *}
+ − 47
1941
+ − 48
ML {*
+ − 49
fun add_raw s = s ^ "_raw"
+ − 50
fun add_raws ss = map add_raw ss
+ − 51
fun raw_bind bn = Binding.suffix_name "_raw" bn
+ − 52
+ − 53
fun replace_str ss s =
+ − 54
case (AList.lookup (op=) ss s) of
+ − 55
SOME s' => s'
+ − 56
| NONE => s
+ − 57
+ − 58
fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts)
+ − 59
| replace_typ ty_ss T = T
+ − 60
+ − 61
fun raw_dts ty_ss dts =
+ − 62
let
+ − 63
fun raw_dts_aux1 (bind, tys, mx) =
+ − 64
(raw_bind bind, map (replace_typ ty_ss) tys, mx)
+ − 65
+ − 66
fun raw_dts_aux2 (ty_args, bind, mx, constrs) =
+ − 67
(ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs)
+ − 68
in
+ − 69
map raw_dts_aux2 dts
+ − 70
end
+ − 71
+ − 72
fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T)
+ − 73
| replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T)
+ − 74
| replace_aterm trm_ss trm = trm
+ − 75
+ − 76
fun replace_term trm_ss ty_ss trm =
+ − 77
trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss)
+ − 78
*}
+ − 79
+ − 80
ML {*
+ − 81
fun rawify_dts dt_names dts dts_env =
+ − 82
let
+ − 83
val raw_dts = raw_dts dts_env dts
+ − 84
val raw_dt_names = add_raws dt_names
+ − 85
in
+ − 86
(raw_dt_names, raw_dts)
+ − 87
end
+ − 88
*}
+ − 89
+ − 90
ML {*
+ − 91
fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs =
+ − 92
let
+ − 93
val bn_funs' = map (fn (bn, ty, mx) =>
2304
+ − 94
(raw_bind bn, SOME (replace_typ dts_env ty), mx)) bn_funs
1941
+ − 95
+ − 96
val bn_eqs' = map (fn (attr, trm) =>
+ − 97
(attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs
+ − 98
in
+ − 99
(bn_funs', bn_eqs')
+ − 100
end
+ − 101
*}
+ − 102
+ − 103
ML {*
+ − 104
fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses =
+ − 105
let
+ − 106
fun rawify_bnds bnds =
+ − 107
map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds
+ − 108
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
+ − 109
fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys)
1941
+ − 110
in
2612
+ − 111
(map o map o map) rawify_bclause bclauses
1941
+ − 112
end
+ − 113
*}
+ − 114
+ − 115
+ − 116
ML {*
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 117
fun define_raw_dts dts bn_funs bn_eqs bclauses lthy =
1941
+ − 118
let
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 119
val thy = Local_Theory.exit_global lthy
1941
+ − 120
val thy_name = Context.theory_name thy
+ − 121
+ − 122
val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
+ − 123
val dt_full_names = map (Long_Name.qualify thy_name) dt_names
+ − 124
val dt_full_names' = add_raws dt_full_names
+ − 125
val dts_env = dt_full_names ~~ dt_full_names'
+ − 126
+ − 127
val cnstrs = get_cnstr_strs dts
+ − 128
val cnstrs_ty = get_typed_cnstrs dts
+ − 129
val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs
+ − 130
val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name
+ − 131
(Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty
+ − 132
val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names'
+ − 133
+ − 134
val bn_fun_strs = get_bn_fun_strs bn_funs
+ − 135
val bn_fun_strs' = add_raws bn_fun_strs
+ − 136
val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
+ − 137
val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name))
+ − 138
(bn_fun_strs ~~ bn_fun_strs')
+ − 139
+ − 140
val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
+ − 141
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
+ − 142
val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses
1941
+ − 143
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 144
val (raw_dt_full_names, thy1) =
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 145
Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 146
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 147
val lthy1 = Named_Target.theory_init thy1
2304
+ − 148
in
2337
+ − 149
(raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1)
2304
+ − 150
end
+ − 151
*}
+ − 152
2046
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
ML {*
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 154
(* for testing porposes - to exit the procedure early *)
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 155
exception TEST of Proof.context
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 156
2436
+ − 157
val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 100);
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
+ − 158
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
+ − 159
fun get_STEPS ctxt = Config.get ctxt STEPS
2046
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 160
*}
2008
1bddffddc03f
attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 161
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
+ − 162
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
+ − 163
setup STEPS_setup
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
+ − 164
1941
+ − 165
ML {*
2436
+ − 166
fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =
1941
+ − 167
let
2294
+ − 168
(* definition of the raw datatypes *)
2316
+ − 169
val _ = warning "Definition of raw datatypes";
2337
+ − 170
val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
2308
+ − 171
if get_STEPS lthy > 0
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 172
then define_raw_dts dts bn_funs bn_eqs bclauses lthy
2046
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 173
else raise TEST lthy
1941
+ − 174
2304
+ − 175
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
2143
871d8a5e0c67
somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 176
val {descr, sorts, ...} = dtinfo
2407
+ − 177
2400
+ − 178
val raw_tys = all_dtyps descr sorts
+ − 179
val raw_full_ty_names = map (fst o dest_Type) raw_tys
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 180
val tvs = hd raw_tys
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 181
|> snd o dest_Type
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 182
|> map dest_TFree
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 183
2400
+ − 184
val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names
+ − 185
2407
+ − 186
val raw_cns_info = all_dtyp_constrs_types descr sorts
2612
+ − 187
val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info
2407
+ − 188
2400
+ − 189
val raw_inject_thms = flat (map #inject dtinfos)
+ − 190
val raw_distinct_thms = flat (map #distinct dtinfos)
+ − 191
val raw_induct_thm = #induct dtinfo
+ − 192
val raw_induct_thms = #inducts dtinfo
+ − 193
val raw_exhaust_thms = map #exhaust dtinfos
2611
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 194
val raw_size_trms = map HOLogic.size_const raw_tys
2388
+ − 195
val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
+ − 196
|> `(fn thms => (length thms) div 2)
2392
+ − 197
|> uncurry drop
2388
+ − 198
2409
+ − 199
(* definitions of raw permutations by primitive recursion *)
2316
+ − 200
val _ = warning "Definition of raw permutations";
2401
7645e18e8b19
modified the code for class instantiations (with help from Florian)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 201
val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
2560
+ − 202
if get_STEPS lthy0 > 0
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 203
then define_raw_perms raw_full_ty_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0
2308
+ − 204
else raise TEST lthy0
2144
+ − 205
+ − 206
(* noting the raw permutations as eqvt theorems *)
2448
+ − 207
val (_, lthy3) = 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
+ − 208
2560
+ − 209
(* definition of raw fv and bn functions *)
+ − 210
val _ = warning "Definition of raw fv- and bn-functions";
2405
+ − 211
val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) =
2560
+ − 212
if get_STEPS lthy3 > 1
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 213
then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 214
(raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
2046
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 215
else raise TEST lthy3
2292
+ − 216
2560
+ − 217
(* defining the permute_bn functions *)
2561
+ − 218
val (raw_perm_bns, raw_perm_bn_simps, lthy3b) =
2560
+ − 219
if get_STEPS lthy3a > 2
+ − 220
then define_raw_bn_perms raw_tys raw_bn_info raw_cns_info
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 221
(raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a
2308
+ − 222
else raise TEST lthy3a
+ − 223
2560
+ − 224
val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) =
+ − 225
if get_STEPS lthy3b > 3
+ − 226
then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses
+ − 227
(raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b
+ − 228
else raise TEST lthy3b
+ − 229
2011
12ce87b55f97
tried to add some comments in the huge(!) nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 230
(* definition of raw alphas *)
2316
+ − 231
val _ = warning "Definition of alphas";
2300
+ − 232
val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
2560
+ − 233
if get_STEPS lthy3c > 4
+ − 234
then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c
+ − 235
else raise TEST lthy3c
2336
+ − 236
val alpha_tys = map (domain_type o fastype_of) alpha_trms
+ − 237
2300
+ − 238
(* definition of alpha-distinct lemmas *)
2316
+ − 239
val _ = warning "Distinct theorems";
2399
+ − 240
val alpha_distincts =
2400
+ − 241
mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys
2300
+ − 242
2361
+ − 243
(* definition of alpha_eq_iff lemmas *)
2316
+ − 244
val _ = warning "Eq-iff theorems";
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
+ − 245
val alpha_eq_iff =
2295
+ − 246
if get_STEPS lthy > 5
2400
+ − 247
then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases
2295
+ − 248
else raise TEST lthy4
2022
+ − 249
2388
+ − 250
(* proving equivariance lemmas for bns, fvs, size and alpha *)
2001
7c8242a02f39
NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 251
val _ = warning "Proving equivariance";
2406
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 252
val raw_bn_eqvt =
2298
+ − 253
if get_STEPS lthy > 6
2405
+ − 254
then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_defs @ raw_perm_simps) lthy4
2298
+ − 255
else raise TEST lthy4
+ − 256
2406
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 257
(* noting the raw_bn_eqvt lemmas in a temprorary theory *)
2448
+ − 258
val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4)
2305
+ − 259
2406
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 260
val raw_fv_eqvt =
2298
+ − 261
if get_STEPS lthy > 7
2384
+ − 262
then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps)
2388
+ − 263
(Local_Theory.restore lthy_tmp)
+ − 264
else raise TEST lthy4
+ − 265
2389
+ − 266
val raw_size_eqvt =
2388
+ − 267
if get_STEPS lthy > 8
+ − 268
then raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps)
+ − 269
(Local_Theory.restore lthy_tmp)
2389
+ − 270
|> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]})
+ − 271
|> map (fn thm => thm RS @{thm sym})
2305
+ − 272
else raise TEST lthy4
+ − 273
2448
+ − 274
val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)
2306
+ − 275
2336
+ − 276
val (alpha_eqvt, lthy6) =
2388
+ − 277
if get_STEPS lthy > 9
2336
+ − 278
then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
2311
+ − 279
else raise TEST lthy4
+ − 280
+ − 281
(* proving alpha equivalence *)
+ − 282
val _ = warning "Proving equivalence"
+ − 283
2316
+ − 284
val alpha_refl_thms =
2388
+ − 285
if get_STEPS lthy > 10
+ − 286
then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6
2336
+ − 287
else raise TEST lthy6
2316
+ − 288
2311
+ − 289
val alpha_sym_thms =
2388
+ − 290
if get_STEPS lthy > 11
2336
+ − 291
then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6
+ − 292
else raise TEST lthy6
2298
+ − 293
2311
+ − 294
val alpha_trans_thms =
2388
+ − 295
if get_STEPS lthy > 12
2400
+ − 296
then raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms)
2336
+ − 297
alpha_intros alpha_induct alpha_cases lthy6
+ − 298
else raise TEST lthy6
2311
+ − 299
2404
+ − 300
val (alpha_equivp_thms, alpha_bn_equivp_thms) =
2388
+ − 301
if get_STEPS lthy > 13
2404
+ − 302
then raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms
+ − 303
alpha_trans_thms lthy6
2336
+ − 304
else raise TEST lthy6
2322
+ − 305
2320
+ − 306
(* proving alpha implies alpha_bn *)
+ − 307
val _ = warning "Proving alpha implies bn"
+ − 308
+ − 309
val alpha_bn_imp_thms =
2388
+ − 310
if get_STEPS lthy > 14
2336
+ − 311
then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6
+ − 312
else raise TEST lthy6
2322
+ − 313
2397
+ − 314
(* respectfulness proofs *)
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_funs_rsp_aux =
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 316
if get_STEPS lthy > 15
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 317
then raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 318
raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 319
else raise TEST lthy6
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 320
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 321
val raw_funs_rsp =
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 322
if get_STEPS lthy > 16
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 323
then map mk_funs_rsp raw_funs_rsp_aux
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 324
else raise TEST lthy6
2388
+ − 325
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 326
val raw_size_rsp =
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 327
if get_STEPS lthy > 17
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 328
then
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 329
raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 330
(raw_size_thms @ raw_size_eqvt) lthy6
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 331
|> map mk_funs_rsp
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 332
else raise TEST lthy6
2392
+ − 333
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 334
val raw_constrs_rsp =
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 335
if get_STEPS lthy > 18
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 336
then raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 337
(alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 338
else raise TEST lthy6
2397
+ − 339
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 340
val alpha_permute_rsp =
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 341
if get_STEPS lthy > 19
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 342
then map mk_alpha_permute_rsp alpha_eqvt
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 343
else raise TEST lthy6
2384
+ − 344
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 345
val alpha_bn_rsp =
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 346
if get_STEPS lthy > 20
2440
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 347
then raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 348
else raise TEST lthy6
2404
+ − 349
2561
+ − 350
val raw_perm_bn_rsp =
+ − 351
if get_STEPS lthy > 21
+ − 352
then raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct
+ − 353
alpha_intros raw_perm_bn_simps lthy6
+ − 354
else raise TEST lthy6
+ − 355
2398
+ − 356
(* noting the quot_respects lemmas *)
+ − 357
val (_, lthy6a) =
2561
+ − 358
if get_STEPS lthy > 22
2448
+ − 359
then Local_Theory.note ((Binding.empty, [rsp_attr]),
2561
+ − 360
raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @
+ − 361
alpha_bn_rsp @ raw_perm_bn_rsp) lthy6
2398
+ − 362
else raise TEST lthy6
+ − 363
2336
+ − 364
(* defining the quotient type *)
+ − 365
val _ = warning "Declaring the quotient types"
+ − 366
val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
2400
+ − 367
2336
+ − 368
val (qty_infos, lthy7) =
2561
+ − 369
if get_STEPS lthy > 23
2400
+ − 370
then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
2398
+ − 371
else raise TEST lthy6a
2336
+ − 372
+ − 373
val qtys = map #qtyp qty_infos
2400
+ − 374
val qty_full_names = map (fst o dest_Type) qtys
+ − 375
val qty_names = map Long_Name.base_name qty_full_names
+ − 376
2339
+ − 377
(* defining of quotient term-constructors, binding functions, free vars functions *)
2378
+ − 378
val _ = warning "Defining the quotient constants"
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 379
val qconstrs_descrs =
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
+ − 380
(map2 o map2) (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) (get_cnstrs dts) raw_constrs
2338
+ − 381
2339
+ − 382
val qbns_descr =
2346
+ − 383
map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns
2339
+ − 384
+ − 385
val qfvs_descr =
2346
+ − 386
map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
2339
+ − 387
2346
+ − 388
val qfv_bns_descr =
2398
+ − 389
map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns
2339
+ − 390
2384
+ − 391
val qalpha_bns_descr =
+ − 392
map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms
+ − 393
2398
+ − 394
val qperm_descr =
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 395
map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
2398
+ − 396
2400
+ − 397
val qsize_descr =
+ − 398
map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
+ − 399
2562
+ − 400
val qperm_bn_descr =
+ − 401
map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns
+ − 402
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 403
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
+ − 404
lthy8) =
2561
+ − 405
if get_STEPS lthy > 24
2346
+ − 406
then
+ − 407
lthy7
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 408
|> fold_map (define_qconsts qtys) qconstrs_descrs
2400
+ − 409
||>> define_qconsts qtys qbns_descr
+ − 410
||>> define_qconsts qtys qfvs_descr
+ − 411
||>> define_qconsts qtys qfv_bns_descr
+ − 412
||>> define_qconsts qtys qalpha_bns_descr
2562
+ − 413
||>> define_qconsts qtys qperm_bn_descr
2338
+ − 414
else raise TEST lthy7
+ − 415
2400
+ − 416
(* definition of the quotient permfunctions and pt-class *)
+ − 417
val lthy9 =
2561
+ − 418
if get_STEPS lthy > 25
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 419
then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8
2400
+ − 420
else raise TEST lthy8
+ − 421
2401
7645e18e8b19
modified the code for class instantiations (with help from Florian)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 422
val lthy9a =
2561
+ − 423
if get_STEPS lthy > 26
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 424
then define_qsizes qtys qty_full_names tvs qsize_descr lthy9
2400
+ − 425
else raise TEST lthy9
2398
+ − 426
2612
+ − 427
val qtrms = (map o map) #qconst qconstrs_infos
2346
+ − 428
val qbns = map #qconst qbns_info
+ − 429
val qfvs = map #qconst qfvs_info
+ − 430
val qfv_bns = map #qconst qfv_bns_info
2384
+ − 431
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
+ − 432
val qperm_bns = map #qconst qperm_bns_info
2434
+ − 433
+ − 434
(* lifting of the theorems *)
+ − 435
val _ = warning "Lifting of Theorems"
+ − 436
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
+ − 437
val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def
2434
+ − 438
prod.cases}
+ − 439
+ − 440
val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) =
2561
+ − 441
if get_STEPS lthy > 27
2434
+ − 442
then
+ − 443
lthy9a
+ − 444
|> lift_thms qtys [] alpha_distincts
+ − 445
||>> lift_thms qtys eq_iff_simps alpha_eq_iff
+ − 446
||>> lift_thms qtys [] raw_fv_defs
+ − 447
||>> lift_thms qtys [] raw_bn_defs
+ − 448
||>> lift_thms qtys [] raw_perm_simps
+ − 449
||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
+ − 450
else raise TEST lthy9a
+ − 451
2594
+ − 452
val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) =
2561
+ − 453
if get_STEPS lthy > 28
2434
+ − 454
then
+ − 455
lthyA
+ − 456
|> lift_thms qtys [] raw_size_eqvt
+ − 457
||>> lift_thms qtys [] [raw_induct_thm]
+ − 458
||>> lift_thms qtys [] raw_exhaust_thms
2487
+ − 459
||>> lift_thms qtys [] raw_size_thms
2563
+ − 460
||>> lift_thms qtys [] raw_perm_bn_simps
2594
+ − 461
||>> lift_thms qtys [] alpha_refl_thms
2434
+ − 462
else raise TEST lthyA
+ − 463
2474
+ − 464
val qinducts = Project_Rule.projections lthyA qinduct
+ − 465
2451
+ − 466
(* supports lemmas *)
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
+ − 467
val _ = warning "Proving Supports Lemmas and fs-Instances"
2448
+ − 468
val qsupports_thms =
2561
+ − 469
if get_STEPS lthy > 29
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 470
then prove_supports lthyB qperm_simps (flat qtrms)
2448
+ − 471
else raise TEST lthyB
+ − 472
2451
+ − 473
(* finite supp lemmas *)
2450
+ − 474
val qfsupp_thms =
2561
+ − 475
if get_STEPS lthy > 30
2450
+ − 476
then prove_fsupp lthyB qtys qinduct qsupports_thms
+ − 477
else raise TEST lthyB
+ − 478
2451
+ − 479
(* fs instances *)
+ − 480
val lthyC =
2561
+ − 481
if get_STEPS lthy > 31
2451
+ − 482
then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB
+ − 483
else raise TEST lthyB
2448
+ − 484
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
+ − 485
(* fv - supp equality *)
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
+ − 486
val _ = warning "Proving Equality between fv and supp"
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
+ − 487
val qfv_supp_thms =
2561
+ − 488
if get_STEPS lthy > 32
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 489
then 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
+ − 490
qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
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
+ − 491
else []
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
+ − 492
2492
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 493
(* 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
+ − 494
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 495
val qeq_iffs' = qeq_iffs
2493
+ − 496
|> map (simplify (HOL_basic_ss addsimps qfv_supp_thms))
+ − 497
|> 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
+ − 498
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 499
val qsupp_constrs = qfv_defs
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 500
|> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms)))
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 501
2493
+ − 502
val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp}
+ − 503
val transform_thms =
+ − 504
[ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp},
+ − 505
@{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp},
+ − 506
@{lemma "(lhs = (a \<notin> {})) \<longleftrightarrow> lhs" by simp},
+ − 507
@{thm fresh_def[symmetric]}]
+ − 508
+ − 509
val qfresh_constrs = qsupp_constrs
+ − 510
|> map (fn thm => thm RS transform_thm)
+ − 511
|> map (simplify (HOL_basic_ss addsimps transform_thms))
+ − 512
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
+ − 513
(* proving that the qbn result is finite *)
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
+ − 514
val qbn_finite_thms =
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
+ − 515
if get_STEPS lthy > 33
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
then prove_bns_finite qtys qbns qinduct qbn_defs lthyC
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
+ − 517
else []
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
+ − 518
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
+ − 519
(* proving that perm_bns preserve alpha *)
2594
+ − 520
val qperm_bn_alpha_thms =
+ − 521
if get_STEPS lthy > 33
+ − 522
then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs'
+ − 523
qalpha_refl_thms lthyC
+ − 524
else []
2493
+ − 525
2598
+ − 526
(* proving the relationship of bn and permute_bn *)
+ − 527
val qpermute_bn_thms =
+ − 528
if get_STEPS lthy > 33
+ − 529
then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
+ − 530
else []
+ − 531
2619
+ − 532
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
+ − 533
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
+ − 534
2603
+ − 535
2436
+ − 536
(* noting the theorems *)
+ − 537
+ − 538
(* generating the prefix for the theorem names *)
+ − 539
val thms_name =
+ − 540
the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name
+ − 541
fun thms_suffix s = Binding.qualified true s thms_name
+ − 542
2451
+ − 543
val (_, lthy9') = lthyC
2436
+ − 544
|> Local_Theory.note ((thms_suffix "distinct", []), qdistincts)
2492
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 545
||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs')
2436
+ − 546
||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs)
+ − 547
||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs)
2448
+ − 548
||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps)
2436
+ − 549
||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts)
2487
+ − 550
||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps)
2436
+ − 551
||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
+ − 552
||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct])
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
+ − 553
||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)
2436
+ − 554
||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 555
||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms)
2448
+ − 556
||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
2450
+ − 557
||>> 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
+ − 558
||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
2493
+ − 559
||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
2500
+ − 560
||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
2563
+ − 561
||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
2571
+ − 562
||>> 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
+ − 563
||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)
2598
+ − 564
||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms)
1941
+ − 565
in
2601
+ − 566
lthy9'
+ − 567
end handle TEST ctxt => ctxt
1941
+ − 568
*}
+ − 569
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
+ − 570
1941
+ − 571
section {* Preparing and parsing of the specification *}
+ − 572
+ − 573
ML {*
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 574
(* generates the parsed datatypes and
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 575
declares the constructors
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 576
*)
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 577
fun prepare_dts dt_strs thy =
1941
+ − 578
let
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 579
fun inter_fs_sort thy (a, S) =
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 580
(a, Type.inter_sort (Sign.tsig_of thy) (@{sort fs}, S))
1941
+ − 581
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 582
fun mk_type tname sorts (cname, cargs, mx) =
1941
+ − 583
let
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 584
val full_tname = Sign.full_name thy tname
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 585
val ty = Type (full_tname, map (TFree o inter_fs_sort thy) sorts)
1941
+ − 586
in
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 587
(cname, cargs ---> ty, mx)
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 588
end
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 589
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 590
fun prep_constr (cname, cargs, mx, _) (constrs, sorts) =
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 591
let
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 592
val (cargs', sorts') =
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 593
fold_map (Datatype.read_typ thy) (map snd cargs) sorts
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 594
|>> map (map_type_tfree (TFree o inter_fs_sort thy))
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 595
in
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 596
(constrs @ [(cname, cargs', mx)], sorts')
1941
+ − 597
end
+ − 598
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 599
fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) =
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 600
let
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 601
val (constrs', sorts') =
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 602
fold prep_constr constrs ([], sorts)
1941
+ − 603
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 604
val constr_trms' =
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 605
map (mk_type tname (rev sorts')) constrs'
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 606
in
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 607
(constr_trms @ constr_trms', dts @ [(tvs, tname, mx, constrs')], sorts')
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 608
end
2425
+ − 609
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 610
val (constr_trms, dts, sorts) = fold prep_dts dt_strs ([], [], []);
1941
+ − 611
in
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 612
thy
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 613
|> Sign.add_consts_i constr_trms
1941
+ − 614
|> pair dts
+ − 615
end
+ − 616
*}
+ − 617
+ − 618
ML {*
+ − 619
(* parsing the binding function specification and *)
+ − 620
(* 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
+ − 621
fun prepare_bn_funs bn_fun_strs bn_eq_strs thy =
1941
+ − 622
let
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 623
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
+ − 624
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 625
val ((bn_funs, bn_eqs), lthy') =
1941
+ − 626
Specification.read_spec bn_fun_strs bn_eq_strs lthy
+ − 627
+ − 628
fun prep_bn_fun ((bn, T), mx) = (bn, T, mx)
+ − 629
+ − 630
val bn_funs' = map prep_bn_fun bn_funs
+ − 631
in
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 632
(Local_Theory.exit_global lthy')
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 633
|> Sign.add_consts_i bn_funs'
1941
+ − 634
|> pair (bn_funs', bn_eqs)
+ − 635
end
+ − 636
*}
+ − 637
+ − 638
text {* associates every SOME with the index in the list; drops NONEs *}
+ − 639
ML {*
+ − 640
fun indexify xs =
+ − 641
let
+ − 642
fun mapp _ [] = []
+ − 643
| mapp i (NONE :: xs) = mapp (i + 1) xs
+ − 644
| mapp i (SOME x :: xs) = (x, i) :: mapp (i + 1) xs
+ − 645
in
+ − 646
mapp 0 xs
+ − 647
end
+ − 648
+ − 649
fun index_lookup xs x =
+ − 650
case AList.lookup (op=) xs x of
+ − 651
SOME x => x
+ − 652
| NONE => error ("Cannot find " ^ x ^ " as argument annotation.");
+ − 653
*}
+ − 654
+ − 655
ML {*
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 656
fun prepare_bclauses dt_strs thy =
1941
+ − 657
let
+ − 658
val annos_bclauses =
+ − 659
get_cnstrs dt_strs
2612
+ − 660
|> (map o map) (fn (_, antys, _, bns) => (map fst antys, bns))
1941
+ − 661
+ − 662
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
+ − 663
case (Syntax.read_term_global thy bn_str) of
1941
+ − 664
Free (x, _) => (NONE, index_lookup env x)
+ − 665
| Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x)
+ − 666
| _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.")
+ − 667
+ − 668
fun prep_body env bn_str = index_lookup env bn_str
+ − 669
+ − 670
fun prep_bclause env (mode, binders, bodies) =
+ − 671
let
+ − 672
val binders' = map (prep_binder env) binders
+ − 673
val bodies' = map (prep_body env) bodies
+ − 674
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
+ − 675
BC (mode, binders', bodies')
1941
+ − 676
end
+ − 677
+ − 678
fun prep_bclauses (annos, bclause_strs) =
+ − 679
let
+ − 680
val env = indexify annos (* for every label, associate the index *)
+ − 681
in
+ − 682
map (prep_bclause env) bclause_strs
+ − 683
end
+ − 684
in
2612
+ − 685
((map o map) prep_bclauses annos_bclauses, thy)
1941
+ − 686
end
+ − 687
*}
+ − 688
1943
+ − 689
text {*
+ − 690
adds an empty binding clause for every argument
+ − 691
that is not already part of a binding clause
+ − 692
*}
+ − 693
1941
+ − 694
ML {*
+ − 695
fun included i bcs =
+ − 696
let
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 697
fun incl (BC (_, bns, bds)) =
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 698
member (op =) (map snd bns) i orelse member (op =) bds i
1941
+ − 699
in
+ − 700
exists incl bcs
+ − 701
end
+ − 702
*}
+ − 703
+ − 704
ML {*
+ − 705
fun complete dt_strs bclauses =
+ − 706
let
+ − 707
val args =
+ − 708
get_cnstrs dt_strs
2612
+ − 709
|> (map o map) (fn (_, antys, _, _) => length antys)
1941
+ − 710
+ − 711
fun complt n bcs =
+ − 712
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
+ − 713
fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])])
1941
+ − 714
in
+ − 715
bcs @ (flat (map_range (add bcs) n))
+ − 716
end
+ − 717
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
+ − 718
(map2 o map2) complt args bclauses
1941
+ − 719
end
+ − 720
*}
+ − 721
+ − 722
ML {*
2436
+ − 723
fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy =
1941
+ − 724
let
2436
+ − 725
val pre_typs =
+ − 726
map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 727
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 728
(* this theory is used just for parsing *)
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 729
val thy = ProofContext.theory_of lthy
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 730
val tmp_thy = Theory.copy thy
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 731
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 732
val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') =
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 733
tmp_thy
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 734
|> Sign.add_types pre_typs
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 735
|> prepare_dts dt_strs
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 736
||>> prepare_bn_funs bn_fun_strs bn_eq_strs
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 737
||>> prepare_bclauses dt_strs
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 738
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 739
val bclauses' = complete dt_strs bclauses
1941
+ − 740
in
2601
+ − 741
timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy)
1941
+ − 742
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
+ − 743
*}
1941
+ − 744
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
+ − 745
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
+ − 746
(* 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
+ − 747
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
+ − 748
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
+ − 749
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
+ − 750
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 751
fun triple ((x, y), z) = (x, y, z)
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 752
fun tuple1 ((x, y, z), u) = (x, y, z, u)
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 753
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
+ − 754
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
+ − 755
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
+ − 756
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
+ − 757
val _ = Keyword.keyword "bind"
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 758
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 759
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
+ − 760
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
+ − 761
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
+ − 762
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
+ − 763
val bind_mode = P.$$$ "bind" |--
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
+ − 764
S.optional (Args.parens
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 765
(Args.$$$ "list" >> K Lst || Args.$$$ "set" >> K Set || Args.$$$ "res" >> K Res)) 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
+ − 766
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
+ − 767
val bind_clauses =
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 768
P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple)
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
+ − 769
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
+ − 770
val cnstr_parser =
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 771
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
+ − 772
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
+ − 773
(* 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
+ − 774
val dt_parser =
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 775
(P.type_args -- P.binding -- P.opt_mixfix >> triple) --
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 776
(P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple1
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
+ − 777
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
+ − 778
(* 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
+ − 779
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
+ − 780
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
+ − 781
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
+ − 782
(* 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
+ − 783
val main_parser =
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 784
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
+ − 785
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
+ − 786
end
1941
+ − 787
+ − 788
(* Command Keyword *)
2168
+ − 789
val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl
1941
+ − 790
(main_parser >> nominal_datatype2_cmd)
+ − 791
*}
+ − 792
2292
+ − 793
1941
+ − 794
end
+ − 795
+ − 796
+ − 797