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