9 sig |
9 sig |
10 val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
10 val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
11 bclause list list list -> term list -> Proof.context -> |
11 bclause list list list -> term list -> Proof.context -> |
12 term list * term list * thm list * thm list * thm * local_theory |
12 term list * term list * thm list * thm list * thm * local_theory |
13 |
13 |
14 val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> |
14 val mk_alpha_distincts: Proof.context -> thm list -> thm list -> |
15 term list -> term list -> bn_info -> thm list * thm list |
15 term list -> typ list -> thm list |
16 |
16 |
17 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
17 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
18 thm list -> (thm list * thm list) |
18 thm list -> (thm list * thm list) |
19 |
19 |
20 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
20 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
268 |
268 |
269 (** produces the distinctness theorems **) |
269 (** produces the distinctness theorems **) |
270 |
270 |
271 (* transforms the distinctness theorems of the constructors |
271 (* transforms the distinctness theorems of the constructors |
272 to "not-alphas" of the constructors *) |
272 to "not-alphas" of the constructors *) |
273 fun mk_alpha_distinct_goal alpha neq = |
273 fun mk_distinct_goal ty_trm_assoc neq = |
274 let |
274 let |
275 val (lhs, rhs) = |
275 val (lhs, rhs) = |
276 neq |
276 neq |
277 |> HOLogic.dest_Trueprop |
277 |> HOLogic.dest_Trueprop |
278 |> HOLogic.dest_not |
278 |> HOLogic.dest_not |
279 |> HOLogic.dest_eq |
279 |> HOLogic.dest_eq |
280 in |
280 val ty = fastype_of lhs |
281 alpha $ lhs $ rhs |
281 in |
|
282 (lookup ty_trm_assoc ty) $ lhs $ rhs |
282 |> HOLogic.mk_not |
283 |> HOLogic.mk_not |
283 |> HOLogic.mk_Trueprop |
284 |> HOLogic.mk_Trueprop |
284 end |
285 end |
285 |
286 |
286 fun distinct_tac cases distinct_thms = |
287 fun distinct_tac cases_thms distinct_thms = |
287 rtac notI THEN' eresolve_tac cases |
288 rtac notI THEN' eresolve_tac cases_thms |
288 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
289 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
289 |
290 |
290 fun mk_alpha_distinct ctxt cases_thms (distinct_thm, alpha) = |
291 |
291 let |
292 fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys = |
292 val ((_, thms), ctxt') = Variable.import false distinct_thm ctxt |
293 let |
293 val goals = map (mk_alpha_distinct_goal alpha o prop_of) thms |
294 val ty_trm_assoc = alpha_tys ~~ alpha_trms |
294 val nrels = map (fn t => Goal.prove ctxt' [] [] t (K (distinct_tac cases_thms distinct_thm 1))) goals |
295 |
295 in |
296 fun mk_alpha_distinct distinct_trm = |
296 Variable.export ctxt' ctxt nrels |
297 let |
297 end |
298 val ([trm'], ctxt') = Variable.import_terms true [distinct_trm] ctxt |
298 |
299 val goal = mk_distinct_goal ty_trm_assoc trm' |
299 fun mk_alpha_distincts ctxt alpha_cases constrs_distinct_thms alpha_trms alpha_bn_trms bn_infos = |
300 in |
300 let |
301 Goal.prove ctxt' [] [] goal |
301 val alpha_distincts = |
302 (K (distinct_tac cases_thms distinct_thms 1)) |
302 map (mk_alpha_distinct ctxt alpha_cases) (constrs_distinct_thms ~~ alpha_trms) |
303 |> singleton (Variable.export ctxt' ctxt) |
303 val distinc_thms = map |
304 end |
304 val alpha_bn_distincts_aux = map (fn (_, i, _) => nth constrs_distinct_thms i) bn_infos |
305 |
305 val alpha_bn_distincts = |
306 in |
306 map (mk_alpha_distinct ctxt alpha_cases) (alpha_bn_distincts_aux ~~ alpha_bn_trms) |
307 map (mk_alpha_distinct o prop_of) distinct_thms |
307 in |
|
308 (flat alpha_distincts, flat alpha_bn_distincts) |
|
309 end |
308 end |
310 |
309 |
311 |
310 |
312 |
311 |
313 (** produces the alpha_eq_iff simplification rules **) |
312 (** produces the alpha_eq_iff simplification rules **) |
690 (K (HEADGOAL |
689 (K (HEADGOAL |
691 (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps))) |
690 (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps))) |
692 end |
691 end |
693 |
692 |
694 |
693 |
695 (* transformation of the natural rsp-lemmas into the standard form *) |
694 (* transformation of the natural rsp-lemmas into standard form *) |
696 |
695 |
697 val fun_rsp = @{lemma |
696 val fun_rsp = @{lemma |
698 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp} |
697 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp} |
699 |
698 |
700 fun mk_funs_rsp thm = |
699 fun mk_funs_rsp thm = |