1(* Title: HOL/Tools/BNF/bnf_tactics.ML 2 Author: Dmitriy Traytel, TU Muenchen 3 Author: Jasmin Blanchette, TU Muenchen 4 Copyright 2012 5 6General tactics for bounded natural functors. 7*) 8 9signature BNF_TACTICS = 10sig 11 include CTR_SUGAR_GENERAL_TACTICS 12 13 val fo_rtac: Proof.context -> thm -> int -> tactic 14 val clean_blast_tac: Proof.context -> int -> tactic 15 val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic 16 val subst_asm_tac: Proof.context -> int list option -> thm list -> int -> tactic 17 18 val mk_rotate_eq_tac: Proof.context -> (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> 19 ''a list -> int -> tactic 20 21 val mk_pointfree2: Proof.context -> thm -> thm 22 23 val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm 24 val mk_Abs_inj_thm: thm -> thm 25 26 val mk_map_comp_id_tac: Proof.context -> thm -> tactic 27 val mk_map_cong0_tac: Proof.context -> int -> thm -> tactic 28 val mk_map_cong0L_tac: Proof.context -> int -> thm -> thm -> tactic 29end; 30 31structure BNF_Tactics : BNF_TACTICS = 32struct 33 34open Ctr_Sugar_General_Tactics 35open BNF_Util 36 37(*stolen from Christian Urban's Cookbook (and adapted slightly)*) 38fun fo_rtac ctxt thm = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => 39 let 40 val concl_pat = Drule.strip_imp_concl (Thm.cprop_of thm) 41 val insts = Thm.first_order_match (concl_pat, concl) 42 in 43 rtac ctxt (Drule.instantiate_normalize insts thm) 1 44 end 45 handle Pattern.MATCH => no_tac) ctxt; 46 47fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of \<^theory_context>\<open>HOL\<close>) ctxt); 48 49(*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*) 50fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0]; 51fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt o the_default [0]; 52 53(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) 54fun mk_pointfree2 ctxt thm = thm 55 |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq 56 |> apply2 (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp) 57 |> mk_Trueprop_eq 58 |> (fn goal => Goal.prove_sorry ctxt [] [] goal 59 (K (rtac ctxt ext 1 THEN 60 unfold_thms_tac ctxt ([o_apply, unfold_thms ctxt [o_apply] (mk_sym thm)]) THEN 61 rtac ctxt refl 1))) 62 |> Thm.close_derivation \<^here>; 63 64 65(* Theorems for open typedefs with UNIV as representing set *) 66 67fun mk_Abs_inj_thm inj = inj OF (replicate 2 @{thm UNIV_I}); 68fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac ctxt surj THEN' etac ctxt exI) 1) 69 (Abs_inj_thm RS @{thm bijI'}); 70 71 72(* General tactic generators *) 73 74(*applies assoc rule to the lhs of an equation as long as possible*) 75fun mk_flatten_assoc_tac ctxt refl_tac trans assoc cong = rtac ctxt trans 1 THEN 76 REPEAT_DETERM (CHANGED ((FIRST' [rtac ctxt trans THEN' rtac ctxt assoc, rtac ctxt cong THEN' refl_tac]) 1)) THEN 77 refl_tac 1; 78 79(*proves two sides of an equation to be equal assuming both are flattened and rhs can be obtained 80from lhs by the given permutation of monoms*) 81fun mk_rotate_eq_tac ctxt refl_tac trans assoc com cong = 82 let 83 fun gen_tac [] [] = K all_tac 84 | gen_tac [x] [y] = if x = y then refl_tac else error "mk_rotate_eq_tac: different lists" 85 | gen_tac (x :: xs) (y :: ys) = if x = y 86 then rtac ctxt cong THEN' refl_tac THEN' gen_tac xs ys 87 else rtac ctxt trans THEN' rtac ctxt com THEN' 88 K (mk_flatten_assoc_tac ctxt refl_tac trans assoc cong) THEN' 89 gen_tac (xs @ [x]) (y :: ys) 90 | gen_tac _ _ = error "mk_rotate_eq_tac: different lists"; 91 in 92 gen_tac 93 end; 94 95fun mk_map_comp_id_tac ctxt map_comp0 = 96 (rtac ctxt trans THEN' rtac ctxt map_comp0 THEN' K (unfold_thms_tac ctxt @{thms comp_id}) THEN' rtac ctxt refl) 1; 97 98fun mk_map_cong0_tac ctxt m map_cong0 = 99 EVERY' [rtac ctxt mp, rtac ctxt map_cong0, 100 CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; 101 102fun mk_map_cong0L_tac ctxt passive map_cong0 map_id = 103 (rtac ctxt trans THEN' rtac ctxt map_cong0 THEN' EVERY' (replicate passive (rtac ctxt refl))) 1 THEN 104 REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt @{thm bspec}, assume_tac ctxt, 105 rtac ctxt sym, rtac ctxt @{thm id_apply}] 1) THEN 106 rtac ctxt map_id 1; 107 108end; 109