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