equal
deleted
inserted
replaced
11 |
11 |
12 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> |
12 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> |
13 bclause list list list -> term list -> Proof.context -> |
13 bclause list list list -> term list -> Proof.context -> |
14 term list * term list * thm list * thm list * thm * local_theory |
14 term list * term list * thm list * thm list * thm * local_theory |
15 |
15 |
16 val mk_alpha_distincts: Proof.context -> thm list -> thm list -> |
16 val raw_prove_alpha_distincts: Proof.context -> thm list -> thm list -> |
17 term list -> string list -> thm list |
17 term list -> string list -> thm list |
18 |
18 |
19 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
19 val raw_prove_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
20 thm list -> thm list |
20 thm list -> thm list |
21 |
21 |
22 val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> |
22 val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> |
23 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
23 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
24 |
24 |
295 fun distinct_tac cases_thms distinct_thms = |
295 fun distinct_tac cases_thms distinct_thms = |
296 rtac notI THEN' eresolve_tac cases_thms |
296 rtac notI THEN' eresolve_tac cases_thms |
297 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
297 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
298 |
298 |
299 |
299 |
300 fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str = |
300 fun raw_prove_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str = |
301 let |
301 let |
302 val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms) |
302 val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms) |
303 |
303 |
304 fun mk_alpha_distinct distinct_trm = |
304 fun mk_alpha_distinct distinct_trm = |
305 let |
305 let |
339 in |
339 in |
340 if hyps = [] then HOLogic.mk_Trueprop concl |
340 if hyps = [] then HOLogic.mk_Trueprop concl |
341 else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) |
341 else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) |
342 end; |
342 end; |
343 |
343 |
344 fun mk_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims = |
344 fun raw_prove_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims = |
345 let |
345 let |
346 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; |
346 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; |
347 val goals = map mk_alpha_eq_iff_goal thms_imp; |
347 val goals = map mk_alpha_eq_iff_goal thms_imp; |
348 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; |
348 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; |
349 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
349 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |