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