src/HOL/Nominal/nominal_thmdecls.ML
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (22 months ago)
changeset 66983 df83b66f1d94
parent 61268 abe08fb15a12
child 69597 ff784d5a5bfb
permissions -rw-r--r--
proper merge (amending fb46c031c841);
     1 (*  Title:      HOL/Nominal/nominal_thmdecls.ML
     2     Author:     Julien Narboux, TU Muenchen
     3     Author:     Christian Urban, TU Muenchen
     4 
     5 Infrastructure for the lemma collection "eqvts".
     6 
     7 By attaching [eqvt] or [eqvt_force] to a lemma, it will get stored in
     8 a data-slot in the context. Possible modifiers are [... add] and
     9 [... del] for adding and deleting, respectively, the lemma from the
    10 data-slot.
    11 *)
    12 
    13 signature NOMINAL_THMDECLS =
    14 sig
    15   val nominal_eqvt_debug: bool Config.T
    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 end;
    23 
    24 structure NominalThmDecls: NOMINAL_THMDECLS =
    25 struct
    26 
    27 structure Data = Generic_Data
    28 (
    29   type T = thm list
    30   val empty = []
    31   val extend = I
    32   val merge = Thm.merge_thms
    33 )
    34 
    35 (* Exception for when a theorem does not conform with form of an equivariance lemma. *)
    36 (* There are two forms: one is an implication (for relations) and the other is an    *)
    37 (* equality (for functions). In the implication-case, say P ==> Q, Q must be equal   *)
    38 (* to P except that every free variable of Q, say x, is replaced by pi o x. In the   *)
    39 (* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *)
    40 (* be equal to t except that every free variable, say x, is replaced by pi o x. In   *)
    41 (* the implicational case it is also checked that the variables and permutation fit  *)
    42 (* together, i.e. are of the right "pt_class", so that a stronger version of the     *)
    43 (* equality-lemma can be derived. *)
    44 exception EQVT_FORM of string
    45 
    46 val nominal_eqvt_debug = Attrib.setup_config_bool @{binding nominal_eqvt_debug} (K false);
    47 
    48 fun tactic ctxt (msg, tac) =
    49   if Config.get ctxt nominal_eqvt_debug
    50   then tac THEN' (K (print_tac ctxt ("after " ^ msg)))
    51   else tac
    52 
    53 fun prove_eqvt_tac ctxt orig_thm pi pi' =
    54   let
    55     val thy = Proof_Context.theory_of ctxt
    56     val T = fastype_of pi'
    57     val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T --> T) $ pi')
    58     val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"
    59   in
    60     EVERY1 [tactic ctxt ("iffI applied", resolve_tac ctxt @{thms iffI}),
    61             tactic ctxt ("remove pi with perm_boolE", dresolve_tac ctxt @{thms perm_boolE}),
    62             tactic ctxt ("solve with orig_thm", eresolve_tac ctxt [orig_thm]),
    63             tactic ctxt ("applies orig_thm instantiated with rev pi",
    64                dresolve_tac ctxt [infer_instantiate ctxt [(#1 (dest_Var pi), mypifree)] orig_thm]),
    65             tactic ctxt ("getting rid of the pi on the right", resolve_tac ctxt @{thms perm_boolI}),
    66             tactic ctxt ("getting rid of all remaining perms",
    67                        full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_pi_simp))]
    68   end;
    69 
    70 fun get_derived_thm ctxt hyp concl orig_thm pi typi =
    71   let
    72     val pi' = Var (pi, typi);
    73     val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
    74     val ([goal_term, pi''], ctxt') = Variable.import_terms false
    75       [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
    76     val _ = writeln (Syntax.string_of_term ctxt' goal_term);
    77   in
    78     Goal.prove ctxt' [] [] goal_term
    79       (fn _ => prove_eqvt_tac ctxt' orig_thm pi' pi'') |>
    80     singleton (Proof_Context.export ctxt' ctxt)
    81   end
    82 
    83 (* replaces in t every variable, say x, with pi o x *)
    84 fun apply_pi trm (pi, typi) =
    85 let
    86   fun replace n ty =
    87   let 
    88     val c  = Const (@{const_name "perm"}, typi --> ty --> ty) 
    89     val v1 = Var (pi, typi)
    90     val v2 = Var (n, ty)
    91   in
    92     c $ v1 $ v2 
    93   end
    94 in
    95   map_aterms (fn Var (n, ty) => replace n ty | t => t) trm
    96 end
    97 
    98 (* returns *the* pi which is in front of all variables, provided there *)
    99 (* exists such a pi; otherwise raises EQVT_FORM                        *)
   100 fun get_pi t thy =
   101   let fun get_pi_aux s =
   102         (case s of
   103           (Const (@{const_name "perm"} ,typrm) $
   104              (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name Product_Type.prod}, [Type (tyatm,[]),_])]))) $
   105                (Var (n,ty))) =>
   106              let
   107                 (* FIXME: this should be an operation the library *)
   108                 val class_name = (Long_Name.map_base_name (fn s => "pt_"^s) tyatm)
   109              in
   110                 if (Sign.of_sort thy (ty,[class_name]))
   111                 then [(pi,typi)]
   112                 else raise
   113                 EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
   114              end
   115         | Abs (_,_,t1) => get_pi_aux t1
   116         | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
   117         | _ => [])
   118   in
   119     (* collect first all pi's in front of variables in t and then use distinct *)
   120     (* to ensure that all pi's must have been the same, i.e. distinct returns  *)
   121     (* a singleton-list  *)
   122     (case (distinct (op =) (get_pi_aux t)) of
   123       [(pi,typi)] => (pi, typi)
   124     | _ => raise EQVT_FORM "All permutation should be the same")
   125   end;
   126 
   127 (* Either adds a theorem (orig_thm) to or deletes one from the equivariance *)
   128 (* lemma list depending on flag. To be added the lemma has to satisfy a     *)
   129 (* certain form. *)
   130 
   131 fun eqvt_add_del_aux flag orig_thm context = 
   132   let
   133     val thy = Context.theory_of context
   134     val thms_to_be_added =
   135       (case Thm.prop_of orig_thm of
   136         (* case: eqvt-lemma is of the implicational form *)
   137         (Const(@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
   138           let
   139             val (pi,typi) = get_pi concl thy
   140           in
   141              if (apply_pi hyp (pi,typi) = concl)
   142              then
   143                (warning ("equivariance lemma of the relational form");
   144                 [orig_thm,
   145                  get_derived_thm (Context.proof_of context) hyp concl orig_thm pi typi])
   146              else raise EQVT_FORM "Type Implication"
   147           end
   148        (* case: eqvt-lemma is of the equational form *)
   149       | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $
   150             (Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
   151            (if (apply_pi lhs (pi,typi)) = rhs
   152                then [orig_thm]
   153                else raise EQVT_FORM "Type Equality")
   154       | _ => raise EQVT_FORM "Type unknown")
   155   in
   156       fold (fn thm => Data.map (flag thm)) thms_to_be_added context
   157   end
   158   handle EQVT_FORM s =>
   159       error (Thm.string_of_thm (Context.proof_of context) orig_thm ^ 
   160                " does not comply with the form of an equivariance lemma (" ^ s ^").")
   161 
   162 
   163 val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm));
   164 val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm));
   165 
   166 val eqvt_force_add  = Thm.declaration_attribute (Data.map o Thm.add_thm);
   167 val eqvt_force_del  = Thm.declaration_attribute (Data.map o Thm.del_thm);
   168 
   169 val get_eqvt_thms = Context.Proof #> Data.get;
   170 
   171 val setup =
   172   Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
   173    "equivariance theorem declaration" #>
   174   Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
   175     "equivariance theorem declaration (without checking the form of the lemma)" #>
   176   Global_Theory.add_thms_dynamic (@{binding eqvts}, Data.get);
   177 
   178 
   179 end;