Theory MyTactics

section ‹Some tactics›

(* author: Andrei Popescu *)

theory MyTactics imports Main 
begin 

(* ML {* clarsimp_tac *}


ML{* val x = [1] @ [2] *}

ML {* simp_tac *}  *)


ML‹
val impI = @{thm impI}  
val allI = @{thm allI} 
val ballI = @{thm ballI}
val conjE = @{thm conjE}
val conjI = @{thm conjI}
val exE = @{thm exE}
val disjE = @{thm disjE}


fun mclarTacs ctxt i =
  [resolve_tac ctxt [impI] i,
   resolve_tac ctxt [allI] i,
   resolve_tac ctxt [ballI] i,
   eresolve_tac ctxt [conjE] i,
   eresolve_tac ctxt [exE] i];

fun mclarify_all_tac ctxt = REPEAT(SOMEGOAL(fn i => FIRST (mclarTacs ctxt i)));
fun mclarsimp_all_tac ctxt = TRY (mclarify_all_tac ctxt) THEN TRYALL (asm_full_simp_tac ctxt)

fun mautoTacs ctxt i = mclarTacs ctxt i @ [resolve_tac ctxt [conjI] i, eresolve_tac ctxt [disjE] i]
fun mauto_no_simp_tac ctxt = REPEAT(SOMEGOAL(fn i => FIRST (mautoTacs ctxt i)))

fun clarify_all_tac ctxt = TRYALL (clarify_tac ctxt)
›

text‹Above, "m" stands for "mild" -- mainly, disjunctions are left untouched.›




(* Note: The variables @{simpset} and @{claset} are *statically bound*, 
hence they refer to the contents of the simp and classical databases at this 
definition time.  For the classical database, this is OK for my purpose, 
since all I care is that it includes HOL_cs.  However, for the simp database 
I shall need to use the current version each time, since the database changes 
continuously with simpliication rules for the newly defined concepts -- thereore 
I shall need to pass that current version as an explicit parameter, which will 
typically be (the current value of) @{simpset}.  *)



(*  Tests: 
lemma "(∀ i j k. P ⟶ (Q1 ∨ Q2  ∧ [] @ L = L)) ∧ (∀ a b. G a ∧ G b ⟶ Q) ∧ D"
apply(tactic {* REPEAT(SOMEGOAL(rtac @{thm conjI})) *})
apply(tactic {* mclarify_all_tac *})
oops


lemma "V ∧ (∀ i j k. P ⟶ (Q1 ∨ Q2 ∧ [] @ L = L)) ∧ (∀ a b. G a ∧ G b ⟶ Q) ∧ D"
apply(tactic {* REPEAT(SOMEGOAL(rtac @{thm conjI})) *})
apply(tactic {* mclarsimp_all_tac @{simpset}*})
oops


lemma "V ∧ (∀ i j k. P ⟶ (Q1 ∨ Q2)) ∧ (∀ a b. G a ∧ G b ⟶ Q) ∧ D"
apply(tactic {* REPEAT(SOMEGOAL(rtac @{thm conjI})) *})
apply(tactic {* clarify_all_tac *})
apply(rule disjE)
oops


lemma "V ∧ (∀ i j k. P ⟶ (Q1 ∨ Q2 ∧ x = x)) ∧ (∀ a b. G a ∧ G b ⟶ Q) ∧ D"
apply(tactic {* REPEAT(SOMEGOAL(rtac @{thm conjI})) *})
apply(tactic {* clarsimp_all_tac @{simpset} *})
oops


lemma "(∀ i j k. P ⟶ Q) ∧ (∀ a b. G a ∧ G b ⟶ (Q ∧ R)) ∧ D"
apply(tactic {* REPEAT(SOMEGOAL(rtac @{thm conjI})) *})
apply(tactic {* mauto_no_simp_tac @{context} *})
oops


lemma test: "(∀ i j k. P ⟶ Q) ∧ (∀ a b. G a ∧ G b ⟶ Q)"
apply(tactic {* mauto_no_simp_tac @{context} *})
apply(rule disjE)
oops

*)


end