src/HOL/Nominal/nominal_thmdecls.ML
author wenzelm
Thu Jun 26 15:06:25 2008 +0200 (2008-06-26)
changeset 27370 8e8f96dfaf63
parent 26928 ca87aff1ad2d
child 29585 c23295521af5
permissions -rw-r--r--
Args.context;
urbanc@22245
     1
(* ID: "$Id$"
urbanc@22245
     2
   Authors: Julien Narboux and Christian Urban
urbanc@22245
     3
wenzelm@22846
     4
   This file introduces the infrastructure for the lemma
narboux@22562
     5
   declaration "eqvts" "bijs" and "freshs".
urbanc@22245
     6
wenzelm@22846
     7
   By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
urbanc@24571
     8
   in a data-slot in the context. Possible modifiers
urbanc@22245
     9
   are [attribute add] and [attribute del] for adding and deleting,
wenzelm@22846
    10
   respectively the lemma from the data-slot.
urbanc@22245
    11
*)
urbanc@22245
    12
urbanc@22245
    13
signature NOMINAL_THMDECLS =
urbanc@22245
    14
sig
urbanc@22245
    15
  val eqvt_add: attribute
urbanc@22245
    16
  val eqvt_del: attribute
urbanc@22715
    17
  val eqvt_force_add: attribute
urbanc@22715
    18
  val eqvt_force_del: attribute
urbanc@22245
    19
  val setup: theory -> theory
urbanc@24571
    20
  val get_eqvt_thms: Proof.context -> thm list
urbanc@24571
    21
  val get_fresh_thms: Proof.context -> thm list
urbanc@24571
    22
  val get_bij_thms: Proof.context -> thm list
wenzelm@22846
    23
urbanc@22245
    24
urbanc@22245
    25
  val NOMINAL_EQVT_DEBUG : bool ref
urbanc@22245
    26
end;
urbanc@22245
    27
urbanc@22245
    28
structure NominalThmDecls: NOMINAL_THMDECLS =
urbanc@22245
    29
struct
urbanc@22245
    30
urbanc@22245
    31
structure Data = GenericDataFun
urbanc@22245
    32
(
narboux@22562
    33
  type T = {eqvts:thm list, freshs:thm list, bijs:thm list};
narboux@22562
    34
  val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
urbanc@22245
    35
  val extend = I;
wenzelm@24039
    36
  fun merge _ (r1:T,r2:T) = {eqvts  = Thm.merge_thms (#eqvts r1, #eqvts r2),
wenzelm@24039
    37
                             freshs = Thm.merge_thms (#freshs r1, #freshs r2),
wenzelm@24039
    38
                             bijs   = Thm.merge_thms (#bijs r1, #bijs r2)}
urbanc@22245
    39
);
urbanc@22245
    40
urbanc@22245
    41
(* Exception for when a theorem does not conform with form of an equivariance lemma. *)
urbanc@22245
    42
(* There are two forms: one is an implication (for relations) and the other is an    *)
urbanc@22245
    43
(* equality (for functions). In the implication-case, say P ==> Q, Q must be equal   *)
urbanc@22245
    44
(* to P except that every free variable of Q, say x, is replaced by pi o x. In the   *)
urbanc@22245
    45
(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *)
urbanc@22245
    46
(* be equal to t except that every free variable, say x, is replaced by pi o x. In   *)
urbanc@22245
    47
(* the implicational case it is also checked that the variables and permutation fit  *)
urbanc@22245
    48
(* together, i.e. are of the right "pt_class", so that a stronger version of the     *)
narboux@24265
    49
(* equality-lemma can be derived. *)
urbanc@22418
    50
exception EQVT_FORM of string;
urbanc@22245
    51
urbanc@24571
    52
val get_eqvt_thms = Context.Proof #> Data.get #> #eqvts;
urbanc@24571
    53
val get_fresh_thms = Context.Proof #> Data.get #> #freshs;
urbanc@24571
    54
val get_bij_thms = Context.Proof #> Data.get #> #bijs;
urbanc@22245
    55
urbanc@22245
    56
(* FIXME: should be a function in a library *)
urbanc@22245
    57
fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
urbanc@22245
    58
urbanc@22245
    59
val NOMINAL_EQVT_DEBUG = ref false;
urbanc@22245
    60
wenzelm@22846
    61
fun tactic (msg,tac) =
wenzelm@22846
    62
    if !NOMINAL_EQVT_DEBUG
wenzelm@26652
    63
    then tac THEN print_tac ("after "^msg)
wenzelm@22846
    64
    else tac
urbanc@22245
    65
wenzelm@22846
    66
fun tactic_eqvt ctx orig_thm pi typi =
wenzelm@22846
    67
    let
urbanc@22245
    68
        val mypi = Thm.cterm_of ctx (Var (pi,typi))
urbanc@22245
    69
        val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
wenzelm@26343
    70
        val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
urbanc@22245
    71
    in
wenzelm@22846
    72
        EVERY [tactic ("iffI applied",rtac iffI 1),
urbanc@24571
    73
	       tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)),
urbanc@24571
    74
               tactic ("solve with orig_thm", (etac orig_thm 1)),
urbanc@22245
    75
               tactic ("applies orig_thm instantiated with rev pi",
wenzelm@22846
    76
                          dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
narboux@24265
    77
	       tactic ("getting rid of the pi on the right",
urbanc@24571
    78
                          (rtac @{thm perm_boolI} 1)),
urbanc@22245
    79
               tactic ("getting rid of all remaining perms",
narboux@24265
    80
                          full_simp_tac (HOL_basic_ss addsimps perm_pi_simp) 1)]
urbanc@22245
    81
    end;
urbanc@22245
    82
urbanc@22245
    83
fun get_derived_thm thy hyp concl orig_thm pi typi =
wenzelm@22846
    84
   let
urbanc@22245
    85
       val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
wenzelm@22846
    86
       val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
wenzelm@22846
    87
       val _ = Display.print_cterm (cterm_of thy goal_term)
wenzelm@24039
    88
   in
wenzelm@22846
    89
     Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
urbanc@22245
    90
   end
urbanc@22245
    91
wenzelm@22846
    92
(* replaces every variable x in t with pi o x *)
urbanc@22245
    93
fun apply_pi trm (pi,typi) =
wenzelm@22846
    94
  let
urbanc@22245
    95
    fun only_vars t =
urbanc@22245
    96
       (case t of
urbanc@22245
    97
          Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty)))
urbanc@22245
    98
        | _ => t)
