src/HOL/Nominal/nominal_thmdecls.ML
author wenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 56245 84fc7dfa3cd4
parent 54990 8dc8d427b313
child 56491 a8ccf3d6a6e4
permissions -rw-r--r--
more qualified names;
wenzelm@32960
     1
(*  Title:      HOL/Nominal/nominal_thmdecls.ML
wenzelm@32960
     2
    Author:     Julien Narboux, TU Muenchen
wenzelm@32960
     3
    Author:     Christian Urban, TU Muenchen
urbanc@22245
     4
wenzelm@32960
     5
Infrastructure for the lemma collection "eqvts".
wenzelm@32960
     6
wenzelm@32960
     7
By attaching [eqvt] or [eqvt_force] to a lemma, it will get stored in
wenzelm@32960
     8
a data-slot in the context. Possible modifiers are [... add] and
wenzelm@32960
     9
[... del] for adding and deleting, respectively, the lemma from the
wenzelm@32960
    10
data-slot.
urbanc@22245
    11
*)
urbanc@22245
    12
urbanc@22245
    13
signature NOMINAL_THMDECLS =
urbanc@22245
    14
sig
wenzelm@54990
    15
  val nominal_eqvt_debug: bool Config.T
urbanc@22245
    16
  val eqvt_add: attribute
urbanc@22245
    17
  val eqvt_del: attribute
urbanc@22715
    18
  val eqvt_force_add: attribute
urbanc@22715
    19
  val eqvt_force_del: attribute
urbanc@22245
    20
  val setup: theory -> theory
urbanc@24571
    21
  val get_eqvt_thms: Proof.context -> thm list
urbanc@22245
    22
end;
urbanc@22245
    23
urbanc@22245
    24
structure NominalThmDecls: NOMINAL_THMDECLS =
urbanc@22245
    25
struct
urbanc@22245
    26
wenzelm@33519
    27
structure Data = Generic_Data
urbanc@22245
    28
(
urbanc@30986
    29
  type T = thm list
wenzelm@33519
    30
  val empty = []
urbanc@30986
    31
  val extend = I
wenzelm@33519
    32
  val merge = Thm.merge_thms
urbanc@30986
    33
)
urbanc@22245
    34
urbanc@22245
    35
(* Exception for when a theorem does not conform with form of an equivariance lemma. *)
urbanc@22245
    36
(* There are two forms: one is an implication (for relations) and the other is an    *)
urbanc@22245
    37
(* equality (for functions). In the implication-case, say P ==> Q, Q must be equal   *)
urbanc@22245
    38
(* to P except that every free variable of Q, say x, is replaced by pi o x. In the   *)
urbanc@22245
    39
(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *)
urbanc@22245
    40
(* be equal to t except that every free variable, say x, is replaced by pi o x. In   *)
urbanc@22245
    41
(* the implicational case it is also checked that the variables and permutation fit  *)
urbanc@22245
    42
(* together, i.e. are of the right "pt_class", so that a stronger version of the     *)
narboux@24265
    43
(* equality-lemma can be derived. *)
urbanc@30986
    44
exception EQVT_FORM of string
urbanc@22245
    45
wenzelm@42616
    46
val nominal_eqvt_debug = Attrib.setup_config_bool @{binding nominal_eqvt_debug} (K false);
urbanc@22245
    47
wenzelm@38807
    48
fun tactic ctxt (msg, tac) =
wenzelm@38807
    49
  if Config.get ctxt nominal_eqvt_debug
urbanc@30986
    50
  then tac THEN' (K (print_tac ("after " ^ msg)))
urbanc@30986
    51
  else tac
urbanc@22245
    52
urbanc@30991
    53
fun prove_eqvt_tac ctxt orig_thm pi pi' =
wenzelm@38807
    54
  let
wenzelm@42361
    55
    val thy = Proof_Context.theory_of ctxt
wenzelm@38807
    56
    val mypi = Thm.cterm_of thy pi
