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