src/FOLP/simpdata.ML
author wenzelm
Sat, 28 Jun 2008 22:52:03 +0200
changeset 27388 226835ea8d2b
parent 26322 eaf634e975fa
child 35762 af3ff2ba4c54
permissions -rw-r--r--
added ML/ml_thms.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1463
49ca5e875691 expanded tabs
clasohm
parents: 1459
diff changeset
     1
(*  Title:      FOLP/simpdata.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
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
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 17325
diff changeset
     6
Simplification data for FOLP.
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
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    10
fun make_iff_T th = th RS @{thm P_Imp_P_iff_T};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    12
val refl_iff_T = make_iff_T @{thm refl};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    14
val norm_thms = [(@{thm norm_eq} RS @{thm sym}, @{thm norm_eq}),
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    15
                 (@{thm NORM_iff} RS @{thm iff_sym}, @{thm NORM_iff})];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
(* Conversion into rewrite rules *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
fun mk_eq th = case concl_of th of
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    21
      _ $ (Const (@{const_name "op <->"}, _) $ _ $ _) $ _ => th
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    22
    | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) $ _ => th
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    23
    | _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
    | _ => make_iff_T th;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
5304
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    26
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    27
val mksimps_pairs =
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    28
  [(@{const_name "op -->"}, [@{thm mp}]),
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    29
   (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    30
   (@{const_name "All"}, [@{thm spec}]),
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    31
   (@{const_name True}, []),
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    32
   (@{const_name False}, [])];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
5304
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    34
fun mk_atomize pairs =
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    35
  let fun atoms th =
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    36
        (case concl_of th of
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    37
           Const ("Trueprop", _) $ p =>
5304
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    38
             (case head_of p of
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    39
                Const(a,_) =>
17325
d9d50222808e introduced new-style AList operations
haftmann
parents: 15570
diff changeset
    40
                  (case AList.lookup (op =) pairs a of
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    41
                     SOME(rls) => maps atoms ([th] RL rls)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 5304
diff changeset
    42
                   | NONE => [th])
5304
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    43
              | _ => [th])
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    44
         | _ => [th])
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    45
  in atoms end;
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    46
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    47
fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
(*destruct function for analysing equations*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    51
  | dest_red t = raise TERM("dest_red", [t]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
structure FOLP_SimpData : SIMP_DATA =
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    54
struct
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    55
  val refl_thms         = [@{thm refl}, @{thm iff_refl}]
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    56
  val trans_thms        = [@{thm trans}, @{thm iff_trans}]
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    57
  val red1              = @{thm iffD1}
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    58
  val red2              = @{thm iffD2}
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    59
  val mk_rew_rules      = mk_rew_rules
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    60
  val case_splits       = []         (*NO IF'S!*)
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    61
  val norm_thms         = norm_thms
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    62
  val subst_thms        = [@{thm subst}];
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    63
  val dest_red          = dest_red
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    64
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
structure FOLP_Simp = SimpFun(FOLP_SimpData);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
(*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 17325
diff changeset
    69
val FOLP_congs =
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    70
   [@{thm all_cong}, @{thm ex_cong}, @{thm eq_cong},
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    71
    @{thm conj_cong}, @{thm disj_cong}, @{thm imp_cong},
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    72
    @{thm iff_cong}, @{thm not_cong}] @ @{thms pred_congs};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
val IFOLP_rews =
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    75
   [refl_iff_T] @ @{thms conj_rews} @ @{thms disj_rews} @ @{thms not_rews} @
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    76
    @{thms imp_rews} @ @{thms iff_rews} @ @{thms quant_rews};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
1009
eb7c50688405 No longer builds the induction structure (from ../Provers/ind.ML)
lcp
parents: 0
diff changeset
    78
open FOLP_Simp;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    80
val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
26322
eaf634e975fa converted legacy ML scripts;
wenzelm
parents: 17480
diff changeset
    85
val FOLP_rews = IFOLP_rews @ @{thms cla_rews};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;