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