src/CTT/rew.ML
author wenzelm
Wed, 22 Apr 2020 19:22:43 +0200
changeset 71787 acfe72ff00c2
parent 59498 50b60f501b05
permissions -rw-r--r--
merged
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
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17496
diff changeset
     5
Simplifier for CTT, using Typedsimp.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
(*Make list of ProdE RS ProdE ... RS ProdE RS EqE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
  for using assumptions as rewrite rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
fun peEs 0 = []
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 35762
diff changeset
    11
  | peEs n = @{thm EqE} :: map (curry (op RS) @{thm ProdE}) (peEs (n-1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
(*Tactic used for proving conditions for the cond_rls*)
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58963
diff changeset
    14
fun prove_cond_tac ctxt = eresolve_tac ctxt (peEs 5);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
structure TSimp_data: TSIMP_DATA =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  struct
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 35762
diff changeset
    19
  val refl              = @{thm refl_elem}
0dec18004e75 more antiquotations;
wenzelm
parents: 35762
diff changeset
    20
  val sym               = @{thm sym_elem}
0dec18004e75 more antiquotations;
wenzelm
parents: 35762
diff changeset
    21
  val trans             = @{thm trans_elem}
0dec18004e75 more antiquotations;
wenzelm
parents: 35762
diff changeset
    22
  val refl_red          = @{thm refl_red}
0dec18004e75 more antiquotations;
wenzelm
parents: 35762
diff changeset
    23
  val trans_red         = @{thm trans_red}
0dec18004e75 more antiquotations;
wenzelm
parents: 35762
diff changeset
    24
  val red_if_equal      = @{thm red_if_equal}
0dec18004e75 more antiquotations;
wenzelm
parents: 35762
diff changeset
    25
  val default_rls       = @{thms comp_rls}
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 39159
diff changeset
    26
  val routine_tac       = routine_tac @{thms routine_rls}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
structure TSimp = TSimpFun (TSimp_data);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 35762
diff changeset
    31
val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
(*Make a rewriting tactic from a normalization tactic*)
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 39159
diff changeset
    34
fun make_rew_tac ctxt ntac =
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58963
diff changeset
    35
    TRY (eqintr_tac ctxt)  THEN  TRYALL (resolve_tac ctxt [TSimp.split_eqn])  THEN  
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
    ntac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 39159
diff changeset
    38
fun rew_tac ctxt thms = make_rew_tac ctxt
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 39159
diff changeset
    39
    (TSimp.norm_tac ctxt (standard_congr_rls, thms));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 39159
diff changeset
    41
fun hyp_rew_tac ctxt thms = make_rew_tac ctxt
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58963
diff changeset
    42
    (TSimp.cond_norm_tac ctxt (prove_cond_tac ctxt, standard_congr_rls, thms));