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