equal
deleted
inserted
replaced
53 tactic |
53 tactic |
54 val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> thm list -> |
54 val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> thm list -> |
55 thm list list -> tactic |
55 thm list list -> tactic |
56 val mk_mor_UNIV_tac: Proof.context -> int -> thm list -> thm -> tactic |
56 val mk_mor_UNIV_tac: Proof.context -> int -> thm list -> thm -> tactic |
57 val mk_mor_comp_tac: Proof.context -> thm -> thm list list -> thm list -> tactic |
57 val mk_mor_comp_tac: Proof.context -> thm -> thm list list -> thm list -> tactic |
58 val mk_mor_convol_tac: Proof.context -> 'a list -> thm -> tactic |
|
59 val mk_mor_elim_tac: Proof.context -> thm -> tactic |
58 val mk_mor_elim_tac: Proof.context -> thm -> tactic |
60 val mk_mor_incl_tac: Proof.context -> thm -> thm list -> tactic |
59 val mk_mor_incl_tac: Proof.context -> thm -> thm list -> tactic |
61 val mk_mor_fold_tac: Proof.context -> ctyp -> cterm -> thm list -> thm -> thm -> tactic |
60 val mk_mor_fold_tac: Proof.context -> ctyp -> cterm -> thm list -> thm -> thm -> tactic |
62 val mk_mor_select_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> |
61 val mk_mor_select_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> |
63 thm list list -> thm list -> tactic |
62 thm list list -> thm list -> tactic |
142 |
141 |
143 fun mk_mor_str_tac ctxt ks mor_def = |
142 fun mk_mor_str_tac ctxt ks mor_def = |
144 (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN' |
143 (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN' |
145 CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN' |
144 CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN' |
146 CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt refl])) ks) 1; |
145 CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt refl])) ks) 1; |
147 |
|
148 fun mk_mor_convol_tac ctxt ks mor_def = |
|
149 (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN' |
|
150 CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN' |
|
151 CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt trans, rtac ctxt @{thm fst_convol'}, rtac ctxt o_apply])) ks) 1; |
|
152 |
146 |
153 fun mk_mor_UNIV_tac ctxt m morEs mor_def = |
147 fun mk_mor_UNIV_tac ctxt m morEs mor_def = |
154 let |
148 let |
155 val n = length morEs; |
149 val n = length morEs; |
156 fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE, |
150 fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE, |