2297
+ − 1
(* Title: nominal_dt_alpha.ML
+ − 2
Author: Cezary Kaliszyk
+ − 3
Author: Christian Urban
+ − 4
2313
+ − 5
Definitions and proofs for the alpha-relations.
2297
+ − 6
*)
+ − 7
+ − 8
signature NOMINAL_DT_ALPHA =
+ − 9
sig
2611
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 10
val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 11
2957
+ − 12
val define_raw_alpha: raw_dt_info -> bn_info list -> bclause list list list -> term list ->
+ − 13
Proof.context -> alpha_result * local_theory
2300
+ − 14
2480
ac7dff1194e8
introduced a general procedure for structural inductions; simplified reflexivity proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 15
val induct_prove: typ list -> (typ * (term -> term)) list -> thm ->
ac7dff1194e8
introduced a general procedure for structural inductions; simplified reflexivity proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 16
(Proof.context -> int -> tactic) -> Proof.context -> thm list
ac7dff1194e8
introduced a general procedure for structural inductions; simplified reflexivity proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 17
2389
+ − 18
val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm ->
+ − 19
(Proof.context -> int -> tactic) -> Proof.context -> thm list
+ − 20
2957
+ − 21
val raw_prove_alpha_distincts: Proof.context -> alpha_result -> raw_dt_info -> thm list
+ − 22
val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> raw_dt_info -> thm list
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23
val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24
val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 25
val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 26
val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list ->
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 27
thm list * thm list
2928
+ − 28
val raw_prove_bn_imp: Proof.context -> alpha_result -> thm list
+ − 29
val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list ->
+ − 30
thm list -> thm list
+ − 31
val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list
3161
aa1ba91ed1ff
Pass proper rsp theorems for constructors and for size
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 32
val raw_constrs_rsp: Proof.context -> alpha_result -> term list list -> thm list -> thm list list
2928
+ − 33
val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list
+ − 34
val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
2561
+ − 35
3226
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 36
val mk_funs_rsp: Proof.context -> thm -> thm
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 37
val mk_alpha_permute_rsp: Proof.context -> thm -> thm
2297
+ − 38
end
+ − 39
+ − 40
structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
+ − 41
struct
+ − 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
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
open Nominal_Dt_Data
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
+ − 45
2320
+ − 46
fun lookup xs x = the (AList.lookup (op=) xs x)
+ − 47
fun group xs = AList.group (op=) xs
+ − 48
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 49
2300
+ − 50
(** definition of the inductive rules for alpha and alpha_bn **)
+ − 51
2297
+ − 52
(* construct the compound terms for prod_fv and prod_alpha *)
+ − 53
fun mk_prod_fv (t1, t2) =
2476
+ − 54
let
+ − 55
val ty1 = fastype_of t1
+ − 56
val ty2 = fastype_of t2
+ − 57
val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"}
+ − 58
in
+ − 59
Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2
+ − 60
end
2297
+ − 61
+ − 62
fun mk_prod_alpha (t1, t2) =
2476
+ − 63
let
+ − 64
val ty1 = fastype_of t1
+ − 65
val ty2 = fastype_of t2
+ − 66
val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2)
+ − 67
val resT = [prodT, prodT] ---> @{typ "bool"}
+ − 68
in
+ − 69
Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2
+ − 70
end
2297
+ − 71
+ − 72
(* generates the compound binder terms *)
2611
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 73
fun comb_binders lthy bmode args binders =
2476
+ − 74
let
+ − 75
fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
+ − 76
| bind_set _ args (SOME bn, i) = bn $ (nth args i)
+ − 77
fun bind_lst lthy args (NONE, i) = listify lthy (nth args i)
+ − 78
| bind_lst _ args (SOME bn, i) = bn $ (nth args i)
2297
+ − 79
2476
+ − 80
val (combine_fn, bind_fn) =
+ − 81
case bmode of
+ − 82
Lst => (mk_append, bind_lst)
+ − 83
| Set => (mk_union, bind_set)
+ − 84
| Res => (mk_union, bind_set)
+ − 85
in
+ − 86
binders
+ − 87
|> map (bind_fn lthy args)
+ − 88
|> foldl1 combine_fn
+ − 89
end
2297
+ − 90
+ − 91
(* produces the term for an alpha with abstraction *)
+ − 92
fun mk_alpha_term bmode fv alpha args args' binders binders' =
2476
+ − 93
let
+ − 94
val (alpha_name, binder_ty) =
+ − 95
case bmode of
+ − 96
Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
+ − 97
| Set => (@{const_name "alpha_set"}, @{typ "atom set"})
+ − 98
| Res => (@{const_name "alpha_res"}, @{typ "atom set"})
+ − 99
val ty = fastype_of args
+ − 100
val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
+ − 101
val alpha_ty = [ty, ty] ---> @{typ "bool"}
+ − 102
val fv_ty = ty --> @{typ "atom set"}
+ − 103
val pair_lhs = HOLogic.mk_prod (binders, args)
+ − 104
val pair_rhs = HOLogic.mk_prod (binders', args')
+ − 105
in
+ − 106
HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},
+ − 107
Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool})
+ − 108
$ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs)
+ − 109
end
2297
+ − 110
+ − 111
(* for non-recursive binders we have to produce alpha_bn premises *)
+ − 112
fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder =
+ − 113
case binder of
+ − 114
(NONE, _) => []
+ − 115
| (SOME bn, i) =>
+ − 116
if member (op=) bodies i then []
2320
+ − 117
else [lookup alpha_bn_map bn $ nth args i $ nth args' i]
2297
+ − 118
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 119
(* generate the premises for an alpha rule; mk_frees is used
2297
+ − 120
if no binders are present *)
+ − 121
fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
2476
+ − 122
let
+ − 123
fun mk_frees i =
+ − 124
let
+ − 125
val arg = nth args i
+ − 126
val arg' = nth args' i
+ − 127
val ty = fastype_of arg
+ − 128
in
+ − 129
if nth is_rec i
+ − 130
then fst (lookup alpha_map ty) $ arg $ arg'
+ − 131
else HOLogic.mk_eq (arg, arg')
+ − 132
end
2297
+ − 133
2476
+ − 134
fun mk_alpha_fv i =
+ − 135
let
+ − 136
val ty = fastype_of (nth args i)
+ − 137
in
+ − 138
case AList.lookup (op=) alpha_map ty of
+ − 139
NONE => (HOLogic.eq_const ty, supp_const ty)
+ − 140
| SOME (alpha, fv) => (alpha, fv)
+ − 141
end
+ − 142
in
+ − 143
case bclause of
+ − 144
BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies
+ − 145
| BC (bmode, binders, bodies) =>
+ − 146
let
+ − 147
val (alphas, fvs) = split_list (map mk_alpha_fv bodies)
+ − 148
val comp_fv = foldl1 mk_prod_fv fvs
+ − 149
val comp_alpha = foldl1 mk_prod_alpha alphas
+ − 150
val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
+ − 151
val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
2611
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 152
val comp_binders = comb_binders lthy bmode args binders
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
val comp_binders' = comb_binders lthy bmode args' binders
2476
+ − 154
val alpha_prem =
+ − 155
mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'
+ − 156
val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)
+ − 157
in
+ − 158
map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)
+ − 159
end
+ − 160
end
2297
+ − 161
+ − 162
(* produces the introduction rule for an alpha rule *)
+ − 163
fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses =
2476
+ − 164
let
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 165
val arg_names = Old_Datatype_Prop.make_tnames arg_tys
2476
+ − 166
val arg_names' = Name.variant_list arg_names arg_names
+ − 167
val args = map Free (arg_names ~~ arg_tys)
+ − 168
val args' = map Free (arg_names' ~~ arg_tys)
+ − 169
val alpha = fst (lookup alpha_map ty)
+ − 170
val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))
+ − 171
val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses
+ − 172
in
+ − 173
Library.foldr Logic.mk_implies (flat prems, concl)
+ − 174
end
2297
+ − 175
+ − 176
(* produces the premise of an alpha-bn rule; we only need to
+ − 177
treat the case special where the binding clause is empty;
+ − 178
+ − 179
- if the body is not included in the bn_info, then we either
+ − 180
produce an equation or an alpha-premise
+ − 181
+ − 182
- if the body is included in the bn_info, then we create
+ − 183
either a recursive call to alpha-bn, or no premise *)
+ − 184
fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause =
+ − 185
let
2476
+ − 186
fun mk_alpha_bn_prem i =
+ − 187
let
+ − 188
val arg = nth args i
+ − 189
val arg' = nth args' i
+ − 190
val ty = fastype_of arg
+ − 191
in
+ − 192
case AList.lookup (op=) bn_args i of
+ − 193
NONE => (case (AList.lookup (op=) alpha_map ty) of
+ − 194
NONE => [HOLogic.mk_eq (arg, arg')]
+ − 195
| SOME (alpha, _) => [alpha $ arg $ arg'])
+ − 196
| SOME (NONE) => []
+ − 197
| SOME (SOME bn) => [lookup alpha_bn_map bn $ arg $ arg']
+ − 198
end
2297
+ − 199
in
2476
+ − 200
case bclause of
+ − 201
BC (_, [], bodies) =>
+ − 202
map HOLogic.mk_Trueprop (flat (map mk_alpha_bn_prem bodies))
+ − 203
| _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
+ − 204
end
2297
+ − 205
+ − 206
fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
2476
+ − 207
let
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 208
val arg_names = Old_Datatype_Prop.make_tnames arg_tys
2476
+ − 209
val arg_names' = Name.variant_list arg_names arg_names
+ − 210
val args = map Free (arg_names ~~ arg_tys)
+ − 211
val args' = map Free (arg_names' ~~ arg_tys)
+ − 212
val alpha_bn = lookup alpha_bn_map bn_trm
+ − 213
val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))
+ − 214
val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses
+ − 215
in
+ − 216
Library.foldr Logic.mk_implies (flat prems, concl)
+ − 217
end
2297
+ − 218
+ − 219
fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) =
2476
+ − 220
let
+ − 221
val nth_constrs_info = nth constrs_info bn_n
+ − 222
val nth_bclausess = nth bclausesss bn_n
+ − 223
in
+ − 224
map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
+ − 225
end
2297
+ − 226
2957
+ − 227
fun define_raw_alpha raw_dt_info bn_info bclausesss fvs lthy =
2476
+ − 228
let
2957
+ − 229
val RawDtInfo {raw_dt_names, raw_tys, raw_cns_info, ...} = raw_dt_info
+ − 230
+ − 231
val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_dt_names
2476
+ − 232
val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys
+ − 233
val alpha_frees = map Free (alpha_names ~~ alpha_tys)
+ − 234
val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs)
2297
+ − 235
2476
+ − 236
val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
+ − 237
val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
+ − 238
val alpha_bn_names = map (prefix "alpha_") bn_names
+ − 239
val alpha_bn_arg_tys = map (nth raw_tys) bn_tys
+ − 240
val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys
+ − 241
val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
+ − 242
val alpha_bn_map = bns ~~ alpha_bn_frees
2297
+ − 243
2957
+ − 244
val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) raw_cns_info bclausesss
+ − 245
val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map raw_cns_info bclausesss) bn_info
2297
+ − 246
2476
+ − 247
val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
+ − 248
(alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
3245
+ − 249
val all_alpha_intros = map (pair Binding.empty_atts) (flat alpha_intros @ flat alpha_bn_intros)
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 250
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 251
val (alpha_info, lthy') = lthy
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 252
|> Inductive.add_inductive_i
2476
+ − 253
{quiet_mode = true, verbose = false, alt_name = Binding.empty,
3200
+ − 254
coind = false, no_elim = false, no_ind = false, skip_mono = false}
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 255
all_alpha_names [] all_alpha_intros []
2297
+ − 256
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 257
val all_alpha_trms_loc = #preds alpha_info;
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 258
val alpha_raw_induct_loc = #raw_induct alpha_info;
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 259
val alpha_intros_loc = #intrs alpha_info;
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 260
val alpha_cases_loc = #elims alpha_info;
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 261
val phi =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 262
Proof_Context.export_morphism lthy'
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 263
(Proof_Context.transfer (Proof_Context.theory_of lthy') lthy);
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
+ − 264
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
+ − 265
val all_alpha_trms = all_alpha_trms_loc
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
+ − 266
|> map (Morphism.term phi)
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
+ − 267
|> map Type.legacy_freeze
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 268
val alpha_raw_induct = Morphism.thm phi alpha_raw_induct_loc
2476
+ − 269
val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
+ − 270
val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
2298
+ − 271
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
+ − 272
val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms
2928
+ − 273
+ − 274
val alpha_tys = map (domain_type o fastype_of) alpha_trms
+ − 275
val alpha_bn_tys = map (domain_type o fastype_of) alpha_bn_trms
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 276
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 277
val alpha_names = map (fst o dest_Const) alpha_trms
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 278
val alpha_bn_names = map (fst o dest_Const) alpha_bn_trms
2928
+ − 279
in
+ − 280
(AlphaResult
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 281
{alpha_names = alpha_names,
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 282
alpha_trms = alpha_trms,
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 283
alpha_tys = alpha_tys,
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 284
alpha_bn_names = alpha_bn_names,
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 285
alpha_bn_trms = alpha_bn_trms,
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 286
alpha_bn_tys = alpha_bn_tys,
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 287
alpha_intros = alpha_intros,
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 288
alpha_cases = alpha_cases,
3245
+ − 289
alpha_raw_induct = alpha_raw_induct}, Local_Theory.reset lthy') (* FIXME disrupts context *)
2476
+ − 290
end
2297
+ − 291
2300
+ − 292
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 293
(** induction proofs **)
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 294
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 295
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 296
(* proof by structural induction over data types *)
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 297
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 298
fun induct_prove tys props induct_thm cases_tac ctxt =
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 299
let
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 300
val (arg_names, ctxt') =
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 301
Variable.variant_fixes (replicate (length tys) "x") ctxt
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 302
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 303
val args = map2 (curry Free) arg_names tys
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 304
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 305
val true_trms = replicate (length tys) (K @{term True})
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 306
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 307
fun apply_all x fs = map (fn f => f x) fs
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 308
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 309
val goals =
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 310
group (props @ (tys ~~ true_trms))
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 311
|> map snd
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 312
|> map2 apply_all args
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 313
|> map fold_conj
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 314
|> foldr1 HOLogic.mk_conj
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 315
|> HOLogic.mk_Trueprop
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 316
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 317
fun tac ctxt =
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 318
HEADGOAL
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 319
(DETERM o (resolve_tac ctxt [induct_thm])
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 320
THEN_ALL_NEW
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 321
(REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt])))
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 322
in
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 323
Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
3045
d0ad264f8c4f
updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 324
|> singleton (Proof_Context.export ctxt' ctxt)
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 325
|> Old_Datatype_Aux.split_conj_thm
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 326
|> map Old_Datatype_Aux.split_conj_thm
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 327
|> flat
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 328
|> filter_out (is_true o Thm.concl_of)
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 329
|> map zero_var_indexes
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 330
end
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 331
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 332
(* proof by rule induction over the alpha-definitions *)
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 333
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 334
fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 335
let
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 336
val arg_tys = map (domain_type o fastype_of) alphas
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 337
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 338
val ((arg_names1, arg_names2), ctxt') =
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 339
ctxt
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 340
|> Variable.variant_fixes (replicate (length alphas) "x")
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 341
||>> Variable.variant_fixes (replicate (length alphas) "y")
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 342
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 343
val args1 = map2 (curry Free) arg_names1 arg_tys
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 344
val args2 = map2 (curry Free) arg_names2 arg_tys
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 345
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 346
val true_trms = replicate (length alphas) (K @{term True})
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 347
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 348
fun apply_all x fs = map (fn f => f x) fs
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 349
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 350
val goals_rhs =
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 351
group (props @ (alphas ~~ true_trms))
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 352
|> map snd
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 353
|> map2 apply_all (args1 ~~ args2)
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 354
|> map fold_conj
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 355
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 356
fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 357
val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 358
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 359
val goals =
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 360
(map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs)
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 361
|> foldr1 HOLogic.mk_conj
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 362
|> HOLogic.mk_Trueprop
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 363
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 364
fun tac ctxt =
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 365
HEADGOAL
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 366
(DETERM o (resolve_tac ctxt [alpha_induct_thm])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 367
THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms TrueI}, cases_tac ctxt])
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 368
in
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 369
Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
3045
d0ad264f8c4f
updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 370
|> singleton (Proof_Context.export ctxt' ctxt)
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 371
|> Old_Datatype_Aux.split_conj_thm
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 372
|> map (fn th => th RS mp)
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 373
|> map Old_Datatype_Aux.split_conj_thm
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 374
|> flat
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 375
|> filter_out (is_true o Thm.concl_of)
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 376
|> map zero_var_indexes
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 377
end
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 378
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 379
2316
+ − 380
2300
+ − 381
(** produces the distinctness theorems **)
+ − 382
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 383
2300
+ − 384
(* transforms the distinctness theorems of the constructors
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
+ − 385
into "not-alphas" of the constructors *)
2399
+ − 386
fun mk_distinct_goal ty_trm_assoc neq =
2476
+ − 387
let
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
+ − 388
val (Const (@{const_name "HOL.eq"}, ty_eq) $ lhs $ rhs) =
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
+ − 389
HOLogic.dest_not (HOLogic.dest_Trueprop neq)
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
+ − 390
val ty_str = fst (dest_Type (domain_type ty_eq))
2476
+ − 391
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
+ − 392
Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs
2476
+ − 393
|> HOLogic.mk_not
+ − 394
|> HOLogic.mk_Trueprop
+ − 395
end
2300
+ − 396
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 397
fun distinct_tac ctxt cases_thms distinct_thms =
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 398
resolve_tac ctxt [notI] THEN' eresolve_tac ctxt cases_thms
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 399
THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms)
2300
+ − 400
2957
+ − 401
fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info =
2476
+ − 402
let
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 403
val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result
2957
+ − 404
val RawDtInfo {raw_dt_names, raw_distinct_thms, ...} = raw_dt_info
2300
+ − 405
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 406
val ty_trm_assoc = raw_dt_names ~~ alpha_names
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 407
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 408
fun mk_alpha_distinct raw_distinct_trm =
2476
+ − 409
let
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 410
val goal = mk_distinct_goal ty_trm_assoc raw_distinct_trm
2476
+ − 411
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
+ − 412
Goal.prove ctxt [] [] goal
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 413
(K (distinct_tac ctxt alpha_cases raw_distinct_thms 1))
2476
+ − 414
end
2399
+ − 415
in
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 416
map (mk_alpha_distinct o Thm.prop_of) raw_distinct_thms
2399
+ − 417
end
2300
+ − 418
+ − 419
2316
+ − 420
2300
+ − 421
(** produces the alpha_eq_iff simplification rules **)
+ − 422
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
+ − 423
(* in case a theorem is of the form (Rel Const Const), it will be
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
+ − 424
rewritten to ((Rel Const = Const) = True)
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
+ − 425
*)
2300
+ − 426
fun mk_simp_rule thm =
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 427
case Thm.prop_of thm of
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
+ − 428
@{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI}
2300
+ − 429
| _ => thm
+ − 430
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 431
fun alpha_eq_iff_tac ctxt dist_inj intros elims =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 432
SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE'
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 433
(resolve_tac ctxt @{thms iffI} THEN'
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 434
RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj),
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 435
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)])
2300
+ − 436
+ − 437
fun mk_alpha_eq_iff_goal thm =
+ − 438
let
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 439
val prop = Thm.prop_of thm;
2300
+ − 440
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
+ − 441
val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
+ − 442
fun list_conj l = foldr1 HOLogic.mk_conj l;
+ − 443
in
+ − 444
if hyps = [] then HOLogic.mk_Trueprop concl
+ − 445
else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))
+ − 446
end;
+ − 447
2957
+ − 448
fun raw_prove_alpha_eq_iff ctxt alpha_result raw_dt_info =
2476
+ − 449
let
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 450
val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result
2957
+ − 451
val RawDtInfo {raw_distinct_thms, raw_inject_thms, ...} = raw_dt_info
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 452
2476
+ − 453
val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;
+ − 454
val goals = map mk_alpha_eq_iff_goal thms_imp;
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 455
val tac = alpha_eq_iff_tac ctxt (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1;
2476
+ − 456
val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;
+ − 457
in
+ − 458
Variable.export ctxt' ctxt thms
+ − 459
|> map mk_simp_rule
+ − 460
end
2300
+ − 461
2311
+ − 462
2316
+ − 463
(** reflexivity proof for the alphas **)
+ − 464
+ − 465
val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}
+ − 466
2480
ac7dff1194e8
introduced a general procedure for structural inductions; simplified reflexivity proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 467
fun cases_tac intros ctxt =
2476
+ − 468
let
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 469
val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv}
2316
+ − 470
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 471
val unbound_tac = REPEAT o (eresolve_tac ctxt @{thms conjE}) THEN' assume_tac ctxt
2316
+ − 472
2476
+ − 473
val bound_tac =
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 474
EVERY' [ resolve_tac ctxt [exi_zero],
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 475
resolve_tac ctxt @{thms alpha_refl},
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 476
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]
2476
+ − 477
in
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 478
resolve_tac ctxt intros THEN_ALL_NEW
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 479
FIRST' [resolve_tac ctxt @{thms refl}, unbound_tac, bound_tac]
2476
+ − 480
end
2316
+ − 481
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 482
fun raw_prove_refl ctxt alpha_result raw_dt_induct =
2476
+ − 483
let
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 484
val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_intros, ...} =
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 485
alpha_result
2480
ac7dff1194e8
introduced a general procedure for structural inductions; simplified reflexivity proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 486
ac7dff1194e8
introduced a general procedure for structural inductions; simplified reflexivity proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 487
val props =
ac7dff1194e8
introduced a general procedure for structural inductions; simplified reflexivity proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 488
map (fn (ty, c) => (ty, fn x => c $ x $ x))
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 489
((alpha_tys ~~ alpha_trms) @ (alpha_bn_tys ~~ alpha_bn_trms))
2476
+ − 490
in
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 491
induct_prove alpha_tys props raw_dt_induct (cases_tac alpha_intros) ctxt
2476
+ − 492
end
2316
+ − 493
+ − 494
+ − 495
2311
+ − 496
(** symmetry proof for the alphas **)
+ − 497
+ − 498
val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p"
+ − 499
by (erule exE, rule_tac x="-p" in exI, auto)}
+ − 500
+ − 501
(* for premises that contain binders *)
2868
+ − 502
fun prem_bound_tac pred_names alpha_eqvt ctxt =
2476
+ − 503
let
+ − 504
fun trans_prem_tac pred_names ctxt =
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 505
SUBPROOF (fn {prems, context = ctxt', ...} =>
2476
+ − 506
let
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 507
val prems' = map (transform_prem1 ctxt' pred_names) prems
2476
+ − 508
in
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 509
resolve_tac ctxt' prems' 1
2476
+ − 510
end) ctxt
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 511
val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas}
2476
+ − 512
in
+ − 513
EVERY'
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 514
[ eresolve_tac ctxt [exi_neg],
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 515
resolve_tac ctxt @{thms alpha_sym_eqvt},
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 516
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps),
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 517
eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN'
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 518
resolve_tac ctxt @{thms refl},
2868
+ − 519
trans_prem_tac pred_names ctxt]
2476
+ − 520
end
2311
+ − 521
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 522
fun raw_prove_sym ctxt alpha_result alpha_eqvt =
2476
+ − 523
let
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 524
val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms,
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 525
alpha_intros, alpha_raw_induct, ...} = alpha_result
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 526
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 527
val alpha_trms = alpha_trms @ alpha_bn_trms
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 528
val alpha_names = alpha_names @ alpha_bn_names
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 529
2476
+ − 530
val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms
2868
+ − 531
2476
+ − 532
fun tac ctxt =
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 533
resolve_tac ctxt alpha_intros THEN_ALL_NEW
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 534
FIRST' [assume_tac ctxt,
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 535
resolve_tac ctxt @{thms sym} THEN' assume_tac ctxt,
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 536
prem_bound_tac alpha_names alpha_eqvt ctxt]
2476
+ − 537
in
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 538
alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt
2389
+ − 539
end
2311
+ − 540
+ − 541
+ − 542
(** transitivity proof for alphas **)
+ − 543
2314
+ − 544
(* applies cases rules and resolves them with the last premise *)
2313
+ − 545
fun ecases_tac cases =
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 546
Subgoal.FOCUS (fn {context = ctxt, prems, ...} =>
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 547
HEADGOAL (resolve_tac ctxt cases THEN' resolve_tac ctxt [List.last prems]))
2313
+ − 548
+ − 549
fun aatac pred_names =
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 550
SUBPROOF (fn {context = ctxt, prems, ...} =>
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 551
HEADGOAL (resolve_tac ctxt (map (transform_prem1 ctxt pred_names) prems)))
2313
+ − 552
2314
+ − 553
(* instantiates exI with the permutation p + q *)
2313
+ − 554
val perm_inst_tac =
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 555
Subgoal.FOCUS (fn {context = ctxt, params, ...} =>
2313
+ − 556
let
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 557
val (p, q) = apply2 snd (last2 params)
3123
+ − 558
val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q]
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 559
val exi_inst = Thm.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
2313
+ − 560
in
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 561
HEADGOAL (resolve_tac ctxt [exi_inst])
2313
+ − 562
end)
+ − 563
2868
+ − 564
fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt =
2476
+ − 565
let
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 566
val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_conv}
2476
+ − 567
in
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 568
resolve_tac ctxt intros
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 569
THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN'
2476
+ − 570
TRY o EVERY' (* if binders are present *)
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 571
[ eresolve_tac ctxt @{thms exE},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 572
eresolve_tac ctxt @{thms exE},
2476
+ − 573
perm_inst_tac ctxt,
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 574
resolve_tac ctxt @{thms alpha_trans_eqvt},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 575
assume_tac ctxt,
2476
+ − 576
aatac pred_names ctxt,
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 577
eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN'
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 578
resolve_tac ctxt @{thms refl},
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 579
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ])
2476
+ − 580
end
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 581
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 582
fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt =
2476
+ − 583
let
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 584
val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 585
val alpha_names = alpha_names @ alpha_bn_names
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 586
2476
+ − 587
fun all_cases ctxt =
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 588
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms)
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 589
THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt
2476
+ − 590
in
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 591
EVERY' [ resolve_tac ctxt @{thms allI},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 592
resolve_tac ctxt @{thms impI},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 593
ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ]
2476
+ − 594
end
2311
+ − 595
2389
+ − 596
fun prep_trans_goal alpha_trm (arg1, arg2) =
2476
+ − 597
let
+ − 598
val arg_ty = fastype_of arg1
+ − 599
val mid = alpha_trm $ arg2 $ (Bound 0)
+ − 600
val rhs = alpha_trm $ arg1 $ (Bound 0)
+ − 601
in
+ − 602
HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs))
+ − 603
end
2311
+ − 604
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 605
fun raw_prove_trans ctxt alpha_result raw_dt_thms alpha_eqvt =
2476
+ − 606
let
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 607
val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms,
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 608
alpha_raw_induct, ...} = alpha_result
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 609
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 610
val alpha_trms = alpha_trms @ alpha_bn_trms
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 611
2476
+ − 612
val props = map prep_trans_goal alpha_trms
+ − 613
in
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 614
alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 615
(prove_trans_tac alpha_result raw_dt_thms alpha_eqvt) ctxt
2476
+ − 616
end
2311
+ − 617
2390
+ − 618
+ − 619
(** proves the equivp predicate for all alphas **)
2322
+ − 620
2592
+ − 621
val reflp_def' =
+ − 622
@{lemma "reflp R == !x. R x x" by (simp add: reflp_def refl_on_def)}
+ − 623
+ − 624
val symp_def' =
+ − 625
@{lemma "symp R == !x y . R x y --> R y x" by (simp add: symp_def sym_def)}
+ − 626
2397
+ − 627
val transp_def' =
+ − 628
@{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)"
2592
+ − 629
by (rule eq_reflection, auto simp add: trans_def transp_def)}
2322
+ − 630
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 631
fun raw_prove_equivp ctxt alpha_result refl symm trans =
2476
+ − 632
let
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 633
val AlphaResult {alpha_trms, alpha_bn_trms, ...} = alpha_result
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 634
3226
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 635
val refl' = map (fold_rule ctxt [reflp_def'] o atomize ctxt) refl
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 636
val symm' = map (fold_rule ctxt [symp_def'] o atomize ctxt) symm
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 637
val trans' = map (fold_rule ctxt [transp_def'] o atomize ctxt) trans
2397
+ − 638
2476
+ − 639
fun prep_goal t =
+ − 640
HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t)
+ − 641
in
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 642
Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms))
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 643
(K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (resolve_tac ctxt @{thms equivpI} THEN'
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 644
RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans']))))
2927
116f9ba4f59f
combined distributed data for alpha in alpha_result (partially done)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 645
|> chop (length alpha_trms)
2476
+ − 646
end
2322
+ − 647
2320
+ − 648
+ − 649
(* proves that alpha_raw implies alpha_bn *)
+ − 650
2928
+ − 651
fun raw_prove_bn_imp_tac alpha_result ctxt =
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 652
SUBPROOF (fn {prems, context = ctxt', ...} =>
2320
+ − 653
let
2928
+ − 654
val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result
+ − 655
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 656
val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 657
val prems'' = map (transform_prem1 ctxt' alpha_names) prems'
2320
+ − 658
in
2322
+ − 659
HEADGOAL
+ − 660
(REPEAT_ALL_NEW
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 661
(FIRST' [ resolve_tac ctxt' @{thms TrueI},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 662
resolve_tac ctxt' @{thms conjI},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 663
resolve_tac ctxt' prems',
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 664
resolve_tac ctxt' prems'',
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 665
resolve_tac ctxt' alpha_intros ]))
2320
+ − 666
end) ctxt
+ − 667
2928
+ − 668
+ − 669
fun raw_prove_bn_imp ctxt alpha_result =
2476
+ − 670
let
2928
+ − 671
val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result
+ − 672
2476
+ − 673
val arg_ty = domain_type o fastype_of
2928
+ − 674
val ty_assoc = alpha_tys ~~ alpha_trms
2476
+ − 675
val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms
+ − 676
in
2928
+ − 677
alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct
+ − 678
(raw_prove_bn_imp_tac alpha_result) ctxt
2476
+ − 679
end
2320
+ − 680
2387
+ − 681
2393
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 682
(* respectfulness for fv_raw / bn_raw *)
2387
+ − 683
2928
+ − 684
fun raw_fv_bn_rsp_aux ctxt alpha_result fvs bns fv_bns simps =
2476
+ − 685
let
2928
+ − 686
val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result
+ − 687
+ − 688
val arg_ty = domain_type o fastype_of
+ − 689
val ty_assoc = alpha_tys ~~ alpha_trms
2476
+ − 690
fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y)
2387
+ − 691
2476
+ − 692
val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs
+ − 693
val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns)
+ − 694
val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns
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
+ − 695
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 696
val simpset =
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 697
put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set_simps append.simps}
2476
+ − 698
@ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left})
+ − 699
in
2928
+ − 700
alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 701
(K (asm_full_simp_tac simpset)) ctxt
2476
+ − 702
end
2387
+ − 703
2395
+ − 704
2393
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 705
(* respectfulness for size *)
2392
+ − 706
2928
+ − 707
fun raw_size_rsp_aux ctxt alpha_result simps =
2476
+ − 708
let
2928
+ − 709
val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} =
+ − 710
alpha_result
+ − 711
2476
+ − 712
fun mk_prop ty (x, y) = HOLogic.mk_eq
+ − 713
(HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)
2392
+ − 714
2928
+ − 715
val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys))
2392
+ − 716
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 717
val simpset =
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 718
put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_conv
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 719
permute_prod_def prod.case prod.rec})
2392
+ − 720
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 721
val tac = (TRY o REPEAT o eresolve_tac ctxt @{thms exE}) THEN' asm_full_simp_tac simpset
2476
+ − 722
in
2928
+ − 723
alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt
2476
+ − 724
end
2392
+ − 725
2393
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 726
2395
+ − 727
(* respectfulness for constructors *)
+ − 728
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 729
fun raw_constr_rsp_tac ctxt alpha_intros simps =
2476
+ − 730
let
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 731
val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms rel_fun_def}
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 732
val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_conv
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 733
prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps
2476
+ − 734
in
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 735
asm_full_simp_tac pre_simpset
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 736
THEN' REPEAT o (resolve_tac ctxt @{thms allI impI})
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 737
THEN' resolve_tac ctxt alpha_intros
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 738
THEN_ALL_NEW (TRY o (resolve_tac ctxt [exi_zero]) THEN' asm_full_simp_tac post_simpset)
2476
+ − 739
end
2395
+ − 740
2928
+ − 741
fun raw_constrs_rsp ctxt alpha_result constrs simps =
2476
+ − 742
let
2928
+ − 743
val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result
+ − 744
2476
+ − 745
fun lookup ty =
2928
+ − 746
case AList.lookup (op=) (alpha_tys ~~ alpha_trms) ty of
2476
+ − 747
NONE => HOLogic.eq_const ty
+ − 748
| SOME alpha => alpha
2395
+ − 749
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 750
fun rel_fun_app (t1, t2) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 751
Const (@{const_name "rel_fun"}, dummyT) $ t1 $ t2
2395
+ − 752
2476
+ − 753
fun prep_goal trm =
+ − 754
trm
+ − 755
|> strip_type o fastype_of
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
+ − 756
|> (fn (tys, ty) => tys @ [ty])
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
+ − 757
|> map lookup
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 758
|> foldr1 rel_fun_app
2476
+ − 759
|> (fn t => t $ trm $ trm)
+ − 760
|> Syntax.check_term ctxt
+ − 761
|> HOLogic.mk_Trueprop
+ − 762
in
3161
aa1ba91ed1ff
Pass proper rsp theorems for constructors and for size
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 763
map (fn constrs =>
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 764
Goal.prove_common ctxt NONE [] [] (map prep_goal constrs)
2476
+ − 765
(K (HEADGOAL
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 766
(Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac ctxt alpha_intros simps)))) constrs
2476
+ − 767
end
2395
+ − 768
+ − 769
2404
+ − 770
(* rsp lemmas for alpha_bn relations *)
+ − 771
+ − 772
val rsp_equivp =
+ − 773
@{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q"
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 774
by (simp only: rel_fun_def equivp_def, metis)}
2404
+ − 775
2440
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 776
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 777
(* we have to reorder the alpha_bn_imps theorems in order
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 778
to be in order with alpha_bn_trms *)
2928
+ − 779
fun raw_alpha_bn_rsp alpha_result alpha_bn_equivp alpha_bn_imps =
2476
+ − 780
let
2928
+ − 781
val AlphaResult {alpha_bn_trms, ...} = alpha_result
+ − 782
2476
+ − 783
fun mk_map thm =
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 784
thm |> `Thm.prop_of
2476
+ − 785
|>> List.last o snd o strip_comb
+ − 786
|>> HOLogic.dest_Trueprop
+ − 787
|>> head_of
+ − 788
|>> fst o dest_Const
2440
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 789
2476
+ − 790
val alpha_bn_imps' =
+ − 791
map (lookup (map mk_map alpha_bn_imps) o fst o dest_Const) alpha_bn_trms
2440
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 792
2476
+ − 793
fun mk_thm thm1 thm2 =
+ − 794
(forall_intr_vars thm2) COMP (thm1 RS rsp_equivp)
+ − 795
in
+ − 796
map2 mk_thm alpha_bn_equivp alpha_bn_imps'
+ − 797
end
2404
+ − 798
+ − 799
2561
+ − 800
(* rsp for permute_bn functions *)
+ − 801
+ − 802
val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f"
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 803
by (simp add: rel_fun_def)}
2561
+ − 804
2928
+ − 805
fun raw_prove_perm_bn_tac alpha_result simps ctxt =
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 806
SUBPROOF (fn {prems, context = ctxt', ...} =>
2561
+ − 807
let
2928
+ − 808
val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result
3239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 809
val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 810
val prems'' = map (transform_prem1 ctxt' (alpha_names @ alpha_bn_names)) prems'
2561
+ − 811
in
+ − 812
HEADGOAL
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 813
(simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ prems'))
2561
+ − 814
THEN' TRY o REPEAT_ALL_NEW
3244
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 815
(FIRST' [ resolve_tac ctxt' @{thms TrueI},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 816
resolve_tac ctxt' @{thms conjI},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 817
resolve_tac ctxt' @{thms refl},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 818
resolve_tac ctxt' prems',
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 819
resolve_tac ctxt' prems'',
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 820
resolve_tac ctxt' alpha_intros ]))
2561
+ − 821
end) ctxt
+ − 822
2928
+ − 823
fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps =
2561
+ − 824
let
2928
+ − 825
val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} =
+ − 826
alpha_result
+ − 827
2561
+ − 828
val perm_bn_ty = range_type o range_type o fastype_of
2928
+ − 829
val ty_assoc = (alpha_tys @ alpha_bn_tys) ~~ (alpha_trms @ alpha_bn_trms)
2561
+ − 830
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 831
val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
2561
+ − 832
val p = Free (p, @{typ perm})
+ − 833
+ − 834
fun mk_prop t =
+ − 835
let
+ − 836
val alpha_trm = lookup ty_assoc (perm_bn_ty t)
+ − 837
in
+ − 838
(alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y))
+ − 839
end
+ − 840
2928
+ − 841
val goals = map mk_prop perm_bns
2561
+ − 842
in
2928
+ − 843
alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct
+ − 844
(raw_prove_perm_bn_tac alpha_result simps) ctxt
3045
d0ad264f8c4f
updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 845
|> Proof_Context.export ctxt' ctxt
3226
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 846
|> map (atomize ctxt)
2561
+ − 847
|> map single
+ − 848
|> map (curry (op OF) perm_bn_rsp)
+ − 849
end
+ − 850
+ − 851
+ − 852
2399
+ − 853
(* transformation of the natural rsp-lemmas into standard form *)
2397
+ − 854
+ − 855
val fun_rsp = @{lemma
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 856
"(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: rel_fun_def)}
2397
+ − 857
3226
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 858
fun mk_funs_rsp ctxt thm =
2476
+ − 859
thm
3226
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 860
|> atomize ctxt
2476
+ − 861
|> single
+ − 862
|> curry (op OF) fun_rsp
2393
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 863
2397
+ − 864
+ − 865
val permute_rsp = @{lemma
+ − 866
"(!x y p. R x y --> R (permute p x) (permute p y))
3229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 867
==> ((op =) ===> R ===> R) permute permute" by (simp add: rel_fun_def)}
2397
+ − 868
3226
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 869
fun mk_alpha_permute_rsp ctxt thm =
2476
+ − 870
thm
3226
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 871
|> atomize ctxt
2476
+ − 872
|> single
+ − 873
|> curry (op OF) permute_rsp
2397
+ − 874
2393
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 875
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 876
2404
+ − 877
2297
+ − 878
end (* structure *)
+ − 879