src/HOL/Nominal/nominal_thmdecls.ML
author haftmann
Wed Jun 17 08:13:05 2009 +0200 (2009-06-17 ago)
changeset 31671 81e5e8ffe92f
parent 30991 c814a34f687e
child 32091 30e2ffbba718
permissions -rw-r--r--
datatype packages: record datatype_config for configuration flags; less verbose signatures
berghofe@30088
     1
(* Authors: Julien Narboux and Christian Urban
urbanc@22245
     2
wenzelm@22846
     3
   This file introduces the infrastructure for the lemma
urbanc@30986
     4
   collection "eqvts".
urbanc@22245
     5
urbanc@30991
     6
   By attaching [eqvt] or [eqvt_force] to a lemma, it will get 
urbanc@30986
     7
   stored in a data-slot in the context. Possible modifiers
urbanc@30991
     8
   are [... add] and [... del] for adding and deleting, 
urbanc@30991
     9
   respectively, the lemma from the data-slot.
urbanc@22245
    10
*)
urbanc@22245
    11
urbanc@22245
    12
signature NOMINAL_THMDECLS =
urbanc@22245
    13
sig
urbanc@22245
    14
  val eqvt_add: attribute
urbanc@22245
    15
  val eqvt_del: attribute
urbanc@22715
    16
  val eqvt_force_add: attribute
urbanc@22715
    17
  val eqvt_force_del: attribute
urbanc@22245
    18
  val setup: theory -> theory
urbanc@24571
    19
  val get_eqvt_thms: Proof.context -> thm list
urbanc@22245
    20
urbanc@22245
    21
  val NOMINAL_EQVT_DEBUG : bool ref
urbanc@22245
    22
end;
urbanc@22245
    23
urbanc@22245
    24
structure NominalThmDecls: NOMINAL_THMDECLS =
urbanc@22245
    25
struct
urbanc@22245
    26
urbanc@22245
    27
structure Data = GenericDataFun
urbanc@22245
    28
(
urbanc@30986
    29
  type T = thm list
urbanc@30986
    30
  val empty = []:T
urbanc@30986
    31
  val extend = I
urbanc@30986
    32
  fun merge _ (r1:T, r2:T) = Thm.merge_thms (r1, r2)
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
urbanc@30986
    46
val NOMINAL_EQVT_DEBUG = ref false
urbanc@22245
    47
urbanc@30986
    48
fun tactic (msg, tac) =
urbanc@30986
    49
  if !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' =
urbanc@30986
    54
let
urbanc@30991
    55
  val mypi = Thm.cterm_of ctxt pi
urbanc@30986
    56
  val T = fastype_of pi'
urbanc@30991
    57
  val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T --> T) $ pi')
urbanc@30991
    58
  val perm_pi_simp = PureThy.get_thms ctxt "perm_pi_simp"
urbanc@30986
    59
in
urbanc@30991
    60
  EVERY1 [tactic ("iffI applied", rtac @{thm iffI}),
urbanc@30986
    61
	  tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
urbanc@30986
    62
          tactic ("solve with orig_thm", etac orig_thm),
urbanc@30986
    63
          tactic ("applies orig_thm instantiated with rev pi",
urbanc@30986
    64
                     dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
urbanc@30986
    65
	  tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
urbanc@30986
    66
          tactic ("getting rid of all remaining perms",
urbanc@30986
    67
                     full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))]
urbanc@30986
    68
end;
urbanc@22245
    69
berghofe@30088
    70
fun get_derived_thm ctxt hyp concl orig_thm pi typi =
berghofe@30088
    71
  let
berghofe@30088
    72
    val thy = ProofContext.theory_of ctxt;
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
berghofe@30088
    77
    val _ = Display.print_cterm (cterm_of thy goal_term)
berghofe@30088
    78
  in
berghofe@30088
    79
    Goal.prove ctxt' [] [] goal_term
urbanc@30991
    80
      (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>
berghofe@30088
    81
    singleton (ProofContext.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) $
urbanc@30991
   105
             (Var (pi,typi as Type(@{type_name "list"}, [Type ("*", [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 *)
urbanc@22245
   137
        (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("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 *)
urbanc@30986
   149
      | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
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 =>
urbanc@30986
   159
      error (Display.string_of_thm 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 =
urbanc@30986
   172
    Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
urbanc@30986
   173
     "equivariance theorem declaration" 
urbanc@30986
   174
 #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
urbanc@30986
   175
     "equivariance theorem declaration (without checking the form of the lemma)" 
urbanc@30986
   176
 #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get) 
urbanc@30986
   177
urbanc@22245
   178
urbanc@22245
   179
end;