author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 39159 0dec18004e75
child 58963 26bf09b95dda
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);

(*  Title:      CTT/rew.ML
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Simplifier for CTT, using Typedsimp.

(*Make list of ProdE RS ProdE ... RS ProdE RS EqE
  for using assumptions as rewrite rules*)
fun peEs 0 = []
  | peEs n = @{thm EqE} :: map (curry (op RS) @{thm ProdE}) (peEs (n-1));

(*Tactic used for proving conditions for the cond_rls*)
val prove_cond_tac = eresolve_tac (peEs 5);

structure TSimp_data: TSIMP_DATA =
  val refl              = @{thm refl_elem}
  val sym               = @{thm sym_elem}
  val trans             = @{thm trans_elem}
  val refl_red          = @{thm refl_red}
  val trans_red         = @{thm trans_red}
  val red_if_equal      = @{thm red_if_equal}
  val default_rls       = @{thms comp_rls}
  val routine_tac       = routine_tac (@{thms routine_rls})

structure TSimp = TSimpFun (TSimp_data);

val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls};

(*Make a rewriting tactic from a normalization tactic*)
fun make_rew_tac ntac =
    TRY eqintr_tac  THEN  TRYALL (resolve_tac [TSimp.split_eqn])  THEN  

fun rew_tac thms = make_rew_tac
    (TSimp.norm_tac(standard_congr_rls, thms));

fun hyp_rew_tac thms = make_rew_tac
    (TSimp.cond_norm_tac(prove_cond_tac, standard_congr_rls, thms));