src/CTT/rew.ML
author wenzelm
Wed, 15 Apr 2009 11:14:48 +0200
changeset 30895 bad26d8f0adf
parent 19761 5cd82054c2c6
child 35762 af3ff2ba4c54
permissions -rw-r--r--
updated for Isabelle2009;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
     1
(*  Title:      CTT/rew.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
     6
Simplifier for CTT, using Typedsimp.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
(*Make list of ProdE RS ProdE ... RS ProdE RS EqE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
  for using assumptions as rewrite rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
fun peEs 0 = []
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
    12
  | peEs n = thm "EqE" :: map (curry (op RS) (thm "ProdE")) (peEs (n-1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
(*Tactic used for proving conditions for the cond_rls*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
val prove_cond_tac = eresolve_tac (peEs 5);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
structure TSimp_data: TSIMP_DATA =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  struct
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
    20
  val refl              = thm "refl_elem"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
    21
  val sym               = thm "sym_elem"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
    22
  val trans             = thm "trans_elem"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
    23
  val refl_red          = thm "refl_red"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
    24
  val trans_red         = thm "trans_red"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
    25
  val red_if_equal      = thm "red_if_equal"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
    26
  val default_rls       = thms "comp_rls"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
    27
  val routine_tac       = routine_tac (thms "routine_rls")
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
structure TSimp = TSimpFun (TSimp_data);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
    32
val standard_congr_rls = thms "intrL2_rls" @ thms "elimL_rls";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
(*Make a rewriting tactic from a normalization tactic*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
fun make_rew_tac ntac =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
    TRY eqintr_tac  THEN  TRYALL (resolve_tac [TSimp.split_eqn])  THEN  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
    ntac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
fun rew_tac thms = make_rew_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
    (TSimp.norm_tac(standard_congr_rls, thms));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
fun hyp_rew_tac thms = make_rew_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
    (TSimp.cond_norm_tac(prove_cond_tac, standard_congr_rls, thms));