wenzelm@22846
    99
  in
wenzelm@22846
   100
     map_aterms only_vars trm
urbanc@22245
   101
  end;
urbanc@22245
   102
urbanc@22245
   103
(* returns *the* pi which is in front of all variables, provided there *)
urbanc@22245
   104
(* exists such a pi; otherwise raises EQVT_FORM                        *)
urbanc@22245
   105
fun get_pi t thy =
urbanc@22245
   106
  let fun get_pi_aux s =
urbanc@22245
   107
        (case s of
wenzelm@22846
   108
          (Const ("Nominal.perm",typrm) $
wenzelm@22846
   109
             (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
wenzelm@22846
   110
               (Var (n,ty))) =>
urbanc@22245
   111
             let
wenzelm@24039
   112
                (* FIXME: this should be an operation the library *)
wenzelm@22846
   113
                val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
wenzelm@24039
   114
             in
wenzelm@24271
   115
                if (Sign.of_sort thy (ty,[class_name]))
wenzelm@22846
   116
                then [(pi,typi)]
wenzelm@22846
   117
                else raise
wenzelm@22846
   118
                EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
wenzelm@22846
   119
             end
urbanc@22245
   120
        | Abs (_,_,t1) => get_pi_aux t1
urbanc@22245
   121
        | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
wenzelm@22846
   122
        | _ => [])
wenzelm@22846
   123
  in
urbanc@22245
   124
    (* collect first all pi's in front of variables in t and then use distinct *)
urbanc@22245
   125
    (* to ensure that all pi's must have been the same, i.e. distinct returns  *)
urbanc@22245
   126
    (* a singleton-list  *)
wenzelm@22846
   127
    (case (distinct (op =) (get_pi_aux t)) of
urbanc@22245
   128
      [(pi,typi)] => (pi,typi)
urbanc@22418
   129
    | _ => raise EQVT_FORM "All permutation should be the same")
urbanc@22245
   130
  end;
urbanc@22245
   131
wenzelm@26652
   132
(* Either adds a theorem (orig_thm) to or deletes one from the equivariance *)
urbanc@22245
   133
(* lemma list depending on flag. To be added the lemma has to satisfy a     *)
wenzelm@22846
   134
(* certain form. *)
narboux@24265
   135
narboux@24265
   136
fun eqvt_add_del_aux flag orig_thm context = 
wenzelm@22846
   137
  let
urbanc@22245
   138
    val thy = Context.theory_of context
urbanc@22245
   139
    val thms_to_be_added = (case (prop_of orig_thm) of
wenzelm@22846
   140
        (* case: eqvt-lemma is of the implicational form *)
urbanc@22245
   141
        (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
wenzelm@22846
   142
          let
urbanc@22245
   143
            val (pi,typi) = get_pi concl thy
urbanc@22245
   144
          in
urbanc@22245
   145
             if (apply_pi hyp (pi,typi) = concl)
wenzelm@22846
   146
             then
urbanc@22245
   147
               (warning ("equivariance lemma of the relational form");
urbanc@22245
   148
                [orig_thm, get_derived_thm thy hyp concl orig_thm pi typi])
urbanc@22418
   149
             else raise EQVT_FORM "Type Implication"
urbanc@22245
   150
          end
wenzelm@22846
   151
       (* case: eqvt-lemma is of the equational form *)
wenzelm@22846
   152
      | (Const ("Trueprop", _) $ (Const ("op =", _) $
urbanc@22418
   153
            (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
wenzelm@24039
   154
           (if (apply_pi lhs (pi,typi)) = rhs
narboux@22437
   155
               then [orig_thm]
urbanc@22418
   156
               else raise EQVT_FORM "Type Equality")
urbanc@22418
   157
      | _ => raise EQVT_FORM "Type unknown")
wenzelm@22846
   158
  in
wenzelm@26652
   159
      fold (fn thm => Data.map (flag thm)) thms_to_be_added context
urbanc@22245
   160
  end
wenzelm@22846
   161
  handle EQVT_FORM s =>
wenzelm@26928
   162
      error (Display.string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
urbanc@22245
   163
urbanc@22245
   164
(* in cases of bij- and freshness, we just add the lemmas to the *)
wenzelm@22846
   165
(* data-slot *)
urbanc@22245
   166
wenzelm@26652
   167
fun eqvt_map f (r:Data.T)  = {eqvts = f (#eqvts r), freshs = #freshs r, bijs = #bijs r};
wenzelm@26652
   168
fun fresh_map f (r:Data.T) = {eqvts = #eqvts r, freshs = f (#freshs r), bijs = #bijs r};
wenzelm@26652
   169
fun bij_map f (r:Data.T)   = {eqvts = #eqvts r, freshs = #freshs r, bijs = f (#bijs r)};
urbanc@22245
   170
wenzelm@26652
   171
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.add_thm));
wenzelm@26652
   172
val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.del_thm));
urbanc@22245
   173
wenzelm@26652
   174
val eqvt_force_add  = Thm.declaration_attribute (Data.map o eqvt_map o Thm.add_thm);
wenzelm@26652
   175
val eqvt_force_del  = Thm.declaration_attribute (Data.map o eqvt_map o Thm.del_thm);
wenzelm@26652
   176
val bij_add   = Thm.declaration_attribute (Data.map o bij_map o Thm.add_thm);
wenzelm@26652
   177
val bij_del   = Thm.declaration_attribute (Data.map o bij_map o Thm.del_thm);
wenzelm@26652
   178
val fresh_add = Thm.declaration_attribute (Data.map o fresh_map o Thm.add_thm);
wenzelm@26652
   179
val fresh_del = Thm.declaration_attribute (Data.map o fresh_map o Thm.del_thm);
urbanc@22245
   180
urbanc@22715
   181
urbanc@22418
   182
urbanc@22245
   183
val setup =
wenzelm@22846
   184
  Attrib.add_attributes
urbanc@22245
   185
     [("eqvt",  Attrib.add_del_args eqvt_add eqvt_del,   "equivariance theorem declaration"),
urbanc@22715
   186
      ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
wenzelm@24039
   187
        "equivariance theorem declaration (without checking the form of the lemma)"),
urbanc@22245
   188
      ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
wenzelm@26400
   189
      ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")] #>
wenzelm@26400
   190
  PureThy.add_thms_dynamic ("eqvts", #eqvts o Data.get) #>
wenzelm@26400
   191
  PureThy.add_thms_dynamic ("freshs", #freshs o Data.get) #>
wenzelm@26400
   192
  PureThy.add_thms_dynamic ("bijs", #bijs o Data.get);
urbanc@22245
   193
urbanc@22245
   194
end;