wenzelm@38807
    57
    val T = fastype_of pi'
wenzelm@38807
    58
    val mypifree = Thm.cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi')
wenzelm@39557
    59
    val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"
wenzelm@38807
    60
  in
wenzelm@38807
    61
    EVERY1 [tactic ctxt ("iffI applied", rtac @{thm iffI}),
wenzelm@38807
    62
            tactic ctxt ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
wenzelm@38807
    63
            tactic ctxt ("solve with orig_thm", etac orig_thm),
wenzelm@38807
    64
            tactic ctxt ("applies orig_thm instantiated with rev pi",
wenzelm@38807
    65
                       dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
wenzelm@38807
    66
            tactic ctxt ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
wenzelm@38807
    67
            tactic ctxt ("getting rid of all remaining perms",
wenzelm@51717
    68
                       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_pi_simp))]
wenzelm@38807
    69
  end;
urbanc@22245
    70
berghofe@30088
    71
fun get_derived_thm ctxt hyp concl orig_thm pi typi =
berghofe@30088
    72
  let
berghofe@30088
    73
    val pi' = Var (pi, typi);
urbanc@30991
    74
    val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
berghofe@30088
    75
    val ([goal_term, pi''], ctxt') = Variable.import_terms false
berghofe@30088
    76
      [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
wenzelm@32429
    77
    val _ = writeln (Syntax.string_of_term ctxt' goal_term);
berghofe@30088
    78
  in
berghofe@30088
    79
    Goal.prove ctxt' [] [] goal_term
wenzelm@38807
    80
      (fn _ => prove_eqvt_tac ctxt' orig_thm pi' pi'') |>
wenzelm@42361
    81
    singleton (Proof_Context.export ctxt' ctxt)
berghofe@30088
    82
  end
urbanc@22245
    83
urbanc@30991
    84
(* replaces in t every variable, say x, with pi o x *)
urbanc@30986
    85
fun apply_pi trm (pi, typi) =
urbanc@30986
    86
let
urbanc@30991
    87
  fun replace n ty =
urbanc@30991
    88
  let 
urbanc@30991
    89
    val c  = Const (@{const_name "perm"}, typi --> ty --> ty) 
urbanc@30991
    90
    val v1 = Var (pi, typi)
urbanc@30991
    91
    val v2 = Var (n, ty)
urbanc@30991
    92
  in
urbanc@30991
    93
    c $ v1 $ v2 
urbanc@30991
    94
  end
urbanc@30986
    95
in
urbanc@30991
    96
  map_aterms (fn Var (n, ty) => replace n ty | t => t) trm
urbanc@30991
    97
end
urbanc@22245
    98
urbanc@22245
    99
(* returns *the* pi which is in front of all variables, provided there *)
urbanc@22245
   100
(* exists such a pi; otherwise raises EQVT_FORM                        *)
urbanc@22245
   101
fun get_pi t thy =
urbanc@22245
   102
  let fun get_pi_aux s =
urbanc@22245
   103
        (case s of
urbanc@30991
   104
          (Const (@{const_name "perm"} ,typrm) $
haftmann@37678
   105
             (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name Product_Type.prod}, [Type (tyatm,[]),_])]))) $
wenzelm@22846
   106
               (Var (n,ty))) =>
urbanc@22245
   107
             let
wenzelm@24039
   108
                (* FIXME: this should be an operation the library *)
wenzelm@30364
   109
                val class_name = (Long_Name.map_base_name (fn s => "pt_"^s) tyatm)
wenzelm@24039
   110
             in
wenzelm@24271
   111
                if (Sign.of_sort thy (ty,[class_name]))
wenzelm@22846
   112
                then [(pi,typi)]
wenzelm@22846
   113
                else raise
wenzelm@22846
   114
                EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
wenzelm@22846
   115
             end
urbanc@22245
   116
        | Abs (_,_,t1) => get_pi_aux t1
urbanc@22245
   117
        | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
wenzelm@22846
   118
        | _ => [])
