src/HOL/Nominal/nominal_thmdecls.ML
author urbanc
Mon, 16 Apr 2007 07:32:23 +0200
changeset 22715 381e6c45f13b
parent 22562 80b814fe284b
child 22846 fb79144af9a3
permissions -rw-r--r--
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
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
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
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
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     7
   By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     8
   in a data-slot in the theory context. Possible modifiers
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,
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    10
   respectively the lemma from the data-slot.  
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
22250
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    15
  val print_data: Proof.context -> unit
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    16
  val eqvt_add: attribute
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    17
  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
    18
  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
    19
  val eqvt_force_del: attribute
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    20
  val setup: theory -> theory
22286
85b065601f45 added get-functions
urbanc
parents: 22250
diff changeset
    21
  val get_eqvt_thms: theory -> thm list
85b065601f45 added get-functions
urbanc
parents: 22250
diff changeset
    22
  val get_fresh_thms: theory -> thm list
85b065601f45 added get-functions
urbanc
parents: 22250
diff changeset
    23
  val get_bij_thms: theory -> thm list
85b065601f45 added get-functions
urbanc
parents: 22250
diff changeset
    24
  
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    25
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    26
  val NOMINAL_EQVT_DEBUG : bool ref
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    27
end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    28
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    29
structure NominalThmDecls: NOMINAL_THMDECLS =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    30
struct
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    31
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    32
structure Data = GenericDataFun
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    33
(
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    34
  val name = "HOL/Nominal/eqvt";
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
    35
  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
    36
  val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    37
  val extend = I;
22541
c33b542394f3 the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
urbanc
parents: 22495
diff changeset
    38
  fun merge _ (r1:T,r2:T) = {eqvts  = Drule.merge_rules (#eqvts r1, #eqvts r2), 
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
    39
                             freshs = Drule.merge_rules (#freshs r1, #freshs r2), 
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
    40
                             bijs   = Drule.merge_rules (#bijs r1, #bijs r2)}
22250
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    41
  fun print context (data:T) =
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    42
    let 
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    43
       fun print_aux msg thms =
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    44
         Pretty.writeln (Pretty.big_list msg
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    45
           (map (ProofContext.pretty_thm (Context.proof_of context)) thms))
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    46
    in
22541
c33b542394f3 the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
urbanc
parents: 22495
diff changeset
    47
      (print_aux "Equivariance lemmas: " (#eqvts data);
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
    48
       print_aux "Freshness lemmas: " (#freshs data);
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
    49
       print_aux "Bijection lemmas: " (#bijs data))
22250
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    50
    end;
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    51
 
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    52
);
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    53
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    54
(* 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
    55
(* 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
    56
(* 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
    57
(* 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
    58
(* 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
    59
(* 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
    60
(* 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
    61
(* together, i.e. are of the right "pt_class", so that a stronger version of the     *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    62
(* eqality-lemma can be derived. *)
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
    63
exception EQVT_FORM of string;
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    64
22250
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    65
val print_data = Data.print o Context.Proof;
22541
c33b542394f3 the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
urbanc
parents: 22495
diff changeset
    66
val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts;
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
    67
val get_fresh_thms = Context.Theory #> Data.get #> #freshs;
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
    68
val get_bij_thms = Context.Theory #> Data.get #> #bijs;
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    69
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    70
(* FIXME: should be a function in a library *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    71
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
    72
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    73
val perm_bool = thm "perm_bool";
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
    74
val perm_fun_def = thm "perm_fun_def";
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    75
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    76
val NOMINAL_EQVT_DEBUG = ref false;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    77
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    78
fun tactic (msg,tac) = 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    79
    if !NOMINAL_EQVT_DEBUG 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    80
    then (EVERY [tac, print_tac ("after "^msg)])
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    81
    else tac 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    82
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
    83
fun dynamic_thms thy name = PureThy.get_thms thy (Name name)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
    84
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    85
fun tactic_eqvt ctx orig_thm pi typi = 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    86
    let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    87
        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
    88
        val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
    89
        val perm_pi_simp = dynamic_thms ctx "perm_pi_simp"
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    90
    in
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    91
        EVERY [tactic ("iffI applied",rtac iffI 1), 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    92
               tactic ("simplifies with orig_thm and perm_bool", 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    93
                          asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1), 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    94
               tactic ("applies orig_thm instantiated with rev pi",
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    95
                          dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    96
               tactic ("getting rid of all remaining perms",
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    97
                          full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)] 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    98
    end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    99
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   100
fun get_derived_thm thy hyp concl orig_thm pi typi =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   101
   let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   102
       val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   103
       val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   104
       val _ = Display.print_cterm (cterm_of thy goal_term) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   105
   in	
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   106
     Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   107
   end
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   108
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   109
(* FIXME: something naughty here, but as long as there is no infrastructure to expose *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   110
(* the eqvt_thm_list to the user, we have to manually update the context and the      *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   111
(* thm-list eqvt *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   112
fun update_context flag thms context =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   113
  let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   114
     val context' = fold (fn thm => Data.map (flag thm)) thms context 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   115
  in 
22541
c33b542394f3 the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
urbanc
parents: 22495
diff changeset
   116
    Context.mapping (snd o PureThy.add_thmss [(("eqvts",(#eqvts (Data.get context'))),[])]) I context'
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   117
  end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   118
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   119
(* replaces every variable x in t with pi o x *) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   120
fun apply_pi trm (pi,typi) =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   121
  let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   122
    fun only_vars t =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   123
       (case t of
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   124
          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
   125
        | _ => t)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   126
  in 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   127
     map_aterms only_vars trm 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   128
  end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   129
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   130
(* 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
   131
(* exists such a pi; otherwise raises EQVT_FORM                        *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   132
fun get_pi t thy =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   133
  let fun get_pi_aux s =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   134
        (case s of
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   135
          (Const ("Nominal.perm",typrm) $ 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   136
             (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   137
               (Var (n,ty))) => 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   138
             let
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   139
		(* FIXME: this should be an operation the library *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   140
                val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   141
	     in 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   142
		if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   143
                then [(pi,typi)] 
22495
c54748fd1f43 clarified an error-message
urbanc
parents: 22437
diff changeset
   144
                else raise 
c54748fd1f43 clarified an error-message
urbanc
parents: 22437
diff changeset
   145
                EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name) 
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   146
             end 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   147
        | Abs (_,_,t1) => get_pi_aux t1
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   148
        | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   149
        | _ => [])  
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   150
  in 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   151
    (* 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
   152
    (* 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
   153
    (* a singleton-list  *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   154
    (case (distinct (op =) (get_pi_aux t)) of 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   155
      [(pi,typi)] => (pi,typi)
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   156
    | _ => 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
   157
  end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   158
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   159
(* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   160
(* lemma list depending on flag. To be added the lemma has to satisfy a     *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   161
(* certain form. *) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   162
fun eqvt_add_del_aux flag orig_thm context =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   163
  let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   164
    val thy = Context.theory_of context
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   165
    val thms_to_be_added = (case (prop_of orig_thm) of
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   166
        (* case: eqvt-lemma is of the implicational form *) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   167
        (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   168
          let  
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   169
            val (pi,typi) = get_pi concl thy
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   170
          in
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   171
             if (apply_pi hyp (pi,typi) = concl)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   172
             then 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   173
               (warning ("equivariance lemma of the relational form");
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   174
                [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
   175
             else raise EQVT_FORM "Type Implication"
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   176
          end
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   177
       (* case: eqvt-lemma is of the equational form *)  
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   178
      | (Const ("Trueprop", _) $ (Const ("op =", _) $ 
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   179
            (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   180
	   (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
   181
               then [orig_thm]
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   182
               else raise EQVT_FORM "Type Equality")
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   183
      | _ => raise EQVT_FORM "Type unknown")
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   184
  in 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   185
      update_context flag thms_to_be_added context
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   186
  end
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   187
  handle EQVT_FORM s => 
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   188
      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
   189
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   190
(* in cases of bij- and freshness, we just add the lemmas to the *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   191
(* data-slot *) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   192
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   193
fun simple_add_del_aux record_access name flag th context = 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   194
   let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   195
     val context' = Data.map (flag th) context
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   196
   in
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   197
     Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context' 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   198
   end
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   199
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
   200
fun bij_add_del_aux f   = simple_add_del_aux #bijs "bijs" f
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
   201
fun fresh_add_del_aux f = simple_add_del_aux #freshs "freshs" f
22541
c33b542394f3 the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
urbanc
parents: 22495
diff changeset
   202
fun eqvt_force_add_del_aux f = simple_add_del_aux #eqvts "eqvts" f
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   203
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
   204
fun eqvt_map f th (r:Data.T)  = {eqvts = (f th (#eqvts r)), freshs = #freshs r, bijs = #bijs r};
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
   205
fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r};
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
   206
fun bij_map f th (r:Data.T)   = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))};
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   207
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   208
val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   209
val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule)); 
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
   210
val eqvt_force_add  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule)); 
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
   211
val eqvt_force_del  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule)); 
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
   212
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   213
val bij_add   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule)); 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   214
val bij_del   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule));
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   215
val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule)); 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   216
val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule));
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   217
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
   218
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   219
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   220
val setup =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   221
  Data.init #>
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   222
  Attrib.add_attributes 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   223
     [("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
   224
      ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
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
   225
                             "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
   226
      ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   227
      ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")];
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   228
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   229
end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   230
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   231
(* Thm.declaration_attribute has type (thm -> Context.generic -> Context.generic) -> attribute *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   232
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   233
(* Drule.add_rule has type thm -> thm list -> thm list *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   234
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   235
(* Data.map has type thm list -> thm list -> Context.generic -> Context.generic *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   236
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   237
(* add_del_args is of type attribute -> attribute -> src -> attribute *)