2297
+ − 1
(* Title: nominal_dt_rawfuns.ML
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>
parents:
diff
changeset
+ − 2
Author: Cezary Kaliszyk
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>
parents:
diff
changeset
+ − 3
Author: Christian Urban
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>
parents:
diff
changeset
+ − 4
2598
+ − 5
Definitions of the raw fv, fv_bn and permute functions.
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>
parents:
diff
changeset
+ − 6
*)
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>
parents:
diff
changeset
+ − 7
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>
parents:
diff
changeset
+ − 8
signature NOMINAL_DT_RAWFUNS =
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>
parents:
diff
changeset
+ − 9
sig
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 10
(* info of raw datatypes *)
2601
+ − 11
type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 12
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 13
(* info of raw binding functions *)
2560
+ − 14
type bn_info = term * int * (int * term option) list list
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>
parents:
diff
changeset
+ − 15
2295
+ − 16
(* binding modes and binding clauses *)
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>
parents:
diff
changeset
+ − 17
datatype bmode = Lst | Res | Set
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>
parents:
diff
changeset
+ − 18
datatype bclause = BC of bmode * (term option * int) list * int list
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>
parents:
diff
changeset
+ − 19
2608
+ − 20
val get_all_binders: bclause list -> (term option * int) list
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
+ − 21
val is_recursive_binder: bclause -> bool
2608
+ − 22
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23
val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list ->
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24
(Attrib.binding * term) list -> thm list -> thm list -> local_theory ->
2560
+ − 25
(term list * thm list * bn_info list * thm list * local_theory)
2601
+ − 26
2560
+ − 27
val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list ->
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 28
thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
2560
+ − 29
+ − 30
val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list ->
+ − 31
local_theory -> (term list * thm list * local_theory)
2305
+ − 32
+ − 33
val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list
2598
+ − 34
+ − 35
val define_raw_perms: string list -> typ list -> (string * sort) list -> term list -> thm ->
+ − 36
local_theory -> (term list * thm list * thm list) * local_theory
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>
parents:
diff
changeset
+ − 37
end
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>
parents:
diff
changeset
+ − 38
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>
parents:
diff
changeset
+ − 39
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>
parents:
diff
changeset
+ − 40
structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
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>
parents:
diff
changeset
+ − 41
struct
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>
parents:
diff
changeset
+ − 42
2765
7ac5e5c86c7d
introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 43
open Nominal_Permeq
7ac5e5c86c7d
introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 45
(* string list - type variables of a datatype
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 46
binding - name of the datatype
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 47
mixfix - its mixfix
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 48
(binding * typ list * mixfix) list - datatype constructors of the type
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 49
*)
2601
+ − 50
type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 51
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 52
2375
+ − 53
(* term - is constant of the bn-function
+ − 54
int - is datatype number over which the bn-function is defined
+ − 55
int * term option - is number of the corresponding argument with possibly
+ − 56
recursive call with bn-function term
+ − 57
*)
2560
+ − 58
type bn_info = term * int * (int * term option) list list
2295
+ − 59
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 60
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>
parents:
diff
changeset
+ − 61
datatype bmode = Lst | Res | Set
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>
parents:
diff
changeset
+ − 62
datatype bclause = BC of bmode * (term option * int) list * int list
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>
parents:
diff
changeset
+ − 63
2608
+ − 64
fun get_all_binders bclauses =
+ − 65
bclauses
2611
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 66
|> map (fn (BC (_, binders, _)) => binders)
2608
+ − 67
|> flat
+ − 68
|> remove_dups (op =)
+ − 69
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
+ − 70
fun is_recursive_binder (BC (_, binders, bodies)) =
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
+ − 71
case (inter (op =) (map snd binders) bodies) of
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
+ − 72
nil => false
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
+ − 73
| _ => true
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
+ − 74
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
+ − 75
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 76
fun lookup xs x = the (AList.lookup (op=) xs x)
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 77
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 78
2601
+ − 79
(** functions that define the raw binding functions **)
+ − 80
+ − 81
(* strip_bn_fun takes a rhs of a bn function: this can only contain unions or
+ − 82
appends of elements; in case of recursive calls it returns also the applied
+ − 83
bn function *)
+ − 84
fun strip_bn_fun lthy args t =
+ − 85
let
+ − 86
fun aux t =
+ − 87
case t of
+ − 88
Const (@{const_name sup}, _) $ l $ r => aux l @ aux r
+ − 89
| Const (@{const_name append}, _) $ l $ r => aux l @ aux r
+ − 90
| Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
+ − 91
(find_index (equal x) args, NONE) :: aux y
+ − 92
| Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
+ − 93
(find_index (equal x) args, NONE) :: aux y
+ − 94
| Const (@{const_name bot}, _) => []
+ − 95
| Const (@{const_name Nil}, _) => []
+ − 96
| (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)]
+ − 97
| _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t))
+ − 98
in
+ − 99
aux t
+ − 100
end
+ − 101
+ − 102
(** definition of the raw binding functions **)
+ − 103
+ − 104
fun prep_bn_info lthy dt_names dts bn_funs eqs =
+ − 105
let
+ − 106
fun process_eq eq =
+ − 107
let
+ − 108
val (lhs, rhs) = eq
+ − 109
|> HOLogic.dest_Trueprop
+ − 110
|> HOLogic.dest_eq
+ − 111
val (bn_fun, [cnstr]) = strip_comb lhs
+ − 112
val (_, ty) = dest_Const bn_fun
+ − 113
val (ty_name, _) = dest_Type (domain_type ty)
+ − 114
val dt_index = find_index (fn x => x = ty_name) dt_names
+ − 115
val (cnstr_head, cnstr_args) = strip_comb cnstr
+ − 116
val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head))
+ − 117
val rhs_elements = strip_bn_fun lthy cnstr_args rhs
+ − 118
in
+ − 119
((bn_fun, dt_index), (cnstr_name, rhs_elements))
+ − 120
end
+ − 121
+ − 122
(* order according to constructor names *)
+ − 123
fun cntrs_order ((bn, dt_index), data) =
+ − 124
let
+ − 125
val dt = nth dts dt_index
+ − 126
val cts = (fn (_, _, _, x) => x) dt
+ − 127
val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts
+ − 128
in
+ − 129
(bn, (bn, dt_index, order (op=) ct_names data))
+ − 130
end
+ − 131
in
+ − 132
eqs
+ − 133
|> map process_eq
+ − 134
|> AList.group (op=) (* eqs grouped according to bn_functions *)
+ − 135
|> map cntrs_order (* inner data ordered according to constructors *)
+ − 136
|> order (op=) bn_funs (* ordered according to bn_functions *)
+ − 137
end
+ − 138
+ − 139
fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
+ − 140
if null raw_bn_funs
+ − 141
then ([], [], [], [], lthy)
+ − 142
else
+ − 143
let
+ − 144
val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs
+ − 145
Function_Common.default_config (pat_completeness_simp constr_thms) lthy
+ − 146
2630
+ − 147
val (info, lthy2) = prove_termination_fun size_thms (Local_Theory.restore lthy1)
2601
+ − 148
val {fs, simps, inducts, ...} = info
+ − 149
+ − 150
val raw_bn_induct = (the inducts)
+ − 151
val raw_bn_eqs = the simps
+ − 152
+ − 153
val raw_bn_info =
+ − 154
prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs)
+ − 155
in
+ − 156
(fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
+ − 157
end
+ − 158
+ − 159
+ − 160
2295
+ − 161
(** functions that construct the equations for fv and fv_bn **)
2292
+ − 162
2464
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 163
fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) =
2295
+ − 164
let
2476
+ − 165
fun mk_fv_body fv_map args i =
+ − 166
let
+ − 167
val arg = nth args i
+ − 168
val ty = fastype_of arg
+ − 169
in
+ − 170
case AList.lookup (op=) fv_map ty of
+ − 171
NONE => mk_supp arg
+ − 172
| SOME fv => fv $ arg
+ − 173
end
2295
+ − 174
2464
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 175
fun mk_fv_binder lthy fv_bn_map args binders =
2476
+ − 176
let
+ − 177
fun bind_set lthy args (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"})
+ − 178
| bind_set _ args (SOME bn, i) = (bn $ (nth args i),
+ − 179
if member (op=) bodies i then @{term "{}::atom set"}
+ − 180
else lookup fv_bn_map bn $ (nth args i))
+ − 181
fun bind_lst lthy args (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"})
+ − 182
| bind_lst _ args (SOME bn, i) = (bn $ (nth args i),
+ − 183
if member (op=) bodies i then @{term "[]::atom list"}
+ − 184
else lookup fv_bn_map bn $ (nth args i))
2464
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 185
2476
+ − 186
val (combine_fn, bind_fn) =
+ − 187
case bmode of
+ − 188
Lst => (fold_append, bind_lst)
+ − 189
| Set => (fold_union, bind_set)
+ − 190
| Res => (fold_union, bind_set)
+ − 191
in
+ − 192
binders
+ − 193
|> map (bind_fn lthy args)
+ − 194
|> split_list
+ − 195
|> pairself combine_fn
+ − 196
end
2295
+ − 197
2476
+ − 198
val t1 = map (mk_fv_body fv_map args) bodies
+ − 199
val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders
+ − 200
in
+ − 201
mk_union (mk_diff (fold_union t1, to_set t2), to_set t3)
+ − 202
end
2292
+ − 203
2293
+ − 204
(* in case of fv_bn we have to treat the case special, where an
+ − 205
"empty" binding clause is given *)
2292
+ − 206
fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
2295
+ − 207
let
2476
+ − 208
fun mk_fv_bn_body i =
+ − 209
let
+ − 210
val arg = nth args i
+ − 211
val ty = fastype_of arg
+ − 212
in
+ − 213
case AList.lookup (op=) bn_args i of
+ − 214
NONE => (case (AList.lookup (op=) fv_map ty) of
+ − 215
NONE => mk_supp arg
+ − 216
| SOME fv => fv $ arg)
+ − 217
| SOME (NONE) => @{term "{}::atom set"}
+ − 218
| SOME (SOME bn) => lookup fv_bn_map bn $ arg
+ − 219
end
2295
+ − 220
in
2476
+ − 221
case bclause of
+ − 222
BC (_, [], bodies) => fold_union (map mk_fv_bn_body bodies)
+ − 223
| _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
+ − 224
end
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>
parents:
diff
changeset
+ − 225
2296
+ − 226
fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses =
2476
+ − 227
let
+ − 228
val arg_names = Datatype_Prop.make_tnames arg_tys
+ − 229
val args = map Free (arg_names ~~ arg_tys)
+ − 230
val fv = lookup fv_map ty
+ − 231
val lhs = fv $ list_comb (constr, args)
+ − 232
val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses
+ − 233
val rhs = fold_union rhs_trms
+ − 234
in
+ − 235
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ − 236
end
2292
+ − 237
2296
+ − 238
fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses =
2476
+ − 239
let
+ − 240
val arg_names = Datatype_Prop.make_tnames arg_tys
+ − 241
val args = map Free (arg_names ~~ arg_tys)
+ − 242
val fv_bn = lookup fv_bn_map bn_trm
+ − 243
val lhs = fv_bn $ list_comb (constr, args)
+ − 244
val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
+ − 245
val rhs = fold_union rhs_trms
+ − 246
in
+ − 247
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ − 248
end
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>
parents:
diff
changeset
+ − 249
2292
+ − 250
fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) =
2476
+ − 251
let
+ − 252
val nth_constrs_info = nth constrs_info bn_n
+ − 253
val nth_bclausess = nth bclausesss bn_n
+ − 254
in
+ − 255
map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
+ − 256
end
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>
parents:
diff
changeset
+ − 257
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 258
fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms size_simps lthy =
2476
+ − 259
let
+ − 260
val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names
+ − 261
val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys
+ − 262
val fv_frees = map Free (fv_names ~~ fv_tys);
+ − 263
val fv_map = raw_tys ~~ fv_frees
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>
parents:
diff
changeset
+ − 264
2476
+ − 265
val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
+ − 266
val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
+ − 267
val fv_bn_names = map (prefix "fv_") bn_names
+ − 268
val fv_bn_arg_tys = map (nth raw_tys) bn_tys
+ − 269
val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys
+ − 270
val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys)
+ − 271
val fv_bn_map = bns ~~ fv_bn_frees
2292
+ − 272
2476
+ − 273
val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss
+ − 274
val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info
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>
parents:
diff
changeset
+ − 275
2476
+ − 276
val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
+ − 277
val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
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>
parents:
diff
changeset
+ − 278
2476
+ − 279
val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
+ − 280
Function_Common.default_config (pat_completeness_simp constr_thms) lthy
2569
94750b31a97d
fixed bug in fv function where a shallow binder binds lists of names
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 281
2630
+ − 282
val (info, lthy'') = prove_termination_fun size_simps (Local_Theory.restore lthy')
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 283
2888
eda5aeb056a6
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 284
val {fs, simps, inducts, ...} = info;
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>
parents:
diff
changeset
+ − 285
2476
+ − 286
val morphism = ProofContext.export_morphism lthy'' lthy
+ − 287
val simps_exp = map (Morphism.thm morphism) (the simps)
+ − 288
val inducts_exp = map (Morphism.thm morphism) (the inducts)
2888
eda5aeb056a6
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 289
2476
+ − 290
val (fvs', fv_bns') = chop (length fv_frees) fs
2888
eda5aeb056a6
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 291
eda5aeb056a6
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 292
(* grafting the types so that they coincide with the input into the function package *)
eda5aeb056a6
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 293
val fvs'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fvs' fv_tys
eda5aeb056a6
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 294
val fv_bns'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fv_bns' fv_bn_tys
2476
+ − 295
in
2888
eda5aeb056a6
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 296
(fvs'', fv_bns'', simps_exp, inducts_exp, lthy'')
2476
+ − 297
end
2305
+ − 298
+ − 299
2560
+ − 300
(** definition of raw permute_bn functions **)
+ − 301
+ − 302
fun mk_perm_bn_eq_rhs p perm_bn_map bn_args (i, arg) =
+ − 303
case AList.lookup (op=) bn_args i of
+ − 304
NONE => arg
+ − 305
| SOME (NONE) => mk_perm p arg
+ − 306
| SOME (SOME bn) => (lookup perm_bn_map bn) $ p $ arg
+ − 307
+ − 308
+ − 309
fun mk_perm_bn_eq lthy bn_trm perm_bn_map bn_args (constr, _, arg_tys, _) =
+ − 310
let
+ − 311
val p = Free ("p", @{typ perm})
+ − 312
val arg_names = Datatype_Prop.make_tnames arg_tys
+ − 313
val args = map Free (arg_names ~~ arg_tys)
+ − 314
val perm_bn = lookup perm_bn_map bn_trm
+ − 315
val lhs = perm_bn $ p $ list_comb (constr, args)
+ − 316
val rhs = list_comb (constr, map_index (mk_perm_bn_eq_rhs p perm_bn_map bn_args) args)
+ − 317
in
+ − 318
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ − 319
end
+ − 320
+ − 321
fun mk_perm_bn_eqs lthy perm_bn_map cns_info (bn_trm, bn_n, bn_argss) =
+ − 322
let
+ − 323
val nth_cns_info = nth cns_info bn_n
+ − 324
in
+ − 325
map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info
+ − 326
end
+ − 327
+ − 328
fun define_raw_bn_perms raw_tys bn_info cns_info cns_thms size_thms lthy =
+ − 329
if null bn_info
+ − 330
then ([], [], lthy)
+ − 331
else
+ − 332
let
+ − 333
val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
+ − 334
val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
+ − 335
val perm_bn_names = map (prefix "permute_") bn_names
+ − 336
val perm_bn_arg_tys = map (nth raw_tys) bn_tys
+ − 337
val perm_bn_tys = map (fn ty => @{typ "perm"} --> ty --> ty) perm_bn_arg_tys
+ − 338
val perm_bn_frees = map Free (perm_bn_names ~~ perm_bn_tys)
+ − 339
val perm_bn_map = bns ~~ perm_bn_frees
+ − 340
+ − 341
val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map cns_info) bn_info
+ − 342
+ − 343
val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names
+ − 344
val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs)
+ − 345
+ − 346
val prod_simps = @{thms prod.inject HOL.simp_thms}
+ − 347
+ − 348
val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
+ − 349
Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy
+ − 350
2630
+ − 351
val (info, lthy'') = prove_termination_fun size_thms (Local_Theory.restore lthy')
2560
+ − 352
+ − 353
val {fs, simps, ...} = info;
+ − 354
+ − 355
val morphism = ProofContext.export_morphism lthy'' lthy
+ − 356
val simps_exp = map (Morphism.thm morphism) (the simps)
+ − 357
in
+ − 358
(fs, simps_exp, lthy'')
+ − 359
end
+ − 360
+ − 361
2305
+ − 362
(** equivarance proofs **)
+ − 363
2311
+ − 364
val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}
+ − 365
+ − 366
fun subproof_tac const_names simps =
2388
+ − 367
SUBPROOF (fn {prems, context, ...} =>
2311
+ − 368
HEADGOAL
+ − 369
(simp_tac (HOL_basic_ss addsimps simps)
2765
7ac5e5c86c7d
introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 370
THEN' eqvt_tac context (eqvt_relaxed_config addexcls const_names)
2388
+ − 371
THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym]))))
2311
+ − 372
+ − 373
fun prove_eqvt_tac insts ind_thms const_names simps ctxt =
+ − 374
HEADGOAL
+ − 375
(Object_Logic.full_atomize_tac
+ − 376
THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms))
+ − 377
THEN_ALL_NEW subproof_tac const_names simps ctxt)
+ − 378
2305
+ − 379
fun mk_eqvt_goal pi const arg =
2476
+ − 380
let
+ − 381
val lhs = mk_perm pi (const $ arg)
+ − 382
val rhs = const $ (mk_perm pi arg)
+ − 383
in
+ − 384
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ − 385
end
2305
+ − 386
2598
+ − 387
2305
+ − 388
fun raw_prove_eqvt consts ind_thms simps ctxt =
2308
+ − 389
if null consts then []
+ − 390
else
+ − 391
let
+ − 392
val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+ − 393
val p = Free (p, @{typ perm})
+ − 394
val arg_tys =
+ − 395
consts
+ − 396
|> map fastype_of
+ − 397
|> map domain_type
2311
+ − 398
val (arg_names, ctxt'') =
+ − 399
Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt'
2308
+ − 400
val args = map Free (arg_names ~~ arg_tys)
+ − 401
val goals = map2 (mk_eqvt_goal p) consts args
+ − 402
val insts = map (single o SOME) arg_names
2311
+ − 403
val const_names = map (fst o dest_Const) consts
2308
+ − 404
in
2311
+ − 405
Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} =>
+ − 406
prove_eqvt_tac insts ind_thms const_names simps context)
2308
+ − 407
|> ProofContext.export ctxt'' ctxt
+ − 408
end
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>
parents:
diff
changeset
+ − 409
2598
+ − 410
+ − 411
+ − 412
(*** raw permutation functions ***)
+ − 413
+ − 414
(** proves the two pt-type class properties **)
+ − 415
+ − 416
fun prove_permute_zero induct perm_defs perm_fns lthy =
+ − 417
let
+ − 418
val perm_types = map (body_type o fastype_of) perm_fns
+ − 419
val perm_indnames = Datatype_Prop.make_tnames perm_types
+ − 420
+ − 421
fun single_goal ((perm_fn, T), x) =
+ − 422
HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))
+ − 423
+ − 424
val goals =
+ − 425
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ − 426
(map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
+ − 427
+ − 428
val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
+ − 429
+ − 430
val tac = (Datatype_Aux.indtac induct perm_indnames
+ − 431
THEN_ALL_NEW asm_simp_tac simps) 1
+ − 432
in
+ − 433
Goal.prove lthy perm_indnames [] goals (K tac)
+ − 434
|> Datatype_Aux.split_conj_thm
+ − 435
end
+ − 436
+ − 437
+ − 438
fun prove_permute_plus induct perm_defs perm_fns lthy =
+ − 439
let
+ − 440
val p = Free ("p", @{typ perm})
+ − 441
val q = Free ("q", @{typ perm})
+ − 442
val perm_types = map (body_type o fastype_of) perm_fns
+ − 443
val perm_indnames = Datatype_Prop.make_tnames perm_types
+ − 444
+ − 445
fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq
+ − 446
(perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
+ − 447
+ − 448
val goals =
+ − 449
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ − 450
(map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
+ − 451
+ − 452
val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
+ − 453
+ − 454
val tac = (Datatype_Aux.indtac induct perm_indnames
+ − 455
THEN_ALL_NEW asm_simp_tac simps) 1
+ − 456
in
+ − 457
Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
+ − 458
|> Datatype_Aux.split_conj_thm
+ − 459
end
+ − 460
+ − 461
+ − 462
fun mk_perm_eq ty_perm_assoc cnstr =
+ − 463
let
+ − 464
fun lookup_perm p (ty, arg) =
+ − 465
case (AList.lookup (op=) ty_perm_assoc ty) of
+ − 466
SOME perm => perm $ p $ arg
+ − 467
| NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg
+ − 468
+ − 469
val p = Free ("p", @{typ perm})
+ − 470
val (arg_tys, ty) =
+ − 471
fastype_of cnstr
+ − 472
|> strip_type
+ − 473
+ − 474
val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
+ − 475
val args = map Free (arg_names ~~ arg_tys)
+ − 476
+ − 477
val lhs = lookup_perm p (ty, list_comb (cnstr, args))
+ − 478
val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args))
+ − 479
+ − 480
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ − 481
in
+ − 482
(Attrib.empty_binding, eq)
+ − 483
end
+ − 484
+ − 485
+ − 486
fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy =
+ − 487
let
+ − 488
val perm_fn_names = full_ty_names
+ − 489
|> map Long_Name.base_name
+ − 490
|> map (prefix "permute_")
+ − 491
+ − 492
val perm_fn_types = map perm_ty tys
+ − 493
val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
+ − 494
val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names
+ − 495
+ − 496
val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs
+ − 497
+ − 498
fun tac _ (_, _, simps) =
+ − 499
Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
+ − 500
+ − 501
fun morphism phi (fvs, dfs, simps) =
+ − 502
(map (Morphism.term phi) fvs,
+ − 503
map (Morphism.thm phi) dfs,
+ − 504
map (Morphism.thm phi) simps);
+ − 505
+ − 506
val ((perm_funs, perm_eq_thms), lthy') =
+ − 507
lthy
+ − 508
|> Local_Theory.exit_global
+ − 509
|> Class.instantiation (full_ty_names, tvs, @{sort pt})
+ − 510
|> Primrec.add_primrec perm_fn_binds perm_eqs
+ − 511
+ − 512
val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'
+ − 513
val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy'
+ − 514
in
+ − 515
lthy'
+ − 516
|> Class.prove_instantiation_exit_result morphism tac
+ − 517
(perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
+ − 518
||> Named_Target.theory_init
+ − 519
end
+ − 520
+ − 521
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>
parents:
diff
changeset
+ − 522
end (* structure *)
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>
parents:
diff
changeset
+ − 523