wenzelm@22846
   119
  in
urbanc@22245
   120
    (* collect first all pi's in front of variables in t and then use distinct *)
urbanc@22245
   121
    (* to ensure that all pi's must have been the same, i.e. distinct returns  *)
urbanc@22245
   122
    (* a singleton-list  *)
wenzelm@22846
   123
    (case (distinct (op =) (get_pi_aux t)) of
urbanc@30986
   124
      [(pi,typi)] => (pi, typi)
urbanc@22418
   125
    | _ => raise EQVT_FORM "All permutation should be the same")
urbanc@22245
   126
  end;
urbanc@22245
   127
wenzelm@26652
   128
(* Either adds a theorem (orig_thm) to or deletes one from the equivariance *)
urbanc@22245
   129
(* lemma list depending on flag. To be added the lemma has to satisfy a     *)
wenzelm@22846
   130
(* certain form. *)
narboux@24265
   131
narboux@24265
   132
fun eqvt_add_del_aux flag orig_thm context = 
wenzelm@22846
   133
  let
urbanc@22245
   134
    val thy = Context.theory_of context
urbanc@22245
   135
    val thms_to_be_added = (case (prop_of orig_thm) of
wenzelm@22846
   136
        (* case: eqvt-lemma is of the implicational form *)
wenzelm@56245
   137
        (Const(@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
wenzelm@22846
   138
          let
urbanc@22245
   139
            val (pi,typi) = get_pi concl thy
urbanc@22245
   140
          in
urbanc@22245
   141
             if (apply_pi hyp (pi,typi) = concl)
wenzelm@22846
   142
             then
urbanc@22245
   143
               (warning ("equivariance lemma of the relational form");
berghofe@30088
   144
                [orig_thm,
berghofe@30088
   145
                 get_derived_thm (Context.proof_of context) hyp concl orig_thm pi typi])
urbanc@22418
   146
             else raise EQVT_FORM "Type Implication"
urbanc@22245
   147
          end
wenzelm@22846
   148
       (* case: eqvt-lemma is of the equational form *)
haftmann@38864
   149
      | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $
urbanc@30991
   150
            (Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
wenzelm@24039
   151
           (if (apply_pi lhs (pi,typi)) = rhs
narboux@22437
   152
               then [orig_thm]
urbanc@22418
   153
               else raise EQVT_FORM "Type Equality")
urbanc@22418
   154
      | _ => raise EQVT_FORM "Type unknown")
wenzelm@22846
   155
  in
wenzelm@26652
   156
      fold (fn thm => Data.map (flag thm)) thms_to_be_added context
urbanc@22245
   157
  end
wenzelm@22846
   158
  handle EQVT_FORM s =>
wenzelm@32091
   159
      error (Display.string_of_thm (Context.proof_of context) orig_thm ^ 
urbanc@30986
   160
               " does not comply with the form of an equivariance lemma (" ^ s ^").")
urbanc@22245
   161
urbanc@22245
   162
urbanc@30991
   163
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm));
urbanc@30991
   164
val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm));
urbanc@22245
   165
urbanc@30991
   166
val eqvt_force_add  = Thm.declaration_attribute (Data.map o Thm.add_thm);
urbanc@30991
   167
val eqvt_force_del  = Thm.declaration_attribute (Data.map o Thm.del_thm);
urbanc@22245
   168
urbanc@30986
   169
val get_eqvt_thms = Context.Proof #> Data.get;
urbanc@22418
   170
urbanc@22245
   171
val setup =
wenzelm@38807
   172
  Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
wenzelm@38807
   173
   "equivariance theorem declaration" #>
wenzelm@38807
   174
  Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
wenzelm@38807
   175
    "equivariance theorem declaration (without checking the form of the lemma)" #>
wenzelm@39557
   176
  Global_Theory.add_thms_dynamic (@{binding eqvts}, Data.get);
urbanc@30986
   177
urbanc@22245
   178
urbanc@22245
   179
end;