src/HOL/Tools/reflection.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 53171 a5e54d4d9081
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned;
wenzelm@52406
     1
(*  Title:      HOL/Tools/reflection.ML
haftmann@51726
     2
    Author:     Amine Chaieb, TU Muenchen
haftmann@51726
     3
wenzelm@52406
     4
A trial for automatical reflection with user-space declarations.
haftmann@51726
     5
*)
haftmann@51726
     6
wenzelm@52406
     7
signature REFLECTION =
haftmann@51726
     8
sig
wenzelm@52406
     9
  val reflect: Proof.context -> thm list -> thm list -> conv
wenzelm@52406
    10
  val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
wenzelm@52406
    11
  val reflect_with_eval: Proof.context -> thm list -> thm list -> conv -> conv
wenzelm@52406
    12
  val reflection_with_eval_tac: Proof.context -> thm list -> thm list -> conv -> term option -> int -> tactic
wenzelm@52406
    13
  val get_default: Proof.context -> { reification_eqs: thm list, correctness_thms: thm list }
wenzelm@52406
    14
  val add_reification_eq: attribute
wenzelm@52406
    15
  val del_reification_eq: attribute
wenzelm@52406
    16
  val add_correctness_thm: attribute
wenzelm@52406
    17
  val del_correctness_thm: attribute
wenzelm@52406
    18
  val default_reify_tac: Proof.context -> thm list -> term option -> int -> tactic
wenzelm@52406
    19
  val default_reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
haftmann@51726
    20
end;
haftmann@51726
    21
wenzelm@52406
    22
structure Reflection : REFLECTION =
haftmann@51726
    23
struct
haftmann@51726
    24
wenzelm@52406
    25
fun subst_correctness corr_thms ct =
wenzelm@52406
    26
  Conv.rewrs_conv (map (Thm.symmetric o mk_eq) corr_thms) ct
wenzelm@52406
    27
    handle CTERM _ => error "No suitable correctness theorem found";
haftmann@51726
    28
wenzelm@52406
    29
fun reflect ctxt corr_thms eqs =
wenzelm@52406
    30
  (Reification.conv ctxt eqs) then_conv (subst_correctness corr_thms)
haftmann@51726
    31
wenzelm@52406
    32
fun reflection_tac ctxt corr_thms eqs =
wenzelm@52406
    33
  Reification.lift_conv ctxt (reflect ctxt corr_thms eqs);
haftmann@52275
    34
wenzelm@52406
    35
fun first_arg_conv conv =
haftmann@51726
    36
  let
wenzelm@52406
    37
    fun conv' ct =
wenzelm@52406
    38
      if can Thm.dest_comb (fst (Thm.dest_comb ct))
wenzelm@52406
    39
      then Conv.combination_conv conv' Conv.all_conv ct
wenzelm@52406
    40
      else Conv.combination_conv Conv.all_conv conv ct;
wenzelm@52406
    41
  in conv' end;
wenzelm@52406
    42
wenzelm@52406
    43
fun reflect_with_eval ctxt corr_thms eqs conv =
wenzelm@52406
    44
  (reflect ctxt corr_thms eqs) then_conv (first_arg_conv conv) then_conv (Reification.dereify ctxt eqs);
wenzelm@52406
    45
wenzelm@52406
    46
fun reflection_with_eval_tac ctxt corr_thms eqs conv =
wenzelm@52406
    47
  Reification.lift_conv ctxt (reflect_with_eval ctxt corr_thms eqs conv);
haftmann@52288
    48
wenzelm@52406
    49
structure Data = Generic_Data
wenzelm@52406
    50
(
wenzelm@52406
    51
  type T = thm list * thm list;
wenzelm@52406
    52
  val empty = ([], []);
wenzelm@52406
    53
  val extend = I;
wenzelm@52406
    54
  fun merge ((ths1, rths1), (ths2, rths2)) =
wenzelm@52406
    55
    (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
wenzelm@52406
    56
);
wenzelm@52406
    57
wenzelm@52406
    58
fun get_default ctxt =
wenzelm@52406
    59
  let
wenzelm@52406
    60
    val (reification_eqs, correctness_thms) = Data.get (Context.Proof ctxt);
wenzelm@52406
    61
  in { reification_eqs = reification_eqs, correctness_thms = correctness_thms } end;
haftmann@52288
    62
wenzelm@52406
    63
val add_reification_eq = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
wenzelm@52406
    64
val del_reification_eq = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
wenzelm@52406
    65
val add_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
wenzelm@52406
    66
val del_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
haftmann@52288
    67
wenzelm@53171
    68
val _ = Theory.setup
wenzelm@52406
    69
  (Attrib.setup @{binding reify}
wenzelm@53171
    70
    (Attrib.add_del add_reification_eq del_reification_eq)
wenzelm@53171
    71
    "declare reification equations" #>
wenzelm@53171
    72
   Attrib.setup @{binding reflection}
wenzelm@53171
    73
    (Attrib.add_del add_correctness_thm del_correctness_thm)
wenzelm@53171
    74
    "declare reflection correctness theorems");
haftmann@51726
    75
wenzelm@52406
    76
fun default_reify_tac ctxt user_eqs =
haftmann@52288
    77
  let
wenzelm@52406
    78
    val { reification_eqs = default_eqs, correctness_thms = _ } =
wenzelm@52406
    79
      get_default ctxt;
wenzelm@52406
    80
    val eqs = fold Thm.add_thm user_eqs default_eqs;
wenzelm@52406
    81
  in Reification.tac ctxt eqs end;
haftmann@52288
    82
wenzelm@52406
    83
fun default_reflection_tac ctxt user_thms user_eqs =
haftmann@52288
    84
  let
wenzelm@52406
    85
    val { reification_eqs = default_eqs, correctness_thms = default_thms } =
wenzelm@52406
    86
      get_default ctxt;
wenzelm@52406
    87
    val corr_thms = fold Thm.add_thm user_thms default_thms;
wenzelm@52406
    88
    val eqs = fold Thm.add_thm user_eqs default_eqs; 
wenzelm@52406
    89
  in reflection_tac ctxt corr_thms eqs end;
haftmann@51726
    90
haftmann@52276
    91
end;