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 ->
|
2337
|
12 |
thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory
|
|
13 |
|
2400
|
14 |
val define_qconsts: typ list -> (string * term * mixfix) list -> local_theory ->
|
2337
|
15 |
Quotient_Info.qconsts_info 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 ->
|
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
(string * term * mixfix) 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 ->
|
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
(string * term * mixfix) 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
|
|
61 |
val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms
|
|
62 |
in
|
|
63 |
fold_map Quotient_Type.add_quotient_type qty_args2 lthy
|
|
64 |
end
|
2337
|
65 |
|
2338
|
66 |
|
2337
|
67 |
(* defines quotient constants *)
|
2400
|
68 |
fun define_qconsts qtys consts_specs lthy =
|
2476
|
69 |
let
|
|
70 |
val (qconst_infos, lthy') =
|
|
71 |
fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy
|
|
72 |
val phi = ProofContext.export_morphism lthy' lthy
|
|
73 |
in
|
|
74 |
(map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy')
|
|
75 |
end
|
2337
|
76 |
|
|
77 |
|
2400
|
78 |
(* 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
|
79 |
fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy =
|
2476
|
80 |
let
|
|
81 |
val lthy1 =
|
|
82 |
lthy
|
|
83 |
|> Local_Theory.exit_global
|
|
84 |
|> Class.instantiation (qfull_ty_names, tvs, @{sort pt})
|
2398
|
85 |
|
2476
|
86 |
val (qs, 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
|
87 |
|
2476
|
88 |
val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2
|
2398
|
89 |
|
2476
|
90 |
val lifted_perm_laws =
|
|
91 |
map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
|
|
92 |
|> Variable.exportT lthy3 lthy2
|
2398
|
93 |
|
2476
|
94 |
fun tac _ =
|
|
95 |
Class.intro_classes_tac [] THEN
|
|
96 |
(ALLGOALS (resolve_tac lifted_perm_laws))
|
|
97 |
in
|
|
98 |
lthy2
|
|
99 |
|> Class.prove_instantiation_exit tac
|
|
100 |
|> Named_Target.theory_init
|
|
101 |
end
|
2346
|
102 |
|
2337
|
103 |
|
2400
|
104 |
(* 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
|
105 |
fun define_qsizes qtys qfull_ty_names tvs size_specs lthy =
|
2476
|
106 |
let
|
|
107 |
val tac = K (Class.intro_classes_tac [])
|
|
108 |
in
|
|
109 |
lthy
|
|
110 |
|> Local_Theory.exit_global
|
|
111 |
|> Class.instantiation (qfull_ty_names, tvs, @{sort size})
|
|
112 |
|> snd o (define_qconsts qtys size_specs)
|
|
113 |
|> Class.prove_instantiation_exit tac
|
|
114 |
|> Named_Target.theory_init
|
|
115 |
end
|
2400
|
116 |
|
2426
|
117 |
|
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
|
118 |
(* 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
|
119 |
from variable names *)
|
2426
|
120 |
|
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
121 |
local
|
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
122 |
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
|
123 |
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
|
124 |
val exclude =
|
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
125 |
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
|
126 |
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
|
127 |
in
|
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
128 |
fun unraw_str s =
|
2574
|
129 |
s |> raw_explode
|
2476
|
130 |
|> Scan.finite Symbol.stopper parser >> implode
|
|
131 |
|> fst
|
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
132 |
end
|
2426
|
133 |
|
|
134 |
fun unraw_vars_thm thm =
|
2476
|
135 |
let
|
|
136 |
fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
|
2426
|
137 |
|
2476
|
138 |
val vars = Term.add_vars (prop_of thm) []
|
|
139 |
val vars' = map (Var o unraw_var_str) vars
|
|
140 |
in
|
|
141 |
Thm.certify_instantiate ([], (vars ~~ vars')) thm
|
|
142 |
end
|
2426
|
143 |
|
|
144 |
fun unraw_bounds_thm th =
|
2476
|
145 |
let
|
|
146 |
val trm = Thm.prop_of th
|
|
147 |
val trm' = Term.map_abs_vars unraw_str trm
|
|
148 |
in
|
|
149 |
Thm.rename_boundvars trm trm' th
|
|
150 |
end
|
2426
|
151 |
|
2434
|
152 |
fun lift_thms qtys simps thms ctxt =
|
|
153 |
(map (Quotient_Tacs.lifted ctxt qtys simps
|
|
154 |
#> unraw_bounds_thm
|
|
155 |
#> unraw_vars_thm
|
|
156 |
#> Drule.zero_var_indexes) thms, ctxt)
|
|
157 |
|
2595
|
158 |
|
|
159 |
|
|
160 |
fun mk_supports_goal ctxt qtrm =
|
|
161 |
let
|
|
162 |
val vs = fresh_args ctxt qtrm
|
|
163 |
val rhs = list_comb (qtrm, vs)
|
|
164 |
val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"}
|
|
165 |
|> mk_supp
|
|
166 |
in
|
|
167 |
mk_supports lhs rhs
|
|
168 |
|> HOLogic.mk_Trueprop
|
|
169 |
end
|
|
170 |
|
|
171 |
fun supports_tac ctxt perm_simps =
|
|
172 |
let
|
|
173 |
val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]}
|
|
174 |
val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair}
|
|
175 |
in
|
|
176 |
EVERY' [ simp_tac ss1,
|
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
|
177 |
eqvt_tac ctxt (eqvt_strict_config addpres perm_simps),
|
2595
|
178 |
simp_tac ss2 ]
|
|
179 |
end
|
|
180 |
|
|
181 |
fun prove_supports_single ctxt perm_simps qtrm =
|
|
182 |
let
|
|
183 |
val goal = mk_supports_goal ctxt qtrm
|
|
184 |
val ctxt' = Variable.auto_fixes goal ctxt
|
|
185 |
in
|
|
186 |
Goal.prove ctxt' [] [] goal
|
|
187 |
(K (HEADGOAL (supports_tac ctxt perm_simps)))
|
|
188 |
|> singleton (ProofContext.export ctxt' ctxt)
|
|
189 |
end
|
|
190 |
|
|
191 |
fun prove_supports ctxt perm_simps qtrms =
|
|
192 |
map (prove_supports_single ctxt perm_simps) qtrms
|
|
193 |
|
|
194 |
|
|
195 |
(* finite supp lemmas for qtypes *)
|
|
196 |
|
|
197 |
fun prove_fsupp ctxt qtys qinduct qsupports_thms =
|
|
198 |
let
|
|
199 |
val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt
|
|
200 |
val goals = vs ~~ qtys
|
|
201 |
|> map Free
|
|
202 |
|> map (mk_finite o mk_supp)
|
|
203 |
|> foldr1 (HOLogic.mk_conj)
|
|
204 |
|> HOLogic.mk_Trueprop
|
|
205 |
|
|
206 |
val tac =
|
|
207 |
EVERY' [ rtac @{thm supports_finite},
|
|
208 |
resolve_tac qsupports_thms,
|
|
209 |
asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ]
|
|
210 |
in
|
|
211 |
Goal.prove ctxt' [] [] goals
|
|
212 |
(K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
|
|
213 |
|> singleton (ProofContext.export ctxt' ctxt)
|
|
214 |
|> Datatype_Aux.split_conj_thm
|
|
215 |
|> map zero_var_indexes
|
|
216 |
end
|
|
217 |
|
|
218 |
|
|
219 |
(* finite supp instances *)
|
|
220 |
|
|
221 |
fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy =
|
|
222 |
let
|
|
223 |
val lthy1 =
|
|
224 |
lthy
|
|
225 |
|> Local_Theory.exit_global
|
|
226 |
|> Class.instantiation (qfull_ty_names, tvs, @{sort fs})
|
|
227 |
|
|
228 |
fun tac _ =
|
|
229 |
Class.intro_classes_tac [] THEN
|
|
230 |
(ALLGOALS (resolve_tac qfsupp_thms))
|
|
231 |
in
|
|
232 |
lthy1
|
|
233 |
|> Class.prove_instantiation_exit tac
|
|
234 |
|> Named_Target.theory_init
|
|
235 |
end
|
|
236 |
|
|
237 |
|
|
238 |
(* proves that fv and fv_bn equals supp *)
|
|
239 |
|
|
240 |
fun gen_mk_goals fv supp =
|
|
241 |
let
|
|
242 |
val arg_ty =
|
|
243 |
fastype_of fv
|
|
244 |
|> domain_type
|
|
245 |
in
|
|
246 |
(arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x))
|
|
247 |
end
|
|
248 |
|
|
249 |
fun mk_fvs_goals fv = gen_mk_goals fv mk_supp
|
|
250 |
fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn)
|
|
251 |
|
|
252 |
fun add_ss thms =
|
|
253 |
HOL_basic_ss addsimps thms
|
|
254 |
|
|
255 |
fun symmetric thms =
|
|
256 |
map (fn thm => thm RS @{thm sym}) thms
|
|
257 |
|
|
258 |
val supp_Abs_set = @{thms supp_Abs(1)[symmetric]}
|
|
259 |
val supp_Abs_res = @{thms supp_Abs(2)[symmetric]}
|
|
260 |
val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]}
|
|
261 |
|
|
262 |
fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set
|
|
263 |
| mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res
|
|
264 |
| mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst
|
|
265 |
|
|
266 |
fun mk_supp_abs_tac ctxt [] = []
|
|
267 |
| mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs
|
|
268 |
| mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs
|
|
269 |
|
|
270 |
fun mk_bn_supp_abs_tac trm =
|
|
271 |
trm
|
|
272 |
|> fastype_of
|
|
273 |
|> body_type
|
|
274 |
|> (fn ty => case ty of
|
|
275 |
@{typ "atom set"} => simp_tac (add_ss supp_Abs_set)
|
|
276 |
| @{typ "atom list"} => simp_tac (add_ss supp_Abs_lst)
|
|
277 |
| _ => raise TERM ("mk_bn_supp_abs_tac", [trm]))
|
|
278 |
|
|
279 |
|
|
280 |
val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
|
|
281 |
val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
|
|
282 |
val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def
|
|
283 |
prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
|
|
284 |
|
|
285 |
fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps
|
|
286 |
fv_bn_eqvts qinduct bclausess ctxt =
|
|
287 |
let
|
|
288 |
val goals1 = map mk_fvs_goals fvs
|
|
289 |
val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns
|
|
290 |
|
|
291 |
fun tac ctxt =
|
|
292 |
SUBGOAL (fn (goal, i) =>
|
|
293 |
let
|
|
294 |
val (fv_fun, arg) =
|
|
295 |
goal |> Envir.eta_contract
|
|
296 |
|> Logic.strip_assums_concl
|
|
297 |
|> HOLogic.dest_Trueprop
|
|
298 |
|> fst o HOLogic.dest_eq
|
|
299 |
|> dest_comb
|
|
300 |
val supp_abs_tac =
|
|
301 |
case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of
|
|
302 |
SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses)
|
|
303 |
| NONE => mk_bn_supp_abs_tac 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
|
304 |
val eqvt_rconfig = eqvt_relaxed_config addpres (perm_simps @ fv_bn_eqvts)
|
2595
|
305 |
in
|
|
306 |
EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)),
|
|
307 |
TRY o supp_abs_tac,
|
|
308 |
TRY o simp_tac (add_ss @{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
|
309 |
TRY o eqvt_tac ctxt eqvt_rconfig,
|
2595
|
310 |
TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
|
|
311 |
TRY o asm_full_simp_tac (add_ss thms3),
|
|
312 |
TRY o simp_tac (add_ss thms2),
|
|
313 |
TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i
|
|
314 |
end)
|
|
315 |
in
|
|
316 |
induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
|
|
317 |
|> map atomize
|
|
318 |
|> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]}))
|
|
319 |
end
|
|
320 |
|
|
321 |
|
|
322 |
fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt =
|
|
323 |
let
|
|
324 |
fun mk_goal qbn =
|
|
325 |
let
|
|
326 |
val arg_ty = domain_type (fastype_of qbn)
|
|
327 |
val finite = @{term "finite :: atom set => bool"}
|
|
328 |
in
|
|
329 |
(arg_ty, fn x => finite $ (to_set (qbn $ x)))
|
|
330 |
end
|
|
331 |
|
|
332 |
val props = map mk_goal qbns
|
|
333 |
val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @
|
|
334 |
@{thms set.simps set_append finite_insert finite.emptyI finite_Un}))
|
|
335 |
in
|
|
336 |
induct_prove qtys props qinduct (K ss_tac) ctxt
|
|
337 |
end
|
|
338 |
|
2598
|
339 |
|
2595
|
340 |
fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt =
|
|
341 |
let
|
|
342 |
val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
|
|
343 |
val p = Free (p, @{typ perm})
|
|
344 |
|
|
345 |
fun mk_goal qperm_bn alpha_bn =
|
|
346 |
let
|
|
347 |
val arg_ty = domain_type (fastype_of alpha_bn)
|
|
348 |
in
|
|
349 |
(arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x)
|
|
350 |
end
|
|
351 |
|
|
352 |
val props = map2 mk_goal qperm_bns alpha_bns
|
|
353 |
val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls
|
|
354 |
val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss)
|
|
355 |
in
|
|
356 |
induct_prove qtys props qinduct (K ss_tac) ctxt'
|
|
357 |
|> ProofContext.export ctxt' ctxt
|
|
358 |
|> map (simplify (HOL_basic_ss addsimps @{thms id_def}))
|
|
359 |
end
|
|
360 |
|
2598
|
361 |
fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt =
|
|
362 |
let
|
|
363 |
val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
|
|
364 |
val p = Free (p, @{typ perm})
|
2595
|
365 |
|
2598
|
366 |
fun mk_goal qbn qperm_bn =
|
|
367 |
let
|
|
368 |
val arg_ty = domain_type (fastype_of qbn)
|
|
369 |
in
|
|
370 |
(arg_ty, fn x =>
|
|
371 |
(mk_id (Abs ("", arg_ty,
|
|
372 |
HOLogic.mk_eq (mk_perm p (qbn $ Bound 0), qbn $ (qperm_bn $ p $ Bound 0)))) $ x))
|
|
373 |
end
|
|
374 |
|
|
375 |
val props = map2 mk_goal qbns qperm_bns
|
|
376 |
val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs
|
|
377 |
val ss_tac =
|
|
378 |
EVERY' [asm_full_simp_tac (HOL_basic_ss 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
|
379 |
TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts),
|
2598
|
380 |
TRY o asm_full_simp_tac HOL_basic_ss]
|
|
381 |
in
|
|
382 |
induct_prove qtys props qinduct (K ss_tac) ctxt'
|
|
383 |
|> ProofContext.export ctxt' ctxt
|
|
384 |
|> map (simplify (HOL_basic_ss addsimps @{thms id_def}))
|
|
385 |
end
|
2595
|
386 |
|
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
387 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
388 |
|
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
|
389 |
(*** 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
|
390 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
391 |
(* 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
|
392 |
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
|
393 |
let
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
394 |
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
|
395 |
case bmode of
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
396 |
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
|
397 |
| 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
|
398 |
| 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
|
399 |
in
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
400 |
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
|
401 |
end
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
402 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
403 |
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
|
404 |
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
|
405 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
406 |
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
|
407 |
let
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
408 |
fun is_abs trm =
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
409 |
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
|
410 |
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
|
411 |
| 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
|
412 |
| 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
|
413 |
| _ => false
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
414 |
in
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
415 |
thm |> prop_of
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
416 |
|> HOLogic.dest_Trueprop
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
417 |
|> HOLogic.dest_eq
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
418 |
|> fst
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
419 |
|> is_abs
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
420 |
end
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
421 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
422 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
423 |
(* 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
|
424 |
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
|
425 |
let
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
426 |
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
|
427 |
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
|
428 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
429 |
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
|
430 |
let
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
431 |
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
|
432 |
in
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
433 |
case opt of
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
434 |
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
|
435 |
| 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
|
436 |
end
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
437 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
438 |
val prems' =
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
439 |
case binders of
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
440 |
[] => prems (* case: no binders *)
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
441 |
| _ => binders (* case: binders *)
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
442 |
|> map prep_binder
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
443 |
|> fold_union_env tys
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
444 |
|> (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
|
445 |
|> (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
|
446 |
in
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
447 |
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
|
448 |
end
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
449 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
450 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
451 |
(* 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
|
452 |
(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
|
453 |
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
|
454 |
let
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
455 |
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
|
456 |
case opt of
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
457 |
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
|
458 |
| 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
|
459 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
460 |
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
|
461 |
case opt of
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
462 |
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
|
463 |
| 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
|
464 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
465 |
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
|
466 |
val lhs = binders
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
467 |
|> map prep_binder
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
468 |
|> fold_union
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
469 |
|> mk_perm (Bound 0)
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
470 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
471 |
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
|
472 |
|> 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
|
473 |
|> HOLogic.mk_Trueprop
|
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 |
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
|
476 |
@ @{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
|
477 |
in
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
478 |
Goal.prove ctxt [] [] goal
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
479 |
(K (HEADGOAL (rtac @{thm at_set_avoiding1}
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
480 |
THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
481 |
end
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
482 |
|
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 |
(* 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
|
485 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
486 |
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
|
487 |
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
|
488 |
*)
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
489 |
fun abs_eq_thm ctxt fprops p parms bn_finite_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
|
490 |
(bclause as (BC (bmode, binders, bodies))) =
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
491 |
case binders of
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
492 |
[] => []
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
493 |
| _ =>
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
494 |
let
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
495 |
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
|
496 |
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
|
497 |
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
|
498 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
499 |
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
|
500 |
val abs_rhs =
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
501 |
if rec_flag
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
502 |
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
|
503 |
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
|
504 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
505 |
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
|
506 |
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
|
507 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
508 |
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
|
509 |
|> (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
|
510 |
|> HOLogic.mk_Trueprop
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
511 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
512 |
val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
513 |
@ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
514 |
fresh_star_set} @ @{thms finite.intros finite_fset}
|
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 |
val tac1 =
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
517 |
if rec_flag
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
518 |
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
|
519 |
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
|
520 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
521 |
val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss]
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
522 |
in
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
523 |
[ 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
|
524 |
|> (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
|
525 |
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
|
526 |
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
|
527 |
end
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
528 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
529 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
530 |
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
|
531 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
532 |
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
|
533 |
prems bclausess qexhaust_thm =
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
534 |
let
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
535 |
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
|
536 |
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
|
537 |
[] => EVERY' [rtac prem, atac]
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
538 |
| 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
|
539 |
let
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
540 |
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
|
541 |
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
|
542 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
543 |
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
|
544 |
val (([(_, fperm)], fprops), ctxt') = Obtain.result
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
545 |
(K (EVERY1 [etac exE,
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
546 |
full_simp_tac (HOL_basic_ss addsimps ss),
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
547 |
REPEAT o (etac @{thm conjE})])) [fthm] ctxt
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
548 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
549 |
val abs_eq_thms = flat
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
550 |
(map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses)
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
551 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
552 |
val ((_, eqs), ctxt'') = Obtain.result
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
553 |
(K (EVERY1
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
554 |
[ 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
|
555 |
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
|
556 |
REPEAT o (dtac setify),
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
557 |
full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt'
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
558 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
559 |
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
|
560 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
561 |
val fprops' =
|
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
|
562 |
map (eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) fprops
|
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
|
563 |
@ 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
|
564 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
565 |
(* for freshness conditions *)
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
566 |
val tac1 = SOLVED' (EVERY'
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
567 |
[ simp_tac (HOL_basic_ss addsimps peqs),
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
568 |
rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
569 |
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
|
570 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
571 |
(* for equalities between constructors *)
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
572 |
val tac2 = SOLVED' (EVERY'
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
573 |
[ rtac (@{thm ssubst} OF prems),
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
574 |
rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
575 |
rewrite_goal_tac (map safe_mk_equiv abs_eqs),
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
576 |
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
|
577 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
578 |
(* proves goal "P" *)
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
579 |
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
|
580 |
(K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
581 |
|> singleton (ProofContext.export ctxt'' ctxt)
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
582 |
in
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
583 |
rtac side_thm 1
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
584 |
end) ctxt
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
585 |
in
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
586 |
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
|
587 |
end
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
588 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
589 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
590 |
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
|
591 |
perm_bn_alphas =
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
592 |
let
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
593 |
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
|
594 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
595 |
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
|
596 |
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
|
597 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
598 |
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
|
599 |
|> map prop_of
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
600 |
|> map Logic.strip_horn
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
601 |
|> split_list
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
602 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
603 |
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
|
604 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
605 |
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
|
606 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
607 |
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
|
608 |
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
|
609 |
prems bclausess exhaust
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
610 |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
611 |
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
|
612 |
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
|
613 |
in
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
614 |
map4 prove premss bclausesss exhausts' main_concls
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
615 |
|> ProofContext.export lthy'' lthy
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
616 |
end
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
617 |
|
2628
|
618 |
|
|
619 |
|
|
620 |
(** strong induction theorems **)
|
|
621 |
|
|
622 |
fun add_c_prop c c_ty trm =
|
|
623 |
let
|
|
624 |
val (P, arg) = dest_comb trm
|
|
625 |
val (P_name, P_ty) = dest_Free P
|
|
626 |
val (ty_args, bool) = strip_type P_ty
|
|
627 |
in
|
|
628 |
Free (P_name, (c_ty :: ty_args) ---> bool) $ c $ arg
|
|
629 |
end
|
|
630 |
|
|
631 |
fun add_qnt_c_prop c_name c_ty trm =
|
|
632 |
trm |> HOLogic.dest_Trueprop
|
|
633 |
|> incr_boundvars 1
|
|
634 |
|> add_c_prop (Bound 0) c_ty
|
|
635 |
|> HOLogic.mk_Trueprop
|
|
636 |
|> mk_all (c_name, c_ty)
|
|
637 |
|
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
|
638 |
fun prep_prem lthy c c_name c_ty bclauses (params, prems, concl) =
|
2628
|
639 |
let
|
|
640 |
val tys = map snd params
|
|
641 |
val binders = get_all_binders bclauses
|
|
642 |
|
|
643 |
fun prep_binder (opt, i) =
|
|
644 |
let
|
|
645 |
val t = Bound (length tys - i - 1)
|
|
646 |
in
|
|
647 |
case opt of
|
|
648 |
NONE => setify_ty lthy (nth tys i) t
|
|
649 |
| SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)
|
|
650 |
end
|
|
651 |
|
|
652 |
val prems' = prems
|
|
653 |
|> map (incr_boundvars 1)
|
|
654 |
|> map (add_qnt_c_prop c_name c_ty)
|
|
655 |
|
|
656 |
val prems'' =
|
|
657 |
case binders of
|
|
658 |
[] => prems' (* case: no binders *)
|
|
659 |
| _ => binders (* case: binders *)
|
|
660 |
|> map prep_binder
|
|
661 |
|> fold_union_env tys
|
|
662 |
|> incr_boundvars 1
|
|
663 |
|> (fn t => mk_fresh_star_ty c_ty t (Bound 0))
|
|
664 |
|> (fn t => HOLogic.mk_Trueprop t :: prems')
|
|
665 |
|
|
666 |
val concl' = concl
|
|
667 |
|> HOLogic.dest_Trueprop
|
|
668 |
|> incr_boundvars 1
|
|
669 |
|> add_c_prop (Bound 0) c_ty
|
|
670 |
|> HOLogic.mk_Trueprop
|
|
671 |
in
|
|
672 |
mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl'
|
|
673 |
end
|
|
674 |
|
2630
|
675 |
fun prove_strong_induct lthy induct exhausts size_thms bclausesss =
|
2628
|
676 |
let
|
2635
|
677 |
val ((_, [induct']), lthy') = Variable.import true [induct] lthy
|
2628
|
678 |
|
|
679 |
val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
|
|
680 |
val c_ty = TFree (a, @{sort fs})
|
|
681 |
val c = Free (c_name, c_ty)
|
|
682 |
|
|
683 |
val (prems, concl) = induct'
|
|
684 |
|> prop_of
|
|
685 |
|> Logic.strip_horn
|
|
686 |
|
|
687 |
val concls = concl
|
|
688 |
|> HOLogic.dest_Trueprop
|
|
689 |
|> HOLogic.dest_conj
|
|
690 |
|> map (add_c_prop c c_ty)
|
|
691 |
|> map HOLogic.mk_Trueprop
|
|
692 |
|
|
693 |
val prems' = prems
|
|
694 |
|> 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
|
695 |
|> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss)
|
2628
|
696 |
|
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
|
697 |
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
|
698 |
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
|
699 |
let
|
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
|
700 |
val thy = ProofContext.theory_of 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
|
701 |
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
|
702 |
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
|
703 |
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
|
704 |
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
|
705 |
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
|
706 |
|
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
|
707 |
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
|
708 |
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
|
709 |
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
|
710 |
end) ctxt
|
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
|
711 |
THEN_ALL_NEW asm_full_simp_tac HOL_basic_ss
|
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
|
712 |
|
2630
|
713 |
val size_simp_tac =
|
|
714 |
simp_tac (size_simpset addsimps (@{thms comp_def snd_conv} @ size_thms))
|
|
715 |
in
|
|
716 |
Goal.prove_multi lthy'' [] prems' concls
|
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
|
717 |
(fn {prems, context} =>
|
2630
|
718 |
Induction_Schema.induction_schema_tac context prems
|
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
|
719 |
THEN RANGE (map (pat_tac context) exhausts) 1
|
2630
|
720 |
THEN prove_termination_ind context 1
|
|
721 |
THEN ALLGOALS size_simp_tac)
|
|
722 |
|> ProofContext.export lthy'' lthy
|
2628
|
723 |
end
|
|
724 |
|
|
725 |
|
2337
|
726 |
end (* structure *)
|
|
727 |
|