2337
+ − 1
(* Title: nominal_dt_alpha.ML
+ − 2
Author: Christian Urban
+ − 3
Author: Cezary Kaliszyk
+ − 4
2595
+ − 5
Performing quotient constructions, lifting theorems and
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 6
deriving support properties for the quotient types.
2337
+ − 7
*)
+ − 8
+ − 9
signature NOMINAL_DT_QUOT =
+ − 10
sig
2400
+ − 11
val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list ->
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
+ − 12
thm list -> local_theory -> Quotient_Info.quotients list * local_theory
2337
+ − 13
3157
de89c95c5377
updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 14
val define_qconsts: typ list -> (string * term * mixfix * thm) list -> local_theory ->
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
+ − 15
Quotient_Info.quotconsts list * local_theory
2346
+ − 16
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 17
val define_qperms: typ list -> string list -> (string * sort) list ->
3157
de89c95c5377
updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 18
(string * term * mixfix * thm) list -> thm list -> local_theory -> local_theory
2400
+ − 19
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 20
val define_qsizes: typ list -> string list -> (string * sort) list ->
3157
de89c95c5377
updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 21
(string * term * mixfix * thm) list -> local_theory -> local_theory
2426
+ − 22
2434
+ − 23
val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context
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
+ − 24
2595
+ − 25
val prove_supports: Proof.context -> thm list -> term list -> thm list
+ − 26
val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list
+ − 27
+ − 28
val fs_instance: typ list -> string list -> (string * sort) list -> thm list ->
+ − 29
local_theory -> local_theory
+ − 30
+ − 31
val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list ->
+ − 32
thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list
+ − 33
+ − 34
val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list
+ − 35
+ − 36
val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
+ − 37
thm list -> Proof.context -> thm list
2598
+ − 38
+ − 39
val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
+ − 40
thm list -> Proof.context -> thm list
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 41
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 42
val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list ->
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 43
thm list -> thm list -> thm list -> thm list -> thm list
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
2630
+ − 45
val prove_strong_induct: Proof.context -> thm -> thm list -> thm list -> bclause list list list ->
+ − 46
thm list
2337
+ − 47
end
+ − 48
+ − 49
structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
+ − 50
struct
+ − 51
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
+ − 52
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
+ − 53
2629
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 54
fun lookup xs x = the (AList.lookup (op=) xs x)
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
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
+ − 56
2337
+ − 57
(* defines the quotient types *)
2400
+ − 58
fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
2476
+ − 59
let
+ − 60
val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
3210
024d07886de8
updated to quotient package changes (by Kuncar)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 61
val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, false, NONE))) qtys_descr qty_args1
3056
756f48abb40a
updated to changes in the quotient package (patch by Ondrej Kuncar)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 62
val qty_args3 = qty_args2 ~~ alpha_equivp_thms
2476
+ − 63
in
3056
756f48abb40a
updated to changes in the quotient package (patch by Ondrej Kuncar)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 64
fold_map Quotient_Type.add_quotient_type qty_args3 lthy
2476
+ − 65
end
2337
+ − 66
3158
+ − 67
(* a wrapper for lifting a raw constant *)
+ − 68
fun lift_raw_const qtys (qconst_name, rconst, mx', rsp_thm) lthy =
+ − 69
let
+ − 70
val rty = fastype_of rconst
+ − 71
val qty = Quotient_Term.derive_qtyp lthy qtys rty
+ − 72
val lhs_raw = Free (qconst_name, qty)
+ − 73
val rhs_raw = rconst
+ − 74
+ − 75
val raw_var = (Binding.name qconst_name, NONE, mx')
+ − 76
val ([(binding, _, mx)], ctxt) = Proof_Context.cert_vars [raw_var] lthy
+ − 77
val lhs = Syntax.check_term ctxt lhs_raw
+ − 78
val rhs = Syntax.check_term ctxt rhs_raw
+ − 79
+ − 80
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
+ − 81
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+ − 82
val _ = if is_Const rhs then () else warning "The definiens is not a constant"
+ − 83
+ − 84
in
+ − 85
Quotient_Def.add_quotient_def (((binding, mx), Attrib.empty_binding), (lhs, rhs)) rsp_thm ctxt
+ − 86
end
+ − 87
2338
+ − 88
2337
+ − 89
(* defines quotient constants *)
2400
+ − 90
fun define_qconsts qtys consts_specs lthy =
2476
+ − 91
let
+ − 92
val (qconst_infos, lthy') =
3158
+ − 93
fold_map (lift_raw_const qtys) consts_specs lthy
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
+ − 94
val phi = Proof_Context.export_morphism lthy' lthy
2476
+ − 95
in
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
+ − 96
(map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy')
2476
+ − 97
end
2337
+ − 98
+ − 99
2400
+ − 100
(* defines the quotient permutations and proves pt-class *)
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 101
fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy =
2476
+ − 102
let
+ − 103
val lthy1 =
+ − 104
lthy
+ − 105
|> Local_Theory.exit_global
+ − 106
|> Class.instantiation (qfull_ty_names, tvs, @{sort pt})
2398
+ − 107
3161
aa1ba91ed1ff
Pass proper rsp theorems for constructors and for size
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 108
val (_, lthy2) = define_qconsts qtys perm_specs lthy1
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 109
3046
9b0324e1293b
all examples work again after quotient package has been "de-localised"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 110
val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2
2398
+ − 111
2476
+ − 112
val lifted_perm_laws =
+ − 113
map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
+ − 114
|> Variable.exportT lthy3 lthy2
2398
+ − 115
2476
+ − 116
fun tac _ =
+ − 117
Class.intro_classes_tac [] THEN
+ − 118
(ALLGOALS (resolve_tac lifted_perm_laws))
+ − 119
in
+ − 120
lthy2
+ − 121
|> Class.prove_instantiation_exit tac
+ − 122
|> Named_Target.theory_init
+ − 123
end
2346
+ − 124
2337
+ − 125
2400
+ − 126
(* defines the size functions and proves size-class *)
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 127
fun define_qsizes qtys qfull_ty_names tvs size_specs lthy =
2476
+ − 128
let
+ − 129
val tac = K (Class.intro_classes_tac [])
+ − 130
in
+ − 131
lthy
+ − 132
|> Local_Theory.exit_global
+ − 133
|> Class.instantiation (qfull_ty_names, tvs, @{sort size})
+ − 134
|> snd o (define_qconsts qtys size_specs)
+ − 135
|> Class.prove_instantiation_exit tac
+ − 136
|> Named_Target.theory_init
+ − 137
end
2400
+ − 138
2426
+ − 139
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
+ − 140
(* lifts a theorem and cleans all "_raw" parts
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 141
from variable names *)
2426
+ − 142
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 143
local
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 144
val any = Scan.one (Symbol.not_eof)
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 145
val raw = Scan.this_string "_raw"
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 146
val exclude =
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 147
Scan.repeat (Scan.unless raw any) --| raw >> implode
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 148
val parser = Scan.repeat (exclude || any)
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 149
in
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 150
fun unraw_str s =
2574
+ − 151
s |> raw_explode
2476
+ − 152
|> Scan.finite Symbol.stopper parser >> implode
+ − 153
|> fst
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 154
end
2426
+ − 155
+ − 156
fun unraw_vars_thm thm =
2476
+ − 157
let
+ − 158
fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
2426
+ − 159
2476
+ − 160
val vars = Term.add_vars (prop_of thm) []
+ − 161
val vars' = map (Var o unraw_var_str) vars
+ − 162
in
+ − 163
Thm.certify_instantiate ([], (vars ~~ vars')) thm
+ − 164
end
2426
+ − 165
+ − 166
fun unraw_bounds_thm th =
2476
+ − 167
let
+ − 168
val trm = Thm.prop_of th
+ − 169
val trm' = Term.map_abs_vars unraw_str trm
+ − 170
in
+ − 171
Thm.rename_boundvars trm trm' th
+ − 172
end
2426
+ − 173
2434
+ − 174
fun lift_thms qtys simps thms ctxt =
+ − 175
(map (Quotient_Tacs.lifted ctxt qtys simps
+ − 176
#> unraw_bounds_thm
+ − 177
#> unraw_vars_thm
+ − 178
#> Drule.zero_var_indexes) thms, ctxt)
+ − 179
2595
+ − 180
+ − 181
+ − 182
fun mk_supports_goal ctxt qtrm =
+ − 183
let
+ − 184
val vs = fresh_args ctxt qtrm
+ − 185
val rhs = list_comb (qtrm, vs)
+ − 186
val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"}
+ − 187
|> mk_supp
+ − 188
in
+ − 189
mk_supports lhs rhs
+ − 190
|> HOLogic.mk_Trueprop
+ − 191
end
+ − 192
+ − 193
fun supports_tac ctxt perm_simps =
+ − 194
let
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 195
val simpset1 =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 196
put_simpset HOL_basic_ss ctxt addsimps @{thms supports_def fresh_def[symmetric]}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 197
val simpset2 =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 198
put_simpset HOL_ss ctxt addsimps @{thms swap_fresh_fresh fresh_Pair}
2595
+ − 199
in
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 200
EVERY' [ simp_tac simpset1,
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
+ − 201
eqvt_tac ctxt (eqvt_strict_config addpres perm_simps),
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 202
simp_tac simpset2 ]
2595
+ − 203
end
+ − 204
+ − 205
fun prove_supports_single ctxt perm_simps qtrm =
+ − 206
let
+ − 207
val goal = mk_supports_goal ctxt qtrm
+ − 208
val ctxt' = Variable.auto_fixes goal ctxt
+ − 209
in
+ − 210
Goal.prove ctxt' [] [] goal
+ − 211
(K (HEADGOAL (supports_tac ctxt perm_simps)))
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
+ − 212
|> singleton (Proof_Context.export ctxt' ctxt)
2595
+ − 213
end
+ − 214
+ − 215
fun prove_supports ctxt perm_simps qtrms =
+ − 216
map (prove_supports_single ctxt perm_simps) qtrms
+ − 217
+ − 218
+ − 219
(* finite supp lemmas for qtypes *)
+ − 220
+ − 221
fun prove_fsupp ctxt qtys qinduct qsupports_thms =
+ − 222
let
+ − 223
val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt
+ − 224
val goals = vs ~~ qtys
+ − 225
|> map Free
+ − 226
|> map (mk_finite o mk_supp)
+ − 227
|> foldr1 (HOLogic.mk_conj)
+ − 228
|> HOLogic.mk_Trueprop
+ − 229
+ − 230
val tac =
+ − 231
EVERY' [ rtac @{thm supports_finite},
+ − 232
resolve_tac qsupports_thms,
3227
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 233
asm_simp_tac (put_simpset HOL_ss ctxt'
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 234
addsimps @{thms finite_supp supp_Pair finite_Un}) ]
2595
+ − 235
in
+ − 236
Goal.prove ctxt' [] [] goals
+ − 237
(K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
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
+ − 238
|> singleton (Proof_Context.export ctxt' ctxt)
2595
+ − 239
|> Datatype_Aux.split_conj_thm
+ − 240
|> map zero_var_indexes
+ − 241
end
+ − 242
+ − 243
+ − 244
(* finite supp instances *)
+ − 245
+ − 246
fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy =
+ − 247
let
+ − 248
val lthy1 =
+ − 249
lthy
+ − 250
|> Local_Theory.exit_global
+ − 251
|> Class.instantiation (qfull_ty_names, tvs, @{sort fs})
+ − 252
+ − 253
fun tac _ =
+ − 254
Class.intro_classes_tac [] THEN
+ − 255
(ALLGOALS (resolve_tac qfsupp_thms))
+ − 256
in
+ − 257
lthy1
+ − 258
|> Class.prove_instantiation_exit tac
+ − 259
|> Named_Target.theory_init
+ − 260
end
+ − 261
+ − 262
+ − 263
(* proves that fv and fv_bn equals supp *)
+ − 264
+ − 265
fun gen_mk_goals fv supp =
+ − 266
let
+ − 267
val arg_ty =
+ − 268
fastype_of fv
+ − 269
|> domain_type
+ − 270
in
+ − 271
(arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x))
+ − 272
end
+ − 273
+ − 274
fun mk_fvs_goals fv = gen_mk_goals fv mk_supp
+ − 275
fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn)
+ − 276
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 277
fun add_simpset ctxt thms = put_simpset HOL_basic_ss ctxt addsimps thms
2595
+ − 278
+ − 279
fun symmetric thms =
+ − 280
map (fn thm => thm RS @{thm sym}) thms
+ − 281
+ − 282
val supp_Abs_set = @{thms supp_Abs(1)[symmetric]}
+ − 283
val supp_Abs_res = @{thms supp_Abs(2)[symmetric]}
+ − 284
val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]}
+ − 285
+ − 286
fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set
+ − 287
| mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res
+ − 288
| mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst
+ − 289
+ − 290
fun mk_supp_abs_tac ctxt [] = []
+ − 291
| mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs
+ − 292
| mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs
+ − 293
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 294
fun mk_bn_supp_abs_tac ctxt trm =
2595
+ − 295
trm
+ − 296
|> fastype_of
+ − 297
|> body_type
+ − 298
|> (fn ty => case ty of
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 299
@{typ "atom set"} => simp_tac (add_simpset ctxt supp_Abs_set)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 300
| @{typ "atom list"} => simp_tac (add_simpset ctxt supp_Abs_lst)
2595
+ − 301
| _ => raise TERM ("mk_bn_supp_abs_tac", [trm]))
+ − 302
+ − 303
+ − 304
val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
+ − 305
val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
+ − 306
val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def
+ − 307
prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
+ − 308
+ − 309
fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps
+ − 310
fv_bn_eqvts qinduct bclausess ctxt =
+ − 311
let
+ − 312
val goals1 = map mk_fvs_goals fvs
+ − 313
val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns
+ − 314
+ − 315
fun tac ctxt =
+ − 316
SUBGOAL (fn (goal, i) =>
+ − 317
let
+ − 318
val (fv_fun, arg) =
+ − 319
goal |> Envir.eta_contract
+ − 320
|> Logic.strip_assums_concl
+ − 321
|> HOLogic.dest_Trueprop
+ − 322
|> fst o HOLogic.dest_eq
+ − 323
|> dest_comb
+ − 324
val supp_abs_tac =
+ − 325
case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of
+ − 326
SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses)
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 327
| NONE => mk_bn_supp_abs_tac ctxt fv_fun
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
+ − 328
val eqvt_rconfig = eqvt_relaxed_config addpres (perm_simps @ fv_bn_eqvts)
2595
+ − 329
in
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 330
EVERY' [ TRY o asm_full_simp_tac (add_simpset ctxt (@{thm supp_Pair[symmetric]}::fv_simps)),
2595
+ − 331
TRY o supp_abs_tac,
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 332
TRY o simp_tac (add_simpset ctxt @{thms supp_def supp_rel_def}),
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
+ − 333
TRY o eqvt_tac ctxt eqvt_rconfig,
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 334
TRY o simp_tac (add_simpset ctxt (@{thms Abs_eq_iff} @ eq_iffs)),
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 335
TRY o asm_full_simp_tac (add_simpset ctxt thms3),
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 336
TRY o simp_tac (add_simpset ctxt thms2),
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 337
TRY o asm_full_simp_tac (add_simpset ctxt (thms1 @ (symmetric fv_bn_eqvts)))] i
2595
+ − 338
end)
+ − 339
in
+ − 340
induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
3226
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 341
|> map (atomize ctxt)
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 342
|> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms fun_eq_iff[symmetric]}))
2595
+ − 343
end
+ − 344
+ − 345
+ − 346
fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt =
+ − 347
let
+ − 348
fun mk_goal qbn =
+ − 349
let
+ − 350
val arg_ty = domain_type (fastype_of qbn)
+ − 351
val finite = @{term "finite :: atom set => bool"}
+ − 352
in
+ − 353
(arg_ty, fn x => finite $ (to_set (qbn $ x)))
+ − 354
end
+ − 355
+ − 356
val props = map mk_goal qbns
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 357
val ss_tac = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (qbn_simps @
2595
+ − 358
@{thms set.simps set_append finite_insert finite.emptyI finite_Un}))
+ − 359
in
+ − 360
induct_prove qtys props qinduct (K ss_tac) ctxt
+ − 361
end
+ − 362
2598
+ − 363
2595
+ − 364
fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt =
+ − 365
let
+ − 366
val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+ − 367
val p = Free (p, @{typ perm})
+ − 368
+ − 369
fun mk_goal qperm_bn alpha_bn =
+ − 370
let
+ − 371
val arg_ty = domain_type (fastype_of alpha_bn)
+ − 372
in
+ − 373
(arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x)
+ − 374
end
+ − 375
+ − 376
val props = map2 mk_goal qperm_bns alpha_bns
+ − 377
val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 378
val ss_tac = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss)
2595
+ − 379
in
+ − 380
induct_prove qtys props qinduct (K ss_tac) 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
+ − 381
|> Proof_Context.export ctxt' ctxt
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 382
|> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms id_def}))
2595
+ − 383
end
+ − 384
2598
+ − 385
fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt =
+ − 386
let
+ − 387
val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+ − 388
val p = Free (p, @{typ perm})
2595
+ − 389
2598
+ − 390
fun mk_goal qbn qperm_bn =
+ − 391
let
+ − 392
val arg_ty = domain_type (fastype_of qbn)
+ − 393
in
+ − 394
(arg_ty, fn x =>
+ − 395
(mk_id (Abs ("", arg_ty,
+ − 396
HOLogic.mk_eq (mk_perm p (qbn $ Bound 0), qbn $ (qperm_bn $ p $ Bound 0)))) $ x))
+ − 397
end
+ − 398
+ − 399
val props = map2 mk_goal qbns qperm_bns
+ − 400
val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs
+ − 401
val ss_tac =
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 402
EVERY' [asm_full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss),
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
+ − 403
TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts),
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 404
TRY o asm_full_simp_tac (put_simpset HOL_basic_ss ctxt')]
2598
+ − 405
in
+ − 406
induct_prove qtys props qinduct (K ss_tac) 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
+ − 407
|> Proof_Context.export ctxt' ctxt
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 408
|> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms id_def}))
2598
+ − 409
end
2595
+ − 410
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 411
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 412
2629
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 413
(*** proves strong exhauts theorems ***)
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 414
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 415
(* fixme: move into nominal_library *)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 416
fun abs_const bmode ty =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 417
let
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 418
val (const_name, binder_ty, abs_ty) =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 419
case bmode of
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 420
Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst})
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 421
| Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set})
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 422
| Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res})
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 423
in
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 424
Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty]))
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 425
end
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 426
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 427
fun mk_abs bmode trm1 trm2 =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 428
abs_const bmode (fastype_of trm2) $ trm1 $ trm2
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 429
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 430
fun is_abs_eq thm =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 431
let
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 432
fun is_abs trm =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 433
case (head_of trm) of
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 434
Const (@{const_name "Abs_set"}, _) => true
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 435
| Const (@{const_name "Abs_lst"}, _) => true
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 436
| Const (@{const_name "Abs_res"}, _) => true
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 437
| _ => false
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 438
in
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 439
thm |> prop_of
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 440
|> HOLogic.dest_Trueprop
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 441
|> HOLogic.dest_eq
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 442
|> fst
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 443
|> is_abs
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 444
end
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 445
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 446
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 447
(* adds a freshness condition to the assumptions *)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 448
fun mk_ecase_prems lthy c (params, prems, concl) bclauses =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 449
let
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 450
val tys = map snd params
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 451
val binders = get_all_binders bclauses
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 452
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 453
fun prep_binder (opt, i) =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 454
let
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 455
val t = Bound (length tys - i - 1)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 456
in
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 457
case opt of
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 458
NONE => setify_ty lthy (nth tys i) t
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 459
| SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 460
end
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 461
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 462
val prems' =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 463
case binders of
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 464
[] => prems (* case: no binders *)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 465
| _ => binders (* case: binders *)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 466
|> map prep_binder
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 467
|> fold_union_env tys
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 468
|> (fn t => mk_fresh_star t c)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 469
|> (fn t => HOLogic.mk_Trueprop t :: prems)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 470
in
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 471
mk_full_horn params prems' concl
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 472
end
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 473
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 474
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 475
(* derives the freshness theorem that there exists a p, such that
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 476
(p o as) #* (c, t1,..., tn) *)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 477
fun fresh_thm ctxt c parms binders bn_finite_thms =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 478
let
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 479
fun prep_binder (opt, i) =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 480
case opt of
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 481
NONE => setify ctxt (nth parms i)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 482
| SOME bn => to_set (bn $ (nth parms i))
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 483
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 484
fun prep_binder2 (opt, i) =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 485
case opt of
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 486
NONE => atomify ctxt (nth parms i)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 487
| SOME bn => bn $ (nth parms i)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 488
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 489
val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders))
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 490
val lhs = binders
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 491
|> map prep_binder
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 492
|> fold_union
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 493
|> mk_perm (Bound 0)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 494
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 495
val goal = mk_fresh_star lhs rhs
2637
3890483c674f
final version of the ESOP paper; used set+ instead of res as requested by one reviewer
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 496
|> mk_exists ("p", @{typ perm})
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 497
|> HOLogic.mk_Trueprop
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 498
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 499
val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp}
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 500
@ @{thms finite.intros finite_Un finite_set finite_fset}
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 501
in
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 502
Goal.prove ctxt [] [] goal
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 503
(K (HEADGOAL (rtac @{thm at_set_avoiding1}
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 504
THEN_ALL_NEW (simp_tac (put_simpset HOL_ss ctxt addsimps ss)))))
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 505
end
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 506
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 507
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 508
(* derives an abs_eq theorem of the form
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 509
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 510
Exists q. [as].x = [p o as].(q o x) for non-recursive binders
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 511
Exists q. [as].x = [q o as].(q o x) for recursive binders
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 512
*)
3060
+ − 513
fun abs_eq_thm ctxt fprops p parms bn_eqvt permute_bns (bclause as (BC (bmode, binders, bodies))) =
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 514
case binders of
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 515
[] => []
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 516
| _ =>
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 517
let
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 518
val rec_flag = is_recursive_binder bclause
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 519
val binder_trm = comb_binders ctxt bmode parms binders
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 520
val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 521
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 522
val abs_lhs = mk_abs bmode binder_trm body_trm
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 523
val abs_rhs =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 524
if rec_flag
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 525
then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 526
else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 527
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 528
val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 529
val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 530
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 531
val goal = HOLogic.mk_conj (abs_eq, peq)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 532
|> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 533
|> HOLogic.mk_Trueprop
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 534
3060
+ − 535
val ss = fprops @ @{thms set.simps set_append union_eqvt}
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 536
@ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
3060
+ − 537
fresh_star_set}
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 538
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 539
val tac1 =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 540
if rec_flag
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 541
then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 542
else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 543
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 544
val tac2 =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 545
EVERY' [simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss),
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 546
TRY o simp_tac (put_simpset HOL_ss ctxt)]
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 547
in
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 548
[ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 549
|> (if rec_flag
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
+ − 550
then eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)
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
+ − 551
else eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) ]
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 552
end
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 553
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 554
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 555
val setify = @{lemma "xs = ys ==> set xs = set ys" by simp}
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 556
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 557
fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 558
prems bclausess qexhaust_thm =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 559
let
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 560
fun aux_tac prem bclauses =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 561
case (get_all_binders bclauses) of
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 562
[] => EVERY' [rtac prem, atac]
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 563
| binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 564
let
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 565
val parms = map (term_of o snd) params
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 566
val fthm = fresh_thm ctxt c parms binders bn_finite_thms
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 567
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 568
val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 569
val (([(_, fperm)], fprops), ctxt') = Obtain.result
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 570
(fn ctxt' => EVERY1 [etac exE,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 571
full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss),
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 572
REPEAT o (etac @{thm conjE})]) [fthm] ctxt
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 573
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 574
val abs_eq_thms = flat
3227
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 575
(map (abs_eq_thm ctxt' fprops (term_of fperm) parms bn_eqvt permute_bns) bclauses)
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 576
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 577
val ((_, eqs), ctxt'') = Obtain.result
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 578
(fn ctxt'' => EVERY1
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 579
[ REPEAT o (etac @{thm exE}),
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 580
REPEAT o (etac @{thm conjE}),
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 581
REPEAT o (dtac setify),
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 582
full_simp_tac (put_simpset HOL_basic_ss ctxt''
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 583
addsimps @{thms set_append set.simps})]) abs_eq_thms ctxt'
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 584
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 585
val (abs_eqs, peqs) = split_filter is_abs_eq eqs
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 586
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 587
val fprops' =
3227
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 588
map (eqvt_rule ctxt'' (eqvt_strict_config addpres permute_bns)) fprops
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 589
@ map (eqvt_rule ctxt'' (eqvt_strict_config addpres bn_eqvt)) fprops
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 590
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 591
(* for freshness conditions *)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 592
val tac1 = SOLVED' (EVERY'
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 593
[ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs),
3226
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 594
rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}),
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 595
conj_tac (DETERM o resolve_tac fprops') ])
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 596
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 597
(* for equalities between constructors *)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 598
val tac2 = SOLVED' (EVERY'
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 599
[ rtac (@{thm ssubst} OF prems),
3226
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 600
rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms),
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 601
rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs),
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 602
conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ])
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 603
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 604
(* proves goal "P" *)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 605
val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 606
(K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
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
+ − 607
|> singleton (Proof_Context.export ctxt'' ctxt)
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 608
in
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 609
rtac side_thm 1
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 610
end) ctxt
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 611
in
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 612
EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)]
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 613
end
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 614
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 615
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 616
fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 617
perm_bn_alphas =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 618
let
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 619
val ((_, exhausts'), lthy') = Variable.import true exhausts lthy
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 620
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 621
val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 622
val c = Free (c, TFree (a, @{sort fs}))
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 623
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 624
val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 625
|> map prop_of
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 626
|> map Logic.strip_horn
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 627
|> split_list
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 628
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 629
val ecases' = (map o map) strip_full_horn ecases
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 630
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 631
val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 632
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 633
fun tac bclausess exhaust {prems, context} =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 634
case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 635
prems bclausess exhaust
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 636
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 637
fun prove prems bclausess exhaust concl =
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 638
Goal.prove lthy'' [] prems concl (tac bclausess exhaust)
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 639
in
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 640
map4 prove premss bclausesss exhausts' main_concls
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
+ − 641
|> Proof_Context.export lthy'' lthy
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 642
end
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 643
2628
+ − 644
+ − 645
+ − 646
(** strong induction theorems **)
+ − 647
+ − 648
fun add_c_prop c c_ty trm =
+ − 649
let
+ − 650
val (P, arg) = dest_comb trm
+ − 651
val (P_name, P_ty) = dest_Free P
+ − 652
val (ty_args, bool) = strip_type P_ty
+ − 653
in
+ − 654
Free (P_name, (c_ty :: ty_args) ---> bool) $ c $ arg
+ − 655
end
+ − 656
+ − 657
fun add_qnt_c_prop c_name c_ty trm =
+ − 658
trm |> HOLogic.dest_Trueprop
+ − 659
|> incr_boundvars 1
+ − 660
|> add_c_prop (Bound 0) c_ty
+ − 661
|> HOLogic.mk_Trueprop
+ − 662
|> mk_all (c_name, c_ty)
+ − 663
2629
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 664
fun prep_prem lthy c c_name c_ty bclauses (params, prems, concl) =
2628
+ − 665
let
+ − 666
val tys = map snd params
+ − 667
val binders = get_all_binders bclauses
+ − 668
+ − 669
fun prep_binder (opt, i) =
+ − 670
let
+ − 671
val t = Bound (length tys - i - 1)
+ − 672
in
+ − 673
case opt of
+ − 674
NONE => setify_ty lthy (nth tys i) t
+ − 675
| SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)
+ − 676
end
+ − 677
+ − 678
val prems' = prems
+ − 679
|> map (incr_boundvars 1)
+ − 680
|> map (add_qnt_c_prop c_name c_ty)
+ − 681
+ − 682
val prems'' =
+ − 683
case binders of
+ − 684
[] => prems' (* case: no binders *)
+ − 685
| _ => binders (* case: binders *)
+ − 686
|> map prep_binder
+ − 687
|> fold_union_env tys
+ − 688
|> incr_boundvars 1
+ − 689
|> (fn t => mk_fresh_star_ty c_ty t (Bound 0))
+ − 690
|> (fn t => HOLogic.mk_Trueprop t :: prems')
+ − 691
+ − 692
val concl' = concl
+ − 693
|> HOLogic.dest_Trueprop
+ − 694
|> incr_boundvars 1
+ − 695
|> add_c_prop (Bound 0) c_ty
+ − 696
|> HOLogic.mk_Trueprop
+ − 697
in
+ − 698
mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl'
+ − 699
end
+ − 700
2630
+ − 701
fun prove_strong_induct lthy induct exhausts size_thms bclausesss =
2628
+ − 702
let
2635
+ − 703
val ((_, [induct']), lthy') = Variable.import true [induct] lthy
2628
+ − 704
+ − 705
val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
+ − 706
val c_ty = TFree (a, @{sort fs})
+ − 707
val c = Free (c_name, c_ty)
+ − 708
+ − 709
val (prems, concl) = induct'
+ − 710
|> prop_of
+ − 711
|> Logic.strip_horn
+ − 712
+ − 713
val concls = concl
+ − 714
|> HOLogic.dest_Trueprop
+ − 715
|> HOLogic.dest_conj
+ − 716
|> map (add_c_prop c c_ty)
+ − 717
|> map HOLogic.mk_Trueprop
+ − 718
+ − 719
val prems' = prems
+ − 720
|> map strip_full_horn
2629
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 721
|> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss)
2628
+ − 722
2629
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 723
fun pat_tac ctxt thm =
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 724
Subgoal.FOCUS (fn {params, context, ...} =>
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 725
let
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
+ − 726
val thy = Proof_Context.theory_of context
2629
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 727
val ty_parms = map (fn (_, ct) => (fastype_of (term_of ct), ct)) params
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 728
val vs = Term.add_vars (prop_of thm) []
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 729
val vs_tys = map (Type.legacy_freeze_type o snd) vs
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 730
val vs_ctrms = map (cterm_of thy o Var) vs
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 731
val assigns = map (lookup ty_parms) vs_tys
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 732
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 733
val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 734
in
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 735
rtac thm' 1
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 736
end) ctxt
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 737
THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt)
2629
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 738
3227
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 739
fun size_simp_tac ctxt =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 740
simp_tac (put_simpset size_ss ctxt addsimps (@{thms comp_def snd_conv} @ size_thms))
2630
+ − 741
in
+ − 742
Goal.prove_multi lthy'' [] prems' concls
3227
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 743
(fn {prems, context = ctxt} =>
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 744
Induction_Schema.induction_schema_tac ctxt prems
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 745
THEN RANGE (map (pat_tac ctxt) exhausts) 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 746
THEN prove_termination_ind ctxt 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 747
THEN ALLGOALS (size_simp_tac 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
+ − 748
|> Proof_Context.export lthy'' lthy
2628
+ − 749
end
+ − 750
+ − 751
2337
+ − 752
end (* structure *)
+ − 753